cdclt_pred_to_sat

add_wd_impls_to_acc([], WDAcc, WDAcc).

add_wd_impls_to_acc([WDImpl|T], WDAcc, NWDAcc) :-
    member(WDImpl, WDAcc),
    !,
    add_wd_impls_to_acc(T, WDAcc, NWDAcc).

add_wd_impls_to_acc([WDImpl|T], WDAcc, NWDAcc) :-
    add_wd_impls_to_acc(T, [WDImpl|WDAcc], NWDAcc).

collect_toplevel_wd_preds(b(Node,Type,Info), TopLevelWdPred, WDAcc, NWDAcc) :-
    collect_toplevel_wd_preds_e(Node, Type, Info, TopLevelWdPred, WDAcc, NWDAcc).

collect_toplevel_wd_preds_e(conjunct(A,B), _, Info, A, WDAcc, NWDAcc) :-
    member(fuzzed_with_wd_po_included, Info),
    conjunction_to_list(A, WDPOs),
    create_wd_impls(WDPOs, B, [], WDImpls),
    add_wd_impls_to_acc(WDImpls, WDAcc, NWDAcc).

collect_toplevel_wd_preds_e(Node, _, _, TopLevelWdPred, WDAcc, NWDAcc) :-
    Node =.. [_,A,B],
    collect_toplevel_wd_preds(A, TopLevelWdPred1, WDAcc, NWDAcc1),
    collect_toplevel_wd_preds(B, TopLevelWdPred2, NWDAcc1, NWDAcc),
    safe_create_texpr(conjunct(TopLevelWdPred1,TopLevelWdPred2), pred, [], TopLevelWdPred).

collect_toplevel_wd_preds_e(_, _, _, b(truth,pred,[]), WDAcc, WDAcc).

create_wd_impls([], _, Acc, Acc).

create_wd_impls([WDPo|T], Pred, Acc, WDImpls) :-
    % don't use added info is_wd_po_for_cdclt here
    NegP = b(negation(Pred),pred,[]),
    safe_create_texpr(disjunct(NegP,WDPo), pred, [], WDImpl1),
    safe_create_texpr(disjunct(WDPo,NegP), pred, [], WDImpl2),
    create_wd_impls(T, Pred, [WDImpl1,WDImpl2|Acc], WDImpls).

debug_format_pred(_, _, _) :-
    print_logs(false),
    !.

debug_format_pred(Msg, Vars, Pred) :-
    format(Msg, Vars),
    print_bexpr(Pred), nl, !.

empty_predicate_env(E) :- empty_avl(E).

fetch_predicate(Pred,Env,StoredPred,SatVar) :- (var(Env) ; \+ is_avl(Env)),!,
    add_internal_error('Illegal env:',fetch_predicate(Pred,Env,StoredPred,SatVar)), fail.

fetch_predicate(Pred,Env,StoredPred,SatVar) :-
    norm_pred_check(Pred, NPred),
    avl_fetch(NPred,Env,pred2satvar(StoredPred,SatVar)), !.

get_amount_of_sat_variables(AmountOfVars) :-
    sat_var_id(AmountOfVars).

get_smt_formula_from_binding(Binding, SatVars, SMT, RestSatVars) :-
    ground(Binding),
    get_var_and_value_from_binding(Binding, SatVarName, Value),
    !,
    select(b(identifier(SatVarName),_,Info), SatVars, RestSatVars),
    member(smt_formula(TSMT), Info),!,
    ( Value == pred_true
    -> SMT = TSMT
    ; Value == pred_false,
    TSMT = b(_,_,TSMTInfo),
    safe_create_texpr(negation(TSMT), pred, TSMTInfo, SMT)
).

get_var_and_value_from_binding(bind(SatVarName,Value), SatVarName, Value).

get_var_and_value_from_binding(binding(SatVarName,Value,_), SatVarName, Value).

map_predicate_to_sat(_, WDAcc, VarAcc, Env, [], Env, WDAcc, BoolFormulas, VarAcc) :- !, BoolFormulas=[].

