dpllt_preprocessing

ast_not_in_candidate_acc(var, global, AstClean, candidate_impls(global(Global),integer(_),integer_ground(_),set(_),set_ground(_))) :-
    \+ member(AstClean, Global).

ast_not_in_candidate_acc(var, integer, AstClean, candidate_impls(global(_),integer(Integer),integer_ground(_),set(_),set_ground(_))) :-
    \+ member(AstClean, Integer).

ast_not_in_candidate_acc(ground, integer, AstClean, candidate_impls(global(_),integer(_),integer_ground(IntegerGrnd),set(_),set_ground(_))) :-
    \+ member(AstClean, IntegerGrnd).

ast_not_in_candidate_acc(var, set, AstClean, candidate_impls(global(_),integer(_),integer_ground(_),set(Set),set_ground(_))) :-
    \+ member(AstClean, Set).

ast_not_in_candidate_acc(ground, set, AstClean, candidate_impls(global(_),integer(_),integer_ground(_),set(_),set_ground(SetGrnd))) :-
    \+ member(AstClean, SetGrnd).

b_function(total_function(Domain,_), Domain).

b_function(total_surjection(Domain,_), Domain).

b_function(total_injection(Domain,_), Domain).

b_function(total_bijection(Domain,_), Domain).

b_function(partial_function(Domain,_), Domain).

b_function(partial_surjection(Domain,_), Domain).

b_function(partial_injection(Domain,_), Domain).

b_function(partial_bijection(Domain,_), Domain).

b_function(surjection_relation(Domain,_), Domain).

b_function(total_relation(Domain,_), Domain).

b_function(relations(Domain,_), Domain).

b_function_membership(b(member(Id,Function),pred,_), Id, Domain) :-
    get_texpr_expr(Function, Expr),
    b_function(Expr, Domain).

build_implications_from_ground_candidates(GrndCandidateImpl, Partners, PartialImplsConj) :-
    build_implications_from_ground_candidates(GrndCandidateImpl, Partners, [], PartialImplsConj).

build_implications_from_ground_candidates(_, [], Acc, PartialImplsConj) :-
    conjunct_predicates(Acc, PartialImplsConj).

build_implications_from_ground_candidates(GrndCandidateImpl, [Partner|T], Acc, PartialImplsConj) :-
    safe_create_texpr(negation(GrndCandidateImpl), pred, [], NegGrndCandidateImpl),
    NegPartner = b(negation(Partner),pred,[]),
    % possibly remove zero var from idl solver
    safe_create_texpr(disjunct(NegGrndCandidateImpl,Partner), pred, [], Impl1),
    remove_zero_var(Impl1, Impl1NoZero),
    safe_create_texpr(disjunct(NegPartner,GrndCandidateImpl), pred, [], Impl2),
    remove_zero_var(Impl2, Impl2NoZero),
    safe_create_texpr(disjunct(NegGrndCandidateImpl,b(negation(Partner),pred,[])), pred, [], Impl3),
    remove_zero_var(Impl3, Impl3NoZero),
    safe_create_texpr(disjunct(NegPartner,b(negation(GrndCandidateImpl),pred,[])), pred, [], Impl4),
    remove_zero_var(Impl4, Impl4NoZero),
    ( %nl,write('Try Impl1: '), nl, translate:print_bexpr(Impl1NoZero), nl,
    prove_sequent(Impl1NoZero)% write('True'),nl
    -> NewAcc = [Impl1|Acc]
    ; %nl,write('Try Impl2: '), nl, translate:print_bexpr(Impl2NoZero), nl,
    prove_sequent(Impl2NoZero)% write('True'),nl
    -> NewAcc = [Impl2|Acc]
    ; %nl,write('Try Impl3: '), nl, translate:print_bexpr(Impl3NoZero), nl,
    prove_sequent(Impl3NoZero)% write('True'),nl
    -> NewAcc = [Impl3|Acc]
    ; %nl,write('Try Impl4: '), nl, translate:print_bexpr(Impl4NoZero), nl,
    prove_sequent(Impl4NoZero)% write('True'),nl
    -> NewAcc = [Impl4|Acc]
    ; NewAcc = Acc
    ),
    build_implications_from_ground_candidates(GrndCandidateImpl, T, NewAcc, PartialImplsConj).

candidate_impl_binary_operator(equal, global).

candidate_impl_binary_operator(member, global).

candidate_impl_binary_operator(equal, integer).

candidate_impl_binary_operator(member, integer).

candidate_impl_binary_operator(equal, set).

candidate_impl_binary_operator(less, integer).

candidate_impl_binary_operator(less_equal, integer).

candidate_impl_binary_operator(greater, integer).

candidate_impl_binary_operator(greater_equal, integer).

candidate_impl_binary_operator(member, set).

candidate_impl_binary_operator(subset, set).

candidate_impl_binary_operator(subset_strict, set).

collect_function_constraints([], []).

