From 1d0572354b448a29bad4431948850f92ca07e6da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Jan 2020 20:14:12 -0800 Subject: [PATCH] add bit-matrix, avoid flattening and/or after bit-blasting, split pdd_grobner into solver/simplifier, add xlin, add smtfd option for incremental mode logic Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 2 +- src/cmd_context/check_logic.cpp | 8 + src/math/dd/dd_pdd.cpp | 54 ++ src/math/dd/dd_pdd.h | 37 ++ src/math/grobner/CMakeLists.txt | 2 + src/math/grobner/pdd_simplifier.cpp | 574 ++++++++++++++++++ src/math/grobner/pdd_simplifier.h | 55 ++ src/math/grobner/pdd_solver.cpp | 360 +---------- src/math/grobner/pdd_solver.h | 21 +- src/math/simplex/CMakeLists.txt | 1 + src/math/simplex/bit_matrix.cpp | 92 +++ src/math/simplex/bit_matrix.h | 112 ++++ src/sat/sat_solver/inc_sat_solver.cpp | 30 +- src/solver/smt_logics.cpp | 4 +- src/tactic/portfolio/smt_strategic_solver.cpp | 3 + src/test/pdd.cpp | 15 + src/test/pdd_solver.cpp | 7 + 17 files changed, 991 insertions(+), 386 deletions(-) create mode 100644 src/math/grobner/pdd_simplifier.cpp create mode 100644 src/math/grobner/pdd_simplifier.h create mode 100644 src/math/simplex/bit_matrix.cpp create mode 100644 src/math/simplex/bit_matrix.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 93ceab484..e926862a6 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -33,7 +33,7 @@ def init_project_def(): add_lib('tactic', ['ast', 'model']) add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution') add_lib('parser_util', ['ast'], 'parsers/util') - add_lib('grobner', ['ast', 'dd'], 'math/grobner') + add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner') add_lib('euclid', ['util'], 'math/euclid') add_lib('proofs', ['rewriter', 'util'], 'ast/proofs') add_lib('solver', ['model', 'tactic', 'proofs']) diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index 35bbde2b2..419970a19 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -197,6 +197,14 @@ struct check_logic::imp { m_dt = true; m_nonlinear = true; // non-linear 0-1 variables may get eliminated } + else if (logic == "SMTFD") { + m_bvs = true; + m_uf = true; + m_arrays = true; + m_ints = false; + m_dt = false; + m_nonlinear = false; + } else { m_unknown_logic = true; } diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 0dd13b7a6..f3488f0b1 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -1007,4 +1007,58 @@ namespace dd { std::ostream& operator<<(std::ostream& out, pdd const& b) { return b.display(out); } + void pdd_iterator::next() { + auto& m = m_pdd.m; + while (!m_nodes.empty()) { + auto& p = m_nodes.back(); + if (p.first && !m.is_val(p.second)) { + p.first = false; + m_mono.vars.pop_back(); + unsigned n = m.lo(p.second); + if (m.is_val(n) && m.val(n).is_zero()) { + m_nodes.pop_back(); + continue; + } + while (!m.is_val(n)) { + m_nodes.push_back(std::make_pair(true, n)); + m_mono.vars.push_back(m.var(n)); + n = m.hi(n); + } + m_mono.coeff = m.val(n); + break; + } + else { + m_nodes.pop_back(); + } + } + } + + void pdd_iterator::first() { + unsigned n = m_pdd.root; + auto& m = m_pdd.m; + while (!m.is_val(n)) { + m_nodes.push_back(std::make_pair(true, n)); + m_mono.vars.push_back(m.var(n)); + n = m.hi(n); + } + m_mono.coeff = m.val(n); + } + + pdd_iterator pdd::begin() const { return pdd_iterator(*this, true); } + pdd_iterator pdd::end() const { return pdd_iterator(*this, false); } + + std::ostream& operator<<(std::ostream& out, pdd_monomial const& m) { + if (!m.coeff.is_one()) { + out << m.coeff; + if (!m.vars.empty()) out << "*"; + } + bool first = true; + for (auto v : m.vars) { + if (first) first = false; else out << "*"; + out << "v" << v; + } + return out; + } + + } diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 73a083a32..9a7c337e9 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -39,12 +39,15 @@ Author: namespace dd { class pdd; + class pdd_manager; + class pdd_iterator; class pdd_manager { public: enum semantics { free_e, mod2_e, zero_one_vars_e }; private: friend pdd; + friend pdd_iterator; typedef unsigned PDD; typedef vector> monomials_t; @@ -241,6 +244,8 @@ namespace dd { pdd_manager(unsigned nodes, semantics s = free_e); ~pdd_manager(); + semantics get_semantics() const { return m_semantics; } + void reset(unsigned_vector const& level2var); void set_max_num_nodes(unsigned n) { m_max_num_nodes = n; } unsigned_vector const& get_level2var() const { return m_level2var; } @@ -274,6 +279,7 @@ namespace dd { bool lt(pdd const& a, pdd const& b); bool different_leading_term(pdd const& a, pdd const& b); double tree_size(pdd const& p); + unsigned num_vars() const { return m_var2pdd.size(); } unsigned_vector const& free_vars(pdd const& p); @@ -285,6 +291,7 @@ namespace dd { class pdd { friend class pdd_manager; + friend class pdd_iterator; unsigned root; pdd_manager& m; pdd(unsigned root, pdd_manager& m): root(root), m(m) { m.inc_ref(root); } @@ -303,6 +310,7 @@ namespace dd { bool is_val() const { return m.is_val(root); } bool is_zero() const { return m.is_zero(root); } bool is_linear() const { return m.is_linear(root); } + bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } bool is_binary() const { return m.is_binary(root); } bool is_monomial() const { return m.is_monomial(root); } bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); } @@ -330,6 +338,11 @@ namespace dd { unsigned dag_size() const { return m.dag_size(*this); } double tree_size() const { return m.tree_size(*this); } unsigned degree() const { return m.degree(*this); } + unsigned_vector const& free_vars() const { return m.free_vars(*this); } + + + pdd_iterator begin() const; + pdd_iterator end() const; }; inline pdd operator*(rational const& r, pdd const& b) { return b * r; } @@ -353,6 +366,30 @@ namespace dd { std::ostream& operator<<(std::ostream& out, pdd const& b); + struct pdd_monomial { + rational coeff; + unsigned_vector vars; + }; + + std::ostream& operator<<(std::ostream& out, pdd_monomial const& m); + + class pdd_iterator { + friend class pdd; + pdd m_pdd; + svector> m_nodes; + pdd_monomial m_mono; + pdd_iterator(pdd const& p, bool at_start): m_pdd(p) { if (at_start) first(); } + void first(); + void next(); + public: + pdd_monomial const& operator*() const { return m_mono; } + pdd_monomial const* operator->() const { return &m_mono; } + pdd_iterator& operator++() { next(); return *this; } + pdd_iterator operator++(int) { auto tmp = *this; next(); return tmp; } + bool operator==(pdd_iterator const& other) const { return m_nodes == other.m_nodes; } + bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; } + }; + } diff --git a/src/math/grobner/CMakeLists.txt b/src/math/grobner/CMakeLists.txt index a194d4b18..84cc9762c 100644 --- a/src/math/grobner/CMakeLists.txt +++ b/src/math/grobner/CMakeLists.txt @@ -1,8 +1,10 @@ z3_add_component(grobner SOURCES grobner.cpp + pdd_simplifier.cpp pdd_solver.cpp COMPONENT_DEPENDENCIES ast dd + simplex ) diff --git a/src/math/grobner/pdd_simplifier.cpp b/src/math/grobner/pdd_simplifier.cpp new file mode 100644 index 000000000..285e9c668 --- /dev/null +++ b/src/math/grobner/pdd_simplifier.cpp @@ -0,0 +1,574 @@ +/*++ + Copyright (c) 2020 Microsoft Corporation + + + Abstract: + + simplification routines for pdd polys + + Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + + Notes: + + + Linear Elimination: + - comprises of a simplification pass that puts linear equations in to_processed + - so before simplifying with respect to the variable ordering, eliminate linear equalities. + + Extended Linear Simplification (as exploited in Bosphorus AAAI 2019): + - multiply each polynomial by one variable from their orbits. + - The orbit of a varible are the variables that occur in the same monomial as it in some polynomial. + - The extended set of polynomials is fed to a linear Gauss Jordan Eliminator that extracts + additional linear equalities. + - Bosphorus uses M4RI to perform efficient GJE to scale on large bit-matrices. + + Long distance vanishing polynomials (used by PolyCleaner ICCAD 2019): + - identify polynomials p, q, such that p*q = 0 + - main case is half-adders and full adders (p := x + y, q := x * y) over GF2 + because (x+y)*x*y = 0 over GF2 + To work beyond GF2 we would need to rely on simplification with respect to asserted equalities. + The method seems rather specific to hardware multipliers so not clear it is useful to + generalize. + - find monomials that contain pairs of vanishing polynomials, transitively + withtout actually inlining. + Then color polynomial variables w by p, resp, q if they occur in polynomial equalities + w - r = 0, such that all paths in r contain a node colored by p, resp q. + polynomial variables that get colored by both p and q can be set to 0. + When some variable gets colored, other variables can be colored. + - We can walk pdd nodes by level to perform coloring in a linear sweep. + PDD nodes that are equal to 0 using some equality are marked as definitions. + First walk definitions to search for vanishing polynomial pairs. + Given two definition polynomials d1, d2, it must be the case that + level(lo(d1)) = level(lo(d1)) for the polynomial lo(d1)*lo(d2) to be vanishing. + Then starting from the lowest level examine pdd nodes. + Let the current node be called p, check if the pdd node p is used in an equation + w - r = 0. In which case, w inherits the labels from r. + Otherwise, label the node by the intersection of vanishing polynomials from lo(p) and hi(p). + + Eliminating multiplier variables, but not adders [Kaufmann et al FMCAD 2019 for GF2]; + - Only apply GB saturation with respect to variables that are part of multipliers. + - Perhaps this amounts to figuring out whether a variable is used in an xor or more + + --*/ +#pragma once + +#include "math/grobner/pdd_simplifier.h" +#include "math/simplex/bit_matrix.h" +#include "util/uint_set.h" + +namespace dd { + + + void simplifier::operator()() { + try { + while (!s.done() && + (simplify_linear_step(true) || + simplify_elim_pure_step() || + simplify_cc_step() || + simplify_leaf_step() || + simplify_linear_step(false) || + /*simplify_elim_dual_step() ||*/ + simplify_exlin() || + false)) { + DEBUG_CODE(s.invariant();); + TRACE("dd.solver", s.display(tout);); + } + } + catch (pdd_manager::mem_out) { + // done reduce + DEBUG_CODE(s.invariant();); + } + } + + struct simplifier::compare_top_var { + bool operator()(equation* a, equation* b) const { + return a->poly().var() < b->poly().var(); + } + }; + + bool simplifier::simplify_linear_step(bool binary) { + TRACE("dd.solver", tout << "binary " << binary << "\n";); + IF_VERBOSE(2, verbose_stream() << "binary " << binary << "\n"); + equation_vector linear; + for (equation* e : s.m_to_simplify) { + pdd p = e->poly(); + if (binary) { + if (p.is_binary()) linear.push_back(e); + } + else if (p.is_linear()) { + linear.push_back(e); + } + } + return simplify_linear_step(linear); + } + + /** + \brief simplify linear equations by using top variable as solution. + The linear equation is moved to set of solved equations. + */ + bool simplifier::simplify_linear_step(equation_vector& linear) { + if (linear.empty()) return false; + use_list_t use_list = get_use_list(); + compare_top_var ctv; + std::stable_sort(linear.begin(), linear.end(), ctv); + equation_vector trivial; + unsigned j = 0; + bool has_conflict = false; + for (equation* src : linear) { + if (has_conflict) { + break; + } + unsigned v = src->poly().var(); + equation_vector const& uses = use_list[v]; + TRACE("dd.solver", + s.display(tout << "uses of: ", *src) << "\n"; + for (equation* e : uses) { + s.display(tout, *e) << "\n"; + }); + bool changed_leading_term; + bool all_reduced = true; + for (equation* dst : uses) { + if (src == dst || s.is_trivial(*dst)) { + continue; + } + pdd q = dst->poly(); + if (!src->poly().is_binary() && !q.is_linear()) { + all_reduced = false; + continue; + } + remove_from_use(dst, use_list, v); + s.simplify_using(*dst, *src, changed_leading_term); + if (s.is_trivial(*dst)) { + trivial.push_back(dst); + } + else if (s.is_conflict(dst)) { + s.pop_equation(dst); + s.set_conflict(dst); + has_conflict = true; + } + else if (changed_leading_term) { + s.pop_equation(dst); + s.push_equation(solver::to_simplify, dst); + } + // v has been eliminated. + SASSERT(!dst->poly().free_vars().contains(v)); + add_to_use(dst, use_list); + } + if (all_reduced) { + linear[j++] = src; + } + } + if (!has_conflict) { + linear.shrink(j); + for (equation* src : linear) { + s.pop_equation(src); + s.push_equation(solver::solved, src); + } + } + for (equation* e : trivial) { + s.del_equation(e); + } + DEBUG_CODE(s.invariant();); + return j > 0 || has_conflict; + } + + /** + \brief simplify using congruences + replace pair px + q and ry + q by + px + q, px - ry + since px = ry + */ + bool simplifier::simplify_cc_step() { + TRACE("dd.solver", tout << "cc\n";); + IF_VERBOSE(2, verbose_stream() << "cc\n"); + u_map los; + bool reduced = false; + unsigned j = 0; + for (equation* eq1 : s.m_to_simplify) { + SASSERT(eq1->state() == solver::to_simplify); + pdd p = eq1->poly(); + auto* e = los.insert_if_not_there2(p.lo().index(), eq1); + equation* eq2 = e->get_data().m_value; + pdd q = eq2->poly(); + if (eq2 != eq1 && (p.hi().is_val() || q.hi().is_val()) && !p.lo().is_val()) { + *eq1 = p - eq2->poly(); + *eq1 = s.m_dep_manager.mk_join(eq1->dep(), eq2->dep()); + reduced = true; + if (s.is_trivial(*eq1)) { + s.retire(eq1); + continue; + } + else if (s.check_conflict(*eq1)) { + continue; + } + } + s.m_to_simplify[j] = eq1; + eq1->set_index(j++); + } + s.m_to_simplify.shrink(j); + return reduced; + } + + /** + \brief remove ax+b from p if x occurs as a leaf in p and a is a constant. + */ + bool simplifier::simplify_leaf_step() { + TRACE("dd.solver", tout << "leaf\n";); + IF_VERBOSE(2, verbose_stream() << "leaf\n"); + use_list_t use_list = get_use_list(); + equation_vector leaves; + for (unsigned i = 0; i < s.m_to_simplify.size(); ++i) { + equation* e = s.m_to_simplify[i]; + pdd p = e->poly(); + if (!p.hi().is_val()) { + continue; + } + leaves.reset(); + for (equation* e2 : use_list[p.var()]) { + if (e != e2 && e2->poly().var_is_leaf(p.var())) { + leaves.push_back(e2); + } + } + for (equation* e2 : leaves) { + bool changed_leading_term; + remove_from_use(e2, use_list); + s.simplify_using(*e2, *e, changed_leading_term); + add_to_use(e2, use_list); + if (s.is_trivial(*e2)) { + s.pop_equation(e2); + s.retire(e2); + } + else if (e2->poly().is_val()) { + s.pop_equation(e2); + s.set_conflict(*e2); + return true; + } + else if (changed_leading_term) { + s.pop_equation(e2); + s.push_equation(solver::to_simplify, e2); + } + } + } + return false; + } + + /** + \brief treat equations as processed if top variable occurs only once. + */ + bool simplifier::simplify_elim_pure_step() { + TRACE("dd.solver", tout << "pure\n";); + IF_VERBOSE(2, verbose_stream() << "pure\n"); + use_list_t use_list = get_use_list(); + unsigned j = 0; + for (equation* e : s.m_to_simplify) { + pdd p = e->poly(); + if (!p.is_val() && p.hi().is_val() && use_list[p.var()].size() == 1) { + s.push_equation(solver::solved, e); + } + else { + s.m_to_simplify[j] = e; + e->set_index(j++); + } + } + if (j != s.m_to_simplify.size()) { + s.m_to_simplify.shrink(j); + return true; + } + return false; + } + + /** + \brief + reduce equations where top variable occurs only twice and linear in one of the occurrences. + */ + bool simplifier::simplify_elim_dual_step() { + use_list_t use_list = get_use_list(); + unsigned j = 0; + bool reduced = false; + for (unsigned i = 0; i < s.m_to_simplify.size(); ++i) { + equation* e = s.m_to_simplify[i]; + pdd p = e->poly(); + // check that e is linear in top variable. + if (e->state() != solver::to_simplify) { + reduced = true; + } + else if (!s.done() && !s.is_trivial(*e) && p.hi().is_val() && use_list[p.var()].size() == 2) { + for (equation* e2 : use_list[p.var()]) { + if (e2 == e) continue; + bool changed_leading_term; + + remove_from_use(e2, use_list); + s.simplify_using(*e2, *e, changed_leading_term); + if (s.is_conflict(e2)) { + s.pop_equation(e2); + s.set_conflict(e2); + } + // when e2 is trivial, leading term is changed + SASSERT(!s.is_trivial(*e2) || changed_leading_term); + if (changed_leading_term) { + s.pop_equation(e2); + s.push_equation(solver::to_simplify, e2); + } + add_to_use(e2, use_list); + break; + } + reduced = true; + s.push_equation(solver::solved, e); + } + else { + s.m_to_simplify[j] = e; + e->set_index(j++); + } + } + if (reduced) { + // clean up elements in s.m_to_simplify + // they may have moved. + s.m_to_simplify.shrink(j); + j = 0; + for (equation* e : s.m_to_simplify) { + if (s.is_trivial(*e)) { + s.retire(e); + } + else if (e->state() == solver::to_simplify) { + s.m_to_simplify[j] = e; + e->set_index(j++); + } + } + s.m_to_simplify.shrink(j); + return true; + } + else { + return false; + } + } + + void simplifier::add_to_use(equation* e, use_list_t& use_list) { + unsigned_vector const& fv = e->poly().free_vars(); + for (unsigned v : fv) { + use_list.reserve(v + 1); + use_list[v].push_back(e); + } + } + + void simplifier::remove_from_use(equation* e, use_list_t& use_list) { + unsigned_vector const& fv = e->poly().free_vars(); + for (unsigned v : fv) { + use_list.reserve(v + 1); + use_list[v].erase(e); + } + } + + void simplifier::remove_from_use(equation* e, use_list_t& use_list, unsigned except_v) { + unsigned_vector const& fv = e->poly().free_vars(); + for (unsigned v : fv) { + if (v != except_v) { + use_list.reserve(v + 1); + use_list[v].erase(e); + } + } + } + + simplifier::use_list_t simplifier::get_use_list() { + use_list_t use_list; + for (equation * e : s.m_to_simplify) { + add_to_use(e, use_list); + } + for (equation * e : s.m_processed) { + add_to_use(e, use_list); + } + return use_list; + } + + + /** + \brief use Gauss elimination to extract linear equalities. + So far just for GF(2) semantics. + */ + + bool simplifier::simplify_exlin() { + if (s.m.get_semantics() != pdd_manager::mod2_e || + !s.m_config.m_enable_exlin) { + return false; + } + vector eqs, simp_eqs; + for (auto* e : s.m_to_simplify) if (!e->dep()) eqs.push_back(e->poly()); + for (auto* e : s.m_processed) if (!e->dep()) eqs.push_back(e->poly()); + exlin_augment(eqs); + simplify_exlin(eqs, simp_eqs); + for (pdd const& p : simp_eqs) { + s.add(p); + } + return !simp_eqs.empty() && simplify_linear_step(false); + } + + /** + augment set of equations by multiplying with selected variables. + Uses orbits to prune which variables are multiplied. + TBD: could also prune added polynomials based on a maximal degree. + */ + void simplifier::exlin_augment(vector& eqs) { + unsigned nv = s.m.num_vars(); + vector orbits(nv); + random_gen rand(s.m_config.m_random_seed); + unsigned modest_num_eqs = std::min(eqs.size(), 500u); + unsigned max_xlin_eqs = modest_num_eqs*modest_num_eqs + eqs.size(); + for (pdd p : eqs) { + auto const& fv = p.free_vars(); + for (unsigned i = fv.size(); i-- > 0; ) { + for (unsigned j = i; j-- > 0; ) { + orbits[fv[i]].insert(fv[j]); + orbits[fv[j]].insert(fv[i]); + } + } + } + TRACE("dd.solver", tout << "augment " << nv << "\n"; + for (auto const& o : orbits) tout << o.num_elems() << "\n"; + ); + vector n_eqs; + unsigned start = rand(); + for (unsigned _v = 0; _v < nv; ++_v) { + unsigned v = (_v + start) % nv; + auto const& orbitv = orbits[v]; + if (orbitv.empty()) continue; + pdd pv = s.m.mk_var(v); + for (pdd p : eqs) { + for (unsigned w : p.free_vars()) { + if (orbitv.contains(w)) { + n_eqs.push_back(pv * p); + break; + } + } + if (n_eqs.size() > max_xlin_eqs) { + goto end_of_new_eqs; + } + } + } + + start = rand(); + for (unsigned _v = 0; _v < nv; ++_v) { + unsigned v = (_v + start) % nv; + auto const& orbitv = orbits[v]; + if (orbitv.empty()) continue; + pdd pv = s.m.mk_var(v); + for (unsigned w : orbitv) { + if (v > w) continue; + pdd pw = s.m.mk_var(w); + for (pdd p : eqs) { + if (n_eqs.size() > max_xlin_eqs) { + goto end_of_new_eqs; + } + for (unsigned u : p.free_vars()) { + if (orbits[w].contains(u) || orbits[v].contains(u)) { + n_eqs.push_back(pw * pv * p); + break; + } + } + } + } + } + end_of_new_eqs: + s.m_config.m_random_seed = rand(); + eqs.append(n_eqs); + TRACE("dd.solver", for (pdd const& p : eqs) tout << p << "\n";); + } + + void simplifier::simplify_exlin(vector const& eqs, vector& simp_eqs) { + + // create variables for each non-constant monomial. + u_map mon2idx; + vector idx2mon; + + // insert monomials of degree > 1 + for (pdd const& p : eqs) { + for (auto const& m : p) { + if (m.vars.size() <= 1) continue; + pdd r = s.m.mk_val(m.coeff); + for (unsigned i = m.vars.size(); i-- > 0; ) + r *= s.m.mk_var(m.vars[i]); + if (!mon2idx.contains(r.index())) { + mon2idx.insert(r.index(), idx2mon.size()); + idx2mon.push_back(r); + } + } + } + + // insert variables last. + unsigned nv = s.m.num_vars(); + for (unsigned v = 0; v < nv; ++v) { + pdd r = s.m.mk_var(v); + mon2idx.insert(r.index(), idx2mon.size()); + idx2mon.push_back(r); + } + + bit_matrix bm; + unsigned const_idx = idx2mon.size(); + bm.reset(const_idx + 1); + + // populate rows + for (pdd const& p : eqs) { + if (p.is_zero()) { + continue; + } + auto row = bm.add_row(); + for (auto const& m : p) { + SASSERT(m.coeff.is_one()); + if (m.vars.empty()) { + row.set(const_idx); + continue; + } + pdd r = s.m.one(); + for (unsigned i = m.vars.size(); i-- > 0; ) + r *= s.m.mk_var(m.vars[i]); + unsigned v = mon2idx[r.index()]; + row.set(v); + } + } + + TRACE("dd.solver", tout << bm << "\n";); + + bm.solve(); + + TRACE("dd.solver", tout << bm << "\n";); + + for (auto const& r : bm) { + bool is_linear = true; + for (unsigned c : r) { + SASSERT(r[c]); + if (c == const_idx) { + break; + } + pdd const& p = idx2mon[c]; + if (!p.is_unary()) { + is_linear = false; + break; + } + } + + if (is_linear) { + pdd p = s.m.zero(); + for (unsigned c : r) { + if (c == const_idx) { + p += s.m.one(); + } + else { + p += idx2mon[c]; + } + } + if (!p.is_zero()) { + TRACE("dd.solver", tout << "new linear: " << p << "\n";); + simp_eqs.push_back(p); + } + } + + // could also consider singleton monomials as Bosphorus does + // Singleton monomials are of the form v*w*u*v == 0 + // Generally want to deal with negations too + // v*(w+1)*u will have shared pdd under w, + // e.g, test every variable in p whether it has hi() == lo(). + // maybe easier to read out of a pdd than the expanded form. + } + } + +} diff --git a/src/math/grobner/pdd_simplifier.h b/src/math/grobner/pdd_simplifier.h new file mode 100644 index 000000000..08c4b4756 --- /dev/null +++ b/src/math/grobner/pdd_simplifier.h @@ -0,0 +1,55 @@ +/*++ + Copyright (c) 2017 Microsoft Corporation + + + Abstract: + + simplification routines for pdd polys + + Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + + --*/ +#pragma once + +#include "math/grobner/pdd_solver.h" + +namespace dd { + +class simplifier { + + typedef solver::equation equation; + typedef ptr_vector equation_vector; + + solver& s; +public: + + simplifier(solver& s): s(s) {} + ~simplifier() {} + + void operator()(); + +private: + + struct compare_top_var; + bool simplify_linear_step(bool binary); + bool simplify_linear_step(equation_vector& linear); + typedef vector use_list_t; + use_list_t get_use_list(); + void add_to_use(equation* e, use_list_t& use_list); + void remove_from_use(equation* e, use_list_t& use_list); + void remove_from_use(equation* e, use_list_t& use_list, unsigned except_v); + + bool simplify_cc_step(); + bool simplify_elim_pure_step(); + bool simplify_elim_dual_step(); + bool simplify_leaf_step(); + bool simplify_exlin(); + void exlin_augment(vector& eqs); + void simplify_exlin(vector const& eqs, vector& simp_eqs); + + +}; + +} diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp index ed1ba733a..b1bfa281e 100644 --- a/src/math/grobner/pdd_solver.cpp +++ b/src/math/grobner/pdd_solver.cpp @@ -12,8 +12,10 @@ --*/ #include "math/grobner/pdd_solver.h" +#include "math/grobner/pdd_simplifier.h" #include "util/uint_set.h" + namespace dd { /*** @@ -71,47 +73,6 @@ namespace dd { Justification: - elements in S have no variables watched - elements in A are always reduced modulo all variables above the current x_i. - - - TBD: - - Linear Elimination: - - comprises of a simplification pass that puts linear equations in to_processed - - so before simplifying with respect to the variable ordering, eliminate linear equalities. - - Extended Linear Simplification (as exploited in Bosphorus AAAI 2019): - - multiply each polynomial by one variable from their orbits. - - The orbit of a varible are the variables that occur in the same monomial as it in some polynomial. - - The extended set of polynomials is fed to a linear Gauss Jordan Eliminator that extracts - additional linear equalities. - - Bosphorus uses M4RI to perform efficient GJE to scale on large bit-matrices. - - Long distance vanishing polynomials (used by PolyCleaner ICCAD 2019): - - identify polynomials p, q, such that p*q = 0 - - main case is half-adders and full adders (p := x + y, q := x * y) over GF2 - because (x+y)*x*y = 0 over GF2 - To work beyond GF2 we would need to rely on simplification with respect to asserted equalities. - The method seems rather specific to hardware multipliers so not clear it is useful to - generalize. - - find monomials that contain pairs of vanishing polynomials, transitively - withtout actually inlining. - Then color polynomial variables w by p, resp, q if they occur in polynomial equalities - w - r = 0, such that all paths in r contain a node colored by p, resp q. - polynomial variables that get colored by both p and q can be set to 0. - When some variable gets colored, other variables can be colored. - - We can walk pdd nodes by level to perform coloring in a linear sweep. - PDD nodes that are equal to 0 using some equality are marked as definitions. - First walk definitions to search for vanishing polynomial pairs. - Given two definition polynomials d1, d2, it must be the case that - level(lo(d1)) = level(lo(d1)) for the polynomial lo(d1)*lo(d2) to be vanishing. - Then starting from the lowest level examine pdd nodes. - Let the current node be called p, check if the pdd node p is used in an equation - w - r = 0. In which case, w inherits the labels from r. - Otherwise, label the node by the intersection of vanishing polynomials from lo(p) and hi(p). - - Eliminating multiplier variables, but not adders [Kaufmann et al FMCAD 2019 for GF2]; - - Only apply GB saturation with respect to variables that are part of multipliers. - - Perhaps this amounts to figuring out whether a variable is used in an xor or more */ @@ -165,323 +126,10 @@ namespace dd { } void solver::simplify() { - try { - while (!done() && - (simplify_linear_step(true) || - simplify_elim_pure_step() || - simplify_cc_step() || - simplify_leaf_step() || - simplify_linear_step(false) || - /*simplify_elim_dual_step() ||*/ - false)) { - DEBUG_CODE(invariant();); - TRACE("dd.solver", display(tout);); - } - } - catch (pdd_manager::mem_out) { - // done reduce - DEBUG_CODE(invariant();); - } + simplifier s(*this); + s(); } - struct solver::compare_top_var { - bool operator()(equation* a, equation* b) const { - return a->poly().var() < b->poly().var(); - } - }; - - bool solver::simplify_linear_step(bool binary) { - TRACE("dd.solver", tout << "binary " << binary << "\n";); - IF_VERBOSE(2, verbose_stream() << "binary " << binary << "\n"); - equation_vector linear; - for (equation* e : m_to_simplify) { - pdd p = e->poly(); - if (binary) { - if (p.is_binary()) linear.push_back(e); - } - else if (p.is_linear()) { - linear.push_back(e); - } - } - return simplify_linear_step(linear); - } - - /** - \brief simplify linear equations by using top variable as solution. - The linear equation is moved to set of solved equations. - */ - bool solver::simplify_linear_step(equation_vector& linear) { - if (linear.empty()) return false; - use_list_t use_list = get_use_list(); - compare_top_var ctv; - std::stable_sort(linear.begin(), linear.end(), ctv); - equation_vector trivial; - unsigned j = 0; - bool has_conflict = false; - for (equation* src : linear) { - if (has_conflict) { - break; - } - unsigned v = src->poly().var(); - equation_vector const& uses = use_list[v]; - TRACE("dd.solver", - display(tout << "uses of: ", *src) << "\n"; - for (equation* e : uses) { - display(tout, *e) << "\n"; - }); - bool changed_leading_term; - bool all_reduced = true; - for (equation* dst : uses) { - if (src == dst || is_trivial(*dst)) { - continue; - } - pdd q = dst->poly(); - if (!src->poly().is_binary() && !q.is_linear()) { - all_reduced = false; - continue; - } - remove_from_use(dst, use_list, v); - simplify_using(*dst, *src, changed_leading_term); - if (is_trivial(*dst)) { - trivial.push_back(dst); - } - else if (is_conflict(dst)) { - pop_equation(dst); - set_conflict(dst); - has_conflict = true; - } - else if (changed_leading_term) { - pop_equation(dst); - push_equation(to_simplify, dst); - } - // v has been eliminated. - SASSERT(!m.free_vars(dst->poly()).contains(v)); - add_to_use(dst, use_list); - } - if (all_reduced) { - linear[j++] = src; - } - } - if (!has_conflict) { - linear.shrink(j); - for (equation* src : linear) { - pop_equation(src); - push_equation(solved, src); - } - } - for (equation* e : trivial) { - del_equation(e); - } - DEBUG_CODE(invariant();); - return j > 0 || has_conflict; - } - - /** - \brief simplify using congruences - replace pair px + q and ry + q by - px + q, px - ry - since px = ry - */ - bool solver::simplify_cc_step() { - TRACE("dd.solver", tout << "cc\n";); - IF_VERBOSE(2, verbose_stream() << "cc\n"); - u_map los; - bool reduced = false; - unsigned j = 0; - for (equation* eq1 : m_to_simplify) { - SASSERT(eq1->state() == to_simplify); - pdd p = eq1->poly(); - auto* e = los.insert_if_not_there2(p.lo().index(), eq1); - equation* eq2 = e->get_data().m_value; - pdd q = eq2->poly(); - if (eq2 != eq1 && (p.hi().is_val() || q.hi().is_val()) && !p.lo().is_val()) { - *eq1 = p - eq2->poly(); - *eq1 = m_dep_manager.mk_join(eq1->dep(), eq2->dep()); - reduced = true; - if (is_trivial(*eq1)) { - retire(eq1); - continue; - } - else if (check_conflict(*eq1)) { - continue; - } - } - m_to_simplify[j] = eq1; - eq1->set_index(j++); - } - m_to_simplify.shrink(j); - return reduced; - } - - /** - \brief remove ax+b from p if x occurs as a leaf in p and a is a constant. - */ - bool solver::simplify_leaf_step() { - TRACE("dd.solver", tout << "leaf\n";); - IF_VERBOSE(2, verbose_stream() << "leaf\n"); - use_list_t use_list = get_use_list(); - equation_vector leaves; - for (unsigned i = 0; i < m_to_simplify.size(); ++i) { - equation* e = m_to_simplify[i]; - pdd p = e->poly(); - if (!p.hi().is_val()) { - continue; - } - leaves.reset(); - for (equation* e2 : use_list[p.var()]) { - if (e != e2 && e2->poly().var_is_leaf(p.var())) { - leaves.push_back(e2); - } - } - for (equation* e2 : leaves) { - bool changed_leading_term; - remove_from_use(e2, use_list); - simplify_using(*e2, *e, changed_leading_term); - add_to_use(e2, use_list); - if (is_trivial(*e2)) { - pop_equation(e2); - retire(e2); - } - else if (e2->poly().is_val()) { - pop_equation(e2); - set_conflict(*e2); - return true; - } - else if (changed_leading_term) { - pop_equation(e2); - push_equation(to_simplify, e2); - } - } - } - return false; - } - - /** - \brief treat equations as processed if top variable occurs only once. - */ - bool solver::simplify_elim_pure_step() { - TRACE("dd.solver", tout << "pure\n";); - IF_VERBOSE(2, verbose_stream() << "pure\n"); - use_list_t use_list = get_use_list(); - unsigned j = 0; - for (equation* e : m_to_simplify) { - pdd p = e->poly(); - if (!p.is_val() && p.hi().is_val() && use_list[p.var()].size() == 1) { - push_equation(solved, e); - } - else { - m_to_simplify[j] = e; - e->set_index(j++); - } - } - if (j != m_to_simplify.size()) { - m_to_simplify.shrink(j); - return true; - } - return false; - } - - /** - \brief - reduce equations where top variable occurs only twice and linear in one of the occurrences. - */ - bool solver::simplify_elim_dual_step() { - use_list_t use_list = get_use_list(); - unsigned j = 0; - bool reduced = false; - for (unsigned i = 0; i < m_to_simplify.size(); ++i) { - equation* e = m_to_simplify[i]; - pdd p = e->poly(); - // check that e is linear in top variable. - if (e->state() != to_simplify) { - reduced = true; - } - else if (!done() && !is_trivial(*e) && p.hi().is_val() && use_list[p.var()].size() == 2) { - for (equation* e2 : use_list[p.var()]) { - if (e2 == e) continue; - bool changed_leading_term; - - remove_from_use(e2, use_list); - simplify_using(*e2, *e, changed_leading_term); - if (is_conflict(e2)) { - pop_equation(e2); - set_conflict(e2); - } - // when e2 is trivial, leading term is changed - SASSERT(!is_trivial(*e2) || changed_leading_term); - if (changed_leading_term) { - pop_equation(e2); - push_equation(to_simplify, e2); - } - add_to_use(e2, use_list); - break; - } - reduced = true; - push_equation(solved, e); - } - else { - m_to_simplify[j] = e; - e->set_index(j++); - } - } - if (reduced) { - // clean up elements in m_to_simplify - // they may have moved. - m_to_simplify.shrink(j); - j = 0; - for (equation* e : m_to_simplify) { - if (is_trivial(*e)) { - retire(e); - } - else if (e->state() == to_simplify) { - m_to_simplify[j] = e; - e->set_index(j++); - } - } - m_to_simplify.shrink(j); - return true; - } - else { - return false; - } - } - - void solver::add_to_use(equation* e, use_list_t& use_list) { - unsigned_vector const& fv = m.free_vars(e->poly()); - for (unsigned v : fv) { - use_list.reserve(v + 1); - use_list[v].push_back(e); - } - } - - void solver::remove_from_use(equation* e, use_list_t& use_list) { - unsigned_vector const& fv = m.free_vars(e->poly()); - for (unsigned v : fv) { - use_list.reserve(v + 1); - use_list[v].erase(e); - } - } - - void solver::remove_from_use(equation* e, use_list_t& use_list, unsigned except_v) { - unsigned_vector const& fv = m.free_vars(e->poly()); - for (unsigned v : fv) { - if (v != except_v) { - use_list.reserve(v + 1); - use_list[v].erase(e); - } - } - } - - solver::use_list_t solver::get_use_list() { - use_list_t use_list; - for (equation * e : m_to_simplify) { - add_to_use(e, use_list); - } - for (equation * e : m_processed) { - add_to_use(e, use_list); - } - return use_list; - } void solver::superpose(equation const & eq) { for (equation* target : m_processed) { diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h index e3a2fe398..8ff6486ed 100644 --- a/src/math/grobner/pdd_solver.h +++ b/src/math/grobner/pdd_solver.h @@ -29,6 +29,7 @@ namespace dd { class solver { + friend class simplifier; public: struct stats { unsigned m_simplified; @@ -44,10 +45,14 @@ public: unsigned m_eqs_threshold; unsigned m_expr_size_limit; unsigned m_max_steps; + unsigned m_random_seed; + bool m_enable_exlin; config() : m_eqs_threshold(UINT_MAX), m_expr_size_limit(UINT_MAX), - m_max_steps(UINT_MAX) + m_max_steps(UINT_MAX), + m_random_seed(0), + m_enable_exlin(false) {} }; @@ -160,20 +165,6 @@ private: void push_equation(eq_state st, equation& eq); void push_equation(eq_state st, equation* eq) { push_equation(st, *eq); } - struct compare_top_var; - bool simplify_linear_step(bool binary); - bool simplify_linear_step(equation_vector& linear); - typedef vector use_list_t; - use_list_t get_use_list(); - void add_to_use(equation* e, use_list_t& use_list); - void remove_from_use(equation* e, use_list_t& use_list); - void remove_from_use(equation* e, use_list_t& use_list, unsigned except_v); - - bool simplify_cc_step(); - bool simplify_elim_pure_step(); - bool simplify_elim_dual_step(); - bool simplify_leaf_step(); - void invariant() const; struct scoped_process { solver& g; diff --git a/src/math/simplex/CMakeLists.txt b/src/math/simplex/CMakeLists.txt index de55f1634..3d2d35741 100644 --- a/src/math/simplex/CMakeLists.txt +++ b/src/math/simplex/CMakeLists.txt @@ -2,6 +2,7 @@ z3_add_component(simplex SOURCES simplex.cpp model_based_opt.cpp + bit_matrix.cpp COMPONENT_DEPENDENCIES util ) diff --git a/src/math/simplex/bit_matrix.cpp b/src/math/simplex/bit_matrix.cpp new file mode 100644 index 000000000..42d3d1a84 --- /dev/null +++ b/src/math/simplex/bit_matrix.cpp @@ -0,0 +1,92 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + bit_matrix.cpp + +Author: + + Nikolaj Bjorner (nbjorner) 2020-01-1 + +Notes: + +--*/ + +#include "math/simplex/bit_matrix.h" + + +bit_matrix::col_iterator bit_matrix::row::begin() const { + return bit_matrix::col_iterator(*this, true); +} + +bit_matrix::col_iterator bit_matrix::row::end() const { + return bit_matrix::col_iterator(*this, false); +} + +void bit_matrix::col_iterator::next() { + ++m_column; + while (m_column < r.m.m_num_columns && !r[m_column]) { + while ((m_column % 64) == 0 && m_column + 64 < r.m.m_num_columns && !r.r[m_column >> 6]) { + m_column += 64; + } + ++m_column; + } +} + +bool bit_matrix::row::operator[](unsigned i) const { + SASSERT((i >> 6) < m.m_num_chunks); + return (r[i >> 6] & (1ull << static_cast(i & 63))) != 0; +} + + +std::ostream& bit_matrix::row::display(std::ostream& out) const { + for (unsigned i = 0; i < m.m_num_columns; ++i) { + out << ((*this)[i]?"1":"0"); + } + return out << "\n"; +} + +void bit_matrix::reset(unsigned num_columns) { + m_region.reset(); + m_num_columns = num_columns; + m_num_chunks = (num_columns + 63)/64; +} + +bit_matrix::row bit_matrix::add_row() { + uint64_t* r = new (m_region) uint64_t[m_num_chunks]; + m_rows.push_back(r); + memset(r, 0, sizeof(uint64_t)*m_num_chunks); + return row(*this, r); +} + +bit_matrix::row& bit_matrix::row::operator+=(row const& other) { + for (unsigned i = 0; i < m.m_num_chunks; ++i) { + r[i] ^= other.r[i]; + } + return *this; +} + +void bit_matrix::solve() { + basic_solve(); +} + +void bit_matrix::basic_solve() { + for (row& r : *this) { + auto ci = r.begin(); + if (ci != r.end()) { + unsigned c = *ci; + for (row& r2 : *this) { + if (r2 != r && r2[c]) r2 += r; + } + } + } +} + +std::ostream& bit_matrix::display(std::ostream& out) { + for (row& r : *this) { + out << r; + } + return out; +} + diff --git a/src/math/simplex/bit_matrix.h b/src/math/simplex/bit_matrix.h new file mode 100644 index 000000000..0d81b7249 --- /dev/null +++ b/src/math/simplex/bit_matrix.h @@ -0,0 +1,112 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + bit_matrix.h + +Abstract: + + Dense bit-matrix utilities. + +Author: + + Nikolaj Bjorner (nbjorner) 2020-01-1 + +Notes: + + Exposes Gauss-Jordan simplification. + Uses extremely basic implementation, can be tuned by 4R method. + +--*/ + +#ifndef BIT_MATRIX_H_ +#define BIT_MATRIX_H_ + +#include "util/region.h" +#include "util/vector.h" + +class bit_matrix { + + region m_region; + unsigned m_num_columns; + unsigned m_num_chunks; + ptr_vector m_rows; + +public: + + class col_iterator; + class row_iterator; + class row { + friend row_iterator; + friend bit_matrix; + bit_matrix& m; + uint64_t* r; + row(bit_matrix& m, uint64_t* r):m(m), r(r) {} + public: + col_iterator begin() const; + col_iterator end() const; + bool operator[](unsigned i) const; + void set(unsigned i, bool b) { if (b) set(i); else unset(i); } + void set(unsigned i) { SASSERT((i >> 6) < m.m_num_chunks); r[i >> 6] |= (1ull << (i & 63)); } + void unset(unsigned i) { SASSERT((i >> 6) < m.m_num_chunks); r[i >> 6] &= ~(1ull << (i & 63)); } + row& operator+=(row const& other); + + // using pointer equality: + bool operator==(row const& other) const { return r == other.r; } + bool operator!=(row const& other) const { return r != other.r; } + std::ostream& display(std::ostream& out) const; + }; + + class col_iterator { + friend row; + friend bit_matrix; + row r; + unsigned m_column; + void next(); + col_iterator(row const& r, bool at_first): r(r), m_column(at_first?0:r.m.m_num_columns) { if (at_first && !r[m_column]) next(); } + public: + unsigned const& operator*() const { return m_column; } + unsigned const* operator->() const { return &m_column; } + col_iterator& operator++() { next(); return *this; } + col_iterator operator++(int) { auto tmp = *this; next(); return tmp; } + bool operator==(col_iterator const& other) const { return m_column == other.m_column; } + bool operator!=(col_iterator const& other) const { return m_column != other.m_column; } + }; + + class row_iterator { + friend class bit_matrix; + row m_row; + unsigned m_index; + row_iterator(bit_matrix& m, bool at_first): m_row(m, at_first ? m.m_rows[0] : nullptr), m_index(at_first ? 0 : m.m_rows.size()) {} + void next() { m_index++; if (m_index < m_row.m.m_rows.size()) m_row.r = m_row.m.m_rows[m_index]; } + public: + row const& operator*() const { return m_row; } + row const* operator->() const { return &m_row; } + row& operator*() { return m_row; } + row* operator->() { return &m_row; } + row_iterator& operator++() { next(); return *this; } + row_iterator operator++(int) { auto tmp = *this; next(); return tmp; } + bool operator==(row_iterator const& other) const { return m_index == other.m_index; } + bool operator!=(row_iterator const& other) const { return m_index != other.m_index; } + }; + + bit_matrix() {} + ~bit_matrix() {} + void reset(unsigned num_columns); + + row_iterator begin() { return row_iterator(*this, true); } + row_iterator end() { return row_iterator(*this, false); } + + row add_row(); + void solve(); + std::ostream& display(std::ostream& out); + +private: + void basic_solve(); +}; + +inline std::ostream& operator<<(std::ostream& out, bit_matrix& m) { return m.display(out); } +inline std::ostream& operator<<(std::ostream& out, bit_matrix::row const& r) { return r.display(out); } + +#endif diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index baea99c03..d07a406ba 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -539,25 +539,29 @@ public: if (!m_bb_rewriter) { m_bb_rewriter = alloc(bit_blaster_rewriter, m, m_params); } + params_ref simp1_p = m_params; + simp1_p.set_bool("som", true); + simp1_p.set_bool("pull_cheap_ite", true); + simp1_p.set_bool("push_ite_bv", false); + simp1_p.set_bool("local_ctx", true); + simp1_p.set_uint("local_ctx_limit", 10000000); + simp1_p.set_bool("flat", true); // required by som + simp1_p.set_bool("hoist_mul", false); // required by som + simp1_p.set_bool("elim_and", true); + simp1_p.set_bool("blast_distinct", true); + params_ref simp2_p = m_params; - simp2_p.set_bool("som", true); - simp2_p.set_bool("pull_cheap_ite", true); - simp2_p.set_bool("push_ite_bv", false); - simp2_p.set_bool("local_ctx", true); - simp2_p.set_uint("local_ctx_limit", 10000000); - simp2_p.set_bool("flat", true); // required by som - simp2_p.set_bool("hoist_mul", false); // required by som - simp2_p.set_bool("elim_and", true); - simp2_p.set_bool("blast_distinct", true); + simp2_p.set_bool("flat", false); + m_preprocess = and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), - //time consuming if done in inner loop: mk_solve_eqs_tactic(m, simp2_p), + //time consuming if done in inner loop: mk_solve_eqs_tactic(m, simp1_p), mk_card2bv_tactic(m, m_params), // updates model converter - using_params(mk_simplify_tactic(m), simp2_p), + using_params(mk_simplify_tactic(m), simp1_p), mk_max_bv_sharing_tactic(m), - mk_bit_blaster_tactic(m, m_bb_rewriter.get()), - using_params(mk_simplify_tactic(m), simp2_p) + mk_bit_blaster_tactic(m, m_bb_rewriter.get()) + /*TBD remove and check what simplifier does with expansion */ , using_params(mk_simplify_tactic(m), simp2_p) ); while (m_bb_rewriter->get_num_scopes() < m_num_scopes) { m_bb_rewriter->push(); diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index 811461f62..f454fb9c6 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -107,6 +107,7 @@ bool smt_logics::logic_has_bv(symbol const & s) { s == "QF_BVFP" || logic_is_allcsp(s) || s == "QF_FD" || + s == "SMTFD" || s == "HORN"; } @@ -129,6 +130,7 @@ bool smt_logics::logic_has_array(symbol const & s) { logic_is_allcsp(s) || s == "QF_ABV" || s == "QF_AUFBV" || + s == "SMTFD" || s == "HORN"; } @@ -145,7 +147,7 @@ bool smt_logics::logic_has_fpa(symbol const & s) { } bool smt_logics::logic_has_uf(symbol const & s) { - return s == "QF_UF" || s == "UF" || s == "QF_DT"; + return s == "QF_UF" || s == "UF" || s == "QF_DT" || s == "SMTFD"; } bool smt_logics::logic_has_horn(symbol const& s) { diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 8a7b54fa6..1704e9802 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -34,6 +34,7 @@ Notes: #include "tactic/smtlogics/nra_tactic.h" #include "tactic/portfolio/default_tactic.h" #include "tactic/fd_solver/fd_solver.h" +#include "tactic/fd_solver/smtfd_solver.h" #include "tactic/ufbv/ufbv_tactic.h" #include "tactic/fpa/qffp_tactic.h" #include "muz/fp/horn_tactic.h" @@ -107,6 +108,8 @@ static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p parallel_params pp(p); if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled() && !pp.enable()) return mk_fd_solver(m, p); + if (logic == "SMTFD" && !m.proofs_enabled() && !pp.enable()) + return mk_smtfd_solver(m, p); return nullptr; } diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp index 4bee7dfb1..9af987f91 100644 --- a/src/test/pdd.cpp +++ b/src/test/pdd.cpp @@ -103,6 +103,20 @@ namespace dd { std::cout << (a + b)*(c + d) << "\n"; } + void test_iterator() { + std::cout << "test iterator\n"; + pdd_manager m(4); + pdd a = m.mk_var(0); + pdd b = m.mk_var(1); + pdd c = m.mk_var(2); + pdd d = m.mk_var(3); + pdd p = (a + b)*(c + 3*d) + 2; + std::cout << p << "\n"; + for (auto const& m : p) { + std::cout << m << "\n"; + } + } + } void tst_pdd() { @@ -110,4 +124,5 @@ void tst_pdd() { dd::test2(); dd::test3(); dd::test_reset(); + dd::test_iterator(); } diff --git a/src/test/pdd_solver.cpp b/src/test/pdd_solver.cpp index cf4e3ca7a..467d5cdd3 100644 --- a/src/test/pdd_solver.cpp +++ b/src/test/pdd_solver.cpp @@ -217,6 +217,13 @@ namespace dd { g.display(std::cout); g.simplify(); g.display(std::cout); + if (use_mod2) { + solver::config cfg; + cfg.m_enable_exlin = true; + g = cfg; + g.simplify(); + g.display(std::cout << "after exlin\n"); + } g.saturate(); g.display(std::cout); }