| 1 | % (c) 2019-2022 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(dpllt_solver, [dpllt_solve_predicate/3, | |
| 6 | dpllt_solve_predicate/4, | |
| 7 | dpllt_solve_predicate_in_state/4, | |
| 8 | dpllt_solve_predicate_in_state/5, | |
| 9 | get_amount_of_sat_variables/2]). | |
| 10 | ||
| 11 | :- use_module(library(lists)). | |
| 12 | :- use_module(library(timeout)). | |
| 13 | :- use_module(library(sets), [subtract/3]). | |
| 14 | :- use_module(library(clpfd), [fd_var/1, fd_min/2, fd_max/2]). | |
| 15 | ||
| 16 | :- use_module(smt_solvers_interface(ast_optimizer_for_smt)). | |
| 17 | ||
| 18 | :- use_module(dpllt_solver('symmetry_check/smt_symmetry_breaking')). | |
| 19 | :- use_module(dpllt_solver('dpllt_preprocessing')). | |
| 20 | :- use_module(dpllt_solver('dpllt_pred_to_sat')). | |
| 21 | :- use_module(dpllt_solver('dpllt_sat_solver')). | |
| 22 | :- use_module(dpllt_solver('difference_logic/difference_logic_solver')). | |
| 23 | :- use_module(dpllt_solver('difference_logic/ast_to_difference_logic')). | |
| 24 | ||
| 25 | :- use_module(probsrc(debug)). | |
| 26 | :- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]). | |
| 27 | :- use_module(probsrc(preferences), [get_preference/2, | |
| 28 | temporary_set_preference/2, | |
| 29 | reset_temporary_preference/1]). | |
| 30 | :- use_module(probsrc(b_compiler), [b_compile/6]). | |
| 31 | :- use_module(probsrc(b_enumerate), [b_tighter_enumerate_all_values/2]). | |
| 32 | :- use_module(probsrc(tools_meta),[safe_time_out/3]). | |
| 33 | :- use_module(probsrc(translate), [print_bexpr/1]). | |
| 34 | :- use_module(probsrc(tools), [start_ms_timer/1,stop_ms_timer_with_debug_msg/2]). | |
| 35 | :- use_module(probsrc(kernel_waitflags), [init_wait_flags/2,ground_wait_flags/1]). | |
| 36 | :- use_module(probsrc(kernel_objects), [infer_value_type/2]). | |
| 37 | :- use_module(probsrc(b_interpreter), [set_up_typed_localstate/6, | |
| 38 | b_test_boolean_expression/4, | |
| 39 | b_convert_bool/5]). | |
| 40 | :- use_module(probsrc(error_manager), [add_error/3, | |
| 41 | add_internal_error/2, | |
| 42 | add_message/2, | |
| 43 | check_error_occured/2, | |
| 44 | enter_new_error_scope/2, | |
| 45 | exit_error_scope/3, | |
| 46 | clear_enumeration_warnings/0, | |
| 47 | clear_wd_errors/0, | |
| 48 | critical_enumeration_warning_occured_in_error_scope/4]). | |
| 49 | :- use_module(probsrc(bsyntaxtree), [find_typed_identifier_uses/2, | |
| 50 | find_identifier_uses/3, | |
| 51 | check_ast/1, | |
| 52 | get_texpr_info/2, | |
| 53 | conjunct_predicates/2]). | |
| 54 | :- use_module(probsrc(module_information), [module_info/2]). | |
| 55 | ||
| 56 | :- module_info(group, dpllt). | |
| 57 | :- module_info(description,'This module provides a DPLL(T) based solver for B.'). | |
| 58 | ||
| 59 | :- dynamic initial_solution/0. | |
| 60 | :- volatile initial_solution/0. | |
| 61 | ||
| 62 | debug_format_dpllt(_, _) :- | |
| 63 | debug_mode(off), | |
| 64 | !. | |
| 65 | debug_format_dpllt(Msg, Vars) :- | |
| 66 | append(Msg, " (DPLL(T) Solver)~n", NCodes), | |
| 67 | atom_codes(NMsg, NCodes), | |
| 68 | format(NMsg, Vars), !. | |
| 69 | ||
| 70 | debug_format_dpllt(_, _, _) :- | |
| 71 | debug_mode(off), | |
| 72 | !. | |
| 73 | debug_format_dpllt(Msg, Vars, Pred) :- | |
| 74 | format(Msg, Vars), | |
| 75 | translate:print_bexpr(Pred), nl, !. | |
| 76 | ||
| 77 | init :- | |
| 78 | %retract(debug:debug_mode(_)), | |
| 79 | %asserta(debug:debug_mode(on)), | |
| 80 | % enumeration has to be linear for symmetry breaking but also set to false by default | |
| 81 | temporary_set_preference(randomise_enumeration_order, false), | |
| 82 | dpllt_pred_to_sat:reset_sat_var_id, | |
| 83 | retractall(initial_solution), | |
| 84 | retractall(idl_candidate_constants(_,_)), | |
| 85 | %temporary_set_preference(use_chr_solver, true), | |
| 86 | temporary_set_preference(unsat_core_algorithm, divide_and_conquer), % default is linear_greedy | |
| 87 | temporary_set_preference(use_smt_mode, false), | |
| 88 | temporary_set_preference(use_clpfd_solver, true), | |
| 89 | temporary_set_preference(optimize_ast, true), | |
| 90 | temporary_set_preference(use_common_subexpression_elimination, false), | |
| 91 | temporary_set_preference(normalize_ast_sort_commutative, false), | |
| 92 | temporary_set_preference(normalize_ast, false). | |
| 93 | ||
| 94 | reset_preferences :- | |
| 95 | reset_temporary_preference(randomise_enumeration_order), | |
| 96 | reset_temporary_preference(unsat_core_algorithm), | |
| 97 | reset_temporary_preference(use_smt_mode), | |
| 98 | reset_temporary_preference(use_clpfd_solver), | |
| 99 | reset_temporary_preference(optimize_ast), | |
| 100 | reset_temporary_preference(use_common_subexpression_elimination), | |
| 101 | reset_temporary_preference(normalize_ast_sort_commutative), | |
| 102 | reset_temporary_preference(normalize_ast). | |
| 103 | ||
| 104 | set_current_state(Pred, State, NPred) :- | |
| 105 | reset_optimizer_state, | |
| 106 | assert_state_id_values(State), | |
| 107 | replace_ids_with_ground_values(Pred, 0, [], NPred), | |
| 108 | reset_optimizer_state, !. | |
| 109 | ||
| 110 | %% dpllt_solve_predicate(+Pred, -SolvedPred, -Result). | |
| 111 | % Main interface predicate for DPLL(T) based solver which times out | |
| 112 | % with respect to ProB's time_out preference. | |
| 113 | dpllt_solve_predicate(Pred, SolvedPred, Result) :- | |
| 114 | dpllt_solve_predicate(default, Pred, SolvedPred, Result). | |
| 115 | ||
| 116 | %% dpllt_solve_predicate(+SolverName, +Pred, -SolvedPred, -Result). | |
| 117 | dpllt_solve_predicate(SolverName, Pred, SolvedPred, Result) :- | |
| 118 | init, | |
| 119 | get_preference(time_out, Timeout), | |
| 120 | safe_time_out(dpllt_solve_predicate_initialized(SolverName, Pred, TSolvedPred, SolverResult), | |
| 121 | Timeout, | |
| 122 | TimeoutResult), | |
| 123 | ( TimeoutResult == time_out | |
| 124 | -> Result = time_out, | |
| 125 | SolvedPred = Pred | |
| 126 | ; ground(SolverResult), | |
| 127 | Result = SolverResult, | |
| 128 | SolvedPred = TSolvedPred | |
| 129 | ). | |
| 130 | ||
| 131 | %% dpllt_solve_predicate_in_state(+Pred, +Pred, -Result). | |
| 132 | dpllt_solve_predicate_in_state(Pred, State, SolvedPred, Result) :- | |
| 133 | dpllt_solve_predicate_in_state(default, Pred, State, SolvedPred, Result). | |
| 134 | ||
| 135 | %% dpllt_solve_predicate_in_state(+SolverName, +Pred, +Pred, -Result). | |
| 136 | dpllt_solve_predicate_in_state(SolverName, Pred, State, SolvedPred, Result) :- | |
| 137 | set_current_state(Pred, State, NPred), | |
| 138 | get_equalities_from_bindings(State, EqConj), | |
| 139 | dpllt_solve_predicate(SolverName, b(conjunct(EqConj,NPred),pred,[]), SolvedPred, Result). | |
| 140 | ||
| 141 | dpllt_solve_predicate_initialized(SolverName, Pred, SolvedPred, Result) :- | |
| 142 | ( check_ast(Pred) | |
| 143 | -> ( check_error_occured(check_ast_typing, _) | |
| 144 | -> % input AST is not correctly typed | |
| 145 | SolvedPred = Pred, | |
| 146 | Result = error | |
| 147 | ; dpllt_solve_predicate_initialized_checked(SolverName, Pred, SolvedPred, Result) | |
| 148 | ) | |
| 149 | ; add_message(dpllt_solve_predicate_no_timeout, 'Input predicate is not well-defined~nProB\'s SMT solver transforms the input to a well-defined predicate before constraint solving~n'), | |
| 150 | dpllt_solve_predicate_initialized_checked(SolverName, Pred, SolvedPred, Result) | |
| 151 | ). | |
| 152 | ||
| 153 | dpllt_solve_predicate_initialized_checked(SolverName, Pred, SolvedPred, Result) :- | |
| 154 | call_cleanup(catch(dpllt_solve_predicate_no_timeout(SolverName, Pred, SolvedPred, Result), | |
| 155 | Exception, % TODO: catch specific exception instead of all | |
| 156 | handle_clpfd_overflow(SolverName, Exception, Pred, SolvedPred, Result) | |
| 157 | ), | |
| 158 | reset_preferences | |
| 159 | ). | |
| 160 | ||
| 161 | get_equalities_from_bindings([], b(truth,pred,[])). | |
| 162 | get_equalities_from_bindings([bind(Id,Val)|T], EqConj) :- | |
| 163 | get_equality_from_binding(bind(Id,Val), Eq), | |
| 164 | get_equalities_from_bindings(T, Eq, EqConj). | |
| 165 | ||
| 166 | get_equalities_from_bindings([], EqConj, EqConj). | |
| 167 | get_equalities_from_bindings([bind(Id,Val)|T], EqAcc, EqConj) :- | |
| 168 | get_equality_from_binding(bind(Id,Val), Eq), | |
| 169 | get_equalities_from_bindings(T, b(conjunct(Eq,EqAcc),pred,[]), EqConj). | |
| 170 | ||
| 171 | %% handle_clpfd_overflow(+SolverName, +Exception, +Pred, -SolvedPred, -Result). | |
| 172 | % Disable CLP(FD) interface and restart DPLL(T) if an overflow occured. | |
| 173 | handle_clpfd_overflow(SolverName, Exception, Pred, SolvedPred, Result) :- | |
| 174 | Exception = error(representation_error(Err),_), | |
| 175 | memberchk(Err, ['CLPFD integer overflow','max_clpfd_integer','min_clpfd_integer']), | |
| 176 | !, | |
| 177 | temporary_set_preference(use_clpfd_solver, false), | |
| 178 | dpllt_solve_predicate_initialized(SolverName, Pred, SolvedPred, Result). | |
| 179 | handle_clpfd_overflow(_, Exception, _, _, unknown) :- | |
| 180 | add_error(dpllt,'Exception occurred during solving:',Exception). | |
| 181 | ||
| 182 | % only for computing the amount of sat variables of benchmarks | |
| 183 | get_amount_of_sat_variables(Pred, AmountOfSatVars) :- | |
| 184 | simplify_negation(Pred, SPred), | |
| 185 | reset_optimizer_state, | |
| 186 | assert_ground_id_values(0, SPred), | |
| 187 | replace_ids_with_ground_values(SPred, 0, [], AstCardOpt), | |
| 188 | precompute_values(AstCardOpt, [instantiate_quantifier_limit(2)], AstPrecomputed), | |
| 189 | %writeq(AstCompiled),nl, | |
| 190 | (clean_up_pred(AstPrecomputed, _, CleanPred) -> true | |
| 191 | ; add_internal_error('Clean up failed ', dpllt), CleanPred=AstPrecomputed), | |
| 192 | ( CleanPred = b(truth,pred,_) | |
| 193 | -> AmountOfSatVars = 1 | |
| 194 | ; CleanPred = b(falsity,pred,_) | |
| 195 | -> AmountOfSatVars = 1 | |
| 196 | ; preprocess_predicate(false, false, CleanPred, LiftedPred, _, _), | |
| 197 | predicate_to_sat(normal, LiftedPred, _, _, _, SatVars1) | |
| 198 | ), | |
| 199 | length(SatVars1, AmountOfSatVars). | |
| 200 | ||
| 201 | %% dpllt_solve_predicate(+SolverName, +Pred, -SolvedPred, -SolverResult). | |
| 202 | % Interface predicate for DPLL(T) based solver without a timeout. | |
| 203 | dpllt_solve_predicate_no_timeout(SolverName, Pred, SolvedPred, SolverResult) :- | |
| 204 | %nl, write('Initial pred: '), nl, translate:print_bexpr(Pred), nl, | |
| 205 | %nl, write('Initial pred: '),nl,writeq(Pred),nl, | |
| 206 | %unfold_let(Pred, Unfolded), | |
| 207 | %nl, write('Unfolded pred: '), nl, translate:print_bexpr(Unfolded), nl, | |
| 208 | %( preferences:get_preference(smtlib2b_cleanup_predicate, true) | |
| 209 | %-> | |
| 210 | debug_format_dpllt("After parsing: ", [], Pred), | |
| 211 | debug_format_dpllt("~nStart preprocessing", []), | |
| 212 | start_ms_timer(T0), | |
| 213 | simplify_negation(Pred, SPred), | |
| 214 | debug_format_dpllt("After simplifying negations: ", [], SPred), | |
| 215 | reset_optimizer_state, | |
| 216 | assert_ground_id_values(0, SPred), % assert for later incremental clause learning | |
| 217 | %replace_ids_with_ground_values(SPred, 0, [], AstOpt), % this is slower for DPLL(T) | |
| 218 | precompute_values(SPred, [instantiate_quantifier_limit(2)], AstPrecomputed), | |
| 219 | debug_format_dpllt("After precomputing values: ", [], SPred), | |
| 220 | stop_ms_timer_with_debug_msg(T0,precompute_values_for_dpllt), | |
| 221 | find_identifier_uses(AstPrecomputed, [], UsedIds), | |
| 222 | temporary_set_preference(data_validation_mode, true), | |
| 223 | b_compile(AstPrecomputed, UsedIds, [], [], AstCompiled, no_wf_available), | |
| 224 | clear_wd_errors, % b_compile might throw a wd error | |
| 225 | reset_temporary_preference(data_validation_mode), | |
| 226 | debug_format_dpllt("After compiling values: ", [], AstCompiled), | |
| 227 | start_ms_timer(T1), | |
| 228 | (clean_up_pred(AstCompiled, _, CleanPred) -> true | |
| 229 | ; add_internal_error('Clean up failed ',SolverName), CleanPred=AstCompiled), | |
| 230 | stop_ms_timer_with_debug_msg(T1,clean_up_pred_for_dpllt), | |
| 231 | start_ms_timer(T2), | |
| 232 | debug_format_dpllt("After AST cleanup: ", [], CleanPred), | |
| 233 | %nl, write('Clean + sym pred: '), nl, translate:print_bexpr(SymPred), nl, | |
| 234 | %; CleanPred = Pred | |
| 235 | %), | |
| 236 | %nl, write('Clean pred: '),nl,writeq(CleanPred),nl, | |
| 237 | %nl, write('Sym pred: '),nl,translate:print_bexpr(SymPred),nl, | |
| 238 | ( CleanPred = b(truth,pred,_) | |
| 239 | -> SolverResult = solution([]), | |
| 240 | SolvedPred = b(truth,pred,[]) | |
| 241 | ; CleanPred = b(falsity,pred,_) | |
| 242 | -> SolverResult = contradiction_found, | |
| 243 | SolvedPred = b(falsity,pred,[]) | |
| 244 | ; is_rewrite_to_idl(RewriteToIdl), | |
| 245 | ( dpllt_settings:static_smt_symmetry_breaking(true) | |
| 246 | -> debug_format_dpllt("Start symmetry breaking..", []), | |
| 247 | ( get_symmetry_breaking_predicates_decomposed(CleanPred, SymPred) | |
| 248 | ; add_message(smt_symmetry_breaking, 'Symmetry breaking failed on the top-level.'), | |
| 249 | SymPred = b(truth,pred,[]) | |
| 250 | ) | |
| 251 | ; SymPred = b(truth,pred,[]) | |
| 252 | ), | |
| 253 | debug_format_dpllt("done.", []), | |
| 254 | dpllt_settings:static_syntax_analysis(PerformStaticAnalysis), | |
| 255 | preprocess_predicate(PerformStaticAnalysis, RewriteToIdl, CleanPred, LiftedPred, FilteredCandidateImplsConj, CandidateImpls), | |
| 256 | debug_format_dpllt("Lifted predicate: ", [], LiftedPred), | |
| 257 | predicate_to_sat(normal, LiftedPred, Env1, WDPOs1, SmtBoolFormula, SatVars1), | |
| 258 | preprocess_predicate(false, RewriteToIdl, SymPred, LiftedSymPred, _, _), | |
| 259 | predicate_to_sat(normal, WDPOs1, SatVars1, Env1, LiftedSymPred, Env2, WDPOs2, SymBoolFormula, SatVars2), | |
| 260 | ( PerformStaticAnalysis=true | |
| 261 | -> predicate_to_sat(only_reuse, WDPOs2, SatVars2, Env2, FilteredCandidateImplsConj, Env3, WDPOsList, ImplBoolFormula, SatVars3), | |
| 262 | debug_format_dpllt("Static analysis inferred: ", [], ImplBoolFormula) | |
| 263 | ; ImplBoolFormula = b(truth,pred,[]), | |
| 264 | SatVars3 = SatVars2, Env3 = Env2, WDPOsList = WDPOs2 | |
| 265 | ), | |
| 266 | % well-definedness implication on the top-level to encode well-definedness in the SAT solver | |
| 267 | dpllt_sat_solver:init_dynamic_solver_state(SolverName), % TODO: check if this can be moved inside the SAT solver again | |
| 268 | conjunct_predicates(WDPOsList, WDPOs), | |
| 269 | preprocess_predicate(false, RewriteToIdl, WDPOs, _, _, WDCandidateImpls), | |
| 270 | % theory deduction for wd | |
| 271 | get_wd_theory_implications(CandidateImpls, WDCandidateImpls, WDTheoryImpls), | |
| 272 | predicate_to_sat(normal, WDTheoryImpls, SatVars3, Env3, WDPOs, Env4, _, WDTheoryImplsBoolFormula, SatVars4), | |
| 273 | debug_format_dpllt("WD Theory Deduction Implications: ", [], WDTheoryImpls), | |
| 274 | predicate_to_sat(normal, WDPOs, SatVars4, Env4, WDPOs, NewEnv, _, WDPosBoolFormula, SatVars), | |
| 275 | debug_format_dpllt("WD Implication: ", [], WDPOs), | |
| 276 | debug_format_dpllt("WD Implication as Boolean formula: ", [], WDPosBoolFormula), | |
| 277 | !, | |
| 278 | conjunct_predicates([SymBoolFormula,WDTheoryImplsBoolFormula,ImplBoolFormula], AnalysisBoolFormula), | |
| 279 | find_typed_identifier_uses(LiftedPred, SmtVars), % TO DO: improve | |
| 280 | debug_format_dpllt("Check LiftedPred", []), | |
| 281 | ( check_ast(LiftedPred) | |
| 282 | -> true | |
| 283 | ; add_internal_error('AST is missing well-definedness information for solver ', SolverName) | |
| 284 | ), | |
| 285 | dpllt_sat_solver:cnf_to_smt(SmtBoolFormula, SolvedPred), | |
| 286 | stop_ms_timer_with_debug_msg(T2,preprocessing_for_dpllt), | |
| 287 | debug_format_dpllt("End preprocessing", []), | |
| 288 | start_ms_timer(T3), | |
| 289 | enter_new_error_scope(ScopeID, dpllt_solve_predicate), | |
| 290 | %nl, write('smtBoolFormula: '), nl, translate:print_bexpr(SmtBoolFormula), nl, | |
| 291 | %nl, write('Analysis Bool formula: '), nl, translate:print_bexpr(AnalysisBoolFormula), nl, | |
| 292 | call_cleanup(conflict_driven_clause_learning_online(SolverName, NewEnv, SmtVars, SatVars, WDPosBoolFormula, AnalysisBoolFormula, SmtBoolFormula, SolverResult), | |
| 293 | exit_error_scope(ScopeID, _, dpllt_solve_predicate)), | |
| 294 | stop_ms_timer_with_debug_msg(T3,dpllt_solving_success) | |
| 295 | ). | |
| 296 | dpllt_solve_predicate_no_timeout(_, Pred, _, _) :- | |
| 297 | add_error(dpllt_solve_predicate, 'Cannot create SAT formula from B predicate:', [Pred]). | |
| 298 | ||
| 299 | is_rewrite_to_idl(Res) :- | |
| 300 | get_preference(dpllt_use_idl_theory_solver,true), | |
| 301 | !, | |
| 302 | Res = true. | |
| 303 | is_rewrite_to_idl(false). | |
| 304 | ||
| 305 | %% conflict_driven_clause_learning_online(+SolverName, +Env, +SmtVars, +SatVars, +WDPosBoolFormula, +AnalysisBoolFormula, +BoolFormula, -SolverResult). | |
| 306 | % Conflict-driven clause learning from incomplete assignments of the boolean formula by setting up reification constraints | |
| 307 | % connecting the SAT and theory solvers. | |
| 308 | conflict_driven_clause_learning_online(_, _, _, _, _, _, b(truth,pred,_), SolverResult) :- | |
| 309 | !, | |
| 310 | SolverResult = solution([]). | |
| 311 | conflict_driven_clause_learning_online(_, _, _, _, _, _, b(falsity,pred,_), SolverResult) :- | |
| 312 | !, | |
| 313 | SolverResult = contradiction_found. | |
| 314 | conflict_driven_clause_learning_online(SolverName, Env, SmtVars, SatVars, WDPosBoolFormula, AnalysisBoolFormula, BoolFormula, SolverResult) :- | |
| 315 | optimize_clause_size_by_rewriting(BoolFormula, SatVars, TOptBoolFormula, NewSatVars, NewVarConjList), | |
| 316 | conjunct_predicates([AnalysisBoolFormula,TOptBoolFormula], TFullBoolFormula), | |
| 317 | conjunct_predicates(NewVarConjList, NewVarConj), | |
| 318 | ( NewVarConj = b(truth,pred,_) | |
| 319 | -> FullBoolFormula = TFullBoolFormula | |
| 320 | ; FullBoolFormula = b(conjunct(NewVarConj,TFullBoolFormula),pred,[]) | |
| 321 | ), | |
| 322 | %bool_formula_to_smt(FullBoolFormula, SmtFullBoolFormula), | |
| 323 | %translate:print_bexpr(FullBoolFormula), nl, | |
| 324 | get_bindings_from_ids(NewSatVars, SatBindings, SatVarNames, IdPrologVarTuples, PrologSatVarTriple), | |
| 325 | ( b_to_cnf(FullBoolFormula, SatBindings, CnfBoolFormula) | |
| 326 | -> true | |
| 327 | ; add_internal_error('B to CNF conversion failed ', dpllt) | |
| 328 | ), | |
| 329 | setup_theory_wf_store(SmtVars, SmtBindings, WfStoreSmt), | |
| 330 | ( get_preference(dpllt_use_idl_theory_solver,true) | |
| 331 | -> difference_logic_solver:init_idl_solver(IdlGraphMut) | |
| 332 | ; true | |
| 333 | ), | |
| 334 | ( WDPosBoolFormula \= b(truth,pred,_) | |
| 335 | -> % add WD PO implications | |
| 336 | b_to_cnf(WDPosBoolFormula, SatBindings, CnfWDPosBoolFormula), | |
| 337 | append(CnfWDPosBoolFormula, CnfBoolFormula, TNCnfBoolFormula) | |
| 338 | ; TNCnfBoolFormula = CnfBoolFormula | |
| 339 | ), | |
| 340 | dpllt_sat_solver:create_solver_state(SatStateMutable), | |
| 341 | SolverEnv = [sat_vars:NewSatVars,sat_varnames:SatVarNames,sat_bindings:SatBindings,t2b_env:Env,pl_vars:PrologSatVarTriple,smt_bindings:SmtBindings], | |
| 342 | dpllt_sat_solver:unit_propagate_cnf(SolverEnv, SatStateMutable, TNCnfBoolFormula, TNCnfBoolFormula2), | |
| 343 | sort(TNCnfBoolFormula2, NCnfBoolFormula), | |
| 344 | ( debug_mode(off) | |
| 345 | -> true | |
| 346 | ; dpllt_sat_solver:portray_cnf(NCnfBoolFormula) | |
| 347 | ), | |
| 348 | setup_reification(SatStateMutable, IdlGraphMut, IdPrologVarTuples, SmtBindings, WfStoreSmt), | |
| 349 | %format("Initial Smt Bindings after deterministic unit propagation:~n~w~n", [SmtBindings]), | |
| 350 | dpllt_sat_solver:sat(SolverName, SolverEnv, SatStateMutable, NCnfBoolFormula), | |
| 351 | %nl,nl,format("Exit sat solver, ground waitflags~n", []), | |
| 352 | %dpllt_sat_solver:portray_sat_stack(SatStateMutable), | |
| 353 | %\+ error_manager:check_error_occured(_, _), | |
| 354 | debug_format_dpllt("Ground waitflags", []), | |
| 355 | ( get_preference(dpllt_use_idl_theory_solver,true) | |
| 356 | -> propagate_fd_bounds_to_idl_solver(IdlGraphMut, SmtBindings),% TO DO: propagate from ProB to IDL solver earlier? | |
| 357 | get_idl_solution_bindings(IdlGraphMut, IdlBindings), | |
| 358 | ( % try one idl solution first since ProB could timeout, but do not enumerate idl solutions here | |
| 359 | set_bindings(IdlBindings, SmtBindings), | |
| 360 | ground_wait_flags(WfStoreSmt) | |
| 361 | ; exclude_idl_solution(IdlBindings, SmtBindings, WfStoreSmt), | |
| 362 | ( ground_wait_flags(WfStoreSmt) | |
| 363 | ; % fallback to idl solver and possibly enumerate all solutions | |
| 364 | critical_enumeration_warning_occured_in_error_scope(_, _, _, _), | |
| 365 | clear_enumeration_warnings, | |
| 366 | propagate_idl_solution_to_bindings_bt(IdlGraphMut, SmtBindings), | |
| 367 | ground_wait_flags(WfStoreSmt) | |
| 368 | ) | |
| 369 | ) | |
| 370 | ; ground_wait_flags(WfStoreSmt) | |
| 371 | ), | |
| 372 | ( check_error_occured(ErrorName, _), | |
| 373 | ErrorName \== warning(smt_symmetry_breaking), | |
| 374 | ErrorName \== smt_symmetry_breaking, | |
| 375 | fail | |
| 376 | ; true | |
| 377 | ), | |
| 378 | SolverResult = solution(SmtBindings), | |
| 379 | log_solution, | |
| 380 | announce_bt_from_smt_solution. | |
| 381 | conflict_driven_clause_learning_online(_, _, _, _, _, _, _, Res) :- | |
| 382 | \+ check_error_occured(well_definedness_error, _), | |
| 383 | critical_enumeration_warning_occured_in_error_scope(A, B, C, D), | |
| 384 | !, | |
| 385 | clear_enumeration_warnings, | |
| 386 | Res = no_solution_found(enumeration_warning(A,B,C,D,critical)). | |
| 387 | conflict_driven_clause_learning_online(_, _, _, _, _, _, _, Res) :- | |
| 388 | check_error_occured(ErrorName, _), | |
| 389 | ErrorName \== smt_symmetry_breaking, | |
| 390 | ErrorName \== warning(smt_symmetry_breaking), | |
| 391 | ErrorName \== well_definedness_error, | |
| 392 | ErrorName \== internal_error(b_compiler), | |
| 393 | !, | |
| 394 | Res = error. | |
| 395 | conflict_driven_clause_learning_online(_, _, _, _, _, _, _, error) :- | |
| 396 | \+ initial_solution, | |
| 397 | check_error_occured(well_definedness_error, Reason), | |
| 398 | add_error(well_definedness_error, Reason, 'conflict_driven_clause_learning_online'). | |
| 399 | conflict_driven_clause_learning_online(_, _, _, _, _, _, _, contradiction_found) :- | |
| 400 | \+ initial_solution, | |
| 401 | \+ check_error_occured(well_definedness_error, _). | |
| 402 | ||
| 403 | %% setup_reification(+SatStateMutable, +IdlGraphMut, +IdPrologVarTuples, +SmtBindings, +WfStoreSmt). | |
| 404 | % Set up reification constraints to connect SAT and SMT solver. | |
| 405 | % Propagates in both directions (b_convert_bool/5 implements theory propagation). | |
| 406 | setup_reification(_, _, [], _, _). | |
| 407 | setup_reification(SatStateMutable, IdlGraphMut, [(SatId,SatPrologVar)|T], SmtBindings, WfStoreSmt) :- | |
| 408 | get_texpr_info(SatId, Info), | |
| 409 | memberchk(smt_formula(SmtFormula), Info), | |
| 410 | !, | |
| 411 | SatId = b(identifier(SatVarName),_,_), | |
| 412 | setup_reification_for_solver(SatStateMutable, IdlGraphMut, SmtFormula, SmtBindings, WfStoreSmt, SatVarName, SatPrologVar), | |
| 413 | %sat_smt_reification(SatId, SatPrologVar, SmtBindings, WfStoreSmt), | |
| 414 | setup_reification(SatStateMutable, IdlGraphMut, T, SmtBindings, WfStoreSmt). | |
| 415 | setup_reification(SatStateMutable, IdlGraphMut, [_|T], SmtBindings, WfStoreSmt) :- | |
| 416 | % plain SAT variable which is not reified with a theory solver, e.g., introduced by CNF optimization rewriting | |
| 417 | setup_reification(SatStateMutable, IdlGraphMut, T, SmtBindings, WfStoreSmt). | |
| 418 | ||
| 419 | /*:- block sat_smt_reification(?, -, ?, ?). | |
| 420 | % without theory propagation | |
| 421 | sat_smt_reification(SatId, SatPrologVar, SmtBindings, WfStoreSmt) :- | |
| 422 | get_texpr_info(SatId, Info), | |
| 423 | memberchk(smt_formula(TSmtFormula), Info), | |
| 424 | ( SatPrologVar == pred_true | |
| 425 | -> SmtFormula = TSmtFormula | |
| 426 | ; SmtFormula = b(negation(TSmtFormula),pred,[]) | |
| 427 | ), | |
| 428 | b_test_boolean_expression(SmtFormula, SmtBindings, [], WfStoreSmt).*/ | |
| 429 | ||
| 430 | setup_reification_for_solver(SatStateMutable, IdlGraphMut, SmtFormula, SmtBindings, WfStoreSmt, SatVarName, SatPrologVar) :- | |
| 431 | log_theory_propagation(SatStateMutable, SatVarName, SatPrologVar), | |
| 432 | ( get_preference(dpllt_use_idl_theory_solver,true) | |
| 433 | % TO DO: Problem beide Solver aufzusetzen: was ist wenn idl solver lösung findet aber prob timeout? | |
| 434 | -> ( ast_to_difference_logic:rewrite_to_idl(SmtFormula, [DLConstraint]) | |
| 435 | -> debug_format_dpllt("Constraint for IDL: ", [], SmtFormula), | |
| 436 | idl_solver_interface(IdlGraphMut, SatPrologVar, [DLConstraint]) | |
| 437 | ; log_idl_candidates_from_constraint(SmtFormula), | |
| 438 | propagate_non_idl_to_idl(IdlGraphMut, SatPrologVar, SmtFormula) | |
| 439 | ), | |
| 440 | sat_debug_msg(SatVarName,SmtFormula,SatPrologVar), | |
| 441 | b_convert_bool(SmtFormula, SmtBindings, [], WfStoreSmt, SatPrologVar) | |
| 442 | ; sat_debug_msg(SatVarName,SmtFormula,SatPrologVar), | |
| 443 | b_convert_bool(SmtFormula, SmtBindings, [], WfStoreSmt, SatPrologVar) | |
| 444 | ). | |
| 445 | ||
| 446 | sat_debug_msg(SatVarName,SmtFormula,SatPrologVar) :- | |
| 447 | (debug_mode(off) -> true | |
| 448 | ; format('% SAT variable ~w (~w) for ProB pred: ',[SatVarName,SatPrologVar]), | |
| 449 | print_bexpr(SmtFormula),nl). | |
| 450 | ||
| 451 | :- block log_theory_propagation(?, ?, -). | |
| 452 | log_theory_propagation(SatStateMutable, SatVarName, SatPrologVar) :- | |
| 453 | ground(SatPrologVar), | |
| 454 | ( is_last_propagated_sat_var(SatStateMutable, SatVarName) | |
| 455 | -> true | |
| 456 | ; dpllt_sat_solver:log_theory_propagation_sat_stack(SatStateMutable, SatVarName, SatPrologVar) | |
| 457 | ). | |
| 458 | ||
| 459 | :- dynamic idl_candidate_constants/2. | |
| 460 | :- volatile idl_candidate_constants/2. | |
| 461 | ||
| 462 | log_idl_candidates_from_constraint(Constraint) :- | |
| 463 | get_ids_and_int_constants(Constraint, Ids, IntConstants), | |
| 464 | Ids \== [], | |
| 465 | IntConstants \== [], | |
| 466 | !, | |
| 467 | assert_idl_candidates(Ids, IntConstants). | |
| 468 | log_idl_candidates_from_constraint(_). | |
| 469 | ||
| 470 | assert_idl_candidates([], _). | |
| 471 | assert_idl_candidates([Id|T], IntConstants) :- | |
| 472 | retract(idl_candidate_constants(Id, Candidates)), | |
| 473 | !, | |
| 474 | subtract(IntConstants, Candidates, New), | |
| 475 | append(Candidates, New, NewCandidates), | |
| 476 | asserta(idl_candidate_constants(Id, NewCandidates)), | |
| 477 | assert_idl_candidates(T, IntConstants). | |
| 478 | assert_idl_candidates([Id|T], IntConstants) :- | |
| 479 | asserta(idl_candidate_constants(Id, IntConstants)), | |
| 480 | assert_idl_candidates(T, IntConstants). | |
| 481 | ||
| 482 | get_ids_and_int_constants(b(Node,pred,_), Ids, IntConstants) :- | |
| 483 | comparison_op(Node, Lhs, Rhs), | |
| 484 | get_ids_and_int_constants_expr(Lhs, [], [], IdsAcc, IntConstantsAcc), | |
| 485 | get_ids_and_int_constants_expr(Rhs, IdsAcc, IntConstantsAcc, Ids, IntConstants). | |
| 486 | ||
| 487 | get_ids_and_int_constants_expr(Id, IdsAcc, IntConstantsAcc, [Name|IdsAcc], IntConstantsAcc) :- | |
| 488 | Id = b(identifier(Name),integer,_). | |
| 489 | get_ids_and_int_constants_expr(Int, IdsAcc, IntConstantsAcc, IdsAcc, [Value,Value1|IntConstantsAcc]) :- | |
| 490 | ( Int = b(integer(Value),integer,_) | |
| 491 | ; Int = b(unary_minus(b(integer(Value),integer,_)),integer,_) | |
| 492 | ), | |
| 493 | % select positive and negative value | |
| 494 | Value1 is Value * -1. | |
| 495 | get_ids_and_int_constants_expr(b(Node,integer,_), IdsAcc, IntConstantsAcc, Ids, IntConstants) :- | |
| 496 | arithmetic_expr(Node, Lhs, Rhs), | |
| 497 | get_ids_and_int_constants_expr(Lhs, IdsAcc, IntConstantsAcc, NIdsAcc, NIntConstantsAcc), | |
| 498 | get_ids_and_int_constants_expr(Rhs, NIdsAcc, NIntConstantsAcc, Ids, IntConstants). | |
| 499 | ||
| 500 | comparison_op(less(Lhs,Rhs), Lhs, Rhs). | |
| 501 | comparison_op(less_equal(Lhs,Rhs), Lhs, Rhs). | |
| 502 | comparison_op(equal(Lhs,Rhs), Lhs, Rhs). | |
| 503 | comparison_op(not_equal(Lhs,Rhs), Lhs, Rhs). | |
| 504 | ||
| 505 | arithmetic_expr(minus(Lhs,Rhs), Lhs, Rhs). | |
| 506 | arithmetic_expr(add(Lhs,Rhs), Lhs, Rhs). | |
| 507 | arithmetic_expr(div(Lhs,Rhs), Lhs, Rhs). | |
| 508 | arithmetic_expr(floored_div(Lhs,Rhs), Lhs, Rhs). | |
| 509 | arithmetic_expr(power_of(Lhs,Rhs), Lhs, Rhs). | |
| 510 | arithmetic_expr(multiplication(Lhs,Rhs), Lhs, Rhs). | |
| 511 | arithmetic_expr(modulo(Lhs,Rhs), Lhs, Rhs). | |
| 512 | ||
| 513 | :- block propagate_non_idl_to_idl(?, -, ?). | |
| 514 | propagate_non_idl_to_idl(IdlGraphMut, SatPrologVar, SmtFormula) :- | |
| 515 | ( SatPrologVar == pred_true % TO DO: pred_false? | |
| 516 | % e.g., x:NAT -> x>=0 | |
| 517 | -> ( infer_constraints_for_idl_solver(SmtFormula, ConjList) | |
| 518 | -> register_constraints(IdlGraphMut, ConjList) | |
| 519 | ; true | |
| 520 | ) | |
| 521 | ; true | |
| 522 | ). | |
| 523 | ||
| 524 | %% idl_solver_interface(+IdlGraphMut, +SatPrologVar, +Constraint). | |
| 525 | :- block idl_solver_interface(?, -, ?). | |
| 526 | idl_solver_interface(IdlGraphMut, SatPrologVar, [DLConstraint]) :- | |
| 527 | SatPrologVar == pred_true, | |
| 528 | difference_logic_solver:remove_unsat_core, | |
| 529 | dpllt_sat_solver:remove_idl_unsat_core, | |
| 530 | ( difference_logic_solver:register_constraint(IdlGraphMut, DLConstraint) | |
| 531 | ; \+ dpllt_sat_solver:is_backjumping, | |
| 532 | propagate_idl_unsat_core_to_sat_solver(IdlGraphMut), | |
| 533 | fail | |
| 534 | ). | |
| 535 | idl_solver_interface(IdlGraphMut, SatPrologVar, [DLConstraint]) :- | |
| 536 | SatPrologVar == pred_false, | |
| 537 | difference_logic_solver:remove_unsat_core, | |
| 538 | dpllt_sat_solver:remove_idl_unsat_core, | |
| 539 | ( difference_logic_solver:register_constraint(IdlGraphMut, b(negation(DLConstraint),pred,[])) | |
| 540 | ; \+ dpllt_sat_solver:is_backjumping, | |
| 541 | propagate_idl_unsat_core_to_sat_solver(IdlGraphMut), | |
| 542 | fail | |
| 543 | ). | |
| 544 | ||
| 545 | propagate_idl_unsat_core_to_sat_solver(IdlGraphMut) :- | |
| 546 | difference_logic_solver:get_solver_result(IdlGraphMut, Res), | |
| 547 | Res == contradiction_found, | |
| 548 | difference_logic_solver:get_unsat_core(IdlCore), | |
| 549 | difference_logic_solver:remove_unsat_core, | |
| 550 | dpllt_sat_solver:store_idl_unsat_core(IdlCore). | |
| 551 | ||
| 552 | %% get_idl_solution_bindings(+IdlGraphMut, -Bindings). | |
| 553 | get_idl_solution_bindings(IdlGraphMut, Bindings) :- | |
| 554 | get_solver_result(IdlGraphMut, SolverResult), | |
| 555 | SolverResult = solution(Bindings). | |
| 556 | ||
| 557 | %% propagate_idl_solution_to_bindings_bt(+IdlGraphMut, +SmtBindings). | |
| 558 | propagate_idl_solution_to_bindings_bt(IdlGraphMut, SmtBindings) :- | |
| 559 | get_preference(dpllt_use_idl_theory_solver,true), | |
| 560 | !, | |
| 561 | % TO DO: try the current solution first | |
| 562 | ( get_candidate_bounds_from_non_idl_constraints(CandidateTuples), | |
| 563 | difference_logic_solver:try_candidate_bounds(IdlGraphMut, CandidateTuples, Result) | |
| 564 | ; difference_logic_solver:get_all_solutions_on_bt(IdlGraphMut, Result) | |
| 565 | ), | |
| 566 | Result = solution(Bindings), | |
| 567 | set_bindings(Bindings, SmtBindings). | |
| 568 | propagate_idl_solution_to_bindings_bt(_, _). | |
| 569 | ||
| 570 | %% propagate_fd_bounds_to_idl_solver(+IdlGraphMut, +SmtBindings). | |
| 571 | propagate_fd_bounds_to_idl_solver(IdlGraphMut, SmtBindings) :- | |
| 572 | get_preference(dpllt_use_idl_theory_solver,true), | |
| 573 | !, | |
| 574 | difference_logic_solver:get_registered_vars(IdlGraphMut, Vars), | |
| 575 | get_constraints_from_fd_bounds(SmtBindings, Vars, [], ConjList), | |
| 576 | difference_logic_solver:register_constraints(IdlGraphMut, ConjList). | |
| 577 | propagate_fd_bounds_to_idl_solver(_, _). | |
| 578 | ||
| 579 | get_constraints_from_fd_bounds(_, [], Acc, Acc). | |
| 580 | get_constraints_from_fd_bounds(SmtBindings, [Var|T], Acc, ConjList) :- | |
| 581 | memberchk(bind(Var, int(Int)), SmtBindings), | |
| 582 | integer(Int), | |
| 583 | !, | |
| 584 | Equality = b(equal(b(identifier(Var),integer,[]),b(integer(Int),integer,[])),pred,[]), | |
| 585 | get_constraints_from_fd_bounds(SmtBindings, T, [Equality|Acc], ConjList). | |
| 586 | get_constraints_from_fd_bounds(SmtBindings, [Var|T], Acc, ConjList) :- | |
| 587 | memberchk(bind(Var, int(FDVar)), SmtBindings), | |
| 588 | fd_var(FDVar), | |
| 589 | fd_min(FDVar, Min), | |
| 590 | fd_max(FDVar, Max), | |
| 591 | !, | |
| 592 | ( var_geq_min(Var, Min, MinBound) | |
| 593 | -> ( var_leq_max(Var, Max, MaxBound) | |
| 594 | -> NAcc = [b(conjunct(MinBound,MaxBound),pred,[])|Acc] | |
| 595 | ; NAcc = [MinBound|Acc] | |
| 596 | ) | |
| 597 | ; ( var_leq_max(Var, Max, MaxBound) | |
| 598 | -> NAcc = [MaxBound|Acc] | |
| 599 | ; NAcc = Acc | |
| 600 | ) | |
| 601 | ), | |
| 602 | get_constraints_from_fd_bounds(SmtBindings, T, NAcc, ConjList). | |
| 603 | get_constraints_from_fd_bounds(SmtBindings, [_|T], Acc, ConjList) :- | |
| 604 | get_constraints_from_fd_bounds(SmtBindings, T, Acc, ConjList). | |
| 605 | ||
| 606 | var_geq_min(Var, Min, MinBound) :- | |
| 607 | % -v <= -min | |
| 608 | integer(Min), | |
| 609 | Min1 is Min * -1, | |
| 610 | MinBound = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),b(identifier(Var),integer,[])),integer,[]),b(integer(Min1),integer,[])),pred,[]). | |
| 611 | ||
| 612 | var_leq_max(Var, Max, MaxBound) :- | |
| 613 | % v <= Max | |
| 614 | integer(Max), | |
| 615 | MaxBound = b(less_equal(b(identifier(Var),integer,[]),b(integer(Max),integer,[])),pred,[]). | |
| 616 | ||
| 617 | get_candidate_bounds_from_non_idl_constraints(CandidateTuples) :- | |
| 618 | findall((VarName,Candidates), idl_candidate_constants(VarName, Candidates), CandidateTuples). | |
| 619 | ||
| 620 | set_bindings([], _). | |
| 621 | set_bindings([binding(VarName,Val,_)|T], SmtBindings) :- | |
| 622 | member(bind(VarName,Val), SmtBindings), | |
| 623 | set_bindings(T, SmtBindings). | |
| 624 | ||
| 625 | %% exclude_idl_solution(+IdlBindings, +SmtBindings, +WfStoreSmt). | |
| 626 | exclude_idl_solution(IdlBindings, SmtBindings, WfStoreSmt) :- | |
| 627 | initial_solution, | |
| 628 | exclude_solution(IdlBindings, Exclusion), | |
| 629 | b_test_boolean_expression(Exclusion, SmtBindings, [], WfStoreSmt). | |
| 630 | exclude_idl_solution(_, _, _) :- | |
| 631 | \+ initial_solution. | |
| 632 | ||
| 633 | %% exclude_solution(+Bindings, -Exclusion). | |
| 634 | exclude_solution([], b(truth,pred,[])). | |
| 635 | exclude_solution([Binding|T], Exclusion) :- | |
| 636 | get_equality_from_binding(Binding, EQ), | |
| 637 | exclude_solution(T, EQ, Exclusion). | |
| 638 | ||
| 639 | exclude_solution([], Acc, Acc). | |
| 640 | exclude_solution([Binding|T], Acc, Exclusion) :- | |
| 641 | get_equality_from_binding(Binding, EQ), | |
| 642 | NAcc = b(disjunct(b(negation(EQ),pred,[]),Acc),pred,[]), | |
| 643 | exclude_solution(T, NAcc, Exclusion). | |
| 644 | ||
| 645 | %% get_equality_from_binding(+Binding, -EQ). | |
| 646 | get_equality_from_binding(Binding, EQ) :- | |
| 647 | ( Binding = bind(VarName,Val) | |
| 648 | ; Binding = binding(VarName,Val,_) | |
| 649 | ), | |
| 650 | infer_value_type(Val, Type), | |
| 651 | EQ = b(equal(b(identifier(VarName),Type,[]),b(value(Val),Type,[])),pred,[]). | |
| 652 | ||
| 653 | %% setup_theory_wf_store(+SmtVars, -SmtBindings, -WFStoreSMT). | |
| 654 | setup_theory_wf_store(SmtVars, SmtBindings, WFStoreSMT) :- | |
| 655 | set_up_typed_localstate(SmtVars, _, SmtTypedVals, [], SmtBindings, positive), | |
| 656 | init_wait_flags(WFStoreSMT, [wf_smt_cdcl]), | |
| 657 | b_tighter_enumerate_all_values(SmtTypedVals, WFStoreSMT),!. | |
| 658 | ||
| 659 | log_solution :- | |
| 660 | \+ initial_solution, | |
| 661 | !, | |
| 662 | asserta(initial_solution). | |
| 663 | log_solution. | |
| 664 | ||
| 665 | /* currently not used: | |
| 666 | unfold_let(Pred, Unfolded) :- | |
| 667 | unfold_let([], Pred, Unfolded). | |
| 668 | ||
| 669 | unfold_let(IdTuples, b(identifier(Name),_,_), Replacement) :- | |
| 670 | member((b(identifier(Name),_,_),Ast), IdTuples), | |
| 671 | !, | |
| 672 | Replacement = Ast. | |
| 673 | unfold_let(IdTuples, b(Node,_,_), Replacement) :- | |
| 674 | ( Node = let_predicate(Ids,Asts,Body) | |
| 675 | ; Node = let_expression(Ids,Asts,Body) | |
| 676 | ), | |
| 677 | !, | |
| 678 | maplist(unfold_let(IdTuples), Asts, NAsts), | |
| 679 | zip_acc(Ids, NAsts, IdTuples, NewIdTuples), % TODO: ideally remove IdTuples which are clashing with Ids | |
| 680 | unfold_let(NewIdTuples, Body, Replacement). | |
| 681 | unfold_let(IdTuples, b(Node,Type,Info), Replacement) :- | |
| 682 | syntaxtransformation(Node,Subs,Names,NSubs,NewNode),!, | |
| 683 | Replacement = b(NewNode,Type,Info), | |
| 684 | exclude(hidden_by_local_var(Names),IdTuples,NIdTuples), | |
| 685 | l_unfold_let(Subs,NIdTuples,NSubs). | |
| 686 | unfold_let(I, Ast, _) :- add_internal_error('Not a typed expression:', unfold_let(I,Ast,_)),fail. | |
| 687 | ||
| 688 | hidden_by_local_var(Names,(TID,_)) :- def_get_texpr_id(TID,ID), member(ID,Names). | |
| 689 | ||
| 690 | l_unfold_let([],_,[]). | |
| 691 | l_unfold_let([H|T],IdTuples,[NH|NT]) :- | |
| 692 | unfold_let(H,IdTuples,NH), | |
| 693 | l_unfold_let(T,IdTuples,NT). | |
| 694 | ||
| 695 | zip_acc([], [], Acc, Acc). | |
| 696 | zip_acc([A|T1], [B|T2], Acc, Zipped) :- | |
| 697 | zip_acc(T1, T2, [(A,B)|Acc], Zipped). % TODO: should we just store ID and not typed ID in A? | |
| 698 | ||
| 699 | */ | |
| 700 | ||
| 701 | %% For debugging: transform bool formula back to SMT | |
| 702 | /*bool_formula_to_smt(b(truth,pred,I), b(truth,pred,I)). | |
| 703 | bool_formula_to_smt(b(falsity,pred,I), b(falsity,pred,I)). | |
| 704 | bool_formula_to_smt(b(equal(Id,Bool),pred,_), Smt) :- | |
| 705 | Id = b(identifier(_),boolean,IdInfo), | |
| 706 | member(smt_formula(TSmt), IdInfo), | |
| 707 | !, | |
| 708 | ( Bool = b(boolean_true,boolean,_) | |
| 709 | -> Smt = TSmt | |
| 710 | ; Smt = b(negation(TSmt),pred,[]) | |
| 711 | ). | |
| 712 | bool_formula_to_smt(b(equal(Id,Bool),pred,I), Out) :- % bool ids from Tseitin optimization | |
| 713 | !, | |
| 714 | Out = b(equal(Id,Bool),pred,I). | |
| 715 | bool_formula_to_smt(b(conjunct(A,B),pred,I), Out) :- | |
| 716 | !, | |
| 717 | bool_formula_to_smt(A, SmtA), | |
| 718 | bool_formula_to_smt(B, SmtB), | |
| 719 | Out = b(conjunct(SmtA,SmtB),pred,I). | |
| 720 | bool_formula_to_smt(b(disjunct(A,B),pred,I), Out) :- | |
| 721 | !, | |
| 722 | bool_formula_to_smt(A, SmtA), | |
| 723 | bool_formula_to_smt(B, SmtB), | |
| 724 | Out = b(disjunct(SmtA,SmtB),pred,I).*/ | |
| 725 | %% |