map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, [Pred|T], NewEnv, WDPOs, [BoolFormula|NT], NVarAcc) :-
    predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, Pred, TempEnv, TWDAcc, BoolFormula, TVarAcc),
    map_predicate_to_sat(ReuseType, TWDAcc, TVarAcc, TempEnv, T, NewEnv, WDPOs, NT, NVarAcc).

negate_bool_atom(boolean_true, boolean_false).

negate_bool_atom(boolean_false, boolean_true).

negate_pred(greater_equal(A,B), less(A,B)).

negate_pred(greater(A,B), less_equal(A,B)).

negate_pred(less_equal(A,B), less(B,A)).

negate_pred(less(A,B), less_equal(B,A)).

next_sat_var_name(SatVarName) :-
    retract(sat_var_id(Old)),
    New is Old + 1,
    asserta(sat_var_id(New)),
    number_codes(New, NC),
    atom_codes(Index, NC),
    atom_concat('sat', Index, SatVarName).

predicate_to_sat(Type, Pred, NewEnv, WDPOs, BoolFormula, VarAcc) :-
    empty_predicate_env(Env),
    predicate_to_sat(Type, [], [], Env, Pred, NewEnv, WDPOs, BoolFormula, VarAcc).

predicate_to_sat(ReuseType, WDAcc, Acc, Env, Pred, NewEnv, WDPOs, BoolFormula, VarAcc) :-
    Pred = b(Expr, Type, Info),
    predicate_to_sat_e(Expr, Type, Info, ReuseType, WDAcc, Acc, Env, NewEnv, WDPOs, BoolFormula, VarAcc).

predicate_to_sat_e(negation(Expr), _, _, ReuseType, WDAcc, Acc, Env, NewEnv, WDPOs, BoolFormula, VarAcc) :-
    predicate_to_sat_neg(Expr, ReuseType, WDAcc, Acc, Env, NewEnv, WDPOs, BoolFormula, VarAcc).

predicate_to_sat_e(truth, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Truth, VarAccOut) :-
    !,
    EnvOut = Env,
    VarAccOut = Acc,
    NWDAcc = WDAcc,
    Truth = b(truth,pred,Info).

predicate_to_sat_e(falsity, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Falsity, VarAccOut) :-
    !,
    EnvOut = Env,
    VarAccOut = Acc,
    NWDAcc = WDAcc,
    Falsity = b(falsity,pred,Info).

predicate_to_sat_e(conjunct(A,B), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    conjunction_to_list(b(conjunct(A,B),pred,[]), PList),
    !,
    map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, PList, NewEnv, WDPOs, SatList, NVarAcc),
    conjunct_predicates(SatList, BoolFormula).

predicate_to_sat_e(disjunct(A,B), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    disjunction_to_list(b(disjunct(A,B),pred,[]), PList),
    !,
    map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, PList, NewEnv, WDPOs, SatList, NVarAcc),
    disjunct_predicates(SatList, BoolFormula).

predicate_to_sat_e(Expr, _, _, _, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, VarAccOut) :-
    ( Expr == value(pred_true)
    ; Expr == value(pred_false)
    ),
    !,
    WDPOs = WDAcc,
    VarAccOut = VarAcc,
    safe_create_texpr(Expr, pred, [], BoolFormula),
    NewEnv = Env.

predicate_to_sat_e(implication(Lhs,Rhs), pred, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    !,
    map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, [Lhs,Rhs], NewEnv, WDPOs, NSatArgs, NVarAcc),
    NSatArgs = [NSatLhs,NSatRhs],
    safe_create_texpr(implication(NSatLhs,NSatRhs), pred, [smt_formula(b(implication(Lhs,Rhs),pred,Info))], BoolFormula).

predicate_to_sat_e(equivalence(Lhs,Rhs), pred, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    !,
    map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, [Lhs,Rhs], NewEnv, WDPOs, NSatArgs, NVarAcc),
    NSatArgs = [NSatLhs,NSatRhs],
    safe_create_texpr(equivalence(NSatLhs,NSatRhs), pred, [smt_formula(b(equivalence(Lhs,Rhs),pred,Info))], BoolFormula).

