1 % (c) 2012-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(b2sat, [init_satsolver/0, bt_sat/2,
6 solve_predicate_with_satsolver_free/2,
7 solve_predicate_with_satsolver_free/4,
8 solve_predicate_with_satsolver_in_state/4,
9 solve_predicate_with_satsolver/2]).
10
11 :- use_module('../../src/module_information.pl').
12 :- module_info(group,satsolver).
13 :- module_info(description,'This is the interface for ProB to use various SAT solvers (glucose, Z3)').
14
15 :- use_module(probsrc(tools),[start_ms_timer/1, stop_ms_timer_with_msg/2,
16 stop_ms_timer_with_debug_msg/2, get_elapsed_walltime/2]).
17 :- use_module(probsrc(debug),[debug_format/3]).
18 :- use_module(probsrc(error_manager),[add_error/3, add_internal_error/2]).
19 :- use_module(b_to_cnf).
20
21 :- use_module(library(lists), [maplist/2,maplist/3,exclude/3]).
22
23 :- use_module(satsolver). % Glucose API
24
25
26 :- use_module(probsrc(bsyntaxtree), [find_typed_identifier_uses/2, def_get_texpr_id/2]).
27 :- use_module(probsrc(solver_interface), [set_up_typed_localstate_for_pred/4]).
28 :- use_module(probsrc(b_compiler),[b_optimize/6]).
29
30 % call to solve a predicate with sat solver assuming all variables are free:
31 solve_predicate_with_satsolver_free(BFormula,Result) :-
32 solve_predicate_with_satsolver_free(BFormula,_,Result,[]).
33 solve_predicate_with_satsolver_free(BFormula,LocalState,Result,Options) :-
34 find_typed_identifier_uses(BFormula,UsedIdentifiers),
35 set_up_typed_localstate_for_pred(UsedIdentifiers,BFormula,TypedVals,LocalState),
36 b_optimize(BFormula,[],LocalState,[],NewTyped,no_wf_available),
37 solve_predicate_with_satsolver(NewTyped,TypedVals,LocalState,Result,Options).
38
39
40 % call to solve a predicate with sat solver with a provided state with variable/constant values:
41 solve_predicate_with_satsolver_in_state(BFormula,State,Result,Options) :-
42 find_typed_identifier_uses(BFormula,UsedIdentifiers),
43 exclude(is_already_declared_in_state(State),UsedIdentifiers,FilteredIdentifiers),
44 set_up_typed_localstate_for_pred(FilteredIdentifiers,BFormula,TypedVals,LocalState),
45 b_optimize(BFormula,[],LocalState,State,NewTyped,no_wf_available),
46 append(LocalState,State,State2),
47 solve_predicate_with_satsolver(NewTyped,TypedVals,State2,Result,Options).
48 is_already_declared_in_state(State,TID) :- def_get_texpr_id(TID,ID), memberchk(bind(ID,_),State).
49
50 solve_predicate_with_satsolver(BFormula,State) :-
51 solve_predicate_with_satsolver(BFormula,[],State,Result,[]),
52 Result = solution(_).
53
54 solve_predicate_with_satsolver(BFormula,TypedVals,State,Result,Options) :-
55 %write(' :sat '),nl, translate:nested_print_bexpr(BFormula),nl,
56 init_satsolver,!,
57 if(solve_pred2(BFormula,TypedVals,State,Result,Options),true,Result=error).
58 solve_predicate_with_satsolver(_,_,_,error,_).
59
60 :- use_module(probsrc(b_enumerate), [b_tighter_enumerate_all_values/2]).
61 :- use_module(probsrc(kernel_waitflags),
62 [init_wait_flags_with_call_stack/2,ground_wait_flags/1,
63 ground_det_wait_flag/1]).
64
65 solve_pred2(BFormula,TypedVals,State,Result,Options) :-
66 init_wait_flags_with_call_stack(WF,[prob_command_context(sat_solving,unknown)]),
67 if(solve_pred3(BFormula,State,Result,Options,WF),
68 (b_tighter_enumerate_all_values(TypedVals,WF),
69 ground_wait_flags(WF)),
70 Result=contradiction_found).
71
72 solve_pred3(BFormula,State,Result,Options,WF) :-
73 start_ms_timer(T1),
74 % Note: b_to_cnf will also look up all identifiers
75 (b_to_cnf_wf(BFormula,State,CNF,WF)
76 -> stop_ms_timer_with_profile(T1,b_to_cnf_walltime,'Converting B to CNF'),
77 ground_det_wait_flag(WF),
78 start_ms_timer(T2),
79 %portray_cnf(CNF),
80 solve_cnf(T2,CNF,State,Result,Options)
81 ; Result=error
82 ).
83
84 solve_cnf(T2,CNF,State,Result,Options) :-
85 bt_sat(CNF,Options),
86 stop_ms_timer_with_profile(T2,sat_walltime,'Formula is SATisfiable'),
87 Result = solution(State).
88 solve_cnf(T2,_,_,_Result,_Options) :-
89 stop_ms_timer_with_profile(T2,sat_walltime,'Formula is UNSATisfiable'),
90 fail. % fail to avoid pending co-routines of b_to_cnf
91
92 :- public portray_cnf/1.
93 portray_cnf(CNF) :- write('CNF:'),nl,maplist(portray_cl,CNF).
94 portray_cl(Clause) :- format(' ~w~n',[Clause]).
95
96
97 :- use_module(covsrc(hit_profiler),[add_to_profile_stats/2]).
98 stop_ms_timer_with_profile(Timer,Category,Msg) :-
99 get_elapsed_walltime(Timer,WT),
100 add_to_profile_stats(Category,WT),
101 stop_ms_timer_with_msg(Timer,Msg).
102
103
104 % --------------
105
106
107 % backtracking solving:
108 bt_sat(CNF,Options) :-
109 get_new_solver(SolverID,Options),
110 call_cleanup(bt_sat_aux(SolverID,CNF),
111 reset_solver(SolverID)).
112
113 bt_sat_aux(SolverID,F) :-
114 addCnf2Solver(SolverID,F,FVars,NrVars),
115 %toDimacs(SolverID,'satsolver_dimacs.cnf'), % comment in to export CNF to Dimacs format
116 debug_format(19,'Solving for ~w sat variables~n',[NrVars]),
117 solve_and_get_model_from_solver(SolverID,Model),
118 debug_format(19,'Model = ~w~n',[Model]),
119 bt_sat3(SolverID,FVars,Model).
120
121 bt_sat3(SolverID,FVars,Model) :-
122 debug_format(19,'Assigning Model~n',[]),
123 assign_model_from_solver(SolverID,FVars,Model).
124 bt_sat3(SolverID,FVars,Model) :-
125 debug_format(19,'Adding negated model to find another solution~n',[]),
126 add_negated_model(SolverID,Model),
127 solve_and_get_model_from_solver(SolverID,NewModel),
128 bt_sat3(SolverID,FVars,NewModel).
129
130 add_negated_model(SolverID,Model):-
131 maplist(neg,Model,NoAsgn),
132 add_extra_clause_to_solver(SolverID,NoAsgn).
133
134 neg(V,VN) :- VN is -V.
135
136 % -----------------
137
138 addCnf2Solver(SolverID,Cnf,FVars,NrVars):-
139 term_variables(Cnf,FVars),!,
140 length(FVars,NrVars), length(Cnf,ClNr),
141 AllCnf = [[1],[-2]|Cnf], % add true literal 1 and false literal 2
142 format('Clauses: ~w, SAT Variables: ~w, Solver ID: ~w ~n',[ClNr,NrVars,SolverID]),
143 add_to_profile_stats(sat_clauses,ClNr),
144 add_to_profile_stats(sat_vars,NrVars),
145 \+ \+ (bind2index(FVars,3,_FN),
146 %portray_cnf(Cnf),
147 add_cnf_clauses_to_solver(SolverID,[1,2|FVars],AllCnf)
148 %,neg(FN,FNeg), add_cnf_clauses([[FN,FNeg]],SolverID) % why did we add this tautology ?
149 ).
150
151 % ------------------
152
153 % dispatching code: chooses between Glucose and Z3
154
155 :- use_module(smt_solvers_interface(smt_solvers_interface),[smt_add_cnf/3, smt_add_extra_clause_cnf/2,
156 smt_solve_cnf/2, smt_reset_cnf/1]).
157
158 get_new_solver(z3,Options) :- member(use_satsolver(z3),Options),!.
159 get_new_solver(SolverID,_) :- % use glucose
160 new_solver(SolverID).
161
162 reset_solver(z3) :- !, smt_reset_cnf(z3).
163 reset_solver(SolverID) :- delete_solver(SolverID).
164
165 add_cnf_clauses_to_solver(z3,FVars,AllCnf) :- !,
166 smt_add_cnf(z3,[1,2|FVars],AllCnf).
167 add_cnf_clauses_to_solver(SolverID,_,AllCnf) :-
168 add_cnf_clauses(AllCnf,SolverID).
169
170 add_extra_clause_to_solver(z3,MiniSatCl) :- !,
171 smt_add_extra_clause_cnf(z3,MiniSatCl).
172 add_extra_clause_to_solver(SolverID,MiniSatCl) :-
173 add_clause(SolverID,MiniSatCl).
174
175 solve_and_get_model_from_solver(z3,AVLModel) :- !,
176 smt_solve_cnf(z3,AVLModel).
177 solve_and_get_model_from_solver(SolverID,Model) :-
178 solve(SolverID),
179 debug_format(19,'Get Model~n',[]),
180 get_model(SolverID,[_|Model]). % model will be something like [-2,3,-4]
181
182
183 assign_model_from_solver(z3,FVars,Model) :- !,
184 debug:debug_println(19,assign_z3_model(FVars,Model)),
185 assign_z3_model(FVars,Model).
186 assign_model_from_solver(SolverID,FVars,_Model) :-
187 assign_model(SolverID,[1|FVars]). % Note: assign model calls SP_unify one by one, and can fail when ProB triggers co-routines
188
189 assign_z3_model(VarsList,[1,-2|Model]) :- !,
190 assign_z3_aux(VarsList,3,Model).
191 assign_z3_model(_,Model) :- add_internal_error('Z3 solution incorrect:',assign_z3_model(_,Model)), fail.
192
193 assign_z3_aux([],_,TM) :- !,
194 (TM=[] -> true ; add_internal_error('Too many literals in model:',assign_z3_aux([],_,TM))).
195 assign_z3_aux([H|T],Nr,[Model|TM]) :- !,
196 (Model=Nr -> H=pred_true
197 ; Model is -Nr -> H=pred_false
198 ; add_internal_error('Unexpected literal:',assign_z3_aux([H|T],Nr,[Model|TM])),
199 fail
200 ),
201 N1 is Nr+1,
202 assign_z3_aux(T,N1,TM).
203 assign_z3_aux(V,Nr,TM) :- add_internal_error('Model mismatch:',assign_z3_aux(V,Nr,TM)).
204
205 % ------------------
206
207
208 add_cnf_clauses([Cl|Cls],SolverID):-!,
209 to_minisat_cl(Cl,MiniSatCl),
210 add_clause(SolverID,MiniSatCl),
211 add_cnf_clauses(Cls,SolverID).
212 add_cnf_clauses([],_):-!.
213
214 to_minisat_cl([],[]).
215 to_minisat_cl([Lit1|TL],[ML1|TM]) :- to_minisat_lit(Lit1,ML1), to_minisat_cl(TL,TM).
216
217 to_minisat_lit(pred_true,1) :- !.
218 to_minisat_lit(pred_false,2) :- !.
219 to_minisat_lit(X,X). % a Prolog variable that has been bound by bind2index to a number
220
221 % bind a list of variables to numbers (representing literals in .cnf)
222 bind2index([N|Ns],N,FN) :- N1 is N+1, bind2index(Ns,N1,FN).
223 bind2index([],N,FN):-!, FN is N - 1.