From bbfe02b25ac47241bf1a5a6cc2368d4d7eaeaac2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Aug 2016 11:16:29 -0700 Subject: [PATCH] modulating data-type solver Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin.cpp | 17 +++++++++-------- src/ast/datatype_decl_plugin.h | 3 ++- src/smt/smt_consequences.cpp | 26 ++++++++++++++++++-------- src/smt/smt_context.cpp | 1 - src/smt/smt_context.h | 4 ++-- src/smt/smt_kernel.cpp | 8 ++++---- src/smt/smt_kernel.h | 3 ++- src/smt/smt_solver.cpp | 3 ++- src/smt/theory_datatype.h | 1 + src/solver/solver.cpp | 4 ++++ 10 files changed, 44 insertions(+), 26 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 8bfd9b36d..8ad33d6fc 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -732,7 +732,8 @@ void datatype_decl_plugin::get_op_names(svector & op_names, symbol datatype_util::datatype_util(ast_manager & m): m_manager(m), m_family_id(m.mk_family_id("datatype")), - m_asts(m) { + m_asts(m), + m_start(0) { } datatype_util::~datatype_util() { @@ -807,11 +808,11 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector const * constructors = get_datatype_constructors(ty); - ptr_vector::const_iterator it = constructors->begin(); - ptr_vector::const_iterator end = constructors->end(); // step 1) - for (; it != end; ++it) { - func_decl * c = *it; + unsigned sz = constructors->size(); + ++m_start; + for (unsigned j = 0; j < sz; ++j) { + func_decl * c = (*constructors)[(j + m_start) % sz]; unsigned num_args = c->get_arity(); unsigned i = 0; for (; i < num_args; i++) { @@ -823,9 +824,8 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vectorbegin(); - for (; it != end; ++it) { - func_decl * c = *it; + for (unsigned j = 0; j < sz; ++j) { + func_decl * c = (*constructors)[(j + m_start) % sz]; TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";); unsigned num_args = c->get_arity(); unsigned i = 0; @@ -964,6 +964,7 @@ void datatype_util::reset() { std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc >()); m_vectors.reset(); m_asts.reset(); + ++m_start; } /** diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 019dd339e..ba0bedd32 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -176,7 +176,8 @@ class datatype_util { obj_map m_is_enum; ast_ref_vector m_asts; ptr_vector > m_vectors; - + unsigned m_start; + func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector & forbidden_set); func_decl * get_constructor(sort * ty, unsigned c_id); diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 49236be1b..1cb943d9f 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -102,7 +102,7 @@ namespace smt { } } - void context::delete_unfixed(obj_map& var2val) { + void context::delete_unfixed(obj_map& var2val, expr_ref_vector& unfixed) { ast_manager& m = m_manager; ptr_vector to_delete; obj_map::iterator it = var2val.begin(), end = var2val.end(); @@ -137,14 +137,16 @@ namespace smt { to_delete.push_back(k); } } - IF_VERBOSE(1, verbose_stream() << "(get-consequences deleting: " << to_delete.size() << " num-values: " << var2val.size() << ")\n";); for (unsigned i = 0; i < to_delete.size(); ++i) { var2val.remove(to_delete[i]); + unfixed.push_back(to_delete[i]); } } lbool context::get_consequences(expr_ref_vector const& assumptions, - expr_ref_vector const& vars, expr_ref_vector& conseq) { + expr_ref_vector const& vars, + expr_ref_vector& conseq, + expr_ref_vector& unfixed) { m_antecedents.reset(); lbool is_sat = check(assumptions.size(), assumptions.c_ptr()); @@ -168,6 +170,9 @@ namespace smt { trail.push_back(val); var2val.insert(vars[i], val); } + else { + unfixed.push_back(vars[i]); + } } extract_fixed_consequences(0, var2val, _assumptions, conseq); unsigned num_units = assigned_literals().size(); @@ -179,7 +184,6 @@ namespace smt { unsigned num_iterations = 0; unsigned model_threshold = 2; while (!var2val.empty()) { - ++num_iterations; obj_map::iterator it = var2val.begin(); expr* e = it->m_key; expr* val = it->m_value; @@ -212,22 +216,29 @@ namespace smt { } if (get_assignment(lit) == l_true) { var2val.erase(e); + unfixed.push_back(e); } else if (get_assign_level(lit) > get_search_level()) { TRACE("context", tout << "Retry fixing: " << mk_pp(e, m) << "\n";); pop_to_search_lvl(); + IF_VERBOSE(1, verbose_stream() << "(get-consequences re-iterating)\n";); continue; } else { TRACE("context", tout << "Fixed: " << mk_pp(e, m) << "\n";); } + ++num_iterations; TRACE("context", tout << "Unfixed variables: " << var2val.size() << "\n";); - if (model_threshold <= num_iterations) { - delete_unfixed(var2val); + if (model_threshold <= num_iterations || num_iterations <= 2) { + unsigned num_deleted = unfixed.size(); + delete_unfixed(var2val, unfixed); + num_deleted = unfixed.size() - num_deleted; // The next time we check the model is after 1.5 additional iterations. model_threshold *= 3; model_threshold /= 2; + IF_VERBOSE(1, verbose_stream() << "(get-consequences deleting: " << num_deleted << " num-values: " << var2val.size() << " num-iterations: " << num_iterations << ")\n";); + } // repeat until we either have a model with negated literal or // the literal is implied at base. @@ -242,8 +253,7 @@ namespace smt { conseq.push_back(fml); var2val.erase(e); SASSERT(get_assignment(lit) == l_false); - } - + } } end_search(); return l_true; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 88d0c8aff..c692173e6 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3422,7 +3422,6 @@ namespace smt { } lbool context::bounded_search() { - SASSERT(!inconsistent()); unsigned counter = 0; TRACE("bounded_search", tout << "starting bounded search...\n";); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 30a262285..b20ad6d5c 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1347,7 +1347,7 @@ namespace smt { u_map m_antecedents; void extract_fixed_consequences(unsigned idx, obj_map& var2val, uint_set const& assumptions, expr_ref_vector& conseq); - void delete_unfixed(obj_map& var2val); + void delete_unfixed(obj_map& var2val, expr_ref_vector& unfixed); expr_ref antecedent2fml(uint_set const& ante); @@ -1391,7 +1391,7 @@ namespace smt { lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true); - lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq); + lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed); lbool setup_and_check(bool reset_cancel = true); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 8f18b7311..f740a39da 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -99,8 +99,8 @@ namespace smt { return m_kernel.check(num_assumptions, assumptions); } - lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) { - return m_kernel.get_consequences(assumptions, vars, conseq); + lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) { + return m_kernel.get_consequences(assumptions, vars, conseq, unfixed); } void get_model(model_ref & m) const { @@ -268,8 +268,8 @@ namespace smt { return r; } - lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) { - return m_imp->get_consequences(assumptions, vars, conseq); + lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) { + return m_imp->get_consequences(assumptions, vars, conseq, unfixed); } void kernel::get_model(model_ref & m) const { diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 4cf170681..a10961207 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -129,7 +129,8 @@ namespace smt { /** \brief extract consequences among variables. */ - lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq); + lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, + expr_ref_vector& conseq, expr_ref_vector& unfixed); /** \brief Return the model associated with the last check command. diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index ec874ed8f..3bd8ece51 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -68,7 +68,8 @@ namespace smt { } virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) { - return m_context.get_consequences(assumptions, vars, conseq); + expr_ref_vector unfixed(m_context.m()); + return m_context.get_consequences(assumptions, vars, conseq, unfixed); } virtual void assert_expr(expr * t) { diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index 95c729dc2..b97adacfe 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -97,6 +97,7 @@ namespace smt { virtual void pop_scope_eh(unsigned num_scopes); virtual final_check_status final_check_eh(); virtual void reset_eh(); + virtual void restart_eh() { m_util.reset(); } virtual bool is_shared(theory_var v) const; public: theory_datatype(ast_manager & m, theory_datatype_params & p); diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index b0ae6a540..79bede1da 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -69,6 +69,7 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector tmp = vars[i]; val = eval(tmp); if (!m.is_value(val)) { + // vars[i] is unfixed continue; } if (m.is_bool(tmp) && is_uninterp_const(tmp)) { @@ -81,6 +82,7 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector lit = m.mk_not(tmp); } else { + // vars[i] is unfixed continue; } scoped_assumption_push _scoped_push(asms1, nlit); @@ -89,6 +91,7 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector case l_undef: return is_sat; case l_true: + // vars[i] is unfixed break; case l_false: get_unsat_core(core); @@ -114,6 +117,7 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector case l_undef: return is_sat; case l_true: + // vars[i] is unfixed break; case l_false: get_unsat_core(core);