From bbfe02b25ac47241bf1a5a6cc2368d4d7eaeaac2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Aug 2016 11:16:29 -0700 Subject: [PATCH 01/15] 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); From f2b5c11d1c4435d98f75d5209c856f89f60b682b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Aug 2016 03:52:45 -0700 Subject: [PATCH 02/15] add option for prettier proof printing, Issue #706 Signed-off-by: Nikolaj Bjorner --- examples/python/mus/mss.py | 52 +++++++++++++++++++--------- src/api/python/z3.py | 2 ++ src/ast/pp_params.pyg | 1 + src/cmd_context/basic_cmds.cpp | 22 +++++++----- src/cmd_context/interpolant_cmds.cpp | 1 - src/sat/sat_bceq.cpp | 4 +-- src/sat/sat_config.cpp | 4 +-- src/sat/sat_config.h | 4 +-- src/sat/sat_mus.cpp | 8 ++--- src/sat/sat_params.pyg | 4 +-- src/sat/sat_solver.cpp | 4 +-- src/smt/theory_arith_eq.h | 12 +++---- 12 files changed, 72 insertions(+), 46 deletions(-) diff --git a/examples/python/mus/mss.py b/examples/python/mus/mss.py index b31fd92a8..fd2d209da 100644 --- a/examples/python/mus/mss.py +++ b/examples/python/mus/mss.py @@ -73,6 +73,10 @@ class MSSSolver: self.varcache[i] = Not(v) return self.varcache[i] + # Retrieve the latest model + # Add formulas that are true in the model to + # the current mss + def update_unknown(self): self.model = self.s.model() new_unknown = set([]) @@ -83,23 +87,29 @@ class MSSSolver: new_unknown.add(x) self.unknown = new_unknown - def relax_core(self, core): - assert(core <= self.soft_vars) - prev = BoolVal(True) - core_list = [x for x in core] - self.soft_vars -= core - # replace x0, x1, x2, .. by - # Or(x1, x0), Or(x2, And(x1, x0)), Or(x3, And(x2, And(x1, x0))), ... - for i in range(len(core_list)-1): - x = core_list[i] - y = core_list[i+1] - prevf = And(x, prev) - prev = Bool("%s" % prevf) - self.s.add(prev == prevf) - zf = Or(prev, y) - z = Bool("%s" % zf) - self.s.add(z == zf) - self.soft_vars.add(z) + # Create a name, propositional atom, + # for formula 'fml' and return the name. + + def add_def(self, fml): + name = Bool("%s" % fml) + self.s.add(name == fml) + return name + + # replace Fs := f0, f1, f2, .. by + # Or(f1, f0), Or(f2, And(f1, f0)), Or(f3, And(f2, And(f1, f0))), ... + + def relax_core(self, Fs): + assert(Fs <= self.soft_vars) + prefix = BoolVal(True) + self.soft_vars -= Fs + Fs = [ f for f in Fs ] + for i in range(len(Fs)-1): + prefix = self.add_def(And(Fs[i], prefix)) + self.soft_vars.add(self.add_def(Or(prefix, Fs[i+1]))) + + # Resolve literals from the core that + # are 'explained', e.g., implied by + # other literals. def resolve_core(self, core): new_core = set([]) @@ -111,6 +121,14 @@ class MSSSolver: return new_core + # Given a current satisfiable state + # Extract an MSS, and ensure that currently + # encoutered cores are avoided in next iterations + # by weakening the set of literals that are + # examined in next iterations. + # Strengthen the solver state by enforcing that + # an element from the MCS is encoutered. + def grow(self): self.mss = [] self.mcs = [] diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 6c4ac13a4..39c646c01 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -118,6 +118,8 @@ def _get_args(args): try: if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)): return args[0] + elif len(args) == 1 and isinstance(args[0], set): + return [arg for arg in args[0]] else: return args except: # len is not necessarily defined when args is not a sequence (use reflection?) diff --git a/src/ast/pp_params.pyg b/src/ast/pp_params.pyg index 46273b140..6b43cbea3 100644 --- a/src/ast/pp_params.pyg +++ b/src/ast/pp_params.pyg @@ -16,4 +16,5 @@ def_module_params('pp', ('fixed_indent', BOOL, False, 'use a fixed indentation for applications'), ('single_line', BOOL, False, 'ignore line breaks when true'), ('bounded', BOOL, False, 'ignore characters exceeding max width'), + ('pretty_proof', BOOL, False, 'use slower, but prettier, printer for proofs'), ('simplify_implies', BOOL, True, 'simplify nested implications for pretty printing'))) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 84a0d9af8..87cbd2738 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -29,6 +29,7 @@ Notes: #include"gparams.h" #include"env_params.h" #include"well_sorted.h" +#include"pp_params.hpp" class help_cmd : public cmd { svector m_cmds; @@ -161,14 +162,19 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", { throw cmd_exception("proof is not well sorted"); } - // TODO: reimplement a new SMT2 pretty printer - ast_smt_pp pp(ctx.m()); - cmd_is_declared isd(ctx); - pp.set_is_declared(&isd); - pp.set_logic(ctx.get_logic()); - // ctx.regular_stream() << mk_pp(pr, ctx.m()) << "\n"; - pp.display_smt2(ctx.regular_stream(), pr); - ctx.regular_stream() << std::endl; + pp_params params; + if (params.pretty_proof()) { + ctx.regular_stream() << mk_pp(pr, ctx.m()) << std::endl; + } + else { + // TODO: reimplement a new SMT2 pretty printer + ast_smt_pp pp(ctx.m()); + cmd_is_declared isd(ctx); + pp.set_is_declared(&isd); + pp.set_logic(ctx.get_logic()); + pp.display_smt2(ctx.regular_stream(), pr); + ctx.regular_stream() << std::endl; + } }); #define PRINT_CORE() \ diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index c482b4d09..53da91d1e 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -28,7 +28,6 @@ #include"mpq.h" #include"expr2var.h" #include"pp.h" -#include"pp_params.hpp" #include"iz3interp.h" #include"iz3checker.h" #include"iz3profiling.h" diff --git a/src/sat/sat_bceq.cpp b/src/sat/sat_bceq.cpp index 9ff286aaa..fa0309327 100644 --- a/src/sat/sat_bceq.cpp +++ b/src/sat/sat_bceq.cpp @@ -493,14 +493,14 @@ namespace sat { void bceq::operator()() { if (!m_solver.m_config.m_bcd) return; flet _disable_bcd(m_solver.m_config.m_bcd, false); - flet _disable_min(m_solver.m_config.m_minimize_core, false); + flet _disable_min(m_solver.m_config.m_core_minimize, false); flet _disable_opt(m_solver.m_config.m_optimize_model, false); flet _bound_maxc(m_solver.m_config.m_max_conflicts, 1500); use_list ul; solver s(m_solver.m_params, m_solver.rlimit(), 0); s.m_config.m_bcd = false; - s.m_config.m_minimize_core = false; + s.m_config.m_core_minimize = false; s.m_config.m_optimize_model = false; s.m_config.m_max_conflicts = 1500; m_use_list = &ul; diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index aff023b22..f976e1d71 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -107,8 +107,8 @@ namespace sat { m_gc_increment = p.gc_increment(); } m_minimize_lemmas = p.minimize_lemmas(); - m_minimize_core = p.minimize_core(); - m_minimize_core_partial = p.minimize_core_partial(); + m_core_minimize = p.core_minimize(); + m_core_minimize_partial = p.core_minimize_partial(); m_optimize_model = p.optimize_model(); m_bcd = p.bcd(); m_dyn_sub_res = p.dyn_sub_res(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 2eff402ad..0234b5710 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -69,8 +69,8 @@ namespace sat { bool m_minimize_lemmas; bool m_dyn_sub_res; - bool m_minimize_core; - bool m_minimize_core_partial; + bool m_core_minimize; + bool m_core_minimize_partial; bool m_optimize_model; bool m_bcd; diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp index 9c7c8c7bb..7b3277b6c 100644 --- a/src/sat/sat_mus.cpp +++ b/src/sat/sat_mus.cpp @@ -58,7 +58,7 @@ namespace sat { } lbool mus::operator()() { - flet _disable_min(s.m_config.m_minimize_core, false); + flet _disable_min(s.m_config.m_core_minimize, false); flet _disable_opt(s.m_config.m_optimize_model, false); flet _is_active(m_is_active, true); IF_VERBOSE(3, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";); @@ -69,7 +69,7 @@ namespace sat { } lbool mus::mus1() { - bool minimize_partial = s.m_config.m_minimize_core_partial; + bool minimize_partial = s.m_config.m_core_minimize_partial; TRACE("sat", tout << "old core: " << s.get_core() << "\n";); literal_vector& core = get_core(); literal_vector& mus = m_mus; @@ -96,7 +96,7 @@ namespace sat { // IF_VERBOSE(0, verbose_stream() << "num literals: " << core << " " << mus << "\n";); break; } - if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) { + if (s.m_config.m_core_minimize_partial && s.m_stats.m_restart - m_restart > m_max_restarts) { IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";); set_core(); return l_true; @@ -172,7 +172,7 @@ namespace sat { lbool mus::qx(literal_set& assignment, literal_set& support, bool has_support) { lbool is_sat = l_true; - if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) { + if (s.m_config.m_core_minimize_partial && s.m_stats.m_restart - m_restart > m_max_restarts) { IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";); return l_true; } diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index c5ac97b4e..90e715a9d 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -19,8 +19,8 @@ def_module_params('sat', ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'), ('minimize_lemmas', BOOL, True, 'minimize learned clauses'), ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), - ('minimize_core', BOOL, False, 'minimize computed core'), - ('minimize_core_partial', BOOL, False, 'apply partial (cheap) core minimization'), + ('core.minimize', BOOL, False, 'minimize computed core'), + ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('optimize_model', BOOL, False, 'enable optimization of soft constraints'), ('bcd', BOOL, False, 'enable blocked clause decomposition for equality extraction'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'))) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 78067238a..d8d273f2b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -937,7 +937,7 @@ namespace sat { bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) { - flet _min1(m_config.m_minimize_core, false); + flet _min1(m_config.m_core_minimize, false); m_weight = 0; m_blocker.reset(); svector values; @@ -2015,7 +2015,7 @@ namespace sat { idx--; } reset_unmark(old_size); - if (m_config.m_minimize_core) { + if (m_config.m_core_minimize) { if (m_min_core_valid && m_min_core.size() < m_core.size()) { IF_VERBOSE(1, verbose_stream() << "(sat.updating core " << m_min_core.size() << " " << m_core.size() << ")\n";); m_core.reset(); diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index 8e1b52ee5..de76b6838 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -64,7 +64,7 @@ namespace smt { lower(v2)->push_justification(ante, numeral::zero(), proofs_enabled()); upper(v)->push_justification(ante, numeral::zero(), proofs_enabled()); - TRACE("arith_fixed_propagate_eq", tout << "propagate eq: v" << v << " = v" << v2 << "\n"; + TRACE("arith_eq", tout << "propagate eq: v" << v << " = v" << v2 << "\n"; display_var(tout, v); display_var(tout, v2);); m_stats.m_fixed_eqs++; @@ -175,7 +175,7 @@ namespace smt { timer.stop(); ok++; if (ok % 100000 == 0) { - TRACE("propagate_cheap_eq", + TRACE("arith_eq", tout << total << " " << ok << " " << static_cast(ok)/static_cast(total) << " " << timer.get_seconds() << "\n"; @@ -216,7 +216,7 @@ namespace smt { void theory_arith::propagate_cheap_eq(unsigned rid) { if (!propagate_eqs()) return; - TRACE("propagate_cheap_eq", tout << "checking if row " << rid << " can propagate equality.\n"; + TRACE("arith_eq", tout << "checking if row " << rid << " can propagate equality.\n"; display_row_info(tout, rid);); row const & r = m_rows[rid]; theory_var x; @@ -258,7 +258,7 @@ namespace smt { // found equality x = y antecedents ante(*this); collect_fixed_var_justifications(r, ante); - TRACE("propagate_cheap_eq", tout << "propagate eq using x-y=0 row:\n"; display_row_info(tout, r);); + TRACE("arith_eq", tout << "propagate eq using x-y=0 row:\n"; display_row_info(tout, r);); m_stats.m_offset_eqs++; propagate_eq_to_core(x, y, ante); } @@ -299,7 +299,7 @@ namespace smt { antecedents ante(*this); collect_fixed_var_justifications(r, ante); collect_fixed_var_justifications(r2, ante); - TRACE("propagate_cheap_eq", tout << "propagate eq two rows:\n"; + TRACE("arith_eq", tout << "propagate eq two rows:\n"; tout << "swapped: " << swapped << "\n"; tout << "x : v" << x << "\n"; tout << "x2 : v" << x2 << "\n"; @@ -343,7 +343,7 @@ namespace smt { antecedents.eqs().size(), antecedents.eqs().c_ptr(), _x, _y, antecedents.num_params(), antecedents.params("eq-propagate"))); - TRACE("propagate_eq_to_core", tout << "detected equality: #" << _x->get_owner_id() << " = #" << _y->get_owner_id() << "\n"; + TRACE("arith_eq", tout << "detected equality: #" << _x->get_owner_id() << " = #" << _y->get_owner_id() << "\n"; display_var(tout, x); display_var(tout, y);); ctx.assign_eq(_x, _y, eq_justification(js)); From 2d8325ed43444fb0d65abd5f14d4eb1511fdaad6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Aug 2016 06:05:13 -0700 Subject: [PATCH 03/15] fix axiomatization of str.replace. Fixes issue #703 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 8b6c5baba..15122d7b6 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2902,9 +2902,11 @@ void theory_seq::add_replace_axiom(expr* r) { expr_ref xty = mk_concat(x, t, y); expr_ref xsy = mk_concat(x, s, y); literal cnt = mk_literal(m_util.str.mk_contains(a ,s)); + literal a_emp = mk_eq_empty(a); + add_axiom(~a_emp, mk_seq_eq(r, a)); add_axiom(cnt, mk_seq_eq(r, a)); - add_axiom(~cnt, mk_seq_eq(a, xsy)); - add_axiom(~cnt, mk_seq_eq(r, xty)); + add_axiom(~cnt, a_emp, mk_seq_eq(a, xsy)); + add_axiom(~cnt, a_emp, mk_seq_eq(r, xty)); tightest_prefix(s, x); } From 879f792125ee295b95be7df59fc6fde6f3da614d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Aug 2016 06:13:52 -0700 Subject: [PATCH 04/15] fix axiomatization of str.replace. Fixes issue #703 Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 3 +++ src/smt/theory_seq.cpp | 6 ++++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index dc7307741..caf8bd5cb 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -144,6 +144,9 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const { if (length() < src.length()) { return zstring(*this); } + if (src.length() == 0) { + return zstring(*this); + } bool found = false; for (unsigned i = 0; i < length(); ++i) { bool eq = !found && i + src.length() <= length(); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 15122d7b6..6a2208ad4 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2903,10 +2903,12 @@ void theory_seq::add_replace_axiom(expr* r) { expr_ref xsy = mk_concat(x, s, y); literal cnt = mk_literal(m_util.str.mk_contains(a ,s)); literal a_emp = mk_eq_empty(a); + literal s_emp = mk_eq_empty(s); add_axiom(~a_emp, mk_seq_eq(r, a)); add_axiom(cnt, mk_seq_eq(r, a)); - add_axiom(~cnt, a_emp, mk_seq_eq(a, xsy)); - add_axiom(~cnt, a_emp, mk_seq_eq(r, xty)); + add_axiom(~s_emp, mk_seq_eq(r, a)); + add_axiom(~cnt, a_emp, s_emp, mk_seq_eq(a, xsy)); + add_axiom(~cnt, a_emp, s_emp, mk_seq_eq(r, xty)); tightest_prefix(s, x); } From 47e95f8676e9cf8db85de1a5127d614d19d92eab Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 20 Aug 2016 17:56:52 -0400 Subject: [PATCH 05/15] Fixed binding substitution in macro_util --- src/ast/macros/macro_util.cpp | 30 +++++++++++++++++------------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index bc2feafed..166b9c4b0 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -458,28 +458,32 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const { expr_ref_buffer var_mapping(m_manager); bool changed = false; unsigned num_args = head->get_num_args(); - unsigned max = num_args; + unsigned max_var_idx = 0; for (unsigned i = 0; i < num_args; i++) { - var * v = to_var(head->get_arg(i)); - if (v->get_idx() >= max) - max = v->get_idx() + 1; + var const * v = to_var(head->get_arg(i)); + if (v->get_idx() > max_var_idx) + max_var_idx = v->get_idx(); } TRACE("normalize_expr_bug", tout << "head: " << mk_pp(head, m_manager) << "\n"; tout << "applying substitution to:\n" << mk_bounded_pp(t, m_manager) << "\n";); for (unsigned i = 0; i < num_args; i++) { - var * v = to_var(head->get_arg(i)); + var * v = to_var(head->get_arg(i)); if (v->get_idx() != i) { changed = true; - var * new_var = m_manager.mk_var(i, v->get_sort()); - CTRACE("normalize_expr_bug", v->get_idx() >= num_args, tout << mk_pp(v, m_manager) << ", num_args: " << num_args << "\n";); - SASSERT(v->get_idx() < max); - var_mapping.setx(max - v->get_idx() - 1, new_var); - } - else { - var_mapping.setx(max - i - 1, v); + var_ref new_var(m_manager.mk_var(i, v->get_sort()), m_manager); + var_mapping.setx(max_var_idx - v->get_idx(), new_var); } + else + var_mapping.setx(max_var_idx - i, v); } + + for (unsigned i = num_args; i <= max_var_idx; i++) + // CMW: Won't be used, but dictates a larger binding size, + // so that the indexes between here and in the rewriter match. + // It's possible that we don't see the true max idx of all vars here. + var_mapping.setx(max_var_idx - i, 0); + if (changed) { // REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution. var_subst subst(m_manager, true); @@ -488,7 +492,7 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const { tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitution:\n"; for (unsigned i = 0; i < var_mapping.size(); i++) { if (var_mapping[i] != 0) - tout << "#" << i << " -> " << mk_pp(var_mapping[i], m_manager) << "\n"; + tout << "#" << i << " -> " << mk_ll_pp(var_mapping[i], m_manager); }); subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t); } From b03dc0af3b60237daf09137c6c9069a53b168ac3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 20 Aug 2016 17:57:00 -0400 Subject: [PATCH 06/15] fixed memory leaks --- src/parsers/smt/smtparser.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/parsers/smt/smtparser.cpp b/src/parsers/smt/smtparser.cpp index f50e8b339..c9b20850c 100644 --- a/src/parsers/smt/smtparser.cpp +++ b/src/parsers/smt/smtparser.cpp @@ -1573,7 +1573,8 @@ private: return false; } } - expr * p = m_manager.mk_pattern(ts.size(), (app*const*)(ts.c_ptr())); + expr_ref p(m_manager); + p = m_manager.mk_pattern(ts.size(), (app*const*)(ts.c_ptr())); if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) { set_error("invalid pattern", children[0]); return false; @@ -1581,8 +1582,11 @@ private: patterns.push_back(p); } else if (children[0]->string() == symbol("ex_act") && ts.size() == 1) { - app * sk_hack = m_manager.mk_app(m_sk_hack, 1, ts.c_ptr()); - expr * p = m_manager.mk_pattern(1, &sk_hack); + app_ref sk_hack(m_manager); + sk_hack = m_manager.mk_app(m_sk_hack, 1, ts.c_ptr()); + app * sk_hackp = sk_hack.get(); + expr_ref p(m_manager); + p = m_manager.mk_pattern(1, &sk_hackp); if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) { set_error("invalid pattern", children[0]); return false; From 0a09d5ff5285aa445634414d7bd99effdb9134fe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Aug 2016 11:33:40 -0300 Subject: [PATCH 07/15] check for non-nullness when handling optional info fields for marking. Fixes issue #719 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 16 ++++++++++++---- src/muz/transforms/dl_mk_coi_filter.cpp | 9 +++++++-- 2 files changed, 19 insertions(+), 6 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index d138685ed..93769a3b4 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1430,14 +1430,22 @@ ast_manager::~ast_manager() { for (; it_a != end_a; ++it_a) { ast* n = (*it_a); switch (n->get_kind()) { - case AST_SORT: - mark_array_ref(mark, to_sort(n)->get_info()->get_num_parameters(), to_sort(n)->get_info()->get_parameters()); + case AST_SORT: { + sort_info* info = to_sort(n)->get_info(); + if (info != 0) { + mark_array_ref(mark, info->get_num_parameters(), info->get_parameters()); + } break; - case AST_FUNC_DECL: - mark_array_ref(mark, to_func_decl(n)->get_info()->get_num_parameters(), to_func_decl(n)->get_info()->get_parameters()); + } + case AST_FUNC_DECL: { + func_decl_info* info = to_func_decl(n)->get_info(); + if (info != 0) { + mark_array_ref(mark, info->get_num_parameters(), info->get_parameters()); + } mark_array_ref(mark, to_func_decl(n)->get_arity(), to_func_decl(n)->get_domain()); mark.mark(to_func_decl(n)->get_range(), true); break; + } case AST_APP: mark.mark(to_app(n)->get_decl(), true); mark_array_ref(mark, to_app(n)->get_num_args(), to_app(n)->get_args()); diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index c452e2611..e3d01a537 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -44,6 +44,9 @@ namespace datalog { if (m_context.has_facts(r->get_decl(i))) { return 0; } + if (false && r->is_neg_tail(i)) { + return 0; + } if (r->is_neg_tail(i)) { if (!engine.get_fact(r->get_decl(i)).is_reachable()) { if (!new_tail) { @@ -53,11 +56,13 @@ namespace datalog { } new_tail = true; } - } else if (new_tail) { + } + else if (new_tail) { m_new_tail.push_back(r->get_tail(i)); m_new_tail_neg.push_back(true); } - } else { + } + else { SASSERT(!new_tail); if (!engine.get_fact(r->get_decl(i)).is_reachable()) { contained = false; From 510231df42f0d40a83121fa5363cd50cce6596ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Aug 2016 12:26:38 -0300 Subject: [PATCH 08/15] fix to #717. The bottom-up COI filter can only use positive facts for filtering Signed-off-by: Nikolaj Bjorner --- src/muz/dataflow/dataflow.h | 6 +++--- src/muz/transforms/dl_mk_coi_filter.cpp | 5 ++--- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/muz/dataflow/dataflow.h b/src/muz/dataflow/dataflow.h index 1e52c5f93..d2be194eb 100644 --- a/src/muz/dataflow/dataflow.h +++ b/src/muz/dataflow/dataflow.h @@ -72,7 +72,7 @@ namespace datalog { } e->get_data().m_value->push_back(cur); } - if (cur->get_uninterpreted_tail_size() == 0) { + if (cur->get_positive_tail_size() == 0) { func_decl *sym = cur->get_head()->get_decl(); bool new_info = m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_up(m_context, cur); if (new_info) { @@ -97,7 +97,7 @@ namespace datalog { } void step_bottom_up() { - for(todo_set::iterator I = m_todo[m_todo_idx].begin(), + for(todo_set::iterator I = m_todo[m_todo_idx].begin(), E = m_todo[m_todo_idx].end(); I!=E; ++I) { ptr_vector * rules; if (!m_body2rules.find(*I, rules)) @@ -236,7 +236,7 @@ namespace datalog { return m_facts.get(m_rule->get_decl(idx), Fact::null_fact); } unsigned size() const { - return m_rule->get_uninterpreted_tail_size(); + return m_rule->get_positive_tail_size(); } }; diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index e3d01a537..0f155f65b 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -44,9 +44,7 @@ namespace datalog { if (m_context.has_facts(r->get_decl(i))) { return 0; } - if (false && r->is_neg_tail(i)) { - return 0; - } + if (r->is_neg_tail(i)) { if (!engine.get_fact(r->get_decl(i)).is_reachable()) { if (!new_tail) { @@ -62,6 +60,7 @@ namespace datalog { m_new_tail_neg.push_back(true); } } + else { SASSERT(!new_tail); if (!engine.get_fact(r->get_decl(i)).is_reachable()) { From 882c3bd0cdcfbaa0f8d0d7a04cee3009e151bb1e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Aug 2016 18:18:11 -0300 Subject: [PATCH 09/15] fix unused variable warnings Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 4 ++-- src/smt/smt_consequences.cpp | 1 - src/smt/smt_internalizer.cpp | 1 - 3 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 93769a3b4..050ada521 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1865,8 +1865,8 @@ void ast_manager::delete_node(ast * n) { dec_array_ref(worklist, to_quantifier(n)->get_num_patterns(), to_quantifier(n)->get_patterns()); dec_array_ref(worklist, to_quantifier(n)->get_num_no_patterns(), to_quantifier(n)->get_no_patterns()); break; - default: - break; + default: + break; } if (m_debug_ref_count) { m_debug_free_indices.insert(n->m_id,0); diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 1ae9f28e7..922156d46 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -234,7 +234,6 @@ namespace smt { expr* e = it->m_key; expr* val = it->m_value; push_scope(); - unsigned current_level = m_scope_lvl; literal lit; if (m.is_bool(e)) { diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index a17271e4e..d4880f7d7 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1284,7 +1284,6 @@ namespace smt { TRACE("mk_clause", tout << "creating clause:\n"; display_literals(tout, num_lits, lits); tout << "\n";); switch (k) { case CLS_AUX: { - unsigned old_num_lits = num_lits; literal_buffer simp_lits; if (!simplify_aux_clause_literals(num_lits, lits, simp_lits)) return 0; // clause is equivalent to true; From d4539b8887306fb88add26efcc1fec36a90dbccb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Aug 2016 11:42:14 +0800 Subject: [PATCH 10/15] fix dt2bv transformation to only work with constants, issue #725 Signed-off-by: Nikolaj Bjorner --- src/tactic/bv/dt2bv_tactic.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 86717c807..e8763475b 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -112,7 +112,7 @@ class dt2bv_tactic : public tactic { unsigned idx = m_t.m_dt.get_constructor_idx(f); result = m_t.m_bv.mk_numeral(idx, bv_size); } - else { + else if (is_uninterp_const(a)) { // create a fresh variable, add bounds constraints for it. unsigned nc = m_t.m_dt.get_datatype_num_constructors(s); result = m.mk_fresh_const(f->get_name().str().c_str(), m_t.m_bv.mk_sort(bv_size)); @@ -130,6 +130,9 @@ class dt2bv_tactic : public tactic { m_t.m_ext->insert(f, f_def); m_t.m_filter->insert(to_app(result)->get_decl()); } + else { + return false; + } m_cache.insert(a, result); ++m_t.m_num_translated; return true; From 310c0f31a10ba2336897ab969f2f00abea61638c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Aug 2016 12:07:06 +0800 Subject: [PATCH 11/15] use type constrsaints for co-variant subtying to enable .net 3.5 Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Context.cs | 60 ++++++++++++++++++------------------ src/api/dotnet/Expr.cs | 8 ++--- src/api/dotnet/Fixedpoint.cs | 4 +-- src/api/dotnet/FuncDecl.cs | 2 +- src/api/dotnet/Goal.cs | 2 +- src/api/dotnet/Quantifier.cs | 12 ++++---- src/api/dotnet/Solver.cs | 6 ++-- src/api/dotnet/Z3Object.cs | 2 +- 8 files changed, 48 insertions(+), 48 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index b37dc12d7..6ca48fcb0 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -286,8 +286,8 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(name); - CheckContextMatch(fieldNames); - CheckContextMatch(fieldSorts); + CheckContextMatch(fieldNames); + CheckContextMatch(fieldSorts); return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts); } @@ -303,7 +303,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(name); - CheckContextMatch(enumNames); + CheckContextMatch(enumNames); return new EnumSort(this, name, enumNames); } @@ -423,7 +423,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(name); - CheckContextMatch(constructors); + CheckContextMatch(constructors); return new DatatypeSort(this, name, constructors); } @@ -436,7 +436,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(constructors, c => c != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(constructors); + CheckContextMatch(constructors); return new DatatypeSort(this, MkSymbol(name), constructors); } @@ -454,7 +454,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(names, name => name != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(names); + CheckContextMatch(names); uint n = (uint)names.Length; ConstructorList[] cla = new ConstructorList[n]; IntPtr[] n_constr = new IntPtr[n]; @@ -462,7 +462,7 @@ namespace Microsoft.Z3 { Constructor[] constructor = c[i]; Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays"); - CheckContextMatch(constructor); + CheckContextMatch(constructor); cla[i] = new ConstructorList(this, constructor); n_constr[i] = cla[i].NativeObject; } @@ -520,7 +520,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(name); - CheckContextMatch(domain); + CheckContextMatch(domain); CheckContextMatch(range); return new FuncDecl(this, name, domain, range); } @@ -551,7 +551,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(domain, d => d != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(domain); + CheckContextMatch(domain); CheckContextMatch(range); return new FuncDecl(this, MkSymbol(name), domain, range); } @@ -582,7 +582,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(domain, d => d != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(domain); + CheckContextMatch(domain); CheckContextMatch(range); return new FuncDecl(this, prefix, domain, range); } @@ -811,7 +811,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(f); - CheckContextMatch(args); + CheckContextMatch(args); return Expr.Create(this, f, args); } @@ -884,7 +884,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); - CheckContextMatch(args); + CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } @@ -970,7 +970,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -982,7 +982,7 @@ namespace Microsoft.Z3 Contract.Requires(t != null); Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.EnumToNative(t))); } @@ -995,7 +995,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -1025,7 +1025,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -1051,7 +1051,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -1064,7 +1064,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t))); } @@ -1077,7 +1077,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -2205,7 +2205,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(f); - CheckContextMatch(args); + CheckContextMatch(args); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args))); } @@ -2315,7 +2315,7 @@ namespace Microsoft.Z3 Contract.Requires(args != null); Contract.Requires(Contract.ForAll(args, a => a != null)); - CheckContextMatch(args); + CheckContextMatch(args); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } @@ -2328,7 +2328,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(args, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(args); + CheckContextMatch(args); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } @@ -2429,7 +2429,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -2593,7 +2593,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -2606,7 +2606,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -2621,7 +2621,7 @@ namespace Microsoft.Z3 { Contract.Requires(args != null); Contract.Requires(Contract.Result() != null); - CheckContextMatch(args); + CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Length, AST.ArrayToNative(args), k)); } @@ -2635,7 +2635,7 @@ namespace Microsoft.Z3 Contract.Requires(coeffs != null); Contract.Requires(args.Length == coeffs.Length); Contract.Requires(Contract.Result() != null); - CheckContextMatch(args); + CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length, AST.ArrayToNative(args), coeffs, k)); @@ -3386,7 +3386,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - CheckContextMatch(ts); + CheckContextMatch(ts); IntPtr last = IntPtr.Zero; if (ts != null && ts.Length > 0) @@ -3577,7 +3577,7 @@ namespace Microsoft.Z3 Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t))); } @@ -4810,7 +4810,7 @@ namespace Microsoft.Z3 } [Pure] - internal void CheckContextMatch(IEnumerable arr) + internal void CheckContextMatch(IEnumerable arr) where T : Z3Object { Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null)); diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index c995a12bd..cac62d2f0 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -98,7 +98,7 @@ namespace Microsoft.Z3 Contract.Requires(args != null); Contract.Requires(Contract.ForAll(args, a => a != null)); - Context.CheckContextMatch(args); + Context.CheckContextMatch(args); if (IsApp && args.Length != NumArgs) throw new Z3Exception("Number of arguments does not match"); NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args)); @@ -120,8 +120,8 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(to, t => t != null)); Contract.Ensures(Contract.Result() != null); - Context.CheckContextMatch(from); - Context.CheckContextMatch(to); + Context.CheckContextMatch(from); + Context.CheckContextMatch(to); if (from.Length != to.Length) throw new Z3Exception("Argument sizes do not match"); return Expr.Create(Context, Native.Z3_substitute(Context.nCtx, NativeObject, (uint)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to))); @@ -152,7 +152,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(to, t => t != null)); Contract.Ensures(Contract.Result() != null); - Context.CheckContextMatch(to); + Context.CheckContextMatch(to); return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to))); } diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 66449ddbb..e2fb7fe5a 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -71,7 +71,7 @@ namespace Microsoft.Z3 Contract.Requires(constraints != null); Contract.Requires(Contract.ForAll(constraints, c => c != null)); - Context.CheckContextMatch(constraints); + Context.CheckContextMatch(constraints); foreach (BoolExpr a in constraints) { Native.Z3_fixedpoint_assert(Context.nCtx, NativeObject, a.NativeObject); @@ -151,7 +151,7 @@ namespace Microsoft.Z3 Contract.Requires(relations != null); Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null)); - Context.CheckContextMatch(relations); + Context.CheckContextMatch(relations); Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject, AST.ArrayLength(relations), AST.ArrayToNative(relations)); switch (r) diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index 15b6a59db..2f5cd0ce8 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -339,7 +339,7 @@ namespace Microsoft.Z3 { Contract.Requires(args == null || Contract.ForAll(args, a => a != null)); - Context.CheckContextMatch(args); + Context.CheckContextMatch(args); return Expr.Create(Context, this, args); } diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index 5ee44f34b..521b453f8 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -82,7 +82,7 @@ namespace Microsoft.Z3 Contract.Requires(constraints != null); Contract.Requires(Contract.ForAll(constraints, c => c != null)); - Context.CheckContextMatch(constraints); + Context.CheckContextMatch(constraints); foreach (BoolExpr c in constraints) { Contract.Assert(c != null); // It was an assume, now made an assert just to be sure we do not regress diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index 38e435309..eb21ed2b9 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -172,10 +172,10 @@ namespace Microsoft.Z3 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); - Context.CheckContextMatch(patterns); - Context.CheckContextMatch(noPatterns); - Context.CheckContextMatch(sorts); - Context.CheckContextMatch(names); + Context.CheckContextMatch(patterns); + Context.CheckContextMatch(noPatterns); + Context.CheckContextMatch(sorts); + Context.CheckContextMatch(names); Context.CheckContextMatch(body); if (sorts.Length != names.Length) @@ -212,8 +212,8 @@ namespace Microsoft.Z3 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); Contract.Requires(bound == null || Contract.ForAll(bound, n => n != null)); - Context.CheckContextMatch(noPatterns); - Context.CheckContextMatch(patterns); + Context.CheckContextMatch(noPatterns); + Context.CheckContextMatch(patterns); //Context.CheckContextMatch(bound); Context.CheckContextMatch(body); diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index f8f340373..8cb7670d7 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -111,7 +111,7 @@ namespace Microsoft.Z3 Contract.Requires(constraints != null); Contract.Requires(Contract.ForAll(constraints, c => c != null)); - Context.CheckContextMatch(constraints); + Context.CheckContextMatch(constraints); foreach (BoolExpr a in constraints) { Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject); @@ -142,8 +142,8 @@ namespace Microsoft.Z3 Contract.Requires(constraints != null); Contract.Requires(Contract.ForAll(constraints, c => c != null)); Contract.Requires(Contract.ForAll(ps, c => c != null)); - Context.CheckContextMatch(constraints); - Context.CheckContextMatch(ps); + Context.CheckContextMatch(constraints); + Context.CheckContextMatch(ps); if (constraints.Length != ps.Length) throw new Z3Exception("Argument size mismatch"); diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs index cd6803341..f32ba30af 100644 --- a/src/api/dotnet/Z3Object.cs +++ b/src/api/dotnet/Z3Object.cs @@ -138,7 +138,7 @@ namespace Microsoft.Z3 } [Pure] - internal static IntPtr[] EnumToNative(IEnumerable a) + internal static IntPtr[] EnumToNative(IEnumerable a) where T : Z3Object { Contract.Ensures(a == null || Contract.Result() != null); Contract.Ensures(a == null || Contract.Result().Length == a.Count()); From 237fde1f76e8d2c1b90dbc17cfdea6f7f7494922 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 31 Aug 2016 09:57:46 +0800 Subject: [PATCH 12/15] fix crash during shutdown. Issue #719 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 050ada521..440179ba8 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -78,7 +78,10 @@ void parameter::del_eh(ast_manager & m, family_id fid) { } else if (is_external()) { SASSERT(fid != null_family_id); - m.get_plugin(fid)->del(*this); + decl_plugin * plugin = m.get_plugin(fid); + if (plugin) { + plugin->del(*this); + } } } @@ -1418,9 +1421,10 @@ ast_manager::~ast_manager() { } it = m_plugins.begin(); for (; it != end; ++it) { - if (*it) + if (*it) dealloc(*it); } + m_plugins.reset(); while (!m_ast_table.empty()) { DEBUG_CODE(std::cout << "ast_manager LEAKED: " << m_ast_table.size() << std::endl;); ptr_vector roots; From 4d9aadde351bb57c62db68e19f1d686a07260d0a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 31 Aug 2016 16:15:36 +0800 Subject: [PATCH 13/15] updated consequence finder to fix bug in processing enumeration types Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 1 + src/smt/smt_consequences.cpp | 147 ++++++++++++++++++++--------------- src/smt/smt_context.h | 1 + src/smt/theory_seq.cpp | 26 ++++++- src/smt/theory_seq.h | 2 + 5 files changed, 112 insertions(+), 65 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 418ccc58c..b6c3384e7 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -415,6 +415,7 @@ extern "C" { return; } mk_c(c)->m().dec_ref(to_ast(a)); + Z3_CATCH; } diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 922156d46..e71abf39d 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "smt_context.h" #include "ast_util.h" +#include "datatype_decl_plugin.h" namespace smt { @@ -31,74 +32,85 @@ namespace smt { return mk_and(premises); } - void context::extract_fixed_consequences(unsigned start, obj_map& vars, uint_set const& assumptions, expr_ref_vector& conseq) { + void context::extract_fixed_consequences(literal lit, obj_map& vars, uint_set const& assumptions, expr_ref_vector& conseq) { ast_manager& m = m_manager; + datatype_util dt(m); + expr* e1, *e2; + expr_ref fml(m); + if (lit == true_literal) return; + expr* e = bool_var2expr(lit.var()); + uint_set s; + if (assumptions.contains(lit.var())) { + s.insert(lit.var()); + } + else { + b_justification js = get_justification(lit.var()); + switch (js.get_kind()) { + case b_justification::CLAUSE: { + clause * cls = js.get_clause(); + unsigned num_lits = cls->get_num_literals(); + for (unsigned j = 0; j < num_lits; ++j) { + literal lit2 = cls->get_literal(j); + if (lit2.var() != lit.var()) { + s |= m_antecedents.find(lit2.var()); + } + } + break; + } + case b_justification::BIN_CLAUSE: { + s |= m_antecedents.find(js.get_literal().var()); + break; + } + case b_justification::AXIOM: { + break; + } + case b_justification::JUSTIFICATION: { + literal_vector literals; + m_conflict_resolution->justification2literals(js.get_justification(), literals); + for (unsigned j = 0; j < literals.size(); ++j) { + s |= m_antecedents.find(literals[j].var()); + } + break; + } + } + } + m_antecedents.insert(lit.var(), s); + TRACE("context", display_literal_verbose(tout, lit); tout << " " << s << "\n";); + bool found = false; + if (vars.contains(e)) { + found = true; + fml = lit.sign() ? m.mk_not(e) : e; + vars.erase(e); + } + else if (!lit.sign() && m.is_eq(e, e1, e2)) { + if (vars.contains(e2)) { + std::swap(e1, e2); + } + if (vars.contains(e1) && m.is_value(e2)) { + found = true; + fml = e; + vars.erase(e1); + } + } + else if (!lit.sign() && is_app(e) && dt.is_recognizer(to_app(e)->get_decl())) { + if (vars.contains(to_app(e)->get_arg(0))) { + found = true; + fml = m.mk_eq(to_app(e)->get_arg(0), m.mk_const(dt.get_recognizer_constructor(to_app(e)->get_decl()))); + vars.erase(to_app(e)->get_arg(0)); + } + } + if (found) { + fml = m.mk_implies(antecedent2fml(s), fml); + conseq.push_back(fml); + } + } + + void context::extract_fixed_consequences(unsigned start, obj_map& vars, uint_set const& assumptions, expr_ref_vector& conseq) { pop_to_search_lvl(); literal_vector const& lits = assigned_literals(); unsigned sz = lits.size(); - expr* e1, *e2; - expr_ref fml(m); for (unsigned i = start; i < sz; ++i) { - literal lit = lits[i]; - if (lit == true_literal) continue; - expr* e = bool_var2expr(lit.var()); - uint_set s; - if (assumptions.contains(lit.var())) { - s.insert(lit.var()); - } - else { - b_justification js = get_justification(lit.var()); - switch (js.get_kind()) { - case b_justification::CLAUSE: { - clause * cls = js.get_clause(); - unsigned num_lits = cls->get_num_literals(); - for (unsigned j = 0; j < num_lits; ++j) { - literal lit2 = cls->get_literal(j); - if (lit2.var() != lit.var()) { - s |= m_antecedents.find(lit2.var()); - } - } - break; - } - case b_justification::BIN_CLAUSE: { - s |= m_antecedents.find(js.get_literal().var()); - break; - } - case b_justification::AXIOM: { - break; - } - case b_justification::JUSTIFICATION: { - literal_vector literals; - m_conflict_resolution->justification2literals(js.get_justification(), literals); - for (unsigned j = 0; j < literals.size(); ++j) { - s |= m_antecedents.find(literals[j].var()); - } - break; - } - } - } - m_antecedents.insert(lit.var(), s); - TRACE("context", display_literal_verbose(tout, lit); tout << " " << s << "\n";); - bool found = false; - if (vars.contains(e)) { - found = true; - fml = lit.sign()?m.mk_not(e):e; - vars.erase(e); - } - else if (!lit.sign() && m.is_eq(e, e1, e2)) { - if (vars.contains(e2)) { - std::swap(e1, e2); - } - if (vars.contains(e1) && m.is_value(e2)) { - found = true; - fml = e; - vars.erase(e1); - } - } - if (found) { - fml = m.mk_implies(antecedent2fml(s), fml); - conseq.push_back(fml); - } + extract_fixed_consequences(lits[i], vars, assumptions, conseq); } } @@ -240,6 +252,7 @@ namespace smt { lit = literal(get_bool_var(e), m.is_true(val)); } else { + TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n";); eq = mk_eq_atom(e, val); internalize_formula(eq, false); lit = literal(get_bool_var(eq), true); @@ -259,9 +272,10 @@ namespace smt { } break; } - if (get_assignment(lit) == l_true) { + if (is_sat == l_true && get_assignment(lit) == l_true) { var2val.erase(e); unfixed.push_back(e); + TRACE("context", tout << mk_pp(e, m) << " is unfixed\n";); } else if (get_assign_level(lit) > get_search_level()) { TRACE("context", tout << "Retry fixing: " << mk_pp(e, m) << "\n";); @@ -305,10 +319,15 @@ namespace smt { << " unfixed-deleted: " << num_unfixed << ")\n";); } + TRACE("context", tout << "finishing " << mk_pp(e, m) << "\n";); if (var2val.contains(e)) { TRACE("context", tout << "Fixed value to " << mk_pp(e, m) << " was not processed\n";); expr_ref fml(m); fml = m.mk_eq(e, var2val.find(e)); + if (!m_antecedents.contains(lit.var())) + { + extract_fixed_consequences(lit, var2val, _assumptions, conseq); + } fml = m.mk_implies(antecedent2fml(m_antecedents[lit.var()]), fml); conseq.push_back(fml); var2val.erase(e); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 48f6004e9..1a5952305 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1345,6 +1345,7 @@ namespace smt { vector b2v, ast_translation& tr); u_map m_antecedents; + void extract_fixed_consequences(literal lit, obj_map& var2val, uint_set const& assumptions, expr_ref_vector& conseq); void extract_fixed_consequences(unsigned idx, obj_map& var2val, uint_set const& assumptions, expr_ref_vector& conseq); unsigned delete_unfixed(obj_map& var2val, expr_ref_vector& unfixed); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 6a2208ad4..5b862b2d1 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -249,6 +249,7 @@ final_check_status theory_seq::final_check_eh() { } m_new_propagation = false; TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n");); + TRACE("seq_verbose", get_context().display(tout);); if (simplify_and_solve_eqs()) { ++m_stats.m_solve_eqs; TRACE("seq", tout << ">>solve_eqs\n";); @@ -1009,6 +1010,17 @@ bool theory_seq::is_nth(expr* e) const { return is_skolem(m_nth, e); } +bool theory_seq::is_nth(expr* e, expr*& e1, expr*& e2) const { + if (is_nth(e)) { + e1 = to_app(e)->get_arg(0); + e2 = to_app(e)->get_arg(1); + return true; + } + else { + return false; + } +} + bool theory_seq::is_tail(expr* e, expr*& s, unsigned& idx) const { rational r; return @@ -1038,6 +1050,10 @@ expr_ref theory_seq::mk_nth(expr* s, expr* idx) { return mk_skolem(m_nth, s, idx, 0, char_sort); } +expr_ref theory_seq::mk_sk_ite(expr* c, expr* t, expr* e) { + return mk_skolem(symbol("seq.if"), c, t, e, m.get_sort(t)); +} + expr_ref theory_seq::mk_last(expr* s) { zstring str; if (m_util.str.is_string(s, str) && str.length() > 0) { @@ -1133,7 +1149,7 @@ bool theory_seq::check_extensionality() { continue; } TRACE("seq", tout << m_lhs << " = " << m_rhs << "\n";); - ctx.assume_eq(n1, n2); + ctx.assume_eq(n1, n2); return false; } } @@ -2668,6 +2684,13 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { } else if (m.is_ite(e, e1, e2, e3)) { literal lit(mk_literal(e1)); +#if 0 + expr_ref sk_ite = mk_sk_ite(e1, e2, e3); + add_axiom(~lit, mk_eq(e2, sk_ite, false)); + add_axiom( lit, mk_eq(e3, sk_ite, false)); + result = sk_ite; + +#else switch (ctx.get_assignment(lit)) { case l_true: deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit))); @@ -2684,6 +2707,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { tout << lit << "@ level: " << ctx.get_scope_level() << "\n";); break; } +#endif } else if (m_util.str.is_itos(e, e1)) { rational val; diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 187573623..21955bf30 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -449,10 +449,12 @@ namespace smt { bool is_var(expr* b); bool add_solution(expr* l, expr* r, dependency* dep); bool is_nth(expr* a) const; + bool is_nth(expr* a, expr*& e1, expr*& e2) const; bool is_tail(expr* a, expr*& s, unsigned& idx) const; bool is_eq(expr* e, expr*& a, expr*& b) const; bool is_pre(expr* e, expr*& s, expr*& i); bool is_post(expr* e, expr*& s, expr*& i); + expr_ref mk_sk_ite(expr* c, expr* t, expr* f); expr_ref mk_nth(expr* s, expr* idx); expr_ref mk_last(expr* e); expr_ref mk_first(expr* e); From c746d46d80ecf1ab6c383ab173be226528762539 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Sep 2016 16:21:23 +0800 Subject: [PATCH 14/15] add validation code, fix bugs in consequence finder Signed-off-by: Nikolaj Bjorner --- src/smt/smt_conflict_resolution.cpp | 1 - src/smt/smt_consequences.cpp | 76 +++++++++++++++++++++++++---- src/smt/smt_context.h | 3 ++ 3 files changed, 70 insertions(+), 10 deletions(-) diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 6907d6f37..8fb8f9f70 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -403,7 +403,6 @@ namespace smt { // the previous levels were already inconsistent, or the inconsistency was // triggered by an axiom or justification proof wrapper, this two kinds // of justification are considered level zero. - if (m_conflict_lvl <= m_ctx.get_search_level()) { TRACE("conflict", tout << "problem is unsat\n";); if (m_manager.proofs_enabled()) diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index e71abf39d..8aa83e407 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -107,11 +107,13 @@ namespace smt { void context::extract_fixed_consequences(unsigned start, obj_map& vars, uint_set const& assumptions, expr_ref_vector& conseq) { pop_to_search_lvl(); + SASSERT(!inconsistent()); literal_vector const& lits = assigned_literals(); unsigned sz = lits.size(); for (unsigned i = start; i < sz; ++i) { extract_fixed_consequences(lits[i], vars, assumptions, conseq); } + SASSERT(!inconsistent()); } unsigned context::delete_unfixed(obj_map& var2val, expr_ref_vector& unfixed) { @@ -160,6 +162,7 @@ namespace smt { // Extract equalities that are congruent at the search level. // unsigned context::extract_fixed_eqs(obj_map& var2val, expr_ref_vector& conseq) { + TRACE("context", tout << "extract fixed consequences\n";); ast_manager& m = m_manager; ptr_vector to_delete; expr_ref fml(m), eq(m); @@ -187,9 +190,10 @@ namespace smt { } eq = mk_eq_atom(k, v); internalize_formula(eq, false); - literal lit(get_bool_var(eq), true); + literal lit(get_bool_var(eq), false); literals.push_back(lit); mk_clause(literals.size(), literals.c_ptr(), 0); + TRACE("context", display_literals_verbose(tout, literals.size(), literals.c_ptr());); } } for (unsigned i = 0; i < to_delete.size(); ++i) { @@ -247,6 +251,9 @@ namespace smt { expr* val = it->m_value; push_scope(); + TRACE("context", tout << "scope level: " << get_scope_level() << "\n";); + SASSERT(!inconsistent()); + literal lit; if (m.is_bool(e)) { lit = literal(get_bool_var(e), m.is_true(val)); @@ -277,19 +284,29 @@ namespace smt { unfixed.push_back(e); TRACE("context", tout << mk_pp(e, m) << " is unfixed\n";); } - else if (get_assign_level(lit) > get_search_level()) { + else if (is_sat == l_true && get_assign_level(lit) > get_search_level()) { TRACE("context", tout << "Retry fixing: " << mk_pp(e, m) << "\n";); - pop_to_search_lvl(); + extract_fixed_consequences(num_units, var2val, _assumptions, conseq); ++num_reiterations; continue; } else { - TRACE("context", tout << "Fixed: " << mk_pp(e, m) << "\n";); + // The state can be labeled as inconsistent when the implied consequence does + // not depend on assumptions, then the conflict level sits at the search level + // which causes the conflict resolver to decide that the state is unsat. + if (l_false == is_sat) { + SASSERT(inconsistent()); + m_conflict = null_b_justification; + m_not_l = null_literal; + } + TRACE("context", tout << "Fixed: " << mk_pp(e, m) << " " << is_sat << "\n"; + if (is_sat == l_false) display(tout);); + } ++num_iterations; bool apply_slow_pass = model_threshold <= num_iterations || num_iterations <= 2; - if (apply_slow_pass) { + if (apply_slow_pass && is_sat == l_true) { num_unfixed += delete_unfixed(var2val, unfixed); // The next time we check the model is after 1.5 additional iterations. model_threshold *= 3; @@ -320,14 +337,14 @@ namespace smt { << ")\n";); } TRACE("context", tout << "finishing " << mk_pp(e, m) << "\n";); + SASSERT(!inconsistent()); if (var2val.contains(e)) { TRACE("context", tout << "Fixed value to " << mk_pp(e, m) << " was not processed\n";); expr_ref fml(m); fml = m.mk_eq(e, var2val.find(e)); - if (!m_antecedents.contains(lit.var())) - { - extract_fixed_consequences(lit, var2val, _assumptions, conseq); - } + if (!m_antecedents.contains(lit.var())) { + extract_fixed_consequences(lit, var2val, _assumptions, conseq); + } fml = m.mk_implies(antecedent2fml(m_antecedents[lit.var()]), fml); conseq.push_back(fml); var2val.erase(e); @@ -335,7 +352,48 @@ namespace smt { } } end_search(); + DEBUG_CODE(validate_consequences(assumptions, vars, conseq, unfixed);); return l_true; } + void context::validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, + expr_ref_vector const& conseq, expr_ref_vector const& unfixed) { + ast_manager& m = m_manager; + expr_ref tmp(m); + SASSERT(!inconsistent()); + for (unsigned i = 0; i < conseq.size(); ++i) { + push(); + for (unsigned j = 0; j < assumptions.size(); ++j) { + assert_expr(assumptions[j]); + } + TRACE("context", tout << "checking: " << mk_pp(conseq[i], m) << "\n";); + tmp = m.mk_not(conseq[i]); + assert_expr(tmp); + lbool is_sat = check(); + SASSERT(is_sat != l_true); + pop(1); + } + model_ref mdl; + for (unsigned i = 0; i < unfixed.size(); ++i) { + push(); + for (unsigned j = 0; j < assumptions.size(); ++j) { + assert_expr(assumptions[j]); + } + TRACE("context", tout << "checking unfixed: " << mk_pp(unfixed[i], m) << "\n";); + lbool is_sat = check(); + SASSERT(is_sat != l_false); + if (is_sat == l_true) { + get_model(mdl); + mdl->eval(unfixed[i], tmp); + if (m.is_value(tmp)) { + tmp = m.mk_not(m.mk_eq(unfixed[i], tmp)); + assert_expr(tmp); + is_sat = check(); + SASSERT(is_sat != l_false); + } + } + pop(1); + } + } + } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 1a5952305..69388e586 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1354,6 +1354,9 @@ namespace smt { expr_ref antecedent2fml(uint_set const& ante); + void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, + expr_ref_vector const& conseq, expr_ref_vector const& unfixed); + public: context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref()); From dc48008d4654e0d1c966519c18f0d48f1761770b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Sep 2016 11:00:40 +0800 Subject: [PATCH 15/15] fixestoconsequences Signed-off-by: Nikolaj Bjorner --- src/smt/smt_consequences.cpp | 106 +++++++++++++++++++++++++++++++---- src/smt/smt_context.cpp | 9 ++- src/smt/smt_context.h | 2 +- 3 files changed, 103 insertions(+), 14 deletions(-) diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 8aa83e407..9e026760c 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -19,6 +19,7 @@ Revision History: #include "smt_context.h" #include "ast_util.h" #include "datatype_decl_plugin.h" +#include "model_pp.h" namespace smt { @@ -32,6 +33,15 @@ namespace smt { return mk_and(premises); } + // + // The literal lit is assigned at the search level, so it follows from the assumptions. + // We retrieve the set of assumptions it depends on in the set 's'. + // The map m_antecedents contains the association from these literals to the assumptions they depend on. + // We then examine the contents of the literal lit and augment the set of consequences in one of the following cases: + // - e is a propositional atom and it is one of the variables that is to be fixed. + // - e is an equality between a variable and value that is to be fixed. + // - e is a data-type recognizer of a variable that is to be fixed. + // void context::extract_fixed_consequences(literal lit, obj_map& vars, uint_set const& assumptions, expr_ref_vector& conseq) { ast_manager& m = m_manager; datatype_util dt(m); @@ -48,6 +58,7 @@ namespace smt { switch (js.get_kind()) { case b_justification::CLAUSE: { clause * cls = js.get_clause(); + if (!cls) break; unsigned num_lits = cls->get_num_literals(); for (unsigned j = 0; j < num_lits; ++j) { literal lit2 = cls->get_literal(j); @@ -115,6 +126,18 @@ namespace smt { } SASSERT(!inconsistent()); } + + + // + // The assignment stack is assumed consistent. + // For each Boolean variable, we check if there is a literal assigned to the + // opposite value of the reference model, and for non-Boolean variables we + // check if the current state forces the variable to be distinct from the reference value. + // + // For yet to be determined Boolean variables we furthermore force the phase to be opposite + // to the reference value in the attempt to let the sat engine emerge with a model that + // rules out as many non-fixed variables as possible. + // unsigned context::delete_unfixed(obj_map& var2val, expr_ref_vector& unfixed) { ast_manager& m = m_manager; @@ -158,8 +181,12 @@ namespace smt { return to_delete.size(); } +#define are_equal(v, k) (e_internalized(k) && e_internalized(v) && get_enode(k)->get_root() == get_enode(v)->get_root()) + // // Extract equalities that are congruent at the search level. + // Add a clause to short-circuit the congruence justifications for + // next rounds. // unsigned context::extract_fixed_eqs(obj_map& var2val, expr_ref_vector& conseq) { TRACE("context", tout << "extract fixed consequences\n";); @@ -170,8 +197,7 @@ namespace smt { for (; it != end; ++it) { expr* k = it->m_key; expr* v = it->m_value; - if (!m.is_bool(k) && e_internalized(k) && e_internalized(v) && - get_enode(k)->get_root() == get_enode(v)->get_root()) { + if (!m.is_bool(k) && are_equal(k, v)) { literal_vector literals; m_conflict_resolution->eq2literals(get_enode(v), get_enode(k), literals); uint_set s; @@ -208,6 +234,7 @@ namespace smt { expr_ref_vector& unfixed) { m_antecedents.reset(); + pop_to_base_lvl(); lbool is_sat = check(assumptions.size(), assumptions.c_ptr()); if (is_sat != l_true) { return is_sat; @@ -223,6 +250,7 @@ namespace smt { expr_ref_vector trail(m); model_evaluator eval(*mdl.get()); expr_ref val(m); + TRACE("context", model_pp(tout, *mdl);); for (unsigned i = 0; i < vars.size(); ++i) { eval(vars[i], val); if (m.is_value(val)) { @@ -249,23 +277,39 @@ namespace smt { obj_map::iterator it = var2val.begin(); expr* e = it->m_key; expr* val = it->m_value; - push_scope(); TRACE("context", tout << "scope level: " << get_scope_level() << "\n";); SASSERT(!inconsistent()); + // + // The current variable is checked to be a backbone + // We add the negation of the reference assignment to the variable. + // If the variable is a Boolean, it means adding literal that has + // the opposite value of the current reference model. + // If the variable is a non-Boolean, it means adding a disequality. + // literal lit; if (m.is_bool(e)) { lit = literal(get_bool_var(e), m.is_true(val)); } else { - TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n";); eq = mk_eq_atom(e, val); internalize_formula(eq, false); lit = literal(get_bool_var(eq), true); + TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n"; + display_literal_verbose(tout, lit); tout << "\n"; + tout << "Equal: " << are_equal(e, val) << "\n";); } + mark_as_relevant(lit); + push_scope(); assign(lit, b_justification::mk_axiom(), true); flet l(m_searching, true); + + // + // We check if the current assignment stack can be extended to a + // satisfying assignment. bounded search may decide to restart, + // in which case it returns l_undef and clears search failure. + // while (true) { is_sat = bounded_search(); TRACE("context", tout << "search result: " << is_sat << "\n";); @@ -279,21 +323,41 @@ namespace smt { } break; } - if (is_sat == l_true && get_assignment(lit) == l_true) { + // + // If the state is satisfiable with the current variable assigned to + // a different value from the reference model, it is unfixed. + // + // If it is assigned above the search level we can't conclude anything + // about its value. + // extract_fixed_consequences pops the assignment stack to the search level + // so this sets up the state to retry finding fixed values. + // + // Otherwise, the variable is fixed. + // - it is either assigned at the search level to l_false, or + // - the state is l_false, which means that the variable is fixed by + // the background constraints (and does not depend on assumptions). + // + if (is_sat == l_true && get_assignment(lit) == l_true && is_relevant(lit)) { var2val.erase(e); unfixed.push_back(e); - TRACE("context", tout << mk_pp(e, m) << " is unfixed\n";); + SASSERT(!are_equal(e, val)); + TRACE("context", tout << mk_pp(e, m) << " is unfixed\n"; + display_literal_verbose(tout, lit); tout << "\n"; + tout << "relevant: " << is_relevant(lit) << "\n"; + display(tout);); } - else if (is_sat == l_true && get_assign_level(lit) > get_search_level()) { + else if (is_sat == l_true && (get_assign_level(lit) > get_search_level() || !is_relevant(lit))) { TRACE("context", tout << "Retry fixing: " << mk_pp(e, m) << "\n";); extract_fixed_consequences(num_units, var2val, _assumptions, conseq); ++num_reiterations; continue; } else { + // // The state can be labeled as inconsistent when the implied consequence does // not depend on assumptions, then the conflict level sits at the search level // which causes the conflict resolver to decide that the state is unsat. + // if (l_false == is_sat) { SASSERT(inconsistent()); m_conflict = null_b_justification; @@ -305,6 +369,11 @@ namespace smt { } ++num_iterations; + // + // Check the slow pass: it retrieves an updated model and checks if the + // values in the updated model differ from the values in the reference + // model. + // bool apply_slow_pass = model_threshold <= num_iterations || num_iterations <= 2; if (apply_slow_pass && is_sat == l_true) { num_unfixed += delete_unfixed(var2val, unfixed); @@ -312,11 +381,20 @@ namespace smt { model_threshold *= 3; model_threshold /= 2; } - // repeat until we either have a model with negated literal or - // the literal is implied at base. + // + // Walk the assignment stack at level 1 for learned consequences. + // The current literal should be assigned at the search level unless + // the state is is_sat == l_true and the assignment to lit is l_true. + // This condition is checked above. + // extract_fixed_consequences(num_units, var2val, _assumptions, conseq); num_units = assigned_literals().size(); + + // + // Fixed equalities can be extracted by walking all variables and checking + // if the congruence roots are equal at the search level. + // if (apply_slow_pass) { num_fixed_eqs += extract_fixed_eqs(var2val, conseq); IF_VERBOSE(1, verbose_stream() << "(get-consequences" @@ -338,6 +416,11 @@ namespace smt { } TRACE("context", tout << "finishing " << mk_pp(e, m) << "\n";); SASSERT(!inconsistent()); + + // + // This becomes unnecessary when the fixed consequence are + // completely extracted. + // if (var2val.contains(e)) { TRACE("context", tout << "Fixed value to " << mk_pp(e, m) << " was not processed\n";); expr_ref fml(m); @@ -348,7 +431,6 @@ namespace smt { fml = m.mk_implies(antecedent2fml(m_antecedents[lit.var()]), fml); conseq.push_back(fml); var2val.erase(e); - SASSERT(get_assignment(lit) == l_false); } } end_search(); @@ -356,6 +438,10 @@ namespace smt { return l_true; } + // + // Validate, in a slow pass, that the current consequences are correctly + // extracted. + // void context::validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector const& conseq, expr_ref_vector const& unfixed) { ast_manager& m = m_manager; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c692173e6..0b3147d6b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1094,7 +1094,7 @@ namespace smt { \brief This method is invoked when a new disequality is asserted. The disequality is propagated to the theories. */ - void context::add_diseq(enode * n1, enode * n2) { + bool context::add_diseq(enode * n1, enode * n2) { enode * r1 = n1->get_root(); enode * r2 = n2->get_root(); TRACE("add_diseq", tout << "assigning: #" << n1->get_owner_id() << " != #" << n2->get_owner_id() << "\n"; @@ -1111,7 +1111,7 @@ namespace smt { if (r1 == r2) { TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";); - return; // context is inconsistent + return false; // context is inconsistent } // Propagate disequalities to theories @@ -1145,6 +1145,7 @@ namespace smt { l1 = l1->get_next(); } } + return true; } /** @@ -1400,7 +1401,9 @@ namespace smt { } else { TRACE("add_diseq", display_eq_detail(tout, bool_var2enode(v));); - add_diseq(get_enode(lhs), get_enode(rhs)); + if (!add_diseq(get_enode(lhs), get_enode(rhs)) && !inconsistent()) { + set_conflict(b_justification(mk_justification(eq_propagation_justification(get_enode(lhs), get_enode(rhs)))), ~l); + } } } else if (d.is_theory_atom()) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 69388e586..79b969118 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -942,7 +942,7 @@ namespace smt { push_eq(n1, n2, eq_justification::mk_cg(used_commutativity)); } - void add_diseq(enode * n1, enode * n2); + bool add_diseq(enode * n1, enode * n2); void assign_quantifier(quantifier * q);