From 6b258578f9b20164d7dc203392a775515c5414de Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Dec 2017 02:38:45 -0800 Subject: [PATCH] fix uninitialized variable m_gc_burst in config, have cuber accept and receive optional vector of variables indicating splits and global autarky as output Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 2 +- src/api/api_solver.cpp | 17 +++++++-- src/api/c++/z3++.h | 44 ++++++++++++++++------- src/api/dotnet/Solver.cs | 14 ++++++-- src/api/python/z3/z3.py | 15 +++++--- src/api/z3_api.h | 11 ++++-- src/sat/sat_asymm_branch.cpp | 2 +- src/sat/sat_config.cpp | 1 + src/sat/sat_elim_eqs.cpp | 4 +-- src/sat/sat_lookahead.cpp | 50 ++++++--------------------- src/sat/sat_lookahead.h | 5 ++- src/sat/sat_solver.cpp | 7 +--- src/sat/sat_solver.h | 4 +-- src/sat/sat_solver/inc_sat_solver.cpp | 43 ++++++++++++----------- src/solver/solver.h | 2 +- 15 files changed, 121 insertions(+), 100 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 732a89099..6fa4e809e 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -707,7 +707,7 @@ void tactic_example7() { std::cout << s.check() << "\n"; model m = s.get_model(); std::cout << "model for subgoal:\n" << m << "\n"; - std::cout << "model for original goal:\n" << r.convert_model(m) << "\n"; + std::cout << "model for original goal:\n" << subgoal.convert_model(m) << "\n"; } void tactic_example8() { diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 9e7223aee..48ce6d22d 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -553,11 +553,19 @@ extern "C" { Z3_CATCH_RETURN(Z3_L_UNDEF); } - Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, unsigned cutoff) { + Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vs, unsigned cutoff) { Z3_TRY; - LOG_Z3_solver_cube(c, s, cutoff); + LOG_Z3_solver_cube(c, s, vs, cutoff); ast_manager& m = mk_c(c)->m(); expr_ref_vector result(m), vars(m); + for (ast* a : to_ast_vector_ref(vs)) { + if (!is_expr(a)) { + SET_ERROR_CODE(Z3_INVALID_USAGE); + } + else { + vars.push_back(to_expr(a)); + } + } unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false); @@ -580,7 +588,10 @@ extern "C" { for (expr* e : result) { v->m_ast_vector.push_back(e); } - // TBD: save return variables from vars into variable ast-vector. + to_ast_vector_ref(vs).reset(); + for (expr* a : vars) { + to_ast_vector_ref(vs).push_back(a); + } RETURN_Z3(of_ast_vector(v)); Z3_CATCH_RETURN(0); } diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 428f210ee..270a98ca9 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1999,18 +1999,23 @@ namespace z3 { param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); } - expr_vector cube(unsigned cutoff) { Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, cutoff); check_error(); return expr_vector(ctx(), r); } + expr_vector cube(expr_vector& vars, unsigned cutoff) { + Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff); + check_error(); + return expr_vector(ctx(), r); + } class cube_iterator { - solver& m_solver; - unsigned& m_cutoff; - expr_vector m_cube; - bool m_end; - bool m_empty; + solver& m_solver; + unsigned& m_cutoff; + expr_vector& m_vars; + expr_vector m_cube; + bool m_end; + bool m_empty; void inc() { assert(!m_end && !m_empty); - m_cube = m_solver.cube(m_cutoff); + m_cube = m_solver.cube(m_vars, m_cutoff); m_cutoff = 0xFFFFFFFF; if (m_cube.size() == 1 && m_cube[0].is_false()) { m_cube = z3::expr_vector(m_solver.ctx()); @@ -2021,9 +2026,10 @@ namespace z3 { } } public: - cube_iterator(solver& s, unsigned& cutoff, bool end): + cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end): m_solver(s), m_cutoff(cutoff), + m_vars(vars), m_cube(s.ctx()), m_end(end), m_empty(false) { @@ -2056,20 +2062,32 @@ namespace z3 { }; class cube_generator { - solver& m_solver; - unsigned m_cutoff; + solver& m_solver; + unsigned m_cutoff; + expr_vector m_default_vars; + expr_vector& m_vars; public: cube_generator(solver& s): m_solver(s), - m_cutoff(0xFFFFFFFF) + m_cutoff(0xFFFFFFFF), + m_default_vars(s.ctx()), + m_vars(m_default_vars) {} - cube_iterator begin() { return cube_iterator(m_solver, m_cutoff, false); } - cube_iterator end() { return cube_iterator(m_solver, m_cutoff, true); } + cube_generator(solver& s, expr_vector& vars): + m_solver(s), + m_cutoff(0xFFFFFFFF), + m_default_vars(s.ctx()), + m_vars(vars) + {} + + cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); } + cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); } void set_cutoff(unsigned c) { m_cutoff = c; } }; cube_generator cubes() { return cube_generator(*this); } + cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); } }; inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; } diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index e136516e4..f67a298bb 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -404,6 +404,11 @@ namespace Microsoft.Z3 /// Backtrack level that can be adjusted by conquer process /// public uint BacktrackLevel { get; set; } + + /// + /// Variables available and returned by the cuber. + /// + public BoolExpr[] CubeVariables { get; set; } /// @@ -411,16 +416,21 @@ namespace Microsoft.Z3 /// public IEnumerable Cube() { + ASTVector cv = new ASTVector(Context); + if (CubeVariables != null) + foreach (var b in CubeVariables) cv.Push(b); + while (true) { var lvl = BacktrackLevel; BacktrackLevel = uint.MaxValue; - ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, lvl)); + ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, cv.NativeObject, lvl)); var v = r.ToBoolExprArray(); + CubeVariables = cv.ToBoolExprArray(); if (v.Length == 1 && v[0].IsFalse) { break; } yield return v; - if (v.Length == 0) { + if (v.Length == 0) { break; } } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index f15386a93..e16459fda 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6313,18 +6313,25 @@ class Solver(Z3PPObject): consequences = [ consequences[i] for i in range(sz) ] return CheckSatResult(r), consequences - def cube(self): + def cube(self, vars = None): """Get set of cubes""" + self.cube_vs = AstVector(None, self.ctx) + if vars is not None: + for v in vars: + self.cube_vs.push(v) while True: lvl = self.backtrack_level self.backtrack_level = 4000000000 - r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, lvl), self.ctx) + r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx) if (len(r) == 1 and is_false(r[0])): - return - yield r + return + yield r if (len(r) == 0): return + def cube_vars(self): + return self.cube_vs + def proof(self): """Return a proof for the last `check()`. Proof construction must be enabled.""" return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index b212912b9..99d6021ef 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6230,13 +6230,20 @@ extern "C" { The number of (non-constant) cubes is by default 1. For the sat solver cubing is controlled using parameters sat.lookahead.cube.cutoff and sat.lookahead.cube.fraction. + The third argument is a vector of variables that may be used for cubing. + The contents of the vector is only used in the first call. The initial list of variables + is used in subsequent calls until it returns the unsatisfiable cube. + The vector is modified to contain a set of Autarky variables that occor in clauses that + are affected by the (last literal in the) cube. These variables could be used by a different + cuber (on a different solver object) for further recursive cubing. + The last argument is a backtracking level. It instructs the cube process to backtrack below the indicated level for the next cube. - def_API('Z3_solver_cube', AST_VECTOR, (_in(CONTEXT), _in(SOLVER), _in(UINT))) + def_API('Z3_solver_cube', AST_VECTOR, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(UINT))) */ - Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, unsigned backtrack_level); + Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level); /** \brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index e3543ff0f..0d0e3a682 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -72,7 +72,7 @@ namespace sat { unsigned elim = m_elim_literals; if (big) big->init_big(s, true); process(big, s.m_clauses); - process(big, s.m_learned); + if (big) process(big, s.m_learned); s.propagate(false); if (s.m_inconsistent) break; diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 361e15d91..09610a3a7 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -136,6 +136,7 @@ namespace sat { m_gc_increment = p.gc_increment(); m_gc_small_lbd = p.gc_small_lbd(); m_gc_k = std::min(255u, p.gc_k()); + m_gc_burst = p.gc_burst(); m_minimize_lemmas = p.minimize_lemmas(); m_core_minimize = p.core_minimize(); diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index a8eb09278..582194bc2 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -182,8 +182,8 @@ namespace sat { literal l(v, false); literal r = roots[v]; SASSERT(v != r.var()); - if (m_solver.is_external(v)) { - m_solver.set_root(l, r); + bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r); + if (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok)) { // cannot really eliminate v, since we have to notify extension of future assignments m_solver.mk_bin_clause(~l, r, false); m_solver.mk_bin_clause(l, ~r, false); diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index fd4f63c1e..9fc818014 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -338,7 +338,7 @@ namespace sat { } TRACE("sat", display_candidates(tout << "sum: " << sum << "\n");); if (skip_candidates > 0) { - IF_VERBOSE(0, verbose_stream() << "candidates: " << m_candidates.size() << " skip: " << skip_candidates << "\n";); + IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :candidates " << m_candidates.size() << " :skipped " << skip_candidates << ")\n";); } return sum; } @@ -2049,15 +2049,15 @@ namespace sat { return h; } - lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) { + lbool lookahead::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) { scoped_ext _scoped_ext(*this); lits.reset(); - m_select_lookahead_vars.reset(); - for (auto v : vars) { - m_select_lookahead_vars.insert(v); - } bool is_first = m_cube_state.m_first; if (is_first) { + m_select_lookahead_vars.reset(); + for (auto v : vars) { + m_select_lookahead_vars.insert(v); + } init_search(); m_model.reset(); m_cube_state.m_first = false; @@ -2109,6 +2109,8 @@ namespace sat { #else lits.append(m_cube_state.m_cube); #endif + vars.reset(); + for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v); backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision); return l_undef; } @@ -2124,6 +2126,8 @@ namespace sat { continue; } if (lit == null_literal) { + vars.reset(); + for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v); return l_true; } TRACE("sat", tout << "choose: " << lit << " cube: " << m_cube_state.m_cube << "\n";); @@ -2246,40 +2250,6 @@ namespace sat { return l; } - - literal lookahead::select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars) { - IF_VERBOSE(1, verbose_stream() << "(sat-select " << vars.size() << ")\n";); - scoped_ext _sext(*this); - m_search_mode = lookahead_mode::searching; - scoped_level _sl(*this, c_fixed_truth); - init(); - if (inconsistent()) return null_literal; - inc_istamp(); - for (auto v : vars) { - m_select_lookahead_vars.insert(v); - } - - scoped_assumptions _sa(*this, assumptions); - literal l = choose(); - m_select_lookahead_vars.reset(); - if (inconsistent()) l = null_literal; - -#if 0 - // assign unit literals that were found during search for lookahead. - if (assumptions.empty()) { - unsigned num_assigned = 0; - for (literal lit : m_trail) { - if (!m_s.was_eliminated(lit.var()) && m_s.value(lit) != l_true) { - m_s.assign(lit, justification()); - ++num_assigned; - } - } - IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_assigned << ")\n";); - } -#endif - return l; - } - /** \brief simplify set of clauses by extracting units from a lookahead at base level. */ diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 6a7bb7449..3ebbfb7a5 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -587,15 +587,14 @@ namespace sat { /** \brief create cubes to std-out in DIMACS form. The cubes are controlled using cut-depth and cut-fraction parameters. - If cut-depth != 0, then it is used to control the depth of cuts. + If cut-depth != 0, then it is used to control thedepth of cuts. Otherwise, cut-fraction gives an adaptive threshold for creating cuts. */ - lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level); + lbool cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level); void update_cube_statistics(statistics& st); - literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars); /** \brief simplify set of clauses by extracting units from a lookahead at base level. */ diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index db6f3d356..8c7c4d421 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -861,12 +861,7 @@ namespace sat { return r; } - literal solver::select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars) { - lookahead lh(*this); - return lh.select_lookahead(assumptions, vars); - } - - lbool solver::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) { + lbool solver::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) { if (!m_cuber) { m_cuber = alloc(lookahead, *this); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 8f70086ba..bac9c4bb3 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -355,10 +355,10 @@ namespace sat { bool check_clauses(model const& m) const; bool is_assumption(bool_var v) const; - literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars); - lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level); + lbool cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level); protected: + unsigned m_conflicts_since_init; unsigned m_restarts; unsigned m_conflicts_since_restart; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 3984ec324..d731c246c 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -67,12 +67,12 @@ class inc_sat_solver : public solver { std::string m_unknown; // access formulas after they have been pre-processed and handled by the sat solver. // this allows to access the internal state of the SAT solver and carry on partial results. - bool m_internalized; // are formulas internalized? bool m_internalized_converted; // have internalized formulas been converted back expr_ref_vector m_internalized_fmls; // formulas in internalized format - typedef obj_map dep2asm_t; + + bool is_internalized() const { return m_fmls_head == m_fmls.size(); } public: inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode): m(m), @@ -84,7 +84,6 @@ public: m_map(m), m_num_scopes(0), m_unknown("no reason given"), - m_internalized(false), m_internalized_converted(false), m_internalized_fmls(m) { updt_params(p); @@ -94,7 +93,6 @@ public: bool override_incremental() const { sat_simplifier_params p(m_params); - std::cout << "override: " << p.override_incremental() << "\n"; return p.override_incremental(); } @@ -124,7 +122,6 @@ public: if (m_mc0) result->m_mc0 = m_mc0->translate(tr); //if (m_sat_mc) result->m_sat_mc = m_sat_mc->translate(tr); MN: commenting this line removes bloat // copy m_bb_rewriter? - result->m_internalized = m_internalized; result->m_internalized_converted = m_internalized_converted; return result; } @@ -188,8 +185,6 @@ public: if (r != l_true) return r; r = internalize_assumptions(sz, _assumptions.c_ptr(), dep2asm); if (r != l_true) return r; - m_internalized = true; - m_internalized_converted = false; init_reason_unknown(); try { @@ -226,11 +221,8 @@ public: m_fmls_head_lim.push_back(m_fmls_head); if (m_bb_rewriter) m_bb_rewriter->push(); m_map.push(); - m_internalized = true; - m_internalized_converted = false; } virtual void pop(unsigned n) { - m_internalized = false; if (n > m_num_scopes) { // allow inc_sat_solver to n = m_num_scopes; // take over for another solver. } @@ -264,7 +256,6 @@ public: virtual ast_manager& get_manager() const { return m; } virtual void assert_expr_core(expr * t) { - m_internalized = false; TRACE("goal2sat", tout << mk_pp(t, m) << "\n";); m_fmls.push_back(t); } @@ -306,17 +297,18 @@ public: } virtual expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) { - if (!m_internalized) { - dep2asm_t dep2asm; + if (!is_internalized()) { m_model = 0; lbool r = internalize_formulas(); if (r != l_true) return expr_ref_vector(m); - m_internalized = true; } convert_internalized(); + obj_hashtable _vs; + for (expr* v : vs) _vs.insert(v); sat::bool_var_vector vars; for (auto& kv : m_map) { - vars.push_back(kv.m_value); + if (_vs.empty() || _vs.contains(kv.m_key)) + vars.push_back(kv.m_value); } sat::literal_vector lits; lbool result = m_solver.cube(vars, lits, backtrack_level); @@ -327,7 +319,7 @@ public: } if (result == l_true) { return expr_ref_vector(m); - } + } expr_ref_vector fmls(m); expr_ref_vector lit2expr(m); lit2expr.resize(m_solver.num_vars() * 2); @@ -335,6 +327,13 @@ public: for (sat::literal l : lits) { fmls.push_back(lit2expr[l.index()].get()); } + vs.reset(); + for (sat::bool_var v : vars) { + expr* x = lit2expr[sat::literal(v, false).index()].get(); + if (x) { + vs.push_back(x); + } + } return fmls; } @@ -419,7 +418,7 @@ public: } virtual unsigned get_num_assertions() const { const_cast(this)->convert_internalized(); - if (m_internalized && m_internalized_converted) { + if (is_internalized() && m_internalized_converted) { return m_internalized_fmls.size(); } else { @@ -427,7 +426,7 @@ public: } } virtual expr * get_assertion(unsigned idx) const { - if (m_internalized && m_internalized_converted) { + if (is_internalized() && m_internalized_converted) { return m_internalized_fmls[idx]; } return m_fmls[idx]; @@ -443,7 +442,7 @@ public: const_cast(this)->convert_internalized(); if (m_cached_mc) return m_cached_mc; - if (m_internalized && m_internalized_converted) { + if (is_internalized() && m_internalized_converted) { m_cached_mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits())); m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get()); m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get()); @@ -455,7 +454,10 @@ public: } void convert_internalized() { - if (!m_internalized || m_internalized_converted) return; + if (!is_internalized() && m_fmls_head > 0) { + internalize_formulas(); + } + if (!is_internalized() || m_internalized_converted) return; sat2goal s2g; m_cached_mc = nullptr; goal g(m, false, true, false); @@ -679,6 +681,7 @@ private: if (res != l_undef) { m_fmls_head = m_fmls.size(); } + m_internalized_converted = false; return res; } diff --git a/src/solver/solver.h b/src/solver/solver.h index 7634a346e..bc6ffb0e0 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -47,7 +47,7 @@ class solver : public check_sat_result { params_ref m_params; bool m_enforce_model_conversion; public: - solver(): m_enforce_model_conversion(true) {} + solver(): m_enforce_model_conversion(false) {} virtual ~solver() {} /**