From cec328cfdc0deadcc50d412e1cc88b9ed1bab1c2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Dec 2012 14:44:51 -0800
Subject: [PATCH] Add get_sort(expr * n) function that does not depend on
ast_manager. Move power_of_two to rational class. Add arith_recognizers and
bv_recognizers classes. The two new classes contain the 'read-only' methods
from arith_util and bv_util.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/ast/arith_decl_plugin.cpp | 24 +--
src/ast/arith_decl_plugin.h | 69 ++++---
src/ast/ast.cpp | 39 ++--
src/ast/ast.h | 4 +-
src/ast/bv_decl_plugin.cpp | 177 +++++++++---------
src/ast/bv_decl_plugin.h | 142 +++++++-------
src/ast/rewriter/bit_blaster/bit_blaster.h | 2 +-
.../bit_blaster/bit_blaster_rewriter.cpp | 2 +-
src/ast/rewriter/bv_rewriter.cpp | 48 ++---
src/ast/simplifier/bv_simplifier_plugin.cpp | 40 ++--
src/ast/simplifier/bv_simplifier_plugin.h | 2 +-
src/tactic/arith/bv2int_rewriter.cpp | 2 +-
src/tactic/arith/nla2bv_tactic.cpp | 2 +-
src/tactic/arith/pb2bv_tactic.cpp | 4 +-
src/tactic/core/elim_uncnstr_tactic.cpp | 6 +-
src/util/rational.cpp | 26 +++
src/util/rational.h | 7 +-
17 files changed, 314 insertions(+), 282 deletions(-)
diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index a89cc18d0..093f6b346 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -573,18 +573,7 @@ expr * arith_decl_plugin::get_some_value(sort * s) {
return mk_numeral(rational(0), s == m_int_decl);
}
-arith_util::arith_util(ast_manager & m):
- m_manager(m),
- m_afid(m.get_family_id("arith")),
- m_plugin(0) {
-}
-
-void arith_util::init_plugin() {
- SASSERT(m_plugin == 0);
- m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(m_afid));
-}
-
-bool arith_util::is_numeral(expr const * n, rational & val, bool & is_int) const {
+bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int) const {
if (!is_app_of(n, m_afid, OP_NUM))
return false;
func_decl * decl = to_app(n)->get_decl();
@@ -593,6 +582,17 @@ bool arith_util::is_numeral(expr const * n, rational & val, bool & is_int) const
return true;
}
+arith_util::arith_util(ast_manager & m):
+ arith_recognizers(m.get_family_id("arith")),
+ m_manager(m),
+ m_plugin(0) {
+}
+
+void arith_util::init_plugin() {
+ SASSERT(m_plugin == 0);
+ m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(m_afid));
+}
+
bool arith_util::is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val) {
if (!is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM))
return false;
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index c39768d4c..e63e866c3 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -187,36 +187,24 @@ public:
virtual void set_cancel(bool f);
};
-class arith_util {
- ast_manager & m_manager;
+/**
+ \brief Procedures for recognizing arithmetic expressions.
+ We don't need access to ast_manager, and operations can be simultaneously
+ executed in different threads.
+*/
+class arith_recognizers {
+protected:
family_id m_afid;
- arith_decl_plugin * m_plugin;
-
- void init_plugin();
-
- arith_decl_plugin & plugin() const {
- if (!m_plugin) const_cast<arith_util*>(this)->init_plugin();
- SASSERT(m_plugin != 0);
- return *m_plugin;
- }
-
public:
- arith_util(ast_manager & m);
+ arith_recognizers(family_id id):m_afid(id) {}
- ast_manager & get_manager() const { return m_manager; }
family_id get_family_id() const { return m_afid; }
- algebraic_numbers::manager & am() {
- return plugin().am();
- }
-
bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == m_afid; }
+ bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
bool is_numeral(expr const * n, rational & val, bool & is_int) const;
bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); }
bool is_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_NUM); }
- bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
- bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val);
- algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
bool is_zero(expr const * n) const { rational val; return is_numeral(n, val) && val.is_zero(); }
bool is_minus_one(expr * n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
// return true if \c n is a term of the form (* -1 r)
@@ -227,6 +215,7 @@ public:
}
return false;
}
+
bool is_le(expr const * n) const { return is_app_of(n, m_afid, OP_LE); }
bool is_ge(expr const * n) const { return is_app_of(n, m_afid, OP_GE); }
bool is_lt(expr const * n) const { return is_app_of(n, m_afid, OP_LT); }
@@ -245,14 +234,13 @@ public:
bool is_power(expr const * n) const { return is_app_of(n, m_afid, OP_POWER); }
bool is_int(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); }
- bool is_int(expr const * n) const { return is_int(m_manager.get_sort(n)); }
+ bool is_int(expr const * n) const { return is_int(get_sort(n)); }
bool is_real(sort const * s) const { return is_sort_of(s, m_afid, REAL_SORT); }
- bool is_real(expr const * n) const { return is_real(m_manager.get_sort(n)); }
+ bool is_real(expr const * n) const { return is_real(get_sort(n)); }
bool is_int_real(sort const * s) const { return s->get_family_id() == m_afid; }
- bool is_int_real(expr const * n) const { return is_int_real(m_manager.get_sort(n)); }
+ bool is_int_real(expr const * n) const { return is_int_real(get_sort(n)); }
MATCH_UNARY(is_uminus);
-
MATCH_BINARY(is_sub);
MATCH_BINARY(is_add);
MATCH_BINARY(is_mul);
@@ -265,6 +253,34 @@ public:
MATCH_BINARY(is_div);
MATCH_BINARY(is_idiv);
+ bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
+ bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
+};
+
+class arith_util : public arith_recognizers {
+ ast_manager & m_manager;
+ arith_decl_plugin * m_plugin;
+
+ void init_plugin();
+
+ arith_decl_plugin & plugin() const {
+ if (!m_plugin) const_cast<arith_util*>(this)->init_plugin();
+ SASSERT(m_plugin != 0);
+ return *m_plugin;
+ }
+
+public:
+ arith_util(ast_manager & m);
+
+ ast_manager & get_manager() const { return m_manager; }
+
+ algebraic_numbers::manager & am() {
+ return plugin().am();
+ }
+
+ bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
+ bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val);
+ algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); }
sort * mk_real() { return m_manager.mk_sort(m_afid, REAL_SORT); }
@@ -320,9 +336,6 @@ public:
app * mk_acosh(expr * arg) { return m_manager.mk_app(m_afid, OP_ACOSH, arg); }
app * mk_atanh(expr * arg) { return m_manager.mk_app(m_afid, OP_ATANH, arg); }
- bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
- bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
-
app * mk_pi() { return plugin().mk_pi(); }
app * mk_e() { return plugin().mk_e(); }
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 3fb422a2e..94637bbdd 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -374,6 +374,31 @@ quantifier::quantifier(bool forall, unsigned num_decls, sort * const * decl_sort
memcpy(const_cast<expr **>(get_no_patterns()), no_patterns, sizeof(expr *) * num_no_patterns);
}
+// -----------------------------------
+//
+// Auxiliary functions
+//
+// -----------------------------------
+
+sort * get_sort(expr const * n) {
+ while (true) {
+ switch(n->get_kind()) {
+ case AST_APP:
+ return to_app(n)->get_decl()->get_range();
+ case AST_VAR:
+ return to_var(n)->get_sort();
+ case AST_QUANTIFIER:
+ // The sort of the quantifier is the sort of the nested expression.
+ // This code assumes the given expression is well-sorted.
+ n = to_quantifier(n)->get_expr();
+ break;
+ default:
+ UNREACHABLE();
+ return 0;
+ }
+ }
+}
+
// -----------------------------------
//
// AST hash-consing
@@ -1495,20 +1520,6 @@ void ast_manager::register_plugin(family_id id, decl_plugin * plugin) {
plugin->set_manager(this, id);
}
-sort * ast_manager::get_sort(expr const * n) const {
- switch(n->get_kind()) {
- case AST_APP:
- return to_app(n)->get_decl()->get_range();
- case AST_VAR:
- return to_var(n)->get_sort();
- case AST_QUANTIFIER:
- return m_bool_sort;
- default:
- UNREACHABLE();
- return 0;
- }
-}
-
bool ast_manager::is_bool(expr const * n) const {
return get_sort(n) == m_bool_sort;
}
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 6af95e3a7..f899ed241 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1287,6 +1287,8 @@ inline bool has_labels(expr const * n) {
else return false;
}
+sort * get_sort(expr const * n);
+
// -----------------------------------
//
// Get Some Value functor
@@ -1548,7 +1550,7 @@ protected:
}
public:
- sort * get_sort(expr const * n) const;
+ sort * get_sort(expr const * n) const { return ::get_sort(n); }
void check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const;
void check_sorts_core(ast const * n) const;
bool check_sorts(ast const * n) const;
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index fd15ca681..434bdaa11 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -41,26 +41,6 @@ bv_decl_plugin::bv_decl_plugin():
m_int_sort(0) {
}
-void bv_decl_plugin::mk_table_upto(unsigned n) {
- if (m_powers.empty()) {
- m_powers.push_back(rational(1));
- }
- unsigned sz = m_powers.size();
- rational curr = m_powers[sz - 1];
- rational two(2);
- for (unsigned i = sz; i <= n; i++) {
- curr *= two;
- m_powers.push_back(curr);
- }
-}
-
-rational bv_decl_plugin::power_of_two(unsigned n) const {
- if (n >= m_powers.size()) {
- const_cast<bv_decl_plugin*>(this)->mk_table_upto(n + 1);
- }
- return m_powers[n];
-}
-
void bv_decl_plugin::set_manager(ast_manager * m, family_id id) {
decl_plugin::set_manager(m, id);
@@ -169,7 +149,7 @@ void bv_decl_plugin::mk_bv_sort(unsigned bv_size) {
sz = sort_size::mk_very_big();
}
else {
- sz = sort_size(power_of_two(bv_size));
+ sz = sort_size(rational::power_of_two(bv_size));
}
m_bv_sorts[bv_size] = m_manager->mk_sort(symbol("bv"), sort_info(m_family_id, BV_SORT, sz, 1, &p));
m_manager->inc_ref(m_bv_sorts[bv_size]);
@@ -436,7 +416,7 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
// This cannot be enforced now, since some Z3 modules try to generate these invalid numerals.
// After SMT-COMP, I should find all offending modules.
// For now, I will just simplify the numeral here.
- parameter p0(mod(parameters[0].get_rational(), power_of_two(bv_size)));
+ parameter p0(mod(parameters[0].get_rational(), rational::power_of_two(bv_size)));
parameter ps[2] = { p0, parameters[1] };
sort * bv = get_bv_sort(bv_size);
return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps));
@@ -621,7 +601,7 @@ void bv_decl_plugin::get_offset_term(app * a, expr * & t, rational & offset) con
offset = decl->get_parameter(0).get_rational();
sz = decl->get_parameter(1).get_int();
t = a->get_arg(1);
- offset = mod(offset, power_of_two(sz));
+ offset = mod(offset, rational::power_of_two(sz));
}
else {
t = a;
@@ -729,37 +709,104 @@ expr * bv_decl_plugin::get_some_value(sort * s) {
return m_manager->mk_app(m_family_id, OP_BV_NUM, 2, p, 0, 0);
}
-bv_util::bv_util(ast_manager & m):
- m_manager(m) {
- SASSERT(m.has_plugin(symbol("bv")));
- m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.get_family_id("bv")));
-}
-
-rational bv_util::norm(rational const & val, unsigned bv_size, bool is_signed) const {
- rational r = mod(val, power_of_two(bv_size));
+rational bv_recognizers::norm(rational const & val, unsigned bv_size, bool is_signed) const {
+ rational r = mod(val, rational::power_of_two(bv_size));
SASSERT(!r.is_neg());
if (is_signed) {
- if (r >= power_of_two(bv_size - 1)) {
- r -= power_of_two(bv_size);
+ if (r >= rational::power_of_two(bv_size - 1)) {
+ r -= rational::power_of_two(bv_size);
}
- if (r < -power_of_two(bv_size - 1)) {
- r += power_of_two(bv_size);
+ if (r < -rational::power_of_two(bv_size - 1)) {
+ r += rational::power_of_two(bv_size);
}
}
return r;
}
-bool bv_util::has_sign_bit(rational const & n, unsigned bv_size) const {
+bool bv_recognizers::has_sign_bit(rational const & n, unsigned bv_size) const {
SASSERT(bv_size > 0);
rational m = norm(n, bv_size, false);
- rational p = power_of_two(bv_size - 1);
+ rational p = rational::power_of_two(bv_size - 1);
return m >= p;
}
-bool bv_util::is_bv_sort(sort const * s) const {
+bool bv_recognizers::is_bv_sort(sort const * s) const {
return (s->get_family_id() == get_fid() && s->get_decl_kind() == BV_SORT && s->get_num_parameters() == 1);
}
+bool bv_recognizers::is_numeral(expr const * n, rational & val, unsigned & bv_size) const {
+ if (!is_app_of(n, get_fid(), OP_BV_NUM)) {
+ return false;
+ }
+ func_decl * decl = to_app(n)->get_decl();
+ val = decl->get_parameter(0).get_rational();
+ bv_size = decl->get_parameter(1).get_int();
+ return true;
+}
+
+bool bv_recognizers::is_allone(expr const * e) const {
+ rational r;
+ unsigned bv_size;
+ if (!is_numeral(e, r, bv_size)) {
+ return false;
+ }
+ bool result = (r == rational::power_of_two(bv_size) - rational(1));
+ TRACE("is_allone", tout << r << " " << result << "\n";);
+ return result;
+}
+
+bool bv_recognizers::is_zero(expr const * n) const {
+ if (!is_app_of(n, get_fid(), OP_BV_NUM)) {
+ return false;
+ }
+ func_decl * decl = to_app(n)->get_decl();
+ return decl->get_parameter(0).get_rational().is_zero();
+}
+
+bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) {
+ if (!is_extract(e)) return false;
+ low = get_extract_low(e);
+ high = get_extract_high(e);
+ b = to_app(e)->get_arg(0);
+ return true;
+}
+
+bool bv_recognizers::is_bv2int(expr const* e, expr*& r) {
+ if (!is_bv2int(e)) return false;
+ r = to_app(e)->get_arg(0);
+ return true;
+}
+
+bool bv_recognizers::mult_inverse(rational const & n, unsigned bv_size, rational & result) {
+ if (n.is_one()) {
+ result = n;
+ return true;
+ }
+
+ if (!mod(n, rational(2)).is_one()) {
+ return false;
+ }
+
+ rational g;
+ rational x;
+ rational y;
+ g = gcd(n, rational::power_of_two(bv_size), x, y);
+ if (x.is_neg()) {
+ x = mod(x, rational::power_of_two(bv_size));
+ }
+ SASSERT(x.is_pos());
+ SASSERT(mod(x * n, rational::power_of_two(bv_size)).is_one());
+ result = x;
+ return true;
+}
+
+bv_util::bv_util(ast_manager & m):
+ bv_recognizers(m.get_family_id(symbol("bv"))),
+ m_manager(m) {
+ SASSERT(m.has_plugin(symbol("bv")));
+ m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.get_family_id("bv")));
+}
+
app * bv_util::mk_numeral(rational const & val, sort* s) {
if (!is_bv_sort(s)) {
return 0;
@@ -774,65 +821,11 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) {
return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, 0);
}
-bool bv_util::is_numeral(expr const * n, rational & val, unsigned & bv_size) const {
- if (!is_app_of(n, get_fid(), OP_BV_NUM)) {
- return false;
- }
- func_decl * decl = to_app(n)->get_decl();
- val = decl->get_parameter(0).get_rational();
- bv_size = decl->get_parameter(1).get_int();
- return true;
-}
-
-
-bool bv_util::is_allone(expr const * e) const {
- rational r;
- unsigned bv_size;
- if (!is_numeral(e, r, bv_size)) {
- return false;
- }
- bool result = (r == power_of_two(bv_size) - rational(1));
- TRACE("is_allone", tout << r << " " << result << "\n";);
- return result;
-}
-
-bool bv_util::is_zero(expr const * n) const {
- if (!is_app_of(n, get_fid(), OP_BV_NUM)) {
- return false;
- }
- func_decl * decl = to_app(n)->get_decl();
- return decl->get_parameter(0).get_rational().is_zero();
-}
-
sort * bv_util::mk_sort(unsigned bv_size) {
parameter p[1] = { parameter(bv_size) };
return m_manager.mk_sort(get_fid(), BV_SORT, 1, p);
}
-
-bool bv_util::mult_inverse(rational const & n, unsigned bv_size, rational & result) {
- if (n.is_one()) {
- result = n;
- return true;
- }
-
- if (!mod(n, rational(2)).is_one()) {
- return false;
- }
-
- rational g;
- rational x;
- rational y;
- g = gcd(n, power_of_two(bv_size), x, y);
- if (x.is_neg()) {
- x = mod(x, power_of_two(bv_size));
- }
- SASSERT(x.is_pos());
- SASSERT(mod(x * n, power_of_two(bv_size)).is_one());
- result = x;
- return true;
-}
-
app * bv_util::mk_bv2int(expr* e) {
sort* s = m_manager.mk_sort(m_manager.get_family_id("arith"), INT_SORT);
parameter p(s);
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index 34f2baf6b..8ea90f844 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -127,9 +127,6 @@ inline func_decl * get_div0_decl(ast_manager & m, func_decl * decl) {
class bv_decl_plugin : public decl_plugin {
protected:
- vector<rational> m_powers;
- void mk_table_upto(unsigned n);
-
symbol m_bv_sym;
symbol m_concat_sym;
symbol m_sign_extend_sym;
@@ -245,8 +242,6 @@ protected:
public:
bv_decl_plugin();
- rational power_of_two(unsigned n) const;
-
virtual ~bv_decl_plugin() {}
virtual void finalize();
@@ -273,7 +268,70 @@ public:
virtual expr * get_some_value(sort * s);
};
-class bv_util {
+class bv_recognizers {
+ family_id m_afid;
+public:
+ bv_recognizers(family_id fid):m_afid(fid) {}
+
+ family_id get_fid() const { return m_afid; }
+ family_id get_family_id() const { return get_fid(); }
+
+ bool is_numeral(expr const * n, rational & val, unsigned & bv_size) const;
+ bool is_numeral(expr const * n) const { return is_app_of(n, get_fid(), OP_BV_NUM); }
+ bool is_allone(expr const * e) const;
+ bool is_zero(expr const * e) const;
+ bool is_bv_sort(sort const * s) const;
+ bool is_bv(expr const* e) const { return is_bv_sort(get_sort(e)); }
+
+ bool is_concat(expr const * e) const { return is_app_of(e, get_fid(), OP_CONCAT); }
+ bool is_extract(func_decl const * f) const { return is_decl_of(f, get_fid(), OP_EXTRACT); }
+ bool is_extract(expr const * e) const { return is_app_of(e, get_fid(), OP_EXTRACT); }
+ unsigned get_extract_high(func_decl const * f) const { return f->get_parameter(0).get_int(); }
+ unsigned get_extract_low(func_decl const * f) const { return f->get_parameter(1).get_int(); }
+ unsigned get_extract_high(expr const * n) { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); }
+ unsigned get_extract_low(expr const * n) { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); }
+ bool is_extract(expr const * e, unsigned & low, unsigned & high, expr * & b);
+ bool is_bv2int(expr const * e, expr * & r);
+ bool is_bv_add(expr const * e) const { return is_app_of(e, get_fid(), OP_BADD); }
+ bool is_bv_sub(expr const * e) const { return is_app_of(e, get_fid(), OP_BSUB); }
+ bool is_bv_mul(expr const * e) const { return is_app_of(e, get_fid(), OP_BMUL); }
+ bool is_bv_neg(expr const * e) const { return is_app_of(e, get_fid(), OP_BNEG); }
+ bool is_bv_sdiv(expr const * e) const { return is_app_of(e, get_fid(), OP_BSDIV); }
+ bool is_bv_udiv(expr const * e) const { return is_app_of(e, get_fid(), OP_BUDIV); }
+ bool is_bv_srem(expr const * e) const { return is_app_of(e, get_fid(), OP_BSREM); }
+ bool is_bv_urem(expr const * e) const { return is_app_of(e, get_fid(), OP_BUREM); }
+ bool is_bv_smod(expr const * e) const { return is_app_of(e, get_fid(), OP_BSMOD); }
+ bool is_bv_and(expr const * e) const { return is_app_of(e, get_fid(), OP_BAND); }
+ bool is_bv_or(expr const * e) const { return is_app_of(e, get_fid(), OP_BOR); }
+ bool is_bv_xor(expr const * e) const { return is_app_of(e, get_fid(), OP_BXOR); }
+ bool is_bv_nand(expr const * e) const { return is_app_of(e, get_fid(), OP_BNAND); }
+ bool is_bv_nor(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOR); }
+ 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_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); }
+ bool is_mkbv(expr const * e) const { return is_app_of(e, get_fid(), OP_MKBV); }
+ bool is_bv_ashr(expr const * e) const { return is_app_of(e, get_fid(), OP_BASHR); }
+ bool is_bv_lshr(expr const * e) const { return is_app_of(e, get_fid(), OP_BLSHR); }
+ bool is_bv_shl(expr const * e) const { return is_app_of(e, get_fid(), OP_BSHL); }
+ bool is_sign_ext(expr const * e) const { return is_app_of(e, get_fid(), OP_SIGN_EXT); }
+
+ MATCH_BINARY(is_bv_add);
+ MATCH_BINARY(is_bv_mul);
+ MATCH_BINARY(is_bv_sle);
+ MATCH_BINARY(is_bv_ule);
+ MATCH_BINARY(is_bv_shl);
+
+ rational norm(rational const & val, unsigned bv_size, bool is_signed) const ;
+ rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); }
+ bool has_sign_bit(rational const & n, unsigned bv_size) const;
+ bool mult_inverse(rational const & n, unsigned bv_size, rational & result);
+
+};
+
+class bv_util : public bv_recognizers {
ast_manager & m_manager;
bv_decl_plugin * m_plugin;
@@ -282,29 +340,10 @@ public:
ast_manager & get_manager() const { return m_manager; }
- family_id get_fid() const { return m_plugin->get_family_id(); }
-
- family_id get_family_id() const { return get_fid(); }
-
- rational power_of_two(unsigned n) const { return m_plugin->power_of_two(n); }
-
- rational norm(rational const & val, unsigned bv_size, bool is_signed) const ;
- rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); }
- bool has_sign_bit(rational const & n, unsigned bv_size) const;
app * mk_numeral(rational const & val, sort* s);
app * mk_numeral(rational const & val, unsigned bv_size);
app * mk_numeral(uint64 u, unsigned bv_size) { return mk_numeral(rational(u, rational::ui64()), bv_size); }
sort * mk_sort(unsigned bv_size);
- bool is_numeral(expr const * n, rational & val, unsigned & bv_size) const;
- bool is_numeral(expr const * n) const {
- return is_app_of(n, get_fid(), OP_BV_NUM);
- }
- bool is_allone(expr const * e) const;
- bool is_zero(expr const * e) const;
- bool is_bv_sort(sort const * s) const;
- bool is_bv(expr const* e) const {
- return is_bv_sort(m_manager.get_sort(e));
- }
unsigned get_bv_size(sort const * s) const {
SASSERT(is_bv_sort(s));
@@ -348,59 +387,6 @@ public:
app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); }
app * mk_bv(unsigned n, expr* const* es) { return m_manager.mk_app(get_fid(), OP_MKBV, n, es); }
-
- bool is_concat(expr const * e) const { return is_app_of(e, get_fid(), OP_CONCAT); }
- bool is_extract(func_decl const * f) const { return is_decl_of(f, get_fid(), OP_EXTRACT); }
- bool is_extract(expr const * e) const { return is_app_of(e, get_fid(), OP_EXTRACT); }
- unsigned get_extract_high(func_decl const * f) const { return f->get_parameter(0).get_int(); }
- unsigned get_extract_low(func_decl const * f) const { return f->get_parameter(1).get_int(); }
- unsigned get_extract_high(expr const * n) { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); }
- unsigned get_extract_low(expr const * n) { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); }
- bool is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) {
- if (!is_extract(e)) return false;
- low = get_extract_low(e);
- high = get_extract_high(e);
- b = to_app(e)->get_arg(0);
- return true;
- }
- bool is_bv2int(expr const* e, expr*& r) {
- if (!is_bv2int(e)) return false;
- r = to_app(e)->get_arg(0);
- return true;
- }
- bool is_bv_add(expr const * e) const { return is_app_of(e, get_fid(), OP_BADD); }
- bool is_bv_sub(expr const * e) const { return is_app_of(e, get_fid(), OP_BSUB); }
- bool is_bv_mul(expr const * e) const { return is_app_of(e, get_fid(), OP_BMUL); }
- bool is_bv_neg(expr const * e) const { return is_app_of(e, get_fid(), OP_BNEG); }
- bool is_bv_sdiv(expr const * e) const { return is_app_of(e, get_fid(), OP_BSDIV); }
- bool is_bv_udiv(expr const * e) const { return is_app_of(e, get_fid(), OP_BUDIV); }
- bool is_bv_srem(expr const * e) const { return is_app_of(e, get_fid(), OP_BSREM); }
- bool is_bv_urem(expr const * e) const { return is_app_of(e, get_fid(), OP_BUREM); }
- bool is_bv_smod(expr const * e) const { return is_app_of(e, get_fid(), OP_BSMOD); }
- bool is_bv_and(expr const * e) const { return is_app_of(e, get_fid(), OP_BAND); }
- bool is_bv_or(expr const * e) const { return is_app_of(e, get_fid(), OP_BOR); }
- bool is_bv_xor(expr const * e) const { return is_app_of(e, get_fid(), OP_BXOR); }
- bool is_bv_nand(expr const * e) const { return is_app_of(e, get_fid(), OP_BNAND); }
- bool is_bv_nor(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOR); }
- 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_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); }
- bool is_mkbv(expr const * e) const { return is_app_of(e, get_fid(), OP_MKBV); }
- bool is_bv_ashr(expr const * e) const { return is_app_of(e, get_fid(), OP_BASHR); }
- bool is_bv_lshr(expr const * e) const { return is_app_of(e, get_fid(), OP_BLSHR); }
- bool is_bv_shl(expr const * e) const { return is_app_of(e, get_fid(), OP_BSHL); }
- bool is_sign_ext(expr const * e) const { return is_app_of(e, get_fid(), OP_SIGN_EXT); }
-
- MATCH_BINARY(is_bv_add);
- MATCH_BINARY(is_bv_mul);
- MATCH_BINARY(is_bv_sle);
- MATCH_BINARY(is_bv_ule);
- MATCH_BINARY(is_bv_shl);
-
- bool mult_inverse(rational const & n, unsigned bv_size, rational & result);
};
#endif /* _BV_DECL_PLUGIN_H_ */
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.h b/src/ast/rewriter/bit_blaster/bit_blaster.h
index 42444aebc..7b317c6cb 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster.h
@@ -36,7 +36,7 @@ public:
bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, basic_simplifier_plugin & _s);
ast_manager & m() const { return m_util.get_manager(); }
- numeral power(unsigned n) const { return m_util.power_of_two(n); }
+ numeral power(unsigned n) const { return rational::power_of_two(n); }
void mk_xor(expr * a, expr * b, expr_ref & r) { s.mk_xor(a, b, r); }
void mk_xor3(expr * a, expr * b, expr * c, expr_ref & r);
void mk_carry(expr * a, expr * b, expr * c, expr_ref & r);
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index 1fd83e91f..80d319377 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -32,7 +32,7 @@ struct blaster_cfg {
blaster_cfg(bool_rewriter & r, bv_util & u):m_rewriter(r), m_util(u) {}
ast_manager & m() const { return m_util.get_manager(); }
- numeral power(unsigned n) const { return m_util.power_of_two(n); }
+ numeral power(unsigned n) const { return rational::power_of_two(n); }
void mk_xor(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_xor(a, b, r); }
void mk_xor3(expr * a, expr * b, expr * c, expr_ref & r) {
expr_ref tmp(m());
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 5fd562676..f8ff27337 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -283,12 +283,12 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
if (is_num1 || is_num2) {
if (is_signed) {
- lower = - m_util.power_of_two(sz - 1);
- upper = m_util.power_of_two(sz - 1) - numeral(1);
+ lower = - rational::power_of_two(sz - 1);
+ upper = rational::power_of_two(sz - 1) - numeral(1);
}
else {
lower = numeral(0);
- upper = m_util.power_of_two(sz) - numeral(1);
+ upper = rational::power_of_two(sz) - numeral(1);
}
}
@@ -387,14 +387,14 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
if (is_numeral(arg, v, sz)) {
sz = high - low + 1;
if (v.is_neg())
- mod(v, m_util.power_of_two(sz), v);
+ mod(v, rational::power_of_two(sz), v);
if (v.is_uint64()) {
uint64 u = v.get_uint64();
uint64 e = shift_right(u, low) & (shift_left(1ull, sz) - 1ull);
result = mk_numeral(numeral(e, numeral::ui64()), sz);
return BR_DONE;
}
- div(v, m_util.power_of_two(low), v);
+ div(v, rational::power_of_two(low), v);
result = mk_numeral(v, sz);
return BR_DONE;
}
@@ -519,7 +519,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
SASSERT(r2 < numeral(bv_size));
SASSERT(r2.is_unsigned());
- r1 = m_util.norm(r1 * m_util.power_of_two(r2.get_unsigned()), bv_size);
+ r1 = m_util.norm(r1 * rational::power_of_two(r2.get_unsigned()), bv_size);
result = mk_numeral(r1, bv_size);
return BR_DONE;
}
@@ -567,7 +567,7 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) {
SASSERT(r2.is_unsigned());
unsigned sh = r2.get_unsigned();
- div(r1, m_util.power_of_two(sh), r1);
+ div(r1, rational::power_of_two(sh), r1);
result = mk_numeral(r1, bv_size);
return BR_DONE;
}
@@ -626,7 +626,7 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) {
if (is_num1 && is_num2 && numeral(bv_size) <= r2) {
if (m_util.has_sign_bit(r1, bv_size))
- result = mk_numeral(m_util.power_of_two(bv_size) - numeral(1), bv_size);
+ result = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size);
else
result = mk_numeral(0, bv_size);
return BR_DONE;
@@ -635,7 +635,7 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) {
if (is_num1 && is_num2) {
SASSERT(r2 < numeral(bv_size));
bool sign = m_util.has_sign_bit(r1, bv_size);
- div(r1, m_util.power_of_two(r2.get_unsigned()), r1);
+ div(r1, rational::power_of_two(r2.get_unsigned()), r1);
if (sign) {
// pad ones.
numeral p(1);
@@ -697,7 +697,7 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e
// The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff)
result = m().mk_ite(m().mk_app(get_fid(), OP_SLT, arg1, mk_numeral(0, bv_size)),
mk_numeral(1, bv_size),
- mk_numeral(m_util.power_of_two(bv_size) - numeral(1), bv_size));
+ mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size));
return BR_REWRITE2;
}
}
@@ -746,7 +746,7 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
}
else {
// The "hardware interpretation" for (bvudiv x 0) is #xffff
- result = mk_numeral(m_util.power_of_two(bv_size) - numeral(1), bv_size);
+ result = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size);
return BR_DONE;
}
@@ -845,7 +845,7 @@ bool bv_rewriter::is_minus_one_core(expr * arg) const {
numeral r;
unsigned bv_size;
if (is_numeral(arg, r, bv_size)) {
- return r == (m_util.power_of_two(bv_size) - numeral(1));
+ return r == (rational::power_of_two(bv_size) - numeral(1));
}
return false;
}
@@ -924,7 +924,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
if (is_x_minus_one(arg1, x) && x == arg2) {
bv_size = get_bv_size(arg1);
expr * x_minus_1 = arg1;
- expr * minus_one = mk_numeral(m_util.power_of_two(bv_size) - numeral(1), bv_size);
+ expr * minus_one = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size);
result = m().mk_ite(m().mk_eq(x, mk_numeral(0, bv_size)),
m().mk_app(get_fid(), OP_BUREM0, minus_one),
x_minus_1);
@@ -1068,7 +1068,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
if (i > 0)
prev = new_args.back();
if (is_numeral(arg, v1, sz1) && prev != 0 && is_numeral(prev, v2, sz2)) {
- v2 *= m_util.power_of_two(sz1);
+ v2 *= rational::power_of_two(sz1);
v2 += v1;
new_args.pop_back();
new_args.push_back(mk_numeral(v2, sz1+sz2));
@@ -1137,7 +1137,7 @@ br_status bv_rewriter::mk_sign_extend(unsigned n, expr * arg, expr_ref & result)
if (is_numeral(arg, r, bv_size)) {
unsigned result_bv_size = bv_size + n;
r = m_util.norm(r, bv_size, true);
- mod(r, m_util.power_of_two(result_bv_size), r);
+ mod(r, rational::power_of_two(result_bv_size), r);
result = mk_numeral(r, result_bv_size);
return BR_DONE;
}
@@ -1213,7 +1213,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
if (m_util.is_bv_not(arg)) {
expr * atom = to_app(arg)->get_arg(0);
if (pos_args.is_marked(atom)) {
- result = mk_numeral(m_util.power_of_two(sz) - numeral(1), sz);
+ result = mk_numeral(rational::power_of_two(sz) - numeral(1), sz);
return BR_DONE;
}
else if (neg_args.is_marked(atom)) {
@@ -1229,7 +1229,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
continue;
}
else if (neg_args.is_marked(arg)) {
- result = mk_numeral(m_util.power_of_two(sz) - numeral(1), sz);
+ result = mk_numeral(rational::power_of_two(sz) - numeral(1), sz);
return BR_DONE;
}
pos_args.mark(arg, true);
@@ -1237,7 +1237,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
}
}
- if (v1 == m_util.power_of_two(sz) - numeral(1)) {
+ if (v1 == rational::power_of_two(sz) - numeral(1)) {
result = mk_numeral(v1, sz);
return BR_DONE;
}
@@ -1294,7 +1294,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
}
if (i != low) {
unsigned num_sz = i - low;
- exs.push_back(m_util.mk_numeral(m_util.power_of_two(num_sz) - numeral(1), num_sz));
+ exs.push_back(m_util.mk_numeral(rational::power_of_two(num_sz) - numeral(1), num_sz));
low = i;
}
while (i < sz && mod(v1, two).is_zero()) {
@@ -1385,7 +1385,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
else if (pos_args.is_marked(atom)) {
pos_args.mark(atom, false);
merged = true;
- v1 = bitwise_xor(v1, m_util.power_of_two(sz) - numeral(1));
+ v1 = bitwise_xor(v1, rational::power_of_two(sz) - numeral(1));
}
else {
neg_args.mark(atom, true);
@@ -1399,7 +1399,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
else if (neg_args.is_marked(arg)) {
neg_args.mark(arg, false);
merged = true;
- v1 = bitwise_xor(v1, m_util.power_of_two(sz) - numeral(1));
+ v1 = bitwise_xor(v1, rational::power_of_two(sz) - numeral(1));
}
else {
pos_args.mark(arg, true);
@@ -1455,7 +1455,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
return BR_REWRITE3;
}
- if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (m_util.power_of_two(sz) - numeral(1)))))
+ if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (rational::power_of_two(sz) - numeral(1)))))
return BR_FAILED;
ptr_buffer<expr> new_args;
@@ -1611,7 +1611,7 @@ br_status bv_rewriter::mk_bv_redand(expr * arg, expr_ref & result) {
numeral r;
unsigned bv_size;
if (is_numeral(arg, r, bv_size)) {
- result = (r == m_util.power_of_two(bv_size) - numeral(1)) ? mk_numeral(1, 1) : mk_numeral(0, 1);
+ result = (r == rational::power_of_two(bv_size) - numeral(1)) ? mk_numeral(1, 1) : mk_numeral(0, 1);
return BR_DONE;
}
return BR_FAILED;
@@ -1707,7 +1707,7 @@ bool bv_rewriter::is_zero_bit(expr * x, unsigned idx) {
if (is_numeral(x, val, bv_size)) {
if (val.is_zero())
return true;
- div(val, m_util.power_of_two(idx), val);
+ div(val, rational::power_of_two(idx), val);
return (val % numeral(2)).is_zero();
}
if (m_util.is_concat(x)) {
diff --git a/src/ast/simplifier/bv_simplifier_plugin.cpp b/src/ast/simplifier/bv_simplifier_plugin.cpp
index 2da1f3bab..3ef55baba 100644
--- a/src/ast/simplifier/bv_simplifier_plugin.cpp
+++ b/src/ast/simplifier/bv_simplifier_plugin.cpp
@@ -76,9 +76,9 @@ app * bv_simplifier_plugin::mk_numeral(numeral const & n) {
}
app * bv_simplifier_plugin::mk_numeral(numeral const& n, unsigned bv_size) {
- numeral r = mod(n, m_util.power_of_two(bv_size));
+ numeral r = mod(n, rational::power_of_two(bv_size));
SASSERT(!r.is_neg());
- SASSERT(r < m_util.power_of_two(bv_size));
+ SASSERT(r < rational::power_of_two(bv_size));
return m_util.mk_numeral(r, bv_size);
}
@@ -225,7 +225,7 @@ inline uint64 bv_simplifier_plugin::to_uint64(const numeral & n, unsigned bv_siz
SASSERT(bv_size <= 64);
numeral tmp = n;
if (tmp.is_neg()) {
- tmp = mod(tmp, m_util.power_of_two(bv_size));
+ tmp = mod(tmp, rational::power_of_two(bv_size));
}
SASSERT(tmp.is_nonneg());
SASSERT(tmp.is_uint64());
@@ -235,7 +235,7 @@ inline uint64 bv_simplifier_plugin::to_uint64(const numeral & n, unsigned bv_siz
#define MK_BV_OP(_oper_,_binop_) \
rational bv_simplifier_plugin::mk_bv_ ## _oper_(numeral const& a0, numeral const& b0, unsigned sz) { \
rational r(0), a(a0), b(b0); \
- numeral p64 = m_util.power_of_two(64); \
+ numeral p64 = rational::power_of_two(64); \
numeral mul(1); \
while (sz > 0) { \
numeral a1 = a % p64; \
@@ -260,7 +260,7 @@ MK_BV_OP(xor,^)
rational bv_simplifier_plugin::mk_bv_not(numeral const& a0, unsigned sz) {
rational r(0), a(a0), mul(1);
- numeral p64 = m_util.power_of_two(64);
+ numeral p64 = rational::power_of_two(64);
while (sz > 0) {
numeral a1 = a % p64;
uint64 u = ~a1.get_uint64();
@@ -320,12 +320,12 @@ void bv_simplifier_plugin::mk_leq_core(bool is_signed, expr * arg1, expr * arg2,
if (is_num1 || is_num2) {
if (is_signed) {
- lower = - m_util.power_of_two(bv_size - 1);
- upper = m_util.power_of_two(bv_size - 1) - numeral(1);
+ lower = - rational::power_of_two(bv_size - 1);
+ upper = rational::power_of_two(bv_size - 1) - numeral(1);
}
else {
lower = numeral(0);
- upper = m_util.power_of_two(bv_size) - numeral(1);
+ upper = rational::power_of_two(bv_size) - numeral(1);
}
}
@@ -509,7 +509,7 @@ bool bv_simplifier_plugin::try_mk_extract(unsigned high, unsigned low, expr * ar
if (m_util.is_numeral(a, r, num_bits)) {
if (r.is_neg()) {
- r = mod(r, m_util.power_of_two(sz));
+ r = mod(r, rational::power_of_two(sz));
}
SASSERT(r.is_nonneg());
if (r.is_uint64()) {
@@ -520,7 +520,7 @@ bool bv_simplifier_plugin::try_mk_extract(unsigned high, unsigned low, expr * ar
result = mk_numeral(numeral(e, numeral::ui64()), sz);
return true;
}
- result = mk_numeral(div(r, m_util.power_of_two(low)), sz);
+ result = mk_numeral(div(r, rational::power_of_two(low)), sz);
return true;
}
// (extract[high:low] (extract[high2:low2] x)) == (extract[high+low2 : low+low2] x)
@@ -902,7 +902,7 @@ void bv_simplifier_plugin::mk_concat(unsigned num_args, expr * const * args, exp
--i;
expr * arg = args[i];
if (is_numeral(arg, arg_val)) {
- arg_val *= m_util.power_of_two(shift);
+ arg_val *= rational::power_of_two(shift);
val += arg_val;
shift += get_bv_size(arg);
TRACE("bv_simplifier_plugin",
@@ -1203,7 +1203,7 @@ bool bv_simplifier_plugin::is_minus_one_core(expr * arg) const {
unsigned bv_size;
if (m_util.is_numeral(arg, r, bv_size)) {
numeral minus_one(-1);
- minus_one = mod(minus_one, m_util.power_of_two(bv_size));
+ minus_one = mod(minus_one, rational::power_of_two(bv_size));
return r == minus_one;
}
return false;
@@ -1295,7 +1295,7 @@ void bv_simplifier_plugin::mk_sign_extend(unsigned n, expr * arg, expr_ref & res
if (m_util.is_numeral(arg, r, bv_size)) {
unsigned result_bv_size = bv_size + n;
r = norm(r, bv_size, true);
- r = mod(r, m_util.power_of_two(result_bv_size));
+ r = mod(r, rational::power_of_two(result_bv_size));
result = mk_numeral(r, result_bv_size);
TRACE("mk_sign_extend", tout << "n: " << n << "\n";
ast_ll_pp(tout, m_manager, arg); tout << "====>\n";
@@ -1373,7 +1373,7 @@ void bv_simplifier_plugin::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result
else if (is_num1 && is_num2) {
SASSERT(r2 < rational(bv_size));
SASSERT(r2.is_unsigned());
- result = mk_numeral(r1 * m_util.power_of_two(r2.get_unsigned()), bv_size);
+ result = mk_numeral(r1 * rational::power_of_two(r2.get_unsigned()), bv_size);
}
//
@@ -1423,7 +1423,7 @@ void bv_simplifier_plugin::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & resul
else if (is_num1 && is_num2) {
SASSERT(r2.is_unsigned());
unsigned sh = r2.get_unsigned();
- r1 = div(r1, m_util.power_of_two(sh));
+ r1 = div(r1, rational::power_of_two(sh));
result = mk_numeral(r1, bv_size);
}
//
@@ -1804,8 +1804,8 @@ void bv_simplifier_plugin::mk_bv_rotate_left_core(unsigned shift, numeral r, uns
result = mk_numeral(r, bv_size);
}
else {
- rational r1 = div(r, m_util.power_of_two(bv_size - shift)); // shift right
- rational r2 = (r * m_util.power_of_two(shift)) % m_util.power_of_two(bv_size); // shift left
+ rational r1 = div(r, rational::power_of_two(bv_size - shift)); // shift right
+ rational r2 = (r * rational::power_of_two(shift)) % rational::power_of_two(bv_size); // shift left
result = mk_numeral(r1 + r2, bv_size);
}
}
@@ -1831,8 +1831,8 @@ void bv_simplifier_plugin::mk_bv_rotate_right_core(unsigned shift, numeral r, un
result = mk_numeral(r, bv_size);
}
else {
- rational r1 = div(r, m_util.power_of_two(shift)); // shift right
- rational r2 = (r * m_util.power_of_two(bv_size - shift)) % m_util.power_of_two(bv_size); // shift left
+ rational r1 = div(r, rational::power_of_two(shift)); // shift right
+ rational r2 = (r * rational::power_of_two(bv_size - shift)) % rational::power_of_two(bv_size); // shift left
result = mk_numeral(r1 + r2, bv_size);
}
}
@@ -1935,7 +1935,7 @@ void bv_simplifier_plugin::mk_bv_ashr(expr* arg1, expr* arg2, expr_ref& result)
else if (is_num1 && is_num2) {
SASSERT(r2 < rational(bv_size));
bool sign = has_sign_bit(r1, bv_size);
- r1 = div(r1, m_util.power_of_two(r2.get_unsigned()));
+ r1 = div(r1, rational::power_of_two(r2.get_unsigned()));
if (sign) {
// pad ones.
rational p(1);
diff --git a/src/ast/simplifier/bv_simplifier_plugin.h b/src/ast/simplifier/bv_simplifier_plugin.h
index 7f66566b6..36e773de0 100644
--- a/src/ast/simplifier/bv_simplifier_plugin.h
+++ b/src/ast/simplifier/bv_simplifier_plugin.h
@@ -172,7 +172,7 @@ public:
app * mk_numeral(rational const & n, unsigned bv_size);
app * mk_numeral(uint64 n, unsigned bv_size) { return mk_numeral(numeral(n, numeral::ui64()), bv_size); }
app* mk_bv0(unsigned bv_size) { return m_util.mk_numeral(numeral(0), bv_size); }
- rational mk_allone(unsigned bv_size) { return m_util.power_of_two(bv_size) - numeral(1); }
+ rational mk_allone(unsigned bv_size) { return rational::power_of_two(bv_size) - numeral(1); }
bool is_minus_one_core(expr * arg) const;
bool is_x_minus_one(expr * arg, expr * & x);
void mk_int2bv(expr * arg, sort* range, expr_ref & result);
diff --git a/src/tactic/arith/bv2int_rewriter.cpp b/src/tactic/arith/bv2int_rewriter.cpp
index 0965f36f2..872981283 100644
--- a/src/tactic/arith/bv2int_rewriter.cpp
+++ b/src/tactic/arith/bv2int_rewriter.cpp
@@ -544,7 +544,7 @@ bool bv2int_rewriter::is_sbv2int(expr* n, expr_ref& s) {
m_bv.is_extract(e2, lo1, hi1, e3) &&
lo1 == 0 && hi1 == hi-1 &&
m_arith.is_numeral(t2, k, is_int) && is_int &&
- k == m_bv.power_of_two(hi)
+ k == rational::power_of_two(hi)
) {
s = e3;
return true;
diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index 188ea7d70..bd5af58f2 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -253,7 +253,7 @@ class nla2bv_tactic : public tactic {
s_bv = m_arith.mk_sub(m_arith.mk_numeral(*up, true), s_bv);
}
else {
- s_bv = m_arith.mk_sub(s_bv, m_arith.mk_numeral(m_bv.power_of_two(num_bits-1), true));
+ s_bv = m_arith.mk_sub(s_bv, m_arith.mk_numeral(rational::power_of_two(num_bits-1), true));
}
m_trail.push_back(s_bv);
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index 8790ca5a7..83a949579 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -583,7 +583,7 @@ private:
return false; // size must be even
// I implemented only the easy (and very common) case, where a_i = 2^{n-i-1} and c = 2^n - 1
unsigned n = sz/2;
- if (c != m_bv_util.power_of_two(n) - numeral(1))
+ if (c != rational::power_of_two(n) - numeral(1))
return false;
for (unsigned i = 0; i < n; i++) {
monomial const & m1 = p[i*2];
@@ -592,7 +592,7 @@ private:
return false;
if (m1.m_a != m2.m_a)
return false;
- if (m1.m_a != m_bv_util.power_of_two(n - i - 1))
+ if (m1.m_a != rational::power_of_two(n - i - 1))
return false;
}
return true;
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index d1dca296a..00e14a41f 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -647,9 +647,9 @@ class elim_uncnstr_tactic : public tactic {
unsigned bv_sz = m_bv_util.get_bv_size(arg1);
rational MAX;
if (is_signed)
- MAX = m_bv_util.power_of_two(bv_sz - 1) - rational(1);
+ MAX = rational::power_of_two(bv_sz - 1) - rational(1);
else
- MAX = m_bv_util.power_of_two(bv_sz) - rational(1);
+ MAX = rational::power_of_two(bv_sz) - rational(1);
app * u;
bool is_new = mk_fresh_uncnstr_var_for(f, arg1, arg2, u);
app * r = m().mk_or(u, m().mk_eq(t, m_bv_util.mk_numeral(MAX, bv_sz)));
@@ -666,7 +666,7 @@ class elim_uncnstr_tactic : public tactic {
unsigned bv_sz = m_bv_util.get_bv_size(arg1);
rational MIN;
if (is_signed)
- MIN = -m_bv_util.power_of_two(bv_sz - 1);
+ MIN = -rational::power_of_two(bv_sz - 1);
else
MIN = rational(0);
app * u;
diff --git a/src/util/rational.cpp b/src/util/rational.cpp
index 0a91bd8da..122db7217 100644
--- a/src/util/rational.cpp
+++ b/src/util/rational.cpp
@@ -27,6 +27,31 @@ synch_mpq_manager * rational::g_mpq_manager = 0;
rational rational::m_zero(0);
rational rational::m_one(1);
rational rational::m_minus_one(-1);
+vector<rational> rational::m_powers_of_two;
+
+void mk_power_up_to(vector<rational> & pws, unsigned n) {
+ if (pws.empty()) {
+ pws.push_back(rational(1));
+ }
+ unsigned sz = pws.size();
+ rational curr = pws[sz - 1];
+ rational two(2);
+ for (unsigned i = sz; i <= n; i++) {
+ curr *= two;
+ pws.push_back(curr);
+ }
+}
+
+rational rational::power_of_two(unsigned k) {
+ rational result;
+ #pragma omp critical (powers_of_two)
+ {
+ if (k >= m_powers_of_two.size())
+ mk_power_up_to(m_powers_of_two, k+1);
+ result = m_powers_of_two[k];
+ }
+ return result;
+}
void rational::initialize() {
if (!g_mpq_manager) {
@@ -35,6 +60,7 @@ void rational::initialize() {
}
void rational::finalize() {
+ m_powers_of_two.finalize();
dealloc(g_mpq_manager);
g_mpq_manager = 0;
}
diff --git a/src/util/rational.h b/src/util/rational.h
index f0406f30a..fc03228bf 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -26,14 +26,13 @@ class rational {
static rational m_zero;
static rational m_one;
static rational m_minus_one;
-
+ static vector<rational> m_powers_of_two;
static synch_mpq_manager * g_mpq_manager;
-
+
static synch_mpq_manager & m() { return *g_mpq_manager; }
public:
static void initialize();
-
static void finalize();
/*
ADD_INITIALIZER('rational::initialize();')
@@ -272,6 +271,8 @@ public:
return result;
}
+ static rational power_of_two(unsigned k);
+
bool is_power_of_two(unsigned & shift) {
return m().is_power_of_two(m_val, shift);
}