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 %translate:print_bstate(State),nl,
81 solve_cnf(T2,CNF,State,Result,Options)
82 ; Result=error
83 ).
84
85 solve_cnf(T2,CNF,State,Result,Options) :-
86 bt_sat(CNF,Options),
87 stop_ms_timer_with_profile(T2,sat_walltime,'Formula is SATisfiable'),
88 Result = solution(State).
89 solve_cnf(T2,_,_,_Result,_Options) :-
90 stop_ms_timer_with_profile(T2,sat_walltime,'Formula is UNSATisfiable'),
91 fail. % fail to avoid pending co-routines of b_to_cnf
92
93 :- public portray_cnf/1.
94 portray_cnf(CNF) :- write('CNF:'),nl,maplist(portray_cl,CNF).
95 portray_cl(Clause) :- format(' ~w~n',[Clause]).
96
97
98 :- use_module(covsrc(hit_profiler),[add_to_profile_stats/2]).
99 stop_ms_timer_with_profile(Timer,Category,Msg) :-
100 get_elapsed_walltime(Timer,WT),
101 add_to_profile_stats(Category,WT),
102 stop_ms_timer_with_msg(Timer,Msg),
103 flush_output.
104
105
106 % --------------
107
108
109 % backtracking solving:
110 bt_sat(CNF,Options) :-
111 get_new_solver(SolverID,Options),
112 call_cleanup(bt_sat_aux(SolverID,CNF),
113 reset_solver(SolverID)).
114
115 bt_sat_aux(SolverID,CNF) :-
116 addCnf2Solver(SolverID,CNF,FVars,NrVars),!,
117 %toDimacs(SolverID,'satsolver_dimacs.cnf'), % comment in to export CNF to Dimacs format
118 debug_format(19,'Solving for ~w sat variables~n',[NrVars]),
119 flush_output,
120 solve_and_get_model_from_solver(SolverID,Model),
121 debug_format(19,'Model = ~w~n',[Model]),
122 bt_sat3(SolverID,FVars,Model).
123 bt_sat_aux(SolverID,_) :-
124 debug_format(19,'Inconsistency detected while adding clauses to SAT Solver ~w~n',[SolverID]),
125 fail.
126
127
128 bt_sat3(SolverID,FVars,Model) :-
129 debug_format(19,'Assigning Model~n',[]),
130 assign_model_from_solver(SolverID,FVars,Model).
131 bt_sat3(SolverID,FVars,Model) :-
132 debug_format(19,'Adding negated model to find another solution~n',[]),
133 add_negated_model(SolverID,Model),
134 solve_and_get_model_from_solver(SolverID,NewModel),
135 bt_sat3(SolverID,FVars,NewModel).
136
137 add_negated_model(SolverID,Model):-
138 maplist(neg,Model,NoAsgn),
139 add_extra_clause_to_solver(SolverID,NoAsgn).
140
141 neg(V,VN) :- VN is -V.
142
143 % -----------------
144
145 addCnf2Solver(SolverID,Cnf,FVars,NrVars):-
146 term_variables(Cnf,FVars),!,
147 length(FVars,NrVars), length(Cnf,ClNr),
148 format('Clauses: ~w, SAT Variables: ~w, Solver ID: ~w ~n',[ClNr,NrVars,SolverID]),
149 add_to_profile_stats(sat_clauses,ClNr),
150 add_to_profile_stats(sat_vars,NrVars),
151 \+ \+ (bind2index(FVars,3,_FN),
152 %portray_cnf(Cnf),
153 simplify_cnf(Cnf,SCnf),
154 AllCnf = [[1],[-2]|SCnf], % add true literal 1 and false literal 2
155 add_cnf_clauses_to_solver(SolverID,[1,2|FVars],AllCnf)
156 %,neg(FN,FNeg), add_cnf_clauses([[FN,FNeg]],SolverID) % why did we add this tautology ?
157 ).
158
159 % simplify CNF in case ProB propagation now has instantiated some of the SAT variables to pred_true/pred_false/...
160 simplify_cnf([],[]).
161 simplify_cnf([Clause|T],Res) :-
162 (simplify_clause(Clause,SC)
163 -> Res=[SC|TR]
164 ; Res=TR), % useless clause
165 simplify_cnf(T,TR).
166
167 simplify_clause([],[]).
168 simplify_clause([FALSE|T],Res) :- false_lit(FALSE),!, simplify_clause(T,Res).
169 simplify_clause([TRUE|_],_Res) :- true_lit(TRUE),!,fail. % clause useless, it is true
170 simplify_clause([Lit|T],[Lit|Res]) :- simplify_clause(T,Res).
171
172 true_lit(1).
173 true_lit(pred_true).
174 true_lit(neg(L)) :- false_lit(L).
175 false_lit(2).
176 false_lit(pred_false).
177 false_lit(neg(L)) :- true_lit(L).
178
179 % ------------------
180
181 % dispatching code: chooses between Glucose and Z3
182
183 :- use_module(smt_solvers_interface(smt_solvers_interface),[smt_add_cnf/3, smt_add_extra_clause_cnf/2,
184 smt_solve_cnf/2, smt_reset_cnf/1]).
185
186 get_new_solver(z3,Options) :- member(use_satsolver(z3),Options),!.
187 get_new_solver(SolverID,_) :- % use glucose
188 new_solver(SolverID).
189
190 reset_solver(z3) :- !, smt_reset_cnf(z3).
191 reset_solver(SolverID) :- delete_solver(SolverID).
192
193 add_cnf_clauses_to_solver(z3,FVars,AllCnf) :- !,
194 smt_add_cnf(z3,[1,2|FVars],AllCnf).
195 add_cnf_clauses_to_solver(SolverID,_,AllCnf) :-
196 add_cnf_clauses(AllCnf,SolverID).
197
198 add_extra_clause_to_solver(z3,MiniSatCl) :- !,
199 smt_add_extra_clause_cnf(z3,MiniSatCl).
200 add_extra_clause_to_solver(SolverID,MiniSatCl) :-
201 add_clause(SolverID,MiniSatCl).
202
203 solve_and_get_model_from_solver(z3,AVLModel) :- !,
204 smt_solve_cnf(z3,AVLModel).
205 solve_and_get_model_from_solver(SolverID,Model) :-
206 solve(SolverID),
207 debug_format(19,'Get Model~n',[]),
208 get_model(SolverID,[_|Model]). % model will be something like [-2,3,-4]
209
210
211 assign_model_from_solver(z3,FVars,Model) :- !,
212 debug:debug_println(19,assign_z3_model(FVars,Model)),
213 assign_z3_model(FVars,Model).
214 %assign_model_from_solver(_,FVars,Model) :- !,
215 % %write(fvars(FVars)),nl, observe_fvars(FVars),trace,
216 % assign_z3_model(FVars,[1|Model]). % this does the binding in Prolog, TODO: check performance wrt C call below
217 assign_model_from_solver(SolverID,FVars,_Model) :-
218 assign_model(SolverID,[1|FVars]).
219 % Note: assign model calls SP_unify one by one, and can fail when ProB triggers co-routines
220 % Co-routines are, however, only triggered once the full model has been assigned
221
222 % debugging code to observe instantiations:
223 %observe_fvars(FVars) :- observe_fvars(FVars,1,FVars).
224 %observe_fvars([],_,_).
225 %observe_fvars([H|T],I,FVars) :- when(nonvar(H),format('Bound sat var nr. ~w to ~w : ~w~n',[I,H,FVars])), I1 is I+1,
226 % observe_fvars(T,I1,FVars).
227
228 assign_z3_model(VarsList,[1,-2|Model]) :- !, % for z3
229 assign_z3_aux(VarsList,3,Model).
230 assign_z3_model(VarsList,[-2|Model]) :- !, % for glucose, minisat, ...
231 assign_z3_aux(VarsList,3,Model).
232 assign_z3_model(_,Model) :- add_internal_error('Z3 solution incorrect:',assign_z3_model(_,Model)), fail.
233
234 assign_z3_aux([],_,TM) :- !,
235 (TM=[] -> true ; add_internal_error('Too many literals in model:',assign_z3_aux([],_,TM))).
236 assign_z3_aux([H|T],Nr,[Model|TM]) :- !,
237 % format('Assigning ~w VAR to ~w~n',[Nr,Model]),
238 (Model=Nr -> H=pred_true
239 ; Model is -Nr -> H=pred_false
240 ; add_internal_error('Unexpected literal:',assign_z3_aux([H|T],Nr,[Model|TM])),
241 fail
242 ),
243 N1 is Nr+1,
244 assign_z3_aux(T,N1,TM).
245 assign_z3_aux(V,Nr,TM) :- add_internal_error('Model mismatch:',assign_z3_aux(V,Nr,TM)).
246
247 % ------------------
248
249
250 add_cnf_clauses([Cl|Cls],SolverID):-!,
251 to_minisat_cl(Cl,MiniSatCl),
252 %format('Adding clause to solver ~w: ~w~n',[SolverID,MiniSatCl]),
253 add_clause(SolverID,MiniSatCl), % add_clause can fail when SAT solver detects inconsistency directly
254 add_cnf_clauses(Cls,SolverID).
255 add_cnf_clauses([],_):-!.
256
257 to_minisat_cl([],[]).
258 to_minisat_cl([Lit1|TL],[ML1|TM]) :- to_minisat_lit(Lit1,ML1), to_minisat_cl(TL,TM).
259
260 % pred_true/pred_false should be eliminated in simplify_cnf above
261 to_minisat_lit(pred_true,1) :- !.
262 to_minisat_lit(pred_false,2) :- !.
263 to_minisat_lit(neg(NL),MSLit) :- !, to_minisat_neg_lit(NL,MSLit).
264 to_minisat_lit(X,R) :- integer(X),!, R=X. % a Prolog variable that has been bound by bind2index to a number
265 to_minisat_lit(X,R) :- add_internal_error('Illegal literal: ',to_minisat_lit(X,R)), R=X.
266
267 to_minisat_neg_lit(pred_false,1) :- !.
268 to_minisat_neg_lit(pred_true,2) :- !.
269 to_minisat_neg_lit(X,R) :- integer(X),!, R=neg(X). % a Prolog variable that has been bound by bind2index to a number
270 to_minisat_neg_lit(X,R) :- add_internal_error('Illegal literal: ',to_minisat_neg_lit(X,R)), R=neg(X).
271
272 % bind a list of variables to numbers (representing literals in .cnf)
273 bind2index([N|Ns],N,FN) :- N1 is N+1, bind2index(Ns,N1,FN).
274 bind2index([],N,FN):-!, FN is N - 1.