b2sat

addCnf2Solver(SolverID,Cnf,FVars,NrVars):-
    term_variables(Cnf,FVars),!,
    length(FVars,NrVars), length(Cnf,ClNr),
    format('Clauses: ~w, SAT Variables: ~w, Solver ID: ~w ~n',[ClNr,NrVars,SolverID]),
    add_to_profile_stats(sat_clauses,ClNr),
    add_to_profile_stats(sat_vars,NrVars),
    \+ \+ (bind2index(FVars,3,_FN),
    %portray_cnf(Cnf),
    simplify_cnf(Cnf,SCnf),
    AllCnf = [[1],[-2]|SCnf], % add true literal 1 and false literal 2
    add_cnf_clauses_to_solver(SolverID,[1,2|FVars],AllCnf)
%,neg(FN,FNeg), add_cnf_clauses([[FN,FNeg]],SolverID) % why did we add this tautology ?
).

add_cnf_clauses([Cl|Cls],SolverID):-!,
    to_minisat_cl(Cl,MiniSatCl),
    %format('Adding clause to solver ~w: ~w~n',[SolverID,MiniSatCl]),
    add_clause(SolverID,MiniSatCl), % add_clause can fail when SAT solver detects inconsistency directly
    add_cnf_clauses(Cls,SolverID).

add_cnf_clauses([],_):-!.

add_cnf_clauses_to_solver(z3,FVars,AllCnf) :- !,
    smt_add_cnf(z3,[1,2|FVars],AllCnf).

add_cnf_clauses_to_solver(SolverID,_,AllCnf) :-
    add_cnf_clauses(AllCnf,SolverID).

add_extra_clause_to_solver(z3,MiniSatCl) :- !,
    smt_add_extra_clause_cnf(z3,MiniSatCl).

add_extra_clause_to_solver(SolverID,MiniSatCl) :-
    add_clause(SolverID,MiniSatCl).

add_negated_model(SolverID,Model):-
    maplist(neg,Model,NoAsgn),
    add_extra_clause_to_solver(SolverID,NoAsgn).

assign_model_from_solver(z3,FVars,Model) :- !,
    debug:debug_println(19,assign_z3_model(FVars,Model)),
    assign_z3_model(FVars,Model).

assign_model_from_solver(SolverID,FVars,_Model) :-
    assign_model(SolverID,[1|FVars]).

assign_z3_aux([],_,TM) :- !,
    (TM=[] -> true ; add_internal_error('Too many literals in model:',assign_z3_aux([],_,TM))).

assign_z3_aux([H|T],Nr,[Model|TM]) :- !,
    % format('Assigning ~w VAR to ~w~n',[Nr,Model]),
    (Model=Nr -> H=pred_true
    ; Model is -Nr -> H=pred_false
    ; add_internal_error('Unexpected literal:',assign_z3_aux([H|T],Nr,[Model|TM])),
    fail
    ),
    N1 is Nr+1,
    assign_z3_aux(T,N1,TM).

assign_z3_aux(V,Nr,TM) :- add_internal_error('Model mismatch:',assign_z3_aux(V,Nr,TM)).

assign_z3_model(VarsList,[1,-2|Model]) :- !, % for z3
    assign_z3_aux(VarsList,3,Model).

assign_z3_model(VarsList,[-2|Model]) :- !, % for glucose, minisat, ...
    assign_z3_aux(VarsList,3,Model).

assign_z3_model(_,Model) :- add_internal_error('Z3 solution incorrect:',assign_z3_model(_,Model)), fail.

bind2index([N|Ns],N,FN) :- N1 is N+1, bind2index(Ns,N1,FN).

bind2index([],N,FN):-!, FN is N - 1.

bt_sat(CNF,Options) :-
    get_new_solver(SolverID,Options),
    call_cleanup(bt_sat_aux(SolverID,CNF),
    reset_solver(SolverID)).

bt_sat3(SolverID,FVars,Model) :-
    debug_format(19,'Assigning Model~n',[]),
    assign_model_from_solver(SolverID,FVars,Model).

bt_sat3(SolverID,FVars,Model) :-
    debug_format(19,'Adding negated model to find another solution~n',[]),
    add_negated_model(SolverID,Model),
    solve_and_get_model_from_solver(SolverID,NewModel),
    bt_sat3(SolverID,FVars,NewModel).

bt_sat_aux(SolverID,CNF) :-
    addCnf2Solver(SolverID,CNF,FVars,NrVars),!,
    %toDimacs(SolverID,'satsolver_dimacs.cnf'), % comment in to export CNF to Dimacs format
    debug_format(19,'Solving for ~w sat variables~n',[NrVars]),
    flush_output,
    solve_and_get_model_from_solver(SolverID,Model),
    debug_format(19,'Model = ~w~n',[Model]),
    bt_sat3(SolverID,FVars,Model).

bt_sat_aux(SolverID,_) :-
    debug_format(19,'Inconsistency detected while adding clauses to SAT Solver ~w~n',[SolverID]),
    fail.

false_lit(2).

false_lit(pred_false).

false_lit(neg(L)) :- true_lit(L).

get_new_solver(z3,Options) :- member(use_satsolver(z3),Options),!.

get_new_solver(SolverID,_) :- % use glucose
    new_solver(SolverID).

is_already_declared_in_state(State,TID) :- def_get_texpr_id(TID,ID), memberchk(bind(ID,_),State).

neg(V,VN) :- VN is -V.

portray_cl(Clause) :- format(' ~w~n',[Clause]).

portray_cnf(CNF) :- write('CNF:'),nl,maplist(portray_cl,CNF).

