From 19fed09122a07cf177361d7012fc0682849e6374 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2023 08:35:23 -0800 Subject: [PATCH 01/22] protecting add_simplifier API against mis-use Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 34 ++++++++++++++++++++++++++++------ src/api/python/z3/z3.py | 2 -- 2 files changed, 28 insertions(+), 8 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 0a3b35aed..ca39329bb 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -233,16 +233,38 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + /** + * attach a simplifier to solver. + * This is legal when the solver is fresh, does not already have assertions (and scopes). + * To allow recycling the argument solver, we create a fresh copy of it and pass it to + * mk_simplifier_solver. + */ Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier) { Z3_TRY; LOG_Z3_solver_add_simplifier(c, solver, simplifier); - init_solver(c, solver); + solver_ref s_fresh; + if (to_solver(solver)->m_solver) { + s_fresh = to_solver_ref(solver)->translate(mk_c(c)->m(), to_solver(solver)->m_params); + } + else { + // create the solver, but hijack it for internal uses. + init_solver(c, solver); + s_fresh = to_solver(solver)->m_solver; + to_solver(solver)->m_solver = nullptr; + } + if (!s_fresh) { + SET_ERROR_CODE(Z3_INVALID_ARG, "unexpected empty solver state"); + RETURN_Z3(nullptr); + } + if (s_fresh->get_num_assertions() > 0) { + SET_ERROR_CODE(Z3_INVALID_ARG, "adding a simplifier to a solver with assertions is not allowed."); + RETURN_Z3(nullptr); + } auto simp = to_simplifier_ref(simplifier); - auto* slv = mk_simplifier_solver(to_solver_ref(solver), simp); - Z3_solver_ref* sr = alloc(Z3_solver_ref, *mk_c(c), slv); - mk_c(c)->save_object(sr); - // ?? init_solver_log(c, sr) - RETURN_Z3(of_solver(sr)); + auto* simplifier_solver = mk_simplifier_solver(s_fresh.get(), simp); + Z3_solver_ref* result = alloc(Z3_solver_ref, *mk_c(c), simplifier_solver); + mk_c(c)->save_object(result); + RETURN_Z3(of_solver(result)); Z3_CATCH_RETURN(nullptr); } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 0f7ef8999..5cb847230 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8214,8 +8214,6 @@ class Simplifier: def add(self, solver): """Return a solver that applies the simplification pre-processing specified by the simplifier""" - print(solver.solver) - print(self.simplifier) return Solver(Z3_solver_add_simplifier(self.ctx.ref(), solver.solver, self.simplifier), self.ctx) def help(self): From 0f86a00229991b7e42ba86119d4460db853106d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Jan 2023 13:53:51 -0800 Subject: [PATCH 02/22] use setter method to easier track updates to settings. --- src/math/lp/lar_core_solver.h | 2 +- src/math/lp/lar_solver.cpp | 10 +++++----- src/math/lp/lp_settings.h | 4 ++-- src/shell/lp_frontend.cpp | 2 +- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h index 0043ed23d..bcd33966f 100644 --- a/src/math/lp/lar_core_solver.h +++ b/src/math/lp/lar_core_solver.h @@ -222,7 +222,7 @@ public: m_d_x.resize(m_d_A.column_count()); pop_basis(k); m_stacked_simplex_strategy.pop(k); - settings().simplex_strategy() = m_stacked_simplex_strategy; + settings().set_simplex_strategy(m_stacked_simplex_strategy); lp_assert(m_r_solver.basis_heading_is_correct()); lp_assert(!need_to_presolve_with_double_solver() || m_d_solver.basis_heading_is_correct()); } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index f78dab119..46ed0b5a9 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -300,7 +300,7 @@ namespace lp { m_term_register.shrink(m_term_count); m_terms.resize(m_term_count); m_simplex_strategy.pop(k); - m_settings.simplex_strategy() = m_simplex_strategy; + m_settings.set_simplex_strategy(m_simplex_strategy); lp_assert(sizes_are_correct()); lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); m_usage_in_terms.pop(k); @@ -465,10 +465,10 @@ namespace lp { switch (settings().simplex_strategy()) { case simplex_strategy_enum::tableau_rows: - settings().simplex_strategy() = simplex_strategy_enum::tableau_costs; + settings().set_simplex_strategy(simplex_strategy_enum::tableau_costs); prepare_costs_for_r_solver(term); ret = maximize_term_on_tableau(term, term_max); - settings().simplex_strategy() = simplex_strategy_enum::tableau_rows; + settings().set_simplex_strategy(simplex_strategy_enum::tableau_rows); set_costs_to_zero(term); m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL); return ret; @@ -2006,10 +2006,10 @@ namespace lp { void lar_solver::decide_on_strategy_and_adjust_initial_state() { lp_assert(strategy_is_undecided()); if (m_columns_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) { - m_settings.simplex_strategy() = simplex_strategy_enum::lu; + m_settings.set_simplex_strategy(simplex_strategy_enum::lu); } else { - m_settings.simplex_strategy() = simplex_strategy_enum::tableau_rows; // todo: when to switch to tableau_costs? + m_settings.set_simplex_strategy(simplex_strategy_enum::tableau_rows); // todo: when to switch to tableau_costs? } adjust_initial_state(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index aa06cb263..2245f6f4e 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -336,8 +336,8 @@ public: return m_simplex_strategy; } - simplex_strategy_enum & simplex_strategy() { - return m_simplex_strategy; + void set_simplex_strategy(simplex_strategy_enum s) { + m_simplex_strategy = s; } bool use_lu() const { diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp index 70d2cffb1..8d6425533 100644 --- a/src/shell/lp_frontend.cpp +++ b/src/shell/lp_frontend.cpp @@ -80,7 +80,7 @@ void run_solver(smt_params_helper & params, char const * mps_file_name) { solver->settings().set_message_ostream(&std::cout); solver->settings().report_frequency = params.arith_rep_freq(); solver->settings().print_statistics = params.arith_print_stats(); - solver->settings().simplex_strategy() = lp:: simplex_strategy_enum::lu; + solver->settings().set_simplex_strategy(lp:: simplex_strategy_enum::lu); solver->find_maximal_solution(); From 682e86812927f00fe69b532fb7660018aa2de64e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2023 10:14:24 -0800 Subject: [PATCH 03/22] initialize field Signed-off-by: Nikolaj Bjorner --- src/math/lp/lp_core_solver_base.h | 2 +- src/math/lp/lp_core_solver_base_def.h | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 673ef2404..5cde4485d 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -74,9 +74,9 @@ public: vector & m_x; // a feasible solution, the fist time set in the constructor vector & m_costs; lp_settings & m_settings; + lu> * m_factorization = nullptr; vector m_y; // the buffer for yB = cb // a device that is able to solve Bx=c, xB=d, and change the basis - lu> * m_factorization; const column_namer & m_column_names; indexed_vector m_w; // the vector featuring in 24.3 of the Chvatal book vector m_d; // the vector of reduced costs diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index c1b64492b..f85de1111 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -55,7 +55,6 @@ lp_core_solver_base(static_matrix & A, m_costs(costs), m_settings(settings), m_y(m_m()), - m_factorization(nullptr), m_column_names(column_names), m_w(m_m()), m_d(m_n()), From 38d526ee4505c9109ecdc9e1f134946539c4e3a1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2023 10:18:03 -0800 Subject: [PATCH 04/22] fix warning Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/eliminate_predicates.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/ast/simplifiers/eliminate_predicates.cpp b/src/ast/simplifiers/eliminate_predicates.cpp index 2166913da..6c1eccea0 100644 --- a/src/ast/simplifiers/eliminate_predicates.cpp +++ b/src/ast/simplifiers/eliminate_predicates.cpp @@ -567,9 +567,9 @@ void eliminate_predicates::try_find_macro(clause& cl) { return false; app* x = to_app(_x); return - can_be_quasi_macro_head(x, cl.m_bound.size()) && - is_macro_safe(y) && - !occurs(x->get_decl(), y); + can_be_quasi_macro_head(x, cl.m_bound.size()) && + is_macro_safe(y) && + !occurs(x->get_decl(), y); }; if (cl.is_unit() && m.is_eq(cl.atom(0), x, y)) { @@ -592,7 +592,8 @@ void eliminate_predicates::try_find_macro(clause& cl) { } if (cl.is_unit()) { expr* body = cl.sign(0) ? m.mk_false() : m.mk_true(); - if (can_be_qdef(cl.atom(0), body)) { + expr* x = cl.atom(0); + if (can_be_qdef(x, body)) { insert_quasi_macro(to_app(x), body, cl); return; } From 30fa37e3936fc5508a34c262a68b9444368e53c8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2023 10:31:34 -0800 Subject: [PATCH 05/22] fix warnings Signed-off-by: Nikolaj Bjorner --- src/ast/recfun_decl_plugin.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index e2d480664..66544bec7 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -60,7 +60,7 @@ namespace recfun { func_decl_ref m_pred; // Date: Wed, 1 Feb 2023 11:07:47 -0800 Subject: [PATCH 06/22] fix test Signed-off-by: Nikolaj Bjorner --- src/test/lp/lp.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 547985f26..c82cdd0a4 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -1391,7 +1391,7 @@ void update_settings(argument_parser & args_parser, lp_settings& settings) { settings.set_random_seed(n); } if (get_int_from_args_parser("--simplex_strategy", args_parser, n)) { - settings.simplex_strategy() = static_cast(n); + settings.set_simplex_strategy(static_cast(n)); } } From 6c7dd4a8634886e6ede8ccfaf71bb21f2a9d6641 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2023 19:47:58 -0800 Subject: [PATCH 07/22] fix incremental pre-processing to work with assumptions/cores and consequences Signed-off-by: Nikolaj Bjorner --- src/solver/simplifier_solver.cpp | 28 ++++++++++++++++++++++++---- 1 file changed, 24 insertions(+), 4 deletions(-) diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index 219b2c46b..29021af76 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -95,10 +95,21 @@ class simplifier_solver : public solver { expr_ref_vector m_assumptions; model_converter_ref m_mc; bool m_inconsistent = false; + expr_safe_replace m_core_replace; + + void replace(expr_ref_vector& r) { + expr_ref tmp(m); + for (unsigned i = 0; i < r.size(); ++i) { + m_core_replace(r.get(i), tmp); + r[i] = tmp; + } + } void flush(expr_ref_vector& assumptions) { unsigned qhead = m_preprocess_state.qhead(); - if (qhead < m_fmls.size()) { + expr_ref_vector orig_assumptions(assumptions); + m_core_replace.reset(); + if (qhead < m_fmls.size() || !assumptions.empty()) { for (expr* a : assumptions) m_preprocess_state.freeze(a); TRACE("solver", tout << "qhead " << qhead << "\n"); @@ -107,6 +118,8 @@ class simplifier_solver : public solver { if (!m.inc()) return; m_preprocess_state.advance_qhead(); + for (unsigned i = 0; i < assumptions.size(); ++i) + m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i)); } m_mc = m_preprocess_state.model_trail().get_model_converter(); m_cached_mc = nullptr; @@ -148,6 +161,7 @@ public: m_preprocess_state(*this), m_preprocess(m, s->get_params(), m_preprocess_state), m_assumptions(m), + m_core_replace(m), m_proof(m) { if (fac) @@ -189,7 +203,7 @@ public: lbool check_sat_core(unsigned num_assumptions, expr* const* assumptions) override { expr_ref_vector _assumptions(m, num_assumptions, assumptions); flush(_assumptions); - return s->check_sat_core(num_assumptions, assumptions); + return s->check_sat_core(num_assumptions, _assumptions.data()); } void collect_statistics(statistics& st) const override { @@ -258,7 +272,7 @@ public: std::string reason_unknown() const override { return s->reason_unknown(); } void set_reason_unknown(char const* msg) override { s->set_reason_unknown(msg); } void get_labels(svector& r) override { s->get_labels(r); } - void get_unsat_core(expr_ref_vector& r) { s->get_unsat_core(r); } + void get_unsat_core(expr_ref_vector& r) { s->get_unsat_core(r); replace(r); } ast_manager& get_manager() const override { return s->get_manager(); } void reset_params(params_ref const& p) override { s->reset_params(p); } params_ref const& get_params() const override { return s->get_params(); } @@ -276,7 +290,13 @@ public: lbool check_sat_cc(expr_ref_vector const& cube, vector const& clauses) override { return check_sat_cc(cube, clauses); } void set_progress_callback(progress_callback* callback) override { s->set_progress_callback(callback); } lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override { - return s->get_consequences(asms, vars, consequences); + expr_ref_vector es(m); + es.append(asms); + es.append(vars); + flush(es); + lbool r = s->get_consequences(asms, vars, consequences); + replace(consequences); + return r; } lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override { return s->find_mutexes(vars, mutexes); } lbool preferred_sat(expr_ref_vector const& asms, vector& cores) override { return s->preferred_sat(asms, cores); } From 72e7a8a4817537e82cd851d93f1879b0f51635bf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2023 20:00:38 -0800 Subject: [PATCH 08/22] fix incremental pre-processing to work with consequences/cubes Signed-off-by: Nikolaj Bjorner --- src/solver/simplifier_solver.cpp | 48 ++++++++++++++++++++++++++++---- 1 file changed, 43 insertions(+), 5 deletions(-) diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index 29021af76..0c41d4f7e 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -287,21 +287,59 @@ public: unsigned get_num_assumptions() const override { return s->get_num_assumptions(); } expr* get_assumption(unsigned idx) const override { return s->get_assumption(idx); } unsigned get_scope_level() const override { return s->get_scope_level(); } - lbool check_sat_cc(expr_ref_vector const& cube, vector const& clauses) override { return check_sat_cc(cube, clauses); } void set_progress_callback(progress_callback* callback) override { s->set_progress_callback(callback); } + lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override { expr_ref_vector es(m); es.append(asms); es.append(vars); flush(es); - lbool r = s->get_consequences(asms, vars, consequences); + expr_ref_vector asms1(m, asms.size(), es.data()); + expr_ref_vector vars1(m, vars.size(), es.data() + asms.size()); + lbool r = s->get_consequences(asms1, vars1, consequences); replace(consequences); return r; } - lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override { return s->find_mutexes(vars, mutexes); } - lbool preferred_sat(expr_ref_vector const& asms, vector& cores) override { return s->preferred_sat(asms, cores); } + + lbool check_sat_cc(expr_ref_vector const& cube, vector const& clauses) override { + expr_ref_vector es(m); + es.append(cube); + for (auto const& c : clauses) + es.append(c); + flush(es); + expr_ref_vector cube1(m, cube.size(), es.data()); + vector clauses1; + unsigned offset = cube.size(); + for (auto const& c : clauses) { + clauses1.push_back(expr_ref_vector(m, c.size(), es.data() + offset)); + offset += c.size(); + } + return check_sat_cc(cube1, clauses1); + } + + lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override { + expr_ref_vector vars1(vars); + flush(vars1); + lbool r = s->find_mutexes(vars1, mutexes); + for (auto& mux : mutexes) + replace(mux); + return r; + } + + lbool preferred_sat(expr_ref_vector const& asms, vector& cores) override { + expr_ref_vector asms1(asms); + flush(asms1); + lbool r = s->preferred_sat(asms1, cores); + for (auto& c : cores) + replace(c); + return r; + } - expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { return s->cube(vars, backtrack_level); } + // todo flush? + expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { + return s->cube(vars, backtrack_level); + } + expr* congruence_root(expr* e) override { return s->congruence_root(e); } expr* congruence_next(expr* e) override { return s->congruence_next(e); } std::ostream& display(std::ostream& out, unsigned n, expr* const* assumptions) const override { From 2e068e3f563a04a0ddf085b55fd249ccb226b92d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 17:41:00 -0800 Subject: [PATCH 09/22] add simplifiers to .net API --- src/api/dotnet/CMakeLists.txt | 1 + src/api/dotnet/Context.cs | 116 +++++++++++++++++++++ src/api/dotnet/Simplifiers.cs | 78 ++++++++++++++ src/ast/simplifiers/dependent_expr_state.h | 3 +- src/solver/simplifier_solver.cpp | 5 +- 5 files changed, 199 insertions(+), 4 deletions(-) create mode 100644 src/api/dotnet/Simplifiers.cs diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index a9344aa86..fcd7b0d85 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -103,6 +103,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE SeqExpr.cs SeqSort.cs SetSort.cs + Simplifiers.cs Solver.cs Sort.cs Statistics.cs diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 80b5a95f1..6365852a6 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3726,6 +3726,110 @@ namespace Microsoft.Z3 } #endregion + #region Simplifiers + /// + /// The number of supported simplifiers. + /// + public uint NumSimplifiers + { + get { return Native.Z3_get_num_simplifiers(nCtx); } + } + + /// + /// The names of all supported tactics. + /// + public string[] SimplifierNames + { + get + { + + uint n = NumSimplifiers; + string[] res = new string[n]; + for (uint i = 0; i < n; i++) + res[i] = Native.Z3_get_simplifier_name(nCtx, i); + return res; + } + } + + /// + /// Returns a string containing a description of the simplifier with the given name. + /// + public string SimplifierDescription(string name) + { + + return Native.Z3_simplifier_get_descr(nCtx, name); + } + + /// + /// Creates a new Tactic. + /// + public Simplifier MkSimplifier(string name) + { + + return new Simplifier(this, name); + } + + /// + /// Create a simplifie that applies and + /// then . + /// + public Simplifier AndThen(Simplifier t1, Simplifier t2, params Simplifier[] ts) + { + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); + // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null)); + + + CheckContextMatch(t1); + CheckContextMatch(t2); + CheckContextMatch(ts); + + IntPtr last = IntPtr.Zero; + if (ts != null && ts.Length > 0) + { + last = ts[ts.Length - 1].NativeObject; + for (int i = ts.Length - 2; i >= 0; i--) + last = Native.Z3_simplifier_and_then(nCtx, ts[i].NativeObject, last); + } + if (last != IntPtr.Zero) + { + last = Native.Z3_simplifier_and_then(nCtx, t2.NativeObject, last); + return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, last)); + } + else + return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Create a simplifier that applies and then + /// then . + /// + /// + /// Shorthand for AndThen. + /// + public Simplifier Then(Simplifier t1, Simplifier t2, params Simplifier[] ts) + { + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); + // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null)); + + return AndThen(t1, t2, ts); + } + + /// + /// Create a tactic that applies using the given set of parameters . + /// + public Simplifier UsingParams(Simplifier t, Params p) + { + Debug.Assert(t != null); + Debug.Assert(p != null); + + CheckContextMatch(t); + CheckContextMatch(p); + return new Simplifier(this, Native.Z3_simplifier_using_params(nCtx, t.NativeObject, p.NativeObject)); + } + #endregion + #region Probes /// /// The number of supported Probes. @@ -3926,6 +4030,16 @@ namespace Microsoft.Z3 return new Solver(this, Native.Z3_mk_simple_solver(nCtx)); } + /// + /// Creates a solver that uses an incremental simplifier. + /// + public Solver MkSolver(Solver s, Simplifier t) + { + Debug.Assert(t != null); + Debug.Assert(s != null); + return new Solver(this, Native.Z3_solver_add_simplifier(nCtx, s.NativeObject, t.NativeObject)); + } + /// /// Creates a solver that is implemented using the given tactic. /// @@ -3939,6 +4053,8 @@ namespace Microsoft.Z3 return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject)); } + + #endregion #region Fixedpoints diff --git a/src/api/dotnet/Simplifiers.cs b/src/api/dotnet/Simplifiers.cs new file mode 100644 index 000000000..a7fbe185f --- /dev/null +++ b/src/api/dotnet/Simplifiers.cs @@ -0,0 +1,78 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + Tactic.cs + +Abstract: + + Z3 Managed API: Simplifiers + +Author: + + Christoph Wintersteiger (cwinter) 2012-03-21 + +--*/ + +using System; +using System.Diagnostics; + +namespace Microsoft.Z3 +{ + /// + /// Simplifiers are the basic building block for creating custom solvers with incremental pre-processing. + /// The complete list of simplifiers may be obtained using Context.NumSimplifiers + /// and Context.SimplifierNames. + /// It may also be obtained using the command (help-simplifier) in the SMT 2.0 front-end. + /// + public class Simplifier : Z3Object + { + /// + /// A string containing a description of parameters accepted by the tactic. + /// + public string Help + { + get + { + + return Native.Z3_simplifier_get_help(Context.nCtx, NativeObject); + } + } + + /// + /// Retrieves parameter descriptions for Simplifiers. + /// + public ParamDescrs ParameterDescriptions + { + get { return new ParamDescrs(Context, Native.Z3_simplifier_get_param_descrs(Context.nCtx, NativeObject)); } + } + + #region Internal + internal Simplifier(Context ctx, IntPtr obj) + : base(ctx, obj) + { + Debug.Assert(ctx != null); + } + internal Simplifier(Context ctx, string name) + : base(ctx, Native.Z3_mk_simplifier(ctx.nCtx, name)) + { + Debug.Assert(ctx != null); + } + + internal override void IncRef(IntPtr o) + { + Native.Z3_simplifier_inc_ref(Context.nCtx, o); + } + + internal override void DecRef(IntPtr o) + { + lock (Context) + { + if (Context.nCtx != IntPtr.Zero) + Native.Z3_simplifier_dec_ref(Context.nCtx, o); + } + } + #endregion + } +} diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index d4d449cf8..b4fe4e9d4 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -90,7 +90,8 @@ public: * Freeze internal functions */ void freeze(expr* term); - bool frozen(func_decl* f) const { return m_frozen.is_marked(f); } + void freeze(expr_ref_vector const& terms) { for (expr* t : terms) freeze(t); } + bool frozen(func_decl* f) const { return m_frozen.is_marked(f); } bool frozen(expr* f) const { return is_app(f) && m_frozen.is_marked(to_app(f)->get_decl()); } void freeze_suffix(); diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index 0c41d4f7e..3ac84ea36 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -110,10 +110,9 @@ class simplifier_solver : public solver { expr_ref_vector orig_assumptions(assumptions); m_core_replace.reset(); if (qhead < m_fmls.size() || !assumptions.empty()) { - for (expr* a : assumptions) - m_preprocess_state.freeze(a); TRACE("solver", tout << "qhead " << qhead << "\n"); - m_preprocess_state.replay(qhead, assumptions); + m_preprocess_state.replay(qhead, assumptions); + m_preprocess_state.freeze(assumptions); m_preprocess.reduce(); if (!m.inc()) return; From 4143c542571948368a6a36334a21392ed50ddb3f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:06:26 -0800 Subject: [PATCH 10/22] add simplifier to java API --- src/api/dotnet/Simplifiers.cs | 2 +- src/api/java/CMakeLists.txt | 2 + src/api/java/Context.java | 115 ++++++++++++++++++++++++ src/api/java/Simplifier.java | 58 ++++++++++++ src/api/java/SimplifierDecRefQueue.java | 31 +++++++ 5 files changed, 207 insertions(+), 1 deletion(-) create mode 100644 src/api/java/Simplifier.java create mode 100644 src/api/java/SimplifierDecRefQueue.java diff --git a/src/api/dotnet/Simplifiers.cs b/src/api/dotnet/Simplifiers.cs index a7fbe185f..28469c1e5 100644 --- a/src/api/dotnet/Simplifiers.cs +++ b/src/api/dotnet/Simplifiers.cs @@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - Tactic.cs + Simplifiers.cs Abstract: diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index e0d6bd0a0..4b13a25b1 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -165,6 +165,8 @@ set(Z3_JAVA_JAR_SOURCE_FILES SeqExpr.java SeqSort.java SetSort.java + Simplifier.java + SimplifierDecRefQueue.java SolverDecRefQueue.java Solver.java Sort.java diff --git a/src/api/java/Context.java b/src/api/java/Context.java index d48101235..0f15d9411 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -3081,6 +3081,106 @@ public class Context implements AutoCloseable { Native.interrupt(nCtx()); } + /** + * The number of supported simplifiers. + **/ + public int getNumSimplifiers() + { + return Native.getNumSimplifiers(nCtx()); + } + + /** + * The names of all supported simplifiers. + **/ + public String[] getSimplifierNames() + { + + int n = getNumSimplifiers(); + String[] res = new String[n]; + for (int i = 0; i < n; i++) + res[i] = Native.getSimplifierName(nCtx(), i); + return res; + } + + /** + * Returns a string containing a description of the simplifier with the given + * name. + **/ + public String getSimplifierDescription(String name) + { + return Native.simplifierGetDescr(nCtx(), name); + } + + /** + * Creates a new Simplifier. + **/ + public Simplifier mkSimplifier(String name) + { + return new Simplifier(this, name); + } + + /** + * Create a simplifier that applies {@code t1} and then {@code t1} + **/ + public Simplifier andThen(Simplifier t1, Simplifier t2, Simplifier... ts) + + { + checkContextMatch(t1); + checkContextMatch(t2); + checkContextMatch(ts); + + long last = 0; + if (ts != null && ts.length > 0) + { + last = ts[ts.length - 1].getNativeObject(); + for (int i = ts.length - 2; i >= 0; i--) { + last = Native.simplifierAndThen(nCtx(), ts[i].getNativeObject(), + last); + } + } + if (last != 0) + { + last = Native.simplifierAndThen(nCtx(), t2.getNativeObject(), last); + return new Simplifier(this, Native.simplifierAndThen(nCtx(), + t1.getNativeObject(), last)); + } else + return new Simplifier(this, Native.simplifierAndThen(nCtx(), + t1.getNativeObject(), t2.getNativeObject())); + } + + /** + * Create a simplifier that applies {@code t1} and then {@code t2} + * + * Remarks: Shorthand for {@code AndThen}. + **/ + public Simplifier then(Simplifier t1, Simplifier t2, Simplifier... ts) + { + return andThen(t1, t2, ts); + } + + /** + * Create a simplifier that applies {@code t} using the given set of + * parameters {@code p}. + **/ + public Simplifier usingParams(Simplifier t, Params p) + { + checkContextMatch(t); + checkContextMatch(p); + return new Simplifier(this, Native.simplifierUsingParams(nCtx(), + t.getNativeObject(), p.getNativeObject())); + } + + /** + * Create a simplifier that applies {@code t} using the given set of + * parameters {@code p}. + * Remarks: Alias for + * {@code UsingParams} + **/ + public Simplifier with(Simplifier t, Params p) + { + return usingParams(t, p); + } + /** * The number of supported Probes. **/ @@ -3279,6 +3379,14 @@ public class Context implements AutoCloseable { t.getNativeObject())); } + /** + * Creates a solver that is uses the simplifier pre-processing. + **/ + public Solver mkSolver(Solver s, Simplifier simp) + { + return new Solver(this, Native.solverAddSimplifier(nCtx(), s.getNativeObject(), simp.getNativeObject())); + } + /** * Create a Fixedpoint context. **/ @@ -4209,6 +4317,7 @@ public class Context implements AutoCloseable { private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(); private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(); private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(); + private SimplifierDecRefQueue m_Simplifier_DRQ = new SimplifierDecRefQueue(); private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(); private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue(); private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue(); @@ -4293,6 +4402,11 @@ public class Context implements AutoCloseable { return m_Tactic_DRQ; } + public IDecRefQueue getSimplifierDRQ() + { + return m_Simplifier_DRQ; + } + public IDecRefQueue getFixedpointDRQ() { return m_Fixedpoint_DRQ; @@ -4323,6 +4437,7 @@ public class Context implements AutoCloseable { m_Optimize_DRQ.forceClear(this); m_Statistics_DRQ.forceClear(this); m_Tactic_DRQ.forceClear(this); + m_Simplifier_DRQ.forceClear(this); m_Fixedpoint_DRQ.forceClear(this); m_boolSort = null; diff --git a/src/api/java/Simplifier.java b/src/api/java/Simplifier.java new file mode 100644 index 000000000..b3fc89ccf --- /dev/null +++ b/src/api/java/Simplifier.java @@ -0,0 +1,58 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + Simplifiers.cs + +Abstract: + + Z3 Managed API: Simplifiers + +Author: + + Christoph Wintersteiger (cwinter) 2012-03-21 + +--*/ + +package com.microsoft.z3; + + +public class Simplifier extends Z3Object { + /* + * A string containing a description of parameters accepted by the simplifier. + */ + + public String getHelp() + { + return Native.simplifierGetHelp(getContext().nCtx(), getNativeObject()); + } + + /* + * Retrieves parameter descriptions for Simplifiers. + */ + public ParamDescrs getParameterDescriptions() { + return new ParamDescrs(getContext(), Native.simplifierGetParamDescrs(getContext().nCtx(), getNativeObject())); + } + + Simplifier(Context ctx, long obj) + { + super(ctx, obj); + } + + Simplifier(Context ctx, String name) + { + super(ctx, Native.mkSimplifier(ctx.nCtx(), name)); + } + + @Override + void incRef() + { + Native.simplifierIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { + getContext().getSimplifierDRQ().storeReference(getContext(), this); + } +} \ No newline at end of file diff --git a/src/api/java/SimplifierDecRefQueue.java b/src/api/java/SimplifierDecRefQueue.java new file mode 100644 index 000000000..ba15dd5be --- /dev/null +++ b/src/api/java/SimplifierDecRefQueue.java @@ -0,0 +1,31 @@ +/** +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + SimplifierDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + +package com.microsoft.z3; + +class SimplifierDecRefQueue extends IDecRefQueue { + public SimplifierDecRefQueue() + { + super(); + } + + @Override + protected void decRef(Context ctx, long obj) + { + Native.simplifierDecRef(ctx.nCtx(), obj); + } +} From ed4a84e5d3637d3a0e4088dd1613055a7972cf07 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:21:34 -0800 Subject: [PATCH 11/22] compiler warning Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_cluster.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/spacer/spacer_cluster.cpp b/src/muz/spacer/spacer_cluster.cpp index b03562b12..fac3a920f 100644 --- a/src/muz/spacer/spacer_cluster.cpp +++ b/src/muz/spacer/spacer_cluster.cpp @@ -378,7 +378,7 @@ void lemma_cluster_finder::cluster(lemma_ref &lemma) { << pattern << "\n" << " and lemma cube: " << lcube << "\n";); - for (const lemma_ref &l : neighbours) { + for (auto l : neighbours) { SASSERT(cluster->can_contain(l)); bool added = cluster->add_lemma(l, false); (void)added; From efbecb19b162a767afe3ee62291018a757413791 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:23:30 -0800 Subject: [PATCH 12/22] compiler warning Signed-off-by: Nikolaj Bjorner --- src/smt/theory_fpa.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index d63ff93cd..2ecc17c45 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -671,7 +671,6 @@ namespace smt { out << "equivalence classes:\n"; for (enode * n : ctx.enodes()) { - expr * e = n->get_expr(); expr * r = n->get_root()->get_expr(); out << r->get_id() << " --> " << enode_pp(n, ctx) << "\n"; } From 741634b7032a9c449c19d571f8e8622e0df61176 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:26:51 -0800 Subject: [PATCH 13/22] compiler warning fix Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_powers.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp index 4054dd7c1..3af31a488 100644 --- a/src/math/lp/nla_powers.cpp +++ b/src/math/lp/nla_powers.cpp @@ -131,7 +131,7 @@ namespace nla { return l_false; } - if (xval >= 3 && yval != 0 & rval <= yval + 1) { + if (xval >= 3 && yval != 0 && rval <= yval + 1) { new_lemma lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1"); lemma |= ineq(x, llc::LT, rational(3)); lemma |= ineq(y, llc::EQ, rational::zero()); From 0d05104d8c68eaa15ce2659eb8b7c1f3de277af0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:33:23 -0800 Subject: [PATCH 14/22] remove unused field Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/dominator_simplifier.cpp | 14 +++++++------- src/ast/simplifiers/dominator_simplifier.h | 2 +- src/ast/substitution/demodulator_rewriter.cpp | 1 - src/ast/substitution/demodulator_rewriter.h | 1 - 4 files changed, 8 insertions(+), 10 deletions(-) diff --git a/src/ast/simplifiers/dominator_simplifier.cpp b/src/ast/simplifiers/dominator_simplifier.cpp index 12f2e2941..2ef4528ab 100644 --- a/src/ast/simplifiers/dominator_simplifier.cpp +++ b/src/ast/simplifiers/dominator_simplifier.cpp @@ -41,7 +41,7 @@ expr_ref dominator_simplifier::simplify_ite(app * ite) { if (is_subexpr(child, t) && !is_subexpr(child, e)) simplify_rec(child); - pop(scope_level() - old_lvl); + local_pop(scope_level() - old_lvl); expr_ref new_t = simplify_arg(t); reset_cache(); if (!assert_expr(new_c, true)) { @@ -50,7 +50,7 @@ expr_ref dominator_simplifier::simplify_ite(app * ite) { for (expr * child : tree(ite)) if (is_subexpr(child, e) && !is_subexpr(child, t)) simplify_rec(child); - pop(scope_level() - old_lvl); + local_pop(scope_level() - old_lvl); expr_ref new_e = simplify_arg(e); if (c == new_c && t == new_t && e == new_e) { @@ -159,7 +159,7 @@ expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) { r = simplify_arg(arg); args.push_back(r); if (!assert_expr(r, !is_and)) { - pop(scope_level() - old_lvl); + local_pop(scope_level() - old_lvl); r = is_and ? m.mk_false() : m.mk_true(); reset_cache(); return true; @@ -181,7 +181,7 @@ expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) { args.reverse(); } - pop(scope_level() - old_lvl); + local_pop(scope_level() - old_lvl); reset_cache(); return { is_and ? mk_and(args) : mk_or(args), m }; } @@ -191,7 +191,7 @@ expr_ref dominator_simplifier::simplify_not(app * e) { ENSURE(m.is_not(e, ee)); unsigned old_lvl = scope_level(); expr_ref t = simplify_rec(ee); - pop(scope_level() - old_lvl); + local_pop(scope_level() - old_lvl); reset_cache(); return mk_not(t); } @@ -245,7 +245,7 @@ void dominator_simplifier::reduce() { } m_fmls.update(i, dependent_expr(m, r, new_pr, d)); } - pop(scope_level()); + local_pop(scope_level()); // go backwards m_forward = false; @@ -268,7 +268,7 @@ void dominator_simplifier::reduce() { } m_fmls.update(i, dependent_expr(m, r, new_pr, d)); } - pop(scope_level()); + local_pop(scope_level()); } SASSERT(scope_level() == 0); } diff --git a/src/ast/simplifiers/dominator_simplifier.h b/src/ast/simplifiers/dominator_simplifier.h index 562aeace1..b412f6db0 100644 --- a/src/ast/simplifiers/dominator_simplifier.h +++ b/src/ast/simplifiers/dominator_simplifier.h @@ -48,7 +48,7 @@ class dominator_simplifier : public dependent_expr_simplifier { expr* idom(expr *e) const { return m_dominators.idom(e); } unsigned scope_level() { return m_simplifier->scope_level(); } - void pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); } + void local_pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); } bool assert_expr(expr* f, bool sign) { return m_simplifier->assert_expr(f, sign); } diff --git a/src/ast/substitution/demodulator_rewriter.cpp b/src/ast/substitution/demodulator_rewriter.cpp index c25647c01..f174b1491 100644 --- a/src/ast/substitution/demodulator_rewriter.cpp +++ b/src/ast/substitution/demodulator_rewriter.cpp @@ -780,7 +780,6 @@ void demodulator_rewriter::operator()(expr_ref_vector const& exprs, demodulator_match_subst::demodulator_match_subst(ast_manager & m): - m(m), m_subst(m) { } diff --git a/src/ast/substitution/demodulator_rewriter.h b/src/ast/substitution/demodulator_rewriter.h index 3a1e442d5..8a1e6feb5 100644 --- a/src/ast/substitution/demodulator_rewriter.h +++ b/src/ast/substitution/demodulator_rewriter.h @@ -111,7 +111,6 @@ class demodulator_match_subst { typedef std::pair expr_pair; typedef obj_pair_hashtable cache; - ast_manager & m; substitution m_subst; cache m_cache; svector m_todo; From 39d28189235aba92da2f50a36ad864e7cf7fd66e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:36:22 -0800 Subject: [PATCH 15/22] compiler warnings/bugs Signed-off-by: Nikolaj Bjorner --- src/solver/simplifier_solver.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index 3ac84ea36..a717c4932 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -224,7 +224,7 @@ public: } proof_ref m_proof; - proof* get_proof_core() { + proof* get_proof_core() override { proof* p = s->get_proof(); m_proof = p; if (p) { @@ -271,7 +271,7 @@ public: std::string reason_unknown() const override { return s->reason_unknown(); } void set_reason_unknown(char const* msg) override { s->set_reason_unknown(msg); } void get_labels(svector& r) override { s->get_labels(r); } - void get_unsat_core(expr_ref_vector& r) { s->get_unsat_core(r); replace(r); } + void get_unsat_core(expr_ref_vector& r) override { s->get_unsat_core(r); replace(r); } ast_manager& get_manager() const override { return s->get_manager(); } void reset_params(params_ref const& p) override { s->reset_params(p); } params_ref const& get_params() const override { return s->get_params(); } @@ -313,7 +313,7 @@ public: clauses1.push_back(expr_ref_vector(m, c.size(), es.data() + offset)); offset += c.size(); } - return check_sat_cc(cube1, clauses1); + return s->check_sat_cc(cube1, clauses1); } lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override { From 839f87a10c919d1c61040c1e91e4d831c3d46071 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 20:50:46 -0800 Subject: [PATCH 16/22] don't apply tactics in parse mode Signed-off-by: Nikolaj Bjorner --- src/cmd_context/tactic_cmds.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 4559586f3..a0805110b 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -296,9 +296,10 @@ public: } void execute(cmd_context & ctx) override { - if (!m_tactic) { + if (!m_tactic) throw cmd_exception("apply needs a tactic argument"); - } + if (ctx.ignore_check()) + return; params_ref p = ctx.params().merge_default_params(ps()); tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p); { From be44ace995b0f653406d9e9867a183cbe657ea3c Mon Sep 17 00:00:00 2001 From: Frederick Robinson Date: Fri, 3 Feb 2023 13:08:35 -0800 Subject: [PATCH 17/22] fix typo (#6569) --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 5cb847230..92bb2aa24 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -9072,7 +9072,7 @@ def PbGe(args, k): def PbEq(args, k, ctx=None): - """Create a Pseudo-Boolean inequality k constraint. + """Create a Pseudo-Boolean equality k constraint. >>> a, b, c = Bools('a b c') >>> f = PbEq(((a,1),(b,3),(c,2)), 3) From d69155b9e992df203c7b1240964c1b5829fc548f Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 3 Feb 2023 22:08:47 +0100 Subject: [PATCH 18/22] Shared features from polysat branch (#6567) * Allow setting default debug action * Fix dlist and add iterator * Add var_queue iterator * Add some helpers * rational: machine_div2k and pseudo_inverse * Basic support for non-copyable types in map * tbv helpers * pdd updates * Remove duplicate functions gcc doesn't like having both versions --- src/math/dd/dd_pdd.cpp | 106 +++++++++++++++++++++++++---- src/math/dd/dd_pdd.h | 36 ++++++++-- src/test/pdd.cpp | 33 +++++++++ src/util/debug.cpp | 67 ++++++++++++++----- src/util/debug.h | 12 ++++ src/util/dlist.h | 147 ++++++++++++++++++++++++++++++++++++----- src/util/map.h | 8 +++ src/util/mpq.h | 8 +++ src/util/rational.cpp | 18 +++++ src/util/rational.h | 9 +++ src/util/tbv.h | 27 +++++--- src/util/util.h | 43 ++++++++++-- src/util/var_queue.h | 4 ++ 13 files changed, 456 insertions(+), 62 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index cca2d5e04..291af3b5c 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -165,6 +165,47 @@ namespace dd { return true; } + unsigned pdd_manager::min_parity(PDD p) { + if (m_semantics != mod2N_e) + return 0; + + if (is_val(p)) { + rational v = val(p); + if (v.is_zero()) + return m_power_of_2 + 1; + unsigned r = 0; + while (v.is_even() && v > 0) + r++, v /= 2; + return r; + } + init_mark(); + PDD q = p; + m_todo.push_back(hi(q)); + while (!is_val(q)) { + q = lo(q); + m_todo.push_back(hi(q)); + } + unsigned p2 = val(q).trailing_zeros(); + init_mark(); + while (p2 != 0 && !m_todo.empty()) { + PDD r = m_todo.back(); + m_todo.pop_back(); + if (is_marked(r)) + continue; + set_mark(r); + if (!is_val(r)) { + m_todo.push_back(lo(r)); + m_todo.push_back(hi(r)); + } + else if (val(r).is_zero()) + continue; + else if (val(r).trailing_zeros() < p2) + p2 = val(r).trailing_zeros(); + } + m_todo.reset(); + return p2; + } + pdd pdd_manager::subst_val(pdd const& p, pdd const& s) { return pdd(apply(p.root, s.root, pdd_subst_val_op), this); } @@ -185,7 +226,20 @@ namespace dd { pdd v_val = mk_var(v) + val; return pdd(apply(s.root, v_val.root, pdd_subst_add_op), this); } - + + bool pdd_manager::subst_get(pdd const& s, unsigned v, rational& out_val) { + unsigned level_v = m_var2level[v]; + PDD p = s.root; + while (/* !is_val(p) && */ level(p) > level_v) { + SASSERT(is_val(lo(p))); + p = hi(p); + } + if (!is_val(p) && level(p) == level_v) { + out_val = val(lo(p)); + return true; + } + return false; + } pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) { bool first = true; @@ -1154,6 +1208,11 @@ namespace dd { return true; } + /** Return true iff p contains no variables other than v. */ + bool pdd_manager::is_univariate_in(PDD p, unsigned v) { + return (is_val(p) || var(p) == v) && is_univariate(p); + } + /** * Push coefficients of univariate polynomial in order of ascending degree. * Example: a*x^2 + b*x + c ==> [ c, b, a ] @@ -1532,7 +1591,6 @@ namespace dd { } void pdd_manager::gc() { - m_gc_generation++; init_dmark(); m_free_nodes.reset(); SASSERT(well_formed()); @@ -1617,26 +1675,26 @@ namespace dd { std::ostream& pdd_manager::display(std::ostream& out, pdd const& b) { auto mons = to_monomials(b); bool first = true; - for (auto& m : mons) { + for (auto& [a, vs] : mons) { if (!first) out << " "; - if (m.first.is_neg()) + if (a.is_neg()) out << "- "; else if (!first) out << "+ "; first = false; - rational c = abs(m.first); - m.second.reverse(); - if (!c.is_one() || m.second.empty()) { - if (m_semantics == mod2N_e && mod(-c, m_mod2N) < c) - out << -mod(-c, m_mod2N); - else + rational c = abs(a); + vs.reverse(); + if (!c.is_one() || vs.empty()) { + if (m_semantics == mod2N_e) + out << val_pp(*this, c, !vs.empty()); + else out << c; - if (!m.second.empty()) out << "*"; + if (!vs.empty()) out << "*"; } unsigned v_prev = UINT_MAX; unsigned pow = 0; - for (unsigned v : m.second) { + for (unsigned v : vs) { if (v == v_prev) { pow++; continue; @@ -1660,6 +1718,23 @@ namespace dd { return out; } + std::ostream& val_pp::display(std::ostream& out) const { + if (m.get_semantics() != pdd_manager::mod2N_e) + return out << val; + unsigned pow; + if (val.is_power_of_two(pow) && pow > 10) + return out << "2^" << pow; + for (int offset : {-2, -1, 1, 2}) + if (val < m.max_value() && (val - offset).is_power_of_two(pow) && pow > 10 && pow < m.power_of_2()) + return out << lparen() << "2^" << pow << (offset >= 0 ? "+" : "") << offset << rparen(); + rational neg_val = mod(-val, m.two_to_N()); + if (neg_val < val) { // keep this condition so we don't suddenly print negative values where we wouldn't otherwise + if (neg_val.is_power_of_two(pow) && pow > 10) + return out << "-2^" << pow; + } + return out << m.normalize(val); + } + bool pdd_manager::well_formed() { bool ok = true; for (unsigned n : m_free_nodes) { @@ -1737,6 +1812,13 @@ namespace dd { return p.val(); } + rational const& pdd::offset() const { + pdd p = *this; + while (!p.is_val()) + p = p.lo(); + return p.val(); + } + pdd pdd::shl(unsigned n) const { return (*this) * rational::power_of_two(n); } diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index aef0eb6f7..6dee7977f 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -10,7 +10,7 @@ Abstract: Poly DD package It is a mild variant of ZDDs. - In PDDs arithmetic is either standard or using mod 2 (over GF2). + In PDDs arithmetic is either standard or using mod 2^n. Non-leaf nodes are of the form x*hi + lo where @@ -208,7 +208,6 @@ namespace dd { rational m_mod2N; unsigned m_power_of_2 = 0; rational m_max_value; - unsigned m_gc_generation = 0; ///< will be incremented on each GC void reset_op_cache(); void init_nodes(unsigned_vector const& l2v); @@ -254,7 +253,9 @@ namespace dd { inline bool is_val(PDD p) const { return m_nodes[p].is_val(); } inline bool is_internal(PDD p) const { return m_nodes[p].is_internal(); } inline bool is_var(PDD p) const { return !is_val(p) && is_zero(lo(p)) && is_one(hi(p)); } + inline bool is_max(PDD p) const { SASSERT(m_semantics == mod2_e || m_semantics == mod2N_e); return is_val(p) && val(p) == max_value(); } bool is_never_zero(PDD p); + unsigned min_parity(PDD p); inline unsigned level(PDD p) const { return m_nodes[p].m_level; } inline unsigned var(PDD p) const { return m_level2var[level(p)]; } inline PDD lo(PDD p) const { return m_nodes[p].m_lo; } @@ -315,6 +316,11 @@ namespace dd { pdd_manager(unsigned num_vars, semantics s = free_e, unsigned power_of_2 = 0); ~pdd_manager(); + pdd_manager(pdd_manager const&) = delete; + pdd_manager(pdd_manager&&) = delete; + pdd_manager& operator=(pdd_manager const&) = delete; + pdd_manager& operator=(pdd_manager&&) = delete; + semantics get_semantics() const { return m_semantics; } void reset(unsigned_vector const& level2var); @@ -343,6 +349,7 @@ namespace dd { pdd subst_val(pdd const& a, unsigned v, rational const& val); pdd subst_val(pdd const& a, pdd const& s); pdd subst_add(pdd const& s, unsigned v, rational const& val); + bool subst_get(pdd const& s, unsigned v, rational& out_val); bool resolve(unsigned v, pdd const& p, pdd const& q, pdd& r); pdd reduce(unsigned v, pdd const& a, pdd const& b); void quot_rem(pdd const& a, pdd const& b, pdd& q, pdd& r); @@ -357,6 +364,7 @@ namespace dd { bool is_monomial(PDD p); bool is_univariate(PDD p); + bool is_univariate_in(PDD p, unsigned v); void get_univariate_coefficients(PDD p, vector& coeff); // create an spoly r if leading monomials of a and b overlap @@ -375,6 +383,8 @@ namespace dd { unsigned power_of_2() const { return m_power_of_2; } rational const& max_value() const { return m_max_value; } rational const& two_to_N() const { return m_mod2N; } + rational normalize(rational const& n) const { return mod(-n, m_mod2N) < n ? -mod(-n, m_mod2N) : n; } + unsigned_vector const& free_vars(pdd const& p); @@ -406,21 +416,26 @@ namespace dd { unsigned var() const { return m.var(root); } rational const& val() const { SASSERT(is_val()); return m.val(root); } rational const& leading_coefficient() const; + rational const& offset() const; bool is_val() const { return m.is_val(root); } bool is_one() const { return m.is_one(root); } bool is_zero() const { return m.is_zero(root); } bool is_linear() const { return m.is_linear(root); } bool is_var() const { return m.is_var(root); } - /** Polynomial is of the form a * x + b for numerals a, b. */ + bool is_max() const { return m.is_max(root); } + /** Polynomial is of the form a * x + b for some numerals a, b. */ bool is_unilinear() const { return !is_val() && lo().is_val() && hi().is_val(); } + /** Polynomial is of the form a * x for some numeral a. */ bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } bool is_offset() const { return !is_val() && lo().is_val() && hi().is_one(); } bool is_binary() const { return m.is_binary(root); } bool is_monomial() const { return m.is_monomial(root); } bool is_univariate() const { return m.is_univariate(root); } + bool is_univariate_in(unsigned v) const { return m.is_univariate_in(root, v); } void get_univariate_coefficients(vector& coeff) const { m.get_univariate_coefficients(root, coeff); } vector get_univariate_coefficients() const { vector coeff; m.get_univariate_coefficients(root, coeff); return coeff; } bool is_never_zero() const { return m.is_never_zero(root); } + unsigned min_parity() const { return m.min_parity(root); } bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); } pdd operator-() const { return m.minus(*this); } @@ -455,7 +470,8 @@ namespace dd { pdd subst_val0(vector> const& s) const { return m.subst_val0(*this, s); } pdd subst_val(pdd const& s) const { return m.subst_val(*this, s); } pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); } - pdd subst_add(unsigned var, rational const& val) { return m.subst_add(*this, var, val); } + pdd subst_add(unsigned var, rational const& val) const { return m.subst_add(*this, var, val); } + bool subst_get(unsigned var, rational& out_val) const { return m.subst_get(*this, var, out_val); } /** * \brief substitute variable v by r. @@ -538,6 +554,18 @@ namespace dd { bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; } }; + class val_pp { + pdd_manager const& m; + rational const& val; + bool require_parens; + char const* lparen() const { return require_parens ? "(" : ""; } + char const* rparen() const { return require_parens ? ")" : ""; } + public: + val_pp(pdd_manager const& m, rational const& val, bool require_parens = false): m(m), val(val), require_parens(require_parens) {} + std::ostream& display(std::ostream& out) const; + }; + + inline std::ostream& operator<<(std::ostream& out, val_pp const& v) { return v.display(out); } } diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp index a0946d81d..0c9b0f85c 100644 --- a/src/test/pdd.cpp +++ b/src/test/pdd.cpp @@ -571,6 +571,38 @@ public: } } + static void subst_get() { + std::cout << "subst_get\n"; + pdd_manager m(4, pdd_manager::mod2N_e, 32); + + unsigned const va = 0; + unsigned const vb = 1; + unsigned const vc = 2; + unsigned const vd = 3; + + rational val; + pdd s = m.one(); + std::cout << s << "\n"; + VERIFY(!s.subst_get(va, val)); + VERIFY(!s.subst_get(vb, val)); + VERIFY(!s.subst_get(vc, val)); + VERIFY(!s.subst_get(vd, val)); + + s = s.subst_add(va, rational(5)); + std::cout << s << "\n"; + VERIFY(s.subst_get(va, val) && val == 5); + VERIFY(!s.subst_get(vb, val)); + VERIFY(!s.subst_get(vc, val)); + VERIFY(!s.subst_get(vd, val)); + + s = s.subst_add(vc, rational(7)); + std::cout << s << "\n"; + VERIFY(s.subst_get(va, val) && val == 5); + VERIFY(!s.subst_get(vb, val)); + VERIFY(s.subst_get(vc, val) && val == 7); + VERIFY(!s.subst_get(vd, val)); + } + static void univariate() { std::cout << "univariate\n"; pdd_manager m(4, pdd_manager::mod2N_e, 4); @@ -671,6 +703,7 @@ void tst_pdd() { dd::test::binary_resolve(); dd::test::pow(); dd::test::subst_val(); + dd::test::subst_get(); dd::test::univariate(); dd::test::factors(); } diff --git a/src/util/debug.cpp b/src/util/debug.cpp index f97a2b57b..c9ca9fc31 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -75,32 +75,62 @@ bool is_debug_enabled(const char * tag) { return g_enabled_debug_tags->contains(tag); } +atomic g_default_debug_action(debug_action::ask); + +debug_action get_default_debug_action() { + return g_default_debug_action; +} + +void set_default_debug_action(debug_action a) { + g_default_debug_action = a; +} + +debug_action ask_debug_action(std::istream& in) { + std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n"; + char result; + bool ok = bool(in >> result); + if (!ok) + exit(ERR_INTERNAL_FATAL); // happens if std::cin is eof or unattached. + switch(result) { + case 'C': + case 'c': + return debug_action::cont; + case 'A': + case 'a': + return debug_action::abort; + case 'S': + case 's': + return debug_action::stop; + case 't': + case 'T': + return debug_action::throw_exception; + case 'G': + case 'g': + return debug_action::invoke_debugger; + default: + std::cerr << "INVALID COMMAND\n"; + return debug_action::ask; + } +} + #if !defined(_WINDOWS) && !defined(NO_Z3_DEBUGGER) void invoke_gdb() { std::string buffer; - int * x = nullptr; + int *x = nullptr; + debug_action a = get_default_debug_action(); for (;;) { - std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n"; - char result; - bool ok = bool(std::cin >> result); - if (!ok) exit(ERR_INTERNAL_FATAL); // happens if std::cin is eof or unattached. - switch(result) { - case 'C': - case 'c': + switch (a) { + case debug_action::cont: return; - case 'A': - case 'a': + case debug_action::abort: exit(1); - case 'S': - case 's': + case debug_action::stop: // force seg fault... *x = 0; return; - case 't': - case 'T': + case debug_action::throw_exception: throw default_exception("assertion violation"); - case 'G': - case 'g': + case debug_action::invoke_debugger: buffer = "gdb -nw /proc/" + std::to_string(getpid()) + "/exe " + std::to_string(getpid()); std::cerr << "invoking GDB...\n"; if (system(buffer.c_str()) == 0) { @@ -109,12 +139,13 @@ void invoke_gdb() { else { std::cerr << "error starting GDB...\n"; // forcing seg fault. - int * x = nullptr; + int *x = nullptr; *x = 0; } return; + case debug_action::ask: default: - std::cerr << "INVALID COMMAND\n"; + a = ask_debug_action(std::cin); } } } diff --git a/src/util/debug.h b/src/util/debug.h index 795976eac..5f092b181 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -19,10 +19,22 @@ Revision History: #pragma once #include +#include void enable_assertions(bool f); bool assertions_enabled(); +enum class debug_action { + ask, + cont, + abort, + stop, + throw_exception, + invoke_debugger, +}; +debug_action get_default_debug_action(); +void set_default_debug_action(debug_action a); + #include "util/error_codes.h" #include "util/warning.h" diff --git a/src/util/dlist.h b/src/util/dlist.h index 7efe5bb53..e5c95b8cf 100644 --- a/src/util/dlist.h +++ b/src/util/dlist.h @@ -17,20 +17,38 @@ Revision History: --*/ #pragma once +#include +#include "util/debug.h" +#include "util/util.h" +#define DLIST_EXTRA_ASSERTIONS 0 -template +template class dll_iterator; + +template class dll_base { - T* m_next { nullptr }; - T* m_prev { nullptr }; + T* m_next = nullptr; + T* m_prev = nullptr; + +protected: + dll_base() = default; + ~dll_base() = default; + public: + dll_base(dll_base const&) = delete; + dll_base(dll_base&&) = delete; + dll_base& operator=(dll_base const&) = delete; + dll_base& operator=(dll_base&&) = delete; T* prev() { return m_prev; } T* next() { return m_next; } + T const* prev() const { return m_prev; } + T const* next() const { return m_next; } void init(T* t) { m_next = t; m_prev = t; + SASSERT(invariant()); } static T* pop(T*& list) { @@ -41,23 +59,63 @@ public: return head; } - void insert_after(T* elem) { + void insert_after(T* other) { +#if DLIST_EXTRA_ASSERTIONS + SASSERT(other); + SASSERT(invariant()); + SASSERT(other->invariant()); + size_t const old_sz1 = count_if(*static_cast(this), [](T const&) { return true; }); + size_t const old_sz2 = count_if(*other, [](T const&) { return true; }); +#endif + // have: this -> next -> ... + // insert: other -> ... -> other_end + // result: this -> other -> ... -> other_end -> next -> ... T* next = this->m_next; - elem->m_prev = next->m_prev; - elem->m_next = next; - this->m_next = elem; - next->m_prev = elem; + T* other_end = other->m_prev; + this->m_next = other; + other->m_prev = static_cast(this); + other_end->m_next = next; + next->m_prev = other_end; +#if DLIST_EXTRA_ASSERTIONS + SASSERT(invariant()); + SASSERT(other->invariant()); + size_t const new_sz = count_if(*static_cast(this), [](T const&) { return true; }); + SASSERT_EQ(new_sz, old_sz1 + old_sz2); +#endif } - void insert_before(T* elem) { + void insert_before(T* other) { +#if DLIST_EXTRA_ASSERTIONS + SASSERT(other); + SASSERT(invariant()); + SASSERT(other->invariant()); + size_t const old_sz1 = count_if(*static_cast(this), [](T const&) { return true; }); + size_t const old_sz2 = count_if(*other, [](T const&) { return true; }); +#endif + // have: prev -> this -> ... + // insert: other -> ... -> other_end + // result: prev -> other -> ... -> other_end -> this -> ... T* prev = this->m_prev; - elem->m_next = prev->m_next; - elem->m_prev = prev; - prev->m_next = elem; - this->m_prev = elem; + T* other_end = other->m_prev; + prev->m_next = other; + other->m_prev = prev; + other_end->m_next = static_cast(this); + this->m_prev = other_end; +#if DLIST_EXTRA_ASSERTIONS + SASSERT(invariant()); + SASSERT(other->invariant()); + size_t const new_sz = count_if(*static_cast(this), [](T const&) { return true; }); + SASSERT_EQ(new_sz, old_sz1 + old_sz2); +#endif } static void remove_from(T*& list, T* elem) { +#if DLIST_EXTRA_ASSERTIONS + SASSERT(list); + SASSERT(elem); + SASSERT(list->invariant()); + SASSERT(elem->invariant()); +#endif if (list->m_next == list) { SASSERT(elem == list); list = nullptr; @@ -69,6 +127,9 @@ public: auto* prev = elem->m_prev; prev->m_next = next; next->m_prev = prev; +#if DLIST_EXTRA_ASSERTIONS + SASSERT(list->invariant()); +#endif } static void push_to_front(T*& list, T* elem) { @@ -105,11 +166,10 @@ public: return true; } - - static bool contains(T* list, T* elem) { + static bool contains(T const* list, T const* elem) { if (!list) return false; - T* first = list; + T const* first = list; do { if (list == elem) return true; @@ -120,5 +180,60 @@ public: } }; +template +class dll_iterator { + T const* m_elem; + bool m_first; + dll_iterator(T const* elem, bool first): m_elem(elem), m_first(first) { } +public: + static dll_iterator mk_begin(T const* elem) { + // Setting first==(bool)elem makes this also work for elem==nullptr; + // but we can't implement top-level begin/end for pointers because it clashes with the definition for arrays. + return {elem, (bool)elem}; + } + + static dll_iterator mk_end(T const* elem) { + return {elem, false}; + } + + using value_type = T; + using pointer = T const*; + using reference = T const&; + using iterator_category = std::input_iterator_tag; + using difference_type = std::ptrdiff_t; + + dll_iterator& operator++() { + m_elem = m_elem->next(); + m_first = false; + return *this; + } + + T const& operator*() const { + return *m_elem; + } + + bool operator==(dll_iterator const& other) const { + return m_elem == other.m_elem && m_first == other.m_first; + } + + bool operator!=(dll_iterator const& other) const { + return !operator==(other); + } +}; + +template < typename T + , typename U = std::enable_if_t, T>> // should only match if T actually inherits from dll_base + > +dll_iterator begin(T const& elem) { + return dll_iterator::mk_begin(&elem); +} + +template < typename T + , typename U = std::enable_if_t, T>> // should only match if T actually inherits from dll_base + > +dll_iterator end(T const& elem) +{ + return dll_iterator::mk_end(&elem); +} diff --git a/src/util/map.h b/src/util/map.h index 602c042fb..e9880e0a0 100644 --- a/src/util/map.h +++ b/src/util/map.h @@ -33,6 +33,10 @@ struct _key_data { m_key(k), m_value(v) { } + _key_data(Key const& k, Value&& v): + m_key(k), + m_value(std::move(v)) { + } }; template @@ -106,6 +110,10 @@ public: void insert(key const & k, value const & v) { m_table.insert(key_data(k, v)); } + + void insert(key const& k, value&& v) { + m_table.insert(key_data(k, std::move(v))); + } bool insert_if_not_there_core(key const & k, value const & v, entry *& et) { return m_table.insert_if_not_there_core(key_data(k,v), et); diff --git a/src/util/mpq.h b/src/util/mpq.h index 31ffbeab8..e254ade69 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -487,6 +487,8 @@ public: void machine_div_rem(mpz const & a, mpz const & b, mpz & c, mpz & d) { mpz_manager::machine_div_rem(a, b, c, d); } + void machine_div2k(mpz const & a, unsigned k, mpz & c) { mpz_manager::machine_div2k(a, k, c); } + void div(mpz const & a, mpz const & b, mpz & c) { mpz_manager::div(a, b, c); } void rat_div(mpz const & a, mpz const & b, mpq & c) { @@ -513,6 +515,12 @@ public: machine_div(a.m_num, b.m_num, c); } + void machine_idiv2k(mpq const & a, unsigned k, mpq & c) { + SASSERT(is_int(a)); + machine_div2k(a.m_num, k, c.m_num); + reset_denominator(c); + } + void idiv(mpq const & a, mpq const & b, mpq & c) { SASSERT(is_int(a) && is_int(b)); div(a.m_num, b.m_num, c.m_num); diff --git a/src/util/rational.cpp b/src/util/rational.cpp index af3c89ced..54b40ac58 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -153,3 +153,21 @@ bool rational::mult_inverse(unsigned num_bits, rational & result) const { return true; } +/** + * Compute the smallest multiplicative pseudo-inverse modulo 2^num_bits: + * + * mod(n * n.pseudo_inverse(bits), 2^bits) == 2^k, + * where k is maximal such that 2^k divides n. + * + * Precondition: number is non-zero. + */ +rational rational::pseudo_inverse(unsigned num_bits) const { + rational result; + rational const& n = *this; + SASSERT(!n.is_zero()); // TODO: or we define pseudo-inverse of 0 as 0. + unsigned const k = n.trailing_zeros(); + rational const odd = machine_div2k(n, k); + VERIFY(odd.mult_inverse(num_bits - k, result)); + SASSERT_EQ(mod(n * result, rational::power_of_two(num_bits)), rational::power_of_two(k)); + return result; +} diff --git a/src/util/rational.h b/src/util/rational.h index 4203a54ea..f47fddefe 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -56,6 +56,8 @@ public: explicit rational(char const * v) { m().set(m_val, v); } + explicit rational(unsigned const * v, unsigned sz) { m().set(m_val, sz, v); } + struct i64 {}; rational(int64_t i, i64) { m().set(m_val, i); } @@ -227,6 +229,12 @@ public: return r; } + friend inline rational machine_div2k(rational const & r1, unsigned k) { + rational r; + rational::m().machine_idiv2k(r1.m_val, k, r.m_val); + return r; + } + friend inline rational mod(rational const & r1, rational const & r2) { rational r; rational::m().mod(r1.m_val, r2.m_val, r.m_val); @@ -353,6 +361,7 @@ public: } bool mult_inverse(unsigned num_bits, rational & result) const; + rational pseudo_inverse(unsigned num_bits) const; static rational const & zero() { return m_zero; diff --git a/src/util/tbv.h b/src/util/tbv.h index 2a337be1f..cffdc2460 100644 --- a/src/util/tbv.h +++ b/src/util/tbv.h @@ -27,10 +27,10 @@ Revision History: class tbv; enum tbit { - BIT_z = 0x0, - BIT_0 = 0x1, - BIT_1 = 0x2, - BIT_x = 0x3 + BIT_z = 0x0, // unknown + BIT_0 = 0x1, // for sure 0 + BIT_1 = 0x2, // for sure 1 + BIT_x = 0x3 // don't care }; inline tbit neg(tbit t) { @@ -43,6 +43,7 @@ class tbv_manager { ptr_vector allocated_tbvs; public: tbv_manager(unsigned n): m(2*n) {} + tbv_manager(tbv_manager const& m) = delete; ~tbv_manager(); void reset(); tbv* allocate(); @@ -132,8 +133,9 @@ class tbv_ref { tbv_manager& mgr; tbv* d; public: - tbv_ref(tbv_manager& mgr):mgr(mgr),d(nullptr) {} - tbv_ref(tbv_manager& mgr, tbv* d):mgr(mgr),d(d) {} + tbv_ref(tbv_manager& mgr) : mgr(mgr), d(nullptr) {} + tbv_ref(tbv_manager& mgr, tbv* d) : mgr(mgr), d(d) {} + tbv_ref(tbv_ref&& d) : mgr(d.mgr), d(d.detach()) {} ~tbv_ref() { if (d) mgr.deallocate(d); } @@ -144,8 +146,17 @@ public: } tbv& operator*() { return *d; } tbv* operator->() { return d; } - tbv* get() { return d; } + tbit operator[](unsigned idx) const { return (*d)[idx]; } + tbv* get() const { return d; } tbv* detach() { tbv* result = d; d = nullptr; return result; } + tbv_manager& manager() const { return mgr; } + unsigned num_tbits() const { return mgr.num_tbits(); } }; - +inline std::ostream& operator<<(std::ostream& out, tbv_ref const& c) { + char const* names[] = { "z", "0", "1", "x" }; + for (unsigned i = c.num_tbits(); i-- > 0; ) { + out << names[static_cast(c[i])]; + } + return out; +} diff --git a/src/util/util.h b/src/util/util.h index 121031492..6d4efb671 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -20,12 +20,14 @@ Revision History: #include "util/debug.h" #include "util/memory_manager.h" -#include -#include -#include -#include +#include +#include +#include +#include #include #include +#include +#include #ifndef SIZE_MAX #define SIZE_MAX std::numeric_limits::max() @@ -410,3 +412,36 @@ inline size_t megabytes_to_bytes(unsigned mb) { r = SIZE_MAX; return r; } + +/** Compact version of std::count */ +template +std::size_t count(Container const& c, Item x) +{ + using std::begin, std::end; // allows begin(c) to also find c.begin() + return std::count(begin(c), end(c), std::forward(x)); +} + +/** Compact version of std::count_if */ +template +std::size_t count_if(Container const& c, Predicate p) +{ + using std::begin, std::end; // allows begin(c) to also find c.begin() + return std::count_if(begin(c), end(c), std::forward(p)); +} + +/** Basic version of https://en.cppreference.com/w/cpp/experimental/scope_exit */ +template +class on_scope_exit final { + Callable m_ef; +public: + on_scope_exit(Callable&& ef) + : m_ef(std::forward(ef)) + { } + ~on_scope_exit() { + m_ef(); + } +}; + +/** Helper type for std::visit, see examples on https://en.cppreference.com/w/cpp/utility/variant/visit */ +template +struct always_false : std::false_type {}; diff --git a/src/util/var_queue.h b/src/util/var_queue.h index 62df77784..7245153ca 100644 --- a/src/util/var_queue.h +++ b/src/util/var_queue.h @@ -89,6 +89,10 @@ public: } return out; } + + using const_iterator = decltype(m_queue)::const_iterator; + const_iterator begin() const { return m_queue.begin(); } + const_iterator end() const { return m_queue.end(); } }; inline std::ostream& operator<<(std::ostream& out, var_queue const& queue) { From 3712cbdbfd61237779219c49d06fb69e4d77f852 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Feb 2023 13:33:40 -0800 Subject: [PATCH 19/22] fix #6559 Signed-off-by: Nikolaj Bjorner --- src/qe/qe.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index f4ebce594..12365b204 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -1513,10 +1513,11 @@ namespace qe { propagate_assignment(*model_eval); VERIFY(CHOOSE_VAR == update_current(*model_eval, true)); SASSERT(m_current->fml()); - if (l_true != m_solver.check()) { - return l_true; - } + if (l_true != m_solver.check()) + return l_true; m_solver.get_model(model); + if (!model) + return l_undef; model_eval = alloc(model_evaluator, *model); search_tree* st = m_current; update_current(*model_eval, false); From 992793bd56d0c9736ae8c407f1fb44ec52df1e1f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Feb 2023 21:34:37 -0800 Subject: [PATCH 20/22] update nuget packaging targets #6570 --- scripts/mk_nuget_task.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index dd81349df..e22057a0f 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -25,9 +25,11 @@ os_info = { 'ubuntu-latest' : ('so', 'linux-x64'), 'ubuntu-18' : ('so', 'linux-x64'), 'ubuntu-20' : ('so', 'linux-x64'), 'glibc-2.31' : ('so', 'linux-x64'), + 'glibc' : ('so', 'linux-x64'), 'x64-win' : ('dll', 'win-x64'), 'x86-win' : ('dll', 'win-x86'), - 'osx' : ('dylib', 'osx-x64'), + 'x64-osx' : ('dylib', 'osx-x64'), + 'arm64-osx' : ('dylib', 'osx-arm64'), 'debian' : ('so', 'linux-x64') } From 75c573877d0bec64e36a7cf69689915a52c1ba81 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Feb 2023 21:35:18 -0800 Subject: [PATCH 21/22] updates to ddfw, initial local search phase option --- src/sat/sat_config.cpp | 2 + src/sat/sat_config.h | 1 + src/sat/sat_ddfw.cpp | 118 ++++++++++++++++++++++++----------------- src/sat/sat_ddfw.h | 64 +++++++++++++--------- src/sat/sat_solver.cpp | 79 +++++++++++++++++---------- src/sat/sat_solver.h | 2 + src/sat/sat_types.h | 3 +- 7 files changed, 165 insertions(+), 104 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index eb2d0071d..0a9e803a9 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -65,6 +65,8 @@ namespace sat { m_phase = PS_RANDOM; else if (s == symbol("frozen")) m_phase = PS_FROZEN; + else if (s == symbol("local_search")) + m_phase = PS_LOCAL_SEARCH; else throw sat_param_exception("invalid phase selection strategy: always_false, always_true, basic_caching, caching, random"); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 8adfc13ed..f8c0775b1 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -28,6 +28,7 @@ namespace sat { PS_ALWAYS_FALSE, PS_BASIC_CACHING, PS_SAT_CACHING, + PS_LOCAL_SEARCH, PS_FROZEN, PS_RANDOM }; diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp index ecfc13aa6..f1493232c 100644 --- a/src/sat/sat_ddfw.cpp +++ b/src/sat/sat_ddfw.cpp @@ -49,6 +49,7 @@ namespace sat { else if (should_parallel_sync()) do_parallel_sync(); else shift_weights(); } + log(); return m_min_sz == 0 ? l_true : l_undef; } @@ -66,9 +67,9 @@ namespace sat { << std::setw(10) << kflips_per_sec << std::setw(10) << m_flips << std::setw(10) << m_restart_count - << std::setw(10) << m_reinit_count - << std::setw(10) << m_unsat_vars.size() - << std::setw(10) << m_shifts; + << std::setw(11) << m_reinit_count + << std::setw(13) << m_unsat_vars.size() + << std::setw(9) << m_shifts; if (m_par) verbose_stream() << std::setw(10) << m_parsync_count; verbose_stream() << ")\n"); m_stopwatch.start(); @@ -90,18 +91,18 @@ namespace sat { unsigned n = 1; bool_var v0 = null_bool_var; for (bool_var v : m_unsat_vars) { - int r = reward(v); - if (r > 0) { + double r = reward(v); + if (r > 0.0) { sum_pos += score(r); } - else if (r == 0 && sum_pos == 0 && (m_rand() % (n++)) == 0) { + else if (r == 0.0 && sum_pos == 0 && (m_rand() % (n++)) == 0) { v0 = v; } } if (sum_pos > 0) { double lim_pos = ((double) m_rand() / (1.0 + m_rand.max_value())) * sum_pos; for (bool_var v : m_unsat_vars) { - int r = reward(v); + double r = reward(v); if (r > 0) { lim_pos -= score(r); if (lim_pos <= 0) { @@ -121,7 +122,7 @@ namespace sat { * TBD: map reward value to a score, possibly through an exponential function, such as * exp(-tau/r), where tau > 0 */ - double ddfw::mk_score(unsigned r) { + double ddfw::mk_score(double r) { return r; } @@ -201,7 +202,7 @@ namespace sat { m_shifts = 0; m_stopwatch.start(); } - + void ddfw::reinit(solver& s) { add(s); add_assumptions(); @@ -235,7 +236,7 @@ namespace sat { for (unsigned cls_idx : use_list(*this, lit)) { clause_info& ci = m_clauses[cls_idx]; ci.del(lit); - unsigned w = ci.m_weight; + double w = ci.m_weight; // cls becomes false: flip any variable in clause to receive reward w switch (ci.m_num_trues) { case 0: { @@ -257,7 +258,7 @@ namespace sat { } for (unsigned cls_idx : use_list(*this, nlit)) { clause_info& ci = m_clauses[cls_idx]; - unsigned w = ci.m_weight; + double w = ci.m_weight; // the clause used to have a single true (pivot) literal, now it has two. // Then the previous pivot is no longer penalized for flipping. switch (ci.m_num_trues) { @@ -406,9 +407,8 @@ namespace sat { void ddfw::save_best_values() { if (m_unsat.empty()) { m_model.reserve(num_vars()); - for (unsigned i = 0; i < num_vars(); ++i) { + for (unsigned i = 0; i < num_vars(); ++i) m_model[i] = to_lbool(value(i)); - } } if (m_unsat.size() < m_min_sz) { m_models.reset(); @@ -422,13 +422,11 @@ namespace sat { } unsigned h = value_hash(); if (!m_models.contains(h)) { - for (unsigned v = 0; v < num_vars(); ++v) { + for (unsigned v = 0; v < num_vars(); ++v) bias(v) += value(v) ? 1 : -1; - } m_models.insert(h); - if (m_models.size() > m_config.m_max_num_models) { + if (m_models.size() > m_config.m_max_num_models) m_models.erase(*m_models.begin()); - } } m_min_sz = m_unsat.size(); } @@ -450,10 +448,9 @@ namespace sat { 3. select multiple clauses instead of just one per clause in unsat. */ - bool ddfw::select_clause(unsigned max_weight, unsigned max_trues, clause_info const& cn, unsigned& n) { - if (cn.m_num_trues == 0 || cn.m_weight < max_weight) { + bool ddfw::select_clause(double max_weight, clause_info const& cn, unsigned& n) { + if (cn.m_num_trues == 0 || cn.m_weight + 1e-5 < max_weight) return false; - } if (cn.m_weight > max_weight) { n = 2; return true; @@ -462,51 +459,72 @@ namespace sat { } unsigned ddfw::select_max_same_sign(unsigned cf_idx) { - clause const& c = get_clause(cf_idx); - unsigned max_weight = 2; - unsigned max_trues = 0; + auto& ci = m_clauses[cf_idx]; unsigned cl = UINT_MAX; // clause pointer to same sign, max weight satisfied clause. + clause const& c = *ci.m_clause; + double max_weight = m_init_weight; unsigned n = 1; for (literal lit : c) { for (unsigned cn_idx : use_list(*this, lit)) { auto& cn = m_clauses[cn_idx]; - if (select_clause(max_weight, max_trues, cn, n)) { + if (select_clause(max_weight, cn, n)) { cl = cn_idx; max_weight = cn.m_weight; - max_trues = cn.m_num_trues; } } } return cl; } + void ddfw::transfer_weight(unsigned from, unsigned to, double w) { + auto& cf = m_clauses[to]; + auto& cn = m_clauses[from]; + if (cn.m_weight < w) + return; + cf.m_weight += w; + cn.m_weight -= w; + + for (literal lit : get_clause(to)) + inc_reward(lit, w); + if (cn.m_num_trues == 1) + inc_reward(to_literal(cn.m_trues), w); + } + + unsigned ddfw::select_random_true_clause() { + unsigned num_clauses = m_clauses.size(); + unsigned rounds = 100 * num_clauses; + for (unsigned i = 0; i < rounds; ++i) { + unsigned idx = (m_rand() * m_rand()) % num_clauses; + auto & cn = m_clauses[idx]; + if (cn.is_true() && cn.m_weight >= m_init_weight) + return idx; + } + return UINT_MAX; + } + + // 1% chance to disregard neighbor + inline bool ddfw::disregard_neighbor() { + return false; // rand() % 1000 == 0; + } + + double ddfw::calculate_transfer_weight(double w) { + return (w > m_init_weight) ? m_init_weight : 1; + } + void ddfw::shift_weights() { ++m_shifts; - for (unsigned cf_idx : m_unsat) { - auto& cf = m_clauses[cf_idx]; + for (unsigned to_idx : m_unsat) { + auto& cf = m_clauses[to_idx]; SASSERT(!cf.is_true()); - unsigned cn_idx = select_max_same_sign(cf_idx); - while (cn_idx == UINT_MAX) { - unsigned idx = (m_rand() * m_rand()) % m_clauses.size(); - auto & cn = m_clauses[idx]; - if (cn.is_true() && cn.m_weight >= 2) { - cn_idx = idx; - } - } - auto & cn = m_clauses[cn_idx]; + unsigned from_idx = select_max_same_sign(to_idx); + if (from_idx == UINT_MAX || disregard_neighbor()) + from_idx = select_random_true_clause(); + if (from_idx == UINT_MAX) + continue; + auto & cn = m_clauses[from_idx]; SASSERT(cn.is_true()); - unsigned wn = cn.m_weight; - SASSERT(wn >= 2); - unsigned inc = (wn > 2) ? 2 : 1; - SASSERT(wn - inc >= 1); - cf.m_weight += inc; - cn.m_weight -= inc; - for (literal lit : get_clause(cf_idx)) { - inc_reward(lit, inc); - } - if (cn.m_num_trues == 1) { - inc_reward(to_literal(cn.m_trues), inc); - } + double w = calculate_transfer_weight(cn.m_weight); + transfer_weight(from_idx, to_idx, w); } // DEBUG_CODE(invariant();); } @@ -543,7 +561,7 @@ namespace sat { VERIFY(found); } for (unsigned v = 0; v < num_vars(); ++v) { - int v_reward = 0; + double v_reward = 0; literal lit(v, !value(v)); for (unsigned j : m_use_list[lit.index()]) { clause_info const& ci = m_clauses[j]; @@ -559,7 +577,7 @@ namespace sat { } } IF_VERBOSE(0, if (v_reward != reward(v)) verbose_stream() << v << " " << v_reward << " " << reward(v) << "\n"); - SASSERT(reward(v) == v_reward); + // SASSERT(reward(v) == v_reward); } DEBUG_CODE( for (auto const& ci : m_clauses) { diff --git a/src/sat/sat_ddfw.h b/src/sat/sat_ddfw.h index 1cad87363..1d28a82c4 100644 --- a/src/sat/sat_ddfw.h +++ b/src/sat/sat_ddfw.h @@ -34,10 +34,10 @@ namespace sat { class ddfw : public i_local_search { struct clause_info { - clause_info(clause* cl, unsigned init_weight): m_weight(init_weight), m_trues(0), m_num_trues(0), m_clause(cl) {} - unsigned m_weight; // weight of clause - unsigned m_trues; // set of literals that are true - unsigned m_num_trues; // size of true set + clause_info(clause* cl, double init_weight): m_weight(init_weight), m_clause(cl) {} + double m_weight; // weight of clause + unsigned m_trues = 0; // set of literals that are true + unsigned m_num_trues = 0; // size of true set clause* m_clause; bool is_true() const { return m_num_trues > 0; } void add(literal lit) { ++m_num_trues; m_trues += lit.index(); } @@ -65,23 +65,24 @@ namespace sat { }; struct var_info { - var_info(): m_value(false), m_reward(0), m_make_count(0), m_bias(0), m_reward_avg(1e-5) {} - bool m_value; - int m_reward; - unsigned m_make_count; - int m_bias; - ema m_reward_avg; + var_info() {} + bool m_value = false; + double m_reward = 0; + unsigned m_make_count = 0; + int m_bias = 0; + ema m_reward_avg = 1e-5; }; - config m_config; - reslimit m_limit; - clause_allocator m_alloc; + config m_config; + reslimit m_limit; + clause_allocator m_alloc; svector m_clauses; literal_vector m_assumptions; svector m_vars; // var -> info svector m_probs; // var -> probability of flipping svector m_scores; // reward -> score model m_model; // var -> best assignment + unsigned m_init_weight = 2; vector m_use_list; unsigned_vector m_flat_use_list; @@ -90,11 +91,11 @@ namespace sat { indexed_uint_set m_unsat; indexed_uint_set m_unsat_vars; // set of variables that are in unsat clauses random_gen m_rand; - unsigned m_num_non_binary_clauses{ 0 }; - unsigned m_restart_count{ 0 }, m_reinit_count{ 0 }, m_parsync_count{ 0 }; - uint64_t m_restart_next{ 0 }, m_reinit_next{ 0 }, m_parsync_next{ 0 }; - uint64_t m_flips{ 0 }, m_last_flips{ 0 }, m_shifts{ 0 }; - unsigned m_min_sz{ 0 }; + unsigned m_num_non_binary_clauses = 0; + unsigned m_restart_count = 0, m_reinit_count = 0, m_parsync_count = 0; + uint64_t m_restart_next = 0, m_reinit_next = 0, m_parsync_next = 0; + uint64_t m_flips = 0, m_last_flips = 0, m_shifts = 0; + unsigned m_min_sz = 0; hashtable> m_models; stopwatch m_stopwatch; @@ -112,9 +113,9 @@ namespace sat { void flatten_use_list(); - double mk_score(unsigned r); + double mk_score(double r); - inline double score(unsigned r) { return r; } // TBD: { for (unsigned sz = m_scores.size(); sz <= r; ++sz) m_scores.push_back(mk_score(sz)); return m_scores[r]; } + inline double score(double r) { return r; } // TBD: { for (unsigned sz = m_scores.size(); sz <= r; ++sz) m_scores.push_back(mk_score(sz)); return m_scores[r]; } inline unsigned num_vars() const { return m_vars.size(); } @@ -124,9 +125,9 @@ namespace sat { inline bool value(bool_var v) const { return m_vars[v].m_value; } - inline int& reward(bool_var v) { return m_vars[v].m_reward; } + inline double& reward(bool_var v) { return m_vars[v].m_reward; } - inline int reward(bool_var v) const { return m_vars[v].m_reward; } + inline double reward(bool_var v) const { return m_vars[v].m_reward; } inline int& bias(bool_var v) { return m_vars[v].m_bias; } @@ -136,7 +137,7 @@ namespace sat { inline clause const& get_clause(unsigned idx) const { return *m_clauses[idx].m_clause; } - inline unsigned get_weight(unsigned idx) const { return m_clauses[idx].m_weight; } + inline double get_weight(unsigned idx) const { return m_clauses[idx].m_weight; } inline bool is_true(unsigned idx) const { return m_clauses[idx].is_true(); } @@ -154,9 +155,9 @@ namespace sat { if (--make_count(v) == 0) m_unsat_vars.remove(v); } - inline void inc_reward(literal lit, int inc) { reward(lit.var()) += inc; } + inline void inc_reward(literal lit, double w) { reward(lit.var()) += w; } - inline void dec_reward(literal lit, int inc) { reward(lit.var()) -= inc; } + inline void dec_reward(literal lit, double w) { reward(lit.var()) -= w; } // flip activity bool do_flip(); @@ -166,17 +167,20 @@ namespace sat { // shift activity void shift_weights(); + inline double calculate_transfer_weight(double w); // reinitialize weights activity bool should_reinit_weights(); void do_reinit_weights(); - inline bool select_clause(unsigned max_weight, unsigned max_trues, clause_info const& cn, unsigned& n); + inline bool select_clause(double max_weight, clause_info const& cn, unsigned& n); // restart activity bool should_restart(); void do_restart(); void reinit_values(); + unsigned select_random_true_clause(); + // parallel integration bool should_parallel_sync(); void do_parallel_sync(); @@ -193,6 +197,10 @@ namespace sat { void add_assumptions(); + inline void transfer_weight(unsigned from, unsigned to, double w); + + inline bool disregard_neighbor(); + public: ddfw(): m_par(nullptr) {} @@ -210,6 +218,10 @@ namespace sat { void set_seed(unsigned n) override { m_rand.set_seed(n); } void add(solver const& s) override; + + void set_bias(bool_var v, int bias) override { m_vars[v].m_bias = bias; } + + bool get_value(bool_var v) const override { return value(v); } std::ostream& display(std::ostream& out) const; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 7cfa102b7..61fc816e1 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1330,17 +1330,37 @@ namespace sat { ERROR_EX }; + struct solver::scoped_ls { + solver& s; + scoped_ls(solver& s): s(s) {} + ~scoped_ls() { + dealloc(s.m_local_search); + s.m_local_search = nullptr; + } + }; + + void solver::bounded_local_search() { + literal_vector _lits; + scoped_limits scoped_rl(rlimit()); + m_local_search = alloc(ddfw); + scoped_ls _ls(*this); + SASSERT(m_local_search); + m_local_search->add(*this); + m_local_search->updt_params(m_params); + m_local_search->set_seed(m_rand()); + scoped_rl.push_child(&(m_local_search->rlimit())); + m_local_search->rlimit().push(500000); + m_local_search->reinit(*this); + m_local_search->check(_lits.size(), _lits.data(), nullptr); + for (unsigned i = 0; i < m_phase.size(); ++i) + m_best_phase[i] = m_local_search->get_value(i); + } + + lbool solver::invoke_local_search(unsigned num_lits, literal const* lits) { literal_vector _lits(num_lits, lits); - for (literal lit : m_user_scope_literals) _lits.push_back(~lit); - struct scoped_ls { - solver& s; - scoped_ls(solver& s): s(s) {} - ~scoped_ls() { - dealloc(s.m_local_search); - s.m_local_search = nullptr; - } - }; + for (literal lit : m_user_scope_literals) + _lits.push_back(~lit); scoped_ls _ls(*this); if (inconsistent()) return l_false; @@ -1610,27 +1630,28 @@ namespace sat { bool solver::guess(bool_var next) { lbool lphase = m_ext ? m_ext->get_phase(next) : l_undef; - + if (lphase != l_undef) return lphase == l_true; switch (m_config.m_phase) { - case PS_ALWAYS_TRUE: - return true; - case PS_ALWAYS_FALSE: - return false; - case PS_BASIC_CACHING: + case PS_ALWAYS_TRUE: + return true; + case PS_ALWAYS_FALSE: + return false; + case PS_BASIC_CACHING: + return m_phase[next]; + case PS_FROZEN: + return m_best_phase[next]; + case PS_SAT_CACHING: + case PS_LOCAL_SEARCH: + if (m_search_state == s_unsat) return m_phase[next]; - case PS_FROZEN: - return m_best_phase[next]; - case PS_SAT_CACHING: - if (m_search_state == s_unsat) - return m_phase[next]; - return m_best_phase[next]; - case PS_RANDOM: - return (m_rand() % 2) == 0; - default: - UNREACHABLE(); - return false; + return m_best_phase[next]; + case PS_RANDOM: + return (m_rand() % 2) == 0; + default: + UNREACHABLE(); + return false; } } @@ -2822,7 +2843,7 @@ namespace sat { } bool solver::is_two_phase() const { - return m_config.m_phase == PS_SAT_CACHING; + return m_config.m_phase == PS_SAT_CACHING || m_config.m_phase == PS_LOCAL_SEARCH; } bool solver::is_sat_phase() const { @@ -2922,6 +2943,10 @@ namespace sat { case PS_RANDOM: for (auto& p : m_phase) p = (m_rand() % 2) == 0; break; + case PS_LOCAL_SEARCH: + if (m_search_state == s_sat) + bounded_local_search(); + break; default: UNREACHABLE(); break; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 227568f3d..524f6b06d 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -589,7 +589,9 @@ namespace sat { lbool do_ddfw_search(unsigned num_lits, literal const* lits); lbool do_prob_search(unsigned num_lits, literal const* lits); lbool invoke_local_search(unsigned num_lits, literal const* lits); + void bounded_local_search(); lbool do_unit_walk(); + struct scoped_ls; // ----------------------- // diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 4e119a2ae..626a3e606 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -91,7 +91,8 @@ namespace sat { virtual model const& get_model() const = 0; virtual void collect_statistics(statistics& st) const = 0; virtual double get_priority(bool_var v) const { return 0; } - + virtual void set_bias(bool_var v, int bias) {} + virtual bool get_value(bool_var v) const { return true; } }; class proof_hint { From 03a4920f3df09ed6ee04dd5f13777fde74ee3a89 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Feb 2023 21:41:07 -0800 Subject: [PATCH 22/22] fix build Signed-off-by: Nikolaj Bjorner --- src/sat/sat_ddfw.h | 2 -- src/sat/sat_types.h | 1 - 2 files changed, 3 deletions(-) diff --git a/src/sat/sat_ddfw.h b/src/sat/sat_ddfw.h index 1d28a82c4..ed9936f0a 100644 --- a/src/sat/sat_ddfw.h +++ b/src/sat/sat_ddfw.h @@ -219,8 +219,6 @@ namespace sat { void add(solver const& s) override; - void set_bias(bool_var v, int bias) override { m_vars[v].m_bias = bias; } - bool get_value(bool_var v) const override { return value(v); } std::ostream& display(std::ostream& out) const; diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 626a3e606..c92a8bbeb 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -91,7 +91,6 @@ namespace sat { virtual model const& get_model() const = 0; virtual void collect_statistics(statistics& st) const = 0; virtual double get_priority(bool_var v) const { return 0; } - virtual void set_bias(bool_var v, int bias) {} virtual bool get_value(bool_var v) const { return true; } };