From 7b91195770479fd4d9e85ffa3d4fc702ad26e3e0 Mon Sep 17 00:00:00 2001 From: Angus Lepper Date: Tue, 20 Feb 2018 19:37:17 +0000 Subject: [PATCH 1/5] Fix Python FiniteDomainSortRef.size() --- src/api/python/z3/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 641dba59c..c8ad4e0b4 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6818,8 +6818,8 @@ class FiniteDomainSortRef(SortRef): def size(self): """Return the size of the finite domain sort""" - r = (ctype.c_ulonglong * 1)() - if Z3_get_finite_domain_sort_size(self.ctx_ref(), self.ast(), r): + r = (ctypes.c_ulonglong * 1)() + if Z3_get_finite_domain_sort_size(self.ctx_ref(), self.ast, r): return r[0] else: raise Z3Exception("Failed to retrieve finite domain sort size") From dbe5df85c303a5b04e1922890d404f79b048e7fd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 22 Feb 2018 08:44:50 -0800 Subject: [PATCH 2/5] fix the override warning Signed-off-by: Lev Nachmanson --- src/util/lp/dense_matrix.h | 6 +++--- src/util/lp/eta_matrix.h | 2 +- src/util/lp/lu.h | 6 +++--- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/util/lp/dense_matrix.h b/src/util/lp/dense_matrix.h index 31b6617ac..e6663d705 100644 --- a/src/util/lp/dense_matrix.h +++ b/src/util/lp/dense_matrix.h @@ -82,10 +82,10 @@ public: void set_number_of_rows(unsigned /*m*/) override {} void set_number_of_columns(unsigned /*n*/) override {} - T get_elem(unsigned i, unsigned j) const { return m_values[i * m_n + j]; } + T get_elem(unsigned i, unsigned j) const override { return m_values[i * m_n + j]; } - unsigned row_count() const { return m_m; } - unsigned column_count() const { return m_n; } + unsigned row_count() const override { return m_m; } + unsigned column_count() const override { return m_n; } void set_elem(unsigned i, unsigned j, const T& val) { m_values[i * m_n + j] = val; } diff --git a/src/util/lp/eta_matrix.h b/src/util/lp/eta_matrix.h index eee4a2674..89d2e641d 100644 --- a/src/util/lp/eta_matrix.h +++ b/src/util/lp/eta_matrix.h @@ -83,7 +83,7 @@ public: void apply_from_right(vector & w) override; void apply_from_right(indexed_vector & w) override; - T get_elem(unsigned i, unsigned j) const; + T get_elem(unsigned i, unsigned j) const override; #ifdef Z3DEBUG unsigned row_count() const override { return m_length; } unsigned column_count() const override { return m_length; } diff --git a/src/util/lp/lu.h b/src/util/lp/lu.h index 2f9a5ec38..f2cae7961 100644 --- a/src/util/lp/lu.h +++ b/src/util/lp/lu.h @@ -78,10 +78,10 @@ public: void set_number_of_columns(unsigned n) override { m_m = n; m_n = n; } T m_one_over_val; - T get_elem (unsigned i, unsigned j) const; + T get_elem (unsigned i, unsigned j) const override; - unsigned row_count() const { return m_m; } // not defined } - unsigned column_count() const { return m_m; } // not defined } + unsigned row_count() const override { return m_m; } // not defined } + unsigned column_count() const override { return m_m; } // not defined } #endif void apply_from_left(vector & w, lp_settings &) override { w[m_i] /= m_val; From a238a0a37da800238b6ade73a2b5f5994109529a Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 22 Feb 2018 17:07:21 -0800 Subject: [PATCH 3/5] fix the build Signed-off-by: Lev Nachmanson --- src/util/lp/dense_matrix.h | 3 ++- src/util/lp/eta_matrix.h | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/util/lp/dense_matrix.h b/src/util/lp/dense_matrix.h index e6663d705..e2ee54058 100644 --- a/src/util/lp/dense_matrix.h +++ b/src/util/lp/dense_matrix.h @@ -81,8 +81,9 @@ public: void set_number_of_rows(unsigned /*m*/) override {} void set_number_of_columns(unsigned /*n*/) override {} - +#ifdef Z3DEBUG T get_elem(unsigned i, unsigned j) const override { return m_values[i * m_n + j]; } +#endif unsigned row_count() const override { return m_m; } unsigned column_count() const override { return m_n; } diff --git a/src/util/lp/eta_matrix.h b/src/util/lp/eta_matrix.h index 89d2e641d..abed6d06b 100644 --- a/src/util/lp/eta_matrix.h +++ b/src/util/lp/eta_matrix.h @@ -83,8 +83,8 @@ public: void apply_from_right(vector & w) override; void apply_from_right(indexed_vector & w) override; - T get_elem(unsigned i, unsigned j) const override; #ifdef Z3DEBUG + T get_elem(unsigned i, unsigned j) const override; unsigned row_count() const override { return m_length; } unsigned column_count() const override { return m_length; } void set_number_of_rows(unsigned m) override { m_length = m; } From c5336f8003dbc23e94156fe4641e1bd9da442cb2 Mon Sep 17 00:00:00 2001 From: Mikhail Ramalho Date: Fri, 23 Feb 2018 14:48:20 +0000 Subject: [PATCH 4/5] Convert BVULT(X,Y) into !BVULE(Y,X) Signed-off-by: Mikhail Ramalho --- src/ast/fpa/fpa2bv_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 033d62825..c84af84d6 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -25,7 +25,7 @@ Notes: #include "ast/fpa/fpa2bv_converter.h" #include "ast/rewriter/fpa_rewriter.h" -#define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); } +#define BVULT(X,Y,R) { expr_ref t(m); t = m_bv_util.mk_ule(Y,X); m_simp.mk_not(t, R); } fpa2bv_converter::fpa2bv_converter(ast_manager & m) : m(m), From 5d0e33c9ad395fa5f0c4e43ed898b6a56f684ad3 Mon Sep 17 00:00:00 2001 From: Moritz Kiefer Date: Fri, 23 Feb 2018 20:22:07 +0100 Subject: [PATCH 5/5] Fix assignment of family ids --- src/ast/ast.cpp | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index b524cd8d4..c27651fca 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1532,6 +1532,17 @@ void ast_manager::copy_families_plugins(ast_manager const & from) { tout << "fid: " << fid << " fidname: " << get_family_name(fid) << "\n"; }); ast_translation trans(const_cast(from), *this, false); + // Inheriting plugins can create new family ids. Since new family ids are + // assigned in the order that they are created, this can result in differing + // family ids. To avoid this, we first assign all family ids and only then inherit plugins. + for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) { + symbol fid_name = from.get_family_name(fid); + if (!m_family_manager.has_family(fid)) { + family_id new_fid = mk_family_id(fid_name); + (void)new_fid; + TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";); + } + } for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) { SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid)); SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid)); @@ -1539,11 +1550,6 @@ void ast_manager::copy_families_plugins(ast_manager const & from) { TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid << ", target has_family: " << m_family_manager.has_family(fid) << "\n"; if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";); - if (!m_family_manager.has_family(fid)) { - family_id new_fid = mk_family_id(fid_name); - (void)new_fid; - TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";); - } TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";); SASSERT(fid == get_family_id(fid_name)); if (from.has_plugin(fid) && !has_plugin(fid)) {