From af90992858823cbb3b28ecd65a88c93a271adf7c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 17:01:36 -0700 Subject: [PATCH] fix #4404 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 18 +----------------- src/cmd_context/cmd_context.h | 1 - src/muz/base/dl_context.cpp | 14 ++++---------- .../transforms/dl_mk_subsumption_checker.cpp | 1 - 4 files changed, 5 insertions(+), 29 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index e7a2f6795..0d36e976b 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -473,7 +473,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_status(UNKNOWN), m_numeral_as_real(false), m_ignore_check(false), - m_processing_pareto(false), m_exit_on_error(false), m_manager(m), m_own_manager(m == nullptr), @@ -1261,7 +1260,6 @@ void cmd_context::insert_aux_pdecl(pdecl * p) { } void cmd_context::reset(bool finalize) { - m_processing_pareto = false; m_logic = symbol::null; m_check_sat_result = nullptr; m_numeral_as_real = false; @@ -1307,7 +1305,6 @@ void cmd_context::reset(bool finalize) { void cmd_context::assert_expr(expr * t) { scoped_rlimit no_limit(m().limit(), 0); - m_processing_pareto = false; if (!m_check_logic(t)) throw cmd_exception(m_check_logic.get_last_error()); m_check_sat_result = nullptr; @@ -1320,7 +1317,6 @@ void cmd_context::assert_expr(expr * t) { } void cmd_context::assert_expr(symbol const & name, expr * t) { - m_processing_pareto = false; if (!m_check_logic(t)) throw cmd_exception(m_check_logic.get_last_error()); if (!produce_unsat_cores() || name == symbol::null) { @@ -1440,7 +1436,6 @@ static void restore(ast_manager & m, ptr_vector & c, unsigned old_sz) { } void cmd_context::restore_assertions(unsigned old_sz) { - m_processing_pareto = false; if (!has_manager()) { // restore_assertions invokes m(), so if cmd_context does not have a manager, it will try to create one. SASSERT(old_sz == m_assertions.size()); @@ -1460,7 +1455,6 @@ void cmd_context::restore_assertions(unsigned old_sz) { void cmd_context::pop(unsigned n) { m_check_sat_result = nullptr; - m_processing_pareto = false; if (n == 0) return; unsigned lvl = m_scopes.size(); @@ -1507,7 +1501,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions scoped_rlimit _rlimit(m().limit(), rlimit); expr_ref_vector asms(m()); asms.append(num_assumptions, assumptions); - if (!m_processing_pareto) { + if (!get_opt()->is_pareto()) { expr_ref_vector assertions(m()); unsigned sz = m_assertions.size(); for (unsigned i = 0; i < sz; ++i) { @@ -1523,9 +1517,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions } try { r = get_opt()->optimize(asms); - if (r == l_true && get_opt()->is_pareto()) { - m_processing_pareto = true; - } } catch (z3_error & ex) { throw ex; @@ -1533,9 +1524,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions catch (z3_exception & ex) { throw cmd_exception(ex.msg()); } - if (m_processing_pareto && r != l_true) { - m_processing_pareto = false; - } get_opt()->set_status(r); } else if (m_solver) { @@ -1575,10 +1563,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions validate_model(); } validate_check_sat_result(r); - if (was_opt && r != l_false && !m_processing_pareto) { - // get_opt()->display_assignment(regular_stream()); - } - model_ref md; if (r == l_true && m_params.m_dump_models && is_model_available(md)) { display_model(md); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 0f471179a..47818c273 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -192,7 +192,6 @@ protected: status m_status; bool m_numeral_as_real; bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files. - bool m_processing_pareto; // used when re-entering check-sat for pareto front. bool m_exit_on_error; static std::ostringstream g_error_stream; diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 707167e17..c418d2327 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -21,15 +21,15 @@ Revision History: #include #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" -#include "muz/base/dl_context.h" #include "ast/for_each_expr.h" #include "ast/ast_smt_pp.h" #include "ast/ast_smt2_pp.h" #include "ast/datatype_decl_plugin.h" #include "ast/scoped_proof.h" -#include "muz/base/fp_params.hpp" #include "ast/ast_pp_util.h" - +#include "ast/ast_util.h" +#include "muz/base/dl_context.h" +#include "muz/base/fp_params.hpp" namespace datalog { @@ -742,13 +742,7 @@ namespace datalog { } expr_ref context::get_background_assertion() { - expr_ref result(m); - switch (m_background.size()) { - case 0: result = m.mk_true(); break; - case 1: result = m_background[0].get(); break; - default: result = m.mk_and(m_background.size(), m_background.c_ptr()); break; - } - return result; + return mk_and(m_background); } void context::assert_expr(expr* e) { diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index d75ae0b46..447976cae 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -350,7 +350,6 @@ namespace datalog { return nullptr; } - //During the construction of the new set we may discover new total relations //(by quantifier elimination on the uninterpreted tails). SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule);