From fbae881ece6a08a6e2a0bbe3fdc1eba8024370d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Nov 2017 16:24:14 -0800 Subject: [PATCH] add option to bypass model converter during constraint addition. Simplify model definitions that come from blocked clauses Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 1 + src/solver/solver.cpp | 33 ++++++++++++++++-------- src/solver/solver.h | 6 +++-- src/tactic/generic_model_converter.cpp | 35 +++++++++++++++++++++++++- src/tactic/generic_model_converter.h | 3 +++ 5 files changed, 65 insertions(+), 13 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 5aab0b25f..7bbe4d29c 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -266,6 +266,7 @@ public: } virtual void set_produce_models(bool f) {} virtual void collect_param_descrs(param_descrs & r) { + solver::collect_param_descrs(r); goal2sat::collect_param_descrs(r); sat::solver::collect_param_descrs(r); } diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 2460557bc..eb2b0d016 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -178,24 +178,37 @@ bool solver::is_literal(ast_manager& m, expr* e) { void solver::assert_expr(expr* f) { expr_ref fml(f, get_manager()); - model_converter_ref mc = get_model_converter(); - mc = concat(mc0(), mc.get()); - if (mc) { - (*mc)(fml); + if (m_enforce_model_conversion) { + model_converter_ref mc = get_model_converter(); + mc = concat(mc0(), mc.get()); + if (mc) { + (*mc)(fml); + } } assert_expr_core(fml); } void solver::assert_expr(expr* f, expr* t) { ast_manager& m = get_manager(); - expr_ref fml(f, m); + expr_ref fml(f, m); expr_ref a(t, m); - model_converter_ref mc = get_model_converter(); - mc = concat(mc0(), mc.get()); - if (mc) { - (*mc)(fml); - // (*mc)(a); + if (m_enforce_model_conversion) { + model_converter_ref mc = get_model_converter(); + mc = concat(mc0(), mc.get()); + if (mc) { + (*mc)(fml); + // (*mc)(a); + } } assert_expr_core(fml, a); } +void solver::collect_param_descrs(param_descrs & r) { + r.insert("solver.enforce_model_conversion", CPK_BOOL, "(default: true) enforce model conversion when asserting formulas"); +} + +void solver::updt_params(params_ref const & p) { + m_params.copy(p); + m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", true); +} + diff --git a/src/solver/solver.h b/src/solver/solver.h index 780a55cf5..f6ad74042 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -45,7 +45,9 @@ public: */ class solver : public check_sat_result { params_ref m_params; + bool m_enforce_model_conversion; public: + solver(): m_enforce_model_conversion(true) {} virtual ~solver() {} /** @@ -56,7 +58,7 @@ public: /** \brief Update the solver internal settings. */ - virtual void updt_params(params_ref const & p) { m_params.copy(p); } + virtual void updt_params(params_ref const & p); /** \brief Retrieve set of parameters set on solver. @@ -67,7 +69,7 @@ public: \brief Store in \c r a description of the configuration parameters available in this solver. */ - virtual void collect_param_descrs(param_descrs & r) {} + virtual void collect_param_descrs(param_descrs & r); /** \brief Enable/Disable model generation for this solver object. diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index 8befffff5..5c0f8ed5c 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -20,6 +20,8 @@ Notes: #include "ast/ast_pp.h" #include "ast/for_each_expr.h" #include "ast/ast_util.h" +#include "ast/occurs.h" +#include "ast/rewriter/expr_safe_replace.h" #include "tactic/generic_model_converter.h" #include "model/model_v2_pp.h" #include "model/model_evaluator.h" @@ -110,7 +112,7 @@ void generic_model_converter::operator()(expr_ref& fml) { entry const& e = m_add_entries[i]; unsigned arity = e.m_f->get_arity(); if (arity == 0) { - fmls.push_back(m.mk_eq(m.mk_const(e.m_f), e.m_def)); + fmls.push_back(simplify_def(e)); } else { expr_ref_vector args(m); @@ -133,3 +135,34 @@ void generic_model_converter::operator()(expr_ref& fml) { } fml = mk_and(fmls); } + +/* + \brief simplify definition expansion from model converter in the case they come from blocked clauses. + In this case the definitions are of the form: + + x <=> x or not (C) + + or dually, + + x <=> not (not x or not C) + + in either case the definitions simplify to + + x or C + + */ +expr_ref generic_model_converter::simplify_def(entry const& e) { + expr_ref result(m); + expr_ref c(m.mk_const(e.m_f), m); + if (m.is_bool(c) && occurs(c, e.m_def)) { + expr_safe_replace rep(m); + expr_ref result1 = e.m_def; + expr_ref result2 = e.m_def; + rep.apply_substitution(c, m.mk_true(), result1); + rep.apply_substitution(c, m.mk_false(), result2); + return expr_ref(m.mk_and(m.mk_or(c, result2), m.mk_or(m.mk_not(c), result1)), m); + } + else { + return expr_ref(m.mk_eq(c, e.m_def), m); + } +} diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index 805bad0d8..a9043d5cf 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -35,6 +35,9 @@ class generic_model_converter : public model_converter { vector m_add_entries; vector m_hide_entries; obj_map m_first_idx; + + expr_ref simplify_def(entry const& e); + public: generic_model_converter(ast_manager & m) : m(m) {}