collect_function_constraints([Candidate|T], FunctionConstraints) :-
    b_function_membership(Candidate, Id, Domain),
    !,
    FunctionConstraints = [Candidate-Id-Domain|NT],
    collect_function_constraints(T, NT).

collect_function_constraints([_|T], NT) :-
    collect_function_constraints(T, NT).

conjunct_two_preds(A,B,Expr) :-
    conjunct_predicates([A,B],b(Expr,_,_)).

disjunct_two_preds(A,B,Expr) :-
    disjunct_predicates([A,B],b(Expr,_,_)).

empty_candidate_impls_acc(candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([]))).

extend_candidate_impls_acc(Type, Functor, Arg1, Arg2, Ast, CandidateAcc, NewCandidateAcc) :-
    Type == pred,
    Arg1 = b(_,AType,_),
    functor(AType, FType, _),
    candidate_impl_binary_operator(Functor, FType),
    ( (ground_b_ast(Arg1),
    is_id_or_pred_containing_id(Arg2))
    ;
    (ground_b_ast(Arg2),
    is_id_or_pred_containing_id(Arg1))
    ),
    remove_all_infos(Ast, AstClean),
    ast_not_in_candidate_acc(ground, FType, AstClean, CandidateAcc),
    !,
    extend_candidate_impls_acc_safe_ground(FType, CandidateAcc, Ast, NewCandidateAcc).

extend_candidate_impls_acc(Type, Functor, Arg1, Arg2, Ast, CandidateAcc, NewCandidateAcc) :-
    Type == pred,
    Arg1 = b(_,AType,_),
    functor(AType, FType, _),
    candidate_impl_binary_operator(Functor, FType),
    is_id_or_pred_containing_id(Arg1),
    is_id_or_pred_containing_id(Arg2),
    remove_all_infos(Ast, AstClean),
    ast_not_in_candidate_acc(var, FType, AstClean, CandidateAcc),
    !,
    extend_candidate_impls_acc_safe(FType, CandidateAcc, Ast, NewCandidateAcc).

extend_candidate_impls_acc(_, _, _, _, _, CandidateAcc, CandidateAcc).

extend_candidate_impls_acc_safe(global, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd)), Ast, candidate_impls(global([Ast|Global]),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd))).

extend_candidate_impls_acc_safe(integer, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd)), Ast, candidate_impls(global(Global),integer([Ast|Integer]),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd))).

extend_candidate_impls_acc_safe(set, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd)), Ast, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set([Ast|Set]),set_ground(SetGrnd))).

extend_candidate_impls_acc_safe_ground(integer, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd)), Ast, candidate_impls(global(Global),integer(Integer),integer_ground([Ast|IntegerGrnd]),set(Set),set_ground(SetGrnd))).

extend_candidate_impls_acc_safe_ground(set, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd)), Ast, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground([Ast|SetGrnd]))).

get_global_type_partner_candidates(GrndCandidateImpl, Rest, Partners, RestRest) :-
    find_identifier_uses(GrndCandidateImpl, [], UsedIds),
    get_global_type_partner_candidates(UsedIds, Rest, [], Partners, [], RestRest),!.

get_global_type_partner_candidates(_, [], PartnersAcc, PartnersAcc, RestAcc, RestAcc).

get_global_type_partner_candidates(UsedIds, Rest, PartnersAcc, Partners, RestAcc, RestRest) :-
    select(Partner, Rest, TRest),
    ( uses_same_id(Partner, UsedIds)
    -> NPartnersAcc = [Partner|PartnersAcc],
    NRestAcc = RestAcc
    ; NPartnersAcc = PartnersAcc,
    NRestAcc = [Partner|RestAcc]
    ),
    !,
    get_global_type_partner_candidates(UsedIds, TRest, NPartnersAcc, Partners, NRestAcc, RestRest).

get_larger_conj(C1, C2, Larger, Other) :-
    C1 = b(conjunct(C1A,C1B),pred,_),
    C2 \= b(conjunct(_,_),pred,_),
    ( \+ is_literal(C1A); \+ is_literal(C1B)),
    !,
    Larger = C1,
    Other = C2.

get_larger_conj(C1, C2, Larger, Other) :-
    C2 = b(conjunct(C2A,C2B),pred,_),
    C1 \= b(conjunct(_,_),pred,_),
    ( \+ is_literal(C2A); \+ is_literal(C2B)),
    !,
    Larger = C2,
    Other = C1.

get_larger_conj(C1, C2, Larger, Other) :-
    C1 = b(conjunct(C1A,C1B),pred,_),
    C2 = b(conjunct(C2A,C2B),pred,_),
    ( \+ is_literal(C1A)
    ; \+ is_literal(C1B)
    ; \+ is_literal(C2A)
    ; \+ is_literal(C2B)
    ),
    term_size(C1, S1),
    term_size(C2, S2),
    ( S1 > S2
    -> Larger = C1,
    Other = C2
    ; Larger = C2,
    Other = C1
).

