dpllt_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).

add_wd_po_to_pred(Pred, WDAcc, IsTopLevel, NWDAcc, WDPred, WDPoConj) :-
    Pred = b(Expr, Type, Info),
    add_wd_po_to_pred_e(Expr, Type, Info, WDAcc, IsTopLevel, NWDAcc, WDPred, WDPoConj).

add_wd_po_to_pred_e(Expr, pred, Info, WDAcc, IsTopLevel, NWDAcc, WDPred, WDPoConj) :-
    functor(Expr, Functor, 2),
    (Functor == conjunct; Functor == disjunct; Functor == implication; Functor == equivalence),
    !,
    arg(1, Expr, A),
    arg(2, Expr, B),
    add_wd_po_to_pred(A, WDAcc, IsTopLevel, NWDAcc1, WDA, WDAConj),
    add_wd_po_to_pred(B, NWDAcc1, IsTopLevel, NWDAcc, WDB, WDBConj),
    functor(NExpr, Functor, 2),
    arg(1, NExpr, WDA),
    arg(2, NExpr, WDB),
    conjunct_predicates([WDAConj,WDBConj], WDPoConj),
    safe_create_texpr(NExpr, pred, Info, WDPred).

add_wd_po_to_pred_e(if_then_else(Cond,Lhs,Rhs), pred, Info, WDAcc, IsTopLevel, NWDAcc, WDPred, WDPoConj) :-
    !,
    add_wd_po_to_pred(Cond, WDAcc, IsTopLevel, NWDAcc1, WDCond, WDPoConj1),
    add_wd_po_to_pred(Lhs, NWDAcc1, IsTopLevel, NWDAcc2, WDLhs, WDPoConj2),
    add_wd_po_to_pred(Rhs, NWDAcc2, IsTopLevel, NWDAcc, WDRhs, WDPoConj3),
    safe_create_texpr(if_then_else(WDCond,WDLhs,WDRhs), pred, Info, WDPred),
    conjunct_predicates([WDPoConj1,WDPoConj2,WDPoConj3], WDPoConj).

add_wd_po_to_pred_e(forall(Ids,Lhs,Rhs), pred, Info, WDAcc, _, NWDAcc, WDPred, _) :-
    !,
    add_wd_po_to_pred(Rhs, WDAcc, false, NWDAcc, WDRhs, _),
    safe_create_texpr(forall(Ids,Lhs,WDRhs), pred, Info, WDPred).

add_wd_po_to_pred_e(Expr, pred, Info, WDAcc, _, NWDAcc, WDPred, _) :-
    Expr =.. [Functor,Ids,Eqs,Body],
    (Functor == let; Functor == let_predicate),
    !,
    add_wd_po_to_pred(Body, WDAcc, false, NWDAcc, WDBody, _),
    NExpr =.. [Functor,Ids,Eqs,WDBody],
    safe_create_texpr(NExpr, pred, Info, WDPred).

add_wd_po_to_pred_e(Expr, Type, Info, WDAcc, _, NWDAcc, WDPred, _) :-
    Expr =.. [Functor,Ids,Body],
    quantified_binary_expr(Functor),
    !,
    add_wd_po_to_pred(Body, WDAcc, false, NWDAcc, WDBody, _),
    NExpr =.. [Functor,Ids,WDBody],
    safe_create_texpr(NExpr, Type, Info, WDPred).

add_wd_po_to_pred_e(Expr, Type, Info, WDAcc, IsTopLevel, NWDAcc, WDPred, WDPoConj) :-
    % e.g., for a = b - {some set comprehension with WD}, we want to add WD POs to the set comprehension but not the equality
    functor(Expr, Functor, 2),
    Functor \== partition,
    Expr =.. [Functor|Args],
    map_add_wd_po_to_pred(Args, WDAcc, false, NWDAcc1, WDArgs, _),
    NExpr =.. [Functor|WDArgs],
    NPred = b(NExpr,Type,Info),
    !,
    ( Type == pred,
    get_all_top_level_wd_pos(NPred, WDPos),
    WDPos \== [],
    create_wd_impls(WDPos, NPred, [], WDImpls),
    conjunct_predicates(WDPos, WDPoConj) % don't use added info is_wd_po_for_dpllt here
    -> debug_format_pred("--------------------------Add WD PO for pred~n", [], NPred),
    ( IsTopLevel == true
    -> add_wd_impls_to_acc(WDImpls, NWDAcc1, NWDAcc)
    ; NWDAcc = NWDAcc1
    ),
    maplist(map_add_texpr_infos([is_wd_po_for_dpllt]), WDPos, NWDPos),
    conjunct_predicates(NWDPos, WDPo),
    conjunct_predicates([WDPo,NPred], WDPred)
    ; WDPred = NPred,
    NWDAcc = NWDAcc1
).

add_wd_po_to_pred_e(Expr, Type, Info, WDAcc, _, WDAcc, b(Expr,Type,Info), _).

