| 1 | % (c) 2019-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(cdclt_sat_solver, [b_to_cnf_safe/3, | |
| 6 | create_solver_state/1, | |
| 7 | sat/3, | |
| 8 | sat/4, | |
| 9 | sat/5, | |
| 10 | restarts/1, | |
| 11 | is_backjumping/0, | |
| 12 | announce_bt_from_smt_solution/0, | |
| 13 | store_idl_unsat_core/1, | |
| 14 | log_theory_propagation_sat_stack/4, | |
| 15 | set_variable_references_in_clauses/3, | |
| 16 | remove_idl_unsat_core/0, | |
| 17 | unit_propagate_cnf/4, | |
| 18 | get_bindings_from_ids/6, | |
| 19 | portray_cnf/1, | |
| 20 | cnf_to_smt/2, | |
| 21 | clear_pending_theory_propagations/0, | |
| 22 | unfixed_deferred_set_error_occurred/0, | |
| 23 | severe_error_occurred/0, | |
| 24 | assignment_timeout_occurred/0, | |
| 25 | log_det_theory_timeout/1, | |
| 26 | sat_bindings_to_smt_formula/2, | |
| 27 | reset_cdclt_sat_solver/0]). | |
| 28 | ||
| 29 | :- meta_predicate asserta_once(0). | |
| 30 | :- meta_predicate retract_if_exists(0). | |
| 31 | :- meta_predicate retract_once(0). | |
| 32 | :- meta_predicate bt_asserta(0). | |
| 33 | :- meta_predicate bt_retract(0). | |
| 34 | ||
| 35 | :- use_module(library(lists)). | |
| 36 | :- use_module(library(sets), [subtract/3]). | |
| 37 | :- use_module(library(heaps)). | |
| 38 | :- use_module(library(ordsets)). | |
| 39 | :- use_module(library(timeout)). | |
| 40 | :- use_module(library(samsort)). | |
| 41 | :- use_module(library(plunit)). | |
| 42 | ||
| 43 | :- use_module(smt_solvers_interface(ast_optimizer_for_smt)). | |
| 44 | :- use_module(cdclt_solver('cdclt_stats')). | |
| 45 | :- use_module(cdclt_solver('cdclt_pred_to_sat')). | |
| 46 | :- use_module(cdclt_solver('cdclt_settings')). | |
| 47 | :- use_module(cdclt_solver('symmetry_check/sat_symmetry_breaking')). | |
| 48 | :- use_module(probsrc(b_global_sets), [list_contains_unfixed_deferred_set_id/1]). | |
| 49 | :- use_module(probsrc(bsyntaxtree),[get_texpr_expr/2, | |
| 50 | find_typed_identifier_uses/3, | |
| 51 | safe_create_texpr/4, | |
| 52 | create_texpr/4, | |
| 53 | disjunct_predicates/2, | |
| 54 | conjunct_predicates/2, | |
| 55 | conjunction_to_list/2]). | |
| 56 | :- use_module(probsrc(debug)). | |
| 57 | :- use_module(probsrc(preferences), [temporary_set_preference/3, | |
| 58 | reset_temporary_preference/2]). | |
| 59 | :- use_module(probsrc(error_manager), [add_internal_error/2, | |
| 60 | add_error_fail/3, | |
| 61 | check_error_occured/2, | |
| 62 | error_occurred_in_error_scope/0]). | |
| 63 | :- use_module(probsrc(translate), [translate_bexpression/2]). | |
| 64 | :- use_module(extrasrc(unsat_cores), [unsat_core_with_fixed_conjuncts/3, | |
| 65 | unsat_chr_core_list_with_auto_time_limit/5]). | |
| 66 | :- use_module(probsrc(module_information), [module_info/2]). | |
| 67 | :- use_module(extension('banditfuzz/welldef')). | |
| 68 | ||
| 69 | :- use_module(extension('fibonacci_heap/fibonacci_heap')). | |
| 70 | %:- use_module(probsrc(tools_portability), [exists_source/1]). | |
| 71 | ||
| 72 | :- module_info(group, cdclt). | |
| 73 | :- module_info(description,'This module provides the SAT solver for CDCL(T) implementing CDCL with backjumping and further improvements.'). | |
| 74 | ||
| 75 | :- public solver_name/1. % but not used at the moment | |
| 76 | :- dynamic solver_name/1, backjump_clause/6, backjump_level/1, conflict_stats/3, saved_phase/2, restarts/1, | |
| 77 | bt_from_smt_solution/0, is_restart/0, | |
| 78 | %exclude_sat_solution_clause/1, | |
| 79 | total_lbd_sum/1, recent_lbds_dl/2, recent_stack_sizes_dl/2, luby_counter/1, | |
| 80 | %amount_clause_reductions/1, | |
| 81 | amount_learned_clauses/1, idl_unsat_core/1, pending_theory_prop/2, unfixed_deferred_set_error/0, assignment_count_on_cur_level/1, | |
| 82 | glue_level/3, glue_clauses/1, allow_partial_model/0, assignment_timeout_occurred/0. | |
| 83 | ||
| 84 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 85 | % A sat solver utilising delay declaration to implement watched literals. | |
| 86 | % Authors: Jacob Howe and Andy King | |
| 87 | % | |
| 88 | % Extended for CDCL(T) with first UIP conflict-driven clause learning, | |
| 89 | % theory propagation, branching heuristics, phase saving for rapid restarts, | |
| 90 | % learned clause reduction, clause minimization, random restarts, and static SMT symmetry breaking. | |
| 91 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 92 | ||
| 93 | % possible improvements: | |
| 94 | % (- FirstNewCutscheme (cf. https://www.aaai.org/Papers/JAIR/Vol22/JAIR-2210.pdf)) | |
| 95 | % [] improve implying constraint detection (e.g., :cdclt x > y & gt : {x+1} & y > gt) | |
| 96 | % -> might be overkill at some point | |
| 97 | % [] clause minimization (cf. Definition 9, "Towards Understanding and Harnessing the Potential of Clause Learning") | |
| 98 | % [] check out "Advances in Symmetry Breaking for SAT Modulo Theories" by Dinliwal et al. for static SMT symmetry breaking | |
| 99 | ||
| 100 | %:- if(exists_source(library(mutdict))). | |
| 101 | %:- use_module(library(mutdict)). | |
| 102 | %:- else. | |
| 103 | % mutdict throws a segmentation fault in SICStus 4.8.0, don't use it until the bug is fixed | |
| 104 | :- use_module(library(avl)). | |
| 105 | %mutdict_empty(Dict) :- | |
| 106 | % get_mutable(Avl, Dict), | |
| 107 | % empty_avl(Avl). | |
| 108 | ||
| 109 | new_mutdict(Dict) :- | |
| 110 | empty_avl(Avl), | |
| 111 | create_mutable(Avl, Dict). | |
| 112 | ||
| 113 | mutdict_put(Dict, Key, Value) :- | |
| 114 | get_mutable(Avl, Dict), | |
| 115 | avl_store(Key, Avl, Value, NewAvl), | |
| 116 | update_mutable(NewAvl, Dict). | |
| 117 | ||
| 118 | mutdict_get(Dict, Key, Value) :- | |
| 119 | get_mutable(Avl, Dict), | |
| 120 | avl_fetch(Key, Avl, Value). | |
| 121 | ||
| 122 | mutdict_keys(Dict, Keys) :- | |
| 123 | get_mutable(Avl, Dict), | |
| 124 | avl_domain(Avl, Keys). | |
| 125 | ||
| 126 | mutdict_update(Dict, Key, OldValue, NewValue) :- | |
| 127 | get_mutable(Avl, Dict), | |
| 128 | avl_change(Key, Avl, OldValue, NewAvl, NewValue), | |
| 129 | update_mutable(NewAvl, Dict). | |
| 130 | ||
| 131 | %mutdict_delete(Dict, Key) :- | |
| 132 | % get_mutable(Avl, Dict), | |
| 133 | % avl_delete(Key, Avl, _, NewAvl), | |
| 134 | % update_mutable(NewAvl, Dict). | |
| 135 | ||
| 136 | mutdict_items(Dict, Items) :- | |
| 137 | get_mutable(Avl, Dict), | |
| 138 | avl_to_list(Avl, Items). | |
| 139 | ||
| 140 | %mutdict_values(Dict, Values) :- | |
| 141 | % get_mutable(Avl, Dict), | |
| 142 | % avl_range(Avl, Values). | |
| 143 | %:- endif. | |
| 144 | ||
| 145 | pretty_print_clause([], []). | |
| 146 | pretty_print_clause([_-Pol-Var-Name|T], [Pol-Var-Name|NT]) :- | |
| 147 | pretty_print_clause(T, NT). | |
| 148 | ||
| 149 | pretty_print_vars([], []). | |
| 150 | pretty_print_vars([strip-Var|T], [NVar|NT]) :- | |
| 151 | !, | |
| 152 | pretty_print_clause(Var, NVar), | |
| 153 | pretty_print_vars(T, NT). | |
| 154 | pretty_print_vars([Var|T], [Var|NT]) :- | |
| 155 | pretty_print_vars(T, NT). | |
| 156 | ||
| 157 | debug_format_sat(_, _) :- | |
| 158 | print_logs(false), | |
| 159 | !. | |
| 160 | debug_format_sat(Msg, Vars) :- | |
| 161 | append(Msg, " (CDCL(T) SAT Solver)~n", NCodes), | |
| 162 | atom_codes(NMsg, NCodes), | |
| 163 | pretty_print_vars(Vars, NVars), | |
| 164 | format(NMsg, NVars), !. | |
| 165 | ||
| 166 | debug_format_sat(_, _, _) :- | |
| 167 | print_logs(false), | |
| 168 | !. | |
| 169 | debug_format_sat(Msg, Vars, Pred) :- | |
| 170 | format(Msg, Vars), | |
| 171 | translate:print_bexpr(Pred), nl, !. | |
| 172 | ||
| 173 | unfixed_deferred_set_error_occurred :- | |
| 174 | unfixed_deferred_set_error. | |
| 175 | ||
| 176 | assignment_count_on_cur_level(0). | |
| 177 | ||
| 178 | reset_assignment_count_on_level :- | |
| 179 | retract(assignment_count_on_cur_level(Old)), | |
| 180 | asserta(assignment_count_on_cur_level(0)), | |
| 181 | ( true | |
| 182 | ; retract(assignment_count_on_cur_level(_)), | |
| 183 | asserta(assignment_count_on_cur_level(Old)), | |
| 184 | fail | |
| 185 | ). | |
| 186 | ||
| 187 | get_next_assignment_count_on_level(NCount) :- | |
| 188 | retract(assignment_count_on_cur_level(Count)), | |
| 189 | NCount is Count + 1, | |
| 190 | asserta(assignment_count_on_cur_level(NCount)), | |
| 191 | ( true | |
| 192 | ; retract(assignment_count_on_cur_level(_)), | |
| 193 | asserta(assignment_count_on_cur_level(Count)), | |
| 194 | fail | |
| 195 | ). | |
| 196 | ||
| 197 | clear_pending_theory_propagations :- | |
| 198 | retractall_once(pending_theory_prop(_,_)). | |
| 199 | ||
| 200 | % this is just to replay the same order as is propagated to ProB using coroutines | |
| 201 | plvar_sort(_-(_-_-_-(_,(DLevel1,ACount1),_,_)), _-(_-_-_-(_,(DLevel2,ACount2),_,_))) :- | |
| 202 | ground(DLevel1), ground(DLevel2), | |
| 203 | ( DLevel1 < DLevel2 | |
| 204 | -> true | |
| 205 | ; DLevel1 == DLevel2 | |
| 206 | -> ACount1 < ACount2 | |
| 207 | ; fail | |
| 208 | ). | |
| 209 | ||
| 210 | sat_bindings_to_smt_formula(PlVars, SmtFormula) :- | |
| 211 | mutdict_items(PlVars, PlItems), | |
| 212 | samsort(plvar_sort, PlItems, SPlItems), | |
| 213 | sat_bindings_to_smt_formula_aux(SPlItems, b(truth,pred,[]), SmtFormula). | |
| 214 | ||
| 215 | sat_bindings_to_smt_formula_aux([], Acc, Acc). | |
| 216 | sat_bindings_to_smt_formula_aux([_-(PrologVar-_-TTheoryConstraint-_)|T], Acc, SmtFormula) :- | |
| 217 | ground(PrologVar), | |
| 218 | !, | |
| 219 | get_smt_formula_for_sat_pol(TTheoryConstraint, PrologVar, TheoryConstraint), | |
| 220 | safe_create_texpr(conjunct(Acc,TheoryConstraint), pred, [], NAcc), | |
| 221 | sat_bindings_to_smt_formula_aux(T, NAcc, SmtFormula). | |
| 222 | sat_bindings_to_smt_formula_aux([_|T], Acc, SmtFormula) :- | |
| 223 | sat_bindings_to_smt_formula_aux(T, Acc, SmtFormula). | |
| 224 | ||
| 225 | %% get_bindings_from_ids(+SatVars, -StackBindings, -SatBindings, -SatVarNames, -IdPrologVarTuples, -PrologSatVarTriple). | |
| 226 | % Given a set of boolean B identifiers. Create a list of bindings containing terms bind/2 | |
| 227 | % and a list of tuples of B identifier and corresponding Prolog variable used for sat solving. | |
| 228 | % StackBindings contain the bind/2 terms as well as the StackInfo in order to unify Prolog variables in b_to_cnf_safe/3. | |
| 229 | get_bindings_from_ids(SatVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :- | |
| 230 | new_mutdict(EmptyDict), | |
| 231 | get_bindings_from_ids_acc(SatVars, [], [], [], [], EmptyDict, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple), !. | |
| 232 | ||
| 233 | get_bindings_from_ids_acc([], AccStackBindings, AccBindings, AccNames, AccTuples, AccPlVars, AccStackBindings, AccBindings, AccNames, AccTuples, AccPlVars). | |
| 234 | get_bindings_from_ids_acc([b(identifier(Name),IdType,IdInfo)|T], AccStackBindings, AccBindings, AccNames, AccTuples, AccPlVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :- | |
| 235 | NewAccBindings = [bind(Name,PrologVar)|AccBindings], | |
| 236 | % we add Prolog variables for stack infos to each var so that we do not have to maintain a genuine stack | |
| 237 | StackInfo = (_PropType, _Level, _Pol, _OriginalClause), | |
| 238 | NewAccStackBindings = [bind(Name,PrologVar)-StackInfo|AccStackBindings], | |
| 239 | NewAccTuples = [(b(identifier(Name),IdType,IdInfo),PrologVar,StackInfo)|AccTuples], | |
| 240 | !, | |
| 241 | ( member(smt_formula(SmtFormula), IdInfo) | |
| 242 | -> mutdict_put(AccPlVars, Name, PrologVar-Name-SmtFormula-StackInfo) | |
| 243 | ; % plain SAT variable which is not reified with a theory solver, e.g., introduced by CNF optimization rewriting | |
| 244 | OptEq = b(equal(b(identifier(Name),boolean,[]),b(boolean_true,boolean,[])),pred,[]), | |
| 245 | mutdict_put(AccPlVars, Name, PrologVar-Name-OptEq-StackInfo) | |
| 246 | ), | |
| 247 | get_bindings_from_ids_acc(T, NewAccStackBindings, NewAccBindings, [Name|AccNames], NewAccTuples, AccPlVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple). | |
| 248 | get_bindings_from_ids_acc([_|T], AccStackBindings, AccBindings, AccNames, AccTuples, AccPlVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple) :- | |
| 249 | get_bindings_from_ids_acc(T, AccStackBindings, AccBindings, AccNames, AccTuples, AccPlVars, StackBindings, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple). | |
| 250 | ||
| 251 | %% sat(+SolverName, +SolverEnv, +Clauses). | |
| 252 | % SolverEnv is a list [sat_vars:_, sat_varnames:_, sat_bindings:_, t2b_env:_, pl_vars:_]. | |
| 253 | % sat_vars are boolean b/3 identifier ASTs for corresponding SAT variables in Clauses. | |
| 254 | % sat_bindings is a list of terms bind/2 as used by the ProB constraint solver. | |
| 255 | % t2b_env is the environment mapping SAT variable names and theory formulae used to | |
| 256 | % translate B predicates to SAT. | |
| 257 | % pl_vars is a dict of tuples PrologVar-SatVarName-SmtFormula-StackInfo. | |
| 258 | sat(SolverName, SolverEnv, Clauses) :- | |
| 259 | debug_format_sat("Start SAT solving with solver ~w ", [SolverName]), | |
| 260 | init_dynamic_solver_state(SolverName), | |
| 261 | create_solver_state(StateMutable), | |
| 262 | get_from_solver_env(SolverEnv, binary_clause_vars, VarsFromBinaryClauses), | |
| 263 | init_decision_heuristic(StateMutable, VarsFromBinaryClauses, Clauses), | |
| 264 | sat_stateful_pre(SolverEnv, StateMutable, Clauses). | |
| 265 | ||
| 266 | %% sat(+SolverName, +SolverEnv, +StateMutable, +Clauses). | |
| 267 | sat(SolverName, SolverEnv, StateMutable, Clauses) :- | |
| 268 | sat(SolverName, SolverEnv, StateMutable, Clauses, []). | |
| 269 | ||
| 270 | %% sat(+SolverName, +SolverEnv, +StateMutable, +Clauses, +Options). | |
| 271 | % Options: | |
| 272 | % allow_partial_model: only for SMT solving: possibly does not assign all SAT variables, | |
| 273 | % but the reification with ProB ensures that all coroutines are triggered | |
| 274 | sat(SolverName, SolverEnv, StateMutable, Clauses, Options) :- | |
| 275 | debug_format_sat("Start SAT solving with solver ~w ", [SolverName]), | |
| 276 | init_dynamic_solver_state(SolverName), | |
| 277 | ( memberchk(allow_partial_model, Options) | |
| 278 | -> asserta(allow_partial_model) | |
| 279 | ; true | |
| 280 | ), | |
| 281 | get_from_solver_env(SolverEnv, binary_clause_vars, VarsFromBinaryClauses), | |
| 282 | init_decision_heuristic(StateMutable, VarsFromBinaryClauses, Clauses), | |
| 283 | sat_stateful_pre(SolverEnv, StateMutable, Clauses). | |
| 284 | ||
| 285 | % Wrapper for sat_stateful_restart_cp/3 to enable backjumping to level 0 several times. | |
| 286 | sat_stateful_pre(SolverEnv, StateMutable, Clauses) :- | |
| 287 | \+ severe_error_occurred, | |
| 288 | sat_stateful_restart_cp(SolverEnv, StateMutable, Clauses). | |
| 289 | ||
| 290 | sat_stateful_restart_cp(SolverEnv, StateMutable, Clauses) :- | |
| 291 | ( sat_stateful(SolverEnv, StateMutable, Clauses) | |
| 292 | ; % we either learned a unit-clause from conflict analysis or randomly restart | |
| 293 | % in both cases, we learn all asserted backjump clauses | |
| 294 | retract(backjump_level(0)), | |
| 295 | ( retract(is_restart) | |
| 296 | -> debug_format_sat("backjump to level 0 random restart", []), | |
| 297 | backjump_clause(LearnFromLevel,_,_,_,_,_) | |
| 298 | ; debug_format_sat("backjump to level 0", []), | |
| 299 | LearnFromLevel = 0 | |
| 300 | ), | |
| 301 | learn_backjump_clause(LearnFromLevel, SolverEnv, StateMutable), | |
| 302 | sat_stateful_pre(SolverEnv, StateMutable, Clauses) | |
| 303 | ). | |
| 304 | ||
| 305 | %% sat_stateful(+Clauses, +StateMutable, +Clauses). | |
| 306 | % CDCL with first UIP conflict-driven clause learning, two-watched literals, EVSIDS branching heuristic, | |
| 307 | % random glucose restarts, and phase saving for rapid restarts. | |
| 308 | % See create_solver_state/1 for variable StateMutable. | |
| 309 | sat_stateful(SolverEnv, StateMutable, Clauses) :- | |
| 310 | problem_setup(SolverEnv, StateMutable, Clauses), | |
| 311 | %static_sat_symmetry_breaking(Clauses, SolverEnv, CurLevelMut, NewSolverEnv), | |
| 312 | elim_vars(SolverEnv, StateMutable). | |
| 313 | ||
| 314 | %% elim_vars(+SolverEnv, +StateMutable). | |
| 315 | elim_vars(SolverEnv, StateMutable) :- | |
| 316 | \+ severe_error_occurred, | |
| 317 | get_full_state(StateMutable, cur_level, CurLevel), | |
| 318 | NextLevel is CurLevel + 1, | |
| 319 | reset_assignment_count_on_level, | |
| 320 | ( % solution found | |
| 321 | fibonacci_heap:is_empty | |
| 322 | -> true | |
| 323 | ; elim_vars_from_asserted_heuristic_rapid_restart(SolverEnv, StateMutable, NextLevel) | |
| 324 | ). | |
| 325 | ||
| 326 | learn_backjump_clause(CurLevel, SolverEnv, StateMutable) :- | |
| 327 | retract(backjump_clause(BjLevel, BjClause, _, BjSatVars, UsedVars, AC)), | |
| 328 | ( CurLevel == BjLevel | |
| 329 | -> true | |
| 330 | ; add_error_fail(learn_backjump_clause, 'Inconsistent backjump level: ', [BjLevel,CurLevel]) | |
| 331 | ), | |
| 332 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
| 333 | set_variable_references_in_clause(PlVars, BjClause, BjClauseRef), | |
| 334 | clause_setup(SolverEnv, StateMutable, BjClauseRef), | |
| 335 | update_heuristic_scores_for_vars(BjSatVars, AC), | |
| 336 | ( bump_scores_for_bj_clause_only(true) | |
| 337 | ; % additionally bump scores for all variables used during conflict analysis | |
| 338 | bump_scores_for_bj_clause_only(false), | |
| 339 | update_heuristic_scores_for_vars(UsedVars, AC) | |
| 340 | ), !. | |
| 341 | ||
| 342 | possibly_backjump(_, _, _). | |
| 343 | possibly_backjump(SolverEnv, StateMutable, NextLevel) :- | |
| 344 | % backjumping to a level other than 0; skip for restart since we then backjump to level 0 | |
| 345 | \+ is_restart, | |
| 346 | backjump_level(C), | |
| 347 | debug_format_sat("Current level is ~w and bj level is ~w", [NextLevel,C]), | |
| 348 | C == NextLevel, | |
| 349 | retract(backjump_level(C)), | |
| 350 | debug_format_sat("~nbackjump branch prop level ~w", [NextLevel]), | |
| 351 | learn_backjump_clause(C, SolverEnv, StateMutable), | |
| 352 | possibly_bump_glue_variable_scores(NextLevel), | |
| 353 | possibly_backjump(SolverEnv, StateMutable, NextLevel). | |
| 354 | ||
| 355 | possibly_bump_glue_variable_scores(CurLevel) :- | |
| 356 | ( ( glue_bumping(true), | |
| 357 | glue_clauses(GC), | |
| 358 | GC \== 0 | |
| 359 | ) | |
| 360 | -> bump_glue_variable_scores(GC, CurLevel) | |
| 361 | ; true | |
| 362 | ). | |
| 363 | ||
| 364 | bump_glue_variable_scores(GC, CurLevel) :- | |
| 365 | ( bt_retract(glue_level(GlueVar,GlueLevel,AlreadyBumped)) | |
| 366 | -> ( ( \+ AlreadyBumped, | |
| 367 | GlueLevel > CurLevel | |
| 368 | ) | |
| 369 | -> fibonacci_heap:get_priority_of(GlueVar, Score), | |
| 370 | bump_glue_variable_score(Score, GlueVar, GlueLevel, GC), | |
| 371 | bump_glue_variable_scores(GC, CurLevel), | |
| 372 | bt_asserta(glue_level(GlueVar,GlueLevel,true)) | |
| 373 | ; bump_glue_variable_scores(GC, CurLevel), | |
| 374 | bt_asserta(glue_level(GlueVar,GlueLevel,AlreadyBumped)) | |
| 375 | ) | |
| 376 | ; true | |
| 377 | ). | |
| 378 | ||
| 379 | bump_glue_variable_score(Score, SatVarName, GlueLevel, GC) :- | |
| 380 | GlueBump is Score * (GlueLevel/GC), | |
| 381 | NScore is Score + GlueBump, | |
| 382 | fibonacci_heap:update_bt(SatVarName, NScore). | |
| 383 | ||
| 384 | %% elim_vars_from_asserted_heuristic_rapid_restart(+SolverEnv, +StateMutable, +NextLevel). | |
| 385 | elim_vars_from_asserted_heuristic_rapid_restart(SolverEnv, StateMutable, NextLevel) :- | |
| 386 | \+ backjump_level(_), | |
| 387 | \+ idl_unsat_core(_), | |
| 388 | get_sat_var_with_max_heuristic(SatVarName, MaxScore), | |
| 389 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
| 390 | mutdict_get(PlVars, SatVarName, Var-SatVarName-_-StackInfo), % we need the variable's references | |
| 391 | debug_format_sat("Max heuristic value with score ~w is ~w", [MaxScore,SatVarName]), | |
| 392 | possibly_backjump(SolverEnv, StateMutable, NextLevel), | |
| 393 | ( saved_phase(SatVarName, SavedPol) | |
| 394 | -> % restore phase/polarity from cache for rapid restart | |
| 395 | SelectedPol = SavedPol, | |
| 396 | retract(saved_phase(SatVarName, _)), % don't undo when backtracking | |
| 397 | debug_format_sat("Restore phase of ~w", [SatVarName]) | |
| 398 | ; % uninformed phase/polarity selection: start with truth | |
| 399 | SelectedPol = pred_true | |
| 400 | ), | |
| 401 | elim_var_for_phase(SatVarName, StackInfo, SelectedPol, Var, SolverEnv, StateMutable, NextLevel). | |
| 402 | ||
| 403 | %% elim_var_for_phase(+SatVarName, +StackInfo, +SavedPol, +Var, +SolverEnv, +StateMutable, +NextLevel). | |
| 404 | elim_var_for_phase(SatVarName, StackInfo, SavedPol, Var, SolverEnv, StateMutable, NextLevel) :- | |
| 405 | ( ground(Var) | |
| 406 | -> add_error_fail(elim_var_for_phase, 'Decision variable is already ground: probably an error in the decision heuristic.', [SatVarName]) | |
| 407 | ; true | |
| 408 | ), | |
| 409 | update_full_state(StateMutable, cur_level, NextLevel), | |
| 410 | get_next_assignment_count_on_level(ACount), | |
| 411 | ( StackInfo = (branch,(NextLevel,ACount),SavedPol,_OriginalClause), | |
| 412 | bt_log_sat_stack(StateMutable, SatVarName, SavedPol), | |
| 413 | debug_format_sat("Decide variable ~w with polarity ~w on level ~w", [SatVarName,SavedPol,NextLevel]), | |
| 414 | log_boolean_decision, | |
| 415 | Var = SavedPol | |
| 416 | ; \+ backjump_level(_), | |
| 417 | \+ severe_error_occurred, | |
| 418 | negate_polarity(SavedPol, NegSavedPol), | |
| 419 | StackInfo = (branch,(NextLevel,ACount),NegSavedPol,_OriginalClause), | |
| 420 | bt_log_sat_stack(StateMutable, SatVarName, NegSavedPol), | |
| 421 | debug_format_sat("Decide variable ~w with polarity ~w on level ~w", [SatVarName,NegSavedPol,NextLevel]), | |
| 422 | log_boolean_decision, | |
| 423 | Var = NegSavedPol | |
| 424 | ), | |
| 425 | elim_vars(SolverEnv, StateMutable). | |
| 426 | ||
| 427 | %% checkout_sat_variable(+SatVarName, +OriginalClause). | |
| 428 | % Remove a SAT variable's information if it has been propagated. | |
| 429 | checkout_sat_variable(SatVarName, OriginalClause) :- | |
| 430 | delete_from_heuristic(SatVarName), | |
| 431 | retract_if_exists(saved_phase(SatVarName, _)), | |
| 432 | ( allow_partial_model | |
| 433 | -> worsen_scores_for_vars_in_clause(OriginalClause) | |
| 434 | ; true | |
| 435 | ). | |
| 436 | ||
| 437 | worsen_scores_for_vars_in_clause([]). | |
| 438 | worsen_scores_for_vars_in_clause([_-_-_-SatVarName|T]) :- | |
| 439 | ( fibonacci_heap:get_priority_of_silent_fail(SatVarName, Score) | |
| 440 | -> ( Score > 1, | |
| 441 | fibonacci_heap:dec_priority_of_bt(SatVarName, 1) | |
| 442 | ; Score =< 1, | |
| 443 | fibonacci_heap:delete_elm_bt(SatVarName) | |
| 444 | ), | |
| 445 | worsen_scores_for_vars_in_clause(T) | |
| 446 | ; worsen_scores_for_vars_in_clause(T) | |
| 447 | ). | |
| 448 | ||
| 449 | problem_setup(_, _, []). | |
| 450 | problem_setup(SolverEnv, StateMutable, [Clause|Clauses]) :- | |
| 451 | clause_setup(SolverEnv, StateMutable, Clause), | |
| 452 | problem_setup(SolverEnv, StateMutable, Clauses). | |
| 453 | ||
| 454 | clause_setup(SolverEnv, StateMutable, Clause) :- | |
| 455 | Clause = [StackInfo-Pol-Var-SatVarName|Triples], | |
| 456 | set_watch(SolverEnv, StateMutable, Clause, Triples, Var, Pol, SatVarName, StackInfo). | |
| 457 | ||
| 458 | set_polarity_of_var_explicitly(_, _, [], []). | |
| 459 | set_polarity_of_var_explicitly(SatVarName, Pol, [CPol-CVar-CName|T], ConflictClause) :- | |
| 460 | var(CVar), | |
| 461 | SatVarName == CName, | |
| 462 | !, | |
| 463 | ConflictClause = [CPol-Pol-CName|T]. | |
| 464 | set_polarity_of_var_explicitly(SatVarName, Pol, [Triple|T], [Triple|NT]) :- | |
| 465 | set_polarity_of_var_explicitly(SatVarName, Pol, T, NT). | |
| 466 | ||
| 467 | set_watch(_, _, OriginalClause, [], Var, Pol, SatVarName, _) :- | |
| 468 | Var == Pol, | |
| 469 | checkout_sat_variable(SatVarName, OriginalClause). | |
| 470 | set_watch(SolverEnv, StateMutable, OriginalClause, [], Var, Pol, _, _) :- | |
| 471 | ground(Var), | |
| 472 | Var \== Pol, | |
| 473 | \+ severe_error_occurred, | |
| 474 | \+ backjump_level(_), | |
| 475 | debug_format_sat("sat conflict", []), | |
| 476 | clause_learning(true), | |
| 477 | possibly_bt_from_smt_solution(SolverEnv,StateMutable, _, _), | |
| 478 | get_full_state(StateMutable, current_stack_size, StackSize), | |
| 479 | get_full_state(StateMutable, cur_level, CurLevel), | |
| 480 | assignment_count_on_cur_level(ACount), | |
| 481 | ACount \== 1, % at least one unit-propagation for CDCL, otherwise just backtrack to the last decision | |
| 482 | compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, CurLevel, OriginalClause), | |
| 483 | fail. | |
| 484 | set_watch(SolverEnv, StateMutable, OriginalClause, [], Var, Pol, SatVarName, StackInfo) :- | |
| 485 | var(Var), | |
| 486 | \+ severe_error_occurred, | |
| 487 | \+ backjump_level(_), | |
| 488 | get_full_state(StateMutable, cur_level, CurLevel), | |
| 489 | debug_format_sat("unit propagation of ~w with polarity ~w on level ~w due to clause ~w", [SatVarName,Pol,CurLevel,strip-OriginalClause]), | |
| 490 | %translate:print_bexpr(TheoryFormula),nl, | |
| 491 | get_next_assignment_count_on_level(ACount), | |
| 492 | StackInfo = (unit,(CurLevel,ACount),Pol,OriginalClause), | |
| 493 | bt_log_sat_stack(StateMutable, SatVarName, Pol), | |
| 494 | log_unit_propagation, | |
| 495 | ( checkout_sat_variable(SatVarName, OriginalClause), | |
| 496 | Var = Pol, | |
| 497 | ( true | |
| 498 | ; % remove idl unsat core from higher decision level when backtracking | |
| 499 | remove_idl_unsat_core, | |
| 500 | fail | |
| 501 | ) | |
| 502 | ; % theory conflict: if Var = Pol triggered a SAT conflict instead, | |
| 503 | % a backjump clause has been computed and backjump_level/1 is asserted | |
| 504 | clause_learning(true), | |
| 505 | \+ severe_error_occurred, | |
| 506 | \+ backjump_level(_), % skip when backjumping | |
| 507 | get_last_decision_level(StateMutable, LastDLevel), % skip if no decision so far | |
| 508 | LastDLevel > 0, % just backtrack if last decision level is 1 or 0 | |
| 509 | possibly_bt_from_smt_solution(SolverEnv,StateMutable, SatVarName, Pol), | |
| 510 | ( learn_idl_core(StateMutable, SolverEnv, SatVarName, Pol) | |
| 511 | -> true | |
| 512 | ; debug_format_sat("theory conflict on level ~w", [CurLevel]), | |
| 513 | get_conflict_clause_for_theory_conflict(SolverEnv, SatVarName, Pol, SolverEnv, TConflictClause), | |
| 514 | % explicitly set the polarity which failed to be assigned above in line 414 for conflict analysis (possibly part of the unsat core) | |
| 515 | set_polarity_of_var_explicitly(SatVarName, Pol, TConflictClause, ConflictClause), | |
| 516 | ( ConflictClause = [SStackInfo-CPol-SingletonVar-SingletonName] | |
| 517 | -> % singleton theory conflict: backjump to level 0 | |
| 518 | debug_format_sat("backjump to level 0 after finding singleton theory conflict for SAT variable ~w", [SingletonName]), | |
| 519 | ( ground(SingletonVar) | |
| 520 | -> negate_polarity(SingletonVar, NSingletonPol) | |
| 521 | ; % static WD PO theory contradiction | |
| 522 | debug_format_sat("Force static theory conflict of WD condition to be false for ~w.", [SingletonName]), | |
| 523 | NSingletonPol = CPol | |
| 524 | ), | |
| 525 | BjClause = [SStackInfo-NSingletonPol-SingletonVar-SingletonName], | |
| 526 | debug_format_sat("learn unit clause ~w", [strip-BjClause]), | |
| 527 | BjLevel = 0, | |
| 528 | compute_lbd_score(BjClause, LbdScore), | |
| 529 | count_found_conflict(NewTotal, _, _), | |
| 530 | asserta(backjump_clause(BjLevel, BjClause, LbdScore, [SingletonName], [], NewTotal)), | |
| 531 | asserta(backjump_level(BjLevel)) | |
| 532 | ; get_maximum_decision_level(ConflictClause, ConflictLevel), | |
| 533 | % it can be the case that ProB first recognizes unsatisfiable after grounding waitflags; the last decision level is then not necessarily the conflict level | |
| 534 | debug_format_sat("theory conflict on level ~w after unsat core computation", [ConflictLevel]), | |
| 535 | get_full_state(StateMutable, current_stack_size, StackSize), | |
| 536 | compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, _BjLevel) | |
| 537 | ) | |
| 538 | ), | |
| 539 | fail | |
| 540 | ). | |
| 541 | set_watch(SolverEnv, StateMutable, OriginalClause, [StackInfo2-Pol2-Var2-Name2|Triples], Var1, Pol1, Name1, StackInfo1):- | |
| 542 | \+ backjump_level(_), | |
| 543 | watch(SolverEnv, StateMutable, OriginalClause, StackInfo1, Var1, Pol1, Name1, StackInfo2, Var2, Pol2, Name2, Triples). | |
| 544 | ||
| 545 | :- block watch(?, ?, ?, ?, -, ?, ?, ?, -, ?, ?, ?). | |
| 546 | watch(SolverEnv, StateMutable, OriginalClause, StackInfo1, Var1, Pol1, Name1, StackInfo2, Var2, Pol2, Name2, Triples) :- | |
| 547 | ( nonvar(Var1) | |
| 548 | -> update_watch(SolverEnv, StateMutable, OriginalClause, StackInfo1, Var1, Pol1, Name1, StackInfo2, Var2, Pol2, Name2, Triples) | |
| 549 | ; update_watch(SolverEnv, StateMutable, OriginalClause, StackInfo2, Var2, Pol2, Name2, StackInfo1, Var1, Pol1, Name1, Triples) | |
| 550 | ). | |
| 551 | ||
| 552 | update_watch(SolverEnv, StateMutable, OriginalClause, _, Var1, Pol1, Name1, StackInfo2, Var2, Pol2, Name2, Triples) :- | |
| 553 | ( Var1 == Pol1 | |
| 554 | -> checkout_sat_variable(Name1, OriginalClause) | |
| 555 | ; set_watch(SolverEnv, StateMutable, OriginalClause, Triples, Var2, Pol2, Name2, StackInfo2) | |
| 556 | ). | |
| 557 | ||
| 558 | retract_once(Assertion) :- | |
| 559 | retract(Assertion), | |
| 560 | !. | |
| 561 | ||
| 562 | severe_error_occurred :- | |
| 563 | error_occurred_in_error_scope, | |
| 564 | check_error_occured(ErrorName, _), | |
| 565 | ErrorName \= warning(_), | |
| 566 | ErrorName \== clpfd_overflow, | |
| 567 | ErrorName \== smt_symmetry_breaking, | |
| 568 | ErrorName \== well_definedness_error, | |
| 569 | ErrorName \== smt_solvers_interface, | |
| 570 | ErrorName \== internal_error(smt_solvers_interface). | |
| 571 | ||
| 572 | %% is_backjumping. | |
| 573 | is_backjumping :- | |
| 574 | backjump_level(_). | |
| 575 | ||
| 576 | assert_update_pending_theory_propagation(SatVarName, Pol) :- | |
| 577 | retract(pending_theory_prop(SatVarName,_)), | |
| 578 | !, | |
| 579 | asserta(pending_theory_prop(SatVarName,Pol)). | |
| 580 | assert_update_pending_theory_propagation(SatVarName, Pol) :- | |
| 581 | asserta(pending_theory_prop(SatVarName,Pol)). | |
| 582 | ||
| 583 | % We use a time limit in b_interpreter:b_convert_bool_timeout/7 which is observed here. | |
| 584 | % It can be the case that ProB/CLP(FD) exceeds the predefined global time limit | |
| 585 | % when assigning a SAT variable in the deterministic propagation phase (b_convert_bool). | |
| 586 | % Simply setting a time limit on the SAT variable's unification in the SAT solver is not possible | |
| 587 | % since CDCL etc. would also be affected by this time limit due to coroutines. | |
| 588 | :- block log_det_theory_timeout(-). | |
| 589 | log_det_theory_timeout(TORes) :- | |
| 590 | ( TORes == time_out | |
| 591 | -> asserta(assignment_timeout_occurred), | |
| 592 | debug_format_sat("Det Theory Timeout", []) | |
| 593 | ; true | |
| 594 | ). | |
| 595 | ||
| 596 | %% log_theory_propagation_sat_stack(+StateMutable, +SatVarName, +SatPrologVar, +StackInfo). | |
| 597 | log_theory_propagation_sat_stack(StateMutable, SatVarName, SatPrologVar, StackInfo) :- | |
| 598 | get_full_state(StateMutable, cur_level, CurLevel), | |
| 599 | log_theory_propagation, | |
| 600 | !, | |
| 601 | debug_format_sat("Theory propagation of ~w with polarity ~w", [SatVarName,SatPrologVar]), | |
| 602 | ( SatPrologVar == pred_true -> Pol = pred_true; Pol = pred_false), | |
| 603 | assert_update_pending_theory_propagation(SatVarName, Pol), | |
| 604 | % explanation (OriginalClause) is computed lazily for conflict analysis if necessary, see explain_theory_propagation/5 | |
| 605 | get_next_assignment_count_on_level(ACount), | |
| 606 | StackInfo = (theory,(CurLevel,ACount),Pol,_), | |
| 607 | bt_log_sat_stack(StateMutable, SatVarName, Pol). | |
| 608 | ||
| 609 | %% learn_idl_core(+StateMutable, +SolverEnv, +LastSatVarName, +FailedPol). | |
| 610 | learn_idl_core(StateMutable, SolverEnv, LastSatVarName, FailedPol) :- | |
| 611 | retract(idl_unsat_core(Core)), | |
| 612 | remove_idl_unsat_core, | |
| 613 | !, | |
| 614 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
| 615 | get_conflict_clause_from_unsat_core(Core, SolverEnv, TConflictClause), | |
| 616 | % explicitly assign the polarity which was undone due to the conflict | |
| 617 | set_polarity_of_var_explicitly(LastSatVarName, FailedPol, TConflictClause, TTConflictClause), | |
| 618 | set_variable_references_in_clause(PlVars, TTConflictClause, ConflictClause), | |
| 619 | get_full_state(StateMutable, current_stack_size, StackSize), | |
| 620 | get_full_state(StateMutable, cur_level, CurLevel), | |
| 621 | compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, CurLevel, ConflictClause). | |
| 622 | ||
| 623 | save_phase(SatVarName, Pol) :- | |
| 624 | (retract(saved_phase(SatVarName, _)), !; true), | |
| 625 | asserta(saved_phase(SatVarName, Pol)). | |
| 626 | ||
| 627 | % Log variable assignments. | |
| 628 | % Effect is undone when backtracking. Cache phase when backtracking and unassigning a variable. | |
| 629 | bt_log_sat_stack(StateMutable, SatVarName, Pol) :- | |
| 630 | increase_stack_size(StateMutable), | |
| 631 | ( true | |
| 632 | ; save_phase(SatVarName, Pol), | |
| 633 | fail | |
| 634 | ). | |
| 635 | ||
| 636 | increase_stack_size(StateMutable) :- | |
| 637 | get_full_state(StateMutable, current_stack_size, Old), | |
| 638 | New is Old + 1, !, | |
| 639 | update_full_state(StateMutable, current_stack_size, New). | |
| 640 | ||
| 641 | %% possibly_bt_from_smt_solution(+SolverEnv,+StateMutable, +SatVarName, +Pol). | |
| 642 | % Backtracking from an SMT solution which should not be handled as a theory conflict. | |
| 643 | possibly_bt_from_smt_solution(_SolverEnv,StateMutable, _SatVarName, _Pol) :- | |
| 644 | retract(bt_from_smt_solution), | |
| 645 | !, | |
| 646 | %( ground(SatVarName) | |
| 647 | %-> get_complete_theory_lemma_fixed_binding(SolverEnv, SatVarName, Pol, TheoryLemmaClause) | |
| 648 | %; get_complete_theory_lemma(SolverEnv, TheoryLemmaClause) | |
| 649 | %), | |
| 650 | % backjump to the last decision level without computing a conflict clause | |
| 651 | % but excluding the last SAT solution when backtracking after finding an SMT solution | |
| 652 | get_last_decision_level(StateMutable, Level), | |
| 653 | %asserta(exclude_sat_solution_clause(TheoryLemmaClause)), % not used currently | |
| 654 | asserta(backjump_level(Level)), | |
| 655 | fail. | |
| 656 | possibly_bt_from_smt_solution(_,_, _, _). | |
| 657 | ||
| 658 | % Just wrap with negation but prevent double negation. | |
| 659 | negate_smt_formula(b(negation(Smt),pred,_), NegSmt) :- | |
| 660 | !, | |
| 661 | NegSmt = Smt. | |
| 662 | negate_smt_formula(Smt, b(negation(Smt),pred,[])). | |
| 663 | ||
| 664 | % iterate over all Prolog variables to find the propagated literals: usually a stack is used but we store stack infos besides each | |
| 665 | % variable in the clauses; explanation of theory propagations is rare and maintaining a genuine stack is more expensive | |
| 666 | get_propagated_sat_vars([], _, []). | |
| 667 | get_propagated_sat_vars([SatVarName-(_-_-_-(_,(Level,_ACount),Pol,_))|T], TheoryPropLevel, SatVarNameTuples) :- | |
| 668 | ground(Level), | |
| 669 | Level < TheoryPropLevel, | |
| 670 | !, | |
| 671 | SatVarNameTuples = [(SatVarName-Pol)|NT], | |
| 672 | get_propagated_sat_vars(T, TheoryPropLevel, NT). | |
| 673 | get_propagated_sat_vars([_|T], TheoryPropLevel, NT) :- | |
| 674 | get_propagated_sat_vars(T, TheoryPropLevel, NT). | |
| 675 | ||
| 676 | %% explain_theory_propagation(+SolverEnv, +TheoryPropSatVar, +TheoryPropLevel, +TheoryPropPol, -ExplainingClause). | |
| 677 | explain_theory_propagation(SolverEnv, TheoryPropSatVar, _, _, ExplainingClause) :- | |
| 678 | minimize_theory_explanations(false), | |
| 679 | !, | |
| 680 | debug_format_sat("Use complete lemma for theory explanation of ~w", [TheoryPropSatVar]), | |
| 681 | get_from_solver_env(SolverEnv, sat_bindings, SatBindings), | |
| 682 | get_clause_from_ground_bindings(SatBindings, _, _, [], TExplainingClause), | |
| 683 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
| 684 | set_variable_references_in_clause(PlVars, TExplainingClause, ExplainingClause), | |
| 685 | debug_format_sat("finished explanation.", []). | |
| 686 | explain_theory_propagation(SolverEnv, TheoryPropSatVar, TheoryPropLevel, TheoryPropPol, ExplainingClause) :- | |
| 687 | debug_format_sat("Explain theory propagation of ~w", [TheoryPropSatVar]), | |
| 688 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
| 689 | mutdict_items(PlVars, PlVarsList), | |
| 690 | get_propagated_sat_vars(PlVarsList, TheoryPropLevel, SatVarNameTuples), | |
| 691 | get_from_solver_env(SolverEnv, sat_vars, SatVars), | |
| 692 | get_smt_formula_from_vars_for_sat_pol(SatVars, TheoryPropSatVar, TheoryPropPol, SmtFormula), | |
| 693 | negate_smt_formula(SmtFormula, NegSmt), | |
| 694 | debug_format_sat("Compute unsat core for explanation: ", [], NegSmt), | |
| 695 | get_explanation_candidate_formula(SatVars, SatVarNameTuples, CandidateFormula), | |
| 696 | ( SatVarNameTuples = [_] | |
| 697 | -> safe_create_texpr(conjunct(CandidateFormula,NegSmt), pred, [], UnsatCore) | |
| 698 | ; temporary_set_preference(time_out, 25, Change1), | |
| 699 | temporary_set_preference(unsat_core_algorithm, linear, Change2), | |
| 700 | call_cleanup(unsat_core_with_fixed_conjuncts(CandidateFormula, NegSmt, TTUnsatCore), | |
| 701 | (reset_temporary_preference(unsat_core_algorithm, Change2), | |
| 702 | reset_temporary_preference(time_out, Change1))), | |
| 703 | safe_create_texpr(conjunct(TTUnsatCore,NegSmt), pred, [], TUnsatCore), | |
| 704 | ( strip_pos_keep_toplevel_conj(TUnsatCore, UnsatCore) | |
| 705 | -> true | |
| 706 | ; add_error_fail(strip_pos_keep_toplevel_conj, 'Removing WD POs for CDCL(T) failed for explaining theory propagation.', [unsat_core_with_wd:TUnsatCore]) | |
| 707 | ) | |
| 708 | ), | |
| 709 | get_from_solver_env(SolverEnv, t2b_env, T2BEnv), | |
| 710 | debug_format_sat("Computed unsat core for explanation: ", [], UnsatCore), | |
| 711 | ( | |
| 712 | ( | |
| 713 | predicate_to_sat(only_reuse, [], SatVars, T2BEnv, UnsatCore, _NewEnv, _, UnsatCoreSat, _NewSatVars), | |
| 714 | sat_conj_negate_to_clause(UnsatCoreSat, TExplainingClause) | |
| 715 | ) | |
| 716 | -> true | |
| 717 | ; add_error_fail(sat_conj_negate_to_clause, 'Explaining theory propagation failed: Explanation cannot be transformed to SAT.', [unsat_core:UnsatCore]) | |
| 718 | ), | |
| 719 | debug_format_sat("finished explanation.", []), | |
| 720 | set_variable_references_in_clause(PlVars, TExplainingClause, TTExplainingClause), | |
| 721 | sort(TTExplainingClause, ExplainingClause). | |
| 722 | ||
| 723 | get_explanation_candidate_formula(SatVars, [SatVarName-Pol|T], CandidateFormula) :- | |
| 724 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula), | |
| 725 | !, | |
| 726 | get_explanation_candidate_formula_acc(SatVars, T, SmtFormula, CandidateFormula). | |
| 727 | get_explanation_candidate_formula(SatVars, [_|T], CandidateFormula) :- | |
| 728 | % can be artificial SAT variable introduced by cnf rewriting | |
| 729 | get_explanation_candidate_formula(SatVars, T, CandidateFormula). | |
| 730 | ||
| 731 | get_explanation_candidate_formula_acc(_, [], Acc, Acc). | |
| 732 | get_explanation_candidate_formula_acc(SatVars, [SatVarName-Pol|T], Acc, CandidateFormula) :- | |
| 733 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula), | |
| 734 | !, | |
| 735 | safe_create_texpr(conjunct(SmtFormula,Acc), pred, [], NAcc), | |
| 736 | get_explanation_candidate_formula_acc(SatVars, T, NAcc, CandidateFormula). | |
| 737 | get_explanation_candidate_formula_acc(SatVars, [_|T], Acc, CandidateFormula) :- | |
| 738 | get_explanation_candidate_formula_acc(SatVars, T, Acc, CandidateFormula). | |
| 739 | ||
| 740 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula) :- | |
| 741 | memberchk(b(identifier(SatVarName),_,Info), SatVars), | |
| 742 | member(smt_formula(TSmtFormula), Info), | |
| 743 | get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula). | |
| 744 | ||
| 745 | get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula) :- | |
| 746 | ( Pol == pred_true | |
| 747 | -> SmtFormula = TSmtFormula | |
| 748 | ; TSmtFormula = b(negation(SmtFormula),pred,[]) | |
| 749 | -> true | |
| 750 | ; TSmtFormula = b(_,_,Info), | |
| 751 | SmtFormula = b(negation(TSmtFormula),pred,Info) | |
| 752 | ). | |
| 753 | ||
| 754 | %% get_sat_var_with_max_heuristic(-SatVarName, -MaxScore). | |
| 755 | get_sat_var_with_max_heuristic(SatVarName, MaxScore) :- | |
| 756 | %\+ fibonacci_heap:is_empty, | |
| 757 | ( print_logs(true) | |
| 758 | -> fibonacci_heap:get_max_priority(MaxScore) | |
| 759 | ; MaxScore = -1 | |
| 760 | ), | |
| 761 | fibonacci_heap:get_and_remove_max_value_bt(SatVarName). | |
| 762 | ||
| 763 | retract_if_exists(Assertion) :- | |
| 764 | ( cdclt_sat_solver:Assertion | |
| 765 | -> retract(cdclt_sat_solver:Assertion) | |
| 766 | ; true | |
| 767 | ). | |
| 768 | ||
| 769 | % Periodically decay heuristic scores for VSIDS heuristic. | |
| 770 | % Not undone when backtracking. | |
| 771 | possibly_decay_heuristic_values :- | |
| 772 | decision_heuristic(vsids), | |
| 773 | conflict_stats(total(AC), _, _), | |
| 774 | AC \== 0, | |
| 775 | vsids_decay_frequency(I), | |
| 776 | C is AC mod I, | |
| 777 | C == 0, | |
| 778 | debug_format_sat("~nDecay heuristic scores", []), | |
| 779 | !, | |
| 780 | vsids_decay_value(Val), | |
| 781 | decay_heuristic_values(Val). | |
| 782 | possibly_decay_heuristic_values. | |
| 783 | ||
| 784 | %% decay_heuristic_values(+DecayValue). | |
| 785 | % Not undone when backtracking. | |
| 786 | decay_heuristic_values(DecayValue) :- | |
| 787 | Decay is (1/DecayValue), | |
| 788 | fibonacci_heap:mult_priority_of_all(Decay). | |
| 789 | ||
| 790 | %% init_decision_heuristic(+StateMutable, +VarsFromBinaryClauses, +Clauses). | |
| 791 | % Each variable is initially assigned the number of its occurrences in all clauses as its score. | |
| 792 | % Variable scores are not split for polarities. | |
| 793 | init_decision_heuristic(StateMutable, VarsFromBinaryClauses, Clauses) :- | |
| 794 | count_var_occurrences_in_clauses(Clauses, VarScoreTuples), | |
| 795 | binary_boost_factor(BoostFactor), | |
| 796 | add_heuristic_tuples(StateMutable, BoostFactor, VarsFromBinaryClauses, VarScoreTuples). | |
| 797 | ||
| 798 | add_heuristic_tuples(_, _, _, []). | |
| 799 | add_heuristic_tuples(StateMutable, BoostFactor, VarsFromBinaryClauses, [SatVarName-Score|T]) :- | |
| 800 | ( select(SatVarName, VarsFromBinaryClauses, TVarsFromBinaryClauses) | |
| 801 | -> NScore is Score * BoostFactor | |
| 802 | ; NScore = Score, | |
| 803 | TVarsFromBinaryClauses = VarsFromBinaryClauses | |
| 804 | ), | |
| 805 | fibonacci_heap:push(NScore, SatVarName), | |
| 806 | add_heuristic_tuples(StateMutable, BoostFactor, TVarsFromBinaryClauses, T). | |
| 807 | ||
| 808 | count_var_occurrences_in_clauses(Clauses, DictItems) :- | |
| 809 | new_mutdict(Dict), | |
| 810 | count_var_occurrences_dict(Dict, Clauses), !, | |
| 811 | mutdict_items(Dict, DictItems), !. | |
| 812 | ||
| 813 | count_var_occurrences_dict(_, []). | |
| 814 | count_var_occurrences_dict(Dict, [Clause|T]) :- | |
| 815 | count_var_occurrences_from_clause_dict(Dict, Clause), | |
| 816 | count_var_occurrences_dict(Dict, T). | |
| 817 | ||
| 818 | count_var_occurrences_from_clause_dict(_, []). | |
| 819 | count_var_occurrences_from_clause_dict(Dict, [_-_-Pol-SatVarName|T]) :- | |
| 820 | var(Pol), % skip variables that are already propagated by deterministic unit propagation | |
| 821 | !, | |
| 822 | ( mutdict_get(Dict, SatVarName, Score) | |
| 823 | -> Score1 is Score + 1, | |
| 824 | mutdict_update(Dict, SatVarName, _, Score1) | |
| 825 | ; mutdict_put(Dict, SatVarName, 1) | |
| 826 | ), | |
| 827 | count_var_occurrences_from_clause_dict(Dict, T). | |
| 828 | count_var_occurrences_from_clause_dict(Dict, [_|T]) :- | |
| 829 | count_var_occurrences_from_clause_dict(Dict, T). | |
| 830 | ||
| 831 | update_heuristic_scores_for_vars(UsedVars, AC) :- | |
| 832 | decision_heuristic(Type), | |
| 833 | update_heuristic_scores(AC, Type, UsedVars). | |
| 834 | ||
| 835 | %% update_heuristic_scores(+AmountOfConflitsAtLevel, +Type, +SatVarNames). | |
| 836 | % Type is either vsids, evsids, vmtf or acids. | |
| 837 | % SatVarNames are the variable names occurring in learned clauses. | |
| 838 | update_heuristic_scores(_, _, []). | |
| 839 | update_heuristic_scores(TotalConflicts, Type, [SatVarName|T]) :- | |
| 840 | ( fibonacci_heap:get_priority_of_silent_fail(SatVarName, OldScore) | |
| 841 | -> bump_heuristic_score_for_type(Type, TotalConflicts, OldScore, NewScore), | |
| 842 | fibonacci_heap:update(SatVarName, NewScore), | |
| 843 | update_heuristic_scores(TotalConflicts, Type, T) | |
| 844 | ; % SAT variable has already been propagated. | |
| 845 | % For instance, this is the case when learning a clause on a level greater zero while | |
| 846 | % a specific SAT variable of this clause has already been propagated on a previous level. | |
| 847 | update_heuristic_scores(TotalConflicts, Type, T) | |
| 848 | ). | |
| 849 | ||
| 850 | % v_s + 1 | |
| 851 | bump_heuristic_score_for_type(vsids, _, OldScore, NewScore) :- | |
| 852 | NewScore is OldScore + 1. | |
| 853 | % k | |
| 854 | bump_heuristic_score_for_type(vmtf, TotalConflicts, _, NewScore) :- | |
| 855 | NewScore is TotalConflicts. | |
| 856 | % (v_s + k) / 2 | |
| 857 | bump_heuristic_score_for_type(acids, TotalConflicts, OldScore, NewScore) :- | |
| 858 | NewScore is (OldScore + TotalConflicts) / 2. | |
| 859 | % v_s + f^(-k), where f is evsids_f_value/1 and it is/was the k-th conflict when finding this clause via conflict analysis | |
| 860 | bump_heuristic_score_for_type(evsids, TotalConflicts, OldScore, NewScore) :- | |
| 861 | evsids_f_value(FVal), | |
| 862 | catch(NewScore is OldScore + FVal**(-TotalConflicts), error(evaluation_error(float_overflow),_), NewScore = 1.35743634973696E+308). | |
| 863 | ||
| 864 | % Literal Block Distance (LBD) as defined in "Predicting Learnt Clauses Quality in Modern SAT Solvers", | |
| 865 | % i.e., the amount of different decision levels in a clause. | |
| 866 | compute_lbd_score(BjClause, LbdScore) :- | |
| 867 | compute_lbd_score(BjClause, [], LbdScore). | |
| 868 | ||
| 869 | compute_lbd_score([], Acc, LbdScore) :- | |
| 870 | length(Acc, LbdScore). | |
| 871 | compute_lbd_score([(_,(Level,_),_,_)-_-_-_|T], Acc, LbdScore) :- | |
| 872 | !, | |
| 873 | ord_add_element(Acc, Level, NewAcc), | |
| 874 | compute_lbd_score(T, NewAcc, LbdScore). | |
| 875 | ||
| 876 | %% count_found_conflict(-NewTotal, -NewSinceRestart, -NewSinceReduction). | |
| 877 | count_found_conflict(Total1, SRes1, SRed1) :- | |
| 878 | log_conflict, | |
| 879 | retract(conflict_stats(total(Total), since_restart(SRes), since_reduction(SRed))), | |
| 880 | Total1 is Total + 1, | |
| 881 | SRes1 is SRes + 1, | |
| 882 | SRed1 is SRed + 1, | |
| 883 | asserta(conflict_stats(total(Total1), since_restart(SRes1), since_reduction(SRed1))). | |
| 884 | ||
| 885 | %% compute_and_assert_backjump_clause(+SolverEnv, +StateMutable, +StackSize, +ConflictClause). | |
| 886 | compute_and_assert_backjump_clause(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause) :- | |
| 887 | compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, _). | |
| 888 | ||
| 889 | cnf_to_smt(BoolPred, Smt) :- | |
| 890 | BoolPred = b(Expr,_,_), | |
| 891 | cnf_to_smt_e(Expr, Smt). | |
| 892 | ||
| 893 | cnf_to_smt_e(falsity, b(falsity,pred,[])). | |
| 894 | cnf_to_smt_e(truth, b(truth,pred,[])). | |
| 895 | cnf_to_smt_e(conjunct(A,B), Smt) :- | |
| 896 | cnf_to_smt(A, NA), | |
| 897 | cnf_to_smt(B, NB), | |
| 898 | safe_create_texpr(conjunct(NA,NB), pred, [], Smt). | |
| 899 | cnf_to_smt_e(disjunct(A,B), Smt) :- | |
| 900 | cnf_to_smt(A, NA), | |
| 901 | cnf_to_smt(B, NB), | |
| 902 | safe_create_texpr(disjunct(NA,NB), pred, [], Smt). | |
| 903 | cnf_to_smt_e(equal(b(identifier(_),_,Info),b(BoolExpr,boolean,_)), Smt) :- | |
| 904 | member(smt_formula(TSmt), Info), | |
| 905 | ( BoolExpr == boolean_true | |
| 906 | -> Smt = TSmt | |
| 907 | ; safe_create_texpr(negation(TSmt), pred, [], Smt) | |
| 908 | ). | |
| 909 | ||
| 910 | /*cnf_to_smt([], _, Acc, SmtFromCnf) :- | |
| 911 | conjunct_predicates(Acc, SmtFromCnf). | |
| 912 | cnf_to_smt([Clause|T], PrologSatVarTriple, Acc, SmtFromCnf) :- | |
| 913 | clause_to_smt(PrologSatVarTriple, Clause, SmtClause), | |
| 914 | cnf_to_smt(T, PrologSatVarTriple, [SmtClause|Acc], SmtFromCnf).*/ | |
| 915 | ||
| 916 | %clause_to_smt(PlVars, Clause, SmtFormula) :- | |
| 917 | % clause_to_smt(PlVars, Clause, [], SmtFormula). | |
| 918 | % | |
| 919 | %clause_to_smt(_, [], Acc, SmtFormula) :- | |
| 920 | % disjunct_predicates(Acc, SmtFormula). | |
| 921 | %clause_to_smt(PlVars, [_-Pol-_-SatVarName|T], Acc, SmtClause) :- | |
| 922 | % mutdict_get(PlVars, SatVarName, _-SatVarName-TSmtFormula-_), | |
| 923 | % !, | |
| 924 | % get_smt_formula_for_sat_pol(TSmtFormula, Pol, SmtFormula), | |
| 925 | % clause_to_smt(PlVars, T, [SmtFormula|Acc], SmtClause). | |
| 926 | %clause_to_smt(_, [_-_-SatVarName|_], _, _) :- | |
| 927 | % add_error_fail(clause_to_smt, 'Unknown SAT variable.', [SatVarName]). | |
| 928 | ||
| 929 | bump_glue_levels([]). | |
| 930 | bump_glue_levels([_-_-_-SatVarName|T]) :- | |
| 931 | ( retract(glue_level(SatVarName, GlueLevel,AlreadyBumped)) | |
| 932 | -> NGlueLevel is GlueLevel + 1 | |
| 933 | ; NGlueLevel = 1, | |
| 934 | AlreadyBumped = false | |
| 935 | ), | |
| 936 | asserta(glue_level(SatVarName,NGlueLevel,AlreadyBumped)), | |
| 937 | bump_glue_levels(T). | |
| 938 | ||
| 939 | %% compute_and_assert_backjump_clause_get_level(+SolverEnv, +StateMutable, +StackSize, +ConflictLevel, +ConflictClause, -BjLevel). | |
| 940 | compute_and_assert_backjump_clause_get_level(SolverEnv, StateMutable, StackSize, ConflictLevel, ConflictClause, BjLevel) :- | |
| 941 | get_last_decision_level(StateMutable, _), | |
| 942 | %possibly_discard_learned_clauses, % TODO: adapt to new bj clause handling; yet, forgetting clauses has not shown to be beneficial so far | |
| 943 | debug_format_sat("~nConflict clause is ~w", [strip-ConflictClause]), | |
| 944 | debug_format_sat("~nStart CDCL..", []), | |
| 945 | ( ( | |
| 946 | get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, BjSatVars, UsedVars), | |
| 947 | BjLevel \== -1 | |
| 948 | ) | |
| 949 | ; add_error_fail(compute_and_assert_backjump_clause_get_level, 'SMT solver\'s conflict resolution failed', []) | |
| 950 | ), | |
| 951 | debug_format_sat("done.", []), | |
| 952 | debug_format_sat("Backjump clause is ~w", [strip-BjClause]), | |
| 953 | debug_format_sat("Backjump level is ~w", [BjLevel]), | |
| 954 | compute_lbd_score(BjClause, LbdScore), | |
| 955 | debug_format_sat("LBD Score is ~w", [LbdScore]), | |
| 956 | ( ( glue_bumping(true), | |
| 957 | LbdScore == 2 | |
| 958 | ) | |
| 959 | -> retract(glue_clauses(Old)), | |
| 960 | New is Old + 1, | |
| 961 | asserta(glue_clauses(New)), | |
| 962 | bump_glue_levels(BjClause) | |
| 963 | ; true | |
| 964 | ), | |
| 965 | count_found_conflict(NewTotal, NewSinceRestart, _), | |
| 966 | asserta(backjump_clause(BjLevel, BjClause, LbdScore, BjSatVars, UsedVars, NewTotal)), | |
| 967 | asserta(backjump_level(BjLevel)), | |
| 968 | store_recent_stack_size(StackSize), | |
| 969 | count_learned_clause, | |
| 970 | possibly_decay_heuristic_values, | |
| 971 | ( \+ clear_lbd_values_or_fail(StateMutable), | |
| 972 | BjLevel \== 0 | |
| 973 | -> store_recent_lbd_score(LbdScore), | |
| 974 | update_total_lbd_sum(LbdScore), | |
| 975 | (random_restart(NewTotal, NewSinceRestart), !; true) | |
| 976 | ; true | |
| 977 | ), !. | |
| 978 | ||
| 979 | count_learned_clause :- | |
| 980 | retract(amount_learned_clauses(Old)), | |
| 981 | New is Old + 1, | |
| 982 | asserta(amount_learned_clauses(New)). | |
| 983 | ||
| 984 | %% store_recent_lbd_score(+LbdScore). | |
| 985 | % The stored list of recent LBDs is a difference list and we insert at the end of the list. | |
| 986 | % The first LBD is thus the oldest one and removed when exceeding the maximum size | |
| 987 | % defined by recent_lbd_threshold/1. | |
| 988 | store_recent_lbd_score(LbdScore) :- | |
| 989 | retract(recent_lbds_dl(Lbds-Diff, Amount)), | |
| 990 | glucose_restart_recent_lbds_threshold(Thresh), | |
| 991 | Diff = [LbdScore|NDiff], | |
| 992 | ( Amount < Thresh | |
| 993 | -> Amount1 is Amount + 1, | |
| 994 | asserta(recent_lbds_dl(Lbds-NDiff, Amount1)) | |
| 995 | ; Lbds = [_|RLbds], | |
| 996 | asserta(recent_lbds_dl(RLbds-NDiff, Amount)) | |
| 997 | ). | |
| 998 | ||
| 999 | store_recent_stack_size(StackSize) :- | |
| 1000 | retract(recent_stack_sizes_dl(StackSizes-Diff, Amount)), | |
| 1001 | glucose_restart_trail_threshold(Thresh), | |
| 1002 | Diff = [StackSize|NDiff], | |
| 1003 | ( Amount < Thresh | |
| 1004 | -> Amount1 is Amount + 1, | |
| 1005 | asserta(recent_stack_sizes_dl(StackSizes-NDiff, Amount1)) | |
| 1006 | ; StackSizes = [_|RStackSizes], | |
| 1007 | asserta(recent_stack_sizes_dl(RStackSizes-NDiff, Amount)) | |
| 1008 | ). | |
| 1009 | ||
| 1010 | %% update_total_lbd_sum(+LbdScore). | |
| 1011 | update_total_lbd_sum(LbdScore) :- | |
| 1012 | retract(total_lbd_sum(Old)), | |
| 1013 | New is Old + LbdScore, | |
| 1014 | asserta(total_lbd_sum(New)). | |
| 1015 | ||
| 1016 | %% random_restart(+AmountOfConflicts, +AmountOfConflictsSinceRestart). | |
| 1017 | % "Randomly" restart after an amount of conflicts since the last restart. | |
| 1018 | random_restart(_AC, ACR) :- | |
| 1019 | restart_policy(luby), | |
| 1020 | random_luby_restart(ACR), !. | |
| 1021 | random_restart(AC, _ACR) :- | |
| 1022 | restart_policy(glucose), | |
| 1023 | random_glucose_restart(AC), !. | |
| 1024 | ||
| 1025 | do_random_restart :- | |
| 1026 | log_restart, | |
| 1027 | retract(restarts(OldR)), | |
| 1028 | NewR is OldR + 1, | |
| 1029 | asserta(restarts(NewR)), | |
| 1030 | retract(backjump_level(_)), | |
| 1031 | asserta(backjump_level(0)), | |
| 1032 | retract(conflict_stats(total(Total), _, since_reduction(SRed))), | |
| 1033 | asserta(conflict_stats(total(Total), since_restart(0), since_reduction(SRed))), | |
| 1034 | asserta_once(is_restart), | |
| 1035 | debug_format_sat("~nRandom restart", []). | |
| 1036 | ||
| 1037 | %% random_glucose_restart(+AmountOfConflicts). | |
| 1038 | % Restart search if recent_lbds_dl/2 contains exactly glucose_restart_recent_lbds_threshold/1 amount | |
| 1039 | % of most recent LBDs and RecentAvg * Proportion > TotalAvg is satisfied, i.e., the recently learned clauses' | |
| 1040 | % LBDs got too large. | |
| 1041 | random_glucose_restart(AC) :- | |
| 1042 | total_lbd_sum(TotalLbdSum), | |
| 1043 | TotalAvg is TotalLbdSum / AC, | |
| 1044 | recent_lbds_dl(RLbds-[], LbdAmount), | |
| 1045 | glucose_restart_recent_lbds_threshold(LbdThresh), | |
| 1046 | LbdAmount == LbdThresh, % queue of recent LBDs is full | |
| 1047 | sumlist(RLbds, RSum), | |
| 1048 | RecentAvg is RSum / LbdAmount, | |
| 1049 | glucose_restart_margin_ratio(Proportion), | |
| 1050 | debug_format_sat("~nTotalAvg: ~w~nRecentAvg: ~w", [TotalAvg,RecentAvg]), | |
| 1051 | ( RecentAvg * Proportion > TotalAvg | |
| 1052 | -> do_random_restart, | |
| 1053 | clear_recent_lbds_state | |
| 1054 | ; true | |
| 1055 | ). | |
| 1056 | ||
| 1057 | % Favor SAT instances too by possibly clearing the recent LBD queue. | |
| 1058 | % Assumption: The queue of recent LBDs is full. | |
| 1059 | clear_lbd_values_or_fail(StateMutable) :- | |
| 1060 | glucose_restart_trail_threshold(TrailThresh), | |
| 1061 | glucose_restart_stack_avg_factor(StackSizeFactor), | |
| 1062 | recent_stack_sizes_dl(StackSizes-[], AmountStackSizes), | |
| 1063 | AmountStackSizes == TrailThresh, % queue of recent stack sizes on conflict is full | |
| 1064 | get_full_state(StateMutable, current_stack_size, StackSize), | |
| 1065 | sumlist(StackSizes, SSum), | |
| 1066 | StackSizesAvg is SSum / AmountStackSizes, | |
| 1067 | StackSize > StackSizeFactor * StackSizesAvg, | |
| 1068 | clear_recent_lbds_state. | |
| 1069 | ||
| 1070 | clear_recent_lbds_state :- | |
| 1071 | retract(recent_lbds_dl(_, _)), | |
| 1072 | asserta(recent_lbds_dl(Diff-Diff, 0)). | |
| 1073 | ||
| 1074 | %% random_luby_restart(+AmountOfConflictsSinceRestart). | |
| 1075 | % The amount of conflicts when to restart is defined by the Luby sequence, | |
| 1076 | % i.e., 1,1,2,1,1,2,4,1,1,2,1,1,2,4,8,.. etc., (cf. "Optimal speedup of Las Vegas algorithms") | |
| 1077 | % using a unit length of 32 (see luby_counter/1). | |
| 1078 | random_luby_restart(ACR) :- | |
| 1079 | restart_policy(luby), | |
| 1080 | get_next_luby_value(Luby), | |
| 1081 | !, | |
| 1082 | ( ACR == Luby | |
| 1083 | -> retract_once(luby_counter(_)), | |
| 1084 | do_random_restart | |
| 1085 | ; true | |
| 1086 | ). | |
| 1087 | random_luby_restart(_) :- | |
| 1088 | add_error_fail(random_restart, 'No more values in predefined Luby sequence', []). | |
| 1089 | ||
| 1090 | get_next_luby_value(LubyValue) :- | |
| 1091 | luby_counter(Luby), | |
| 1092 | luby_restart_unit_length(UnitLength), | |
| 1093 | LubyValue is UnitLength * Luby, | |
| 1094 | !. | |
| 1095 | ||
| 1096 | %% get_sat_solution_exclusion_clauses(+PlVars, -ExclClausesNoRef). | |
| 1097 | % We exclude SAT solutions when backtracking from finding an SMT solution to find a different assignment. | |
| 1098 | /*get_sat_solution_exclusion_clauses(PlVars, ExclClausesNoRef) :- | |
| 1099 | findall(ExclClause, | |
| 1100 | (exclude_sat_solution_clause(TExclClause), set_variable_references_in_clause(PlVars, TExclClause, ExclClause)), | |
| 1101 | ExclClausesNoRef), !.*/ | |
| 1102 | ||
| 1103 | %% set_variable_references_in_clauses(+PlVars, +Clauses, -RefClauses). | |
| 1104 | set_variable_references_in_clauses(_, [], []). | |
| 1105 | set_variable_references_in_clauses(PlVars, [Clause|T], [RefClause|NT]) :- | |
| 1106 | set_variable_references_in_clause(PlVars, Clause, RefClause), | |
| 1107 | set_variable_references_in_clauses(PlVars, T, NT). | |
| 1108 | ||
| 1109 | %% set_variable_references_in_clause(+PlVars, +Clause, -RefClauses). | |
| 1110 | % We need to set the correct variable references in a new learned clause | |
| 1111 | % to trigger co-routines etc. | |
| 1112 | set_variable_references_in_clause(_, [], Out) :- !, Out = []. | |
| 1113 | set_variable_references_in_clause(PlVars, [_-Pol-_-Name|T], [StackInfo-Pol-Var-Name|NT]) :- | |
| 1114 | mutdict_get(PlVars, Name, TVar-Name-_-TStackInfo), | |
| 1115 | !, | |
| 1116 | Var = TVar, | |
| 1117 | StackInfo = TStackInfo, | |
| 1118 | set_variable_references_in_clause(PlVars, T, NT). | |
| 1119 | set_variable_references_in_clause(_, [_-_-_-Name|_], _) :- | |
| 1120 | add_error_fail(set_variable_references_in_clause, 'Cannot set references: unknown SAT variable.', [Name]). | |
| 1121 | ||
| 1122 | get_from_solver_env(SolverEnv, Key, OutValue) :- | |
| 1123 | get_from_solver_env_ordered(Key, SolverEnv, Value), | |
| 1124 | !, | |
| 1125 | OutValue = Value. | |
| 1126 | get_from_solver_env(SolverEnv, Key, _) :- | |
| 1127 | add_error_fail(get_from_solver_env, | |
| 1128 | 'Wrong key or corrupt solver environment in CDCL(T) SAT solver', | |
| 1129 | [solver_env:SolverEnv,key:Key]). | |
| 1130 | ||
| 1131 | get_from_solver_env_ordered(sat_vars, [sat_vars:SatVars,_,_,_,_,_], SatVars). | |
| 1132 | get_from_solver_env_ordered(sat_varnames, [_,sat_varnames:SatVarNames,_,_,_,_], SatVarNames). | |
| 1133 | get_from_solver_env_ordered(sat_bindings, [_,_,sat_bindings:SatBindings,_,_,_], SatBindings). | |
| 1134 | get_from_solver_env_ordered(t2b_env, [_,_,_,t2b_env:Env,_,_], Env). | |
| 1135 | get_from_solver_env_ordered(pl_vars, [_,_,_,_,pl_vars:PlVars,_], PlVars). | |
| 1136 | get_from_solver_env_ordered(binary_clause_vars, [_,_,_,_,_,binary_clause_vars:VarsFromBinaryClauses], VarsFromBinaryClauses). | |
| 1137 | ||
| 1138 | bt_asserta(Assertion) :- | |
| 1139 | asserta(Assertion); (retract(Assertion), !, fail). | |
| 1140 | ||
| 1141 | bt_retract(Assertion) :- | |
| 1142 | ( retract(Assertion) | |
| 1143 | -> ( true | |
| 1144 | ; asserta(Assertion), | |
| 1145 | !, | |
| 1146 | fail | |
| 1147 | ) | |
| 1148 | ; fail | |
| 1149 | ). | |
| 1150 | ||
| 1151 | %% get_unsat_core_from_smt_formula(+FullFormula, +LastVarName, -UnsatCore). | |
| 1152 | % Assumption: unsat core computation only removes constraints and does not deduce new ones. | |
| 1153 | % Fails if +FullFormula is satisfiable. | |
| 1154 | get_unsat_core_from_smt_formula(FullFormula, LastVarName, UnsatCore) :- | |
| 1155 | debug_format_sat("Compute unsat core for: ", [], FullFormula), | |
| 1156 | preferences:temporary_set_preference(time_out, 25, Change), | |
| 1157 | call_cleanup(time_out(unsat_chr_core_list_with_auto_time_limit(FullFormula, 30000, | |
| 1158 | [auto_time_out_factor(180), % we add 80 % | |
| 1159 | ignore_if_sol_found, | |
| 1160 | inspect_quantifiers(false)], GlobalRes, CoreList), 30000, TimeoutResult), | |
| 1161 | reset_temporary_preference(time_out, Change)), | |
| 1162 | !, | |
| 1163 | ( GlobalRes = solution(_) | |
| 1164 | -> % the present theory conflict only occurs within the current state of ProB's waitflag store; there is at least one choice point | |
| 1165 | % in the theory solver which needs to be evaluated; we thus do not learn from this "spurious counterexample" but | |
| 1166 | % trigger chronological backtracking instead of backjumping | |
| 1167 | debug_format_sat("Spurious counterexample found. Skip backjumping and use chronological backtracking instead.", []), | |
| 1168 | fail | |
| 1169 | ; GlobalRes == time_out | |
| 1170 | -> % ignore core if global result is timeout | |
| 1171 | TUnsatCore = FullFormula | |
| 1172 | ; TimeoutResult == time_out | |
| 1173 | -> % don't waste too much time in unsat core computation | |
| 1174 | debug_format_sat("Canceled unsat core computation due to exceeding a timeout" ,[]), | |
| 1175 | TUnsatCore = FullFormula | |
| 1176 | ; ( CoreList == [] | |
| 1177 | -> add_error_fail(get_conflict_clause_for_theory_conflict, 'Conflict clause in SMT solving is not a conflict.', [LastVarName]) | |
| 1178 | ; conjunct_predicates(CoreList, TUnsatCore) | |
| 1179 | ) | |
| 1180 | ), | |
| 1181 | debug_format_sat("Computed unsat core with added WD POs: ", [], TUnsatCore), | |
| 1182 | ( strip_pos_keep_toplevel_conj(TUnsatCore, UnsatCore) | |
| 1183 | -> true | |
| 1184 | ; add_error_fail(strip_pos_keep_toplevel_conj, 'Removing WD POs for CDCL(T) failed.', [unsat_core_with_wd:TUnsatCore]) | |
| 1185 | ), | |
| 1186 | debug_format_sat("Computed unsat core: ", [], UnsatCore). | |
| 1187 | ||
| 1188 | %% get_conflict_clause_for_theory_conflict(+LastVarName, +LastVarValue, +SolverEnv, -ConflictClause). | |
| 1189 | % Translate current sat solution, which is a theory conflict, to the theory and compute | |
| 1190 | % the (minimum) unsat core. Return the negated theory conflict as a conflict clause. | |
| 1191 | % Note that an SMT formula passed to the theory solver is always a conjunction and | |
| 1192 | % thus the negated unsat core is a disjunction (clause). | |
| 1193 | get_conflict_clause_for_theory_conflict(SolverEnv, LastVarName, LastVarValue, SolverEnv, ConflictClause) :- | |
| 1194 | ( retract(idl_unsat_core(UnsatCore)) | |
| 1195 | -> true | |
| 1196 | ; get_from_solver_env(SolverEnv, sat_bindings, SatBindingsNoLast), | |
| 1197 | get_from_solver_env(SolverEnv, sat_vars, SatVars), | |
| 1198 | sat_to_predicate_from_solution(SatBindingsNoLast, SatVars, SmtFormulaNoLast), | |
| 1199 | findall(bind(PendingName,PendingPol), pending_theory_prop(PendingName,PendingPol), PendingTheoryProps), | |
| 1200 | sat_to_predicate_from_solution([bind(LastVarName,LastVarValue)|PendingTheoryProps], SatVars, FixedConj), | |
| 1201 | safe_create_texpr(conjunct(FixedConj,SmtFormulaNoLast), pred, [] , FullFormula), | |
| 1202 | get_unsat_core_from_smt_formula(FullFormula, LastVarName, UnsatCore) | |
| 1203 | ), !, | |
| 1204 | find_typed_identifier_uses(UnsatCore, [], UsedIds), | |
| 1205 | ( list_contains_unfixed_deferred_set_id(UsedIds) | |
| 1206 | -> asserta(unfixed_deferred_set_error) | |
| 1207 | ; true | |
| 1208 | ), | |
| 1209 | get_conflict_clause_from_unsat_core(UnsatCore, SolverEnv, TConflictClause), | |
| 1210 | sort(TConflictClause, TTConflictClause), % there can be duplicates due to added top-level WD POs; important to remove | |
| 1211 | ( TTConflictClause = [_] | |
| 1212 | -> % currently undiscovered static theory contradiction; SAT variable might not be propagated yet if added WD PO | |
| 1213 | ConflictClause = TTConflictClause | |
| 1214 | ; % remove not propagated top-level WD POs; we enforce WD POs in the theory solver but it can | |
| 1215 | % be the case that a theory conflict occurs before the WD POs are propagated in the SAT solver | |
| 1216 | remove_not_propagated(TTConflictClause, LastVarName, ConflictClause) | |
| 1217 | ), | |
| 1218 | !. | |
| 1219 | ||
| 1220 | remove_not_propagated([], _, []). | |
| 1221 | remove_not_propagated([Pol-Var-Name|T], LastVarName, [Pol-Var-Name|NT]) :- | |
| 1222 | ( ground(Var) | |
| 1223 | ; Name == LastVarName | |
| 1224 | ), | |
| 1225 | !, | |
| 1226 | remove_not_propagated(T, LastVarName, NT). | |
| 1227 | remove_not_propagated([_-_-Name|T], LastVarName, NT) :- | |
| 1228 | debug_format_sat("Remove not propagated SAT variable ~w from conflict clause.", [Name]), | |
| 1229 | remove_not_propagated(T, LastVarName, NT). | |
| 1230 | ||
| 1231 | %% get_conflict_clause_from_unsat_core(+UnsatCore, +SolverEnv, -ConflictClause). | |
| 1232 | get_conflict_clause_from_unsat_core(UnsatCore, SolverEnv, ConflictClause) :- | |
| 1233 | get_from_solver_env(SolverEnv, sat_vars, SatVars), | |
| 1234 | get_from_solver_env(SolverEnv, t2b_env, T2BEnv), | |
| 1235 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
| 1236 | predicate_to_sat(only_reuse, [], SatVars, T2BEnv, UnsatCore, _NewEnv, _, UnsatCoreSat, _NewSatVars), | |
| 1237 | sat_conj_negate_to_clause(UnsatCoreSat, TConflictClause), | |
| 1238 | set_variable_references_in_clause(PlVars, TConflictClause, ConflictClause), | |
| 1239 | !. | |
| 1240 | get_conflict_clause_from_unsat_core(_, _, _) :- | |
| 1241 | add_error_fail(get_conflict_clause_from_unsat_core, 'Unsat core to conflict clause failed.', []). | |
| 1242 | ||
| 1243 | :- public get_complete_theory_lemma/2. % not used at the moment, for Spider | |
| 1244 | %% get_complete_theory_lemma(+SolverEnv, -TheoryLemmaClause) :- | |
| 1245 | % Return the complete unsatisfiable SMT formula as a conflict clause. | |
| 1246 | get_complete_theory_lemma(SolverEnv, TheoryLemmaClause) :- | |
| 1247 | get_complete_theory_lemma_fixed_binding(SolverEnv, _, _, TheoryLemmaClause). | |
| 1248 | ||
| 1249 | %% get_complete_theory_lemma_fixed_binding(+SolverEnv, +SatVarName, +SatVarPol, -TheoryLemmaClause). | |
| 1250 | % Enforce +SatVarName to have +SatVarPol binding. This is important for theory conflicts since the last | |
| 1251 | % binding has been undone when backtracking. This is not applied if both inputs are variables, e.g., for SAT conflicts. | |
| 1252 | get_complete_theory_lemma_fixed_binding(SolverEnv, SatVarName, SatVarPol, TheoryLemmaClause) :- | |
| 1253 | get_from_solver_env(SolverEnv, pl_vars, PlVars), | |
| 1254 | get_from_solver_env(SolverEnv, sat_bindings, SatBindings), | |
| 1255 | get_clause_from_negated_ground_bindings(SatBindings, SatVarName, SatVarPol, TTheoryLemmaClause), | |
| 1256 | set_variable_references_in_clause(PlVars, TTheoryLemmaClause, TheoryLemmaClause), !. | |
| 1257 | ||
| 1258 | %% get_clause_from_negated_ground_bindings(+SatBindings, +FSatVarName, +FSatVarPol, -TheoryLemmaClause) :- | |
| 1259 | % FSatVarName: name of SAT variable whose binding should be set to +FSatVarPol | |
| 1260 | get_clause_from_negated_ground_bindings(SatBindings, FSatVarName, FSatVarPol, TheoryLemmaClause) :- | |
| 1261 | get_clause_from_negated_ground_bindings(SatBindings, FSatVarName, FSatVarPol, [], TheoryLemmaClause). | |
| 1262 | ||
| 1263 | get_clause_from_negated_ground_bindings([], _, _, Acc, Acc). | |
| 1264 | get_clause_from_negated_ground_bindings([bind(SatVarName,_)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
| 1265 | % theory propagations during grounding are possibly undone in the stack if finding a contradiction during grounding waitflags | |
| 1266 | % we restore such pending theory propagations here | |
| 1267 | pending_theory_prop(SatVarName, SatVarPol), | |
| 1268 | !, | |
| 1269 | negate_polarity(SatVarPol, NegPol), | |
| 1270 | get_clause_from_negated_ground_bindings(T, FSatVarName, FSatVarPol, [_-NegPol-_-SatVarName|Acc], TheoryLemmaClause). | |
| 1271 | get_clause_from_negated_ground_bindings([bind(SatVarName,_)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
| 1272 | % set fixed polarity | |
| 1273 | SatVarName == FSatVarName, | |
| 1274 | !, | |
| 1275 | negate_polarity(FSatVarPol, NegPol), | |
| 1276 | get_clause_from_negated_ground_bindings(T, FSatVarName, FSatVarPol, [_-NegPol-_-SatVarName|Acc], TheoryLemmaClause). | |
| 1277 | get_clause_from_negated_ground_bindings([bind(SatVarName,Pol)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
| 1278 | ground(Pol), | |
| 1279 | !, | |
| 1280 | negate_polarity(Pol, NegPol), | |
| 1281 | get_clause_from_negated_ground_bindings(T, FSatVarName, FSatVarPol, [_-NegPol-_-SatVarName|Acc], TheoryLemmaClause). | |
| 1282 | get_clause_from_negated_ground_bindings([_|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
| 1283 | get_clause_from_negated_ground_bindings(T, FSatVarName, FSatVarPol, Acc, TheoryLemmaClause). | |
| 1284 | ||
| 1285 | get_clause_from_ground_bindings([], _, _, Acc, Acc). | |
| 1286 | get_clause_from_ground_bindings([bind(SatVarName,_)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
| 1287 | % theory propagations during grounding are possibly undone in the stack if finding a contradiction during grounding waitflags | |
| 1288 | % we restore such pending theory propagations here | |
| 1289 | pending_theory_prop(SatVarName, SatVarPol), | |
| 1290 | !, | |
| 1291 | get_clause_from_ground_bindings(T, FSatVarName, FSatVarPol, [_-SatVarPol-_-SatVarName|Acc], TheoryLemmaClause). | |
| 1292 | get_clause_from_ground_bindings([bind(SatVarName,Pol)|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
| 1293 | ground(Pol), | |
| 1294 | !, | |
| 1295 | get_clause_from_ground_bindings(T, FSatVarName, FSatVarPol, [_-Pol-_-SatVarName|Acc], TheoryLemmaClause). | |
| 1296 | get_clause_from_ground_bindings([_|T], FSatVarName, FSatVarPol, Acc, TheoryLemmaClause) :- | |
| 1297 | get_clause_from_ground_bindings(T, FSatVarName, FSatVarPol, Acc, TheoryLemmaClause). | |
| 1298 | ||
| 1299 | % Fail if no decision has been made so far, i.e., the decision level is set to -1. | |
| 1300 | get_last_decision_level(StateMutable, Level) :- | |
| 1301 | get_full_state(StateMutable, cur_level, TLevel), | |
| 1302 | TLevel > 0, | |
| 1303 | !, | |
| 1304 | Level = TLevel. | |
| 1305 | ||
| 1306 | %negate_polarities([], []). | |
| 1307 | %negate_polarities([StackInfo-Pol-Var-Name|T], [StackInfo-NPol-Var-Name|NT]) :- | |
| 1308 | % negate_polarity(Pol, NPol), | |
| 1309 | % negate_polarities(T, NT). | |
| 1310 | ||
| 1311 | get_maximum_decision_level([(_,(Level,_),_,_)-_-_-_|T], ConflictLevel) :- | |
| 1312 | !, | |
| 1313 | get_maximum_decision_level(T, Level, ConflictLevel). | |
| 1314 | get_maximum_decision_level([_-_-_-Name|_], _) :- | |
| 1315 | add_error_fail(get_maximum_decision_level, 'The SAT variable has not been decided yet', [Name]). | |
| 1316 | ||
| 1317 | get_maximum_decision_level([], Acc, Acc). | |
| 1318 | get_maximum_decision_level([(_,(Level,_),_,_)-_-_-_|T], Acc, ConflictLevel) :- | |
| 1319 | !, | |
| 1320 | ( Level > Acc | |
| 1321 | -> NAcc = Level | |
| 1322 | ; NAcc = Acc | |
| 1323 | ), | |
| 1324 | get_maximum_decision_level(T, NAcc, ConflictLevel). | |
| 1325 | get_maximum_decision_level([_-_-_-Name|_], _, _) :- | |
| 1326 | add_error_fail(get_maximum_decision_level, 'The SAT variable has not been decided yet', [Name]). | |
| 1327 | ||
| 1328 | get_maximum_decision_level_other_than_current([_], _, _, BjLevel) :- | |
| 1329 | % zero if learning a unit clause | |
| 1330 | !, | |
| 1331 | BjLevel = 0. | |
| 1332 | get_maximum_decision_level_other_than_current(BjClause, BjLevelAcc, CurLevel, BjLevel) :- | |
| 1333 | get_maximum_decision_level_other_than_current_not_unit(BjClause, BjLevelAcc, CurLevel, BjLevel). | |
| 1334 | ||
| 1335 | get_maximum_decision_level_other_than_current_not_unit([], BjLevelAcc, _, BjLevelAcc). | |
| 1336 | get_maximum_decision_level_other_than_current_not_unit([(_,(Level,_),_,_)-_-_-_|T], BjLevelAcc, CurLevel, BjLevel) :- | |
| 1337 | ( (Level \== CurLevel, | |
| 1338 | Level > BjLevelAcc | |
| 1339 | ) | |
| 1340 | -> NBjLevelAcc = Level | |
| 1341 | ; NBjLevelAcc = BjLevelAcc | |
| 1342 | ), | |
| 1343 | get_maximum_decision_level_other_than_current_not_unit(T, NBjLevelAcc, CurLevel, BjLevel). | |
| 1344 | ||
| 1345 | %% get_antecedent_assignments(+SolverEnv, +ConflictDLevel, +SatVarName, +RPol, +RPropType, +ROriginalClause, -Antecedent). | |
| 1346 | get_antecedent_assignments(_, _, SatVarName, _, _, ROriginalClause, Antecedent) :- | |
| 1347 | is_list(ROriginalClause), | |
| 1348 | !, | |
| 1349 | select(_-_-_-SatVarName, ROriginalClause, TAntecedent), !, | |
| 1350 | Antecedent = TAntecedent. | |
| 1351 | get_antecedent_assignments(SolverEnv, ConflictDLevel, SatVarName, RPol, theory, ROriginalClause, Antecedent) :- | |
| 1352 | \+ is_list(ROriginalClause), | |
| 1353 | !, | |
| 1354 | explain_theory_propagation(SolverEnv, SatVarName, ConflictDLevel, RPol, OriginalClause), | |
| 1355 | ROriginalClause = OriginalClause, | |
| 1356 | select(_-_-_-SatVarName, OriginalClause, TAntecedent), !, | |
| 1357 | Antecedent = TAntecedent. | |
| 1358 | get_antecedent_assignments(_, _, SatVarName, _, _, _, _) :- | |
| 1359 | add_error_fail(get_antecedent_assignments, 'No antecedent assignments since variable has not been propagated.', SatVarName). | |
| 1360 | ||
| 1361 | %% join_assignments(+A1, +A2, +A2Full, -Joined). | |
| 1362 | join_assignments([], _, A, A). | |
| 1363 | join_assignments([StackInfo-Pol-Var-Name|T], A2, A3, Res) :- | |
| 1364 | ( select(_-_-_-Name, A2, A4) % removes dups assuming that A2 has no dups | |
| 1365 | -> join_assignments(T, A4, A3, Res) | |
| 1366 | ; join_assignments(T, A2, [StackInfo-Pol-Var-Name|A3], Res) | |
| 1367 | ). | |
| 1368 | ||
| 1369 | %% resolve(+SolverEnv, +TBjClause, +Resolver, +ROriginalClause, -NTBjClause). | |
| 1370 | % +Resolver is a SAT variable name to resolve next (i.e., expand its antecedent assignments). | |
| 1371 | resolve(SolverEnv, TBjClause, ConflictDLevel, Resolver, RPol, RPropType, ROriginalClause, NTBjClause) :- | |
| 1372 | get_antecedent_assignments(SolverEnv, ConflictDLevel, Resolver, RPol, RPropType, ROriginalClause, Antecedent), | |
| 1373 | join_assignments(Antecedent, TBjClause, TBjClause, TNTBjClause), % important to not have duplicates | |
| 1374 | select(_-_-_-Resolver, TNTBjClause, NTBjClause). | |
| 1375 | ||
| 1376 | add_used_vars_to_mutdict([], _). | |
| 1377 | add_used_vars_to_mutdict([_-_-_-SatVarName|T], VarNamesDict) :- | |
| 1378 | \+ mutdict_get(VarNamesDict, SatVarName, _), | |
| 1379 | !, | |
| 1380 | mutdict_put(VarNamesDict, SatVarName, SatVarName), | |
| 1381 | add_used_vars_to_mutdict(T, VarNamesDict). | |
| 1382 | add_used_vars_to_mutdict([_|T], VarNamesDict) :- | |
| 1383 | add_used_vars_to_mutdict(T, VarNamesDict). | |
| 1384 | ||
| 1385 | get_variables_used_in_cdcl(ResolvedSoFar, BjClause, UsedVars) :- | |
| 1386 | add_used_vars_to_mutdict(BjClause, ResolvedSoFar), | |
| 1387 | mutdict_keys(ResolvedSoFar, UsedVars). | |
| 1388 | ||
| 1389 | get_variable_names_in_clause([], []). | |
| 1390 | get_variable_names_in_clause([_-_-_-SatVarName|T], [SatVarName|NT]) :- | |
| 1391 | get_variable_names_in_clause(T, NT). | |
| 1392 | ||
| 1393 | % sort in reversed stack order | |
| 1394 | reversed_stack_sort((_,(DLevel1,ACount1),_,_)-_-_-_, (_,(DLevel2,ACount2),_,_)-_-_-_) :- | |
| 1395 | ground(DLevel1), ground(DLevel2), | |
| 1396 | ( DLevel1 > DLevel2 | |
| 1397 | -> true | |
| 1398 | ; DLevel1 == DLevel2 | |
| 1399 | -> ACount1 > ACount2 | |
| 1400 | ; fail | |
| 1401 | ). | |
| 1402 | ||
| 1403 | :- dynamic part_of_first_uip/1. | |
| 1404 | ||
| 1405 | % See https://cca.informatik.uni-freiburg.de/papers/SoerenssonBiere-SAT09.pdf | |
| 1406 | % Generate the 1-UIP clause. Mark all its literals. Remove those implied variables which have all their antecedent literals marked. | |
| 1407 | minimize_clause(SolverEnv, ConflictDLevel, BjClause, local, MinBjClause) :- | |
| 1408 | mark_literals(BjClause), | |
| 1409 | remove_where_all_antecedent_marked(BjClause, SolverEnv, ConflictDLevel, MinBjClause). | |
| 1410 | % Generate the 1-UIP clause. Mark its literals. Implied variables in 1-UIP clause are candidates for removal. | |
| 1411 | % Search implication graph. Start from antecedent literals of candidate. Stop at marked literals or decisions. | |
| 1412 | % If search always ends at marked literals, the candidate can be removed. | |
| 1413 | minimize_clause(SolverEnv, ConflictDLevel, BjClause, recursive, MinBjClause) :- | |
| 1414 | mark_literals(BjClause), | |
| 1415 | remove_recursively_stop_marked(BjClause, SolverEnv, ConflictDLevel, MinBjClause). | |
| 1416 | ||
| 1417 | remove_recursively_stop_marked([], _, _, []). | |
| 1418 | remove_recursively_stop_marked([(PropType,_,_,OriginalClause)-_-Pol-SatVarName|T], SolverEnv, ConflictDLevel, MinBjClause) :- | |
| 1419 | PropType \== branch, | |
| 1420 | get_antecedent_assignments(SolverEnv, ConflictDLevel, SatVarName, Pol, PropType, OriginalClause, Antecedent), | |
| 1421 | samsort(reversed_stack_sort, Antecedent, SAntecedent), % reverse assignment order | |
| 1422 | recursively_inspect_antecedent(SAntecedent, SolverEnv, ConflictDLevel), | |
| 1423 | !, | |
| 1424 | remove_recursively_stop_marked(T, SolverEnv, ConflictDLevel, MinBjClause). | |
| 1425 | remove_recursively_stop_marked([Lit|T], SolverEnv, ConflictDLevel, [Lit|NT]) :- | |
| 1426 | remove_recursively_stop_marked(T, SolverEnv, ConflictDLevel, NT). | |
| 1427 | ||
| 1428 | recursively_inspect_antecedent([], _, _). | |
| 1429 | recursively_inspect_antecedent([(PropType,_,_,OriginalClause)-_-Pol-SatVarName|T], SolverEnv, ConflictDLevel) :- | |
| 1430 | recursive_search_stops_at_marked_or_decision(PropType, OriginalClause, Pol, SatVarName, SolverEnv, ConflictDLevel), | |
| 1431 | recursively_inspect_antecedent(T, SolverEnv, ConflictDLevel). | |
| 1432 | ||
| 1433 | recursive_search_stops_at_marked_or_decision(_, _, _, SatVarName, _, _) :- | |
| 1434 | part_of_first_uip(SatVarName), | |
| 1435 | !. | |
| 1436 | recursive_search_stops_at_marked_or_decision(PropType, OriginalClause, Pol, SatVarName, SolverEnv, ConflictDLevel) :- | |
| 1437 | PropType \== branch, | |
| 1438 | get_antecedent_assignments(SolverEnv, ConflictDLevel, SatVarName, Pol, PropType, OriginalClause, Antecedent), | |
| 1439 | recursively_inspect_antecedent(Antecedent, SolverEnv, ConflictDLevel). | |
| 1440 | ||
| 1441 | all_literals_are_marked([]). | |
| 1442 | all_literals_are_marked([_-_-_-SatVarName|T]) :- | |
| 1443 | part_of_first_uip(SatVarName), | |
| 1444 | !, | |
| 1445 | all_literals_are_marked(T). | |
| 1446 | ||
| 1447 | remove_where_all_antecedent_marked([], _, _, []). | |
| 1448 | remove_where_all_antecedent_marked([(PropType,_,_,OriginalClause)-_-Pol-SatVarName|T], SolverEnv, ConflictDLevel, MinBjClause) :- | |
| 1449 | PropType == unit, | |
| 1450 | get_antecedent_assignments(SolverEnv, ConflictDLevel, SatVarName, Pol, PropType, OriginalClause, Antecedent), | |
| 1451 | all_literals_are_marked(Antecedent), | |
| 1452 | !, | |
| 1453 | remove_where_all_antecedent_marked(T, SolverEnv, ConflictDLevel, MinBjClause). | |
| 1454 | remove_where_all_antecedent_marked([Lit|T], SolverEnv, ConflictDLevel, [Lit|NT]) :- | |
| 1455 | remove_where_all_antecedent_marked(T, SolverEnv, ConflictDLevel, NT). | |
| 1456 | ||
| 1457 | mark_literals(Lits) :- | |
| 1458 | retractall(part_of_first_uip(_)), | |
| 1459 | mark_literals_state(Lits). | |
| 1460 | ||
| 1461 | mark_literals_state([]). | |
| 1462 | mark_literals_state([_-_-_-SatVarName|T]) :- | |
| 1463 | asserta(part_of_first_uip(SatVarName)), | |
| 1464 | mark_literals_state(T). | |
| 1465 | ||
| 1466 | %% get_backjump_clause_conflict_resolution(+SolverEnv, +StateMutable, +ConflictLevel, +ConflictClause, -BjClause, -BjLevel, -BjSatVars, -UsedVars). | |
| 1467 | % In the conflict graph each node corresponds to a variable assignment. | |
| 1468 | % The predecessors of node x are the antecedent assignments A^w(x) corresponding | |
| 1469 | % to the unit clause w (in its original form) that led to the propagation of x (logical implications). | |
| 1470 | % The directed edges from the nodes in A^w(x) to node x are all labeled with w. | |
| 1471 | % Nodes that have no predecessor correspond to decision/branching assignments | |
| 1472 | % (cf. GRASP: A Search Algorithm for Propositional Satisfiability, by Marques-Silva and Sakallah). | |
| 1473 | % As an improvement, we apply first UIP clause learning (cf. Efficient Conflict Driven Learning in a Boolean Satisfiability Solver, Zhang et al.). | |
| 1474 | % Compute the conflict graph for a conflicting unit-propagation of a variable and extract a backjump clause. | |
| 1475 | % -UsedVars are the SAT variables used during conflict analysis that are not part of the final bj clause (can be necessary for branching heuristic). | |
| 1476 | % -BjSatVars are the SAT variables in the final bj clause. | |
| 1477 | % Notes: | |
| 1478 | % - the variable references in the returned clause are not yet set | |
| 1479 | % - we do not create an actual graph but apply Boolean resolution | |
| 1480 | get_backjump_clause_conflict_resolution(SolverEnv, StateMutable, ConflictLevel, ConflictClause, BjClause, BjLevel, BjSatVars, UsedVars) :- | |
| 1481 | get_last_decision_level(StateMutable, _), | |
| 1482 | new_mutdict(ResolvedSoFar), | |
| 1483 | get_backjump_clause_and_level(SolverEnv, ConflictLevel, ResolvedSoFar, ConflictClause, BjClause, BjLevel, TUsedVars), | |
| 1484 | get_variable_names_in_clause(BjClause, BjSatVars), | |
| 1485 | subtract(TUsedVars, BjSatVars, UsedVars). | |
| 1486 | ||
| 1487 | %% get_backjump_clause_and_level(+SolverEnv, +ConflictDLevel, +ResolvedSoFar, +TBjClause, -BjClause, -BjLevel, -UsedVars). | |
| 1488 | get_backjump_clause_and_level(SolverEnv, ConflictDLevel, ResolvedSoFar, TBjClause, MinBjClause, BjLevel, UsedVars) :- | |
| 1489 | get_backjump_clause_and_level_sub(ConflictDLevel, 0, _, TBjClause, Resolver-RPol-RPropType-ROriginalClause, ThisLevelCount), | |
| 1490 | ( ThisLevelCount == 1 | |
| 1491 | -> % break, first UIP | |
| 1492 | BjClause = TBjClause, | |
| 1493 | clause_minimization(ClauseMinType), | |
| 1494 | ( ClauseMinType \== none | |
| 1495 | -> ( minimize_clause(SolverEnv, ConflictDLevel, BjClause, ClauseMinType, MinBjClause), ! | |
| 1496 | ; add_error_fail(minimize_clause, 'Clause minimization failed: ', [BjClause]) | |
| 1497 | ) | |
| 1498 | ; MinBjClause = BjClause | |
| 1499 | ), | |
| 1500 | get_maximum_decision_level_other_than_current(MinBjClause, 0, ConflictDLevel, BjLevel), | |
| 1501 | get_variables_used_in_cdcl(ResolvedSoFar, MinBjClause, UsedVars) | |
| 1502 | ; ground(Resolver), | |
| 1503 | resolve(SolverEnv, TBjClause, ConflictDLevel, Resolver, RPol, RPropType, ROriginalClause, NToExpand), | |
| 1504 | mutdict_put(ResolvedSoFar, Resolver, Resolver), | |
| 1505 | get_backjump_clause_and_level(SolverEnv, ConflictDLevel, ResolvedSoFar, NToExpand, MinBjClause, BjLevel, UsedVars) | |
| 1506 | ). | |
| 1507 | ||
| 1508 | get_backjump_clause_and_level_sub(_, ThisLevelCountAcc, ResolverAcc-_-RPol-RPropType-ROriginalClause, [], ResolverAcc-RPol-RPropType-ROriginalClause, ThisLevelCountAcc). | |
| 1509 | get_backjump_clause_and_level_sub(ConflictDLevel, ThisLevelCountAcc, ResolverAcc-RACount-RPol-RPropType-ROriginalClause, [(PropType,(Level,ACount),_,OriginalClause)-Pol-_-SatVarName|T], Resolver, ThisLevelCount) :- | |
| 1510 | ( Level == ConflictDLevel | |
| 1511 | -> NThisLevelCountAcc is ThisLevelCountAcc + 1 | |
| 1512 | ; NThisLevelCountAcc = ThisLevelCountAcc | |
| 1513 | ), | |
| 1514 | ( ( | |
| 1515 | Level == ConflictDLevel, | |
| 1516 | % unit or theory propagation | |
| 1517 | PropType \== branch, | |
| 1518 | % use last assigned literal to resolve next | |
| 1519 | ( var(ResolverAcc) | |
| 1520 | ; ACount > RACount | |
| 1521 | ) | |
| 1522 | ) | |
| 1523 | -> NResolverAcc = SatVarName-ACount-Pol-PropType-OriginalClause | |
| 1524 | ; NResolverAcc = ResolverAcc-RACount-RPol-RPropType-ROriginalClause | |
| 1525 | ), | |
| 1526 | get_backjump_clause_and_level_sub(ConflictDLevel, NThisLevelCountAcc, NResolverAcc, T, Resolver, ThisLevelCount). | |
| 1527 | ||
| 1528 | negate_polarity(pred_true, pred_false). | |
| 1529 | negate_polarity(pred_false, pred_true). | |
| 1530 | ||
| 1531 | retractall_once(Assertion) :- | |
| 1532 | retractall(cdclt_sat_solver:Assertion), | |
| 1533 | !. | |
| 1534 | ||
| 1535 | asserta_once(Assertion) :- | |
| 1536 | call(cdclt_sat_solver:Assertion), | |
| 1537 | !. | |
| 1538 | asserta_once(Assertion) :- | |
| 1539 | asserta(cdclt_sat_solver:Assertion). | |
| 1540 | ||
| 1541 | b_pred_or_bool_true(X) :- X == truth; X == boolean_true; X == value(pred_true). | |
| 1542 | %b_pred_or_bool_false(X) :- X == falsity; X == boolean_false; X == value(pred_false). | |
| 1543 | ||
| 1544 | sat_conj_negate_to_clause(Pred, Clause) :- | |
| 1545 | conjunction_to_list(Pred, List), | |
| 1546 | maplist(sat_equality_negate_to_literal, List, Clause). | |
| 1547 | ||
| 1548 | sat_equality_negate_to_literal(b(equal(ID,Pol),pred,_), _-NegPol-_-Name) :- | |
| 1549 | ID = b(identifier(Name),_,_), | |
| 1550 | Pol = b(Value,boolean,_), | |
| 1551 | ( b_pred_or_bool_true(Value) | |
| 1552 | -> NegPol = pred_false | |
| 1553 | ; NegPol = pred_true | |
| 1554 | ). | |
| 1555 | ||
| 1556 | %%%%% Solver State | |
| 1557 | create_solver_state(StateMutable) :- | |
| 1558 | State = [cur_level:0,current_stack_size:0], | |
| 1559 | create_mutable(solver_state(State), StateMutable). | |
| 1560 | ||
| 1561 | %% get_full_state(+StateMutable, +Key, -Datum). | |
| 1562 | % We assume an order of the SolverState to prevent using member. | |
| 1563 | get_full_state(StateMutable, Key, Datum) :- | |
| 1564 | get_mutable(solver_state(SolverState), StateMutable), | |
| 1565 | get_full_state_ordered(Key, SolverState, Datum), !. | |
| 1566 | ||
| 1567 | get_full_state_ordered(cur_level, [cur_level:CurLevel,_], CurLevel). | |
| 1568 | get_full_state_ordered(current_stack_size, [_,current_stack_size:Size], Size). | |
| 1569 | ||
| 1570 | %% delete_from_heuristic(+SatVarName). | |
| 1571 | delete_from_heuristic(SatVarName) :- | |
| 1572 | ( fibonacci_heap:elm_exists(SatVarName) | |
| 1573 | -> fibonacci_heap:delete_elm_bt(SatVarName) | |
| 1574 | ; % it can be the case that SatVarName has already been removed | |
| 1575 | % from the mutable due to coroutines etc.; succeed in this case | |
| 1576 | true | |
| 1577 | ). | |
| 1578 | ||
| 1579 | %% update_full_state(+StateMutable, +Key, +Datum). | |
| 1580 | % We assume an order of the SolverState to prevent using member. | |
| 1581 | update_full_state(StateMutable, Key, Datum) :- | |
| 1582 | get_mutable(solver_state(SolverState), StateMutable), | |
| 1583 | update_full_state_ordered(Key, Datum, SolverState, NewSolverState), !, | |
| 1584 | update_mutable(solver_state(NewSolverState), StateMutable). | |
| 1585 | ||
| 1586 | update_full_state_ordered(cur_level, NewDatum, [cur_level:_,B], [cur_level:NewDatum,B]). | |
| 1587 | update_full_state_ordered(current_stack_size, NewDatum, [A,current_stack_size:_], [A,current_stack_size:NewDatum]). | |
| 1588 | ||
| 1589 | %% Initialize the dynamic solver state for a specific solver. | |
| 1590 | init_dynamic_solver_state(SolverName) :- | |
| 1591 | fibonacci_heap:init, | |
| 1592 | clean_dynamic_solver_state, | |
| 1593 | clear_pending_theory_propagations, | |
| 1594 | asserta(solver_name(SolverName)), | |
| 1595 | asserta(restarts(0)), | |
| 1596 | asserta(glue_clauses(0)), | |
| 1597 | %asserta(amount_clause_reductions(0)), | |
| 1598 | asserta(assignment_count_on_cur_level(0)), | |
| 1599 | asserta(amount_learned_clauses(0)), | |
| 1600 | asserta(conflict_stats(total(0), since_restart(0), since_reduction(0))), | |
| 1601 | asserta(recent_lbds_dl(Diff1-Diff1, 0)), | |
| 1602 | asserta(recent_stack_sizes_dl(Diff2-Diff2, 0)), | |
| 1603 | asserta(total_lbd_sum(0)), | |
| 1604 | init_luby_sequence. | |
| 1605 | ||
| 1606 | % avoid that cdclt reports solver_answered_unknown if preceding run had a time-out | |
| 1607 | % and no SAT solver used | |
| 1608 | reset_cdclt_sat_solver :- | |
| 1609 | retractall(assignment_timeout_occurred), | |
| 1610 | retractall(unfixed_deferred_set_error). | |
| 1611 | ||
| 1612 | clean_dynamic_solver_state :- | |
| 1613 | retractall(assignment_timeout_occurred), | |
| 1614 | retractall(allow_partial_model), | |
| 1615 | retractall(unfixed_deferred_set_error), | |
| 1616 | retractall(assignment_count_on_cur_level(_)), | |
| 1617 | retractall(pending_theory_prop(_,_)), | |
| 1618 | retractall(glue_clauses(_)), | |
| 1619 | retractall(glue_level(_,_,_)), | |
| 1620 | retractall(solver_name(_)), | |
| 1621 | retractall(restarts(_)), | |
| 1622 | retractall(is_restart), | |
| 1623 | retractall(bt_from_smt_solution), | |
| 1624 | retractall(recent_lbds_dl(_, _)), | |
| 1625 | retractall(recent_stack_sizes_dl(_, _)), | |
| 1626 | retractall(saved_phase(_, _)), | |
| 1627 | %retractall(amount_clause_reductions(_)), | |
| 1628 | retractall(amount_learned_clauses(_)), | |
| 1629 | retractall(luby_counter(_)), | |
| 1630 | %retractall(exclude_sat_solution_clause(_)), | |
| 1631 | retractall(total_lbd_sum(_)), | |
| 1632 | retractall(conflict_stats(_, _, _)), | |
| 1633 | retractall(idl_unsat_core(_)), | |
| 1634 | retractall(backjump_level(_)), | |
| 1635 | retractall(backjump_clause(_, _, _, _, _, _)). | |
| 1636 | ||
| 1637 | %% Remove dynamically stored unsat core found by the IDL solver. | |
| 1638 | remove_idl_unsat_core :- | |
| 1639 | retractall_once(idl_unsat_core(_)). | |
| 1640 | ||
| 1641 | %% Store an unsat core found by the IDL solver in the SMT solver's dynamic state. | |
| 1642 | store_idl_unsat_core(Core) :- | |
| 1643 | assignment_count_on_cur_level(ACount), | |
| 1644 | ACount > 1, % at least one unit propagation on this level, otherwise just backtrack | |
| 1645 | retractall_once(idl_unsat_core(_)), | |
| 1646 | asserta(idl_unsat_core(Core)). | |
| 1647 | ||
| 1648 | %% Announce backtracking after a solution has been found in order to backtrack to search for another solution. | |
| 1649 | %% We have to be able to distinguish between backtracking due to not finding a solution or backtracking | |
| 1650 | %% triggered by the user to find another solution. | |
| 1651 | announce_bt_from_smt_solution :- | |
| 1652 | asserta(bt_from_smt_solution). | |
| 1653 | %%%%% | |
| 1654 | ||
| 1655 | %% b_to_cnf_safe(+In, +State, -Out). | |
| 1656 | b_to_cnf_safe(In, State, Out) :- | |
| 1657 | b_to_cnf(In, State, TOut), | |
| 1658 | !, | |
| 1659 | Out = TOut. | |
| 1660 | b_to_cnf_safe(_, _, _) :- | |
| 1661 | add_internal_error('B to CNF conversion failed ', cdclt), | |
| 1662 | fail. | |
| 1663 | ||
| 1664 | %% b_to_cnf(+In, +State, -Out). | |
| 1665 | % Accepts predicates with conjunction, disjunction, and equality of SAT variables. No negations. | |
| 1666 | b_to_cnf(In, State, Out) :- | |
| 1667 | get_texpr_expr(In, Expr), | |
| 1668 | b_to_cnf_aux(Expr, State, Res, []), | |
| 1669 | !, | |
| 1670 | Res = Out. | |
| 1671 | b_to_cnf(In, _, _) :- | |
| 1672 | translate_bexpression(In, PPIn), | |
| 1673 | !, | |
| 1674 | add_error_fail(b_to_cnf, 'CNF conversion failed', PPIn). | |
| 1675 | ||
| 1676 | b_to_cnf(b(Expr,_,_Info), State) --> | |
| 1677 | !, | |
| 1678 | b_to_cnf_aux(Expr, State). | |
| 1679 | b_to_cnf(In, _, _, _) :- | |
| 1680 | add_error_fail(b_to_cnf, 'Not properly wrapped:', In). | |
| 1681 | ||
| 1682 | b_to_cnf_aux(X, _) --> | |
| 1683 | {X == truth}, !, | |
| 1684 | []. | |
| 1685 | b_to_cnf_aux(X, _) --> | |
| 1686 | {X == falsity}, !, | |
| 1687 | [[]]. | |
| 1688 | b_to_cnf_aux(equal(A,B), State) --> | |
| 1689 | {get_texpr_expr(B, Expr), | |
| 1690 | Expr == boolean_true, | |
| 1691 | get_texpr_expr(A, identifier(Name))}, | |
| 1692 | !, | |
| 1693 | {member(bind(Name,Res)-StackInfo, State)}, | |
| 1694 | [[StackInfo-pred_true-Res-Name]]. | |
| 1695 | b_to_cnf_aux(equal(A,B), State) --> | |
| 1696 | {get_texpr_expr(B, Expr), | |
| 1697 | Expr == boolean_false, | |
| 1698 | get_texpr_expr(A, identifier(Name)), | |
| 1699 | member(bind(Name,Res)-StackInfo, State)}, | |
| 1700 | [[StackInfo-pred_false-Res-Name]]. | |
| 1701 | b_to_cnf_aux(disjunct(D1,D2), State) --> | |
| 1702 | b_to_cnf_disj_aux(D1, D2, State). | |
| 1703 | b_to_cnf_aux(conjunct(A,B), State) --> | |
| 1704 | b_to_cnf(A, State), | |
| 1705 | b_to_cnf(B, State). | |
| 1706 | ||
| 1707 | b_to_cnf_disj_aux(D1, D2, State) --> | |
| 1708 | {get_texpr_expr(D1, conjunct(A,B))}, !, | |
| 1709 | {create_texpr(disjunct(A,D2), pred, [], DJ1), | |
| 1710 | create_texpr(disjunct(B,D2), pred, [], DJ2)}, | |
| 1711 | b_to_cnf_aux(conjunct(DJ1,DJ2), State). | |
| 1712 | b_to_cnf_disj_aux(D1, D2, State) --> | |
| 1713 | {get_texpr_expr(D2, conjunct(A,B))}, !, | |
| 1714 | {create_texpr(disjunct(D1,A), pred, [], DJ1), | |
| 1715 | create_texpr(disjunct(D1,B), pred, [], DJ2)}, | |
| 1716 | b_to_cnf_aux(conjunct(DJ1,DJ2), State). | |
| 1717 | b_to_cnf_disj_aux(D1, D2, State, Res, Acc) :- | |
| 1718 | b_to_cnf(D1, State, Res1), | |
| 1719 | b_to_cnf(D2, State, Res2), | |
| 1720 | !, | |
| 1721 | ( Res1 = [] | |
| 1722 | -> Res = Acc | |
| 1723 | ; Res1 = [[]] | |
| 1724 | -> append(Res2,Acc,Res) | |
| 1725 | ; Res2 = [] | |
| 1726 | -> Res = Acc | |
| 1727 | ; Res2 = [[]] | |
| 1728 | -> append(Res1,Acc,Res) | |
| 1729 | ; ( Res1 = [ResD1], | |
| 1730 | Res2 = [ResD2] | |
| 1731 | ) | |
| 1732 | -> Res = [Res12|Acc], | |
| 1733 | append(ResD1, ResD2, Res12) | |
| 1734 | ; join_clauses(Res1,Res2,Res,Acc) | |
| 1735 | -> true | |
| 1736 | ; add_error_fail(b_to_cnf_disj, 'Cannot join clauses: ', Res1:Res2) | |
| 1737 | ). | |
| 1738 | ||
| 1739 | join_clauses([], _) --> []. | |
| 1740 | join_clauses([Clause1|T], Clauses2) --> | |
| 1741 | join_clauses_aux(Clause1,Clauses2), | |
| 1742 | join_clauses(T,Clauses2). | |
| 1743 | ||
| 1744 | join_clauses_aux(_, []) --> []. | |
| 1745 | join_clauses_aux(Clause1, [Clause2|T]) --> | |
| 1746 | {append(Clause1, Clause2, NewClause)}, | |
| 1747 | [NewClause], | |
| 1748 | join_clauses_aux(Clause1, T). | |
| 1749 | ||
| 1750 | ||
| 1751 | % Used for random restarts. | |
| 1752 | % First restart is after 32nd conflict, second after additional 32 conflicts, | |
| 1753 | % third after additional 64 conflicts etc. | |
| 1754 | init_luby_sequence :- | |
| 1755 | retractall(luby_counter(_)), | |
| 1756 | % unit length of 32 | |
| 1757 | % 1,1,2,1,1,2,4,1,1,2,1,1,2,4,8,.. | |
| 1758 | assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), assertz(luby_counter(1)), assertz(luby_counter(1)), | |
| 1759 | assertz(luby_counter(2)), assertz(luby_counter(4)), assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), | |
| 1760 | assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), assertz(luby_counter(4)), assertz(luby_counter(8)), | |
| 1761 | assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), assertz(luby_counter(1)), assertz(luby_counter(1)), | |
| 1762 | assertz(luby_counter(2)), assertz(luby_counter(4)), assertz(luby_counter(8)), assertz(luby_counter(16)), assertz(luby_counter(1)), | |
| 1763 | assertz(luby_counter(1)), assertz(luby_counter(2)), assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), | |
| 1764 | assertz(luby_counter(4)), assertz(luby_counter(8)), assertz(luby_counter(16)), assertz(luby_counter(32)), assertz(luby_counter(1)), | |
| 1765 | assertz(luby_counter(1)), assertz(luby_counter(2)), assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), | |
| 1766 | assertz(luby_counter(4)), assertz(luby_counter(8)), assertz(luby_counter(16)), assertz(luby_counter(32)), assertz(luby_counter(64)), | |
| 1767 | assertz(luby_counter(1)), assertz(luby_counter(1)), assertz(luby_counter(2)), assertz(luby_counter(1)), assertz(luby_counter(1)), | |
| 1768 | assertz(luby_counter(2)), assertz(luby_counter(4)), assertz(luby_counter(8)), assertz(luby_counter(16)), assertz(luby_counter(32)), | |
| 1769 | assertz(luby_counter(64)), assertz(luby_counter(128)). | |
| 1770 | ||
| 1771 | % ---------------- | |
| 1772 | ||
| 1773 | %% simplify_cnf(+CNF, -Simplified). | |
| 1774 | % Boolean resolution. | |
| 1775 | simplify_cnf([], []). | |
| 1776 | simplify_cnf([Clause|T], NewCnf) :- | |
| 1777 | simplify_clause(Clause, _, Simplified, IsTrue), !, | |
| 1778 | Simplified \== [], % contradiction if a clause is empty | |
| 1779 | ( IsTrue == true | |
| 1780 | -> NewCnf = NT % remove true clauses | |
| 1781 | ; NewCnf = [Simplified|NT] | |
| 1782 | ), | |
| 1783 | simplify_cnf(T, NT). | |
| 1784 | ||
| 1785 | simplify_clause([], IsTrue, [], IsTrue). | |
| 1786 | simplify_clause([_-Pol-Var-_|T], IsTrueAcc, NT, IsTrue) :- | |
| 1787 | ground(Var), | |
| 1788 | Pol \== Var, | |
| 1789 | !, | |
| 1790 | simplify_clause(T, IsTrueAcc, NT, IsTrue). | |
| 1791 | simplify_clause([StackInfo-Pol-Var-SatVarName|T], IsTrueAcc, [StackInfo-Pol-Var-SatVarName|NT], IsTrue) :- | |
| 1792 | ( Pol == Var | |
| 1793 | -> IsTrueAcc = true | |
| 1794 | ; true | |
| 1795 | ), | |
| 1796 | simplify_clause(T, IsTrueAcc, NT, IsTrue). | |
| 1797 | ||
| 1798 | clause_order(_-_-_-A3, _-_-_-B3) :- A3 @< B3. | |
| 1799 | ||
| 1800 | %% unit_propagate_cnf(+SolverEnv, +StateMutable, +Clauses, -NewClauses). | |
| 1801 | % A simple unit propagation, useful to run before reification. | |
| 1802 | % Removes duplicates from each clause. | |
| 1803 | % Important to identify all unit clauses, b_to_cnf does not check for unique sat variables in clauses. | |
| 1804 | % An exhaustive unit-propagation prior to the reification is not beneficial | |
| 1805 | % since simplifying a CNF is slow compared to using watched literals in sat/4. | |
| 1806 | % Note: It is important to remove duplicates, e.g., using sort/2. Otherwise, a conflict clause with duplicates | |
| 1807 | % would lead to failure for first UIP CDCL (first UIP not recognized due to duplicate decision level). | |
| 1808 | unit_propagate_cnf(SolverEnv, StateMutable, Clauses, NewClauses) :- | |
| 1809 | unit_prop_clause_sort(true, SolverEnv, StateMutable, Clauses, _, _, TNewClauses), !, | |
| 1810 | simplify_cnf(TNewClauses, NewClauses). | |
| 1811 | ||
| 1812 | propagate_unit_clause([StackInfo-Pol-PrologVar-SatVarName], StateMutable, RAcc) :- | |
| 1813 | ( PrologVar == Pol | |
| 1814 | -> % duplicate unit clause already propagated | |
| 1815 | true | |
| 1816 | ; PrologVar = Pol, | |
| 1817 | RAcc = true, | |
| 1818 | debug_format_sat("deterministic unit propagation of ~w with polarity ~w before reification", [SatVarName,Pol]), | |
| 1819 | get_next_assignment_count_on_level(ACount), | |
| 1820 | StackInfo = (unit,(0,ACount),Pol,[_-Pol-PrologVar-SatVarName]), | |
| 1821 | bt_log_sat_stack(StateMutable, SatVarName, Pol), | |
| 1822 | log_unit_propagation | |
| 1823 | ). | |
| 1824 | ||
| 1825 | %% unit_prop_clause_sort(+Sort, +SolverEnv, +StateMutable, +CNF, +RAcc, -Resolved, -NewClauses). | |
| 1826 | % Removes duplicates from each clause if +Sort is true. | |
| 1827 | % Logs if a variable has been unit propagated in -Resolved using +RAcc. | |
| 1828 | unit_prop_clause_sort(_, _, _, [], RAcc, RAcc, []). | |
| 1829 | unit_prop_clause_sort(Sort, SolverEnv, StateMutable, [[StackInfo-Pol-PrologVar-SatVarName]|T], RAcc, Resolved, NT) :- | |
| 1830 | propagate_unit_clause([StackInfo-Pol-PrologVar-SatVarName], StateMutable, RAcc), | |
| 1831 | !, | |
| 1832 | unit_prop_clause_sort(Sort, SolverEnv, StateMutable, T, RAcc, Resolved, NT). | |
| 1833 | unit_prop_clause_sort(Sort, SolverEnv, StateMutable, [Clause|T], RAcc, Resolved, NewClauses) :- | |
| 1834 | ( Sort = true | |
| 1835 | -> remove_dups(Clause, TNewClause), | |
| 1836 | % clause_order ensures that watched literals are initially set to the same variables for stronger propagation | |
| 1837 | samsort(clause_order, TNewClause, NewClause) | |
| 1838 | ; NewClause = Clause | |
| 1839 | ), | |
| 1840 | ( NewClause = [_-_-_-_] | |
| 1841 | -> propagate_unit_clause(NewClause, StateMutable, RAcc), | |
| 1842 | NewClauses = NT | |
| 1843 | ; NewClauses = [NewClause|NT] | |
| 1844 | ), !, | |
| 1845 | unit_prop_clause_sort(Sort, SolverEnv, StateMutable, T, RAcc, Resolved, NT). | |
| 1846 | ||
| 1847 | % ---------------- | |
| 1848 | ||
| 1849 | portray_cnf(Clauses) :- length(Clauses,Len), format('CNF with ~w clauses:~n',[Len]), | |
| 1850 | maplist(portray_sat_clause,Clauses). | |
| 1851 | ||
| 1852 | portray_sat_clause(Clause) :- write(' '),maplist(portray_literal,Clause),nl. | |
| 1853 | ||
| 1854 | portray_literal(pred_false-PrologVar-ID) :- !, format('- ~w(~w) ',[ID,PrologVar]). | |
| 1855 | portray_literal(pred_true-PrologVar-ID) :- !, format(' ~w(~w) ',[ID,PrologVar]). | |
| 1856 | portray_literal(_StackInfo-pred_false-PrologVar-ID) :- !, format(' ~w(~w)* ',[ID,PrologVar]). | |
| 1857 | portray_literal(_StackInfo-pred_true-PrologVar-ID) :- !, format(' ~w(~w)* ',[ID,PrologVar]). | |
| 1858 | portray_literal(Lit) :- format(' *** UNKNOWN: ~w ',[Lit]). | |
| 1859 | ||
| 1860 | % ---------------- | |
| 1861 | ||
| 1862 | /* | |
| 1863 | %% static_sat_symmetry_breaking(+Clauses, +SolverEnv, +CurLevelMut, -NewSolverEnv). | |
| 1864 | % Static SAT symmetry breaking after unit propagation of problem_setup/3 but only once, e.g., not after a restart or bj to level 0 | |
| 1865 | % Can only be used for pure SAT solving. | |
| 1866 | static_sat_symmetry_breaking(_, SolverEnv, _, NewSolverEnv) :- | |
| 1867 | static_sat_symmetry_breaking(false), | |
| 1868 | !, | |
| 1869 | NewSolverEnv = SolverEnv. | |
| 1870 | static_sat_symmetry_breaking(Clauses, SolverEnv, CurLevelMut, NewSolverEnv) :- | |
| 1871 | \+ symmetry_breaking_pred(_, _), | |
| 1872 | !, | |
| 1873 | get_symmetry_breaking_predicates(Clauses, SBPsConjNoRef, NewSatVars), | |
| 1874 | asserta(symmetry_breaking_pred(SBPsConjNoRef,NewSatVars)), | |
| 1875 | static_sat_symmetry_breaking(Clauses, SolverEnv, CurLevelMut, NewSolverEnv). | |
| 1876 | static_sat_symmetry_breaking(_, SolverEnv, CurLevelMut, NewSolverEnv) :- | |
| 1877 | get_asserted_symmetry_breaking_pred(SolverEnv, SBPsConj, NewSolverEnv), | |
| 1878 | problem_setup(NewSolverEnv, CurLevelMut, SBPsConj). | |
| 1879 | ||
| 1880 | get_asserted_symmetry_breaking_pred(SolverEnv, SBPsConj, NewSolverEnv) :- | |
| 1881 | symmetry_breaking_pred(SBPsConjNoRef, NewSatVars), | |
| 1882 | add_symmetry_breaking_eqs_to_solver_env(NewSatVars, SolverEnv, NewSolverEnv), | |
| 1883 | get_from_solver_env(NewSolverEnv, pl_vars, PlVars), | |
| 1884 | set_variable_references_in_clauses(PlVars, SBPsConjNoRef, SBPsConj), | |
| 1885 | findall(Var, (member(Var, NewSatVars), bt_asserta(heuristic_tuple(Var,1))), _). | |
| 1886 | ||
| 1887 | %% add_symmetry_breaking_eqs_to_solver_env(+NewSatVars, +SolverEnv, -NewSolverEnv). | |
| 1888 | % Symmetry breaking might introduce new SAT variables for equalities inbetween cycles of permutations. | |
| 1889 | % We update the solver environment and create the corresponding SMT formulas for equalities here. | |
| 1890 | % This is necessary, e.g., if a SAT variable corresponding to an equality introduced | |
| 1891 | % from symmetry breaking is involved in a conflict. | |
| 1892 | add_symmetry_breaking_eqs_to_solver_env(NewSatVars, SolverEnv, NewSolverEnv) :- | |
| 1893 | SolverEnv = [sat_vars:SatVars,sat_varnames:SatVarNames,sat_bindings:SatBindings,t2b_env:Env,pl_vars:PrologSatVarTriple], | |
| 1894 | add_symmetry_breaking_eqs_to_solver_env(NewSatVars, SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple, NSatVars, NSatVarNames, NSatBindings, NEnv, NPrologSatVarTriple), | |
| 1895 | NewSolverEnv = [sat_vars:NSatVars,sat_varnames:NSatVarNames,sat_bindings:NSatBindings,t2b_env:NEnv,pl_vars:NPrologSatVarTriple]. | |
| 1896 | ||
| 1897 | add_symmetry_breaking_eqs_to_solver_env([], SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple, SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple). | |
| 1898 | add_symmetry_breaking_eqs_to_solver_env([NewSatVarName-EqClauses|T], SatVars, SatVarNames, SatBindings, Env, PrologSatVarTriple, NSatVars, NSatVarNames, NSatBindings, NEnv, NPrologSatVarTriple) :- | |
| 1899 | maplist(clause_to_smt_disjunction(SatVars), EqClauses, EqSmtClauses), | |
| 1900 | conjunct_predicates(EqSmtClauses, EqSmt1), % all true | |
| 1901 | maplist(negate_smt_formula, EqSmtClauses, NegEqSmtClauses), | |
| 1902 | conjunct_predicates(NegEqSmtClauses, EqSmt2), % or all false | |
| 1903 | EqSmt = b(disjunct(EqSmt1,EqSmt2),pred,[]), | |
| 1904 | SatVars1 = [b(identifier(NewSatVarName),boolean,[smt_formula(EqSmt),eq_symmetry_break])|SatVars], | |
| 1905 | SatVarNames1 = [NewSatVarName|SatVarNames], | |
| 1906 | SatBindings1 = [bind(NewSatVarName,Var)|SatBindings], | |
| 1907 | PrologSatVarTriple1 = [Var-NewSatVarName-EqSmt|PrologSatVarTriple], | |
| 1908 | Env1 = [(EqSmt,b(identifier(NewSatVarName),boolean,[]))|Env], | |
| 1909 | add_symmetry_breaking_eqs_to_solver_env(T, SatVars1, SatVarNames1, SatBindings1, Env1, PrologSatVarTriple1, NSatVars, NSatVarNames, NSatBindings, NEnv, NPrologSatVarTriple). | |
| 1910 | ||
| 1911 | %clause_to_smt_disjunction(_, [], b(truth,pred,[])). | |
| 1912 | clause_to_smt_disjunction(SatVars, [Pol-_-SatVarName|T], SmtDisj) :- | |
| 1913 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula), | |
| 1914 | clause_to_smt_disjunction(SatVars, T, SmtFormula, SmtDisj). | |
| 1915 | ||
| 1916 | clause_to_smt_disjunction(_, [], Acc, Acc). | |
| 1917 | clause_to_smt_disjunction(SatVars, [Pol-_-SatVarName|T], Acc, SmtDisj) :- | |
| 1918 | get_smt_formula_from_vars_for_sat_pol(SatVars, SatVarName, Pol, SmtFormula), | |
| 1919 | NAcc = b(disjunct(SmtFormula,Acc),pred,[]), | |
| 1920 | clause_to_smt_disjunction(SatVars, T, NAcc, SmtDisj). | |
| 1921 | */ | |
| 1922 | ||
| 1923 | /* | |
| 1924 | % Remove half of the clauses every "frequency_constant + constant_factor * x" conflicts, | |
| 1925 | % where x is the amount of clause reductions so far. We keep clauses with a small LBD forever. | |
| 1926 | possibly_discard_learned_clauses :- | |
| 1927 | conflict_stats(_, _, since_reduction(SRed)), | |
| 1928 | cdclt_settings:discard_learned_clauses_frequency_constant(Frequency), | |
| 1929 | SRed >= Frequency, % first check to improve performance | |
| 1930 | amount_clause_reductions(Reductions), | |
| 1931 | cdclt_settings:discard_learned_clauses_constant_factor(Factor), | |
| 1932 | Threshold is Frequency + Factor * Reductions, | |
| 1933 | SRed == Threshold, | |
| 1934 | !, | |
| 1935 | log_set_of_learned_clauses_reduction, | |
| 1936 | debug_format_sat("~nDiscard half of learned clauses..", []), | |
| 1937 | cdclt_settings:discard_clause_greater_lbd(LbdLimit), | |
| 1938 | amount_learned_clauses(ALC), | |
| 1939 | Half is ALC // 2, | |
| 1940 | NReductions is Reductions + 1, | |
| 1941 | retract(amount_clause_reductions(_)), | |
| 1942 | asserta(amount_clause_reductions(NReductions)), | |
| 1943 | discard_half_of_learned_clauses_greater_lbd(0, Half, LbdLimit, Removed), | |
| 1944 | log_forgotten_clauses(Removed), | |
| 1945 | retract(amount_learned_clauses(Old)), | |
| 1946 | New is Old - Removed, | |
| 1947 | asserta(amount_learned_clauses(New)), | |
| 1948 | retract(conflict_stats(total(Total), since_restart(SRRed), _)), | |
| 1949 | asserta(conflict_stats(total(Total), since_restart(SRRed), since_reduction(0))), !. | |
| 1950 | possibly_discard_learned_clauses. | |
| 1951 | % Remove half of the clauses learned so far. | |
| 1952 | % We keep clauses with an LBD smaller than cdclt_settings:discard_clause_greater_lbd/1 | |
| 1953 | % forever. Thus it is not guaranteed that exactly half of the clauses are deleted if | |
| 1954 | % a lot of high quality clauses have been learned. | |
| 1955 | discard_half_of_learned_clauses_greater_lbd(C, Half, LbdLimit, Removed) :- | |
| 1956 | C =< Half, | |
| 1957 | retract(backjump_clause(BjLevel, BjClause, LbdScore, BjSatVars, UsedVars, AC)), | |
| 1958 | !, | |
| 1959 | ( LbdScore > LbdLimit | |
| 1960 | -> C1 is C + 1, | |
| 1961 | discard_half_of_learned_clauses_greater_lbd(C1, Half, LbdLimit, Removed) | |
| 1962 | ; discard_half_of_learned_clauses_greater_lbd(C, Half, LbdLimit, Removed), | |
| 1963 | asserta(backjump_clause(BjLevel, BjClause, LbdScore, BjSatVars, UsedVars, AC)) | |
| 1964 | ). | |
| 1965 | discard_half_of_learned_clauses_greater_lbd(C, _, _, C). | |
| 1966 | */ |