predicate_to_sat_e(Expr, Type, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    functor(Expr, _, Arity),
    ( Arity == 2
    ; Arity == 3
    ),
    !,
    reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, b(Expr,Type,Info), boolean_true, NewEnv, WDPOs, BoolFormula, NVarAcc).

predicate_to_sat_e(Expr, Type, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    % formula is a singleton pred which is not splitted such as a subset
    reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, b(Expr,Type,Info), boolean_true, NewEnv, WDPOs, BoolFormula, NVarAcc).

predicate_to_sat_neg(Ast, ReuseType, WDAcc, Acc, Env, EnvOut, NWDAcc, NAst, VarAccOut) :-
    Ast = b(Expr,Type,Info),
    predicate_to_sat_neg_e(Expr, Type, Info, ReuseType, WDAcc, Acc, Env, EnvOut, NWDAcc, NAst, VarAccOut).

predicate_to_sat_neg_e(truth, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Falsity, VarAccOut) :-
    !,
    EnvOut = Env, VarAccOut = Acc,
    NWDAcc = WDAcc,
    Falsity = b(falsity,pred,Info).

predicate_to_sat_neg_e(falsity, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Truth, VarAccOut) :-
    !,
    EnvOut = Env, VarAccOut = Acc,
    NWDAcc = WDAcc,
    Truth = b(truth,pred,Info).

predicate_to_sat_neg_e(negation(Pred), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    !,
    predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, Pred, NewEnv, WDPOs, BoolFormula, NVarAcc).

predicate_to_sat_neg_e(Expr, Type, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, b(Expr,Type,Info), boolean_false, TNewEnv, TWDPOs, TBoolFormula, TNVarAcc),
    !,
    NewEnv = TNewEnv,
    WDPOs = TWDPOs,
    BoolFormula = TBoolFormula,
    NVarAcc = TNVarAcc.

predicate_to_sat_neg_e(disjunct(A,B), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    !,
    predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, b(negation(A),pred,[]), NewEnv1, WDAcc1, ABoolFormula, NVarAcc1),
    predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(B),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc),
    % conjunct_predicate/ ensures that truth and falsity are simplified (1)
    conjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula).

predicate_to_sat_neg_e(conjunct(A,B), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    !,
    predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, b(negation(A),pred,[]), NewEnv1, WDAcc1, ABoolFormula, NVarAcc1),
    predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(B),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc),
    % see above comment (1) for conjunct_predicates/2
    disjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula).

predicate_to_sat_neg_e(implication(A,B), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    !,
    predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, A, NewEnv1, WDAcc1, ABoolFormula, NVarAcc1),
    predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(B),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc),
    % see (1)
    conjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula).

predicate_to_sat_neg_e(equivalence(A,B), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    !,
    predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, b(negation(b(implication(A,B),pred,[])),pred,[]), NewEnv1, WDAcc1, ABoolFormula, NVarAcc1),
    predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(b(implication(B,A),pred,[])),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc),
    % see (1)
    disjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula).

register_predicate(Pred,WDPred,Env,UniqueId,NewEnv) :-
    ( var(Env)
    ; \+ is_avl(Env)
    ),
    !,
    add_internal_error('Illegal env:', register_predicate(Pred,WDPred,Env,UniqueId,NewEnv)),
    NewEnv = Env.

register_predicate(Pred,WDPred,Env,UniqueId,NewEnv) :- %print('storing: '), writeq(WDPred),nl,
    norm_pred_check(Pred, NPred),
    avl_store(NPred,Env,pred2satvar(WDPred,UniqueId),NewEnv).

reset_sat_var_id :-
    retractall(sat_var_id(_)),
    asserta(sat_var_id(0)).

