From a89be68050122a6ee51d967637aba964c52ca9b7 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 1 Aug 2022 21:43:41 +0700 Subject: [PATCH 01/19] Use `false` instead of `0`. --- src/math/lp/hnf_cutter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp index 70a9222e4..c1f93c9d8 100644 --- a/src/math/lp/hnf_cutter.cpp +++ b/src/math/lp/hnf_cutter.cpp @@ -20,7 +20,7 @@ namespace lp { lra(lia.lra), m_settings(lia.settings()), m_abs_max(zero_of_type()), - m_var_register(0) {} + m_var_register(false) {} bool hnf_cutter::is_full() const { return From 79ee543d25bab9bd58d76c5ac739d949dd01d789 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 11:59:18 +0200 Subject: [PATCH 02/19] Move tbv to util --- src/muz/ddnf/ddnf.cpp | 2 +- src/muz/rel/CMakeLists.txt | 1 - src/muz/rel/doc.cpp | 34 +++++++++++++++++++++++++++++----- src/muz/rel/doc.h | 6 ++++-- src/test/ddnf.cpp | 2 +- src/test/tbv.cpp | 2 +- src/util/CMakeLists.txt | 1 + src/{muz/rel => util}/tbv.cpp | 26 +------------------------- src/{muz/rel => util}/tbv.h | 5 +---- 9 files changed, 39 insertions(+), 40 deletions(-) rename src/{muz/rel => util}/tbv.cpp (91%) rename src/{muz/rel => util}/tbv.h (96%) diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp index c0c3d839c..cf759c76e 100644 --- a/src/muz/ddnf/ddnf.cpp +++ b/src/muz/ddnf/ddnf.cpp @@ -25,7 +25,7 @@ Revision History: #include "muz/base/dl_context.h" #include "ast/scoped_proof.h" #include "ast/bv_decl_plugin.h" -#include "muz/rel/tbv.h" +#include "util/tbv.h" #include namespace datalog { diff --git a/src/muz/rel/CMakeLists.txt b/src/muz/rel/CMakeLists.txt index f03a90406..1129b6dd9 100644 --- a/src/muz/rel/CMakeLists.txt +++ b/src/muz/rel/CMakeLists.txt @@ -23,7 +23,6 @@ z3_add_component(rel doc.cpp karr_relation.cpp rel_context.cpp - tbv.cpp udoc_relation.cpp COMPONENT_DEPENDENCIES muz diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp index 0b7800905..fbe6b1f61 100644 --- a/src/muz/rel/doc.cpp +++ b/src/muz/rel/doc.cpp @@ -695,12 +695,36 @@ void doc_manager::check_equiv(ast_manager& m, expr* fml1, expr* fml2) { SASSERT(res == l_false); } + +expr_ref doc_manager::to_formula(ast_manager & m, tbv const& src) { + expr_ref result(m); + expr_ref_vector conj(m); + for (unsigned i = 0; i < num_tbits(); ++i) { + switch (src[i]) { + case BIT_0: + conj.push_back(m.mk_not(m.mk_const(symbol(i), m.mk_bool_sort()))); + break; + case BIT_1: + conj.push_back(m.mk_const(symbol(i), m.mk_bool_sort())); + break; + default: + break; + } + } + result = mk_and(m, conj.size(), conj.data()); + return result; +} + +expr_ref doc_manager::mk_var(ast_manager & m, unsigned i) { + return expr_ref(m.mk_const(symbol(i), m.mk_bool_sort()), m); +} + expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) { expr_ref result(m); expr_ref_vector conj(m); - conj.push_back(tbvm().to_formula(m, src.pos())); + conj.push_back(to_formula(m, src.pos())); for (unsigned i = 0; i < src.neg().size(); ++i) { - conj.push_back(m.mk_not(tbvm().to_formula(m, src.neg()[i]))); + conj.push_back(m.mk_not(to_formula(m, src.neg()[i]))); } result = mk_and(m, conj.size(), conj.data()); return result; @@ -712,9 +736,9 @@ void doc_manager::project_expand(expr_ref& fml, bit_vector const& to_delete) { for (unsigned i = 0; i < num_tbits(); ++i) { if (to_delete.get(i)) { expr_safe_replace rep1(m), rep2(m); - rep1.insert(tbvm().mk_var(m, i), m.mk_true()); + rep1.insert(mk_var(m, i), m.mk_true()); rep1(fml, tmp1); - rep2.insert(tbvm().mk_var(m, i), m.mk_false()); + rep2.insert(mk_var(m, i), m.mk_false()); rep2(fml, tmp2); if (tmp1 == tmp2) { fml = tmp1; @@ -731,7 +755,7 @@ void doc_manager::project_rename(expr_ref& fml, bit_vector const& to_delete) { expr_safe_replace rep(m); for (unsigned i = 0, j = 0; i < num_tbits(); ++i) { if (!to_delete.get(i)) { - rep.insert(tbvm().mk_var(m, j), tbvm().mk_var(m, i)); + rep.insert(mk_var(m, j), mk_var(m, i)); ++j; } } diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h index 10120ce8b..bae9f64e6 100644 --- a/src/muz/rel/doc.h +++ b/src/muz/rel/doc.h @@ -22,10 +22,10 @@ Revision History: #pragma once -#include "muz/rel/tbv.h" +#include "util/tbv.h" #include "util/union_find.h" #include "util/buffer.h" - +#include "ast/ast.h" class doc; template class union_bvec; @@ -101,6 +101,8 @@ private: void project_rename(expr_ref& fml, bit_vector const& to_delete); void project_expand(expr_ref& fml, bit_vector const& to_delete); expr_ref to_formula(ast_manager& m, doc const& src); + expr_ref to_formula(ast_manager& m, tbv const& src); + expr_ref mk_var(ast_manager& m, unsigned i); void check_equiv(ast_manager& m, expr* fml1, expr* fml2); }; diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp index b1bb624a2..c62adb4f9 100644 --- a/src/test/ddnf.cpp +++ b/src/test/ddnf.cpp @@ -4,7 +4,7 @@ Copyright (c) 2015 Microsoft Corporation --*/ #include "muz/ddnf/ddnf.h" -#include "muz/rel/tbv.h" +#include "util/tbv.h" #include #include #include diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp index 6107fad85..fe33baba5 100644 --- a/src/test/tbv.cpp +++ b/src/test/tbv.cpp @@ -4,7 +4,7 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#include "muz/rel/tbv.h" +#include "util/tbv.h" #include static void tst1(unsigned num_bits) { diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 35727bce2..c2a7e8296 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -54,6 +54,7 @@ z3_add_component(util state_graph.cpp statistics.cpp symbol.cpp + tbv.cpp timeit.cpp timeout.cpp trace.cpp diff --git a/src/muz/rel/tbv.cpp b/src/util/tbv.cpp similarity index 91% rename from src/muz/rel/tbv.cpp rename to src/util/tbv.cpp index 289e43b4e..017ca0eb7 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/util/tbv.cpp @@ -18,9 +18,8 @@ Revision History: --*/ -#include "muz/rel/tbv.h" +#include "util/tbv.h" #include "util/hashtable.h" -#include "ast/ast_util.h" static bool s_debug_alloc = false; @@ -301,26 +300,3 @@ std::ostream& tbv_manager::display(std::ostream& out, tbv const& b) const { if (num_tbits() == 0) return out << "[]"; return display(out, b, num_tbits()-1, 0); } - -expr_ref tbv_manager::to_formula(ast_manager& m, tbv const& src) { - expr_ref result(m); - expr_ref_vector conj(m); - for (unsigned i = 0; i < num_tbits(); ++i) { - switch (src[i]) { - case BIT_0: - conj.push_back(m.mk_not(m.mk_const(symbol(i), m.mk_bool_sort()))); - break; - case BIT_1: - conj.push_back(m.mk_const(symbol(i), m.mk_bool_sort())); - break; - default: - break; - } - } - result = mk_and(m, conj.size(), conj.data()); - return result; -} - -expr_ref tbv_manager::mk_var(ast_manager& m, unsigned i) { - return expr_ref(m.mk_const(symbol(i), m.mk_bool_sort()), m); -} diff --git a/src/muz/rel/tbv.h b/src/util/tbv.h similarity index 96% rename from src/muz/rel/tbv.h rename to src/util/tbv.h index a8aaea234..2a337be1f 100644 --- a/src/muz/rel/tbv.h +++ b/src/util/tbv.h @@ -21,8 +21,8 @@ Revision History: #pragma once #include "util/fixed_bit_vector.h" +#include "util/bit_vector.h" #include "util/rational.h" -#include "ast/ast.h" class tbv; @@ -84,10 +84,7 @@ public: void set(tbv& dst, tbv const& other, unsigned hi, unsigned lo); void set(tbv& dst, unsigned index, tbit value); - static void debug_alloc(); - expr_ref to_formula(ast_manager& m, tbv const& src); - expr_ref mk_var(ast_manager& m, unsigned i); }; class tbv: private fixed_bit_vector { From d2fe1743209c327f71f45d756ae3bf68f41a96bf Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 12:04:57 +0200 Subject: [PATCH 03/19] Add SASSERT_EQ and VERIFY_EQ --- src/util/debug.h | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/util/debug.h b/src/util/debug.h index 9ad55a7c2..795976eac 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -63,6 +63,13 @@ bool is_debug_enabled(const char * tag); #define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); }) #define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); }) +#define SASSERT_EQ(LHS, RHS) \ + DEBUG_CODE(if (assertions_enabled() && !((LHS) == (RHS))) { \ + notify_assertion_violation(__FILE__, __LINE__, #LHS " == " #RHS); \ + std::cerr << "LHS value: " << (LHS) << "\nRHS value: " << (RHS) << "\n"; \ + INVOKE_DEBUGGER(); \ + }) + #ifdef Z3DEBUG # define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); INVOKE_DEBUGGER();) #else @@ -78,7 +85,14 @@ bool is_debug_enabled(const char * tag); #define VERIFY(_x_) if (!(_x_)) { \ notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #_x_ "\n"); \ exit(ERR_UNREACHABLE); \ - } + } + +#define VERIFY_EQ(LHS, RHS) \ + if (!((LHS) == (RHS))) { \ + notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #LHS " == " #RHS "\n"); \ + std::cerr << "LHS value: " << (LHS) << "\nRHS value: " << (RHS) << "\n"; \ + exit(ERR_UNREACHABLE); \ + } #define ENSURE(_x_) VERIFY(_x_) From 6a929f91c8218d5a36d6b55992d97acef9e4c821 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 12:07:56 +0200 Subject: [PATCH 04/19] scoped_ptr_vector usability --- src/util/scoped_ptr_vector.h | 38 ++++++++++++++++++++++++++++++++++-- 1 file changed, 36 insertions(+), 2 deletions(-) diff --git a/src/util/scoped_ptr_vector.h b/src/util/scoped_ptr_vector.h index fee80d584..3c33cc708 100644 --- a/src/util/scoped_ptr_vector.h +++ b/src/util/scoped_ptr_vector.h @@ -26,9 +26,25 @@ template class scoped_ptr_vector { ptr_vector m_vector; public: + scoped_ptr_vector() = default; ~scoped_ptr_vector() { reset(); } + scoped_ptr_vector(scoped_ptr_vector& other) = delete; + scoped_ptr_vector& operator=(scoped_ptr_vector& other) = delete; + + scoped_ptr_vector(scoped_ptr_vector&& other) noexcept { + m_vector.swap(other.m_vector); + } + scoped_ptr_vector& operator=(scoped_ptr_vector&& other) { + if (this == &other) + return *this; + reset(); + m_vector.swap(other.m_vector); + return *this; + } + void reset() { std::for_each(m_vector.begin(), m_vector.end(), delete_proc()); m_vector.reset(); } void push_back(T * ptr) { m_vector.push_back(ptr); } + void push_back(scoped_ptr&& ptr) { push_back(ptr.detach()); } void pop_back() { SASSERT(!empty()); set(size()-1, nullptr); m_vector.pop_back(); } T * back() const { return m_vector.back(); } T * operator[](unsigned idx) const { return m_vector[idx]; } @@ -39,6 +55,7 @@ public: dealloc(m_vector[idx]); m_vector[idx] = ptr; } + void swap(unsigned i, unsigned j) { std::swap(m_vector[i], m_vector[j]); } unsigned size() const { return m_vector.size(); } bool empty() const { return m_vector.empty(); } void resize(unsigned sz) { @@ -64,7 +81,24 @@ public: ptr = m_vector.back(); m_vector[m_vector.size()-1] = tmp; } - typename ptr_vector::const_iterator begin() const { return m_vector.begin(); } - typename ptr_vector::const_iterator end() const { return m_vector.end(); } + + T* detach_back() { + SASSERT(!empty()); + T* tmp = m_vector.back(); + m_vector.back() = nullptr; + return tmp; + } + + ptr_vector detach() { + ptr_vector tmp(std::move(m_vector)); + SASSERT(m_vector.empty()); + return tmp; + } + + T* const* data() const { return m_vector.data(); } + + using const_iterator = typename ptr_vector::const_iterator; + const_iterator begin() const { return m_vector.begin(); } + const_iterator end() const { return m_vector.end(); } }; From e31926d1321ab65abb3b024251f21345651ea20b Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 12:08:38 +0200 Subject: [PATCH 05/19] var_queue display --- src/util/var_queue.h | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/src/util/var_queue.h b/src/util/var_queue.h index e5a21d9a4..62df77784 100644 --- a/src/util/var_queue.h +++ b/src/util/var_queue.h @@ -52,7 +52,7 @@ public: void mk_var_eh(var v) { m_queue.reserve(v+1); - m_queue.insert(v); + unassign_var_eh(v); } void del_var_eh(var v) { @@ -76,5 +76,21 @@ public: var min_var() { SASSERT(!empty()); return m_queue.min_value(); } bool more_active(var v1, var v2) const { return m_queue.less_than(v1, v2); } + + std::ostream& display(std::ostream& out) const { + bool first = true; + for (auto v : m_queue) { + if (first) { + first = false; + } else { + out << " "; + } + out << v; + } + return out; + } }; +inline std::ostream& operator<<(std::ostream& out, var_queue const& queue) { + return queue.display(out); +} From 6eae27ffadf01d50b84482e6b49900819802c778 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 12:14:06 +0200 Subject: [PATCH 06/19] numeral helper functions --- src/util/mpf.h | 2 ++ src/util/mpz.cpp | 7 +++++++ src/util/mpz.h | 3 +++ src/util/rational.cpp | 2 +- src/util/rational.h | 13 ++++++++++++- src/util/scoped_numeral.h | 4 ++-- 6 files changed, 27 insertions(+), 4 deletions(-) diff --git a/src/util/mpf.h b/src/util/mpf.h index fb5f2a022..466d23ea5 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -88,6 +88,8 @@ public: void neg(mpf & o); void neg(mpf const & x, mpf & o); + + void swap(mpf& a, mpf& b) { a.swap(b); } bool is_zero(mpf const & x); bool is_neg(mpf const & x); diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 736b401b8..d3e9941d3 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -76,6 +76,13 @@ static uint64_t _trailing_zeros64(uint64_t x) { } #endif +unsigned trailing_zeros(uint32_t x) { + return static_cast(_trailing_zeros32(x)); +} + +unsigned trailing_zeros(uint64_t x) { + return static_cast(_trailing_zeros64(x)); +} #define _bit_min(x, y) (y + ((x - y) & ((int)(x - y) >> 31))) #define _bit_max(x, y) (x - ((x - y) & ((int)(x - y) >> 31))) diff --git a/src/util/mpz.h b/src/util/mpz.h index f3c3b19b9..1a7b6f55e 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -29,6 +29,9 @@ Revision History: unsigned u_gcd(unsigned u, unsigned v); uint64_t u64_gcd(uint64_t u, uint64_t v); +unsigned trailing_zeros(uint64_t); +unsigned trailing_zeros(uint32_t); + #ifdef _MP_GMP typedef unsigned digit_t; diff --git a/src/util/rational.cpp b/src/util/rational.cpp index bb443935a..af3c89ced 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -130,7 +130,7 @@ bool rational::limit_denominator(rational &num, rational const& limit) { return false; } -bool rational::mult_inverse(unsigned num_bits, rational & result) { +bool rational::mult_inverse(unsigned num_bits, rational & result) const { rational const& n = *this; if (n.is_one()) { result = n; diff --git a/src/util/rational.h b/src/util/rational.h index f28a502ef..cffd0083c 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -157,6 +157,12 @@ public: friend inline rational numerator(rational const & r) { rational result; m().get_numerator(r.m_val, result.m_val); return result; } friend inline rational denominator(rational const & r) { rational result; m().get_denominator(r.m_val, result.m_val); return result; } + + friend inline rational inv(rational const & r) { + rational result; + m().inv(r.m_val, result.m_val); + return result; + } rational & operator+=(rational const & r) { m().add(m_val, r.m_val, m_val); @@ -346,8 +352,13 @@ public: bool is_power_of_two(unsigned & shift) const { return m().is_power_of_two(m_val, shift); } + + bool is_power_of_two() const { + unsigned shift = 0; + return m().is_power_of_two(m_val, shift); + } - bool mult_inverse(unsigned num_bits, rational & result); + bool mult_inverse(unsigned num_bits, rational & result) const; static rational const & zero() { return m_zero; diff --git a/src/util/scoped_numeral.h b/src/util/scoped_numeral.h index 3b35a1bd8..65b75053d 100644 --- a/src/util/scoped_numeral.h +++ b/src/util/scoped_numeral.h @@ -61,11 +61,11 @@ public: } void swap(_scoped_numeral & n) { - m_num.swap(n.m_num); + m().swap(m_num, n.m_num); } void swap(numeral & n) { - m_num.swap(n); + m().swap(m_num, n); } _scoped_numeral & operator+=(numeral const & a) { From 9275d1e57aac84face30b8e9af0f58bfdb8b4931 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 12:17:21 +0200 Subject: [PATCH 07/19] sparse_matrix iterators --- src/math/simplex/sparse_matrix.h | 23 +++++++++++++++++++---- src/math/simplex/sparse_matrix_def.h | 2 +- src/smt/theory_dense_diff_logic_def.h | 2 +- src/smt/theory_diff_logic_def.h | 2 +- 4 files changed, 22 insertions(+), 7 deletions(-) diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index a33ea55bd..ecba27af5 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -36,6 +36,8 @@ namespace simplex { numeral m_coeff; var_t m_var; row_entry(numeral && c, var_t v) : m_coeff(std::move(c)), m_var(v) {} + inline numeral const& coeff() const { return m_coeff; } + inline var_t var() const { return m_var; } }; private: @@ -202,17 +204,17 @@ namespace simplex { row_iterator row_begin(row const& r) { return row_iterator(m_rows[r.id()], true); } row_iterator row_end(row const& r) { return row_iterator(m_rows[r.id()], false); } - class row_vars { + class row_entries_t { friend class sparse_matrix; sparse_matrix& s; row r; - row_vars(sparse_matrix& s, row r): s(s), r(r) {} + row_entries_t(sparse_matrix& s, row r): s(s), r(r) {} public: row_iterator begin() { return s.row_begin(r); } row_iterator end() { return s.row_end(r); } }; - row_vars get_row(row r) { return row_vars(*this, r); } + row_entries_t get_row(row r) { return row_entries_t(*this, r); } unsigned column_size(var_t v) const { return m_columns[v].size(); } @@ -247,7 +249,8 @@ namespace simplex { row get_row() const { return row(m_col.m_entries[m_curr].m_row_id); } - row_entry& get_row_entry() { + + row_entry& get_row_entry() const { col_entry const& c = m_col.m_entries[m_curr]; int row_id = c.m_row_id; return m_rows[row_id].m_entries[c.m_row_idx]; @@ -263,6 +266,18 @@ namespace simplex { col_iterator col_begin(int v) { return col_iterator(m_columns[v], m_rows, true); } col_iterator col_end(int v) { return col_iterator(m_columns[v], m_rows, false); } + class col_entries_t { + friend class sparse_matrix; + sparse_matrix& m; + int v; + col_entries_t(sparse_matrix& m, int v): m(m), v(v) {} + public: + col_iterator begin() { return m.col_begin(v); } + col_iterator end() { return m.col_end(v); } + }; + + col_entries_t get_col(int v) { return col_entries_t(*this, v); } + class var_rows { friend class sparse_matrix; sparse_matrix& s; diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h index dc3700f2e..255e62f11 100644 --- a/src/math/simplex/sparse_matrix_def.h +++ b/src/math/simplex/sparse_matrix_def.h @@ -98,7 +98,7 @@ namespace simplex { if (!t1.is_dead()) { if (i != j) { _row_entry & t2 = m_entries[j]; - t2.m_coeff.swap(t1.m_coeff); + m.swap(t2.m_coeff, t1.m_coeff); t2.m_var = t1.m_var; t2.m_col_idx = t1.m_col_idx; SASSERT(!t2.is_dead()); diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 3a19b1c19..b5abc7a2a 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -1011,7 +1011,7 @@ namespace smt { expr_ref tmp(m); core.reset(); for (; it != end; ++it) { - unsigned v = it->m_var; + unsigned v = it->var(); if (num_nodes <= v && v < num_nodes + num_edges) { unsigned edge_id = v - num_nodes; literal lit = m_edges[edge_id].m_justification; diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index e9747c4ae..80fbe4022 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -1283,7 +1283,7 @@ theory_diff_logic::maximize(theory_var v, expr_ref& blocker, bool& has_shar expr_ref tmp(m); core.reset(); for (; it != end; ++it) { - unsigned v = it->m_var; + unsigned v = it->var(); if (is_simplex_edge(v)) { unsigned edge_id = simplex2edge(v); literal lit = m_graph.get_explanation(edge_id); From 42233ab5c875409d9952b890ab70e0289e9fbba3 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 12:30:34 +0200 Subject: [PATCH 08/19] Additional BDD operations; BDD vectors and finite domain abstraction --- src/math/dd/CMakeLists.txt | 1 + src/math/dd/dd_bdd.cpp | 363 ++++++++++++++++++++++++++- src/math/dd/dd_bdd.h | 133 +++++++++- src/math/dd/dd_fdd.cpp | 366 +++++++++++++++++++++++++++ src/math/dd/dd_fdd.h | 108 ++++++++ src/test/bdd.cpp | 493 +++++++++++++++++++++++++++++++++++-- 6 files changed, 1432 insertions(+), 32 deletions(-) create mode 100644 src/math/dd/dd_fdd.cpp create mode 100644 src/math/dd/dd_fdd.h diff --git a/src/math/dd/CMakeLists.txt b/src/math/dd/CMakeLists.txt index ac9d28b0d..3f25a8406 100644 --- a/src/math/dd/CMakeLists.txt +++ b/src/math/dd/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(dd SOURCES dd_bdd.cpp + dd_fdd.cpp dd_pdd.cpp COMPONENT_DEPENDENCIES util diff --git a/src/math/dd/dd_bdd.cpp b/src/math/dd/dd_bdd.cpp index 86f2b9408..ee0f1600c 100644 --- a/src/math/dd/dd_bdd.cpp +++ b/src/math/dd/dd_bdd.cpp @@ -142,6 +142,8 @@ namespace dd { if (a == b) return false_bdd; if (is_false(a)) return b; if (is_false(b)) return a; + if (is_true(a)) return mk_not_rec(b); + if (is_true(b)) return mk_not_rec(a); break; default: UNREACHABLE(); @@ -571,7 +573,63 @@ namespace dd { e1->m_result = r; return r; } + + /** + * co-factor a using b. + * b must be a variable bdd (it can be generalized to a cube) + */ + + bdd bdd_manager::mk_cofactor(bdd const& a, bdd const& b) { + bool first = true; + scoped_push _sp(*this); + SASSERT(!b.is_const() && b.lo().is_const() && b.hi().is_const()); + while (true) { + try { + return bdd(mk_cofactor_rec(a.root, b.root), this); + } + catch (const mem_out &) { + if (!first) throw; + try_reorder(); + first = false; + } + } + } + + bdd_manager::BDD bdd_manager::mk_cofactor_rec(BDD a, BDD b) { + if (is_const(a)) return a; + if (is_const(b)) return a; + unsigned la = level(a), lb = level(b); + // cases where b is a single literal + if (la == lb && is_const(lo(b)) && is_const(hi(b))) + return is_true(hi(b)) ? hi(a) : lo(a); + if (la < lb && is_const(lo(b)) && is_const(hi(b))) + return a; + // cases where b is a proper cube (with more than one literal + if (la == lb) { + if (is_false(lo(b))) + a = hi(a), b = hi(b); + else + a = lo(a), b = lo(b); + return mk_cofactor_rec(a, b); + } + if (la < lb) + return mk_cofactor_rec(a, is_false(lo(b)) ? hi(b) : lo(b)); + + op_entry* e1 = pop_entry(a, b, bdd_cofactor_op); + op_entry const* e2 = m_op_cache.insert_if_not_there(e1); + if (check_result(e1, e2, a, b, bdd_cofactor_op)) + return e2->m_result; + + SASSERT(la > lb); + push(mk_cofactor_rec(lo(a), b)); + push(mk_cofactor_rec(hi(a), b)); + BDD r = make_node(la, read(2), read(1)); + pop(2); + e1->m_result = r; + return r; + } + bdd bdd_manager::mk_ite(bdd const& c, bdd const& t, bdd const& e) { bool first = true; scoped_push _sp(*this); @@ -587,14 +645,15 @@ namespace dd { } } + bdd_manager::BDD bdd_manager::mk_ite_rec(BDD a, BDD b, BDD c) { if (is_true(a)) return b; if (is_false(a)) return c; if (b == c) return b; - if (is_true(b)) return apply(a, c, bdd_or_op); - if (is_false(c)) return apply(a, b, bdd_and_op); - if (is_false(b)) return apply(mk_not_rec(a), c, bdd_and_op); - if (is_true(c)) return apply(mk_not_rec(a), b, bdd_or_op); + if (is_true(b)) return apply_rec(a, c, bdd_or_op); + if (is_false(c)) return apply_rec(a, b, bdd_and_op); + if (is_false(b)) return apply_rec(mk_not_rec(a), c, bdd_and_op); + if (is_true(c)) return apply_rec(mk_not_rec(a), b, bdd_or_op); SASSERT(!is_const(a) && !is_const(b) && !is_const(c)); op_entry * e1 = pop_entry(a, b, c); op_entry const* e2 = m_op_cache.insert_if_not_there(e1); @@ -644,6 +703,7 @@ namespace dd { bdd_manager::BDD bdd_manager::mk_quant(unsigned n, unsigned const* vars, BDD b, bdd_op op) { BDD result = b; + // TODO: should this method catch mem_out like the other non-rec mk_ methods? for (unsigned i = 0; i < n; ++i) { result = mk_quant_rec(m_var2level[vars[i]], result, op); } @@ -895,4 +955,299 @@ namespace dd { bdd& bdd::operator=(bdd const& other) { unsigned r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; } std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); } + + bdd bdd_manager::mk_eq(bddv const& a, bddv const& b) { + SASSERT(a.size() == b.size()); + bdd eq = mk_true(); + for (unsigned i = 0; i < a.size(); ++i) + eq &= !(a[i] ^ b[i]); + return eq; + } + + bdd bdd_manager::mk_eq(bddv const& a, rational const& n) { + SASSERT(n.is_int() && n >= 0 && n < rational(2).expt(a.size())); + bdd b = mk_true(); + for (unsigned i = 0; i < a.size(); ++i) + b &= n.get_bit(i) ? a[i] : !a[i]; + return b; + } + + bdd bdd_manager::mk_eq(unsigned_vector const& vars, rational const& n) { + SASSERT(n.is_int() && n >= 0 && n < rational(2).expt(vars.size())); + bdd b = mk_true(); + for (unsigned i = 0; i < vars.size(); ++i) + b &= n.get_bit(i) ? mk_var(vars[i]) : mk_nvar(vars[i]); + return b; + } + + bdd bdd_manager::mk_ule(bddv const& a, bddv const& b) { + SASSERT(a.size() == b.size()); + bdd lt = mk_false(); + bdd eq = mk_true(); + for (unsigned i = a.size(); i-- > 0 && !eq.is_false(); ) { + lt |= eq && (!a[i] && b[i]); + eq &= !(a[i] ^ b[i]); + } + return lt || eq; + } + bdd bdd_manager::mk_uge(bddv const& a, bddv const& b) { return mk_ule(b, a); } + bdd bdd_manager::mk_ult(bddv const& a, bddv const& b) { return mk_ule(a, b) && !mk_eq(a, b); } + bdd bdd_manager::mk_ugt(bddv const& a, bddv const& b) { return mk_ult(b, a); } + + bdd bdd_manager::mk_sle(bddv const& a, bddv const& b) { + SASSERT(a.size() == b.size()); + // Note: sle can be reduced to ule by flipping the sign bits of both arguments + bdd lt = mk_false(); + bdd eq = mk_true(); + unsigned const sz = a.size(); + if (sz > 0) { + lt = a[sz - 1] && !b[sz - 1]; + eq = !(a[sz - 1] ^ b[sz - 1]); + for (unsigned i = sz - 1; i-- > 0; ) { + lt |= eq && (!a[i] && b[i]); + eq &= !(a[i] ^ b[i]); + } + } + return lt || eq; + } + bdd bdd_manager::mk_sge(bddv const& a, bddv const& b) { return mk_sle(b, a); } + bdd bdd_manager::mk_slt(bddv const& a, bddv const& b) { return mk_sle(a, b) && !mk_eq(a, b); } + bdd bdd_manager::mk_sgt(bddv const& a, bddv const& b) { return mk_slt(b, a); } + + bddv bdd_manager::mk_add(bddv const& a, bddv const& b) { + SASSERT(a.size() == b.size()); + bdd carry = mk_false(); + bddv result(this); +#if 0 + for (unsigned i = 0; i < a.size(); ++i) { + result.push_back(carry ^ a[i] ^ b[i]); + carry = (carry && a[i]) || (carry && b[i]) || (a[i] && b[i]); + } +#else + if (a.size() > 0) + result.push_back(a[0] ^ b[0]); + for (unsigned i = 1; i < a.size(); ++i) { + carry = (carry && a[i-1]) || (carry && b[i-1]) || (a[i-1] && b[i-1]); + result.push_back(carry ^ a[i] ^ b[i]); + } +#endif + return result; + } + + bddv bdd_manager::mk_add(bddv const& a, std::function& b) { + bdd carry = mk_false(); + bddv result(this); + if (a.size() > 0) + result.push_back(a[0] ^ b(0)); + for (unsigned i = 1; i < a.size(); ++i) { + auto bi1 = b(i-1); + carry = (carry && a[i-1]) || (carry && bi1) || (a[i-1] && bi1); + result.push_back(carry ^ a[i] ^ b(i)); + } + return result; + } + + + bddv bdd_manager::mk_sub(bddv const& a, bddv const& b) { + SASSERT(a.size() == b.size()); + bdd carry = mk_false(); + bddv result(this); + if (a.size() > 0) + result.push_back(a[0] ^ b[0]); + for (unsigned i = 1; i < a.size(); ++i) { + // carry = (a[i-1] && b[i-1] && carry) || (!a[i-1] && (b[i-1] || carry)); + carry = mk_ite(a[i-1], b[i-1] && carry, b[i-1] || carry); + result.push_back(carry ^ a[i] ^ b[i]); + } + return result; + } + + bddv bdd_manager::mk_usub(bddv const& a) { + bddv result(this); + bdd carry = mk_false(); + result.push_back(a[0]); + for (unsigned i = 1; i < a.size(); ++i) { + carry = a[i-1] || carry; + result.push_back(carry ^ a[i]); + } + return result; + } + + bool_vector bdd_manager::mk_usub(bool_vector const& b) { + bool_vector result; + if (b.empty()) + return result; + bool carry = false; + result.push_back(b[0]); + for (unsigned i = 1; i < b.size(); ++i) { + carry = carry || b[i-1]; + result.push_back(carry ^ b[i]); + } + return result; + } + + + bddv bdd_manager::mk_mul(bddv const& a, bddv const& b) { + SASSERT(a.size() == b.size()); + bddv result = mk_zero(a.size()); + for (unsigned i = 0; i < b.size(); ++i) { + std::function get_a = [&](unsigned k) { + if (k < i) + return mk_false(); + else + return a[k - i] && b[i]; + }; + result = mk_add(result, get_a); + } + return result; + } + + bddv bdd_manager::mk_mul(bddv const& a, rational const& val) { + SASSERT(val.is_int() && val >= 0 && val < rational::power_of_two(a.size())); + bool_vector b; + for (unsigned i = 0; i < a.size(); ++i) + b.push_back(val.get_bit(i)); + return mk_mul(a, b); + } + + bddv bdd_manager::mk_mul(bddv const& a, bool_vector const& b) { + SASSERT(a.size() == b.size()); + bddv result = mk_zero(a.size()); + + // use identity (bvmul a b) == (bvneg (bvmul (bvneg a) b)) + unsigned cnt = 0; + for (auto v : b) if (v) cnt++; + if (cnt*2 > b.size()+1) + return mk_usub(mk_mul(a, mk_usub(b))); + + for (unsigned i = 0; i < a.size(); ++i) { + std::function get_a = [&](unsigned k) { + if (k < i) + return mk_false(); + else + return a[k - i]; + }; + if (b[i]) + result = mk_add(result, get_a); + } + return result; + } + + bddv bdd_manager::mk_concat(bddv const& a, bddv const& b) { + bddv result = a; + result.m_bits.append(b.m_bits); + return result; + } + + + /** + * Quotient remainder + * + * rem, div have size 2*|a| = worksize. + * Initialization: + * rem := a ++ false + * div := false ++ b + */ + void bdd_manager::mk_quot_rem(bddv const& a, bddv const& b, bddv& quot, bddv& rem) { + SASSERT(a.size() == b.size()); + quot = mk_zero(a.size()); + unsigned worksize = a.size() + b.size(); + rem = a.append(mk_zero(b.size())); + bddv div = mk_zero(a.size()).append(b); + // + // Keep shifting divisor to the right and subtract whenever it is + // smaller than the remaining value + // + for (unsigned i = 0; i <= b.size(); ++i) { + bdd divLteRem = div <= rem; + bddv remSubDiv = rem - div; + + for (unsigned j = 0; j < worksize; ++j) + rem[j] = mk_ite(divLteRem, remSubDiv[j], rem[j]); + + if (i > 0) + quot[b.size() - i] = divLteRem; + + div.shr(); + } + rem.m_bits.shrink(b.size()); + } + + bddv bdd_manager::mk_num(rational const& n, unsigned num_bits) { + SASSERT(n.is_int() && n >= 0 && n < rational::power_of_two(num_bits)); + bddv result(this); + for (unsigned i = 0; i < num_bits; ++i) + result.push_back(n.get_bit(i) ? mk_true() : mk_false()); + return result; + } + + bddv bdd_manager::mk_ones(unsigned num_bits) { + bddv result(this); + for (unsigned i = 0; i < num_bits; ++i) + result.push_back(mk_true()); + return result; + } + + bddv bdd_manager::mk_zero(unsigned num_bits) { + bddv result(this); + for (unsigned i = 0; i < num_bits; ++i) + result.push_back(mk_false()); + return result; + } + + bddv bdd_manager::mk_var(unsigned num_bits, unsigned const* vars) { + bddv result(this); + for (unsigned i = 0; i < num_bits; ++i) + result.push_back(mk_var(vars[i])); + return result; + } + + bddv bdd_manager::mk_var(unsigned_vector const& vars) { + return mk_var(vars.size(), vars.data()); + } + + bool bdd_manager::is_constv(bddv const& a) { + for (bdd const& bit : a.bits()) + if (!is_const(bit.root)) + return false; + return true; + } + + rational bdd_manager::to_val(bddv const& a) { + rational result = rational::zero(); + for (unsigned i = 0; i < a.size(); ++i) { + bdd const &bit = a[i]; + SASSERT(is_const(bit.root)); + if (bit.is_true()) + result += rational::power_of_two(i); + } + return result; + } + + void bddv::shl() { + for (unsigned j = size(); j-- > 1;) + m_bits[j] = m_bits[j - 1]; + m_bits[0] = m->mk_false(); + } + + void bddv::shr() { + for (unsigned j = 1; j < size(); ++j) + m_bits[j - 1] = m_bits[j]; + m_bits[size() - 1] = m->mk_false(); + } + + bdd bddv::all0() const { + bdd r = m->mk_true(); + for (unsigned i = 0; i < size() && !r.is_false(); ++i) + r &= !m_bits[i]; + return r; + } + + bdd bddv::all1() const { + bdd r = m->mk_true(); + for (unsigned i = 0; i < size() && !r.is_false(); ++i) + r &= m_bits[i]; + return r; + } + } diff --git a/src/math/dd/dd_bdd.h b/src/math/dd/dd_bdd.h index 1892c5317..109f3dc19 100644 --- a/src/math/dd/dd_bdd.h +++ b/src/math/dd/dd_bdd.h @@ -21,13 +21,18 @@ Revision History: #include "util/vector.h" #include "util/map.h" #include "util/small_object_allocator.h" +#include "util/rational.h" namespace dd { class bdd; + class bddv; + class test_bdd; class bdd_manager { friend bdd; + friend bddv; + friend test_bdd; typedef unsigned BDD; @@ -40,7 +45,8 @@ namespace dd { bdd_not_op = 5, bdd_and_proj_op = 6, bdd_or_proj_op = 7, - bdd_no_op = 8, + bdd_cofactor_op = 8, + bdd_no_op = 9, }; struct bdd_node { @@ -141,6 +147,7 @@ namespace dd { BDD mk_not_rec(BDD b); BDD mk_ite_rec(BDD a, BDD b, BDD c); BDD mk_quant_rec(unsigned lvl, BDD b, bdd_op op); + BDD mk_cofactor_rec(BDD a, BDD b); void push(BDD b); void pop(unsigned num_scopes); @@ -188,6 +195,7 @@ namespace dd { bdd mk_and(bdd const& a, bdd const& b); bdd mk_or(bdd const& a, bdd const& b); bdd mk_xor(bdd const& a, bdd const& b); + bdd mk_cofactor(bdd const& a, bdd const& b); void reserve_var(unsigned v); bool well_formed(); @@ -199,10 +207,13 @@ namespace dd { ~scoped_push() { m.m_bdd_stack.shrink(m_size); } }; + bool_vector mk_usub(bool_vector const& b); + + public: struct mem_out {}; - bdd_manager(unsigned nodes); + bdd_manager(unsigned num_vars); ~bdd_manager(); void set_max_num_nodes(unsigned n) { m_max_num_bdd_nodes = n; } @@ -219,6 +230,39 @@ namespace dd { bdd mk_forall(unsigned v, bdd const& b); bdd mk_ite(bdd const& c, bdd const& t, bdd const& e); + /* BDD vector operations + * - Fixed-width arithmetic, i.e., modulo 2^size + * - The lowest index is the LSB + */ + bdd mk_ule(bddv const& a, bddv const& b); + bdd mk_uge(bddv const& a, bddv const& b); // { return mk_ule(b, a); } + bdd mk_ult(bddv const& a, bddv const& b); // { return mk_ule(a, b) && !mk_eq(a, b); } + bdd mk_ugt(bddv const& a, bddv const& b); // { return mk_ult(b, a); } + bdd mk_sle(bddv const& a, bddv const& b); + bdd mk_sge(bddv const& a, bddv const& b); // { return mk_sle(b, a); } + bdd mk_slt(bddv const& a, bddv const& b); // { return mk_sle(a, b) && !mk_eq(a, b); } + bdd mk_sgt(bddv const& a, bddv const& b); // { return mk_slt(b, a); } + bdd mk_eq(bddv const& a, bddv const& b); + bdd mk_eq(bddv const& a, rational const& v); + bdd mk_eq(unsigned_vector const& vars, rational const& v); + bddv mk_num(rational const& n, unsigned num_bits); + bddv mk_ones(unsigned num_bits); + bddv mk_zero(unsigned num_bits); + bddv mk_var(unsigned num_bits, unsigned const* vars); + bddv mk_var(unsigned_vector const& vars); + bddv mk_add(bddv const& a, bddv const& b); + bddv mk_add(bddv const& a, std::function& get_bit); + bddv mk_sub(bddv const& a, bddv const& b); + bddv mk_usub(bddv const& a); + bddv mk_mul(bddv const& a, bddv const& b); + bddv mk_mul(bddv const& a, bool_vector const& b); + bddv mk_mul(bddv const& a, rational const& val); + bddv mk_concat(bddv const& a, bddv const& b); + void mk_quot_rem(bddv const& a, bddv const& b, bddv& quot, bddv& rem); + bool is_constv(bddv const& a); + rational to_val(bddv const& a); + + std::ostream& display(std::ostream& out); std::ostream& display(std::ostream& out, bdd const& b); @@ -242,14 +286,16 @@ namespace dd { unsigned var() const { return m->var(root); } bool is_true() const { return root == bdd_manager::true_bdd; } - bool is_false() const { return root == bdd_manager::false_bdd; } + bool is_false() const { return root == bdd_manager::false_bdd; } + bool is_const() const { return is_false() || is_true(); } - bdd operator!() { return m->mk_not(*this); } - bdd operator&&(bdd const& other) { return m->mk_and(*this, other); } - bdd operator||(bdd const& other) { return m->mk_or(*this, other); } - bdd operator^(bdd const& other) { return m->mk_xor(*this, other); } + bdd operator!() const { return m->mk_not(*this); } + bdd operator&&(bdd const& other) const { return m->mk_and(*this, other); } + bdd operator||(bdd const& other) const { return m->mk_or(*this, other); } + bdd operator^(bdd const& other) const { return m->mk_xor(*this, other); } bdd operator|=(bdd const& other) { return *this = *this || other; } bdd operator&=(bdd const& other) { return *this = *this && other; } + bdd cofactor(bdd const& cube) { return m->mk_cofactor(*this, cube); } std::ostream& display(std::ostream& out) const { return m->display(out, *this); } bool operator==(bdd const& other) const { return root == other.root; } bool operator!=(bdd const& other) const { return root != other.root; } @@ -260,6 +306,79 @@ namespace dd { std::ostream& operator<<(std::ostream& out, bdd const& b); + class bddv { + friend bdd_manager; + + vector m_bits; + bdd_manager* m; + + bddv(vector const& bits, bdd_manager* m): m_bits(bits), m(m) { SASSERT(m); } + bddv(vector&& bits, bdd_manager* m): m_bits(std::move(bits)), m(m) { SASSERT(m); } + + bddv(bdd_manager* m): m_bits(), m(m) { SASSERT(m); } + bdd const& operator[](unsigned i) const { return m_bits[i]; } + bdd& operator[](unsigned i) { return m_bits[i]; } + void push_back(bdd const& a) { m_bits.push_back(a); } + void push_back(bdd&& a) { m_bits.push_back(std::move(a)); } + void shl(); + void shr(); + + public: + unsigned size() const { return m_bits.size(); } + vector const& bits() const { return m_bits; } + + /* unsigned comparison operators */ + bdd operator<=(bddv const& other) const { return m->mk_ule(*this, other); } ///< unsigned comparison + bdd operator>=(bddv const& other) const { return m->mk_uge(*this, other); } ///< unsigned comparison + bdd operator< (bddv const& other) const { return m->mk_ult(*this, other); } ///< unsigned comparison + bdd operator> (bddv const& other) const { return m->mk_ugt(*this, other); } ///< unsigned comparison + bdd operator<=(rational const& other) const { return m->mk_ule(*this, m->mk_num(other, size())); } ///< unsigned comparison + bdd operator>=(rational const& other) const { return m->mk_uge(*this, m->mk_num(other, size())); } ///< unsigned comparison + bdd operator< (rational const& other) const { return m->mk_ult(*this, m->mk_num(other, size())); } ///< unsigned comparison + bdd operator> (rational const& other) const { return m->mk_ugt(*this, m->mk_num(other, size())); } ///< unsigned comparison + + /* signed comparison operators */ + bdd sle(bddv const& other) const { return m->mk_sle(*this, other); } + bdd sge(bddv const& other) const { return m->mk_sge(*this, other); } + bdd slt(bddv const& other) const { return m->mk_slt(*this, other); } + bdd sgt(bddv const& other) const { return m->mk_sgt(*this, other); } + + bdd all0() const; + bdd all1() const; + + bdd operator==(bddv const& other) const { return m->mk_eq(*this, other); } + bdd operator==(rational const& other) const { return m->mk_eq(*this, other); } + bdd operator!=(bddv const& other) const { return !m->mk_eq(*this, other); } + bdd operator!=(rational const& other) const { return !m->mk_eq(*this, other); } + + bddv operator+(bddv const& other) const { return m->mk_add(*this, other); } + bddv operator+(rational const& other) const { return m->mk_add(*this, m->mk_num(other, size())); } + bddv operator-(bddv const& other) const { return m->mk_sub(*this, other); } + bddv operator-(rational const& other) const { return m->mk_sub(*this, m->mk_num(other, size())); } + bddv rev_sub(rational const& other) const { return m->mk_sub(m->mk_num(other, size()), *this); } + bddv operator*(bddv const& other) const { return m->mk_mul(*this, other); } + bddv operator*(rational const& other) const { return m->mk_mul(*this, other); } + bddv operator*(bool_vector const& other) const { return m->mk_mul(*this, other); } + bddv append(bddv const& other) const { return m->mk_concat(*this, other); } + void quot_rem(bddv const& divisor, bddv& quot, bddv& rem) const { m->mk_quot_rem(*this, divisor, quot, rem); } + + bool is_const() const { return m->is_constv(*this); } + rational to_val() const { return m->to_val(*this); } + }; + + inline bdd operator<=(rational const& r, bddv const& a) { return a >= r; } ///< unsigned comparison + inline bdd operator>=(rational const& r, bddv const& a) { return a <= r; } ///< unsigned comparison + inline bdd operator< (rational const& r, bddv const& a) { return a > r; } ///< unsigned comparison + inline bdd operator> (rational const& r, bddv const& a) { return a < r; } ///< unsigned comparison + inline bdd operator==(rational const& r, bddv const& a) { return a == r; } + inline bdd operator!=(rational const& r, bddv const& a) { return a != r; } + inline bddv operator*(rational const& r, bddv const& a) { return a * r; } + inline bddv operator+(rational const& r, bddv const& a) { return a + r; } + inline bddv operator-(rational const& r, bddv const& a) { return a.rev_sub(r); } + inline bdd operator<=(int i, bddv const& a) { return a >= rational(i); } + inline bdd operator<=(bddv const& a, int i) { return a <= rational(i); } + + } diff --git a/src/math/dd/dd_fdd.cpp b/src/math/dd/dd_fdd.cpp new file mode 100644 index 000000000..21ec82fd1 --- /dev/null +++ b/src/math/dd/dd_fdd.cpp @@ -0,0 +1,366 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + dd_fdd + +Abstract: + + Finite domain abstraction for using BDDs as sets of integers, inspired by BuDDy's fdd module. + +Author: + + Nikolaj Bjorner (nbjorner) 2021-04-20 + Jakob Rath 2021-04-20 + +--*/ + +#include "math/dd/dd_fdd.h" + +namespace dd { + + fdd::fdd(bdd_manager& manager, unsigned_vector&& vars) + : m_pos2var(std::move(vars)) + , m_var2pos() + , m(&manager) + , m_var(manager.mk_var(m_pos2var)) + { + for (unsigned pos = 0; pos < m_pos2var.size(); ++pos) { + unsigned const var = m_pos2var[pos]; + while (var >= m_var2pos.size()) + m_var2pos.push_back(UINT_MAX); + m_var2pos[var] = pos; + } + } + + bdd fdd::non_zero() const { + bdd non_zero = m->mk_false(); + for (unsigned var : m_pos2var) { + non_zero |= m->mk_var(var); + } + return non_zero; + } + + unsigned fdd::var2pos(unsigned var) const { + return var < m_var2pos.size() ? m_var2pos[var] : UINT_MAX; + } + + bool fdd::contains(bdd b, rational const& val) const { + while (!b.is_const()) { + unsigned const pos = var2pos(b.var()); + SASSERT(pos != UINT_MAX && "Unexpected BDD variable"); + b = val.get_bit(pos) ? b.hi() : b.lo(); + } + return b.is_true(); + } + + find_t fdd::find(bdd b, rational& out_val) const { + return find_hint(b, rational::zero(), out_val); + } + + find_t fdd::find_hint(bdd b, rational const& hint, rational& out_val) const { + out_val = 0; + if (b.is_false()) + return find_t::empty; + bool is_unique = true; + bool hint_ok = !hint.is_zero(); // since we choose the 'lo' branch by default, we don't need to check the hint when it is 0. + unsigned num_vars = 0; + while (!b.is_true()) { + ++num_vars; + unsigned const pos = var2pos(b.var()); + SASSERT(pos != UINT_MAX && "Unexpected BDD variable"); + + bool go_hi = false; + if (b.lo().is_false()) { + go_hi = true; + if (hint_ok && !hint.get_bit(pos)) + hint_ok = false; + } + else if (b.hi().is_false()) { + if (hint_ok && hint.get_bit(pos)) + hint_ok = false; + } + else { + // This is the only case where we have a choice + // => follow the hint + SASSERT(!b.lo().is_false() && !b.hi().is_false()); + is_unique = false; + if (hint_ok && hint.get_bit(pos)) + go_hi = true; + } + + if (go_hi) { + out_val += rational::power_of_two(pos); + b = b.hi(); + } + else + b = b.lo(); + } + if (num_vars != num_bits()) + is_unique = false; + // If a variable corresponding to a 1-bit in hint does not appear in the BDD, + // out_val is wrong at this point, so we set it explicitly. + if (hint_ok) + out_val = hint; + // TODO: instead of computing out_val incrementally, we could mark the visited 'hi'-positions and only compute out_val from the marks when !hint_ok. + return is_unique ? find_t::singleton : find_t::multiple; + } + + std::ostream& operator<<(std::ostream& out, find_t x) { + switch (x) { + case find_t::empty: + return out << "empty"; + case find_t::singleton: + return out << "singleton"; + case find_t::multiple: + return out << "multiple"; + } + UNREACHABLE(); + return out; + } + + bool fdd::contains(bdd const& x, bool_vector const& value) const { + bdd b = x; + while (!b.is_true()) { + unsigned const pos = var2pos(b.var()); + SASSERT(pos != UINT_MAX && "Unexpected BDD variable"); + if (value[pos] && b.hi().is_false()) + return false; + if (!value[pos] && b.lo().is_false()) + return false; + if (value[pos]) + b = b.hi(); + else + b = b.lo(); + } + return true; + } + + + // subtract one from x + static void dec(bool_vector& x) { + for (auto& b : x) { + b = !b; + if (!b) + break; + } + } + + // add one to x + static void inc(bool_vector& x) { + for (auto& b : x) { + b = !b; + if (b) + break; + } + } + + static void reset(bool_vector& x, bool value) { + for (auto& b : x) + b = value; + } + + + bool fdd::sup(bdd const& x, bool_vector& lo) const { + SASSERT(lo.size() == num_bits()); + // + // Assumption: common case is that high-order bits are before lower-order bits also + // after re-ordering. Then co-factoring is relatively cheap. + // + + if (!contains(x, lo)) + return false; + + // + // find minimal index where b is false for some + // value larger than lo. + // + // Let ua(x lo) be shorthand for "unbounded-above" of variable + // x with bit-string lo. + // + // we have the following identities: + // ua(_ []) = true + // ua(x 1 ++ lo) = hi(x) = T or ua(hi(x), lo) + // ua(x 0 ++ lo) = hi(x) = T and ua(lo(x), lo) + // + // the least significant bit where ua is false + // represents the position where the smallest number above + // lo resides that violates x. + + unsigned idx = UINT_MAX; + vector trail; + bdd b = x; + for (unsigned i = lo.size(); i-- > 0; ) { + trail.push_back(b); + unsigned v = m_pos2var[i]; + bdd w = m->mk_var(v); + bdd hi = b.cofactor(w); + if (lo[i]) { + if (hi.is_true()) + break; + SASSERT(!hi.is_false()); + b = hi; + } + else { + if (!hi.is_true()) + idx = i; + b = b.cofactor(m->mk_nvar(v)); + } + } + if (idx == UINT_MAX) { + // all values above lo satisfy x + reset(lo, true); + return true; + } + + SASSERT(!lo[idx]); + lo[idx] = true; + unsigned v = m_pos2var[idx]; + b = trail[lo.size() - idx - 1].cofactor(m->mk_var(v)); + for (unsigned i = idx; i-- > 0; ) { + SASSERT(!b.is_true()); + if (b.is_false()) { + for (unsigned j = 0; j <= i; ++j) + lo[j] = false; + break; + } + lo[i] = b.lo().is_true(); + if (lo[i]) + b = b.hi(); + else + b = b.lo(); + } + + dec(lo); + + return true; + } + + bool fdd::inf(bdd const& x, bool_vector& hi) const { + SASSERT(hi.size() == num_bits()); + if (!contains(x, hi)) + return false; + + // Let ub(x hi) be shorthand for "unbounded-below" of variable + // x with bit-string hi. + // + // we have the following identities: + // ub(_ []) = true + // ub(x 0 ++ hi) = lo(x) = T or ub(lo(x), hi) + // ub(x 1 ++ hi) = lo(x) = T and ub(hi(x), hi) + // + + unsigned idx = UINT_MAX; + vector trail; + bdd b = x; + for (unsigned i = hi.size(); i-- > 0; ) { + trail.push_back(b); + unsigned v = m_pos2var[i]; + bdd nw = m->mk_nvar(v); + bdd lo = b.cofactor(nw); + if (!hi[i]) { + if (lo.is_true()) + break; + SASSERT(!lo.is_false()); + b = lo; + } + else { + if (!lo.is_true()) + idx = i; + b = b.cofactor(m->mk_var(v)); + } + } + if (idx == UINT_MAX) { + // all values below hi satisfy x + reset(hi, false); + return true; + } + + SASSERT(hi[idx]); + hi[idx] = false; + unsigned v = m_pos2var[idx]; + b = trail[hi.size() - idx - 1].cofactor(m->mk_nvar(v)); + + for (unsigned i = idx; i-- > 0; ) { + SASSERT(!b.is_true()); + if (b.is_false()) { + for (unsigned j = 0; j <= i; ++j) + hi[j] = true; + break; + } + hi[i] = !b.hi().is_true(); + if (!hi[i]) + b = b.lo(); + else + b = b.hi(); + } + + inc(hi); + + return true; + } + + bool_vector fdd::rational2bits(rational const& r) const { + bool_vector result; + for (unsigned i = 0; i < num_bits(); ++i) + result.push_back(r.get_bit(i)); + return result; + } + + rational fdd::bits2rational(bool_vector const& v) const { + rational result(0); + for (unsigned i = 0; i < num_bits(); ++i) + if (v[i]) + result += rational::power_of_two(i); + return result; + } + + bool fdd::sup(bdd const& b, rational& _lo) const { + bool_vector lo = rational2bits(_lo); + if (!sup(b, lo)) + return false; + _lo = bits2rational(lo); + return true; + } + + bool fdd::inf(bdd const& b, rational& _hi) const { + bool_vector hi = rational2bits(_hi); + if (!inf(b, hi)) + return false; + _hi = bits2rational(hi); + return true; + } + + rational fdd::max(bdd b) const { + SASSERT(!b.is_false()); + rational result(0); + for (unsigned i = num_bits(); i-- > 0; ) { + unsigned v = m_pos2var[i]; + bdd w = m->mk_var(v); + bdd hi = b.cofactor(w); + if (!hi.is_false()) { + b = hi; + result += rational::power_of_two(i); + } + } + return result; + } + + rational fdd::min(bdd b) const { + SASSERT(!b.is_false()); + rational result(0); + for (unsigned i = num_bits(); i-- > 0; ) { + unsigned v = m_pos2var[i]; + bdd nw = m->mk_nvar(v); + bdd lo = b.cofactor(nw); + if (lo.is_false()) + result += rational::power_of_two(i); + else + b = lo; + } + return result; + } + + +} diff --git a/src/math/dd/dd_fdd.h b/src/math/dd/dd_fdd.h new file mode 100644 index 000000000..e17233aa4 --- /dev/null +++ b/src/math/dd/dd_fdd.h @@ -0,0 +1,108 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + dd_fdd + +Abstract: + + Finite domain abstraction for using BDDs as sets of integers, inspired by BuDDy's fdd module. + +Author: + + Jakob Rath 2021-04-20 + Nikolaj Bjorner (nbjorner) 2021-04-20 + +--*/ +#pragma once + +#include "math/dd/dd_bdd.h" +#include "util/vector.h" +#include "util/rational.h" + +namespace dd { + + enum class find_t { empty, singleton, multiple }; + std::ostream& operator<<(std::ostream& out, find_t x); + + /** + * Finite domain abstraction over BDDs. + */ + class fdd { + unsigned_vector m_pos2var; // pos -> BDD var + unsigned_vector m_var2pos; // var -> pos (pos = place number in the bit representation, 0 is LSB's place) + bdd_manager* m; + bddv m_var; + + static unsigned_vector seq(unsigned count, unsigned start = 0, unsigned step = 1) { + unsigned_vector result; + unsigned k = start; + for (unsigned i = 0; i < count; ++i, k += step) + result.push_back(k); + return result; + } + + unsigned var2pos(unsigned var) const; + + bool contains(bdd const& b, bool_vector const& value) const; + + rational bits2rational(bool_vector const& v) const; + + bool_vector rational2bits(rational const& r) const; + + public: + /** Initialize FDD using BDD variables from 0 to num_bits-1. */ + fdd(bdd_manager& manager, unsigned num_bits, unsigned start = 0, unsigned step = 1) : fdd(manager, seq(num_bits, start, step)) { } + fdd(bdd_manager& manager, unsigned_vector const& vars) : fdd(manager, unsigned_vector(vars)) { } + fdd(bdd_manager& manager, unsigned_vector&& vars); + + unsigned num_bits() const { return m_pos2var.size(); } + unsigned_vector const& bdd_vars() const { return m_pos2var; } + + bddv const& var() const { return m_var; } + + /** Equivalent to var() != 0 */ + bdd non_zero() const; + + /** Checks whether the integer val is contained in the BDD when viewed as set of integers. + * Precondition: the bdd only contains variables managed by this fdd. + */ + bool contains(bdd b, rational const& val) const; + + /** Returns an integer contained in the BDD, if any, and whether the BDD is a singleton. + * Precondition: the bdd only contains variables managed by this fdd. + */ + find_t find(bdd b, rational& out_val) const; + + /** Like find, but returns hint if it is contained in the BDD. */ + find_t find_hint(bdd b, rational const& hint, rational& out_val) const; + + /* + * find largest value at lo or above such that bdd b evaluates to true + * at lo and all values between. + * dually, find smallest value below hi that evaluates b to true + * and all values between the value and hi also evaluate b to true. + * \param b - a bdd using variables from this + * \param lo/hi - bound to be traversed. + * \return false if b is false at lo/hi + * \pre variables in b are a subset of variables from the fdd + */ + bool sup(bdd const& b, bool_vector& lo) const; + + bool inf(bdd const& b, bool_vector& hi) const; + + bool sup(bdd const& b, rational& lo) const; + + bool inf(bdd const& b, rational& hi) const; + + /* + * Find the min-max satisfying assignment. + * \pre b is not false. + */ + rational max(bdd b) const; + + rational min(bdd b) const; + }; + +} diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index d08d10a11..12d5b27d8 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -1,7 +1,12 @@ #include "math/dd/dd_bdd.h" +#include "math/dd/dd_fdd.h" #include namespace dd { + +class test_bdd { +public: + static void test1() { bdd_manager m(20); bdd v0 = m.mk_var(0); @@ -10,13 +15,13 @@ namespace dd { bdd c1 = v0 && v1 && v2; bdd c2 = v2 && v0 && v1; std::cout << c1 << "\n"; - SASSERT(c1 == c2); + VERIFY(c1 == c2); std::cout << "cnf size: " << c1.cnf_size() << "\n"; c1 = v0 || v1 || v2; c2 = v2 || v1 || v0; std::cout << c1 << "\n"; - SASSERT(c1 == c2); + VERIFY(c1 == c2); std::cout << "cnf size: " << c1.cnf_size() << "\n"; } @@ -25,14 +30,14 @@ namespace dd { bdd v0 = m.mk_var(0); bdd v1 = m.mk_var(1); bdd v2 = m.mk_var(2); - SASSERT(m.mk_ite(v0,v0,v1) == (v0 || v1)); - SASSERT(m.mk_ite(v0,v1,v1) == v1); - SASSERT(m.mk_ite(v1,v0,v1) == (v0 && v1)); - SASSERT(m.mk_ite(v1,v0,v0) == v0); - SASSERT(m.mk_ite(v0,!v0,v1) == (!v0 && v1)); - SASSERT(m.mk_ite(v0,v1,!v0) == (!v0 || v1)); - SASSERT((!(v0 && v1)) == (!v0 || !v1)); - SASSERT((!(v0 || v1)) == (!v0 && !v1)); + VERIFY(m.mk_ite(v0,v0,v1) == (v0 || v1)); + VERIFY(m.mk_ite(v0,v1,v1) == v1); + VERIFY(m.mk_ite(v1,v0,v1) == (v0 && v1)); + VERIFY(m.mk_ite(v1,v0,v0) == v0); + VERIFY(m.mk_ite(v0,!v0,v1) == (!v0 && v1)); + VERIFY(m.mk_ite(v0,v1,!v0) == (!v0 || v1)); + VERIFY((!(v0 && v1)) == (!v0 || !v1)); + VERIFY((!(v0 || v1)) == (!v0 && !v1)); } static void test3() { @@ -44,19 +49,19 @@ namespace dd { bdd c2 = m.mk_exists(0, c1); std::cout << c1 << "\n"; std::cout << c2 << "\n"; - SASSERT(c2 == (v1 || v2)); + VERIFY(c2 == (v1 || v2)); c2 = m.mk_exists(1, c1); - SASSERT(c2 == (v0 || v2)); + VERIFY(c2 == (v0 || v2)); c2 = m.mk_exists(2, c1); - SASSERT(c2.is_true()); - SASSERT(m.mk_exists(3, c1) == c1); + VERIFY(c2.is_true()); + VERIFY(m.mk_exists(3, c1) == c1); c1 = (v0 && v1) || (v1 && v2) || (!v0 && !v2); c2 = m.mk_exists(0, c1); - SASSERT(c2 == (v1 || (v1 && v2) || !v2)); + VERIFY(c2 == (v1 || (v1 && v2) || !v2)); c2 = m.mk_exists(1, c1); - SASSERT(c2 == (v0 || v2 || (!v0 && !v2))); + VERIFY(c2 == (v0 || v2 || (!v0 && !v2))); c2 = m.mk_exists(2, c1); - SASSERT(c2 == ((v0 && v1) || v1 || !v0)); + VERIFY(c2 == ((v0 && v1) || v1 || !v0)); } static void test4() { @@ -74,11 +79,457 @@ namespace dd { std::cout << c1 << "\n"; std::cout << c1.bdd_size() << "\n"; } + + static void test_xor() { + bdd_manager m(4); + bdd v0 = m.mk_var(0); + bdd v1 = m.mk_var(0); + VERIFY((m.mk_false() ^ v0) == v0); + VERIFY((v0 ^ m.mk_false()) == v0); + VERIFY((m.mk_true() ^ v0) == !v0); + VERIFY((v0 ^ m.mk_true()) == !v0); + VERIFY((v0 ^ v1) == ((v0 && !v1) || (!v0 && v1))); + } + + static void test_bddv_ops_on_constants() { + std::cout << "test_bddv_ops_on_constants\n"; + unsigned const num_bits = 3; + rational const modulus = rational::power_of_two(num_bits); + bdd_manager m(num_bits); + + VERIFY_EQ(m.to_val(m.mk_zero(num_bits)), rational(0)); + VERIFY_EQ(m.to_val(m.mk_ones(num_bits)), modulus - 1); + + for (unsigned n = 0; n < 8; ++n) { + rational const nr(n); + VERIFY_EQ(m.to_val(m.mk_num(nr, num_bits)), nr); + } + + for (unsigned n = 0; n < 8; ++n) { + for (unsigned k = 0; k < 8; ++k) { + rational const nr(n); + rational const kr(k); + bddv const nv = m.mk_num(nr, num_bits); + bddv const kv = m.mk_num(kr, num_bits); + VERIFY_EQ((nv + kv).to_val(), (nr + kr) % modulus); + VERIFY_EQ((nv - kv).to_val(), (nr - kr + modulus) % modulus); + VERIFY_EQ((nv * kr).to_val(), (nr * kr) % modulus); + VERIFY_EQ((nv * kv).to_val(), (nr * kr) % modulus); + bdd eq = m.mk_eq(nv, kv); + VERIFY(eq.is_const() && (eq.is_true() == (n == k))); + eq = m.mk_eq(nv, kr); + VERIFY(eq.is_const() && (eq.is_true() == (n == k))); + + VERIFY(m.mk_usub(nv).to_val() == (m.mk_zero(num_bits) - nv).to_val()); + + bdd cmp = nv <= kv; + VERIFY(cmp.is_const() && (cmp.is_true() == (nr <= kr))); + cmp = nv >= kv; + VERIFY(cmp.is_const() && (cmp.is_true() == (nr >= kr))); + cmp = nv < kv; + VERIFY(cmp.is_const() && (cmp.is_true() == (nr < kr))); + cmp = nv > kv; + VERIFY(cmp.is_const() && (cmp.is_true() == (nr > kr))); + + // signed versions + rational const nrs = (nr < modulus / 2) ? nr : nr - modulus; + rational const krs = (kr < modulus / 2) ? kr : kr - modulus; + cmp = nv.sle(kv); + VERIFY(cmp.is_const() && (cmp.is_true() == (nrs <= krs))); + cmp = nv.sge(kv); + VERIFY(cmp.is_const() && (cmp.is_true() == (nrs >= krs))); + cmp = nv.slt(kv); + VERIFY(cmp.is_const() && (cmp.is_true() == (nrs < krs))); + cmp = nv.sgt(kv); + VERIFY(cmp.is_const() && (cmp.is_true() == (nrs > krs))); + + bddv quotv = m.mk_zero(num_bits); + bddv remv = m.mk_zero(num_bits); + nv.quot_rem(kv, quotv, remv); + if (k != 0) { + VERIFY_EQ(quotv.to_val(), rational(n / k)); + VERIFY_EQ(remv.to_val(), rational(n % k)); + } else { + // std::cout << "n=" << n << " k=" << k << "\n"; + // std::cout << " quot: " << quotv.to_val() << "\n"; + // std::cout << " rem: " << remv.to_val() << "\n"; + } + } + } + } + + static void test_bddv_eqfind_small() { + std::cout << "test_bddv_eqfind_small\n"; + bdd_manager m(4); + fdd const x_dom(m, 1); + bddv const x = x_dom.var(); + bdd x_is_one = (x == rational(1)); + std::cout << "x_is_one:\n" << x_is_one << "\n"; + rational r; + auto res = x_dom.find(x_is_one, r); + VERIFY_EQ(res, find_t::singleton); + VERIFY_EQ(r, rational(1)); + } + + static void test_bddv_eqfind() { + std::cout << "test_bddv_eqfind\n"; + bdd_manager m(4); + + unsigned_vector bits; + bits.push_back(0); + bits.push_back(1); + bits.push_back(4); + bits.push_back(27); + + fdd const x_dom(m, bits); + bddv const x = x_dom.var(); + bddv const zero = m.mk_zero(x_dom.num_bits()); + bddv const one = m.mk_num(rational(1), x_dom.num_bits()); + bddv const five = m.mk_num(rational(5), x_dom.num_bits()); + + VERIFY((one == rational(1)).is_true()); + VERIFY((five == rational(5)).is_true()); + VERIFY((five == rational(4)).is_false()); + VERIFY((five == five).is_true()); + VERIFY((five == one).is_false()); + + // Test the three different mk_eq overloads + { + bdd const x_is_five = m.mk_eq(x, rational(5)); + rational r; + auto res = x_dom.find(x_is_five, r); + VERIFY_EQ(res, find_t::singleton); + VERIFY_EQ(r, 5); + } + + { + bdd const x_is_five = m.mk_eq(bits, rational(5)); + rational r; + auto res = x_dom.find(x_is_five, r); + VERIFY_EQ(res, find_t::singleton); + VERIFY_EQ(r, 5); + } + + { + bdd const x_is_five = m.mk_eq(x, five); + rational r; + auto res = x_dom.find(x_is_five, r); + VERIFY_EQ(res, find_t::singleton); + VERIFY_EQ(r, 5); + } + } + + static void test_bddv_addsub() { + std::cout << "test_bddv_addsub\n"; + unsigned_vector bits; + bits.push_back(0); + bits.push_back(1); + bits.push_back(2); + bdd_manager m(bits.size()); + bddv const x = m.mk_var(bits); + VERIFY_EQ(x - rational(3) == rational(2), x == rational(5)); + VERIFY_EQ(x + rational(3) == rational(5), x == rational(2)); + VERIFY_EQ(x - rational(3) == rational(6), x == rational(1)); + VERIFY_EQ(x + rational(3) == rational(2), x == rational(7)); + } + + static void test_bddv_mul() { + std::cout << "test_bddv_mul\n"; + unsigned const num_bits = 4; + bdd_manager m(num_bits); + + unsigned_vector bits; + bits.push_back(0); + bits.push_back(1); + bits.push_back(4); + bits.push_back(27); + + bddv const x = m.mk_var(bits); + bddv const zero = m.mk_zero(num_bits); + bddv const one = m.mk_num(rational(1), num_bits); + bddv const five = m.mk_num(rational(5), num_bits); + bddv const six = m.mk_num(rational(6), num_bits); + + // 5*x == 1 (mod 16) => x == 13 (mod 16) + bdd const five_inv = x * five == one; + VERIFY_EQ(five_inv, x == rational(13)); + + // 6*x == 1 (mod 16) => no solution for x + bdd const six_inv = x * six == one; + VERIFY(six_inv.is_false()); + + // 6*x == 0 (mod 16) => x is either 0 or 8 (mod 16) + bdd const b = six * x == zero; + VERIFY_EQ(b, x == rational(0) || x == rational(8)); + VERIFY((b && (x != rational(0)) && (x != rational(8))).is_false()); + VERIFY_EQ(b && (x != rational(0)), x == rational(8)); + + VERIFY_EQ((x * zero).bits(), (x * rational(0)).bits()); + VERIFY_EQ((x * one).bits(), (x * rational(1)).bits()); + VERIFY_EQ((x * five).bits(), (x * rational(5)).bits()); + VERIFY_EQ((x * six).bits(), (x * rational(6)).bits()); + } + + static void test_bddv_ule() { + std::cout << "test_bddv_ule\n"; + unsigned const num_bits = 4; + bdd_manager m(num_bits); + + unsigned_vector bits; + bits.push_back(0); + bits.push_back(1); + bits.push_back(2); + bits.push_back(3); + + bddv const x = m.mk_var(bits); + bddv const three = m.mk_num(rational(3), num_bits); + bddv const four = m.mk_num(rational(4), num_bits); + bddv const five = m.mk_num(rational(5), num_bits); + + VERIFY_EQ(x >= four && x < five, x == four); + VERIFY_EQ(four <= x && x < five, x == four); + VERIFY_EQ(three < x && x < five, x == four); + VERIFY_EQ(three < x && x <= four, x == four); + VERIFY_EQ(three <= x && x < five, x == four || x == three); + } + + static void test_fdd3() { + std::cout << "test_fdd3\n"; + unsigned const w = 3; // bit width + bdd_manager m(w); + + fdd const x_dom(m, w); + bddv const& x = x_dom.var(); + + // Encodes the values x satisfying a*x + b == 0 (mod 2^w) as BDD. + auto mk_affine = [] (unsigned a, bddv const& x, unsigned b) { + return (rational(a)*x + rational(b) == rational(0)); + }; + + vector num; + for (unsigned n = 0; n < (1< num; + for (unsigned n = 0; n < (1ul << x_dom.num_bits()); ++n) { + num.push_back(x == rational(n)); + VERIFY(x_dom.contains(num[n], rational(n))); + rational r; + VERIFY_EQ(x_dom.find(num[n], r), find_t::singleton); + VERIFY_EQ(r, n); + } + + // need something extra to skew costs and trigger a reorder + bdd atleast3 = (x >= rational(3)); + VERIFY(x_dom.contains(atleast3, rational(3))); + + auto const old_levels = m.m_var2level; + std::cout << "old levels: " << old_levels << "\n"; + m.gc(); + m.try_reorder(); + std::cout << "new levels: " << m.m_var2level << "\n"; + VERIFY(old_levels != m.m_var2level); // ensure that reorder actually did something. + + // Should still give the correct answer after reordering + for (unsigned n = 0; n < (1ul << x_dom.num_bits()); ++n) { + VERIFY(x_dom.contains(num[n], rational(n))); + rational r; + VERIFY_EQ(x_dom.find(num[n], r), find_t::singleton); + VERIFY_EQ(r, n); + } + } + + static void test_fdd_twovars() { + std::cout << "test_fdd_twovars\n"; + bdd_manager m(6); + fdd const x_dom(m, 3, 0, 2); + fdd const y_dom(m, 3, 1, 2); + bddv const& x = x_dom.var(); + bddv const& y = y_dom.var(); + VERIFY_EQ(x - y <= rational(0), x == y); + } + + static void test_fdd_find_hint() { + std::cout << "test_fdd_find_hint\n"; + bdd_manager m(4); + fdd const x_dom(m, 4); + bddv const& x = x_dom.var(); + + bdd s358 = x == rational(3) || x == rational(5) || x == rational(8); + rational r; + VERIFY_EQ(x_dom.find_hint(s358, rational(8), r), find_t::multiple); + VERIFY_EQ(r, 8); + VERIFY_EQ(x_dom.find_hint(s358, rational(5), r), find_t::multiple); + VERIFY_EQ(r, 5); + VERIFY_EQ(x_dom.find_hint(s358, rational(3), r), find_t::multiple); + VERIFY_EQ(r, 3); + VERIFY_EQ(x_dom.find_hint(s358, rational(7), r), find_t::multiple); + VERIFY(r == 3 || r == 5 || r == 8); + + VERIFY_EQ(x_dom.find_hint(x == rational(5), rational(3), r), find_t::singleton); + VERIFY_EQ(r, 5); + VERIFY_EQ(x_dom.find_hint(x == rational(5), rational(5), r), find_t::singleton); + VERIFY_EQ(r, 5); + + VERIFY_EQ(x_dom.find_hint(s358 && (x == rational(4)), rational(5), r), find_t::empty); + } + + static void test_cofactor() { + std::cout << "test_cofactor\n"; + bdd_manager m(20); + bdd v0 = m.mk_var(0); + bdd v1 = m.mk_var(1); + bdd v2 = m.mk_var(2); + bdd c1 = v0 && v1 && v2; + VERIFY(c1.cofactor(v0) == (v1 && v2)); + VERIFY(c1.cofactor(v1) == (v0 && v2)); + VERIFY(c1.cofactor(v2) == (v0 && v1)); + VERIFY(c1.cofactor(!v1) == m.mk_false()); + } + + static void inc(bool_vector& x) { + for (auto& b : x) { + b = !b; + if (b) + break; + } + } + + static void dec(bool_vector& x) { + for (auto& b : x) { + b = !b; + if (!b) + break; + } + } + + static unsigned value(bool_vector const& x) { + unsigned p = 1; + unsigned v = 0; + for (auto b : x) { + v += p*b; + p <<= 1; + } + return v; + } + + static void test_sup() { + std::cout << "test_sup\n"; + bdd_manager m(20); + fdd const x_dom(m, 10); + bddv const& x = x_dom.var(); + bdd c = (1 <= x && x <= 5) || (11 <= x && x <= 13) || (29 <= x && x <= 33); + bool_vector lo(10, false); + for (unsigned i = 0; i < 20; ++i) { + unsigned v = value(lo); + bool found = x_dom.sup(c, lo); + std::cout << found << ": " << v << " - " << value(lo) << "\n"; + if (found) + std::cout << x_dom.sup(c, lo) << ": " << value(lo) << "\n"; + c = !c; + inc(lo); + } + } + + static void test_inf() { + std::cout << "test_inf\n"; + bdd_manager m(20); + fdd const x_dom(m, 10); + bddv const& x = x_dom.var(); + bdd c = (1 <= x && x <= 5) || (11 <= x && x <= 13) || (29 <= x && x <= 33); + bool_vector hi(10, true); + for (unsigned i = 0; i < 10; ++i) { + bool found = x_dom.inf(c, hi); + std::cout << found << ": " << value(hi) << "\n"; + if (found) { + std::cout << x_dom.inf(c, hi) << ": " << value(hi) << "\n"; + VERIFY(value(hi) == 0 || value(hi) == 1 || value(hi) == 5 || value(hi) == 6 || + value(hi) == 10 || value(hi) == 11 || + value(hi) == 13 || value(hi) == 14 || + value(hi) == 28 || value(hi) == 29 || + value(hi) == 33 || value(hi) == 34 || value(hi) == 1023); + } + c = !c; + dec(hi); + } + } + + + +}; + } void tst_bdd() { - dd::test1(); - dd::test2(); - dd::test3(); - dd::test4(); + dd::test_bdd::test1(); + dd::test_bdd::test2(); + dd::test_bdd::test3(); + dd::test_bdd::test4(); + dd::test_bdd::test_xor(); + dd::test_bdd::test_bddv_ops_on_constants(); + dd::test_bdd::test_bddv_eqfind_small(); + dd::test_bdd::test_bddv_eqfind(); + dd::test_bdd::test_bddv_addsub(); + dd::test_bdd::test_bddv_mul(); + dd::test_bdd::test_bddv_ule(); + dd::test_bdd::test_fdd3(); + dd::test_bdd::test_fdd4(); + dd::test_bdd::test_fdd_reorder(); + dd::test_bdd::test_fdd_twovars(); + dd::test_bdd::test_fdd_find_hint(); + dd::test_bdd::test_cofactor(); + dd::test_bdd::test_inf(); + dd::test_bdd::test_sup(); } From de6a0ab1a7991e8bc713621320b319131f57e1a6 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 14:49:06 +0200 Subject: [PATCH 09/19] PDD operations --- src/math/dd/dd_pdd.cpp | 511 ++++++++++++++++++++++++++++++++++++++--- src/math/dd/dd_pdd.h | 123 ++++++++-- src/test/pdd.cpp | 301 +++++++++++++++++++++++- 3 files changed, 877 insertions(+), 58 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index b8946ebf6..cca2d5e04 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -34,6 +34,7 @@ namespace dd { s = mod2_e; m_semantics = s; m_mod2N = rational::power_of_two(power_of_2); + m_max_value = m_mod2N - 1; m_power_of_2 = power_of_2; unsigned_vector l2v; for (unsigned i = 0; i < num_vars; ++i) l2v.push_back(i); @@ -50,6 +51,7 @@ namespace dd { void pdd_manager::reset(unsigned_vector const& level2var) { reset_op_cache(); + m_factor_cache.reset(); m_node_table.reset(); m_nodes.reset(); m_free_nodes.reset(); @@ -126,7 +128,7 @@ namespace dd { * Example: 2^4*x + 2 is non-zero for every x. */ - bool pdd_manager::is_non_zero(PDD p) { + bool pdd_manager::is_never_zero(PDD p) { if (is_val(p)) return !is_zero(p); if (m_semantics != mod2N_e) @@ -163,7 +165,11 @@ namespace dd { return true; } - pdd pdd_manager::subst_val(pdd const& p, vector> const& _s) { + pdd pdd_manager::subst_val(pdd const& p, pdd const& s) { + return pdd(apply(p.root, s.root, pdd_subst_val_op), this); + } + + pdd pdd_manager::subst_val0(pdd const& p, vector> const& _s) { typedef std::pair pr; vector s(_s); std::function compare_level = @@ -171,10 +177,16 @@ namespace dd { std::sort(s.begin(), s.end(), compare_level); pdd r(one()); for (auto const& q : s) - r = (r*mk_var(q.first)) + q.second; - return pdd(apply(p.root, r.root, pdd_subst_val_op), this); + r = (r * mk_var(q.first)) + q.second; + return subst_val(p, r); } + pdd pdd_manager::subst_add(pdd const& s, unsigned v, rational const& val) { + pdd v_val = mk_var(v) + val; + return pdd(apply(s.root, v_val.root, pdd_subst_add_op), this); + } + + pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) { bool first = true; SASSERT(well_formed()); @@ -216,6 +228,7 @@ namespace dd { if (is_val(p) && is_val(q)) return imk_val(val(p) - val(q)); if (m_semantics != mod2_e) break; op = pdd_add_op; + Z3_fallthrough; case pdd_add_op: if (is_zero(p)) return q; if (is_zero(q)) return p; @@ -239,12 +252,16 @@ namespace dd { break; case pdd_subst_val_op: while (!is_val(q) && !is_val(p)) { - if (level(p) == level(q)) break; - if (level(p) < level(q)) q = lo(q); - else p = lo(p); + if (level(p) < level(q)) q = hi(q); + else break; } if (is_val(p) || is_val(q)) return p; break; + case pdd_subst_add_op: + if (is_one(p)) return q; + SASSERT(!is_val(p)); + SASSERT(!is_val(q)); + break; default: UNREACHABLE(); break; @@ -345,7 +362,8 @@ namespace dd { push(make_node(level_p, lo(n), read(1))); r = make_node(level_p, bd, read(1)); npop = 7; - } else { + } + else { push(make_node(level_p, n, ac)); r = make_node(level_p, bd, read(1)); npop = 6; @@ -387,12 +405,33 @@ namespace dd { case pdd_subst_val_op: SASSERT(!is_val(p)); SASSERT(!is_val(q)); - SASSERT(level_p == level_q); + SASSERT(level_p >= level_q); push(apply_rec(lo(p), q, pdd_subst_val_op)); // lo := subst(lo(p), s) push(apply_rec(hi(p), q, pdd_subst_val_op)); // hi := subst(hi(p), s) - push(apply_rec(lo(q), read(1), pdd_mul_op)); // hi := hi*s[var(p)] - r = apply_rec(read(1), read(3), pdd_add_op); // r := hi + lo := subst(lo(p),s) + s[var(p)]*subst(hi(p),s) - npop = 3; + + if (level_p > level_q) { + r = make_node(level_p, read(2), read(1)); + npop = 2; + } + else { + push(apply_rec(lo(q), read(1), pdd_mul_op)); // hi := hi*s[var(p)] + r = apply_rec(read(1), read(3), pdd_add_op); // r := hi + lo := subst(lo(p),s) + s[var(p)]*subst(hi(p),s) + npop = 3; + } + break; + case pdd_subst_add_op: + SASSERT(!is_val(p)); + SASSERT(!is_val(q)); + SASSERT(level_p != level_q); + if (level_p < level_q) { + r = make_node(level_q, lo(q), p); // p*hi(q) + lo(q) + npop = 0; + } + else { + push(apply_rec(hi(p), q, pdd_subst_add_op)); // hi := add_subst(hi(p), q) + r = make_node(level_p, lo(p), read(1)); // r := hi*var(p) + lo(p) + npop = 1; + } break; default: r = null_pdd; @@ -405,6 +444,7 @@ namespace dd { return r; } + pdd pdd_manager::minus(pdd const& a) { if (m_semantics == mod2_e) { return a; @@ -442,6 +482,113 @@ namespace dd { return r; } + /** + * Divide PDD by a constant value. + * + * IMPORTANT: Performs regular numerical division. + * For semantics 'mod2N_e', this means that 'c' must be an integer + * and all coefficients of 'a' must be divisible by 'c'. + * + * NOTE: Why do we not just use 'mul(a, inv(c))' instead? + * In case of semantics 'mod2N_e', an invariant is that all PDDs have integer coefficients. + * But such a multiplication would create nodes with non-integral coefficients. + */ + pdd pdd_manager::div(pdd const& a, rational const& c) { + pdd res(zero_pdd, this); + VERIFY(try_div(a, c, res)); + return res; + } + + bool pdd_manager::try_div(pdd const& a, rational const& c, pdd& out_result) { + if (m_semantics == free_e) { + // Don't cache separately for the free semantics; + // use 'mul' so we can share results for a/c and a*(1/c). + out_result = mul(inv(c), a); + return true; + } + SASSERT(c.is_int()); + bool first = true; + SASSERT(well_formed()); + scoped_push _sp(*this); + while (true) { + try { + PDD res = div_rec(a.root, c, null_pdd); + if (res != null_pdd) + out_result = pdd(res, this); + SASSERT(well_formed()); + return res != null_pdd; + } + catch (const mem_out &) { + try_gc(); + if (!first) throw; + first = false; + } + } + } + + /// Returns null_pdd if one of the coefficients is not divisible by c. + pdd_manager::PDD pdd_manager::div_rec(PDD a, rational const& c, PDD c_pdd) { + SASSERT(m_semantics != free_e); + SASSERT(c.is_int()); + if (is_zero(a)) + return zero_pdd; + if (is_val(a)) { + rational r = val(a) / c; + if (r.is_int()) + return imk_val(r); + else + return null_pdd; + } + if (c_pdd == null_pdd) + c_pdd = imk_val(c); + op_entry* e1 = pop_entry(a, c_pdd, pdd_div_const_op); + op_entry const* e2 = m_op_cache.insert_if_not_there(e1); + if (check_result(e1, e2, a, c_pdd, pdd_div_const_op)) + return e2->m_result; + push(div_rec(lo(a), c, c_pdd)); + push(div_rec(hi(a), c, c_pdd)); + PDD l = read(2); + PDD h = read(1); + PDD res = null_pdd; + if (l != null_pdd && h != null_pdd) + res = make_node(level(a), l, h); + pop(2); + e1->m_result = res; + return res; + } + + pdd pdd_manager::pow(pdd const &p, unsigned j) { + return pdd(pow(p.root, j), this); + } + + pdd_manager::PDD pdd_manager::pow(PDD p, unsigned j) { + if (j == 0) + return one_pdd; + else if (j == 1) + return p; + else if (is_zero(p)) + return zero_pdd; + else if (is_one(p)) + return one_pdd; + else if (is_val(p)) + return imk_val(power(val(p), j)); + else + return pow_rec(p, j); + } + + pdd_manager::PDD pdd_manager::pow_rec(PDD p, unsigned j) { + SASSERT(j > 0); + if (j == 1) + return p; + // j even: pow(p,2*j') = pow(p*p,j') + // j odd: pow(p,2*j'+1) = p*pow(p*p,j') + PDD q = pow_rec(apply(p, p, pdd_mul_op), j / 2); + if (j & 1) { + q = apply(q, p, pdd_mul_op); + } + return q; + } + // // produce polynomial where a is reduced by b. // all monomials in a that are divisible by lm(b) @@ -691,27 +838,37 @@ namespace dd { * factor p into lc*v^degree + rest * such that degree(rest, v) < degree * Initial implementation is very naive - * - memoize intermediary results */ void pdd_manager::factor(pdd const& p, unsigned v, unsigned degree, pdd& lc, pdd& rest) { unsigned level_v = m_var2level[v]; if (degree == 0) { - lc = p; - rest = zero(); - } - else if (level(p.root) < level_v) { lc = zero(); rest = p; + return; } - else if (level(p.root) > level_v) { + if (level(p.root) < level_v) { + lc = zero(); + rest = p; + return; + } + // Memoize nontrivial cases + auto* et = m_factor_cache.insert_if_not_there2({p.root, v, degree}); + factor_entry* e = &et->get_data(); + if (e->is_valid()) { + lc = pdd(e->m_lc, this); + rest = pdd(e->m_rest, this); + return; + } + + if (level(p.root) > level_v) { pdd lc1 = zero(), rest1 = zero(); pdd vv = mk_var(p.var()); factor(p.hi(), v, degree, lc, rest); factor(p.lo(), v, degree, lc1, rest1); - lc += lc1; - rest += rest1; lc *= vv; rest *= vv; + lc += lc1; + rest += rest1; } else { unsigned d = 0; @@ -733,8 +890,228 @@ namespace dd { rest = p; } } + et = m_factor_cache.insert_if_not_there2({p.root, v, degree}); + e = &et->get_data(); + e->m_lc = lc.root; + e->m_rest = rest.root; } + bool pdd_manager::factor(pdd const& p, unsigned v, unsigned degree, pdd& lc) { + pdd rest = lc; + factor(p, v, degree, lc, rest); + return rest.is_zero(); + } + + /** + * Apply function f to all coefficients of the polynomial. + * The function should be of type + * rational const& -> rational + * rational const& -> unsigned + * and should always return integers. + * + * NOTE: the operation is not cached. + */ + template + pdd pdd_manager::map_coefficients(pdd const& p, Fn f) { + if (p.is_val()) { + return mk_val(rational(f(p.val()))); + } else { + pdd x = mk_var(p.var()); + pdd lo = map_coefficients(p.lo(), f); + pdd hi = map_coefficients(p.hi(), f); + return x*hi + lo; + } + } + + /** + * Perform S-polynomial reduction on p by q, + * treating monomial with v as leading. + * + * p = a v^l + b = a' 2^j v^l + b + * q = c v^m + d = c' 2^j v^m + d + * such that + * deg(v, p) = l, i.e., v does not divide a and there is no v^l in b + * deg(v, q) = m, i.e., v does not divide c and there is no v^m in d + * l >= m + * j maximal, i.e., not both of a', c' are divisible by 2 + * + * Then we reduce p by q: + * + * r = c' p - a' v^(l-m) q + * = b c' - a' d v^(l-m) + */ + bool pdd_manager::resolve(unsigned v, pdd const& p, pdd const& q, pdd& r) { + unsigned const l = p.degree(v); + unsigned const m = q.degree(v); + // no reduction + if (l < m || m == 0) + return false; + + pdd a = zero(); + pdd b = zero(); + pdd c = zero(); + pdd d = zero(); + p.factor(v, l, a, b); + q.factor(v, m, c, d); + unsigned const j = std::min(max_pow2_divisor(a), max_pow2_divisor(c)); + SASSERT(j != UINT_MAX); // should only be possible when both l and m are 0 + rational const pow2j = rational::power_of_two(j); + pdd const aa = div(a, pow2j); + pdd const cc = div(c, pow2j); + pdd vv = pow(mk_var(v), l - m); + r = b * cc - aa * d * vv; + return true; + } + + /** + * Reduce polynomial a with respect to b by eliminating terms using v + * + * a := a1*v^l + a2 + * b := b1*v^m + b2 + * l >= m + * q, r := quot_rem(a1, b1) + * that is: + * q * b1 + r = a1 + * r = 0 + * result := reduce(v, q*b2*v^{l-m}, b) + reduce(v, a2, b) + */ + pdd pdd_manager::reduce(unsigned v, pdd const& a, pdd const& b) { + unsigned const m = b.degree(v); + // no reduction + if (m == 0) + return a; + + pdd b1 = zero(); + pdd b2 = zero(); + b.factor(v, m, b1, b2); + + // TODO - generalize this case to when leading coefficient is not a value + if (m_semantics == mod2N_e && b1.is_val() && b1.val().is_odd() && !b1.is_one()) { + rational b_inv; + VERIFY(b1.val().mult_inverse(m_power_of_2, b_inv)); + b1 = 1; + b2 *= b_inv; + } + + return reduce(v, a, m, b1, b2); + } + + pdd pdd_manager::reduce(unsigned v, pdd const& a, unsigned m, pdd const& b1, pdd const& b2) { + SASSERT(m > 0); + unsigned const l = a.degree(v); + if (l < m) + return a; + + pdd a1 = zero(); + pdd a2 = zero(); + pdd q = zero(); + pdd r = zero(); + a.factor(v, l, a1, a2); + + quot_rem(a1, b1, q, r); + if (r.is_zero()) { + SASSERT(q * b1 == a1); + a1 = -q * b2; + if (l > m) + a1 = reduce(v, a1 * pow(mk_var(v), l - m), m, b1, b2); + } + else + a1 = a1 * pow(mk_var(v), l); + a2 = reduce(v, a2, m, b1, b2); + + return a1 + a2; + } + + /** + * quotient/remainder of 'a' divided by 'b' + * a := x*hi + lo + * x > level(b): + * hi = q1*b + r1 + * lo = q2*b + r2 + * x*hi + lo = (x*q1 + q2)*b + (x*r1 + r2) + * q := x*q1 + q2 + * r := x*r1 + r2 + * Some special cases. + * General multi-variable polynomial division is TBD. + */ + void pdd_manager::quot_rem(pdd const& a, pdd const& b, pdd& q, pdd& r) { + if (level(a.root) > level(b.root)) { + pdd q1(*this), q2(*this), r1(*this), r2(*this); + quot_rem(a.hi(), b, q1, r1); + quot_rem(a.lo(), b, q2, r2); + q = mk_var(a.var()) * q1 + q2; + r = mk_var(a.var()) * r1 + r2; + } + else if (level(a.root) < level(b.root)) { + q = zero(); + r = a; + } + else if (a == b) { + q = one(); + r = zero(); + } + else if (a.is_val() && b.is_val() && divides(b.val(), a.val())) { + q = mk_val(a.val() / b.val()); + r = zero(); + } + else if (a.is_val() || b.is_val()) { + q = zero(); + r = a; + } + else { + SASSERT(level(a.root) == level(b.root)); + pdd q1(*this), q2(*this), r1(*this), r2(*this); + quot_rem(a.hi(), b.hi(), q1, r1); + quot_rem(a.lo(), b.lo(), q2, r2); + if (q1 == q2 && r1.is_zero() && r2.is_zero()) { + q = q1; + r = zero(); + } + else { + q = zero(); + r = a; + } + } + } + + /** + * Returns the largest j such that 2^j divides p. + */ + unsigned pdd_manager::max_pow2_divisor(PDD p) { + init_mark(); + unsigned min_j = UINT_MAX; + m_todo.push_back(p); + while (!m_todo.empty()) { + PDD r = m_todo.back(); + m_todo.pop_back(); + if (is_marked(r)) { + continue; + } + set_mark(r); + if (is_zero(r)) { + // skip + } + else if (is_val(r)) { + rational const& c = val(r); + if (c.is_odd()) { + m_todo.reset(); + return 0; + } else { + unsigned j = c.trailing_zeros(); + min_j = std::min(j, min_j); + } + } + else { + m_todo.push_back(lo(r)); + m_todo.push_back(hi(r)); + } + } + return min_j; + } + + unsigned pdd_manager::max_pow2_divisor(pdd const& p) { + return max_pow2_divisor(p.root); + } bool pdd_manager::is_linear(pdd const& p) { return is_linear(p.root); @@ -764,6 +1141,32 @@ namespace dd { } } + /** Determine whether p contains at most one variable. */ + bool pdd_manager::is_univariate(PDD p) { + unsigned const lvl = level(p); + while (!is_val(p)) { + if (!is_val(lo(p))) + return false; + if (level(p) != lvl) + return false; + p = hi(p); + } + return true; + } + + /** + * Push coefficients of univariate polynomial in order of ascending degree. + * Example: a*x^2 + b*x + c ==> [ c, b, a ] + */ + void pdd_manager::get_univariate_coefficients(PDD p, vector& coeff) { + SASSERT(is_univariate(p)); + while (!is_val(p)) { + coeff.push_back(val(lo(p))); + p = hi(p); + } + coeff.push_back(val(p)); + } + /* \brief determine if v occurs as a leaf variable. */ @@ -832,9 +1235,8 @@ namespace dd { if (m_semantics == mod2N_e && (r < 0 || r >= m_mod2N)) return imk_val(mod(r, m_mod2N)); const_info info; - if (!m_mpq_table.find(r, info)) { + if (!m_mpq_table.find(r, info)) init_value(info, r); - } return info.m_node_index; } @@ -1005,7 +1407,7 @@ namespace dd { unsigned pdd_manager::degree(PDD p, unsigned v) { init_mark(); - unsigned level_v = level(v); + unsigned level_v = m_var2level[v]; unsigned max_d = 0, d = 0; m_todo.push_back(p); while (!m_todo.empty()) { @@ -1017,15 +1419,17 @@ namespace dd { else if (level(r) < level_v) m_todo.pop_back(); else if (level(r) == level_v) { - d = 1; - while (!is_val(hi(r)) && level(hi(r)) == level_v) { + d = 0; + do { ++d; + set_mark(r); r = hi(r); - } + } while (!is_val(r) && level(r) == level_v); max_d = std::max(d, max_d); m_todo.pop_back(); } else { + set_mark(r); m_todo.push_back(lo(r)); m_todo.push_back(hi(r)); } @@ -1128,6 +1532,7 @@ namespace dd { } void pdd_manager::gc() { + m_gc_generation++; init_dmark(); m_free_nodes.reset(); SASSERT(well_formed()); @@ -1167,6 +1572,8 @@ namespace dd { m_op_cache.insert(e); } + m_factor_cache.reset(); + m_node_table.reset(); // re-populate node cache for (unsigned i = m_nodes.size(); i-- > 2; ) { @@ -1221,14 +1628,32 @@ namespace dd { rational c = abs(m.first); m.second.reverse(); if (!c.is_one() || m.second.empty()) { - out << c; + if (m_semantics == mod2N_e && mod(-c, m_mod2N) < c) + out << -mod(-c, m_mod2N); + else + out << c; if (!m.second.empty()) out << "*"; } - bool f = true; + unsigned v_prev = UINT_MAX; + unsigned pow = 0; for (unsigned v : m.second) { - if (!f) out << "*"; - f = false; - out << "v" << v; + if (v == v_prev) { + pow++; + continue; + } + if (v_prev != UINT_MAX) { + out << "v" << v_prev; + if (pow > 1) + out << "^" << pow; + out << "*"; + } + pow = 1; + v_prev = v; + } + if (v_prev != UINT_MAX) { + out << "v" << v_prev; + if (pow > 1) + out << "^" << pow; } } if (first) out << "0"; @@ -1291,6 +1716,30 @@ namespace dd { return *this; } + pdd& pdd::operator=(unsigned k) { + m.dec_ref(root); + root = m.mk_val(k).root; + m.inc_ref(root); + return *this; + } + + pdd& pdd::operator=(rational const& k) { + m.dec_ref(root); + root = m.mk_val(k).root; + m.inc_ref(root); + return *this; + } + + rational const& pdd::leading_coefficient() const { + pdd p = *this; + while (!p.is_val()) + p = p.hi(); + return p.val(); + } + + pdd pdd::shl(unsigned n) const { + return (*this) * rational::power_of_two(n); + } /** * \brief substitute variable v by r. diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 9cd454698..aef0eb6f7 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -23,6 +23,11 @@ Abstract: - try_spoly(a, b, c) returns true if lt(a) and lt(b) have a non-trivial overlap. c is the resolvent (S polynomial). + - reduce(v, a, b) reduces 'a' using b = 0 with respect to eliminating v. + Given b = v^l*b1 + b2, where l is the leading coefficient of v in b + Given a = v^m*a1 + b2, where m >= l is the leading coefficient of v in b. + reduce(a1, b1)*v^{m - l} + reduce(v, a2, b); + Author: Nikolaj Bjorner (nbjorner) 2019-12-17 @@ -63,7 +68,9 @@ namespace dd { pdd_mul_op = 5, pdd_reduce_op = 6, pdd_subst_val_op = 7, - pdd_no_op = 8 + pdd_subst_add_op = 8, + pdd_div_const_op = 9, + pdd_no_op = 10 }; struct node { @@ -140,9 +147,44 @@ namespace dd { typedef ptr_hashtable op_table; + struct factor_entry { + factor_entry(PDD p, unsigned v, unsigned degree): + m_p(p), + m_v(v), + m_degree(degree), + m_lc(UINT_MAX), + m_rest(UINT_MAX) + {} + + factor_entry(): m_p(0), m_v(0), m_degree(0), m_lc(UINT_MAX), m_rest(UINT_MAX) {} + + PDD m_p; // input + unsigned m_v; // input + unsigned m_degree; // input + PDD m_lc; // output + PDD m_rest; // output + + bool is_valid() { return m_lc != UINT_MAX; } + + unsigned hash() const { return mk_mix(m_p, m_v, m_degree); } + }; + + struct hash_factor_entry { + unsigned operator()(factor_entry const& e) const { return e.hash(); } + }; + + struct eq_factor_entry { + bool operator()(factor_entry const& a, factor_entry const& b) const { + return a.m_p == b.m_p && a.m_v == b.m_v && a.m_degree == b.m_degree; + } + }; + + typedef hashtable factor_table; + svector m_nodes; vector m_values; op_table m_op_cache; + factor_table m_factor_cache; node_table m_node_table; mpq_table m_mpq_table; svector m_pdd_stack; @@ -164,7 +206,9 @@ namespace dd { unsigned_vector m_free_values; rational m_freeze_value; rational m_mod2N; - unsigned m_power_of_2 { 0 }; + 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); @@ -177,6 +221,9 @@ namespace dd { PDD apply(PDD arg1, PDD arg2, pdd_op op); PDD apply_rec(PDD arg1, PDD arg2, pdd_op op); PDD minus_rec(PDD p); + PDD div_rec(PDD p, rational const& c, PDD c_pdd); + PDD pow(PDD p, unsigned j); + PDD pow_rec(PDD p, unsigned j); PDD reduce_on_match(PDD a, PDD b); bool lm_occurs(PDD p, PDD q) const; @@ -206,7 +253,8 @@ namespace dd { inline bool is_one(PDD p) const { return p == one_pdd; } 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(); } - bool is_non_zero(PDD p); + inline bool is_var(PDD p) const { return !is_val(p) && is_zero(lo(p)) && is_one(hi(p)); } + bool is_never_zero(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; } @@ -226,8 +274,14 @@ namespace dd { unsigned degree(pdd const& p) const; unsigned degree(PDD p) const; unsigned degree(PDD p, unsigned v); + unsigned max_pow2_divisor(PDD p); + unsigned max_pow2_divisor(pdd const& p); + template pdd map_coefficients(pdd const& p, Fn f); void factor(pdd const& p, unsigned v, unsigned degree, pdd& lc, pdd& rest); + bool factor(pdd const& p, unsigned v, unsigned degree, pdd& lc); + + pdd reduce(unsigned v, pdd const& a, unsigned m, pdd const& b1, pdd const& b2); bool var_is_leaf(PDD p, unsigned v); @@ -258,7 +312,7 @@ namespace dd { struct mem_out {}; - pdd_manager(unsigned nodes, semantics s = free_e, unsigned power_of_2 = 0); + pdd_manager(unsigned num_vars, semantics s = free_e, unsigned power_of_2 = 0); ~pdd_manager(); semantics get_semantics() const { return m_semantics; } @@ -278,13 +332,21 @@ namespace dd { pdd sub(pdd const& a, pdd const& b); pdd mul(pdd const& a, pdd const& b); pdd mul(rational const& c, pdd const& b); + pdd div(pdd const& a, rational const& c); + bool try_div(pdd const& a, rational const& c, pdd& out_result); pdd mk_or(pdd const& p, pdd const& q); pdd mk_xor(pdd const& p, pdd const& q); pdd mk_xor(pdd const& p, unsigned q); pdd mk_not(pdd const& p); pdd reduce(pdd const& a, pdd const& b); - pdd subst_val(pdd const& a, vector> const& s); + pdd subst_val0(pdd const& a, vector> const& s); 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 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); + pdd pow(pdd const& p, unsigned j); bool is_linear(PDD p) { return degree(p) == 1; } bool is_linear(pdd const& p); @@ -294,6 +356,9 @@ namespace dd { bool is_monomial(PDD p); + bool is_univariate(PDD p); + void get_univariate_coefficients(PDD p, vector& coeff); + // create an spoly r if leading monomials of a and b overlap bool try_spoly(pdd const& a, pdd const& b, pdd& r); @@ -308,6 +373,8 @@ namespace dd { unsigned num_vars() const { return m_var2pdd.size(); } 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; } unsigned_vector const& free_vars(pdd const& p); @@ -330,21 +397,30 @@ namespace dd { pdd(pdd const& other): root(other.root), m(other.m) { m.inc_ref(root); } pdd(pdd && other) noexcept : root(0), m(other.m) { std::swap(root, other.root); } pdd& operator=(pdd const& other); + pdd& operator=(unsigned k); + pdd& operator=(rational const& k); ~pdd() { m.dec_ref(root); } pdd lo() const { return pdd(m.lo(root), m); } pdd hi() const { return pdd(m.hi(root), m); } unsigned index() const { return root; } unsigned var() const { return m.var(root); } rational const& val() const { SASSERT(is_val()); return m.val(root); } + rational const& leading_coefficient() 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_unilinear() const { return !is_val() && lo().is_val() && hi().is_val(); } 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_non_zero() const { return m.is_non_zero(root); } + bool is_univariate() const { return m.is_univariate(root); } + 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); } bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); } pdd operator-() const { return m.minus(*this); } @@ -359,20 +435,28 @@ namespace dd { pdd operator*(rational const& other) const { return m.mul(other, *this); } pdd operator+(rational const& other) const { return m.add(other, *this); } pdd operator~() const { return m.mk_not(*this); } + pdd shl(unsigned n) const; pdd rev_sub(rational const& r) const { return m.sub(m.mk_val(r), *this); } + pdd div(rational const& other) const { return m.div(*this, other); } + bool try_div(rational const& other, pdd& out_result) const { return m.try_div(*this, other, out_result); } + pdd pow(unsigned j) const { return m.pow(*this, j); } pdd reduce(pdd const& other) const { return m.reduce(*this, other); } bool different_leading_term(pdd const& other) const { return m.different_leading_term(*this, other); } - void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) { m.factor(*this, v, degree, lc, rest); } + void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) const { m.factor(*this, v, degree, lc, rest); } + bool factor(unsigned v, unsigned degree, pdd& lc) const { return m.factor(*this, v, degree, lc); } + bool resolve(unsigned v, pdd const& other, pdd& result) { return m.resolve(v, *this, other, result); } + pdd reduce(unsigned v, pdd const& other) const { return m.reduce(v, *this, other); } /** * \brief factor out variables */ std::pair var_factors() const; - pdd subst_val(vector> const& s) const { return m.subst_val(*this, s); } + 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); } - /** * \brief substitute variable v by r. */ @@ -381,6 +465,7 @@ namespace dd { std::ostream& display(std::ostream& out) const { return m.display(out, *this); } bool operator==(pdd const& other) const { return root == other.root; } bool operator!=(pdd const& other) const { return root != other.root; } + unsigned hash() const { return root; } unsigned power_of_2() const { return m.power_of_2(); } @@ -388,11 +473,15 @@ namespace dd { double tree_size() const { return m.tree_size(*this); } unsigned degree() const { return m.degree(*this); } unsigned degree(unsigned v) const { return m.degree(root, v); } + unsigned max_pow2_divisor() const { return m.max_pow2_divisor(root); } unsigned_vector const& free_vars() const { return m.free_vars(*this); } + void swap(pdd& other) { std::swap(root, other.root); } pdd_iterator begin() const; pdd_iterator end() const; + + pdd_manager& manager() const { return m; } }; inline pdd operator*(rational const& r, pdd const& b) { return b * r; } @@ -403,23 +492,25 @@ namespace dd { inline pdd operator+(int x, pdd const& b) { return b + rational(x); } inline pdd operator+(pdd const& b, int x) { return b + rational(x); } - inline pdd operator^(unsigned x, pdd const& b) { return b + x; } - inline pdd operator^(bool x, pdd const& b) { return b + x; } + inline pdd operator^(unsigned x, pdd const& b) { return b ^ x; } + inline pdd operator^(bool x, pdd const& b) { return b ^ x; } inline pdd operator-(rational const& r, pdd const& b) { return b.rev_sub(r); } inline pdd operator-(int x, pdd const& b) { return rational(x) - b; } inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); } inline pdd operator-(pdd const& b, rational const& r) { return b + (-r); } - + inline pdd& operator&=(pdd & p, pdd const& q) { p = p & q; return p; } inline pdd& operator^=(pdd & p, pdd const& q) { p = p ^ q; return p; } - inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; } inline pdd& operator|=(pdd & p, pdd const& q) { p = p | q; return p; } + inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; } inline pdd& operator-=(pdd & p, pdd const& q) { p = p - q; return p; } inline pdd& operator+=(pdd & p, pdd const& q) { p = p + q; return p; } - inline pdd& operator+=(pdd & p, rational const& v) { p = p + v; return p; } - inline pdd& operator-=(pdd & p, rational const& v) { p = p - v; return p; } - inline pdd& operator*=(pdd & p, rational const& v) { p = p * v; return p; } + inline pdd& operator*=(pdd & p, rational const& q) { p = p * q; return p; } + inline pdd& operator-=(pdd & p, rational const& q) { p = p - q; return p; } + inline pdd& operator+=(pdd & p, rational const& q) { p = p + q; return p; } + + inline void swap(pdd& p, pdd& q) { p.swap(q); } std::ostream& operator<<(std::ostream& out, pdd const& b); diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp index 9139e499f..a0946d81d 100644 --- a/src/test/pdd.cpp +++ b/src/test/pdd.cpp @@ -4,7 +4,7 @@ namespace dd { class test { -public : +public: static void hello_world() { pdd_manager m(3); @@ -310,17 +310,288 @@ public : sub1.push_back(std::make_pair(va, rational(1))); sub2.push_back(std::make_pair(va, rational(2))); sub3.push_back(std::make_pair(va, rational(3))); - std::cout << "sub 0 " << p.subst_val(sub0) << "\n"; - std::cout << "sub 1 " << p.subst_val(sub1) << "\n"; - std::cout << "sub 2 " << p.subst_val(sub2) << "\n"; - std::cout << "sub 3 " << p.subst_val(sub3) << "\n"; + std::cout << "sub 0 " << p.subst_val0(sub0) << "\n"; + std::cout << "sub 1 " << p.subst_val0(sub1) << "\n"; + std::cout << "sub 2 " << p.subst_val0(sub2) << "\n"; + std::cout << "sub 3 " << p.subst_val0(sub3) << "\n"; - std::cout << "expect 1 " << (2*a + 1).is_non_zero() << "\n"; - std::cout << "expect 1 " << (2*a*b + 2*b + 1).is_non_zero() << "\n"; - std::cout << "expect 0 " << (2*a + 2).is_non_zero() << "\n"; - SASSERT((2*a + 1).is_non_zero()); - SASSERT((2*a + 2*b + 1).is_non_zero()); - SASSERT(!(2*a*b + 3*b + 2).is_non_zero()); + std::cout << "expect 1 " << (2*a + 1).is_never_zero() << "\n"; + std::cout << "expect 1 " << (2*a*b + 2*b + 1).is_never_zero() << "\n"; + std::cout << "expect 0 " << (2*a + 2).is_never_zero() << "\n"; + VERIFY((2*a + 1).is_never_zero()); + VERIFY((2*a + 2*b + 1).is_never_zero()); + VERIFY(!(2*a*b + 3*b + 2).is_never_zero()); + } + + static void degree_of_variables() { + std::cout << "degree of variables\n"; + pdd_manager m(4, pdd_manager::mod2N_e, 3); + unsigned va = 0; + unsigned vb = 1; + unsigned vc = 2; + pdd a = m.mk_var(va); + pdd b = m.mk_var(vb); + pdd c = m.mk_var(vc); + + VERIFY(a.var() == va); + VERIFY(b.var() == vb); + + VERIFY(a.degree(va) == 1); + VERIFY(a.degree(vb) == 0); + VERIFY(a.degree(vc) == 0); + VERIFY(c.degree(vc) == 1); + VERIFY(c.degree(vb) == 0); + VERIFY(c.degree(va) == 0); + + { + pdd p = a * a * a; + VERIFY(p.degree(va) == 3); + VERIFY(p.degree(vb) == 0); + } + + { + pdd p = b * a; + VERIFY(p.degree(va) == 1); + VERIFY(p.degree(vb) == 1); + VERIFY(p.degree(vc) == 0); + } + + { + pdd p = (a*a*b + b*a*b + b + a*c)*a + b*b*c; + VERIFY(p.degree(va) == 3); + VERIFY(p.degree(vb) == 2); + VERIFY(p.degree(vc) == 1); + } + + { + // check that skipping marked nodes works (1) + pdd p = b*a + c*a*a*a; + VERIFY(p.degree(va) == 3); + } + + { + // check that skipping marked nodes works (2) + pdd p = (b+c)*(a*a*a); + VERIFY(p.degree(va) == 3); + } + + { + // check that skipping marked nodes works (3) + pdd p = a*a*a*b*b*b*c + a*a*a*b*b*b; + VERIFY(p.degree(va) == 3); + } + } + + static void factor() { + std::cout << "factor\n"; + pdd_manager m(4, pdd_manager::mod2N_e, 3); + + unsigned const va = 0; + unsigned const vb = 1; + unsigned const vc = 2; + unsigned const vd = 3; + pdd const a = m.mk_var(va); + pdd const b = m.mk_var(vb); + pdd const c = m.mk_var(vc); + pdd const d = m.mk_var(vd); + + auto test_one = [&m](pdd const& p, unsigned v, unsigned d) { + pdd lc = m.zero(); + pdd rest = m.zero(); + std::cout << "Factoring p = " << p << " by v" << v << "^" << d << "\n"; + p.factor(v, d, lc, rest); + std::cout << " lc = " << lc << "\n"; + std::cout << " rest = " << rest << "\n"; + pdd x = m.mk_var(v); + pdd x_pow_d = m.one(); + for (unsigned i = 0; i < d; ++i) { + x_pow_d *= x; + } + VERIFY( p == lc * x_pow_d + rest ); + VERIFY( d == 0 || rest.degree(v) < d ); + VERIFY( d != 0 || lc.is_zero() ); + }; + + auto test_multiple = [=](pdd const& p) { + for (auto v : {va, vb, vc, vd}) { + for (unsigned d = 0; d <= 5; ++d) { + test_one(p, v, d); + } + } + }; + + test_multiple( b ); + test_multiple( b*b*b ); + test_multiple( b + c ); + test_multiple( a*a*a*a*a + a*a*a*b + a*a*b*b + c ); + test_multiple( c*c*c*c*c + b*b*b*c + 3*b*c*c + a ); + test_multiple( (a + b) * (b + c) * (c + d) * (d + a) ); + } + + static void max_pow2_divisor() { + std::cout << "max_pow2_divisor\n"; + pdd_manager m(4, pdd_manager::mod2N_e, 256); + + unsigned const va = 0; + unsigned const vb = 1; + pdd const a = m.mk_var(va); + pdd const b = m.mk_var(vb); + + VERIFY(m.zero().max_pow2_divisor() == UINT_MAX); + VERIFY(m.one().max_pow2_divisor() == 0); + pdd p = (1 << 20)*a*b + 1024*b*b*b; + std::cout << p << " divided by 2^" << p.max_pow2_divisor() << "\n"; + VERIFY(p.max_pow2_divisor() == 10); + VERIFY(p.div(rational::power_of_two(10)) == 1024*a*b + b*b*b); + VERIFY((p + p).max_pow2_divisor() == 11); + VERIFY((p * p).max_pow2_divisor() == 20); + VERIFY((p + 2*b).max_pow2_divisor() == 1); + VERIFY((p + b*b*b).max_pow2_divisor() == 0); + } + + static void try_div() { + std::cout << "try_div\n"; + pdd_manager m(4, pdd_manager::mod2N_e, 256); + pdd const a = m.mk_var(0); + pdd const b = m.mk_var(1); + + pdd const p = 5*a + 15*a*b; + VERIFY_EQ(p.div(rational(5)), a + 3*a*b); + pdd res = a; + VERIFY(!p.try_div(rational(3), res)); + } + + static void binary_resolve() { + std::cout << "binary resolve\n"; + pdd_manager m(4, pdd_manager::mod2N_e, 4); + + unsigned const va = 0; + unsigned const vb = 1; + unsigned const vc = 2; + pdd const a = m.mk_var(va); + pdd const b = m.mk_var(vb); + pdd const c = m.mk_var(vc); + + pdd r = m.zero(); + + pdd p = a*a*b - a*a; + pdd q = a*b*b - b*b; + VERIFY(m.resolve(va, p, q, r)); + VERIFY(r == a*b*b*b - a*b*b); + VERIFY(!m.resolve(va, q, p, r)); + VERIFY(!m.resolve(vb, p, q, r)); + VERIFY(m.resolve(vb, q, p, r)); + VERIFY(r == a*a*a*b - a*a*b); + VERIFY(!m.resolve(vc, p, q, r)); + + p = 2*a*a*b + 13*a*a; + q = 6*a*b*b*b + 14*b*b*b; + VERIFY(m.resolve(va, p, q, r)); + VERIFY(r == (2*b+13)*2*b*b*b*a); + VERIFY(!m.resolve(va, q, p, r)); + VERIFY(!m.resolve(vb, p, q, r)); + VERIFY(m.resolve(vb, q, p, r)); + VERIFY(r == 9*a*a*a*b*b + 5*a*a*b*b); + + p = a*a*b - a*a + 4*a*c + 2; + q = 3*b*b - b*b*b + 8*b*c; + VERIFY(!m.resolve(va, p, q, r)); + VERIFY(!m.resolve(va, q, p, r)); + VERIFY(!m.resolve(vb, p, q, r)); + VERIFY(m.resolve(vb, q, p, r)); + VERIFY(r == 2*a*a*b*b + 8*a*a*b*c + 4*a*b*b*c + 2*b*b); + VERIFY(m.resolve(vc, p, q, r)); + VERIFY(r == 2*a*a*b*b - 2*a*a*b - 3*a*b*b + a*b*b*b + 4*b); + VERIFY(m.resolve(vc, q, p, r)); + VERIFY(r == -(2*a*a*b*b - 2*a*a*b - 3*a*b*b + a*b*b*b + 4*b)); + } + + static void pow() { + std::cout << "pow\n"; + pdd_manager m(4, pdd_manager::mod2N_e, 5); + + unsigned const va = 0; + unsigned const vb = 1; + pdd const a = m.mk_var(va); + pdd const b = m.mk_var(vb); + + VERIFY(a.pow(0) == m.one()); + VERIFY(a.pow(1) == a); + VERIFY(a.pow(2) == a*a); + VERIFY(a.pow(7) == a*a*a*a*a*a*a); + VERIFY((3*a*b).pow(3) == 27*a*a*a*b*b*b); + } + + static void subst_val() { + std::cout << "subst_val\n"; + pdd_manager m(4, pdd_manager::mod2N_e, 2); + + unsigned const va = 0; + unsigned const vb = 1; + unsigned const vc = 2; + unsigned const vd = 3; + pdd const a = m.mk_var(va); + pdd const b = m.mk_var(vb); + pdd const c = m.mk_var(vc); + pdd const d = m.mk_var(vd); + + { + pdd const p = 2*a + b + 1; + VERIFY(p.subst_val(va, rational(0)) == b + 1); + } + + { + pdd const p = a + 2*b; + VERIFY(p.subst_val(va, rational(0)) == 2*b); + VERIFY(p.subst_val(va, rational(2)) == 2*b + 2); + VERIFY(p.subst_val(vb, rational(0)) == a); + VERIFY(p.subst_val(vb, rational(1)) == a + 2); + VERIFY(p.subst_val(vb, rational(2)) == a); + VERIFY(p.subst_val(vb, rational(3)) == a + 2); + VERIFY(p.subst_val(va, rational(0)).subst_val(vb, rational(3)) == 2*m.one()); + } + + { + pdd const p = a + b + c + d; + vector> sub; + sub.push_back({vb, rational(2)}); + sub.push_back({vc, rational(3)}); + VERIFY(p.subst_val0(sub) == a + d + 1); + } + + { + pdd const p = (a + b) * (b + c) * (c + d); + vector> sub; + sub.push_back({vb, rational(2)}); + sub.push_back({vc, rational(3)}); + VERIFY(p.subst_val0(sub) == (a + 2) * (d + 3)); + sub.push_back({va, rational(3)}); + sub.push_back({vd, rational(2)}); + VERIFY(p.subst_val0(sub) == m.one()); + } + } + + static void univariate() { + std::cout << "univariate\n"; + pdd_manager m(4, pdd_manager::mod2N_e, 4); + + unsigned const va = 0; + unsigned const vb = 1; + pdd const a = m.mk_var(va); + pdd const b = m.mk_var(vb); + + pdd p = a*a*b - a*a; + VERIFY(!p.is_univariate()); + + pdd q = 3*a*a*a + 1*a + 2; + VERIFY(q.is_univariate()); + vector coeff; + q.get_univariate_coefficients(coeff); + VERIFY_EQ(coeff.size(), 4); + VERIFY_EQ(coeff[0], 2); + VERIFY_EQ(coeff[1], 1); + VERIFY_EQ(coeff[2], 0); + VERIFY_EQ(coeff[3], 3); } static void factors() { @@ -393,5 +664,13 @@ void tst_pdd() { dd::test::order(); dd::test::order_lm(); dd::test::mod4_operations(); + dd::test::degree_of_variables(); + dd::test::factor(); + dd::test::max_pow2_divisor(); + dd::test::try_div(); + dd::test::binary_resolve(); + dd::test::pow(); + dd::test::subst_val(); + dd::test::univariate(); dd::test::factors(); } From e8e64d3098b3c22a0d616c512ddc3bef5bc27302 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 14:53:41 +0200 Subject: [PATCH 10/19] dlist::insert_before/after --- src/util/dlist.h | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/util/dlist.h b/src/util/dlist.h index df28217c0..7efe5bb53 100644 --- a/src/util/dlist.h +++ b/src/util/dlist.h @@ -40,6 +40,22 @@ public: remove_from(list, head); return head; } + + void insert_after(T* elem) { + T* next = this->m_next; + elem->m_prev = next->m_prev; + elem->m_next = next; + this->m_next = elem; + next->m_prev = elem; + } + + void insert_before(T* elem) { + T* prev = this->m_prev; + elem->m_next = prev->m_next; + elem->m_prev = prev; + prev->m_next = elem; + this->m_prev = elem; + } static void remove_from(T*& list, T* elem) { if (list->m_next == list) { From 5d858da58a47bf1619f8dd901af6ed1b79d3cac3 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 14:54:26 +0200 Subject: [PATCH 11/19] union_find::reserve --- src/util/uint_set.h | 2 +- src/util/union_find.h | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/util/uint_set.h b/src/util/uint_set.h index 2b7e36360..6e64cc7ae 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -192,7 +192,7 @@ public: m_set(&s), m_index(at_end?s.get_max_elem():0), m_last(s.get_max_elem()) { scan(); SASSERT(invariant()); - } + } unsigned operator*() const { return m_index; } bool operator==(iterator const& it) const { return m_index == it.m_index; } bool operator!=(iterator const& it) const { return m_index != it.m_index; } diff --git a/src/util/union_find.h b/src/util/union_find.h index c82d25857..7e42e1bba 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -93,6 +93,11 @@ public: return r; } + void reserve(unsigned v) { + while (get_num_vars() <= v) + mk_var(); + } + unsigned get_num_vars() const { return m_find.size(); } From 2c2ab0d57a5aed0480dda3e0d98ae4c2590d35ba Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 14:59:12 +0200 Subject: [PATCH 12/19] Additional BV matchers --- src/ast/bv_decl_plugin.h | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 372eedb8e..60efc73a9 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -342,6 +342,14 @@ public: bool is_bv_not(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOT); } bool is_bv_ule(expr const * e) const { return is_app_of(e, get_fid(), OP_ULEQ); } bool is_bv_sle(expr const * e) const { return is_app_of(e, get_fid(), OP_SLEQ); } + bool is_ule(expr const * e) const { return is_app_of(e, get_fid(), OP_ULEQ); } + bool is_sle(expr const * e) const { return is_app_of(e, get_fid(), OP_SLEQ); } + bool is_ult(expr const * e) const { return is_app_of(e, get_fid(), OP_ULT); } + bool is_slt(expr const * e) const { return is_app_of(e, get_fid(), OP_SLT); } + bool is_ugt(expr const * e) const { return is_app_of(e, get_fid(), OP_UGT); } + bool is_sgt(expr const * e) const { return is_app_of(e, get_fid(), OP_SGT); } + bool is_uge(expr const * e) const { return is_app_of(e, get_fid(), OP_UGEQ); } + bool is_sge(expr const * e) const { return is_app_of(e, get_fid(), OP_SGEQ); } bool is_bit2bool(expr const * e) const { return is_app_of(e, get_fid(), OP_BIT2BOOL); } bool is_bv2int(expr const* e) const { return is_app_of(e, get_fid(), OP_BV2INT); } bool is_int2bv(expr const* e) const { return is_app_of(e, get_fid(), OP_INT2BV); } @@ -355,9 +363,19 @@ public: MATCH_UNARY(is_bv_not); MATCH_BINARY(is_bv_add); + MATCH_BINARY(is_bv_sub); MATCH_BINARY(is_bv_mul); MATCH_BINARY(is_bv_sle); MATCH_BINARY(is_bv_ule); + MATCH_BINARY(is_ule); + MATCH_BINARY(is_sle); + MATCH_BINARY(is_ult); + MATCH_BINARY(is_slt); + MATCH_BINARY(is_uge); + MATCH_BINARY(is_sge); + MATCH_BINARY(is_ugt); + MATCH_BINARY(is_sgt); + MATCH_BINARY(is_bv_umul_no_ovfl); MATCH_BINARY(is_bv_ashr); MATCH_BINARY(is_bv_lshr); MATCH_BINARY(is_bv_shl); From 059b795faa3f8a2e9c83f5f3abcc4bdaa5f0aa9e Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 1 Aug 2022 21:04:33 +0700 Subject: [PATCH 13/19] Fix warning about \ref when building website.dox --- doc/website.dox.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/website.dox.in b/doc/website.dox.in index 5249f2ae0..651652ce4 100644 --- a/doc/website.dox.in +++ b/doc/website.dox.in @@ -8,5 +8,5 @@ This website hosts the automatically generated documentation for the Z3 APIs. - - \ref @C_API@ @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@ + @C_API@ @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@ */ From 82d853e5f8c15ec54849cdfe9eac7f3037425c9e Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 1 Aug 2022 22:45:50 +0700 Subject: [PATCH 14/19] Use `= delete` to delete special methods. This provides a better experience than just marking them as private and leaving them as undefined symbols. --- src/ast/pattern/pattern_inference.h | 4 ++-- src/muz/base/dl_costs.h | 6 ++---- src/muz/base/dl_rule_subsumption_index.h | 6 ++---- src/muz/rel/dl_base.h | 21 +++++++++------------ src/muz/rel/dl_mk_simple_joins.cpp | 3 +-- src/muz/transforms/dl_mk_slice.cpp | 4 ++-- src/util/array.h | 4 ++-- src/util/params.h | 3 ++- src/util/scoped_numeral_buffer.h | 3 ++- 9 files changed, 24 insertions(+), 30 deletions(-) diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h index d036ad789..28218ee17 100644 --- a/src/ast/pattern/pattern_inference.h +++ b/src/ast/pattern/pattern_inference.h @@ -48,14 +48,14 @@ class smaller_pattern { void save(expr * p1, expr * p2); bool process(expr * p1, expr * p2); - smaller_pattern & operator=(smaller_pattern const &); - public: smaller_pattern(ast_manager & m): m(m) { } + smaller_pattern & operator=(smaller_pattern const &) = delete; + bool operator()(unsigned num_bindings, expr * p1, expr * p2); }; diff --git a/src/muz/base/dl_costs.h b/src/muz/base/dl_costs.h index 333dac996..ea3efcda9 100644 --- a/src/muz/base/dl_costs.h +++ b/src/muz/base/dl_costs.h @@ -80,10 +80,8 @@ namespace datalog { bool passes_output_thresholds(context & ctx) const; void output_profile(std::ostream & out) const; - private: - //private and undefined copy constructor and operator= to avoid the default ones - accounted_object(const accounted_object &); - accounted_object& operator=(const accounted_object &); + accounted_object(const accounted_object &) = delete; + accounted_object& operator=(const accounted_object &) = delete; }; diff --git a/src/muz/base/dl_rule_subsumption_index.h b/src/muz/base/dl_rule_subsumption_index.h index 02f373377..9c29683b3 100644 --- a/src/muz/base/dl_rule_subsumption_index.h +++ b/src/muz/base/dl_rule_subsumption_index.h @@ -25,10 +25,6 @@ Revision History: namespace datalog { class rule_subsumption_index { - //private and undefined copy constroctor - rule_subsumption_index(rule_subsumption_index const&); - //private and undefined operator= - rule_subsumption_index& operator=(rule_subsumption_index const&); typedef obj_hashtable app_set; @@ -53,6 +49,8 @@ namespace datalog { reset_dealloc_values(m_unconditioned_heads); } + rule_subsumption_index(rule_subsumption_index const&) = delete; + rule_subsumption_index& operator=(rule_subsumption_index const&) = delete; void add(rule * r); bool is_subsumed(rule * r); bool is_subsumed(app * query); diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index f0634f0d5..1a4125ed4 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -180,10 +180,9 @@ namespace datalog { public: base_fn() = default; virtual ~base_fn() {} - private: - //private and undefined copy constructor and operator= to avoid copying - base_fn(const base_fn &); - base_fn& operator=(const base_fn &); + + base_fn(const base_fn &) = delete; + base_fn& operator=(const base_fn &) = delete; }; class join_fn : public base_fn { @@ -1098,6 +1097,9 @@ namespace datalog { iterator_core() : m_ref_cnt(0) {} virtual ~iterator_core() {} + iterator_core(const iterator_core &) = delete; + iterator_core & operator=(const iterator_core &) = delete; + void inc_ref() { m_ref_cnt++; } void dec_ref() { SASSERT(m_ref_cnt>0); @@ -1116,10 +1118,6 @@ namespace datalog { //the equality with the end() iterator return is_finished() && it.is_finished(); } - private: - //private and undefined copy constructor and assignment operator - iterator_core(const iterator_core &); - iterator_core & operator=(const iterator_core &); }; struct row_iterator_core { @@ -1128,6 +1126,9 @@ namespace datalog { row_iterator_core() : m_ref_cnt(0) {} virtual ~row_iterator_core() {} + row_iterator_core(const row_iterator_core &) = delete; + row_iterator_core & operator=(const row_iterator_core &) = delete; + void inc_ref() { m_ref_cnt++; } void dec_ref() { SASSERT(m_ref_cnt>0); @@ -1146,10 +1147,6 @@ namespace datalog { //the equality with the end() iterator return is_finished() && it.is_finished(); } - private: - //private and undefined copy constructor and assignment operator - row_iterator_core(const row_iterator_core &); - row_iterator_core & operator=(const row_iterator_core &); }; public: diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp index 3fa52ae2f..37fd3ef36 100644 --- a/src/muz/rel/dl_mk_simple_joins.cpp +++ b/src/muz/rel/dl_mk_simple_joins.cpp @@ -56,6 +56,7 @@ namespace datalog { pair_info() {} + pair_info & operator=(const pair_info &) = delete; bool can_be_joined() const { return m_consumers > 0; } @@ -110,8 +111,6 @@ namespace datalog { SASSERT(!m_rules.empty() || m_consumers == 0); return m_rules.empty(); } - private: - pair_info & operator=(const pair_info &); //to avoid the implicit one }; typedef std::pair app_pair; typedef pair_hash, obj_ptr_hash > app_pair_hash; diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index 28cbf638e..eda00b64d 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -111,8 +111,6 @@ namespace datalog { rule_unifier m_unifier; - slice_proof_converter(slice_proof_converter const& other); - void init_form2rule() { if (!m_sliceform2rule.empty()) { return; @@ -271,6 +269,8 @@ namespace datalog { m_renaming.insert(orig_rule, unsigned_vector(sz, renaming)); } + slice_proof_converter(slice_proof_converter const& other) = delete; + proof_ref operator()(ast_manager& m, unsigned num_source, proof * const * source) override { SASSERT(num_source == 1); proof_ref result(source[0], m); diff --git a/src/util/array.h b/src/util/array.h index 6c04c10d2..a4c2aa2c7 100644 --- a/src/util/array.h +++ b/src/util/array.h @@ -37,8 +37,6 @@ private: char * raw_ptr() const { return reinterpret_cast(reinterpret_cast(m_data) - 1); } - array & operator=(array const & source); - void set_data(void * mem, unsigned sz) { size_t * _mem = static_cast(mem); *_mem = sz; @@ -115,6 +113,8 @@ public: destroy_elements(); } + array & operator=(array const & source) = delete; + // Free the memory used to store the array. template void finalize(Allocator & a) { diff --git a/src/util/params.h b/src/util/params.h index da05dff90..7ad152a59 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -35,13 +35,14 @@ class params_ref { params * m_params; void init(); void copy_core(params const * p); - params_ref& operator=(params_ref const& p) = delete; void set(params_ref const& p); public: params_ref():m_params(nullptr) {} params_ref(params_ref const & p); ~params_ref(); + params_ref& operator=(params_ref const& p) = delete; + static params_ref const & get_empty() { return g_empty_params_ref; } diff --git a/src/util/scoped_numeral_buffer.h b/src/util/scoped_numeral_buffer.h index 86181f761..81d10ba40 100644 --- a/src/util/scoped_numeral_buffer.h +++ b/src/util/scoped_numeral_buffer.h @@ -24,13 +24,14 @@ template class _scoped_numeral_buffer : public sbuffer { typedef sbuffer super; Manager & m_manager; - _scoped_numeral_buffer(_scoped_numeral_buffer const & v); public: _scoped_numeral_buffer(Manager & m):m_manager(m) {} ~_scoped_numeral_buffer() { reset(); } + _scoped_numeral_buffer(_scoped_numeral_buffer const & v) = delete; + void reset() { unsigned sz = this->size(); for (unsigned i = 0; i < sz; i++) { From 9a99c78ffb7361f968853b5997f4f36ba6d5eaf5 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 1 Aug 2022 23:01:49 +0700 Subject: [PATCH 15/19] Enable thread_local code more broadly. This was only being enabled on Windows, Linux, and FreeBSD. (FreeBSD only had it enabled in the legacy build system, not in cmake.) `thread_local` is part of C++11, so now that we require C++17 or later and more recent compilers, this should work everywhere that threading does, so only disable it within a `SINGLE_THREAD` build. --- CMakeLists.txt | 3 --- scripts/mk_util.py | 2 -- src/util/memory_manager.cpp | 2 +- 3 files changed, 1 insertion(+), 6 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 607a851cf..514eebebb 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -188,9 +188,6 @@ set(CMAKE_CXX_STANDARD_REQUIRED ON) if (CMAKE_SYSTEM_NAME STREQUAL "Linux") message(STATUS "Platform: Linux") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_LINUX_") - if (TARGET_ARCHITECTURE STREQUAL "x86_64") - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL") - endif() elseif (CMAKE_SYSTEM_NAME STREQUAL "Android") message(STATUS "Platform: Android") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_ANDROID_") diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 54242dfe6..781961259 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2640,8 +2640,6 @@ def mk_config(): if is64(): if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'): CXXFLAGS = '%s -fPIC' % CXXFLAGS - if sysname == 'Linux' or sysname == 'FreeBSD': - CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS elif not LINUX_X64: CXXFLAGS = '%s -m32' % CXXFLAGS LDFLAGS = '%s -m32' % LDFLAGS diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 15646f216..67f5b82b3 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -215,7 +215,7 @@ void * memory::allocate(char const* file, int line, char const* obj, size_t s) { } #endif -#if !defined(SINGLE_THREAD) && (defined(_WINDOWS) || defined(_USE_THREAD_LOCAL)) +#if !defined(SINGLE_THREAD) // ================================== // ================================== // THREAD LOCAL VERSION From fb1d0bc8991266235d88981ddcaaf5e97a35b35b Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Aug 2022 08:30:44 +0700 Subject: [PATCH 16/19] cmake: Remove ExternalProject BUILD_ALWAYS workaround. This was only needed for cmake < 3.1, but we require later than that. --- examples/CMakeLists.txt | 17 +++++------------ 1 file changed, 5 insertions(+), 12 deletions(-) diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index dcc21f255..07a53f8f0 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -1,11 +1,4 @@ include(ExternalProject) -# Unfortunately `BUILD_ALWAYS` only seems to be supported with the version of ExternalProject -# that shipped with CMake >= 3.1. -if (("${CMAKE_VERSION}" VERSION_EQUAL "3.1") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.1")) - set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 1) -else() - set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "") -endif() option(Z3_C_EXAMPLES_FORCE_CXX_LINKER "Force C++ linker when building C example projects" OFF) @@ -43,7 +36,7 @@ ExternalProject_Add(c_example "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}" "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step - ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BUILD_ALWAYS ON BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir" # Install Step INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command @@ -62,7 +55,7 @@ ExternalProject_Add(c_maxsat_example "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}" "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step - ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BUILD_ALWAYS ON BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_maxsat_example_build_dir" # Install Step INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command @@ -81,7 +74,7 @@ ExternalProject_Add(cpp_example "-DZ3_DIR=${PROJECT_BINARY_DIR}" "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step - ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BUILD_ALWAYS ON BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/cpp_example_build_dir" # Install Step INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command @@ -99,7 +92,7 @@ ExternalProject_Add(z3_tptp5 "-DZ3_DIR=${PROJECT_BINARY_DIR}" "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step - ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BUILD_ALWAYS ON BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/tptp_build_dir" # Install Step INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command @@ -117,7 +110,7 @@ ExternalProject_Add(userPropagator "-DZ3_DIR=${PROJECT_BINARY_DIR}" "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step - ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BUILD_ALWAYS ON BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/userPropagator_build_dir" # Install Step INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command From 053c3ec9e86e579938b6b94badd56211feb50c5c Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 1 Aug 2022 22:29:26 +0000 Subject: [PATCH 17/19] Bump docker/build-push-action from 3.0.0 to 3.1.0 Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 3.0.0 to 3.1.0. - [Release notes](https://github.com/docker/build-push-action/releases) - [Commits](https://github.com/docker/build-push-action/compare/v3.0.0...v3.1.0) --- updated-dependencies: - dependency-name: docker/build-push-action dependency-type: direct:production update-type: version-update:semver-minor ... Signed-off-by: dependabot[bot] --- .github/workflows/docker-image.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml index e7ca0f1b5..04d13b1e8 100644 --- a/.github/workflows/docker-image.yml +++ b/.github/workflows/docker-image.yml @@ -41,7 +41,7 @@ jobs: type=edge type=sha,prefix=ubuntu-20.04-bare-z3-sha- - name: Build and push Bare Z3 Docker Image - uses: docker/build-push-action@v3.0.0 + uses: docker/build-push-action@v3.1.0 with: context: . push: true From 886c3abec1dad877c0cfada633c9eff1bc0853ce Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Aug 2022 08:43:59 +0700 Subject: [PATCH 18/19] Remove remnants of _MP_MSBIGNUM checks. --- src/util/mpz.h | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/util/mpz.h b/src/util/mpz.h index 1a7b6f55e..a1bb19395 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -44,7 +44,7 @@ typedef unsigned digit_t; template class mpz_manager; template class mpq_manager; -#if !defined(_MP_GMP) && !defined(_MP_MSBIGNUM) && !defined(_MP_INTERNAL) +#if !defined(_MP_GMP) && !defined(_MP_INTERNAL) #ifdef _WINDOWS #define _MP_INTERNAL #else @@ -52,13 +52,8 @@ template class mpq_manager; #endif #endif -#if defined(_MP_MSBIGNUM) -typedef size_t digit_t; -#elif defined(_MP_INTERNAL) -typedef unsigned int digit_t; -#endif - #ifndef _MP_GMP +typedef unsigned int digit_t; class mpz_cell { unsigned m_size; unsigned m_capacity; From b3612264a92d093e37fa925ad1375157c0d6bb31 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Aug 2022 00:58:02 +0700 Subject: [PATCH 19/19] Use cmake properties for symbol visibility and PIC. --- CMakeLists.txt | 22 ---------------------- cmake/z3_add_component.cmake | 6 ++++++ 2 files changed, 6 insertions(+), 22 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 514eebebb..e3fb1860b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -345,14 +345,6 @@ endif() option(Z3_BUILD_LIBZ3_SHARED "Build libz3 as a shared library if true, otherwise build a static library" ON) -################################################################################ -# Symbol visibility -################################################################################ -if (NOT MSVC) - z3_add_cxx_flag("-fvisibility=hidden" REQUIRED) - z3_add_cxx_flag("-fvisibility-inlines-hidden" REQUIRED) -endif() - ################################################################################ # Tracing ################################################################################ @@ -364,20 +356,6 @@ else() list(APPEND Z3_COMPONENT_CXX_DEFINES $<$:_TRACE>) endif() -################################################################################ -# Position independent code -################################################################################ -# This is required because code built in the components will end up in a shared -# library. - -# Avoid adding -fPIC compiler switch if we compile with MSVC (which does not -# support the flag) or if we target Windows, which generally does not use -# position independent code for native code shared libraries (DLLs). -if (NOT (MSVC OR MINGW OR WIN32)) - z3_add_cxx_flag("-fPIC" REQUIRED) -endif() - - ################################################################################ # Link time optimization ################################################################################ diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake index c4b2dfbfe..47ecb04aa 100644 --- a/cmake/z3_add_component.cmake +++ b/cmake/z3_add_component.cmake @@ -206,6 +206,12 @@ macro(z3_add_component component_name) foreach (flag ${Z3_COMPONENT_CXX_FLAGS}) target_compile_options(${component_name} PRIVATE ${flag}) endforeach() + set_target_properties(${component_name} PROPERTIES + # Position independent code needed in shared libraries + POSITION_INDEPENDENT_CODE ON + # Symbol visibility + CXX_VISIBILITY_PRESET hidden + VISIBILITY_INLINES_HIDDEN ON) # It's unfortunate that we have to manage dependencies ourselves. #