From f645ef7677cb126ca16400c65c0a60c93a1abdc5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 18:08:42 -0700 Subject: [PATCH 01/21] fix #4461 Signed-off-by: Nikolaj Bjorner --- src/tactic/core/reduce_invertible_tactic.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index ea427145d..80b561d08 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -196,7 +196,6 @@ private: case OP_BSHL: case OP_BASHR: case OP_BLSHR: - case OP_BOR: model = rational::zero(); return true; From d3e20d41b2479c7ab3d5db3543aea8f1dcb3cba2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 18:31:28 -0700 Subject: [PATCH 02/21] fix $4457 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 1 + src/smt/old_interval.cpp | 1 + src/smt/theory_arith_nl.h | 1 + 3 files changed, 3 insertions(+) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 641c01285..8bd125dd7 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -218,6 +218,7 @@ unsigned decl_info::hash() const { bool decl_info::operator==(decl_info const & info) const { return m_family_id == info.m_family_id && m_kind == info.m_kind && + m_parameters.size() == info.m_parameters.size() && compare_arrays(m_parameters.begin(), info.m_parameters.begin(), m_parameters.size()); } diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp index 48fd7d69a..a7b2dfd53 100644 --- a/src/smt/old_interval.cpp +++ b/src/smt/old_interval.cpp @@ -235,6 +235,7 @@ interval::interval(interval const & other): m_upper_open(other.m_upper_open), m_lower_dep(other.m_lower_dep), m_upper_dep(other.m_upper_dep) { + std::cout << "copy " << m_lower << " " << m_upper << "\n"; } interval & interval::operator=(interval const & other) { diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index d75ab0f13..79e317e44 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -1995,6 +1995,7 @@ bool theory_arith::is_inconsistent2(grobner::equation const * eq, grobner & grobner::monomial const * m = eq->get_monomial(i); intervals.push_back(mk_interval_for(m)); } + std::cout << intervals.size() << "\n"; sbuffer deleted; deleted.resize(num, false); ptr_buffer monomials; From 3f2dafe047001303a2c316454239793bf96e495e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 18:32:01 -0700 Subject: [PATCH 03/21] fix $4457 Signed-off-by: Nikolaj Bjorner --- src/smt/old_interval.cpp | 1 - src/smt/theory_arith_nl.h | 1 - 2 files changed, 2 deletions(-) diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp index a7b2dfd53..48fd7d69a 100644 --- a/src/smt/old_interval.cpp +++ b/src/smt/old_interval.cpp @@ -235,7 +235,6 @@ interval::interval(interval const & other): m_upper_open(other.m_upper_open), m_lower_dep(other.m_lower_dep), m_upper_dep(other.m_upper_dep) { - std::cout << "copy " << m_lower << " " << m_upper << "\n"; } interval & interval::operator=(interval const & other) { diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 79e317e44..d75ab0f13 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -1995,7 +1995,6 @@ bool theory_arith::is_inconsistent2(grobner::equation const * eq, grobner & grobner::monomial const * m = eq->get_monomial(i); intervals.push_back(mk_interval_for(m)); } - std::cout << intervals.size() << "\n"; sbuffer deleted; deleted.resize(num, false); ptr_buffer monomials; From df75792e9c43ebd456b5ccca1a44da35a3456c27 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 18:35:38 -0700 Subject: [PATCH 04/21] fix #4454 Signed-off-by: Nikolaj Bjorner --- src/api/java/Context.java | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index ef1f6bb07..3de37129e 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2048,6 +2048,16 @@ public class Context implements AutoCloseable { return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject())); } + /** + * Retrieve element at index. + */ + public SeqExpr MkNth(SeqExpr s, Expr index) + { + checkContextMatch(s, index); + return (SeqExpr) Expr.create(this, Native.Z3_mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); + } + + /** * Extract subsequence. */ From 04829e6b7a75199f33d0c832f9543b6c11b07dc1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 18:41:26 -0700 Subject: [PATCH 05/21] fix #4437, not really interesting bug as debug assertion is really for non-interrupted flow Signed-off-by: Nikolaj Bjorner --- src/api/java/Context.java | 2 +- src/qe/qsat.cpp | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 3de37129e..31c9771b1 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2054,7 +2054,7 @@ public class Context implements AutoCloseable { public SeqExpr MkNth(SeqExpr s, Expr index) { checkContextMatch(s, index); - return (SeqExpr) Expr.create(this, Native.Z3_mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 248344c21..8f78a9106 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -166,7 +166,9 @@ namespace qe { expr_ref val(m); for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) { app* p = m_preds[level - 1][j].get(); - eval(p, val); + eval(p, val); + if (!m.inc()) + return; if (m.is_false(val)) { m_asms.push_back(m.mk_not(p)); } @@ -179,6 +181,8 @@ namespace qe { for (unsigned i = level + 1; i < m_preds.size(); i += 2) { for (unsigned j = 0; j < m_preds[i].size(); ++j) { + if (!m.inc()) + return; app* p = m_preds[i][j].get(); max_level lvl = m_elevel.find(p); bool use = From 3d98bccc33da27b977a6d152185b218c4c427ba2 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 3 Jun 2020 10:26:00 +0100 Subject: [PATCH 06/21] fix mem leak in buffer and remove copies in interval (#4458) --- src/smt/old_interval.cpp | 10 ---------- src/smt/old_interval.h | 9 +++------ src/util/buffer.h | 3 +++ 3 files changed, 6 insertions(+), 16 deletions(-) diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp index 48fd7d69a..c0e52c17b 100644 --- a/src/smt/old_interval.cpp +++ b/src/smt/old_interval.cpp @@ -227,16 +227,6 @@ interval::interval(v_dependency_manager & m, rational const & val, bool open, bo } } -interval::interval(interval const & other): - m_manager(other.m_manager), - m_lower(other.m_lower), - m_upper(other.m_upper), - m_lower_open(other.m_lower_open), - m_upper_open(other.m_upper_open), - m_lower_dep(other.m_lower_dep), - m_upper_dep(other.m_upper_dep) { -} - interval & interval::operator=(interval const & other) { m_lower = other.m_lower; m_upper = other.m_upper; diff --git a/src/smt/old_interval.h b/src/smt/old_interval.h index a666908e4..8919d9ca0 100644 --- a/src/smt/old_interval.h +++ b/src/smt/old_interval.h @@ -27,14 +27,12 @@ public: enum kind { MINUS_INFINITY, FINITE, PLUS_INFINITY }; private: kind m_kind; - rational m_value; - explicit ext_numeral(kind k):m_kind(k) {} + rational m_value; public: ext_numeral():m_kind(FINITE) {} /* zero */ explicit ext_numeral(bool plus_infinity):m_kind(plus_infinity ? PLUS_INFINITY : MINUS_INFINITY) {} explicit ext_numeral(rational const & val):m_kind(FINITE), m_value(val) {} explicit ext_numeral(int i):m_kind(FINITE), m_value(i) {} - ext_numeral(ext_numeral const & other):m_kind(other.m_kind), m_value(other.m_value) {} bool is_infinite() const { return m_kind != FINITE; } bool sign() const { return m_kind == MINUS_INFINITY || (m_kind == FINITE && m_value.is_neg()); } void neg(); @@ -78,13 +76,12 @@ class old_interval { v_dependency * join_opt(v_dependency * d1, v_dependency * d2, v_dependency * opt1, v_dependency * opt2); public: - explicit old_interval(v_dependency_manager & m); + explicit old_interval(v_dependency_manager & m); explicit old_interval(v_dependency_manager & m, rational const & lower, bool l_open, v_dependency * l_dep, rational const & upper, bool u_open, v_dependency * u_dep); explicit old_interval(v_dependency_manager & m, rational const & val, v_dependency * l_dep = nullptr, v_dependency * u_dep = nullptr); explicit old_interval(v_dependency_manager & m, rational const & val, bool open, bool lower, v_dependency * d); explicit old_interval(v_dependency_manager & m, ext_numeral const& lower, bool l_open, v_dependency * l_dep, ext_numeral const & upper, bool u_open, v_dependency * u_dep); - old_interval(old_interval const & other); - + bool minus_infinity() const { return m_lower.is_infinite(); } bool plus_infinity() const { return m_upper.is_infinite(); } bool is_lower_open() const { return m_lower_open; } diff --git a/src/util/buffer.h b/src/util/buffer.h index aec826a55..57150a124 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -43,6 +43,9 @@ protected: T * new_buffer = reinterpret_cast(memory::allocate(sizeof(T) * new_capacity)); for (unsigned i = 0; i < m_pos; ++i) { new (&new_buffer[i]) T(std::move(m_buffer[i])); + if (CallDestructors) { + m_buffer[i].~T(); + } } free_memory(); m_buffer = new_buffer; From 98b5abb1d4e880fcab68f56b01c15d8e70c64d28 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 3 Jun 2020 11:57:49 +0100 Subject: [PATCH 07/21] buffer: require a move constructor to avoid copies remove unneded copy constructors from several classes --- src/ast/ast.h | 2 +- src/math/grobner/pdd_solver.h | 1 + src/math/hilbert/hilbert_basis.h | 7 ++----- src/math/lp/lp_settings.h | 1 + src/math/simplex/sparse_matrix.h | 7 ++----- src/math/subpaving/subpaving_types.h | 8 ++------ src/smt/old_interval.cpp | 12 ++++++++++++ src/smt/old_interval.h | 13 ++++--------- src/util/buffer.h | 3 ++- src/util/checked_int64.h | 6 +----- src/util/hwf.h | 8 +++----- src/util/mpf.cpp | 1 + src/util/mpfx.cpp | 1 + src/util/mpz.cpp | 1 + src/util/mpz.h | 8 ++------ src/util/rational.h | 9 ++------- 16 files changed, 38 insertions(+), 50 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 0410a4edd..611c07eec 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -130,7 +130,7 @@ public: explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} parameter(parameter const&); - parameter(parameter && other) : m_kind(other.m_kind) { + parameter(parameter && other) noexcept : m_kind(other.m_kind) { switch (other.m_kind) { case PARAM_INT: m_int = other.get_int(); break; case PARAM_AST: m_ast = other.get_ast(); break; diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h index b8fc04b0a..cceb34b0b 100644 --- a/src/math/grobner/pdd_solver.h +++ b/src/math/grobner/pdd_solver.h @@ -25,6 +25,7 @@ #include "util/rlimit.h" #include "util/statistics.h" #include "math/dd/dd_pdd.h" +#include namespace dd { diff --git a/src/math/hilbert/hilbert_basis.h b/src/math/hilbert/hilbert_basis.h index cb4dd146e..46563195c 100644 --- a/src/math/hilbert/hilbert_basis.h +++ b/src/math/hilbert/hilbert_basis.h @@ -25,14 +25,14 @@ Revision History: --*/ -#ifndef HILBERT_BASIS_H_ -#define HILBERT_BASIS_H_ +#pragma once #include "util/rational.h" #include "util/lbool.h" #include "util/statistics.h" #include "util/checked_int64.h" #include "util/rlimit.h" +#include typedef vector rational_vector; @@ -198,6 +198,3 @@ public: void reset_statistics(); }; - - -#endif diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index a7d7e9b86..0cd0305fc 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -24,6 +24,7 @@ Revision History: #include #include #include +#include #include "math/lp/lp_utils.h" #include "util/stopwatch.h" #include "math/lp/lp_types.h" diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index 96b2dd03c..f18bb6f87 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -16,11 +16,11 @@ Notes: --*/ -#ifndef SPARSE_MATRIX_H_ -#define SPARSE_MATRIX_H_ +#pragma once #include "util/mpq_inf.h" #include "util/statistics.h" +#include namespace simplex { @@ -271,6 +271,3 @@ namespace simplex { }; }; - - -#endif diff --git a/src/math/subpaving/subpaving_types.h b/src/math/subpaving/subpaving_types.h index e81b86e09..28150cc04 100644 --- a/src/math/subpaving/subpaving_types.h +++ b/src/math/subpaving/subpaving_types.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef SUBPAVING_TYPES_H_ -#define SUBPAVING_TYPES_H_ +#pragma once namespace subpaving { @@ -34,7 +33,6 @@ class power : public std::pair { public: power():std::pair() {} power(var v, unsigned d):std::pair(v, d) {} - power(power const & p):std::pair(p) {} var x() const { return first; } var get_var() const { return first; } unsigned degree() const { return second; } @@ -47,6 +45,4 @@ struct display_var_proc { virtual void operator()(std::ostream & out, var x) const { out << "x" << x; } }; -}; - -#endif +} diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp index c0e52c17b..a5ea1a14c 100644 --- a/src/smt/old_interval.cpp +++ b/src/smt/old_interval.cpp @@ -228,6 +228,7 @@ interval::interval(v_dependency_manager & m, rational const & val, bool open, bo } interval & interval::operator=(interval const & other) { + SASSERT(&m == &other.m); m_lower = other.m_lower; m_upper = other.m_upper; m_lower_open = other.m_lower_open; @@ -237,6 +238,17 @@ interval & interval::operator=(interval const & other) { return *this; } +interval & interval::operator=(interval && other) { + SASSERT(&m == &other.m); + m_lower = std::move(other.m_lower); + m_upper = std::move(other.m_upper); + m_lower_open = other.m_lower_open; + m_upper_open = other.m_upper_open; + m_lower_dep = other.m_lower_dep; + m_upper_dep = other.m_upper_dep; + return *this; +} + interval & interval::operator+=(interval const & other) { m_lower += other.m_lower; m_upper += other.m_upper; diff --git a/src/smt/old_interval.h b/src/smt/old_interval.h index 8919d9ca0..7a6f41e26 100644 --- a/src/smt/old_interval.h +++ b/src/smt/old_interval.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef OLD_INTERVAL_H_ -#define OLD_INTERVAL_H_ +#pragma once #include "util/rational.h" #include "util/dependency.h" @@ -81,6 +80,8 @@ public: explicit old_interval(v_dependency_manager & m, rational const & val, v_dependency * l_dep = nullptr, v_dependency * u_dep = nullptr); explicit old_interval(v_dependency_manager & m, rational const & val, bool open, bool lower, v_dependency * d); explicit old_interval(v_dependency_manager & m, ext_numeral const& lower, bool l_open, v_dependency * l_dep, ext_numeral const & upper, bool u_open, v_dependency * u_dep); + old_interval(const old_interval&) = default; + old_interval(old_interval&&) = default; bool minus_infinity() const { return m_lower.is_infinite(); } bool plus_infinity() const { return m_upper.is_infinite(); } @@ -91,6 +92,7 @@ public: rational const & get_lower_value() const { SASSERT(!minus_infinity()); return m_lower.to_rational(); } rational const & get_upper_value() const { SASSERT(!plus_infinity()); return m_upper.to_rational(); } old_interval & operator=(old_interval const & other); + old_interval & operator=(old_interval && other); old_interval & operator+=(old_interval const & other); old_interval & operator-=(old_interval const & other); old_interval & operator*=(old_interval const & other); @@ -125,12 +127,5 @@ inline old_interval operator/(old_interval const & i1, old_interval const & i2) inline old_interval expt(old_interval const & i, unsigned n) { old_interval tmp(i); tmp.expt(n); return tmp; } inline std::ostream & operator<<(std::ostream & out, old_interval const & i) { i.display(out); return out; } -struct interval_detail{}; -inline std::pair wd(old_interval const & i) { interval_detail d; return std::make_pair(i, d); } -inline std::ostream & operator<<(std::ostream & out, std::pair const & p) { p.first.display_with_dependencies(out); return out; } - // allow "customers" of this file to keep using interval #define interval old_interval - -#endif /* OLD_INTERVAL_H_ */ - diff --git a/src/util/buffer.h b/src/util/buffer.h index 57150a124..a261788ee 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -21,7 +21,7 @@ Revision History: --*/ #pragma once -#include +#include #include "util/memory_manager.h" template @@ -39,6 +39,7 @@ protected: } void expand() { + static_assert(std::is_nothrow_move_constructible::value); unsigned new_capacity = m_capacity << 1; T * new_buffer = reinterpret_cast(memory::allocate(sizeof(T) * new_capacity)); for (unsigned i = 0; i < m_pos; ++i) { diff --git a/src/util/checked_int64.h b/src/util/checked_int64.h index 507564a2e..06b957fcf 100644 --- a/src/util/checked_int64.h +++ b/src/util/checked_int64.h @@ -21,8 +21,7 @@ Revision History: --*/ -#ifndef CHECKED_INT64_H_ -#define CHECKED_INT64_H_ +#pragma once #include "util/z3_exception.h" #include "util/rational.h" @@ -38,7 +37,6 @@ public: checked_int64(): m_value(0) {} checked_int64(int64_t v): m_value(v) {} - checked_int64(checked_int64 const& other) { m_value = other.m_value; } class overflow_exception : public z3_exception { char const * msg() const override { return "checked_int64 overflow/underflow";} @@ -217,5 +215,3 @@ inline checked_int64 operator*(checked_int64 const& a, checked_int result *= b; return result; } - -#endif diff --git a/src/util/hwf.h b/src/util/hwf.h index 21e7655ea..3230cdb7e 100644 --- a/src/util/hwf.h +++ b/src/util/hwf.h @@ -16,10 +16,10 @@ Author: Revision History: --*/ -#ifndef HWF_H_ -#define HWF_H_ +#pragma once -#include +#include +#include #include "util/mpz.h" #include "util/mpq.h" #include "util/mpf.h" @@ -172,5 +172,3 @@ protected: typedef _scoped_numeral scoped_hwf; typedef _scoped_numeral_vector scoped_hwf_vector; - -#endif diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index cdd8f5f3e..1e93d0d3d 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -16,6 +16,7 @@ Author: Revision History: --*/ +#include #include #include #include "util/mpf.h" diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp index 4769ab24a..8595e0185 100644 --- a/src/util/mpfx.cpp +++ b/src/util/mpfx.cpp @@ -16,6 +16,7 @@ Author: Revision History: --*/ +#include #include #include #include "util/mpfx.h" diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index eb6754654..3a7922e13 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -16,6 +16,7 @@ Author: Revision History: --*/ +#include #include #include #include "util/mpz.h" diff --git a/src/util/mpz.h b/src/util/mpz.h index dee54b1c8..266b9aa34 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef MPZ_H_ -#define MPZ_H_ +#pragma once #include #include "util/mutex.h" @@ -104,7 +103,7 @@ public: mpz(int v):m_val(v), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {} mpz():m_val(0), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {} mpz(mpz_type* ptr): m_val(0), m_kind(mpz_small), m_owner(mpz_ext), m_ptr(ptr) { SASSERT(ptr);} - mpz(mpz && other) : m_val(other.m_val), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) { + mpz(mpz && other) noexcept : m_val(other.m_val), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) { std::swap(m_ptr, other.m_ptr); unsigned o = m_owner; m_owner = other.m_owner; other.m_owner = o; unsigned k = m_kind; m_kind = other.m_kind; other.m_kind = k; @@ -734,6 +733,3 @@ typedef mpz_manager unsynch_mpz_manager; typedef _scoped_numeral scoped_mpz; typedef _scoped_numeral scoped_synch_mpz; typedef _scoped_numeral_vector scoped_mpz_vector; - -#endif /* MPZ_H_ */ - diff --git a/src/util/rational.h b/src/util/rational.h index c7f0358dd..eec5c50ec 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef RATIONAL_H_ -#define RATIONAL_H_ +#pragma once #include "util/mpq.h" @@ -41,7 +40,7 @@ public: rational() {} rational(rational const & r) { m().set(m_val, r.m_val); } - rational(rational && r) : m_val(std::move(r.m_val)) {} + rational(rational && r) noexcept : m_val(std::move(r.m_val)) {} explicit rational(int n) { m().set(m_val, n); } @@ -576,7 +575,3 @@ inline rational gcd(rational const & r1, rational const & r2, rational & a, rati rational::m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val); return result; } - - -#endif /* RATIONAL_H_ */ - From 7ac2791482e173fcb2095356a5dbe2eafd5cc0b0 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 3 Jun 2020 17:09:27 +0100 Subject: [PATCH 08/21] remove a bunch of constructors to avoid copies still not enough to guarantee that vector::expand doesnt copy (WIP) --- src/ast/justified_expr.h | 14 ++++++++++---- src/ast/normal_forms/nnf.cpp | 10 ---------- src/math/automata/automaton.h | 4 ++++ src/sat/sat_model_converter.cpp | 2 +- src/sat/sat_model_converter.h | 19 ++++--------------- src/smt/old_interval.cpp | 4 ++-- src/util/buffer.h | 2 +- src/util/hashtable.h | 20 +++++++++++++++----- src/util/hwf.h | 3 --- src/util/mpf.h | 14 +++----------- src/util/mpq.h | 10 +++------- src/util/mpz.h | 4 ++-- src/util/optional.h | 12 ++++++------ src/util/rational.h | 2 +- src/util/ref_vector.h | 22 ++++++++++------------ src/util/vector.h | 7 ++++--- 16 files changed, 66 insertions(+), 83 deletions(-) diff --git a/src/ast/justified_expr.h b/src/ast/justified_expr.h index d9a6fc629..2e49051e3 100644 --- a/src/ast/justified_expr.h +++ b/src/ast/justified_expr.h @@ -1,6 +1,5 @@ -#ifndef JUSTIFIED_EXPR_H_ -#define JUSTIFIED_EXPR_H_ +#pragma once #include "ast/ast.h" @@ -40,6 +39,15 @@ public: m.inc_ref(m_proof); } + justified_expr(justified_expr && other): + m(other.m), + m_fml(nullptr), + m_proof(nullptr) + { + std::swap(m_fml, other.m_fml); + std::swap(m_proof, other.m_proof); + } + ~justified_expr() { m.dec_ref(m_fml); m.dec_ref(m_proof); @@ -50,5 +58,3 @@ public: expr* get_fml() const { return m_fml; } proof* get_proof() const { return m_proof; } }; - -#endif diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index db9f5eb66..7bf9de2e0 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -221,16 +221,6 @@ struct nnf::imp { m_cache_result(cache_res), m_spos(spos) { } - frame(frame && other): - m_curr(std::move(other.m_curr)), - m_i(other.m_i), - m_pol(other.m_pol), - m_in_q(other.m_in_q), - m_new_child(other.m_new_child), - m_cache_result(other.m_cache_result), - m_spos(other.m_spos) { - } - }; // There are four caches: diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index 4903b2067..3d42f13a0 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -54,6 +54,10 @@ public: if (m_t) m.inc_ref(m_t); } + move(move &&other) noexcept : m(other.m), m_t(nullptr), m_src(other.m_src), m_dst(other.m_dst) { + std::swap(m_t, other.m_t); + } + move& operator=(move const& other) { SASSERT(&m == &other.m); T* t = other.m_t; diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 0abb38eae..062b6904d 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -208,7 +208,7 @@ namespace sat { } void model_converter::add_elim_stack(entry & e) { - e.m_elim_stack.push_back(stackv().empty() ? nullptr : alloc(elim_stack, stackv())); + e.m_elim_stack.push_back(stackv().empty() ? nullptr : alloc(elim_stack, std::move(m_elim_stack))); // VERIFY(for (auto const& s : stackv()) VERIFY(legal_to_flip(s.second.var()));); stackv().reset(); } diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index 93a078818..e453bcaa1 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef SAT_MODEL_CONVERTER_H_ -#define SAT_MODEL_CONVERTER_H_ +#pragma once #include "sat/sat_types.h" #include "util/ref_vector.h" @@ -51,12 +50,12 @@ namespace sat { unsigned m_counter; unsigned m_refcount; elim_stackv m_stack; - elim_stack(elim_stack const& ); public: - elim_stack(elim_stackv const& stack): + elim_stack(elim_stack const&) = delete; + elim_stack(elim_stackv && stack): m_counter(0), m_refcount(0), - m_stack(stack) { + m_stack(std::move(stack)) { m_counter = ++counter; } ~elim_stack() { } @@ -76,14 +75,6 @@ namespace sat { sref_vector m_elim_stack; entry(kind k, bool_var v): m_var(v), m_kind(k) {} public: - entry(entry const & src): - m_var(src.m_var), - m_kind(src.m_kind), - m_clauses(src.m_clauses), - m_clause(src.m_clause) - { - m_elim_stack.append(src.m_elim_stack); - } bool_var var() const { return m_var; } kind get_kind() const { return m_kind; } }; @@ -166,5 +157,3 @@ namespace sat { } }; - -#endif diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp index a5ea1a14c..efdb78754 100644 --- a/src/smt/old_interval.cpp +++ b/src/smt/old_interval.cpp @@ -228,7 +228,7 @@ interval::interval(v_dependency_manager & m, rational const & val, bool open, bo } interval & interval::operator=(interval const & other) { - SASSERT(&m == &other.m); + SASSERT(&m_manager == &other.m_manager); m_lower = other.m_lower; m_upper = other.m_upper; m_lower_open = other.m_lower_open; @@ -239,7 +239,7 @@ interval & interval::operator=(interval const & other) { } interval & interval::operator=(interval && other) { - SASSERT(&m == &other.m); + SASSERT(&m_manager == &other.m_manager); m_lower = std::move(other.m_lower); m_upper = std::move(other.m_upper); m_lower_open = other.m_lower_open; diff --git a/src/util/buffer.h b/src/util/buffer.h index a261788ee..22cf17ada 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -39,7 +39,7 @@ protected: } void expand() { - static_assert(std::is_nothrow_move_constructible::value); + static_assert(std::is_nothrow_move_constructible::value, ""); unsigned new_capacity = m_capacity << 1; T * new_buffer = reinterpret_cast(memory::allocate(sizeof(T) * new_capacity)); for (unsigned i = 0; i < m_pos; ++i) { diff --git a/src/util/hashtable.h b/src/util/hashtable.h index 55866065e..78abd3c87 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -16,8 +16,8 @@ Author: Revision History: --*/ -#ifndef HASHTABLE_H_ -#define HASHTABLE_H_ +#pragma once + #include "util/debug.h" #include #include "util/util.h" @@ -269,6 +269,19 @@ public: m_st_collision = 0; }); } + + core_hashtable(core_hashtable && source) noexcept : + HashProc(source), + EqProc(source), + m_table(nullptr) { + m_capacity = source.m_capacity; + std::swap(m_table, source.m_table); + m_size = source.m_size; + m_num_deleted = 0; + HS_CODE({ + m_st_collision = 0; + }); + } ~core_hashtable() { delete_table(); @@ -736,6 +749,3 @@ public: EqProc const & e = EqProc()): core_hashtable, HashProc, EqProc>(initial_capacity, h, e) {} }; - - -#endif /* HASHTABLE_H_ */ diff --git a/src/util/hwf.h b/src/util/hwf.h index 3230cdb7e..f2afbee63 100644 --- a/src/util/hwf.h +++ b/src/util/hwf.h @@ -36,9 +36,6 @@ class hwf { } public: - hwf() {} - hwf(hwf const & other) { this->value = other.value; } - ~hwf() {} void swap(hwf & other) { double t = value; value = other.value; other.value = t; } }; diff --git a/src/util/mpf.h b/src/util/mpf.h index 107ada0bd..fb5f2a022 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef MPF_H_ -#define MPF_H_ +#pragma once #include #include "util/mpz.h" @@ -45,18 +44,13 @@ class mpf { unsigned sign:1; // counts as one sbit. mpz significand; mpf_exp_t exponent; - mpf & operator=(mpf const & other) { UNREACHABLE(); return *this; } void set(unsigned _ebits, unsigned _sbits); public: mpf(); mpf(unsigned ebits, unsigned sbits); - mpf(mpf && other) : - ebits(other.ebits), - sbits(other.sbits), - sign(other.sign), - significand(std::move(other.significand)), - exponent(other.exponent) {} + mpf(mpf &&) = default; ~mpf(); + mpf & operator=(mpf const & other) = delete; unsigned get_ebits() const { return ebits; } unsigned get_sbits() const { return sbits; } void swap(mpf & other); @@ -325,5 +319,3 @@ public: }; typedef _scoped_numeral_vector scoped_mpf_vector; - -#endif diff --git a/src/util/mpq.h b/src/util/mpq.h index 4cc15229f..a9e6063a3 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef MPQ_H_ -#define MPQ_H_ +#pragma once #include "util/mpz.h" #include "util/trace.h" @@ -27,11 +26,11 @@ class mpq { mpz m_den; friend class mpq_manager; friend class mpq_manager; - mpq & operator=(mpq const & other) { UNREACHABLE(); return *this; } public: mpq(int v):m_num(v), m_den(1) {} mpq():m_den(1) {} - mpq(mpq && other) : m_num(std::move(other.m_num)), m_den(std::move(other.m_den)) {} + mpq(mpq &&) = default; + mpq & operator=(mpq const &) = delete; void swap(mpq & other) { m_num.swap(other.m_num); m_den.swap(other.m_den); } mpz const & numerator() const { return m_num; } mpz const & denominator() const { return m_den; } @@ -862,6 +861,3 @@ typedef mpq_manager unsynch_mpq_manager; typedef _scoped_numeral scoped_mpq; typedef _scoped_numeral scoped_synch_mpq; typedef _scoped_numeral_vector scoped_mpq_vector; - -#endif /* MPQ_H_ */ - diff --git a/src/util/mpz.h b/src/util/mpz.h index 266b9aa34..248048888 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -105,8 +105,8 @@ public: mpz(mpz_type* ptr): m_val(0), m_kind(mpz_small), m_owner(mpz_ext), m_ptr(ptr) { SASSERT(ptr);} mpz(mpz && other) noexcept : m_val(other.m_val), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) { std::swap(m_ptr, other.m_ptr); - unsigned o = m_owner; m_owner = other.m_owner; other.m_owner = o; - unsigned k = m_kind; m_kind = other.m_kind; other.m_kind = k; + m_owner = other.m_owner; + m_kind = other.m_kind; } void swap(mpz & other) { std::swap(m_val, other.m_val); diff --git a/src/util/optional.h b/src/util/optional.h index d496fd322..b9687df8c 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -18,8 +18,7 @@ Revision History: --*/ -#ifndef OPTIONAL_H_ -#define OPTIONAL_H_ +#pragma once template class optional { @@ -47,6 +46,11 @@ public: construct(val); } + optional(T && val) noexcept : m_obj(nullptr), m_initialized(0) { + std::swap(m_obj, val.m_obj); + std::swap(m_initialized, val.m_initialized); + } + optional(const optional & val): m_initialized(0) { if (val.m_initialized == 1) { @@ -160,7 +164,3 @@ public: T * & operator*() { return m_ptr; } }; - - -#endif /* OPTIONAL_H_ */ - diff --git a/src/util/rational.h b/src/util/rational.h index eec5c50ec..0f2a2a1b7 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -40,7 +40,7 @@ public: rational() {} rational(rational const & r) { m().set(m_val, r.m_val); } - rational(rational && r) noexcept : m_val(std::move(r.m_val)) {} + rational(rational&&) = default; explicit rational(int n) { m().set(m_val, n); } diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index 5b5d9ac34..ce8060cd3 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef REF_VECTOR_H_ -#define REF_VECTOR_H_ +#pragma once #include "util/vector.h" #include "util/obj_ref.h" @@ -49,11 +48,14 @@ protected: public: typedef T * data; - ref_vector_core(Ref const & r = Ref()):Ref(r) {} + ref_vector_core() = default; + ref_vector_core(Ref const & r) : Ref(r) {} - ref_vector_core(ref_vector_core && other) : - Ref(std::move(other)), - m_nodes(std::move(other.m_nodes)) {} + ref_vector_core(const ref_vector_core & other) { + append(other); + } + + ref_vector_core(ref_vector_core &&) = default; ~ref_vector_core() { dec_range_ref(m_nodes.begin(), m_nodes.end()); @@ -400,9 +402,8 @@ public: /** \brief Vector of unmanaged references. */ -template -class sref_vector : public ref_vector_core > { -}; +template +using sref_vector = ref_vector_core>; /** \brief Hash utilities on ref_vector pointers. @@ -440,6 +441,3 @@ struct ref_vector_ptr_eq { return true; } }; - - -#endif /* REF_VECTOR_H_ */ diff --git a/src/util/vector.h b/src/util/vector.h index 9de2b2a86..588be7ae8 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -69,6 +69,7 @@ class vector { m_data = reinterpret_cast(mem); } else { + //static_assert(std::is_nothrow_move_constructible::value, ""); SASSERT(capacity() > 0); SZ old_capacity = reinterpret_cast(m_data)[CAPACITY_IDX]; SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2; @@ -163,7 +164,7 @@ public: SASSERT(size() == source.size()); } - vector(vector&& other) : m_data(nullptr) { + vector(vector&& other) noexcept : m_data(nullptr) { std::swap(m_data, other.m_data); } @@ -587,7 +588,7 @@ public: ptr_vector(unsigned s):vector(s) {} ptr_vector(unsigned s, T * elem):vector(s, elem) {} ptr_vector(ptr_vector const & source):vector(source) {} - ptr_vector(ptr_vector && other) : vector(std::move(other)) {} + ptr_vector(ptr_vector && other) noexcept : vector(std::move(other)) {} ptr_vector(unsigned s, T * const * data):vector(s, const_cast(data)) {} ptr_vector & operator=(ptr_vector const & source) { vector::operator=(source); @@ -602,7 +603,7 @@ public: svector(SZ s):vector(s) {} svector(SZ s, T const & elem):vector(s, elem) {} svector(svector const & source):vector(source) {} - svector(svector && other) : vector(std::move(other)) {} + svector(svector && other) noexcept : vector(std::move(other)) {} svector(SZ s, T const * data):vector(s, data) {} svector & operator=(svector const & source) { vector::operator=(source); From 0bc33e9c9d4016d4a44db31228fd27a7e63257a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 09:10:44 -0700 Subject: [PATCH 09/21] correct the type returned by mkNth #4454 Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Context.cs | 4 ++-- src/api/java/Context.java | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 3987004ef..0293fc76a 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2488,12 +2488,12 @@ namespace Microsoft.Z3 /// /// Retrieve element at index. /// - public SeqExpr MkNth(SeqExpr s, Expr index) + public Expr MkNth(SeqExpr s, Expr index) { Debug.Assert(s != null); Debug.Assert(index != null); CheckContextMatch(s, index); - return new SeqExpr(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject)); + return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject)); } /// diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 31c9771b1..06fe6061a 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2051,10 +2051,10 @@ public class Context implements AutoCloseable { /** * Retrieve element at index. */ - public SeqExpr MkNth(SeqExpr s, Expr index) + public Expr MkNth(SeqExpr s, Expr index) { checkContextMatch(s, index); - return (SeqExpr) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); + return Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); } From a23ca1792be3bb41a64658fefcf3fa61ff0b7d6b Mon Sep 17 00:00:00 2001 From: "Andrew V. Jones" Date: Wed, 3 Jun 2020 17:35:14 +0100 Subject: [PATCH 10/21] Ensure that Z3 uses the correct SMT-LIB2 syntax for `push` and `pop` (#4495) * When pretty-printing SMTLIB2, ensure that Z3 uses the correct syntax for 'push' Signed-off-by: Andrew V. Jones * When pretty-printing SMTLIB2, ensure that Z3 uses the correct syntax for 'pop' Signed-off-by: Andrew V. Jones --- src/api/api_solver.cpp | 2 +- src/muz/base/dl_context.cpp | 4 ++-- src/muz/spacer/spacer_manager.cpp | 4 ++-- src/muz/spacer/spacer_util.cpp | 4 ++-- src/qe/qe.cpp | 4 ++-- src/test/theory_pb.cpp | 4 ++-- 6 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index de4d3732f..596ba011d 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -61,7 +61,7 @@ extern "C" { } void solver2smt2_pp::push() { - m_out << "(push)\n"; + m_out << "(push 1)\n"; m_pp_util.push(); m_tracked_lim.push_back(m_tracked.size()); } diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index c9252eece..707167e17 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -1231,14 +1231,14 @@ namespace datalog { } else { for (unsigned i = 0; i < queries.size(); ++i) { - if (queries.size() > 1) out << "(push)\n"; + if (queries.size() > 1) out << "(push 1)\n"; out << "(assert "; expr_ref q(m); q = m.mk_not(queries[i].get()); PP(q); out << ")\n"; out << "(check-sat)\n"; - if (queries.size() > 1) out << "(pop)\n"; + if (queries.size() > 1) out << "(pop 1)\n"; } } } diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp index 61fd9447d..f560ef4dd 100644 --- a/src/muz/spacer/spacer_manager.cpp +++ b/src/muz/spacer/spacer_manager.cpp @@ -141,12 +141,12 @@ void inductive_property::display(datalog::rule_manager& rm, ptr_vector Date: Wed, 3 Jun 2020 10:09:18 -0700 Subject: [PATCH 11/21] fix #4434 Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_array_eq_rewrite.cpp | 6 +- .../transforms/dl_mk_array_instantiation.cpp | 516 ++++++++---------- src/muz/transforms/dl_mk_backwards.cpp | 4 +- src/muz/transforms/dl_mk_coalesce.cpp | 8 +- .../dl_mk_interp_tail_simplifier.cpp | 5 +- src/muz/transforms/dl_mk_loop_counter.cpp | 4 +- src/muz/transforms/dl_mk_magic_sets.cpp | 4 +- src/muz/transforms/dl_mk_magic_symbolic.cpp | 4 +- .../dl_mk_quantifier_abstraction.cpp | 5 +- .../dl_mk_quantifier_instantiation.cpp | 5 +- src/muz/transforms/dl_mk_scale.cpp | 4 +- src/muz/transforms/dl_mk_slice.cpp | 5 +- .../transforms/dl_mk_subsumption_checker.cpp | 8 +- 13 files changed, 268 insertions(+), 310 deletions(-) diff --git a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp b/src/muz/transforms/dl_mk_array_eq_rewrite.cpp index c8a3d4357..c37370d14 100644 --- a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp +++ b/src/muz/transforms/dl_mk_array_eq_rewrite.cpp @@ -38,14 +38,14 @@ namespace datalog { rule_set * mk_array_eq_rewrite::operator()(rule_set const & source) { m_src_set = &source; - rule_set * result = alloc(rule_set, m_ctx); + scoped_ptr result = alloc(rule_set, m_ctx); result->inherit_predicates(source); - m_dst = result; + m_dst = result.get(); m_src_manager = &source.get_rule_manager(); for (rule * rp : source) { instantiate_rule(*rp, *result); } - return result; + return result.detach(); } void mk_array_eq_rewrite::instantiate_rule(const rule& r, rule_set & dest) diff --git a/src/muz/transforms/dl_mk_array_instantiation.cpp b/src/muz/transforms/dl_mk_array_instantiation.cpp index a94383453..9c962d774 100644 --- a/src/muz/transforms/dl_mk_array_instantiation.cpp +++ b/src/muz/transforms/dl_mk_array_instantiation.cpp @@ -27,7 +27,7 @@ Revision History: namespace datalog { - mk_array_instantiation::mk_array_instantiation( + mk_array_instantiation::mk_array_instantiation( context & ctx, unsigned priority): plugin(priority), m(ctx.get_manager()), @@ -35,289 +35,253 @@ namespace datalog { m_a(m), eq_classes(m), ownership(m) - { - } - - rule_set * mk_array_instantiation::operator()(rule_set const & source) - { - std::cout<<"Array Instantiation called with parameters :" - <<" enforce="<display(std::cout); - return result; - } - - void mk_array_instantiation::instantiate_rule(const rule& r, rule_set & dest) - { - //Reset everything - selects.reset(); - eq_classes.reset(); - cnt = src_manager->get_counter().get_max_rule_var(r)+1; - done_selects.reset(); - ownership.reset(); - - expr_ref_vector phi(m); - expr_ref_vector preds(m); - expr_ref new_head = create_head(to_app(r.get_head())); - unsigned nb_predicates = r.get_uninterpreted_tail_size(); - unsigned tail_size = r.get_tail_size(); - for(unsigned i=0;i::iterator it = done_selects.begin(); it!=done_selects.end(); ++it) - { - expr_ref tmp(m); - tmp = &it->get_key(); - new_tail.push_back(m.mk_eq(it->get_value(), tmp)); - } - proof_ref pr(m); - src_manager->mk_rule(m.mk_implies(m.mk_and(new_tail.size(), new_tail.c_ptr()), new_head), pr, dest, r.name()); - } - - expr_ref mk_array_instantiation::create_head(app* old_head) - { - expr_ref_vector new_args(m); - for(unsigned i=0;iget_num_args();i++) - { - expr*arg = old_head->get_arg(i); - if(m_a.is_array(get_sort(arg))) - { - for(unsigned k=0; k< m_ctx.get_params().xform_instantiate_arrays_nb_quantifier();k++) - { - expr_ref_vector dummy_args(m); - dummy_args.push_back(arg); - for(unsigned i=0;i()); - selects[arg].push_back(select); - } - if(!m_ctx.get_params().xform_instantiate_arrays_enforce()) - new_args.push_back(arg); - } - else - new_args.push_back(arg); - } - return create_pred(old_head, new_args); - } - - - void mk_array_instantiation::retrieve_selects(expr* e) - { - //If the expression is not a function application, we ignore it - if (!is_app(e)) { - return; - } - app*f=to_app(e); - //Call the function recursively on all arguments - unsigned nbargs = f->get_num_args(); - for(unsigned i=0;iget_arg(i)); - } - //If it is a select, then add it to selects - if(m_a.is_select(f)) - { - SASSERT(!m_a.is_array(get_sort(e))); - selects.insert_if_not_there(f->get_arg(0), ptr_vector()); - selects[f->get_arg(0)].push_back(e); - } - //If it is a condition between arrays, for example the result of a store, then add it to the equiv_classes - if(m_a.is_store(f)) - { - eq_classes.merge(e, f->get_arg(0)); - } - else if(m.is_eq(f) && m_a.is_array(get_sort(f->get_arg(0)))) - { - eq_classes.merge(f->get_arg(0), f->get_arg(1)); - } - } - - - expr_ref_vector mk_array_instantiation::getId(app*old_pred, const expr_ref_vector& n_args) - { - expr_ref_vector res(m); - for(unsigned i=0;iget_num_args();j++) - { - res.push_back(select->get_arg(j)); + rule_set * mk_array_instantiation::operator()(rule_set const & source) { + std::cout<<"Array Instantiation called with parameters :" + <<" enforce="< result = alloc(rule_set, m_ctx); + dst = result.get(); + unsigned nbrules = source.get_num_rules(); + src_manager = &source.get_rule_manager(); + for(unsigned i = 0; i < nbrules; i++) { + rule & r = *source.get_rule(i); + instantiate_rule(r, *result); } - } + std::cout<<"\n\nOutput rules = \n"; + result->display(std::cout); + return result.detach(); } - return res; - } - expr_ref mk_array_instantiation::create_pred(app*old_pred, expr_ref_vector& n_args) - { - expr_ref_vector new_args(m); - new_args.append(n_args); - new_args.append(getId(old_pred, n_args)); - for(unsigned i=0;iget_decl()->get_name().str()+"!inst").c_str()), new_sorts.size(), new_sorts.c_ptr(), old_pred->get_decl()->get_range()); - m_ctx.register_predicate(fun_decl, false); - if(src_set->is_output_predicate(old_pred->get_decl())) - dst->set_output_predicate(fun_decl); - res=m.mk_app(fun_decl,new_args.size(), new_args.c_ptr()); - return res; - } + void mk_array_instantiation::instantiate_rule(const rule& r, rule_set & dest) { + //Reset everything + selects.reset(); + eq_classes.reset(); + cnt = src_manager->get_counter().get_max_rule_var(r)+1; + done_selects.reset(); + ownership.reset(); - var * mk_array_instantiation::mk_select_var(expr* select) - { - var*result; - if(!done_selects.find(select, result)) - { - ownership.push_back(select); - result = m.mk_var(cnt, get_sort(select)); - cnt++; - done_selects.insert(select, result); - } - return result; - } - - expr_ref mk_array_instantiation::rewrite_select(expr*array, expr*select) - { - app*s = to_app(select); - expr_ref res(m); - expr_ref_vector args(m); - args.push_back(array); - for(unsigned i=1; iget_num_args();i++) - { - args.push_back(s->get_arg(i)); - } - res = m_a.mk_select(args.size(), args.c_ptr()); - return res; - } - - expr_ref_vector mk_array_instantiation::retrieve_all_selects(expr*array) - { - expr_ref_vector all_selects(m); - for(expr_equiv_class::iterator it = eq_classes.begin(array); - it != eq_classes.end(array); ++it) - { - selects.insert_if_not_there(*it, ptr_vector()); - ptr_vector& select_ops = selects[*it]; - for(unsigned i=0;iget_num_args(); - //Stores, for each old position, the list of a new possible arguments - vector arg_correspondance; - for(unsigned i=0;iget_arg(i), m); - if(m_a.is_array(get_sort(arg))) - { - vector arg_possibilities(m_ctx.get_params().xform_instantiate_arrays_nb_quantifier(), retrieve_all_selects(arg)); - arg_correspondance.append(arg_possibilities); - if(!m_ctx.get_params().xform_instantiate_arrays_enforce()) - { - expr_ref_vector tmp(m); - tmp.push_back(arg); - arg_correspondance.push_back(tmp); + expr_ref_vector phi(m); + expr_ref_vector preds(m); + expr_ref new_head = create_head(to_app(r.get_head())); + unsigned nb_predicates = r.get_uninterpreted_tail_size(); + unsigned tail_size = r.get_tail_size(); + for(unsigned i=0;i chosen(arg_correspondance.size(), 0u); - while(true) - { - expr_ref_vector new_args(m); - for(unsigned i=0;i::iterator it = done_selects.begin(); it!=done_selects.end(); ++it) { + expr_ref tmp(m); + tmp = &it->get_key(); + new_tail.push_back(m.mk_eq(it->get_value(), tmp)); + } + proof_ref pr(m); + src_manager->mk_rule(m.mk_implies(m.mk_and(new_tail.size(), new_tail.c_ptr()), new_head), pr, dest, r.name()); + } + + expr_ref mk_array_instantiation::create_head(app* old_head) { + expr_ref_vector new_args(m); + for(unsigned i=0;iget_num_args();i++) { + expr*arg = old_head->get_arg(i); + if(m_a.is_array(get_sort(arg))) { + for(unsigned k=0; k< m_ctx.get_params().xform_instantiate_arrays_nb_quantifier();k++) { + expr_ref_vector dummy_args(m); + dummy_args.push_back(arg); + for(unsigned i=0;i()); + selects[arg].push_back(select); + } + if(!m_ctx.get_params().xform_instantiate_arrays_enforce()) + new_args.push_back(arg); + } + else + new_args.push_back(arg); + } + return create_pred(old_head, new_args); + } + + + void mk_array_instantiation::retrieve_selects(expr* e) { + //If the expression is not a function application, we ignore it + if (!is_app(e)) { + return; + } + app*f=to_app(e); + //Call the function recursively on all arguments + unsigned nbargs = f->get_num_args(); + for(unsigned i=0;iget_arg(i)); + } + //If it is a select, then add it to selects + if(m_a.is_select(f)) { + SASSERT(!m_a.is_array(get_sort(e))); + selects.insert_if_not_there(f->get_arg(0), ptr_vector()); + selects[f->get_arg(0)].push_back(e); + } + //If it is a condition between arrays, for example the result of a store, then add it to the equiv_classes + if(m_a.is_store(f)) { + eq_classes.merge(e, f->get_arg(0)); + } + else if(m.is_eq(f) && m_a.is_array(get_sort(f->get_arg(0)))) { + eq_classes.merge(f->get_arg(0), f->get_arg(1)); + } + } + + + expr_ref_vector mk_array_instantiation::getId(app*old_pred, const expr_ref_vector& n_args) + { + expr_ref_vector res(m); + for(unsigned i=0;iget_num_args();j++) { + res.push_back(select->get_arg(j)); + } + } + } + return res; + } + + expr_ref mk_array_instantiation::create_pred(app*old_pred, expr_ref_vector& n_args) + { + expr_ref_vector new_args(m); + new_args.append(n_args); + new_args.append(getId(old_pred, n_args)); + for(unsigned i=0;iget_decl()->get_name().str()+"!inst").c_str()), new_sorts.size(), new_sorts.c_ptr(), old_pred->get_decl()->get_range()); + m_ctx.register_predicate(fun_decl, false); + if(src_set->is_output_predicate(old_pred->get_decl())) + dst->set_output_predicate(fun_decl); + res=m.mk_app(fun_decl,new_args.size(), new_args.c_ptr()); + return res; + } + + var * mk_array_instantiation::mk_select_var(expr* select) + { + var*result; + if(!done_selects.find(select, result)) { + ownership.push_back(select); + result = m.mk_var(cnt, get_sort(select)); + cnt++; + done_selects.insert(select, result); + } + return result; + } + + expr_ref mk_array_instantiation::rewrite_select(expr*array, expr*select) + { + app*s = to_app(select); + expr_ref res(m); + expr_ref_vector args(m); + args.push_back(array); + for(unsigned i=1; iget_num_args();i++) { + args.push_back(s->get_arg(i)); + } + res = m_a.mk_select(args.size(), args.c_ptr()); + return res; + } + + expr_ref_vector mk_array_instantiation::retrieve_all_selects(expr*array) + { + expr_ref_vector all_selects(m); + for(expr_equiv_class::iterator it = eq_classes.begin(array); + it != eq_classes.end(array); ++it) { + selects.insert_if_not_there(*it, ptr_vector()); + ptr_vector& select_ops = selects[*it]; + for(unsigned i=0;iget_num_args(); + //Stores, for each old position, the list of a new possible arguments + vector arg_correspondance; + for(unsigned i=0;iget_arg(i), m); + if(m_a.is_array(get_sort(arg))) { + vector arg_possibilities(m_ctx.get_params().xform_instantiate_arrays_nb_quantifier(), retrieve_all_selects(arg)); + arg_correspondance.append(arg_possibilities); + if(!m_ctx.get_params().xform_instantiate_arrays_enforce()) { + expr_ref_vector tmp(m); + tmp.push_back(arg); + arg_correspondance.push_back(tmp); + } + } + else { + expr_ref_vector tmp(m); + tmp.push_back(arg); + arg_correspondance.push_back(tmp); + } + } + //Now, we need to deal with every combination + + expr_ref_vector res(m); + + svector chosen(arg_correspondance.size(), 0u); + while(true) { + expr_ref_vector new_args(m); + for(unsigned i=0;i=arg_correspondance[pos].size()); + chosen[pos]++; } - }while(chosen[pos]+1>=arg_correspondance[pos].size()); - chosen[pos]++; } - } } diff --git a/src/muz/transforms/dl_mk_backwards.cpp b/src/muz/transforms/dl_mk_backwards.cpp index 0aa3c4d9a..4899ed126 100644 --- a/src/muz/transforms/dl_mk_backwards.cpp +++ b/src/muz/transforms/dl_mk_backwards.cpp @@ -33,7 +33,7 @@ namespace datalog { rule_set * mk_backwards::operator()(rule_set const & source) { context& ctx = source.get_context(); rule_manager& rm = source.get_rule_manager(); - rule_set * result = alloc(rule_set, ctx); + scoped_ptr result = alloc(rule_set, ctx); unsigned sz = source.get_num_rules(); rule_ref new_rule(rm); app_ref_vector tail(m); @@ -72,7 +72,7 @@ namespace datalog { } } TRACE("dl", result->display(tout);); - return result; + return result.detach(); } }; diff --git a/src/muz/transforms/dl_mk_coalesce.cpp b/src/muz/transforms/dl_mk_coalesce.cpp index 6613b6551..2ff4372c4 100644 --- a/src/muz/transforms/dl_mk_coalesce.cpp +++ b/src/muz/transforms/dl_mk_coalesce.cpp @@ -172,7 +172,7 @@ namespace datalog { } rule_set * mk_coalesce::operator()(rule_set const & source) { - rule_set* rules = alloc(rule_set, m_ctx); + scoped_ptr rules = alloc(rule_set, m_ctx); rules->inherit_predicates(source); rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules(); for (; it != end; ++it) { @@ -181,8 +181,8 @@ namespace datalog { for (unsigned i = 0; i < d_rules.size(); ++i) { rule_ref r1(d_rules[i].get(), rm); for (unsigned j = i + 1; j < d_rules.size(); ++j) { - if (same_body(*r1.get(), *d_rules[j].get())) { - merge_rules(r1, *d_rules[j].get()); + if (same_body(*r1.get(), *d_rules.get(j))) { + merge_rules(r1, *d_rules.get(j)); d_rules[j] = d_rules.back(); d_rules.pop_back(); --j; @@ -191,7 +191,7 @@ namespace datalog { rules->add_rule(r1.get()); } } - return rules; + return rules.detach(); } }; diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 5ad3f67d2..eccbd0921 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -602,17 +602,16 @@ namespace datalog { return nullptr; } - rule_set * res = alloc(rule_set, m_context); + scoped_ptr res = alloc(rule_set, m_context); if (transform_rules(source, *res)) { res->inherit_predicates(source); TRACE("dl", source.display(tout); res->display(tout);); } else { - dealloc(res); res = nullptr; } - return res; + return res.detach(); } }; diff --git a/src/muz/transforms/dl_mk_loop_counter.cpp b/src/muz/transforms/dl_mk_loop_counter.cpp index e0895981f..b22d9fa3b 100644 --- a/src/muz/transforms/dl_mk_loop_counter.cpp +++ b/src/muz/transforms/dl_mk_loop_counter.cpp @@ -68,7 +68,7 @@ namespace datalog { m_old2new.reset(); m_new2old.reset(); rule_manager& rm = source.get_rule_manager(); - rule_set * result = alloc(rule_set, m_ctx); + scoped_ptr result = alloc(rule_set, m_ctx); unsigned sz = source.get_num_rules(); rule_ref new_rule(rm); app_ref_vector tail(m); @@ -118,7 +118,7 @@ namespace datalog { // model converter: remove references to extra argument. // proof converter: remove references to extra argument as well. - return result; + return result.detach(); } rule_set * mk_loop_counter::revert(rule_set const & source) { diff --git a/src/muz/transforms/dl_mk_magic_sets.cpp b/src/muz/transforms/dl_mk_magic_sets.cpp index b951cfd28..85c88716c 100644 --- a/src/muz/transforms/dl_mk_magic_sets.cpp +++ b/src/muz/transforms/dl_mk_magic_sets.cpp @@ -345,7 +345,7 @@ namespace datalog { var_idx_set empty_var_idx_set; adorn_literal(goal_head, empty_var_idx_set); - rule_set * result = alloc(rule_set, m_context); + scoped_ptr result = alloc(rule_set, m_context); result->inherit_predicates(source); while (!m_todo.empty()) { @@ -373,7 +373,7 @@ namespace datalog { rule * back_to_goal_rule = m_context.get_rule_manager().mk(goal_head, 1, &adn_goal_head, nullptr); result->add_rule(back_to_goal_rule); - return result; + return result.detach(); } }; diff --git a/src/muz/transforms/dl_mk_magic_symbolic.cpp b/src/muz/transforms/dl_mk_magic_symbolic.cpp index acdf0bff0..ac4efd448 100644 --- a/src/muz/transforms/dl_mk_magic_symbolic.cpp +++ b/src/muz/transforms/dl_mk_magic_symbolic.cpp @@ -72,7 +72,7 @@ namespace datalog { } context& ctx = source.get_context(); rule_manager& rm = source.get_rule_manager(); - rule_set * result = alloc(rule_set, ctx); + scoped_ptr result = alloc(rule_set, ctx); unsigned sz = source.get_num_rules(); rule_ref new_rule(rm); app_ref_vector tail(m); @@ -109,7 +109,7 @@ namespace datalog { } TRACE("dl", result->display(tout);); - return result; + return result.detach(); } app_ref mk_magic_symbolic::mk_query(app* q) { diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index dacb32d1b..f956ca429 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -329,7 +329,7 @@ namespace datalog { if (m_ctx.get_model_converter()) { m_mc = alloc(qa_model_converter, m); } - rule_set * result = alloc(rule_set, m_ctx); + scoped_ptr result = alloc(rule_set, m_ctx); for (unsigned i = 0; i < sz; ++i) { tail.reset(); @@ -354,7 +354,6 @@ namespace datalog { // proof converter: proofs are not necessarily preserved using this transformation. if (m_old2new.empty()) { - dealloc(result); dealloc(m_mc); result = nullptr; } @@ -363,7 +362,7 @@ namespace datalog { } m_mc = nullptr; - return result; + return result.detach(); } diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index 0a183b923..032b4b19c 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -264,7 +264,7 @@ namespace datalog { expr_ref_vector conjs(m); quantifier_ref_vector qs(m); - rule_set * result = alloc(rule_set, m_ctx); + scoped_ptr result = alloc(rule_set, m_ctx); bool instantiated = false; @@ -286,10 +286,9 @@ namespace datalog { result->inherit_predicates(source); } else { - dealloc(result); result = nullptr; } - return result; + return result.detach(); } diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp index 95397fa67..84e48d514 100644 --- a/src/muz/transforms/dl_mk_scale.cpp +++ b/src/muz/transforms/dl_mk_scale.cpp @@ -120,7 +120,7 @@ namespace datalog { return nullptr; } rule_manager& rm = source.get_rule_manager(); - rule_set * result = alloc(rule_set, m_ctx); + scoped_ptr result = alloc(rule_set, m_ctx); unsigned sz = source.get_num_rules(); rule_ref new_rule(rm); app_ref_vector tail(m); @@ -166,7 +166,7 @@ namespace datalog { } m_trail.reset(); m_cache.reset(); - return result; + return result.detach(); } app_ref mk_scale::mk_pred(unsigned sigma_idx, app* q) { diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index b2f464931..b4b64de24 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -841,11 +841,10 @@ namespace datalog { m_mc = smc.get(); reset(); saturate(src); - rule_set* result = alloc(rule_set, m_ctx); + scoped_ptr result = alloc(rule_set, m_ctx); declare_predicates(src, *result); if (m_predicates.empty()) { // nothing could be sliced. - dealloc(result); return nullptr; } TRACE("dl", display(tout);); @@ -859,7 +858,7 @@ namespace datalog { } m_ctx.add_proof_converter(spc.get()); m_ctx.add_model_converter(smc.get()); - return result; + return result.detach(); } }; diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index 4c5a08eb5..e277a93b4 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -343,11 +343,10 @@ namespace datalog { scan_for_total_rules(source); m_have_new_total_rule = false; - rule_set * res = alloc(rule_set, m_context); + scoped_ptr res = alloc(rule_set, m_context); bool modified = transform_rules(source, *res); if (!m_have_new_total_rule && !modified) { - dealloc(res); return nullptr; } @@ -358,13 +357,12 @@ namespace datalog { while (m_have_new_total_rule) { m_have_new_total_rule = false; - rule_set * old = res; + scoped_ptr old = res; res = alloc(rule_set, m_context); transform_rules(*old, *res); - dealloc(old); } - return res; + return res.detach(); } }; From 38176256c4bc9a7a896f2054dbde4dbbf166b88f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 10:12:49 -0700 Subject: [PATCH 12/21] fix #4434 Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_array_blast.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp index 34e739bc3..a8093634d 100644 --- a/src/muz/transforms/dl_mk_array_blast.cpp +++ b/src/muz/transforms/dl_mk_array_blast.cpp @@ -322,18 +322,19 @@ namespace datalog { if (!m_ctx.array_blast ()) { return nullptr; } - rule_set* rules = alloc(rule_set, m_ctx); + scoped_ptr rules = alloc(rule_set, m_ctx); rules->inherit_predicates(source); rule_set::iterator it = source.begin(), end = source.end(); bool change = false; - for (; !m_ctx.canceled() && it != end; ++it) { - change = blast(**it, *rules) || change; + for (rule* r : source) { + if (m_ctx.canceled()) + return nullptr; + change = blast(*r, *rules) || change; } if (!change) { - dealloc(rules); rules = nullptr; } - return rules; + return rules.detach(); } }; From f5cd4e3ac0097ef2303d89b2f550586b4c315978 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 10:15:55 -0700 Subject: [PATCH 13/21] janitor services Signed-off-by: Nikolaj Bjorner --- src/test/old_interval.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/test/old_interval.cpp b/src/test/old_interval.cpp index 7ef9cdc87..751f6fdbe 100644 --- a/src/test/old_interval.cpp +++ b/src/test/old_interval.cpp @@ -140,6 +140,7 @@ class interval_tester { std::cerr << l(-10, true) << "\n"; std::cerr << r(10, true) << "\n"; std::cerr << b(2, 10) << "\n"; +#if 0 std::cerr << wd(b(-5, 5, true, false, 1, 2) * b(-5, 5, false, true, 3, 4)) << "\n"; std::cerr << wd(l(2, false, 1) / b(2, 6, false, false, 2, 3)) << "\n"; std::cerr << wd(expt(b(-2, 3, true, false, 1, 2), 2)) << "\n"; @@ -148,6 +149,7 @@ class interval_tester { std::cerr << wd(expt(b(0, 3, true, false, 1, 2), 2)) << "\n"; std::cerr << wd(expt(b(-4, -2, true, false, 1, 2), 2)) << "\n"; std::cerr << b(2, 10, false, false, 1, 2) << " * " << l(10, false, 3).inv() << " = " << wd(b(2, 10, false, false, 1, 2) / l(10, false, 3)) << "\n"; +#endif std::cerr << b(-2, -1, false, true) << " * " << b(-3,0) << " = "; std::cerr.flush(); std::cerr << (b(-2, -1, false, true) * b(-3,0)) << "\n"; std::cerr << b(1, 2, true, false) << " * " << b(0,3) << " = "; std::cerr.flush(); From 8ae42b5ae120b268d7b29e1545d377a0f2f6c410 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 10:23:26 -0700 Subject: [PATCH 14/21] fix #4433 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_finder.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 6ba4868cb..5b6e4638a 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -2386,9 +2386,9 @@ namespace smt { expr * e = q->get_expr(); reset_cache(); if (!m.inc()) return; - SASSERT(m_ttodo.empty()); - SASSERT(m_ftodo.empty()); - + m_ttodo.reset(); + m_ftodo.reset(); + if (is_clause(m, e)) { process_clause(e); } From 377dbad3b95a54ec30b36aa0e365153222f1d386 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 10:27:08 -0700 Subject: [PATCH 15/21] fix #4435 Signed-off-by: Nikolaj Bjorner --- src/smt/asserted_formulas.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index cba9832d2..576a85a87 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -665,11 +665,12 @@ proof * asserted_formulas::get_inconsistency_proof() const { return nullptr; if (!m.proofs_enabled()) return nullptr; + if (!m.inc()) + return nullptr; for (justified_expr const& j : m_formulas) { if (m.is_false(j.get_fml())) return j.get_proof(); } - UNREACHABLE(); return nullptr; } From 3a7df2c6ef6518c8fcae8b136b318023e50d8e7e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 12:28:32 -0700 Subject: [PATCH 16/21] fix various nullability checks in seq_regex Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_array_blast.cpp | 1 - src/nlsat/nlsat_solver.cpp | 4 +++- src/qe/qe_arith_plugin.cpp | 11 ++++------- src/smt/seq_regex.cpp | 22 +++++++++++++++------- 4 files changed, 22 insertions(+), 16 deletions(-) diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp index a8093634d..e32ddf269 100644 --- a/src/muz/transforms/dl_mk_array_blast.cpp +++ b/src/muz/transforms/dl_mk_array_blast.cpp @@ -324,7 +324,6 @@ namespace datalog { } scoped_ptr rules = alloc(rule_set, m_ctx); rules->inherit_predicates(source); - rule_set::iterator it = source.begin(), end = source.end(); bool change = false; for (rule* r : source) { if (m_ctx.canceled()) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index a7dbedca4..3e4773f7e 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1967,7 +1967,9 @@ namespace nlsat { bool resolve(clause const & conflict) { clause const * conflict_clause = &conflict; m_lemma_assumptions = nullptr; - start: + std::cout << "resolve\n"; + start: + std::cout << "start\n"; SASSERT(check_marks()); TRACE("nlsat_proof", tout << "STARTING RESOLUTION\n";); TRACE("nlsat_proof_sk", tout << "STARTING RESOLUTION\n";); diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index 6b7eb2897..30b09a381 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -2412,24 +2412,21 @@ public: } bool update_bounds(contains_app& contains_x, expr* fml) { - bounds_proc* bounds = nullptr; - if (m_bounds_cache.find(contains_x.x(), fml, bounds)) { + bounds_proc* _bounds = nullptr; + if (m_bounds_cache.find(contains_x.x(), fml, _bounds)) { return true; } - bounds = alloc(bounds_proc, m_util); - + scoped_ptr bounds = alloc(bounds_proc, m_util); if (!update_bounds(*bounds, contains_x, fml, m_ctx.pos_atoms(), true)) { - dealloc(bounds); return false; } if (!update_bounds(*bounds, contains_x, fml, m_ctx.neg_atoms(), false)) { - dealloc(bounds); return false; } m_trail.push_back(contains_x.x()); m_trail.push_back(fml); - m_bounds_cache.insert(contains_x.x(), fml, bounds); + m_bounds_cache.insert(contains_x.x(), fml, bounds.detach()); return true; } }; diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 30d7b66c3..4ca6cdbf7 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -195,11 +195,22 @@ namespace smt { VERIFY(sk().is_accept(e, s, i, idx, r)); expr_ref is_nullable(m), d(r, m); + TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";); if (block_unfolding(lit, idx)) return true; + literal_vector conds; + conds.push_back(~lit); + if (!unfold_cofactors(d, conds)) + return false; + + if (re().is_empty(d)) { + th.add_axiom(conds); + return true; + } + // s in R & len(s) <= i => nullable(R) literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx); switch (ctx.get_assignment(len_s_le_i)) { @@ -207,25 +218,22 @@ namespace smt { ctx.mark_as_relevant(len_s_le_i); return false; case l_true: - is_nullable = seq_rw().is_nullable(r); + is_nullable = seq_rw().is_nullable(d); rewrite(is_nullable); - th.add_axiom(~lit, ~len_s_le_i, th.mk_literal(is_nullable)); + conds.push_back(~len_s_le_i); + conds.push_back(th.mk_literal(is_nullable)); + th.add_axiom(conds); return true; case l_false: break; } - literal_vector conds; - if (!unfold_cofactors(d, conds)) - return false; - // (accept s i R) & len(s) > i => (accept s (+ i 1) D(nth(s, i), R)) or conds expr_ref head = th.mk_nth(s, i); d = re().mk_derivative(head, r); rewrite(d); literal acc_next = th.mk_literal(sk().mk_accept(s, a().mk_int(idx + 1), d)); - conds.push_back(~lit); conds.push_back(len_s_le_i); conds.push_back(acc_next); th.add_axiom(conds); From e2b2b7f82e295f7675ab44ced33bcc33c9c95a2a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 12:29:29 -0700 Subject: [PATCH 17/21] na Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 3e4773f7e..a7dbedca4 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1967,9 +1967,7 @@ namespace nlsat { bool resolve(clause const & conflict) { clause const * conflict_clause = &conflict; m_lemma_assumptions = nullptr; - std::cout << "resolve\n"; - start: - std::cout << "start\n"; + start: SASSERT(check_marks()); TRACE("nlsat_proof", tout << "STARTING RESOLUTION\n";); TRACE("nlsat_proof_sk", tout << "STARTING RESOLUTION\n";); From e844aef896be906d2f100f7e7f216c9878cd874b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 3 Jun 2020 20:30:21 +0100 Subject: [PATCH 18/21] remove a few more copy constructors, though still not enough to enable the assertion in vector I give up for now; there are too many copies left for little return.. --- src/ast/justified_expr.h | 2 +- src/ast/recfun_decl_plugin.cpp | 2 -- src/math/dd/dd_pdd.h | 2 +- src/math/lp/indexed_value.h | 13 ------------- src/math/lp/numeric_pair.h | 2 -- src/math/simplex/model_based_opt.h | 1 - src/opt/maxsmt.h | 2 -- src/opt/pb_sls.cpp | 10 ---------- src/qe/qe_arrays.cpp | 11 +++-------- src/util/array_map.h | 16 ++++++++-------- src/util/inf_rational.h | 11 ++--------- src/util/inf_s_integer.h | 9 +-------- src/util/obj_ref.h | 7 ++----- src/util/ref_vector.h | 14 +++++++++++++- src/util/scoped_numeral.h | 6 ++---- src/util/scoped_numeral_vector.h | 15 ++++++++++----- src/util/uint_set.h | 16 +--------------- 17 files changed, 44 insertions(+), 95 deletions(-) diff --git a/src/ast/justified_expr.h b/src/ast/justified_expr.h index 2e49051e3..786061065 100644 --- a/src/ast/justified_expr.h +++ b/src/ast/justified_expr.h @@ -39,7 +39,7 @@ public: m.inc_ref(m_proof); } - justified_expr(justified_expr && other): + justified_expr(justified_expr && other) noexcept : m(other.m), m_fml(nullptr), m_proof(nullptr) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 99e0da198..87a09afb0 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -131,8 +131,6 @@ namespace recfun { path(nullptr), to_split(nullptr), to_unfold(to_unfold) {} branch(choice_lst const * path, ite_lst const * to_split, unfold_lst const * to_unfold) : path(path), to_split(to_split), to_unfold(to_unfold) {} - branch(branch const & from) : - path(from.path), to_split(from.to_split), to_unfold(from.to_unfold) {} }; // state for computing cases from the RHS of a functions' definition diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index b24f95c6d..d12af2585 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -320,7 +320,7 @@ namespace dd { public: pdd(pdd_manager& pm): root(0), m(pm) { SASSERT(is_zero()); } pdd(pdd const& other): root(other.root), m(other.m) { m.inc_ref(root); } - pdd(pdd && other): root(0), m(other.m) { std::swap(root, other.root); } + pdd(pdd && other) noexcept : root(0), m(other.m) { std::swap(root, other.root); } pdd& operator=(pdd const& other); ~pdd() { m.dec_ref(root); } pdd lo() const { return pdd(m.lo(root), m); } diff --git a/src/math/lp/indexed_value.h b/src/math/lp/indexed_value.h index 38e48f4aa..c48376470 100644 --- a/src/math/lp/indexed_value.h +++ b/src/math/lp/indexed_value.h @@ -35,19 +35,6 @@ public: m_value(v), m_index(i), m_other(other) { } - indexed_value(const indexed_value & iv) { - m_value = iv.m_value; - m_index = iv.m_index; - m_other = iv.m_other; - } - - indexed_value & operator=(const indexed_value & right_side) { - m_value = right_side.m_value; - m_index = right_side.m_index; - m_other = right_side.m_other; - return *this; - } - const T & value() const { return m_value; } diff --git a/src/math/lp/numeric_pair.h b/src/math/lp/numeric_pair.h index cd992ccb2..e7586cf5a 100644 --- a/src/math/lp/numeric_pair.h +++ b/src/math/lp/numeric_pair.h @@ -144,8 +144,6 @@ struct numeric_pair { explicit numeric_pair(const X & n) : x(n), y(0) { } - numeric_pair(const numeric_pair & n) : x(n.x), y(n.y) {} - template numeric_pair(X xp, Y yp) : x(convert_struct::convert(xp)), y(convert_struct::convert(yp)) {} diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h index 7311850ab..4740a4899 100644 --- a/src/math/simplex/model_based_opt.h +++ b/src/math/simplex/model_based_opt.h @@ -67,7 +67,6 @@ namespace opt { struct def { def(): m_div(1) {} def(row const& r, unsigned x); - def(def const& other): m_vars(other.m_vars), m_coeff(other.m_coeff), m_div(other.m_div) {} vector m_vars; rational m_coeff; rational m_div; diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 291ec26d8..02fc16e02 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -64,8 +64,6 @@ namespace opt { void set_value(lbool t) { value = t; } bool is_true() const { return value == l_true; } soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {} - soft(soft const& other):s(other.s), weight(other.weight), value(other.value) {} - soft& operator=(soft const& other) { s = other.s; weight = other.weight; value = other.value; return *this; } }; ast_manager& m; maxsat_context& m_c; diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index c433f56d3..315b6f22a 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -77,16 +77,6 @@ namespace smt { m_value(m), m_eq(true) {} - clause(clause const& cls): - m_lits(cls.m_lits), - m_weights(cls.m_weights.m()), - m_k(cls.m_k), - m_value(cls.m_value), - m_eq(cls.m_eq) { - for (unsigned i = 0; i < cls.m_weights.size(); ++i) { - m_weights.push_back(cls.m_weights[i]); - } - } }; struct stats { diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index cee6e3e8e..cec3a7726 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -899,12 +899,8 @@ namespace qe { expr_ref_vector idx; expr_ref_vector val; vector rval; - idx_val(expr_ref_vector & idx, expr_ref_vector & val, vector const& rval): idx(idx), val(val), rval(rval) {} - idx_val& operator=(idx_val const& o) { - idx.reset(); val.reset(); rval.reset(); - idx.append(o.idx); val.append(o.val); rval.append(o.rval); - return *this; - } + idx_val(expr_ref_vector && idx, expr_ref_vector && val, vector && rval): + idx(std::move(idx)), val(std::move(val)), rval(std::move(rval)) {} }; ast_manager& m; array_util m_arr_u; @@ -1049,8 +1045,7 @@ namespace qe { } if (is_new) { // new repr, val, and sel const - vector rvals = to_num(vals); - m_idxs.push_back(idx_val(idxs, vals, rvals)); + m_idxs.push_back(idx_val(std::move(idxs), std::move(vals), to_num(vals))); app_ref c (m.mk_fresh_const ("sel", val_sort), m); m_sel_consts.push_back (c); // substitute sel term with new const diff --git a/src/util/array_map.h b/src/util/array_map.h index f3f99d015..91d226dab 100644 --- a/src/util/array_map.h +++ b/src/util/array_map.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef ARRAY_MAP_H_ -#define ARRAY_MAP_H_ +#pragma once #include "util/vector.h" #include "util/optional.h" @@ -40,9 +39,9 @@ class array_map { entry(Key const & k, Data const & d, unsigned t): m_key(k), m_data(d), m_timestamp(t) {} }; - unsigned m_timestamp; - unsigned m_garbage; - unsigned m_non_garbage; + unsigned m_timestamp = 0; + unsigned m_garbage = 0; + unsigned m_non_garbage = 0; static const unsigned m_gc_threshold = 10000; vector, CallDestructors > m_map; Plugin m_plugin; @@ -76,7 +75,10 @@ class array_map { public: - array_map(Plugin const & p = Plugin()):m_timestamp(0), m_garbage(0), m_non_garbage(0), m_plugin(p) {} + array_map() = default; + array_map(array_map&&) noexcept = default; + array_map(Plugin const & p) : m_plugin(p) {} + ~array_map() { really_flush(); } bool contains(Key const & k) const { @@ -155,5 +157,3 @@ public: } }; - -#endif /* ARRAY_MAP_H_ */ diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h index c3f4160ba..86e04543c 100644 --- a/src/util/inf_rational.h +++ b/src/util/inf_rational.h @@ -17,8 +17,8 @@ Author: Revision History: --*/ -#ifndef INF_RATIONAL_H_ -#define INF_RATIONAL_H_ +#pragma once + #include #include #include "util/debug.h" @@ -67,11 +67,6 @@ class inf_rational { inf_rational() {} - inf_rational(const inf_rational & r): - m_first(r.m_first), - m_second(r.m_second) - {} - explicit inf_rational(int n): m_first(rational(n)), m_second(rational()) @@ -470,5 +465,3 @@ inline inf_rational abs(const inf_rational & r) { } return result; } - -#endif /* INF_RATIONAL_H_ */ diff --git a/src/util/inf_s_integer.h b/src/util/inf_s_integer.h index dd136d1b9..b99167b32 100644 --- a/src/util/inf_s_integer.h +++ b/src/util/inf_s_integer.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef INF_S_INTEGER_H_ -#define INF_S_INTEGER_H_ +#pragma once #include "util/s_integer.h" #include "util/rational.h" @@ -47,8 +46,6 @@ class inf_s_integer { inf_s_integer():m_first(0), m_second(0) {} - inf_s_integer(const inf_s_integer & r):m_first(r.m_first), m_second(r.m_second) {} - explicit inf_s_integer(int n):m_first(n), m_second(0) {} explicit inf_s_integer(int n, int d): m_first(n), m_second(0) { SASSERT(d == 1); } explicit inf_s_integer(s_integer const& r, bool pos_inf):m_first(r.get_int()), m_second(pos_inf ? 1 : -1) {} @@ -345,7 +342,3 @@ inline inf_s_integer abs(const inf_s_integer & r) { } return result; } - - -#endif /* INF_S_INTEGER_H_ */ - diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h index e3b0d0710..6b00f894f 100644 --- a/src/util/obj_ref.h +++ b/src/util/obj_ref.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef OBJ_REF_H_ -#define OBJ_REF_H_ +#pragma once /** Smart pointer for T objects. @@ -53,7 +52,7 @@ public: inc_ref(); } - obj_ref(obj_ref && other) : m_obj(nullptr), m_manager(other.m_manager) { + obj_ref(obj_ref && other) noexcept : m_obj(nullptr), m_manager(other.m_manager) { std::swap(m_obj, other.m_obj); } @@ -146,5 +145,3 @@ inline void dec_range_ref(IT const & begin, IT const & end, TManager & m) { } } } - -#endif /* OBJ_REF_H_ */ diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index ce8060cd3..40c01b012 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -191,6 +191,13 @@ public: push_back(data[i]); } + void operator=(ref_vector_core && other) { + if (this != &other) { + reset(); + m_nodes = std::move(other.m_nodes); + } + } + void swap(unsigned idx1, unsigned idx2) { std::swap(m_nodes[idx1], m_nodes[idx2]); } @@ -234,7 +241,7 @@ public: this->append(other); } - ref_vector(ref_vector && other) : super(std::move(other)) {} + ref_vector(ref_vector &&) = default; ref_vector(TManager & m, unsigned sz, T * const * data): super(ref_manager_wrapper(m)) { @@ -320,6 +327,11 @@ public: // prevent abuse: ref_vector & operator=(ref_vector const & other) = delete; + ref_vector & operator=(ref_vector && other) { + super::operator=(std::move(other)); + return *this; + } + bool operator==(ref_vector const& other) const { if (other.size() != this->size()) return false; for (unsigned i = this->size(); i-- > 0; ) { diff --git a/src/util/scoped_numeral.h b/src/util/scoped_numeral.h index 2c80c4703..3b35a1bd8 100644 --- a/src/util/scoped_numeral.h +++ b/src/util/scoped_numeral.h @@ -17,8 +17,7 @@ Author: Revision History: --*/ -#ifndef SCOPED_NUMERAL_H_ -#define SCOPED_NUMERAL_H_ +#pragma once template class _scoped_numeral { @@ -30,6 +29,7 @@ private: public: _scoped_numeral(Manager & m):m_manager(m) {} _scoped_numeral(_scoped_numeral const & n):m_manager(n.m_manager) { m().set(m_num, n.m_num); } + _scoped_numeral(_scoped_numeral &&) = default; ~_scoped_numeral() { m_manager.del(m_num); } Manager & m() const { return m_manager; } @@ -189,5 +189,3 @@ public: } }; - -#endif diff --git a/src/util/scoped_numeral_vector.h b/src/util/scoped_numeral_vector.h index cb9a6b4fd..f53d93470 100644 --- a/src/util/scoped_numeral_vector.h +++ b/src/util/scoped_numeral_vector.h @@ -16,17 +16,24 @@ Author: Revision History: --*/ -#ifndef SCOPED_NUMERAL_VECTOR_H_ -#define SCOPED_NUMERAL_VECTOR_H_ +#pragma once #include "util/vector.h" template class _scoped_numeral_vector : public svector { Manager & m_manager; - _scoped_numeral_vector(_scoped_numeral_vector const & v); public: _scoped_numeral_vector(Manager & m):m_manager(m) {} + + _scoped_numeral_vector(const _scoped_numeral_vector & other) : m_manager(other.m_manager) { + for (unsigned i = 0, e = other.size(); i != e; ++i) { + push_back((*this)[i]); + } + } + + _scoped_numeral_vector(_scoped_numeral_vector&&) = default; + ~_scoped_numeral_vector() { reset(); } @@ -66,5 +73,3 @@ public: svector::resize(sz, 0); } }; - -#endif diff --git a/src/util/uint_set.h b/src/util/uint_set.h index ebef623aa..46a606e8f 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -16,8 +16,7 @@ Author: Revision History: --*/ -#ifndef UINT_SET_H_ -#define UINT_SET_H_ +#pragma once #include "util/util.h" #include "util/vector.h" @@ -29,16 +28,6 @@ public: typedef unsigned data; - uint_set() {} - - uint_set(const uint_set & source) { - for (unsigned i = 0; i < source.size(); ++i) { - push_back(source[i]); - } - } - - ~uint_set() {} - void swap(uint_set & other) { unsigned_vector::swap(other); } @@ -384,6 +373,3 @@ inline std::ostream& operator<<(std::ostream& out, indexed_uint_set const& s) { for (unsigned i : s) out << i << " "; return out; } - -#endif /* UINT_SET_H_ */ - From 9fac010d8e3ef373d26ac3f24deaeed06eeafb19 Mon Sep 17 00:00:00 2001 From: "Andrew V. Jones" Date: Wed, 3 Jun 2020 21:34:43 +0100 Subject: [PATCH 19/21] Fixing build errors when building test-z3 (#4496) Signed-off-by: Andrew V. Jones --- src/math/hilbert/heap_trie.h | 2 +- src/test/mpff.cpp | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/math/hilbert/heap_trie.h b/src/math/hilbert/heap_trie.h index 3c6ecd1cb..add64d2a0 100644 --- a/src/math/hilbert/heap_trie.h +++ b/src/math/hilbert/heap_trie.h @@ -37,13 +37,13 @@ Notes: #ifndef HEAP_TRIE_H_ #define HEAP_TRIE_H_ +#include #include "util/map.h" #include "util/vector.h" #include "util/buffer.h" #include "util/statistics.h" #include "util/small_object_allocator.h" - template class heap_trie { diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp index c78489f21..83c500b49 100644 --- a/src/test/mpff.cpp +++ b/src/test/mpff.cpp @@ -16,7 +16,8 @@ Author: Revision History: --*/ -#include +#include +#include #include "util/mpff.h" #include "util/mpz.h" #include "util/mpq.h" From d50fc6976b131f74fe465257afd1ed610ceebcc7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 13:47:50 -0700 Subject: [PATCH 20/21] fix #4430 Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index a7dbedca4..65c2a8795 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1961,6 +1961,13 @@ namespace nlsat { return new_lvl; } + struct scoped_reset_marks { + imp& i; + scoped_reset_marks(imp& i):i(i) {} + ~scoped_reset_marks() { if (i.m_num_marks > 0) { i.m_num_marks = 0; for (char& m : i.m_marks) m = 0; } } + }; + + /** \brief Return true if the conflict was solved. */ @@ -1980,7 +1987,7 @@ namespace nlsat { m_num_marks = 0; m_lemma.reset(); m_lemma_assumptions = nullptr; - + scoped_reset_marks _sr(*this); resolve_clause(null_bool_var, *conflict_clause); unsigned top = m_trail.size(); From f986ae97bdcbfc64820969eb5540412439961511 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 15:12:08 -0700 Subject: [PATCH 21/21] fix build Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_coi_filter.cpp | 3 ++- src/muz/transforms/dl_mk_interp_tail_simplifier.cpp | 3 ++- src/muz/transforms/dl_mk_subsumption_checker.cpp | 5 ++--- src/muz/transforms/dl_mk_unbound_compressor.cpp | 4 ++-- src/muz/transforms/dl_mk_unfold.cpp | 9 ++++----- 5 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index 8c34325a4..79959d9bf 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -128,7 +128,8 @@ namespace datalog { func_decl * pred = r->get_decl(); if (engine.get_fact(pred).is_reachable()) { res->add_rule(r); - } else if (m_context.get_model_converter()) { + } + else if (m_context.get_model_converter()) { pruned_preds.insert(pred); } } diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index eccbd0921..fe9dee45e 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -608,7 +608,8 @@ namespace datalog { TRACE("dl", source.display(tout); res->display(tout);); - } else { + } + else { res = nullptr; } return res.detach(); diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index e277a93b4..d75ae0b46 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -335,7 +335,7 @@ namespace datalog { rule_set * mk_subsumption_checker::operator()(rule_set const & source) { // TODO mc if (!m_context.get_params ().xform_subsumption_checker()) - return nullptr; + return nullptr; m_have_new_total_rule = false; collect_ground_unconditional_rule_heads(source); @@ -356,8 +356,7 @@ namespace datalog { SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule); while (m_have_new_total_rule) { m_have_new_total_rule = false; - - scoped_ptr old = res; + scoped_ptr old = res.detach(); res = alloc(rule_set, m_context); transform_rules(*old, *res); } diff --git a/src/muz/transforms/dl_mk_unbound_compressor.cpp b/src/muz/transforms/dl_mk_unbound_compressor.cpp index 6be75fc2c..c9d4fd3c6 100644 --- a/src/muz/transforms/dl_mk_unbound_compressor.cpp +++ b/src/muz/transforms/dl_mk_unbound_compressor.cpp @@ -387,7 +387,7 @@ namespace datalog { } } - rule_set * result = static_cast(nullptr); + scoped_ptr result; if (m_modified) { result = alloc(rule_set, m_context); unsigned fin_rule_cnt = m_rules.size(); @@ -397,7 +397,7 @@ namespace datalog { result->inherit_predicates(source); } reset(); - return result; + return result.detach(); } diff --git a/src/muz/transforms/dl_mk_unfold.cpp b/src/muz/transforms/dl_mk_unfold.cpp index c9b8becde..6a1ae1535 100644 --- a/src/muz/transforms/dl_mk_unfold.cpp +++ b/src/muz/transforms/dl_mk_unfold.cpp @@ -51,13 +51,12 @@ namespace datalog { } rule_set * mk_unfold::operator()(rule_set const & source) { - rule_set* rules = alloc(rule_set, m_ctx); - rule_set::iterator it = source.begin(), end = source.end(); - for (; it != end; ++it) { - expand_tail(**it, 0, source, *rules); + scoped_ptr rules = alloc(rule_set, m_ctx); + for (rule* r : source) { + expand_tail(*r, 0, source, *rules); } rules->inherit_predicates(source); - return rules; + return rules.detach(); } };