clean_up_pred_cut(Pred, Clean) :-
    clean_up_pred(Pred, _, TClean), !,
    Clean = TClean.

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

create_wd_impls([WDPo|T], Pred, Acc, WDImpls) :-
    % don't use added info is_wd_po_for_dpllt here
    safe_create_texpr(disjunct(b(negation(Pred),pred,[]),WDPo), pred, [], WDImpl),
    create_wd_impls(T, Pred, [WDImpl|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_all_top_level_wd_pos(Pred, WDPos) :-
    findall(WDPo, get_top_level_wd_po_no_typing(Pred, WDPo), TWDPos), !,
    remove_duplicate_preds(TWDPos, WDPos).

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_top_level_wd_po_no_typing(Pred, WDPo) :-
    empty_hyps(Hyps),
    find_identifier_uses(Pred, [], TopLevelIds),
    compute_wd(Pred, Hyps, [discharge_po,skip_finite_po], TWDPo), % choicepoint
    find_identifier_uses(TWDPo, [], WDIds),
    subtract(WDIds, TopLevelIds, QIds),
    QIds == [], % is top-level
    TWDPo = b(_,_,TWDInfo),
    ( member(discharged(true, _), TWDInfo)
    -> debug_format_pred('Removed discharged predicate from WD POs: ', [], TWDPo),
    fail
    ; true
    ),
    % important to use b_ast_cleanup:clean_up_pred/3 for WD POs collected by compute_wd/4 since
    % typing constraints are optimized to 'typeset' nodes, which is undone by the cleanup.
    clean_up_pred_cut(TWDPo, WDPo),
    ( is_typing_pred_without_wd(WDPo)
    -> debug_format_pred('Removed typing predicate from WD POs: ', [], WDPo),
    fail
    ; true
).

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

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

is_typing_pred_without_wd(b(member(Id,B),pred,_)) :-
    B \= b(domain(_),_,_),
    B \= b(seq(_),_,_), % seq typing has a wd condition
    Id = b(identifier(_),_,_).

is_typing_pred_without_wd(b(subset(Id,B),pred,_)) :-
    B \= b(domain(_),_,_),
    B \= b(seq(_),_,_),
    Id = b(identifier(_),_,_).

is_typing_pred_without_wd(b(subset_strict(Id,B),pred,_)) :-
    B \= b(domain(_),_,_),
    B \= b(seq(_),_,_),
    Id = b(identifier(_),_,_).

map_add_texpr_infos(ToBeAdded, Ast, NAst) :-
    add_texpr_infos(Ast, ToBeAdded, NAst).

map_add_wd_po_to_pred([Arg|T], WDAcc, IsTopLevel, NWDAcc, [WDArg|TWDArgs], WDConj) :-
    add_wd_po_to_pred(Arg, WDAcc, IsTopLevel, NWDAcc1, WDArg, WDConjArg),
    map_add_wd_po_to_pred_acc(T, NWDAcc1, IsTopLevel, NWDAcc, WDConjArg, TWDArgs, WDConj).

map_add_wd_po_to_pred_acc([], WDAcc, _, WDAcc, WDConjAcc, [], WDConjAcc).

map_add_wd_po_to_pred_acc([Arg|T], WDAcc, IsTopLevel, NWDAcc, WDConjAcc, [WDArg|TWDArgs], WDConj) :-
    add_wd_po_to_pred(Arg, WDAcc, IsTopLevel, NWDAcc1, WDArg, WDConjArg),
    ( ground(WDConjArg)
    -> safe_create_texpr(conjunct(WDConjArg,WDConjAcc),pred,[],NWDConjAcc)
    ; NWDConjAcc = WDConjAcc
    ),
    map_add_wd_po_to_pred_acc(T, NWDAcc1, IsTopLevel, NWDAcc, NWDConjAcc, TWDArgs, WDConj).

map_predicate_to_sat(_, WDAcc, VarAcc, Env, [], Env, WDAcc, [], VarAcc).

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(b(truth,pred,Info)), _, _, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Falsity, VarAccOut) :-
    !,
    EnvOut = Env,
    VarAccOut = Acc,
    NWDAcc = WDAcc,
    Falsity = b(falsity,pred,Info).

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

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(negation(b(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_e(negation(Pred), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, Pred, boolean_false, TNewEnv, TWDPOs, TBoolFormula, TNVarAcc),
    !,
    NewEnv = TNewEnv,
    WDPOs = TWDPOs,
    BoolFormula = TBoolFormula,
    NVarAcc = TNVarAcc.

predicate_to_sat_e(negation(Pred), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    Pred = b(disjunct(A,B),pred,_),
    !,
    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_e(negation(Pred), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    Pred = b(conjunct(A,B),pred,_),
    !,
    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_e(negation(Pred), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    Pred = b(implication(A,B),pred,_),
    !,
    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_e(negation(Pred), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
    Pred = b(equivalence(A,B),pred,_),
    !,
    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).

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).

quantified_binary_expr(exists).

quantified_binary_expr(comprehension_set).

quantified_binary_expr(event_b_comprehension_set).

quantified_binary_expr(lambda).

quantified_binary_expr(general_sum).

quantified_binary_expr(general_product).

quantified_binary_expr(quantified_union).

quantified_binary_expr(quantified_intersection).

quantified_expr(forall(Ids,Lhs,Rhs), forall, Ids, [Lhs,Rhs]).

quantified_expr(exists(Ids,Body), exists, Ids, [Body]).

quantified_expr(comprehension_set(Ids,Body), comprehension_set, Ids, [Body]).

quantified_expr(event_b_comprehension_set(Ids,Body), event_b_comprehension_set, Ids, [Body]).

quantified_expr(lambda(Ids,Body), lambda, Ids, [Body]).

quantified_expr(general_sum(Ids,Body), general_sum, Ids, [Body]).

quantified_expr(general_product(Ids,Body), general_product, Ids, [Body]).

quantified_expr(quantified_union(Ids,Body), quantified_union, Ids, [Body]).

quantified_expr(quantified_intersection(Ids,Body), quantified_intersection, Ids, [Body]).

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).

remove_duplicate_preds(Constraints, NoDups) :-
    remove_duplicate_preds(Constraints, [], [], NoDups).

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

remove_duplicate_preds([Pred|T], NormAcc, Acc, NoDups) :-
    norm_pred_check(Pred, NPred),
    ( memberchk(NPred, NormAcc)
    -> NAcc = Acc,
    NNormAcc = NormAcc
    ; NAcc = [Pred|Acc],
    NNormAcc = [NPred|NormAcc]
    ),
    remove_duplicate_preds(T, NNormAcc, NAcc, NoDups).

remove_wd_pos_introduced_for_dpllt(Remove, Conj, NConj) :-
    conjunction_to_list(Conj, List),
    remove_wd_pos_introduced_for_dpllt_l(Remove, List, NList),
    conjunct_predicates(NList, NConj).

remove_wd_pos_introduced_for_dpllt_keep_toplevel(Conj, NConj) :-
    remove_wd_pos_introduced_for_dpllt(false, Conj, NConj).

remove_wd_pos_introduced_for_dpllt_l(_, [], []).

remove_wd_pos_introduced_for_dpllt_l(Remove, [b(negation(Pred),pred,NInfo)|T], [Out|NT]) :-
    !,
    remove_wd_pos_introduced_for_dpllt(true, Pred, NPred),
    Out = b(negation(NPred),pred,NInfo),
    remove_wd_pos_introduced_for_dpllt_l(Remove, T, NT).

remove_wd_pos_introduced_for_dpllt_l(Remove, [Pred|T], [Out|NT]) :-
    Pred = b(Expr,Type,Info),
    quantified_expr(Expr, Functor, Ids, Subs),
    !,
    maplist(remove_wd_pos_introduced_for_dpllt(true), Subs, NSubs),
    NExpr =.. [Functor,Ids|NSubs],
    Out = b(NExpr,Type,Info),
    remove_wd_pos_introduced_for_dpllt_l(Remove, T, NT).

remove_wd_pos_introduced_for_dpllt_l(Remove, [Pred|T], Out) :-
    Pred = b(_,_,Info),
    memberchk(is_wd_po_for_dpllt, Info),
    !,
    ( Remove == true
    -> Out = NT,
    debug_format_pred("-----------------------removed wd po from unsat core: ", [], Pred)
    ; Out = [Pred|NT]
    ),
    remove_wd_pos_introduced_for_dpllt_l(Remove, T, NT).

remove_wd_pos_introduced_for_dpllt_l(Remove, [Pred|T], [Out|NT]) :-
    Pred = b(Expr,Type,Info),
    functor(Expr, Functor, 2),
    Functor \== external_pred_call,
    !,
    arg(1, Expr, Arg1),
    arg(2, Expr, Arg2),
    remove_wd_pos_introduced_for_dpllt(Remove, Arg1, NArg1),
    remove_wd_pos_introduced_for_dpllt(Remove, Arg2, NArg2),
    functor(NExpr, Functor, 2),
    arg(1, NExpr, NArg1),
    arg(2, NExpr, NArg2),
    Out = b(NExpr,Type,Info),
    remove_wd_pos_introduced_for_dpllt_l(Remove, T, NT).

remove_wd_pos_introduced_for_dpllt_l(Remove, [Pred|T], [Pred|NT]) :-
    remove_wd_pos_introduced_for_dpllt_l(Remove, T, NT).

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 \== only_reuse,
    !,
    next_sat_var_name(SatVarName),
    add_wd_po_to_pred(Pred, WDAcc, true, NWDAcc, WDPred, TopLevelWdPred),
    debug_format_pred("Introduce sat var ~w for pred~n", [SatVarName], WDPred),
    safe_create_texpr(identifier(SatVarName), boolean, [], TUniqueId),
    %find_identifier_uses(Pred, [], UsedIds),
    ( ground(TopLevelWdPred)
    -> 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].

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).