1		% (c) 2012-2026 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		generate_cnf_vig_graph/1, cnf_vig_graph_available/0]).
11
12		:- use_module('../../src/module_information.pl').
13		:- module_info(group,satsolver).
14		:- module_info(description,'This is the interface for ProB to use various SAT solvers (glucose, Z3)').
15
16		:- use_module(probsrc(tools),[start_ms_timer/1, stop_ms_timer_with_msg/2,
17		stop_ms_timer_with_debug_msg/2, get_elapsed_walltime/2]).
18		:- use_module(probsrc(debug),[debug_format/3]).
19		:- use_module(probsrc(error_manager),[add_error/3, add_internal_error/2]).
20		:- use_module(b_to_cnf).
21
22		:- use_module(library(lists), [maplist/2,maplist/3,exclude/3]).
23
24		:- use_module(satsolver). % Glucose API
25
26
27		:- use_module(probsrc(bsyntaxtree), [find_typed_identifier_uses/2, def_get_texpr_id/2]).
28		:- use_module(probsrc(solver_interface), [set_up_typed_localstate_for_pred/4]).
29		:- use_module(probsrc(b_compiler),[b_optimize/6]).
30
31		% call to solve a predicate with sat solver assuming all variables are free:
32		solve_predicate_with_satsolver_free(BFormula,Result) :-
33		solve_predicate_with_satsolver_free(BFormula,_,Result,[]).
34		solve_predicate_with_satsolver_free(BFormula,LocalState,Result,Options) :-
35		find_typed_identifier_uses(BFormula,UsedIdentifiers),
36		set_up_typed_localstate_for_pred(UsedIdentifiers,BFormula,TypedVals,LocalState),
37		b_optimize(BFormula,[],LocalState,[],NewTyped,no_wf_available),
38		solve_predicate_with_satsolver(NewTyped,TypedVals,LocalState,Result,Options).
39
40
41		% call to solve a predicate with sat solver with a provided state with variable/constant values:
42		solve_predicate_with_satsolver_in_state(BFormula,State,Result,Options) :-
43		find_typed_identifier_uses(BFormula,UsedIdentifiers),
44		exclude(is_already_declared_in_state(State),UsedIdentifiers,FilteredIdentifiers),
45		set_up_typed_localstate_for_pred(FilteredIdentifiers,BFormula,TypedVals,LocalState),
46		b_optimize(BFormula,[],LocalState,State,NewTyped,no_wf_available),
47		append(LocalState,State,State2),
48		solve_predicate_with_satsolver(NewTyped,TypedVals,State2,Result,Options).
49		is_already_declared_in_state(State,TID) :- def_get_texpr_id(TID,ID), memberchk(bind(ID,_),State).
50
51		solve_predicate_with_satsolver(BFormula,State) :-
52		solve_predicate_with_satsolver(BFormula,[],State,Result,[]),
53		Result = solution(_).
54
55		solve_predicate_with_satsolver(BFormula,TypedVals,State,Result,Options) :-
56		%write(' :sat '),nl, translate:nested_print_bexpr(BFormula),nl,
57		init_satsolver,!,
58		catch(if(solve_pred2(BFormula,TypedVals,State,Result,Options),true,Result=error),
59		smt_cnf_no_result(Reason), % thrown by smt_solvers_interface when using Z3 as SAT solver
60		cnf_no_result(Reason,Result)).
61		solve_predicate_with_satsolver(_,_,_,error,_).
62
63		cnf_no_result(time_out,Res) :- !, Res=time_out.
64		cnf_no_result(unknown,Res) :- !, Res=no_solution_found(solver_answered_unknown).
65		cnf_no_result(Reason,no_solution_found(Reason)).
66
67		:- use_module(probsrc(b_enumerate), [b_tighter_enumerate_all_values/2]).
68		:- use_module(probsrc(kernel_waitflags),
69		[init_wait_flags_with_call_stack/2,ground_wait_flags/1,
70		ground_det_wait_flag/1]).
71
72		solve_pred2(BFormula,TypedVals,State,Result,Options) :-
73		init_wait_flags_with_call_stack(WF,[prob_command_context(sat_solving,unknown)]),
74		if(solve_pred3(BFormula,State,Result,Options,WF),
75		(b_tighter_enumerate_all_values(TypedVals,WF),
76		ground_wait_flags(WF)),
77		Result=contradiction_found).
78
79		solve_pred3(BFormula,State,Result,Options,WF) :-
80		start_ms_timer(T1),
81		% Note: b_to_cnf will also look up all identifiers
82		(b_to_cnf_wf(BFormula,State,CNF,WF)
83		-> stop_ms_timer_with_profile(T1,b_to_cnf_walltime,'Converting B to CNF'),
84		ground_det_wait_flag(WF),
85		start_ms_timer(T2),
86		%portray_cnf(CNF),
87		%translate:print_bstate(State),nl,
88		solve_cnf(T2,CNF,State,Result,Options)
89		; Result=error
90		).
91
92		solve_cnf(T2,CNF,State,Result,Options) :-
93		bt_sat(CNF,Options),
94		stop_ms_timer_with_profile(T2,sat_walltime,'Formula is SATisfiable'),
95		Result = solution(State).
96		solve_cnf(T2,_,_,_Result,_Options) :-
97		stop_ms_timer_with_profile(T2,sat_walltime,'Formula is UNSATisfiable'),
98		fail. % fail to avoid pending co-routines of b_to_cnf
99
100		:- public portray_cnf/1.
101		portray_cnf(CNF) :- write('CNF:'),nl,maplist(portray_cl,CNF).
102		portray_cl(Clause) :- format(' ~w~n',[Clause]).
103
104
105		:- use_module(library(system),[ datime/1]).
106		:- use_module(probsrc(version),[version_str/1]).
107		:- use_module(probsrc(tools_strings),[number_codes_min_length/3]).
108		:- use_module(probsrc(error_manager), [add_warning/3]).
109		portray_cnf_in_dimacs(Stream,CNF,ClNr,NrVars) :-
110		Offset=2, % assumes that variables start at 3, variable 1 is truth, variable 2 falsity
111		format(Stream,'c Dimacs export by ProB~n',[]),
112		version_str(Str),datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
113		number_codes_min_length(Min,2,MC),
114		format(Stream,'c generated on ~w/~w/~w at ~w:~s using ProB version ~w~n',[Day,Mon,Yr,Hr,MC,Str]),
115		format(Stream,'p cnf ~w ~w~n',[NrVars,ClNr]),
116		maplist(portray_dimacs_clause(Stream,Offset),CNF).
117		portray_dimacs_clause(Stream,Offset,Clause) :- portray_dimacs_cl(Clause,Offset,Stream),format(Stream,'0~n',[]).
118		portray_dimacs_cl([],_,_).
119		portray_dimacs_cl([neg(H)|T],Offset,Stream) :- !, H1 is H-Offset,
120		(H1 < 1 -> add_warning(b2sat,'CNF variable too small: ',H) ; true),
121		format(Stream,'-~w ',H1),
122		portray_dimacs_cl(T,Offset,Stream).
123		portray_dimacs_cl([H|T],Offset,Stream) :- H1 is H-Offset,
124		(H1 < 1 -> add_warning(b2sat,'CNF variable too small: ',H) ; true),
125		format(Stream,'~w ',H1),
126		portray_dimacs_cl(T,Offset,Stream).
127
128		:- use_module(library(between),[between/3]).
129		:- use_module(probsrc(tools_strings),[ajoin/2,ajoin_with_sep/3]).
130		:- use_module(library(lists),[nth1/3]).
131		:- use_module(probsrc(translate),[translate_span/2]).
132
133		:- public cnf_node_predicate/7.
134		% predicates for dot_graph_generator
135		cnf_node_predicate(_CNF,_ClNr,NrVars,Model,NodeID,SubGraph,Attributes) :- SubGraph=none,
136		between(1,NrVars,NodeID), ModelID is NodeID+2,
137		(b2sat_cnf_literal_info(ModelID,Name,Info)
138		-> translate_span(Info,TIP),
139		(Name \= unknown
140		-> ajoin(['x',NodeID,'\n',Name],VarName)
141		; ajoin(['x',NodeID],VarName))
142		; ajoin(['x',NodeID],VarName), TIP = 'Unknown source'
143		),
144		Attributes = [label/VarName,shape/box,style/rounded,color/COL,penwidth/2,tooltip/TIP],
145		(member(ModelID,Model) -> COL=olivedrab2 ; COL=tomato).
146		cnf_node_predicate(CNF,ClNr,NrVars,_Model,NodeID,SubGraph,Attributes) :- SubGraph=none,
147		between(1,ClNr,CID), NodeID is CID+NrVars,
148		nth1(CID,CNF,Clause),
149		convert_clause(Clause,CAtoms,[]),
150		ajoin(['Clause ',CID,'\n'|CAtoms],VarName),
151		Attributes = [label/VarName,shape/box,color/blue].
152
153		convert_clause([A]) --> !, convert_lit(A).
154		convert_clause([A|T]) --> convert_lit(A), ['\x2228\'], convert_clause(T).
155
156		convert_lit(neg(A)) --> !,['\xAC\'],
157		convert_lit(A).
158		convert_lit(A) --> [x],{A1 is A-2},[A1].
159
160
161		:- public cnf_trans_predicate/7.
162		cnf_trans_predicate(CNF,_ClNr,NrVars,Model,RealNodeID,SuccID,[dir/none,color/COL,style/STY,penwidth/2,label/LBL]) :-
163		nth1(CID,CNF,Clause), SuccID is CID+NrVars,
164		member(Lit,Clause),
165		%write(user_output,trans(clause(CID),Lit,Model)),nl(user_output),
166		(Lit = neg(NodeID)
167		-> LBL='-', COL=purple,
168		(member(NodeID,Model) -> STY = dotted ; STY = solid)
169		; NodeID=Lit, LBL='+', COL=black,
170		(member(NodeID,Model) -> STY = solid ; STY = dotted)
171		), RealNodeID is NodeID-2. % literals 1 and 2 are virtual
172
173
174		:- use_module(covsrc(hit_profiler),[add_to_profile_stats/2]).
175		stop_ms_timer_with_profile(Timer,Category,Msg) :-
176		get_elapsed_walltime(Timer,WT),
177		add_to_profile_stats(Category,WT),
178		stop_ms_timer_with_msg(Timer,Msg),
179		flush_output.
180
181
182		% --------------
183
184
185		% backtracking solving:
186		bt_sat(CNF,Options) :-
187		get_new_solver(SolverID,Options),
188		call_cleanup(bt_sat_aux(SolverID,CNF),
189		reset_solver(SolverID)).
190
191		bt_sat_aux(SolverID,CNF) :-
192		addCnf2Solver(SolverID,CNF,FVars,NrVars),!,
193		%write_c_solver_dimacs_file_if_requested(SolverID),
194		debug_format(19,'Solving for ~w sat variables~n',[NrVars]),
195		flush_output,
196		solve_and_get_model_from_solver(SolverID,Model),
197		debug_format(19,'Model = ~w~n',[Model]),
198		bt_sat3(SolverID,FVars,Model).
199		bt_sat_aux(SolverID,_) :-
200		debug_format(19,'Inconsistency detected while adding clauses to SAT Solver ~w~n',[SolverID]),
201		fail.
202
203		:- use_module(probsrc(bmachine),[bmachine_is_precompiled/0, b_absolute_file_name_relative_to_main_machine/2]).
204		:- use_module(probsrc(preferences), [get_preference/2]).
205		%write_c_solver_dimacs_file_if_requested(SolverID) :-
206		% get_preference(path_to_intermediate_output,Path), Path \= '', !,
207		% % TODO: if path is folder, append satsolver_dimacs.cnf
208		% (bmachine_is_precompiled, b_absolute_file_name_relative_to_main_machine(Path,AbsPath) -> true
209		% ; AbsPath=Path),
210		% format('% Writing CNF in Dimacs format for B2SAT solver ~w to file: ~w~n',[SolverID,AbsPath]),
211		% toDimacs(SolverID,AbsPath). % export CNF to Dimacs format, satsolver_dimacs.cnf
212		% % Note: sometimes Glucose simply writes p cnf 0 0 if the solver state is contradictory?!
213		%write_c_solver_dimacs_file_if_requested(_).
214
215
216		:- use_module(probsrc(tools_io),[safe_intelligent_open_file/4]).
217		write_dimacs_file_if_requested(CNF,NrVars) :-
218		get_preference(path_to_intermediate_output,Path), Path \= '', !,
219		length(CNF,ClNr), % the number of clauses after simplification
220		% TODO: if path is folder, append satsolver_dimacs.cnf
221		(bmachine_is_precompiled, b_absolute_file_name_relative_to_main_machine(Path,AbsPath) -> true
222		; AbsPath=Path),
223		format('% Writing CNF in Dimacs format for B2SAT solver to file: ~w~n',[AbsPath]),
224		safe_intelligent_open_file(AbsPath, write, Stream,[encoding(utf8)]),
225		call_cleanup(portray_cnf_in_dimacs(Stream,CNF,ClNr,NrVars),close(Stream)),
226		store_cnf_for_dot(CNF,NrVars). %write_vig_graph_if_requested(CNF,ClNr,NrVars,[]).
227		write_dimacs_file_if_requested(_,_).
228
229		:- dynamic b2sat_model_for_dot/1, b2sat_cnf_for_dot/3.
230
231		:- use_module(probsrc(eventhandling),[register_event_listener/3]).
232		:- register_event_listener(clear_specification,reset_b2sat,
233		'Reset B2SAT.').
234		reset_b2sat :- retractall(b2sat_model_for_dot(_)),
235		retractall(b2sat_cnf_for_dot(_,_,_)).
236
237		store_model_for_dot(Model) :- get_preference(path_to_intermediate_output,Path), Path \= '',!,
238		retractall(b2sat_model_for_dot(_)),
239		assert(b2sat_model_for_dot(Model)). % model will be something like [-2,3,-4]
240		store_model_for_dot(_).
241
242		store_cnf_for_dot(CNF,NrVars) :- get_preference(path_to_intermediate_output,Path), Path \= '',!,
243		retractall(b2sat_cnf_for_dot(_,_,_)),
244		advanced_simplify_cnf(CNF,SCNF),!,
245		length(SCNF,ClNr),
246		assert(b2sat_cnf_for_dot(SCNF,ClNr,NrVars)).
247		store_cnf_for_dot(_,_).
248
249		% generate variable incidence graph if we have stored the infos
250		generate_cnf_vig_graph(File) :- b2sat_cnf_for_dot(CNF,ClNr,NrVars), !,
251		(b2sat_model_for_dot(Model) -> true ; Model = []),
252		gen_cnf_vig_graph(File,CNF,ClNr,NrVars,Model).
253		generate_cnf_vig_graph(_File) :-
254		add_warning(b2sat,'No CNF stored, be sure to set path_to_intermediate_output preference','').
255
256		cnf_vig_graph_available :- b2sat_cnf_for_dot(_,_,_).
257
258		%write_vig_graph_if_requested(CNF,ClNr,NrVars,Model) :- fail,
259		% get_preference(path_to_intermediate_output,Path), Path \= '',
260		% bmachine_is_precompiled, b_absolute_file_name_relative_to_main_machine('cnf_vig_graph.dot',AbsPath),
261		% advanced_simplify_cnf(CNF,SCNF),!,
262		% gen_cnf_vig_graph(AbsPath,SCNF,ClNr,NrVars,Model).
263		%write_vig_graph_if_requested(_,_,_,_).
264
265		% Variable Incidence Graph (VIG)
266		:- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/6,use_new_dot_attr_pred/7,dot_no_same_rank/1, dot_no_subgraph/3]).
267		gen_cnf_vig_graph(File,CNF,ClNr,NrVars,Model) :- GraphAttrs=[],
268		gen_dot_graph(File,GraphAttrs,
269		use_new_dot_attr_pred(b2sat:cnf_node_predicate(CNF,ClNr,NrVars,Model)),
270		use_new_dot_attr_pred(b2sat:cnf_trans_predicate(CNF,ClNr,NrVars,Model)),
271		dot_no_same_rank,dot_no_subgraph).
272
273
274		bt_sat3(SolverID,FVars,Model) :-
275		debug_format(19,'Assigning Model~n',[]),
276		assign_model_from_solver(SolverID,FVars,Model),
277		store_model_for_dot(Model).
278		bt_sat3(SolverID,FVars,Model) :-
279		debug_format(19,'Adding negated model to find another solution~n',[]),
280		add_negated_model(SolverID,Model),
281		solve_and_get_model_from_solver(SolverID,NewModel),
282		bt_sat3(SolverID,FVars,NewModel).
283
284		add_negated_model(SolverID,Model):-
285		maplist(neg,Model,NoAsgn),
286		add_extra_clause_to_solver(SolverID,NoAsgn).
287
288		neg(V,VN) :- VN is -V.
289
290		% -----------------
291
292		addCnf2Solver(SolverID,Cnf,FVars,NrVars):-
293		term_variables(Cnf,FVars),!,
294		length(FVars,NrVars), length(Cnf,ClNr),
295		format('Clauses: ~w, SAT Variables: ~w, Solver ID: ~w ~n',[ClNr,NrVars,SolverID]),
296		add_to_profile_stats(sat_clauses,ClNr),
297		add_to_profile_stats(sat_vars,NrVars),
298		\+ \+ (bind2index(FVars,3,FN),
299		%portray_cnf(Cnf),
300		simplify_cnf(Cnf,SCnf),
301		AllCnf = [[1],[-2]|SCnf], % add true literal 1 and false literal 2
302
303		%nl,portray_cnf(AllCnf),
304		write_dimacs_file_if_requested(SCnf,NrVars),
305		add_cnf_clauses_to_solver(SolverID,[1,2|FVars],FN,AllCnf)
306		).
307
308		% simplify CNF in case ProB propagation now has instantiated some of the SAT variables to pred_true/pred_false/...
309		simplify_cnf([],[]).
310		simplify_cnf([Clause|T],Res) :-
311		(simplify_clause(Clause,SC) % advanced_simplify_clause
312		-> Res=[SC|TR]
313		; Res=TR), % useless clause
314		simplify_cnf(T,TR).
315
316		simplify_clause([],[]).
317		simplify_clause([FALSE|T],Res) :- false_lit(FALSE),!, simplify_clause(T,Res).
318		simplify_clause([TRUE|_],_Res) :- true_lit(TRUE),!,fail. % clause useless, it is true
319		simplify_clause([Lit|T],[Lit|Res]) :- simplify_clause(T,Res).
320
321		true_lit(1).
322		true_lit(pred_true).
323		true_lit(neg(L)) :- false_lit(L).
324		false_lit(2).
325		false_lit(pred_false).
326		false_lit(neg(L)) :- true_lit(L).
327
328		advanced_simplify_cnf([],[]).
329		advanced_simplify_cnf([Clause|T],Res) :-
330		(advanced_simplify_clause(Clause,SC)
331		-> Res=[SC|TR]
332		; Res=TR), % useless clause
333		advanced_simplify_cnf(T,TR).
334
335		:- use_module(library(lists),[remove_dups/2]).
336		% use instead of simplify_clause if you wish to remove some tautologies or duplicate literals before sending them off:
337		advanced_simplify_clause(Clause,SC3) :-
338		simplify_clause(Clause,SC1),
339		sort(SC1,SC2),
340		remove_dups(SC2,SC3),
341		\+ tautology(SC3).
342
343		tautology(SC) :- split_clause(SC,Pos,Neg),
344		member(P,Pos),
345		member(neg(P),Neg). % TODO: advance in Pos and Neg at the same time to obtain linear algorithm
346
347		split_clause([neg(H)|T],[],NegT) :-!, NegT=[neg(H)|T].
348		split_clause([H|T],[H|PosT],NegT) :- split_clause(T,PosT,NegT).
349
350		% ------------------
351
352		% dispatching code: chooses between Glucose and Z3
353
354		:- use_module(smt_solvers_interface(smt_solvers_interface),[smt_add_cnf/3, smt_add_extra_clause_cnf/2,
355		smt_solve_cnf/2, smt_reset_cnf/1]).
356		:- use_module(smt_solvers_interface(solver_dispatcher),[init_interface/1]).
357
358		get_new_solver(z3,Options) :- member(use_satsolver(z3),Options),!,
359		(init_interface(z3) -> true
360		; throw(smt_cnf_no_result(solver_not_available))). % failing would mean the CNF is unsatisfiable
361		get_new_solver(SolverID,_) :- % use glucose
362		new_solver(SolverID).
363
364		% reset_solver is used as cleanup in bt_sat: it must not fail, as SICStus then drops
365		% a pending exception (e.g., smt_cnf_no_result) and call_cleanup fails
366		reset_solver(z3) :- !, (smt_reset_cnf(z3) -> true ; true).
367		reset_solver(SolverID) :- delete_solver(SolverID).
368
369		add_cnf_clauses_to_solver(z3,FVars,_,AllCnf) :- !,
370		smt_add_cnf(z3,[1,2|FVars],AllCnf).
371		add_cnf_clauses_to_solver(SolverID,_,FN,AllCnf) :-
372		% The tautology FN or not(FN) makes Glucose create all variables up to the last literal FN,
373		% even if some of them no longer occur in AllCnf after simplify_cnf.
374		% Otherwise the model would be too short for assign_model, and solutions differing only
375		% in these unconstrained variables would not be enumerated.
376		neg(FN,FNeg),
377		add_clause(SolverID,[FN,FNeg]),
378		add_cnf_clauses(AllCnf,SolverID).
379
380		add_extra_clause_to_solver(z3,MiniSatCl) :- !,
381		smt_add_extra_clause_cnf(z3,MiniSatCl).
382		add_extra_clause_to_solver(SolverID,MiniSatCl) :-
383		add_clause(SolverID,MiniSatCl).
384
385		solve_and_get_model_from_solver(z3,AVLModel) :- !,
386		smt_solve_cnf(z3,AVLModel).
387		solve_and_get_model_from_solver(SolverID,Model) :-
388		solve(SolverID),
389		debug_format(19,'Get Model~n',[]),
390		get_model(SolverID,[_|Model]). % model will be something like [-2,3,-4]
391
392
393		assign_model_from_solver(z3,FVars,Model) :- !,
394		debug:debug_println(19,assign_z3_model(FVars,Model)),
395		assign_z3_model(FVars,Model).
396		%assign_model_from_solver(_,FVars,Model) :- !,
397		% %write(fvars(FVars)),nl, observe_fvars(FVars),trace,
398		% assign_z3_model(FVars,[1|Model]). % this does the binding in Prolog, TODO: check performance wrt C call below
399		assign_model_from_solver(SolverID,FVars,_Model) :-
400		assign_model(SolverID,FVars). % FVars correspond to the literals 3, 4, ...
401		% Note: assign model calls SP_unify one by one, and can fail when ProB triggers co-routines
402		% Co-routines are, however, only triggered once the full model has been assigned
403
404		% debugging code to observe instantiations:
405		%observe_fvars(FVars) :- observe_fvars(FVars,1,FVars).
406		%observe_fvars([],_,_).
407		%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,
408		% observe_fvars(T,I1,FVars).
409
410		assign_z3_model(VarsList,[1,-2|Model]) :- !, % for z3
411		assign_z3_aux(VarsList,3,Model).
412		assign_z3_model(VarsList,[-2|Model]) :- !, % for glucose, minisat, ...
413		assign_z3_aux(VarsList,3,Model).
414		assign_z3_model(_,Model) :- add_internal_error('Z3 solution incorrect:',assign_z3_model(_,Model)), fail.
415
416		assign_z3_aux([],_,TM) :- !,
417		(TM=[] -> true ; add_internal_error('Too many literals in model:',assign_z3_aux([],_,TM))).
418		assign_z3_aux([H|T],Nr,[Model|TM]) :- !,
419		% format('Assigning ~w VAR to ~w~n',[Nr,Model]),
420		(Model=Nr -> H=pred_true
421		; Model is -Nr -> H=pred_false
422		; add_internal_error('Unexpected literal:',assign_z3_aux([H|T],Nr,[Model|TM])),
423		fail
424		),
425		N1 is Nr+1,
426		assign_z3_aux(T,N1,TM).
427		assign_z3_aux(V,Nr,TM) :- add_internal_error('Model mismatch:',assign_z3_aux(V,Nr,TM)).
428
429		% ------------------
430
431
432		add_cnf_clauses([Cl|Cls],SolverID):-!,
433		to_minisat_cl(Cl,MiniSatCl),
434		%format('Adding clause to solver ~w: ~w~n',[SolverID,MiniSatCl]),
435		add_clause(SolverID,MiniSatCl), % add_clause can fail when SAT solver detects inconsistency directly
436		add_cnf_clauses(Cls,SolverID).
437		add_cnf_clauses([],_):-!.
438
439		to_minisat_cl([],[]).
440		to_minisat_cl([Lit1|TL],[ML1|TM]) :- to_minisat_lit(Lit1,ML1), to_minisat_cl(TL,TM).
441
442		% pred_true/pred_false should be eliminated in simplify_cnf above
443		to_minisat_lit(pred_true,1) :- !.
444		to_minisat_lit(pred_false,2) :- !.
445		to_minisat_lit(neg(NL),MSLit) :- !, to_minisat_neg_lit(NL,MSLit).
446		to_minisat_lit(X,R) :- integer(X),!, R=X. % a Prolog variable that has been bound by bind2index to a number
447		to_minisat_lit(X,R) :- add_internal_error('Illegal literal: ',to_minisat_lit(X,R)), R=X.
448
449		to_minisat_neg_lit(pred_false,1) :- !.
450		to_minisat_neg_lit(pred_true,2) :- !.
451		to_minisat_neg_lit(X,R) :- integer(X),!, R=neg(X). % a Prolog variable that has been bound by bind2index to a number
452		to_minisat_neg_lit(X,R) :- add_internal_error('Illegal literal: ',to_minisat_neg_lit(X,R)), R=neg(X).
453
454		% bind a list of variables to numbers (representing literals in .cnf)
455		bind2index([N|Ns],N,FN) :- N1 is N+1, bind2index(Ns,N1,FN).
456		bind2index([],N,FN):-!, FN is N - 1.