get_partner_candidates(GrndCandidateImpl, Rest, Partners, RestRest) :-
    find_identifier_uses(GrndCandidateImpl, [], UsedIds),
    get_partner_candidates(UsedIds, Rest, [], Partners, [], RestRest),!.

get_partner_candidates(_, [], PartnersAcc, PartnersAcc, RestAcc, RestAcc).

get_partner_candidates(UsedIds, Rest, PartnersAcc, Partners, RestAcc, RestRest) :-
    select(Partner, Rest, TRest),
    ( uses_exactly_same_ids(Partner, UsedIds)
    -> NPartnersAcc = [Partner|PartnersAcc],
    NRestAcc = RestAcc
    ; NPartnersAcc = PartnersAcc,
    NRestAcc = [Partner|RestAcc]
    ),
    !,
    get_partner_candidates(UsedIds, TRest, NPartnersAcc, Partners, NRestAcc, RestRest).

get_wd_theory_implications(CandidateImpls, WDCandidateImpls, WDTheoryImpls) :-
    CandidateImpls = candidate_impls(global(Global),integer(Integer),integer_ground(_),set(Set),set_ground(_)),
    WDCandidateImpls = candidate_impls(global(WDGlobal),integer(WDInteger),integer_ground(_),set(WDSet),set_ground(_)),
    append(WDInteger, WDSet, WDCandidates),
    get_wd_theory_implications_for_candidates(Global, WDGlobal, GlobalImpls),
    get_wd_theory_implications_for_candidates(Integer, WDCandidates, IntegerImpls),
    get_wd_theory_implications_for_candidates(Set, WDCandidates, SetImpls),
    conjunct_predicates([GlobalImpls,IntegerImpls,SetImpls], WDTheoryImpls).

get_wd_theory_implications_for_candidates(_, [], Out) :-
    !,
    Out = b(truth,pred,[]).

get_wd_theory_implications_for_candidates(Candidates, WDCandidates, ImplsConj) :-
    collect_function_constraints(Candidates, FunctionConstraints),
    get_wd_theory_implications_of_function_memberships(FunctionConstraints, WDCandidates, Impls),
    conjunct_predicates(Impls, ImplsConj).

get_wd_theory_implications_of_function_memberships([], _, []).

get_wd_theory_implications_of_function_memberships([FunMem-Id-Domain|T], WDCandidates, Impls) :-
    remove_all_infos(Id, CId),
    memberchk(b(member(DomId,b(domain(CId),DType,DInfo)),pred,MInfo), WDCandidates),
    !,
    safe_create_texpr(member(DomId,b(domain(CId),DType,DInfo)), pred, MInfo, DomMember),
    safe_create_texpr(disjunct(b(disjunct(b(negation(DomMember),pred,[]),b(negation(FunMem),pred,[])),pred,[]),b(member(DomId,Domain),pred,[])), pred, [], Impl),
    Impls = [Impl|NT],
    get_wd_theory_implications_of_function_memberships(T, WDCandidates, NT).

get_wd_theory_implications_of_function_memberships([_|T], WDCandidates, NT) :-
    get_wd_theory_implications_of_function_memberships(T, WDCandidates, NT).

ground_b_ast(Ast) :-
    ( var(Ast)
    -> fail
    ; ground_b_ast_nonvar(Ast)
).

ground_b_ast_nonvar(b(truth,_,_)).

ground_b_ast_nonvar(b(falsity,_,_)).

ground_b_ast_nonvar(b(integer(Int),_,_)) :-
    ground(Int).

ground_b_ast_nonvar(b(value(int(Int)),_,_)) :-
    ground(Int).

ground_b_ast_nonvar(b(interval(Min,Max),_,_)) :-
    Min = b(integer(I1),integer,_),
    Max = b(integer(I2),integer,_),
    integer(I1),
    integer(I2).

ground_b_ast_nonvar(b(set_extension(AstList),_,_)) :-
    maplist(ground_b_ast, AstList).

ground_b_ast_nonvar(b(value(Set),_,_)) :-
    ground(Set).

is_boolean_true(b(boolean_true,boolean,_)).

is_boolean_true(b(value(pred_true),boolean,_)).

is_id_or_pred_containing_id(TExpr) :-
    get_texpr_expr(TExpr, Expr),
    functor(Expr, Functor, _),
    % no ASTs with local identifiers
    \+ member(Functor, [forall,exists,comprehension_set,lambda,general_sum,general_product,event_b_comprehension_set,quantified_union,quantified_intersection]),
    map_over_bexpr(is_identifier, TExpr).

is_identifier(identifier(_)).

is_literal(b(truth,pred,[])).

is_literal(b(falsity,pred,[])).

is_literal(b(equal(b(_,boolean,_),b(identifier(_),boolean,_)),pred,[])).

is_literal(b(equal(b(identifier(_),boolean,_),b(_,boolean,_)),pred,[])).

is_true(X) :- (X==true -> true
    ; X== false -> fail
    ; add_internal_error('Illegal call:',is_true(X)), fail
).

