From 5bf57c270071a29835a8dcafa93f411a91ad56f7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Oct 2018 08:14:19 -0700 Subject: [PATCH] fix cubing semantics Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 17 ++++++++--------- src/solver/tactic2solver.cpp | 1 + 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 7a77e3b4e..df2da82e7 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -308,9 +308,9 @@ public: return nullptr; } - expr_ref_vector last_cube() { + expr_ref_vector last_cube(bool is_sat) { expr_ref_vector result(m); - result.push_back(m.mk_false()); + result.push_back(is_sat ? m.mk_true() : m.mk_false()); return result; } @@ -334,16 +334,16 @@ public: lbool result = m_solver.cube(vars, lits, backtrack_level); switch (result) { case l_true: - return expr_ref_vector(m); + return last_cube(true); case l_false: - return last_cube(); + return last_cube(false); default: - SASSERT(!lits.empty()); - if (lits.empty()) { - IF_VERBOSE(0, verbose_stream() << "empty cube for undef\n";); - } break; } + if (lits.empty()) { + set_reason_unknown(m_solver.get_reason_unknown()); + return expr_ref_vector(m); + } expr_ref_vector fmls(m); expr_ref_vector lit2expr(m); lit2expr.resize(m_solver.num_vars() * 2); @@ -358,7 +358,6 @@ public: vs.push_back(x); } } - if (fmls.empty()) { IF_VERBOSE(0, verbose_stream() << "no literals were produced in cube\n"); } return fmls; } diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index cf0c6f9bc..3a905bafd 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -79,6 +79,7 @@ public: expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override { + set_reason_unknown("cubing is not supported on tactics"); return expr_ref_vector(get_manager()); }