reuse_or_introduce_bool_var(_, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :-
    fetch_predicate(Pred, Env, _, SatVar),
    !,
    safe_create_texpr(equal(SatVar,b(BoolAtom,boolean,[])), pred, [], BoolFormula),
    NewEnv = Env,
    NWDAcc = WDAcc,
    NVarAcc = VarAcc.

reuse_or_introduce_bool_var(_, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :-
    Pred = b(Expr,Type,Info),
    negate_pred(Expr, NExpr),
    fetch_predicate(b(NExpr,Type,Info), Env, _, SatVar),
    !,
    negate_bool_atom(BoolAtom, NBoolAtom),
    safe_create_texpr(equal(SatVar,b(NBoolAtom,boolean,[])), pred, [], BoolFormula),
    NewEnv = Env,
    NWDAcc = WDAcc,
    NVarAcc = VarAcc.

reuse_or_introduce_bool_var(Type, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :-
    Type == normal,
    !,
    next_sat_var_name(SatVarName),
    debug_format_pred("Introduce sat var ~w for pred~n", [SatVarName], Pred),
    safe_create_texpr(identifier(SatVarName), boolean, [], TUniqueId),
    add_texpr_infos(TUniqueId, [smt_formula(Pred)], UniqueId),
    register_predicate(Pred,Pred,Env,UniqueId,NewEnv),
    safe_create_texpr(equal(UniqueId,b(BoolAtom,boolean,[])), pred, [], BoolFormula),
    NWDAcc = WDAcc,
    NVarAcc = [UniqueId|VarAcc].

reuse_or_introduce_bool_var(Type, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :-
    Type == normal_make_wd,
    !,
    next_sat_var_name(SatVarName),
    ensure_wd(Pred, WDPred),
    collect_toplevel_wd_preds(WDPred, TopLevelWdPred, WDAcc, NWDAcc),
    debug_format_pred("Introduce sat var ~w for pred~n", [SatVarName], WDPred),
    safe_create_texpr(identifier(SatVarName), boolean, [], TUniqueId),
    %find_identifier_uses(Pred, [], UsedIds),
    ( TopLevelWdPred \= b(truth,_,_)
    -> add_texpr_infos(TUniqueId, [smt_formula(WDPred),contains_top_level_wd_condition(TopLevelWdPred,Pred)], UniqueId)
    ; add_texpr_infos(TUniqueId, [smt_formula(WDPred)], UniqueId)
    ),
    register_predicate(Pred,WDPred,Env,UniqueId,NewEnv),
    safe_create_texpr(equal(UniqueId,b(BoolAtom,boolean,[])), pred, [], BoolFormula),
    NVarAcc = [UniqueId|VarAcc].

reuse_or_introduce_bool_var(Type, _, _, _, Pred, _, _, _, _, _) :-
    Type == only_reuse,
    add_error_fail(reuse_or_introduce_bool_var, 'Missing SAT variable for SMT constraint. b_interpreter_check:norm_pred_check/2 might be inconsistent.', [Pred]).

sat_to_predicate_from_solution([], _, b(truth,pred,[])).

sat_to_predicate_from_solution([Binding|T], SatVars, Conjunction) :-
    get_smt_formula_from_binding(Binding, SatVars, SMT, RestSatVars),
    !,
    sat_to_predicate_from_solution(T, SMT, RestSatVars, Conjunction).

sat_to_predicate_from_solution([_|T], SatVars, Conjunction) :-
    % skip: binding might be a variable if instantiation is not required
    sat_to_predicate_from_solution(T, SatVars, Conjunction).

sat_to_predicate_from_solution([], SmtAcc, _, SmtAcc).

sat_to_predicate_from_solution([Binding|T], SmtAcc, SatVars, Conjunction) :-
    get_smt_formula_from_binding(Binding, SatVars, SMT, RestSatVars),
    !,
    safe_create_texpr(conjunct(SMT,SmtAcc), pred, [], NewSmtAcc),
    sat_to_predicate_from_solution(T, NewSmtAcc, RestSatVars, Conjunction).

sat_to_predicate_from_solution([_|T], SmtAcc, SatVars, Conjunction) :-
    sat_to_predicate_from_solution(T, SmtAcc, SatVars, Conjunction).

sat_var_id(0).