lift_negations_find_impls(Pred, RewriteToIdl, CandidateAcc, LPred, CandidateImpls) :-
    Pred = b(Expr,Type,Info),
    !,
    lift_negations_find_impls_e(Expr, Type, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls),
    safe_create_texpr(LExpr,Type,Info,LPred).

lift_negations_find_impls(Pred, _, CandidateAcc, Pred, CandidateAcc).

lift_negations_find_impls_e(Expr, _, _, _, _, _, _) :- var(Expr),!,
    add_internal_error('Illegal var B AST: ',lift_negations_find_impls_e(Expr, _, _, _, _, _, _)),fail.

lift_negations_find_impls_e(Expr, _, _, _, CandidateAcc, LPred, CandidateImpls) :-
    % important to use the same SAT variables, e.g., for x=TRUE & x=FALSE
    (Expr = equal(Bool,BoolId) ; Expr = equal(BoolId,Bool)),
    BoolId = b(identifier(_),boolean,_),
    is_boolean_true(Bool),
    !,
    LPred = negation(b(equal(b(boolean_false,boolean,[]),BoolId),pred,[])),
    CandidateImpls = CandidateAcc.

lift_negations_find_impls_e(Expr, _, Info, RewriteToIdl, CandidateAcc, LPred, CandidateImpls) :-
    Expr = equivalence(Lhs,Rhs),
    !,
    create_implication(Lhs,Rhs,Impl1),
    create_implication(Rhs,Lhs,Impl2),
    Rewritten = conjunct(Impl1,Impl2),
    /*Disj1 = b(conjunct(Lhs,Rhs),pred,[]),
    Disj2 = b(conjunct(b(negation(Lhs),pred,[]),b(negation(Rhs),pred,[])),pred,[]),
    Rewritten = b(disjunct(Disj1,Disj2),pred,[]),*/
    lift_negations_find_impls_e(Rewritten, pred, Info, RewriteToIdl, CandidateAcc, LPred, CandidateImpls).

