From adad468cd7ea30f0530f86fcce8eeeb1cb46ee55 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 Jul 2023 19:46:08 -0700 Subject: [PATCH] allow copy within a user scope #6827 this will allow copying the solver state within a scope. The new solver state has its state at level 0. It is not possible to pop scopes from the new solver (you can still pop scopes from the original solver). The reason for this semantics is the relative difficulty of implementing (getting it right) of a state copy that preserves scopes. --- src/sat/sat_solver.cpp | 3 ++- src/sat/sat_solver/inc_sat_solver.cpp | 3 --- src/smt/smt_context.cpp | 5 ++--- src/smt/smt_internalizer.cpp | 5 +++-- src/smt/smt_kernel.cpp | 4 ++-- src/smt/smt_kernel.h | 2 +- src/smt/smt_solver.cpp | 16 ++++++++-------- src/solver/assertions/asserted_formulas.cpp | 6 +++++- src/solver/tactic2solver.cpp | 3 --- 9 files changed, 23 insertions(+), 24 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e636ab110..b899ee479 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -238,7 +238,8 @@ namespace sat { } m_user_scope_literals.reset(); - m_user_scope_literals.append(src.m_user_scope_literals); + for (auto lit : src.m_user_scope_literals) + assign_unit(~lit); m_mc = src.m_mc; m_stats.m_units = init_trail_size(); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 8bf665ebf..4574d3da3 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -115,9 +115,6 @@ public: } solver* translate(ast_manager& dst_m, params_ref const& p) override { - if (m_num_scopes > 0) { - throw default_exception("Cannot translate sat solver at non-base level"); - } ast_translation tr(m, dst_m); m_solver.pop_to_base_level(); inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p, is_incremental()); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 7902a3440..27494cb58 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -154,9 +154,8 @@ namespace smt { src_af.get_macro_manager().copy_to(dst_af.get_macro_manager()); - if (!src_ctx.m_setup.already_configured()) { + if (!src_ctx.m_setup.already_configured()) return; - } for (unsigned i = 0; !src_m.proofs_enabled() && i < src_ctx.m_assigned_literals.size(); ++i) { literal lit = src_ctx.m_assigned_literals[i]; @@ -3233,7 +3232,7 @@ namespace smt { } expr * f = m_asserted_formulas.get_formula(qhead); proof * pr = m_asserted_formulas.get_formula_proof(qhead); - SASSERT(!pr || f == m.get_fact(pr)); + SASSERT(!pr || f == m.get_fact(pr)); internalize_assertion(f, pr, 0); ++qhead; } diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 68879b8ac..0e9e39996 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -297,9 +297,10 @@ namespace smt { void context::assert_default(expr * n, proof * pr) { internalize(n, true); literal l = get_literal(n); - if (l == false_literal) { + if (l == false_literal) set_conflict(mk_justification(justification_proof_wrapper(*this, pr))); - } + else if (l == true_literal) + return; else { justification* j = mk_justification(justification_proof_wrapper(*this, pr)); m_clause_proof.add(l, CLS_AUX, j); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index c4ecf6787..74f0bded6 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -63,8 +63,8 @@ namespace smt { return m_imp->m_kernel.get_manager(); } - void kernel::copy(kernel& src, kernel& dst) { - context::copy(src.m_imp->m_kernel, dst.m_imp->m_kernel); + void kernel::copy(kernel& src, kernel& dst, bool override_base) { + context::copy(src.m_imp->m_kernel, dst.m_imp->m_kernel, override_base); } bool kernel::set_logic(symbol logic) { diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index ccea5caf8..dacbb525e 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -50,7 +50,7 @@ namespace smt { ~kernel(); - static void copy(kernel& src, kernel& dst); + static void copy(kernel& src, kernel& dst, bool override_base); ast_manager & m() const; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index d415812b0..f91a31111 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -20,7 +20,7 @@ Notes: #include "util/dec_ref_util.h" #include "ast/reg_decl_plugins.h" #include "ast/for_each_expr.h" -#include "ast/ast_smt2_pp.h" +#include "ast/ast_pp.h" #include "ast/func_decl_dependencies.h" #include "smt/smt_kernel.h" #include "smt/params/smt_params.h" @@ -88,14 +88,14 @@ namespace { ast_translation translator(get_manager(), m); smt_solver * result = alloc(smt_solver, m, p, m_logic); - smt::kernel::copy(m_context, result->m_context); + smt::kernel::copy(m_context, result->m_context, true); if (mc0()) result->set_model_converter(mc0()->translate(translator)); - for (auto & kv : m_name2assertion) { - expr* val = translator(kv.m_value); - expr* key = translator(kv.m_key); + for (auto & [k, v] : m_name2assertion) { + expr* val = translator(k); + expr* key = translator(v); result->assert_expr(val, key); } @@ -104,9 +104,9 @@ namespace { ~smt_solver() override { dealloc(m_cuber); - for (auto& kv : m_name2assertion) { - get_manager().dec_ref(kv.m_key); - get_manager().dec_ref(kv.m_value); + for (auto& [k,v] : m_name2assertion) { + get_manager().dec_ref(k); + get_manager().dec_ref(v); } } diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index 4e64ee39f..ee94ac355 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -161,6 +161,9 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { if (inconsistent()) return; + if (m.is_true(e)) + return; + if (m_smt_params.m_preprocess) { TRACE("assert_expr_bug", tout << r << "\n";); set_eliminate_and(false); // do not eliminate and before nnf. @@ -507,7 +510,8 @@ void asserted_formulas::simplify_fmls::operator()() { else { af.push_assertion(result, result_pr, new_fmls); } - if (af.canceled()) return; + if (af.canceled()) + return; } af.swap_asserted_formulas(new_fmls); TRACE("asserted_formulas", af.display(tout);); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 8ecfb3680..861a83185 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -294,9 +294,6 @@ solver* tactic2solver::translate(ast_manager& m, params_ref const& p) { tactic* t = m_tactic->translate(m); tactic2solver* r = alloc(tactic2solver, m, t, p, m_produce_proofs, m_produce_models, m_produce_unsat_cores, m_logic); r->m_result = nullptr; - if (!m_scopes.empty()) { - throw default_exception("translation of contexts is only supported at base level"); - } ast_translation tr(m_assertions.get_manager(), m, false); for (unsigned i = 0; i < get_num_assertions(); ++i) {