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