lift_negations_find_impls_e(Expr, _, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
    Expr = implication(Lhs,Rhs),
    !,
    create_negation(Lhs,NLhs),
    Rewritten = disjunct(NLhs,Rhs),
    lift_negations_find_impls_e(Rewritten, pred, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls).

lift_negations_find_impls_e(Expr, _, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
    Expr = negation(b(negation(Pos),pred,_)),
    get_texpr_expr(Pos, PosExpr),
    get_texpr_type(Pos, PosType),
    !,
    lift_negations_find_impls_e(PosExpr, PosType, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls).

lift_negations_find_impls_e(Expr, _, _, _, CandidateAcc, LExpr, CandidateImpls) :-
    Expr = negation(b(truth,pred,_)),
    !,
    LExpr = falsity,
    CandidateImpls = CandidateAcc.

lift_negations_find_impls_e(Expr, _, _, _, CandidateAcc, LExpr, CandidateImpls) :-
    Expr = negation(b(falsity,pred,_)),
    !,
    LExpr = truth,
    CandidateImpls = CandidateAcc.

lift_negations_find_impls_e(Inequality, _, _, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
    is_true(RewriteToIdl),
    ( Inequality = not_equal(b(_,integer,[]),_)
    %IEQ = Inequality
    ; Inequality = negation(b(equal(b(_,integer,[]),_),pred,_))
    %IEQ = b(not_equal(Arg1,Arg2),pred,EQInfo)
    ),
    rewrite_inequality_to_idl_disj_no_zero(b(Inequality,pred,[]), DLConstraint),
    !,
    DLConstraint = b(disjunct(Lhs,Rhs),pred,_),
    create_negation(LhsPos,Lhs),
    create_negation(RhsPos,Rhs),
    safe_create_texpr(less_equal(LArg1,LArg2),pred,[],LhsPos),
    safe_create_texpr(less_equal(RArg1,RArg2),pred,[],RhsPos),
    disjunct_two_preds(Lhs,Rhs,LExpr),
    %extend_candidate_impls_acc(pred, not_equal, Arg1, Arg2, IEQ, CandidateAcc, CandidateAcc1),
    extend_candidate_impls_acc(pred, less_equal, LArg1, LArg2, LhsPos, CandidateAcc, CandidateAcc1),
    extend_candidate_impls_acc(pred, less_equal, RArg1, RArg2, RhsPos, CandidateAcc1, CandidateImpls).

lift_negations_find_impls_e(Equality, _, _, RewriteToIdl, CandidateAcc, LPred, CandidateImpls) :-
    is_true(RewriteToIdl),
    ( Equality = equal(b(_,integer,_),_)
    %EQ = Equality
    ; Equality = negation(b(not_equal(b(_,integer,_),_),pred,_))
    %EQ = b(equal(Arg1,Arg2),pred,EQInfo)
    ),
    rewrite_to_idl_no_zero(b(Equality,pred,[]), ConjList),
    !,
    ConjList = [TLhs,TRhs],
    % don't create _zero var from idl solver in SAT formula
    remove_idl_origin_from_info(TLhs, Lhs),
    remove_idl_origin_from_info(TRhs, Rhs),
    safe_create_texpr(less_equal(LArg1,LArg2),pred,[],Lhs),
    safe_create_texpr(less_equal(RArg1,RArg2),pred,[],Rhs),
    conjunct_two_preds(Lhs,Rhs,LPred),
    extend_candidate_impls_acc(pred, less_equal, LArg1, LArg2, Lhs, CandidateAcc, CandidateAcc1),
    extend_candidate_impls_acc(pred, less_equal, RArg1, RArg2, Rhs, CandidateAcc1, CandidateImpls).

lift_negations_find_impls_e(Expr, Type, _, _, CandidateAcc, LExpr, CandidateImpls) :-
    negated_b_operator(Expr, TrueNode),
    !,
    safe_create_texpr(TrueNode,Type,[],TrueAst),
    TrueNode =.. [NFunctor, Arg1, Arg2],
    extend_candidate_impls_acc(Type, NFunctor, Arg1, Arg2, TrueAst, CandidateAcc, CandidateImpls),
    LExpr = negation(TrueAst).

lift_negations_find_impls_e(Expr, _, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
    Expr = negation(Arg),
    Arg = b(conjunct(Conj1,Conj2),pred,_),
    !,
    create_negation(Conj1,NConj1),
    create_negation(Conj2,NConj2),
    disjunct_two_preds(NConj1,NConj2,Rewritten),
    lift_negations_find_impls_e(Rewritten, pred, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls).

lift_negations_find_impls_e(Expr, _, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
    Expr = negation(Arg),
    Arg = b(disjunct(Conj1,Conj2),pred,_),
    !,
    create_negation(Conj1,NConj1),
    create_negation(Conj2,NConj2),
    Rewritten = conjunct(NConj1,NConj2),
    lift_negations_find_impls_e(Rewritten, pred, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls).

lift_negations_find_impls_e(Expr, pred, _Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
    Expr = negation(Arg),
    Arg = b(ArgExpr,ArgType,ArgInfo),
    lift_negations_find_impls_e(ArgExpr, ArgType, ArgInfo, RewriteToIdl, CandidateAcc, LArgExpr, CandidateImpls),
    safe_create_texpr(LArgExpr,pred,ArgInfo,TLA),
    create_negation(TLA,b(LExpr,_,_)).

lift_negations_find_impls_e(Expr, pred, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
    functor(Expr, Functor, 2),
    Names = [], % quantifications (comprehension_set, exists) will be abstracted by a single SAT variable
    syntaxtransformation(Expr,[Arg1,Arg2],Names,[LLhs,LRhs],LExpr), % TODO REVIEW: syntaxtransformation could have two subarguments even if arity is not 2
    !,
    extend_candidate_impls_acc(pred, Functor, Arg1, Arg2, b(Expr,pred,Info), CandidateAcc, CandidateAcc1),
    lift_negations_find_impls(Arg1, RewriteToIdl, CandidateAcc1, LLhs, CandidateAcc2),
    lift_negations_find_impls(Arg2, RewriteToIdl, CandidateAcc2, LRhs, CandidateImpls).

lift_negations_find_impls_e(Expr, _, _, _, CandidateAcc, Expr, CandidateAcc).

negate_bool_expr(boolean_true, boolean_false).

negate_bool_expr(boolean_false, boolean_true).

negate_bool_expr(value(pred_true), boolean_false).

negate_bool_expr(value(pred_false), boolean_true).

negate_bool_formula(b(negation(b(truth,pred,Info)),pred,_), b(falsity,pred,Info)).

negate_bool_formula(b(negation(b(falsity,pred,Info)),pred,_), b(truth,pred,Info)).

negate_bool_formula(b(negation(b(negation(Ast))),pred,_), NAst) :-
    !,
    negate_bool_formula(Ast, NAst).

negate_bool_formula(b(negation(Eq),pred,_), b(equal(Id,Negated),pred,EqInfo)) :-
    ( Eq = b(equal(Bool,Id),pred,EqInfo)
    ; Eq = b(equal(Id,Bool),pred,EqInfo)
    ),
    Bool = b(Expr,boolean,BoolInfo),
    negate_bool_expr(Expr, NExpr),
    safe_create_texpr(NExpr, boolean, BoolInfo, Negated),
    Id = b(identifier(_),_,_).

negate_bool_formula(b(negation(b(conjunct(A,B),pred,I)),pred,_), New) :-
    negate_bool_formula(b(negation(A),pred,[]), NewA),
    negate_bool_formula(b(negation(B),pred,[]), NewB),
    safe_create_texpr(disjunct(NewA,NewB), pred, I, New).

negate_bool_formula(b(negation(b(disjunct(A,B),pred,I)),pred,_), New) :-
    negate_bool_formula(b(negation(A),pred,[]), NewA),
    negate_bool_formula(b(negation(B),pred,[]), NewB),
    safe_create_texpr(conjunct(NewA,NewB), pred, I, New).

negated_b_operator(not_equal(A,B), equal(A,B)).

negated_b_operator(not_member(A,B), member(A,B)).

negated_b_operator(not_subset(A,B), subset(A,B)).

negated_b_operator(not_subset_strict(A,B), subset_strict(A,B)).

optimize_clause_size_by_rewriting(BoolFormula, SatVars, OptBoolFormula, NewSatVars, NewVarConj) :-
    BoolFormula = b(Expr,Type,Info),
    optimize_clause_size_by_rewriting_expr(Expr, SatVars, OptExpr, NewSatVars, NewVarConj),
    safe_create_texpr(OptExpr, Type, Info, OptBoolFormula).

optimize_clause_size_by_rewriting_expr(disjunct(D1,D2), SatVars, OptExpr, NewSatVars, NewVarConj) :-
    D1 = b(conjunct(_,_),pred,_),
    D2 \= b(conjunct(_,_),pred,_),
    !,
    optimize_clause_size_by_rewriting_expr(disjunct(D2,D1), SatVars, OptExpr, NewSatVars, NewVarConj).

optimize_clause_size_by_rewriting_expr(disjunct(D1,D2), SatVars, OptExpr, NewSatVars, NewVarConj) :-
    get_larger_conj(D1, D2, ToReplace, ToKeep),
    !,
    unique_typed_id("_cnf_opt", boolean, NewSatVar),
    optimize_clause_size_by_rewriting(ToReplace, SatVars, NToReplace, SatVars1, NewVarConj1),
    safe_create_texpr(equal(NewSatVar,b(boolean_true,boolean,[])), pred, [], NewVarTrue),
    safe_create_texpr(equal(NewSatVar,b(boolean_false,boolean,[])), pred, [], NewVarFalse),
    safe_create_texpr(disjunct(NewVarFalse,NToReplace), pred, [], NewVarImpl1),
    safe_create_texpr(negation(NToReplace), pred, [], ToReplaceNeg),
    negate_bool_formula(ToReplaceNeg, ToReplaceNegClean),
    optimize_clause_size_by_rewriting(ToReplaceNegClean, SatVars1, NToReplaceNegClean, SatVars2, NewVarConj2),
    safe_create_texpr(disjunct(NewVarTrue,NToReplaceNegClean), pred, [], NewVarImpl2),
    optimize_clause_size_by_rewriting(ToKeep, SatVars2, NToKeep, SatVars3, NewVarConj3),
    OptExpr = disjunct(NToKeep,NewVarTrue),
    NewSatVars = [NewSatVar|SatVars3],
    append([NewVarConj1, NewVarConj2, NewVarConj3], TNewVarConj),
    safe_create_texpr(conjunct(NewVarImpl1,NewVarImpl2), pred, [], Conj),
    NewVarConj = [Conj|TNewVarConj].

optimize_clause_size_by_rewriting_expr(Binary, SatVars, NBinary, NewSatVars, NewVarConj) :-
    functor(Binary, Functor, 2),
    (Functor = conjunct; Functor = disjunct; Functor = implication; Functor = equivalence),
    !,
    arg(1, Binary, Arg1),
    arg(2, Binary, Arg2),
    optimize_clause_size_by_rewriting(Arg1, SatVars, NArg1, SatVars1, NewVarConj1),
    optimize_clause_size_by_rewriting(Arg2, SatVars1, NArg2, NewSatVars, NewVarConj2),
    functor(NBinary, Functor, 2),
    arg(1, NBinary, NArg1),
    arg(2, NBinary, NArg2),
    append(NewVarConj1, NewVarConj2, NewVarConj).

optimize_clause_size_by_rewriting_expr(Expr, SatVars, Expr, SatVars, []).

preprocess_predicate(PerformStaticAnalysis, RewriteToIdl, Pred, LiftedPred, FilteredCandidateImplsConj, CandidateImpls) :-
    empty_candidate_impls_acc(CandidateAcc),
    lift_negations_find_impls(Pred, RewriteToIdl, CandidateAcc, TLiftedPred, CandidateImpls), !,
    LiftedPred = TLiftedPred,
    ( PerformStaticAnalysis=true
    -> process_candidate_impls(CandidateImpls, FilteredCandidateImplsConj)
    ; FilteredCandidateImplsConj = b(truth,pred,[])
).

process_candidate_impls(CandidateImpls, FilteredCandidateImplsConj) :-
    CandidateImpls = candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd)),
    process_candidate_impls_list(true, Global, GlobalImplsConj),
    process_candidate_impls_list(false, Integer, IntImplsConj),
    process_candidate_impls_list(false, IntegerGrnd, IntGrndImplsConj),
    process_candidate_impls_list(false, Set, SetImplsConj),
    process_candidate_impls_list(false, SetGrnd, SetGrndImplsConj),
    conjunct_predicates([GlobalImplsConj,IntImplsConj,IntGrndImplsConj,SetImplsConj,SetGrndImplsConj], FilteredCandidateImplsConj).

process_candidate_impls_list(IsGlobalType, GrndCandidateImpls, ImplsConj) :-
    process_candidate_impls_list(IsGlobalType, GrndCandidateImpls, [], Impls),
    conjunct_predicates(Impls, ImplsConj).

process_candidate_impls_list(_, [], Acc, ImplsConj) :- !, ImplsConj=Acc.

process_candidate_impls_list(IsGlobalType, [GrndCandidateImpl|T], Acc, ImplsConj) :-
    ( is_true(IsGlobalType)
    -> get_global_type_partner_candidates(GrndCandidateImpl, T, Partners, _RestT)
    ; get_partner_candidates(GrndCandidateImpl, T, Partners, _RestT)
    ),
    Partners \== [],
    !,
    build_implications_from_ground_candidates(GrndCandidateImpl, Partners, PartialImplsConj),
    process_candidate_impls_list(IsGlobalType, T, [PartialImplsConj|Acc], ImplsConj).

process_candidate_impls_list(IsGlobalType, [_|T], Acc, ImplsConj) :-
    process_candidate_impls_list(IsGlobalType, T, Acc, ImplsConj).

simplify_negation(Ast, Simplified) :-
    Ast = b(Expr,Type,Info),
    simplify_negation_e(Expr, SimplifiedExpr),
    safe_create_texpr(SimplifiedExpr, Type, Info, Simplified).

simplify_negation_e(negation(A), SimplifiedExpr) :-
    A = b(truth,pred,_),
    !,
    SimplifiedExpr = falsity.

simplify_negation_e(negation(A), SimplifiedExpr) :-
    A = b(falsity,pred,_),
    !,
    SimplifiedExpr = truth.

simplify_negation_e(negation(A), SimplifiedExpr) :-
    A = b(Expr,pred,_),
    negated_b_operator(Expr, NExpr),
    !,
    SimplifiedExpr=NExpr.

simplify_negation_e(negation(BoolEq), SimplifiedExpr) :-
    % important for SAT constraints such as x=TRUE & not(x=TRUE)
    ( BoolEq = b(equal(Bool,Id),pred,_)
    ; BoolEq = b(equal(Id,Bool),pred,_)
    ),
    Id = b(identifier(_),boolean,_),
    Bool = b(Expr,boolean,Info),
    negate_bool_expr(Expr, NExpr),
    safe_create_texpr(NExpr, boolean, Info, NBool),
    !,
    SimplifiedExpr = equal(NBool,Id).

simplify_negation_e(negation(Neg), SimplifiedExpr) :-
    Neg = b(negation(A),pred,_),
    !,
    A = b(SimplifiedExpr,_,_).

simplify_negation_e(negation(Conj), SimplifiedExpr) :-
    Conj = b(conjunct(A,B),pred,_),
    !,
    simplify_negation(b(negation(A),pred,[]), SimplifiedA),
    simplify_negation(b(negation(B),pred,[]), SimplifiedB),
    disjunct_two_preds(SimplifiedA,SimplifiedB,SimplifiedExpr).

simplify_negation_e(negation(Disj), SimplifiedExpr) :-
    Disj = b(disjunct(A,B),pred,_),
    !,
    simplify_negation(b(negation(A),pred,[]), SimplifiedA),
    simplify_negation(b(negation(B),pred,[]), SimplifiedB),
    conjunct_two_preds(SimplifiedA,SimplifiedB,SimplifiedExpr).

simplify_negation_e(negation(Impl), SimplifiedExpr) :-
    Impl = b(implication(A,B),pred,_),
    !,
    simplify_negation_e(conjunct(A,b(negation(B),pred,[])), SimplifiedExpr).

simplify_negation_e(negation(Equi), SimplifiedExpr) :-
    Equi = b(equivalence(A,B),pred,_),
    !,
    simplify_negation_e(disjunct(b(negation(b(implication(A,B),pred,[])),pred,[]),
    b(negation(b(implication(B,A),pred,[])),pred,[])), SimplifiedExpr).

simplify_negation_e(Conn, SimplifiedExpr) :-
    ( Conn = conjunct(A,B)
    ; Conn = disjunct(A,B)
    ; Conn = implication(A,B)
    ; Conn = equivalence(A,B)
    ),
    !,
    simplify_negation(A, SimplifiedA),
    simplify_negation(B, SimplifiedB),
    ( Conn = conjunct(A,B) ->
    SimplifiedExpr = conjunct(SimplifiedA,SimplifiedB)
    ; Conn = disjunct(A,B) ->
    SimplifiedExpr = disjunct(SimplifiedA,SimplifiedB)
    ; Conn = implication(A,B) ->
    SimplifiedExpr = implication(SimplifiedA,SimplifiedB)
    ; Conn = equivalence(A,B) ->
    SimplifiedExpr = equivalence(SimplifiedA,SimplifiedB)
).

simplify_negation_e(Expr, Expr).

test(extend_candidate_impls_acc_less, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([b(less(b(identifier(x),integer,[]),b(integer(7),integer,[])),pred,[])]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),integer,[]),
    Arg2 = b(integer(7),integer,[]),
    Ast = b(less(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, less, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_less_non_ground, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([_]),set(set(integer)),[]),
    Ast = b(less(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, less, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_less_no_identifier, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(comprehension_set([b(identifier(x),integer,[])],b(member(b(identifier(x),integer,[]), b(set_extension([b(integer(234),integer,[]),b(integer(34),integer,[])]),set(integer),[])),pred,[])),set(integer),[some,info]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(less(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, less, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_less_eq, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([b(less_equal(b(identifier(x),integer,[]),b(integer(7),integer,[])),pred,[])]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),integer,[]),
    Arg2 = b(integer(7),integer,[]),
    Ast = b(less_equal(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, less_equal, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_less_eq_non_ground, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([_]),set(set(integer)),[]),
    Ast = b(less_equal(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, less_equal, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_less_eq_no_identifier, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(comprehension_set([b(identifier(x),integer,[])],b(member(b(identifier(x),integer,[]), b(set_extension([b(integer(234),integer,[]),b(integer(34),integer,[])]),set(integer),[])),pred,[])),set(integer),[some,info]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(less_equal(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, less_equal, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_subset, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([b(subset(b(identifier(x),set(set(integer)),[]),b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[])),pred,[])])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(subset(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, subset, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_subset_non_ground, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([_]),set(set(integer)),[]),
    Ast = b(subset(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, subset, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_subset_no_identifier, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(comprehension_set([b(identifier(x),integer,[])],b(member(b(identifier(x),integer,[]), b(set_extension([b(integer(234),integer,[]),b(integer(34),integer,[])]),set(integer),[])),pred,[])),set(integer),[some,info]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(subset(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, subset, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_subset_strict, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([b(subset_strict(b(identifier(x),set(set(integer)),[]),b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[])),pred,[])])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(subset_strict(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, subset_strict, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_subset_strict_non_ground, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([_]),set(set(integer)),[]),
    Ast = b(subset_strict(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, subset_strict, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_subset_strict_no_identifier, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(comprehension_set([b(identifier(x),integer,[])],b(member(b(identifier(x),integer,[]), b(set_extension([b(integer(234),integer,[]),b(integer(34),integer,[])]),set(integer),[])),pred,[])),set(integer),[some,info]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(subset_strict(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, subset_strict, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_equal, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([b(equal(b(identifier(x),set(set(integer)),[]),b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[])),pred,[])])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(set(integer)),[]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(equal(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, equal, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_member, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([b(member(b(identifier(x),set(integer),[]),b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[])),pred,[])])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(integer),[]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(member(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(pred, member, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_member_non_ground_type, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(identifier(x),set(integer),[]),
    Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
    Ast = b(member(Arg1,Arg2),pred,[]),
    extend_candidate_impls_acc(_Type, member, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_add, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(integer(1),integer,[]),
    Arg2 = b(integer(1),integer,[]),
    Ast = b(add(Arg1,Arg2),integer,[]),
    extend_candidate_impls_acc(integer, add, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_overwrite, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(set_extension([b(couple(b(integer(1),integer,[]),b(integer(2),integer,[])),couple(integer,integer),[info(o),o])]),set(couple(integer,integer)),[]),
    Arg2 = b(set_extension([b(couple(b(integer(1),integer,[]),b(integer(2),integer,[])),couple(integer,integer),[ein(e),wei(t,e(re)),info])]),set(couple(integer,integer)),[]),
    Ast = b(overwrite(Arg1,Arg2),set(couple(integer,integer)),[]),
    extend_candidate_impls_acc(integer, add, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

test(extend_candidate_impls_acc_overwrite_non_ground_type, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
    empty_candidate_impls_acc(EmptyAcc),
    Arg1 = b(set_extension([b(couple(b(integer(1),integer,[]),b(integer(2),integer,[])),couple(integer,integer),[info(o),o])]),set(couple(integer,integer)),[]),
    Arg2 = b(set_extension([b(couple(b(integer(1),integer,[]),b(integer(2),integer,[])),couple(integer,integer),[ein(e),wei(t,e(re)),info])]),set(couple(integer,integer)),[]),
    Ast = b(overwrite(Arg1,Arg2),set(couple(integer,integer)),[]),
    extend_candidate_impls_acc(_Type, add, Arg1, Arg2, Ast, EmptyAcc, NewAcc).

uses_exactly_same_ids(A, UsedIds) :-
    find_identifier_uses(A, [], UsedA),
    sets:subset(UsedA, UsedIds),
    sets:subset(UsedIds, UsedA), !.

uses_same_id(A, UsedIds) :-
    find_identifier_uses(A, [], UsedA),
    sets:intersection(UsedA, UsedIds, Inter),
    Inter \== [].