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) {