From 7b3b1b6e9f70231d29981def70522913bc96ec20 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Sep 2018 14:04:15 -0700 Subject: [PATCH] pop to base before incremental internalization to ensure that units are not lost Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 3 ++- src/solver/solver.cpp | 21 +++++++++++---------- 2 files changed, 13 insertions(+), 11 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index ff55598c2..097d3f0fa 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -259,7 +259,7 @@ public: return m_num_scopes; } - void assert_expr_core2(expr * t, expr * a) override { + void assert_expr_core2(expr * t, expr * a) override { if (a) { m_asmsf.push_back(a); assert_expr_core(m.mk_implies(a, t)); @@ -473,6 +473,7 @@ public: } void convert_internalized() { + m_solver.pop_to_base_level(); if (!is_internalized() && m_fmls_head > 0) { internalize_formulas(); } diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 1f0dac0ce..0e2128990 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -178,10 +178,19 @@ lbool solver::preferred_sat(expr_ref_vector const& asms, vector return check_sat(0, nullptr); } -bool solver::is_literal(ast_manager& m, expr* e) { - return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e)); + +static bool is_m_atom(ast_manager& m, expr* f) { + if (!is_app(f)) return true; + app* _f = to_app(f); + family_id bfid = m.get_basic_family_id(); + if (_f->get_family_id() != bfid) return true; + if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) return false; + return m.is_eq(f) || m.is_distinct(f); } +bool solver::is_literal(ast_manager& m, expr* e) { + return is_m_atom(m, e) || (m.is_not(e, e) && is_m_atom(m, e)); +} void solver::assert_expr(expr* f) { expr_ref fml(f, get_manager()); @@ -257,14 +266,6 @@ expr_ref_vector solver::get_units(ast_manager& m) { return result; } -static bool is_m_atom(ast_manager& m, expr* f) { - if (!is_app(f)) return true; - app* _f = to_app(f); - family_id bfid = m.get_basic_family_id(); - if (_f->get_family_id() != bfid) return true; - if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) return false; - return m.is_eq(f) || m.is_distinct(f); -} expr_ref_vector solver::get_non_units(ast_manager& m) { expr_ref_vector result(m), fmls(m);