reset_solver(z3) :- !, smt_reset_cnf(z3).

reset_solver(SolverID) :- delete_solver(SolverID).

simplify_clause([],[]).

simplify_clause([FALSE|T],Res) :- false_lit(FALSE),!, simplify_clause(T,Res).

simplify_clause([TRUE|_],_Res) :- true_lit(TRUE),!,fail. % clause useless, it is true

simplify_clause([Lit|T],[Lit|Res]) :- simplify_clause(T,Res).

simplify_cnf([],[]).

simplify_cnf([Clause|T],Res) :-
    (simplify_clause(Clause,SC)
    -> Res=[SC|TR]
    ; Res=TR), % useless clause
    simplify_cnf(T,TR).

solve_and_get_model_from_solver(z3,AVLModel) :- !,
    smt_solve_cnf(z3,AVLModel).

solve_and_get_model_from_solver(SolverID,Model) :-
    solve(SolverID),
    debug_format(19,'Get Model~n',[]),
    get_model(SolverID,[_|Model]). % model will be something like [-2,3,-4]

solve_cnf(T2,CNF,State,Result,Options) :-
    bt_sat(CNF,Options),
    stop_ms_timer_with_profile(T2,sat_walltime,'Formula is SATisfiable'),
    Result = solution(State).

solve_cnf(T2,_,_,_Result,_Options) :-
    stop_ms_timer_with_profile(T2,sat_walltime,'Formula is UNSATisfiable'),
    fail. % fail to avoid pending co-routines of b_to_cnf

solve_pred2(BFormula,TypedVals,State,Result,Options) :-
    init_wait_flags_with_call_stack(WF,[prob_command_context(sat_solving,unknown)]),
    if(solve_pred3(BFormula,State,Result,Options,WF),
    (b_tighter_enumerate_all_values(TypedVals,WF),
    ground_wait_flags(WF)),
    Result=contradiction_found).

solve_pred3(BFormula,State,Result,Options,WF) :-
    start_ms_timer(T1),
    % Note: b_to_cnf will also look up all identifiers
    (b_to_cnf_wf(BFormula,State,CNF,WF)
    -> stop_ms_timer_with_profile(T1,b_to_cnf_walltime,'Converting B to CNF'),
    ground_det_wait_flag(WF),
    start_ms_timer(T2),
    %portray_cnf(CNF),
    %translate:print_bstate(State),nl,
    solve_cnf(T2,CNF,State,Result,Options)
    ; Result=error
).

solve_predicate_with_satsolver(BFormula,State) :-
    solve_predicate_with_satsolver(BFormula,[],State,Result,[]),
    Result = solution(_).

solve_predicate_with_satsolver(BFormula,TypedVals,State,Result,Options) :-
    %write(' :sat '),nl, translate:nested_print_bexpr(BFormula),nl,
    init_satsolver,!,
    if(solve_pred2(BFormula,TypedVals,State,Result,Options),true,Result=error).

solve_predicate_with_satsolver(_,_,_,error,_).

solve_predicate_with_satsolver_free(BFormula,Result) :-
    solve_predicate_with_satsolver_free(BFormula,_,Result,[]).

solve_predicate_with_satsolver_free(BFormula,LocalState,Result,Options) :-
    find_typed_identifier_uses(BFormula,UsedIdentifiers),
    set_up_typed_localstate_for_pred(UsedIdentifiers,BFormula,TypedVals,LocalState),
    b_optimize(BFormula,[],LocalState,[],NewTyped,no_wf_available),
    solve_predicate_with_satsolver(NewTyped,TypedVals,LocalState,Result,Options).

solve_predicate_with_satsolver_in_state(BFormula,State,Result,Options) :-
    find_typed_identifier_uses(BFormula,UsedIdentifiers),
    exclude(is_already_declared_in_state(State),UsedIdentifiers,FilteredIdentifiers),
    set_up_typed_localstate_for_pred(FilteredIdentifiers,BFormula,TypedVals,LocalState),
    b_optimize(BFormula,[],LocalState,State,NewTyped,no_wf_available),
    append(LocalState,State,State2),
    solve_predicate_with_satsolver(NewTyped,TypedVals,State2,Result,Options).

stop_ms_timer_with_profile(Timer,Category,Msg) :-
    get_elapsed_walltime(Timer,WT),
    add_to_profile_stats(Category,WT),
    stop_ms_timer_with_msg(Timer,Msg),
    flush_output.

to_minisat_cl([],[]).

to_minisat_cl([Lit1|TL],[ML1|TM]) :- to_minisat_lit(Lit1,ML1), to_minisat_cl(TL,TM).

to_minisat_lit(pred_true,1) :- !.

to_minisat_lit(pred_false,2) :- !.

to_minisat_lit(neg(NL),MSLit) :- !, to_minisat_neg_lit(NL,MSLit).

to_minisat_lit(X,R) :- integer(X),!, R=X. % a Prolog variable that has been bound by bind2index to a number

to_minisat_lit(X,R) :- add_internal_error('Illegal literal: ',to_minisat_lit(X,R)), R=X.

to_minisat_neg_lit(pred_false,1) :- !.

to_minisat_neg_lit(pred_true,2) :- !.

to_minisat_neg_lit(X,R) :- integer(X),!, R=neg(X). % a Prolog variable that has been bound by bind2index to a number

to_minisat_neg_lit(X,R) :- add_internal_error('Illegal literal: ',to_minisat_neg_lit(X,R)), R=neg(X).

true_lit(1).

true_lit(pred_true).

true_lit(neg(L)) :- false_lit(L).