mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-02-06 16:14:07 +00:00
commit fc1f37efc9
8 changed files with 528 additions and 485 deletions
Download patch file Download diff file Expand all files Collapse all files

5
scripts/mk_util.py
View file

@ -596,7 +596,7 @@ def display_help(exit_code):
else: else:
print(" --parallel=num use cl option /MP with 'num' parallel processes") print(" --parallel=num use cl option /MP with 'num' parallel processes")
print(" --pypkgdir=<dir> Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR) print(" --pypkgdir=<dir> Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR)
print(" -b <sudir>, --build=<subdir> subdirectory where Z3 will be built (default: build).") print(" -b <subdir>, --build=<subdir> subdirectory where Z3 will be built (default: %s)." % BUILD_DIR)
print(" --githash=hash include the given hash in the binaries.") print(" --githash=hash include the given hash in the binaries.")
print(" -d, --debug compile Z3 in debug mode.") print(" -d, --debug compile Z3 in debug mode.")
print(" -t, --trace enable tracing in release mode.") print(" -t, --trace enable tracing in release mode.")
@ -742,7 +742,8 @@ def extract_c_includes(fname):
# Given a path dir1/subdir2/subdir3 returns ../../.. # Given a path dir1/subdir2/subdir3 returns ../../..
def reverse_path(p): def reverse_path(p):
l = p.split(os.sep) # Filter out empty components (e.g. will have one if path ends in a slash)
l = list(filter(lambda x: len(x) > 0, p.split(os.sep)))
n = len(l) n = len(l)
r = '..' r = '..'
for i in range(1, n): for i in range(1, n):

55
src/ast/arith_decl_plugin.h
View file

@ -115,7 +115,7 @@ protected:
func_decl * m_i_div_decl; func_decl * m_i_div_decl;
func_decl * m_i_mod_decl; func_decl * m_i_mod_decl;
func_decl * m_i_rem_decl; func_decl * m_i_rem_decl;
func_decl * m_to_real_decl; func_decl * m_to_real_decl;
func_decl * m_to_int_decl; func_decl * m_to_int_decl;
func_decl * m_is_int_decl; func_decl * m_is_int_decl;
@ -140,7 +140,7 @@ protected:
app * m_pi; app * m_pi;
app * m_e; app * m_e;
app * m_0_pw_0_int; app * m_0_pw_0_int;
app * m_0_pw_0_real; app * m_0_pw_0_real;
func_decl * m_neg_root_decl; func_decl * m_neg_root_decl;
@ -149,7 +149,7 @@ protected:
func_decl * m_mod_0_decl; func_decl * m_mod_0_decl;
func_decl * m_u_asin_decl; func_decl * m_u_asin_decl;
func_decl * m_u_acos_decl; func_decl * m_u_acos_decl;
ptr_vector<app> m_small_ints; ptr_vector<app> m_small_ints;
ptr_vector<app> m_small_reals; ptr_vector<app> m_small_reals;
@ -175,11 +175,11 @@ public:
} }
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range); unsigned arity, sort * const * domain, sort * range);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range); unsigned num_args, expr * const * args, sort * range);
virtual bool is_value(app * e) const; virtual bool is_value(app * e) const;
@ -202,15 +202,34 @@ public:
app * mk_numeral(sexpr const * p, unsigned i); app * mk_numeral(sexpr const * p, unsigned i);
app * mk_pi() const { return m_pi; } app * mk_pi() const { return m_pi; }
app * mk_e() const { return m_e; } app * mk_e() const { return m_e; }
app * mk_0_pw_0_int() const { return m_0_pw_0_int; } app * mk_0_pw_0_int() const { return m_0_pw_0_int; }
app * mk_0_pw_0_real() const { return m_0_pw_0_real; } app * mk_0_pw_0_real() const { return m_0_pw_0_real; }
virtual expr * get_some_value(sort * s); virtual expr * get_some_value(sort * s);
virtual bool is_considered_uninterpreted(func_decl * f) {
if (f->get_family_id() != get_family_id())
return false;
switch (f->get_decl_kind())
{
case OP_0_PW_0_INT:
case OP_0_PW_0_REAL:
case OP_NEG_ROOT:
case OP_DIV_0:
case OP_IDIV_0:
case OP_MOD_0:
case OP_U_ASIN:
case OP_U_ACOS:
return true;
default:
return false;
}
return false;
}
}; };
/** /**
@ -258,7 +277,7 @@ public:
bool is_to_int(expr const * n) const { return is_app_of(n, m_afid, OP_TO_INT); } bool is_to_int(expr const * n) const { return is_app_of(n, m_afid, OP_TO_INT); }
bool is_is_int(expr const * n) const { return is_app_of(n, m_afid, OP_IS_INT); } bool is_is_int(expr const * n) const { return is_app_of(n, m_afid, OP_IS_INT); }
bool is_power(expr const * n) const { return is_app_of(n, m_afid, OP_POWER); } 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(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); }
bool is_int(expr const * n) const { return is_int(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(sort const * s) const { return is_sort_of(s, m_afid, REAL_SORT); }
@ -275,7 +294,7 @@ public:
MATCH_BINARY(is_le); MATCH_BINARY(is_le);
MATCH_BINARY(is_ge); MATCH_BINARY(is_ge);
MATCH_BINARY(is_lt); MATCH_BINARY(is_lt);
MATCH_BINARY(is_gt); MATCH_BINARY(is_gt);
MATCH_BINARY(is_mod); MATCH_BINARY(is_mod);
MATCH_BINARY(is_rem); MATCH_BINARY(is_rem);
MATCH_BINARY(is_div); MATCH_BINARY(is_div);
@ -297,25 +316,25 @@ class arith_util : public arith_recognizers {
SASSERT(m_plugin != 0); SASSERT(m_plugin != 0);
return *m_plugin; return *m_plugin;
} }
public: public:
arith_util(ast_manager & m); arith_util(ast_manager & m);
ast_manager & get_manager() const { return m_manager; } ast_manager & get_manager() const { return m_manager; }
algebraic_numbers::manager & am() { algebraic_numbers::manager & am() {
return plugin().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) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val); bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val);
algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n); 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_int() { return m_manager.mk_sort(m_afid, INT_SORT); }
sort * mk_real() { return m_manager.mk_sort(m_afid, REAL_SORT); } sort * mk_real() { return m_manager.mk_sort(m_afid, REAL_SORT); }
app * mk_numeral(rational const & val, bool is_int) const { app * mk_numeral(rational const & val, bool is_int) const {
return plugin().mk_numeral(val, is_int); return plugin().mk_numeral(val, is_int);
} }
app * mk_numeral(rational const & val, sort const * s) const { app * mk_numeral(rational const & val, sort const * s) const {
SASSERT(is_int(s) || is_real(s)); SASSERT(is_int(s) || is_real(s));
@ -379,9 +398,9 @@ public:
app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); } app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); }
app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); } app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); }
app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); } app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); }
/** /**
\brief Return the equality (= lhs rhs), but it makes sure that \brief Return the equality (= lhs rhs), but it makes sure that
if one of the arguments is a numeral, then it will be in the right-hand-side; if one of the arguments is a numeral, then it will be in the right-hand-side;
if none of them are numerals, then the left-hand-side has a smaller id than the right hand side. if none of them are numerals, then the left-hand-side has a smaller id than the right hand side.
*/ */

492
src/ast/ast.h
View file

File diff suppressed because it is too large Load diff

67
src/ast/bv_decl_plugin.h
View file

@ -33,7 +33,7 @@ enum bv_op_kind {
OP_BADD, OP_BADD,
OP_BSUB, OP_BSUB,
OP_BMUL, OP_BMUL,
OP_BSDIV, OP_BSDIV,
OP_BUDIV, OP_BUDIV,
OP_BSREM, OP_BSREM,
@ -41,20 +41,20 @@ enum bv_op_kind {
OP_BSMOD, OP_BSMOD,
// special functions to record the division by 0 cases // special functions to record the division by 0 cases
// these are internal functions // these are internal functions
OP_BSDIV0, OP_BSDIV0,
OP_BUDIV0, OP_BUDIV0,
OP_BSREM0, OP_BSREM0,
OP_BUREM0, OP_BUREM0,
OP_BSMOD0, OP_BSMOD0,
// special functions where division by 0 has a fixed interpretation. // special functions where division by 0 has a fixed interpretation.
OP_BSDIV_I, OP_BSDIV_I,
OP_BUDIV_I, OP_BUDIV_I,
OP_BSREM_I, OP_BSREM_I,
OP_BUREM_I, OP_BUREM_I,
OP_BSMOD_I, OP_BSMOD_I,
OP_ULEQ, OP_ULEQ,
OP_SLEQ, OP_SLEQ,
OP_UGEQ, OP_UGEQ,
@ -95,7 +95,7 @@ enum bv_op_kind {
OP_BSMUL_NO_UDFL, // no signed multiplication underflow predicate OP_BSMUL_NO_UDFL, // no signed multiplication underflow predicate
OP_BIT2BOOL, // predicate OP_BIT2BOOL, // predicate
OP_MKBV, // bools to bv OP_MKBV, // bools to bv
OP_INT2BV, OP_INT2BV,
OP_BV2INT, OP_BV2INT,
@ -176,7 +176,7 @@ protected:
ptr_vector<func_decl> m_bv_slt; ptr_vector<func_decl> m_bv_slt;
ptr_vector<func_decl> m_bv_ugt; ptr_vector<func_decl> m_bv_ugt;
ptr_vector<func_decl> m_bv_sgt; ptr_vector<func_decl> m_bv_sgt;
ptr_vector<func_decl> m_bv_and; ptr_vector<func_decl> m_bv_and;
ptr_vector<func_decl> m_bv_or; ptr_vector<func_decl> m_bv_or;
ptr_vector<func_decl> m_bv_not; ptr_vector<func_decl> m_bv_not;
@ -184,7 +184,7 @@ protected:
ptr_vector<func_decl> m_bv_nand; ptr_vector<func_decl> m_bv_nand;
ptr_vector<func_decl> m_bv_nor; ptr_vector<func_decl> m_bv_nor;
ptr_vector<func_decl> m_bv_xnor; ptr_vector<func_decl> m_bv_xnor;
ptr_vector<func_decl> m_bv_redor; ptr_vector<func_decl> m_bv_redor;
ptr_vector<func_decl> m_bv_redand; ptr_vector<func_decl> m_bv_redand;
ptr_vector<func_decl> m_bv_comp; ptr_vector<func_decl> m_bv_comp;
@ -203,7 +203,7 @@ protected:
ptr_vector<func_decl> m_int2bv; ptr_vector<func_decl> m_int2bv;
vector<ptr_vector<func_decl> > m_bit2bool; vector<ptr_vector<func_decl> > m_bit2bool;
ptr_vector<func_decl> m_mkbv; ptr_vector<func_decl> m_mkbv;
virtual void set_manager(ast_manager * m, family_id id); virtual void set_manager(ast_manager * m, family_id id);
void mk_bv_sort(unsigned bv_size); void mk_bv_sort(unsigned bv_size);
sort * get_bv_sort(unsigned bv_size); sort * get_bv_sort(unsigned bv_size);
@ -218,9 +218,9 @@ protected:
bool get_bv_size(sort * t, int & result); bool get_bv_size(sort * t, int & result);
bool get_bv_size(expr * t, int & result); bool get_bv_size(expr * t, int & result);
bool get_concat_size(unsigned arity, sort * const * domain, int & result); bool get_concat_size(unsigned arity, sort * const * domain, int & result);
bool get_extend_size(unsigned num_parameters, parameter const * parameters, bool get_extend_size(unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, int & result); unsigned arity, sort * const * domain, int & result);
bool get_extract_size(unsigned num_parameters, parameter const * parameters, bool get_extract_size(unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, int & result); unsigned arity, sort * const * domain, int & result);
func_decl * mk_bv2int(unsigned bv_size, unsigned num_parameters, parameter const * parameters, func_decl * mk_bv2int(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
@ -229,13 +229,13 @@ protected:
func_decl * mk_int2bv(unsigned bv_size, unsigned num_parameters, parameter const * parameters, func_decl * mk_int2bv(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain); unsigned arity, sort * const * domain);
func_decl * mk_bit2bool(unsigned bv_size, unsigned num_parameters, parameter const * parameters, func_decl * mk_bit2bool(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain); unsigned arity, sort * const * domain);
func_decl * mk_mkbv(unsigned arity, sort * const * domain); func_decl * mk_mkbv(unsigned arity, sort * const * domain);
bool get_int2bv_size(unsigned num_parameters, parameter const * parameters, int & result); bool get_int2bv_size(unsigned num_parameters, parameter const * parameters, int & result);
func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity); func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity);
void get_offset_term(app * a, expr * & t, rational & offset) const; void get_offset_term(app * a, expr * & t, rational & offset) const;
@ -248,24 +248,40 @@ public:
virtual decl_plugin * mk_fresh() { return alloc(bv_decl_plugin); } virtual decl_plugin * mk_fresh() { return alloc(bv_decl_plugin); }
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range); unsigned arity, sort * const * domain, sort * range);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range); unsigned num_args, expr * const * args, sort * range);
virtual bool is_value(app * e) const; virtual bool is_value(app * e) const;
virtual bool is_unique_value(app * e) const { return is_value(e); } virtual bool is_unique_value(app * e) const { return is_value(e); }
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic); virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic); virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
virtual bool are_distinct(app* a, app* b) const; virtual bool are_distinct(app* a, app* b) const;
virtual expr * get_some_value(sort * s); virtual expr * get_some_value(sort * s);
virtual bool is_considered_uninterpreted(func_decl * f) {
if (f->get_family_id() != get_family_id())
return false;
switch (f->get_decl_kind()) {
case OP_BSDIV0:
case OP_BUDIV0:
case OP_BSREM0:
case OP_BUREM0:
case OP_BSMOD0:
return true;
default:
return false;
}
return false;
}
}; };
class bv_recognizers { class bv_recognizers {
@ -282,7 +298,7 @@ public:
bool is_zero(expr const * e) const; bool is_zero(expr const * e) const;
bool is_bv_sort(sort const * s) 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_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_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(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); } bool is_extract(expr const * e) const { return is_app_of(e, get_fid(), OP_EXTRACT); }
@ -353,7 +369,6 @@ public:
rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); } 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 has_sign_bit(rational const & n, unsigned bv_size) const;
bool mult_inverse(rational const & n, unsigned bv_size, rational & result); bool mult_inverse(rational const & n, unsigned bv_size, rational & result);
}; };
class bv_util : public bv_recognizers { class bv_util : public bv_recognizers {
@ -369,8 +384,8 @@ public:
app * mk_numeral(rational const & val, unsigned bv_size); 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); } app * mk_numeral(uint64 u, unsigned bv_size) { return mk_numeral(rational(u, rational::ui64()), bv_size); }
sort * mk_sort(unsigned bv_size); sort * mk_sort(unsigned bv_size);
unsigned get_bv_size(sort const * s) const { unsigned get_bv_size(sort const * s) const {
SASSERT(is_bv_sort(s)); SASSERT(is_bv_sort(s));
return static_cast<unsigned>(s->get_parameter(0).get_int()); return static_cast<unsigned>(s->get_parameter(0).get_int());
} }
@ -393,11 +408,11 @@ public:
app * mk_bv_add(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); } app * mk_bv_add(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); }
app * mk_bv_sub(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); } app * mk_bv_sub(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); }
app * mk_bv_mul(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); } app * mk_bv_mul(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); }
app * mk_zero_extend(unsigned n, expr* e) { app * mk_zero_extend(unsigned n, expr* e) {
parameter p(n); parameter p(n);
return m_manager.mk_app(get_fid(), OP_ZERO_EXT, 1, &p, 1, &e); return m_manager.mk_app(get_fid(), OP_ZERO_EXT, 1, &p, 1, &e);
} }
app * mk_sign_extend(unsigned n, expr* e) { app * mk_sign_extend(unsigned n, expr* e) {
parameter p(n); parameter p(n);
return m_manager.mk_app(get_fid(), OP_SIGN_EXT, 1, &p, 1, &e); return m_manager.mk_app(get_fid(), OP_SIGN_EXT, 1, &p, 1, &e);
} }
@ -413,6 +428,6 @@ public:
app * mk_bv(unsigned n, expr* const* es) { return m_manager.mk_app(get_fid(), OP_MKBV, n, es); } app * mk_bv(unsigned n, expr* const* es) { return m_manager.mk_app(get_fid(), OP_MKBV, n, es); }
}; };
#endif /* BV_DECL_PLUGIN_H_ */ #endif /* BV_DECL_PLUGIN_H_ */

354
src/ast/rewriter/bv_rewriter.cpp
View file

@ -78,91 +78,91 @@ void bv_rewriter::get_param_descrs(param_descrs & r) {
poly_rewriter<bv_rewriter_core>::get_param_descrs(r); poly_rewriter<bv_rewriter_core>::get_param_descrs(r);
bv_rewriter_params::collect_param_descrs(r); bv_rewriter_params::collect_param_descrs(r);
#ifndef _EXTERNAL_RELEASE #ifndef _EXTERNAL_RELEASE
r.insert("mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral"); r.insert("mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral");
#endif #endif
} }
br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(f->get_family_id() == get_fid()); SASSERT(f->get_family_id() == get_fid());
switch(f->get_decl_kind()) { switch(f->get_decl_kind()) {
case OP_BIT0: SASSERT(num_args == 0); result = m_util.mk_numeral(0, 1); return BR_DONE; case OP_BIT0: SASSERT(num_args == 0); result = m_util.mk_numeral(0, 1); return BR_DONE;
case OP_BIT1: SASSERT(num_args == 0); result = m_util.mk_numeral(1, 1); return BR_DONE; case OP_BIT1: SASSERT(num_args == 0); result = m_util.mk_numeral(1, 1); return BR_DONE;
case OP_ULEQ: case OP_ULEQ:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_ule(args[0], args[1], result); return mk_ule(args[0], args[1], result);
case OP_UGEQ: case OP_UGEQ:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_uge(args[0], args[1], result); return mk_uge(args[0], args[1], result);
case OP_ULT: case OP_ULT:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_ult(args[0], args[1], result); return mk_ult(args[0], args[1], result);
case OP_UGT: case OP_UGT:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_ult(args[1], args[0], result); return mk_ult(args[1], args[0], result);
case OP_SLEQ: case OP_SLEQ:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_sle(args[0], args[1], result); return mk_sle(args[0], args[1], result);
case OP_SGEQ: case OP_SGEQ:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_sge(args[0], args[1], result); return mk_sge(args[0], args[1], result);
case OP_SLT: case OP_SLT:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_slt(args[0], args[1], result); return mk_slt(args[0], args[1], result);
case OP_SGT: case OP_SGT:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_slt(args[1], args[0], result); return mk_slt(args[1], args[0], result);
case OP_BADD: case OP_BADD:
SASSERT(num_args > 0); SASSERT(num_args > 0);
return mk_bv_add(num_args, args, result); return mk_bv_add(num_args, args, result);
case OP_BMUL: case OP_BMUL:
SASSERT(num_args > 0); SASSERT(num_args > 0);
return mk_bv_mul(num_args, args, result); return mk_bv_mul(num_args, args, result);
case OP_BSUB: case OP_BSUB:
SASSERT(num_args > 0); SASSERT(num_args > 0);
return mk_sub(num_args, args, result); return mk_sub(num_args, args, result);
case OP_BNEG: case OP_BNEG:
SASSERT(num_args == 1); SASSERT(num_args == 1);
return mk_uminus(args[0], result); return mk_uminus(args[0], result);
case OP_BSHL: case OP_BSHL:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_shl(args[0], args[1], result); return mk_bv_shl(args[0], args[1], result);
case OP_BLSHR: case OP_BLSHR:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_lshr(args[0], args[1], result); return mk_bv_lshr(args[0], args[1], result);
case OP_BASHR: case OP_BASHR:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_ashr(args[0], args[1], result); return mk_bv_ashr(args[0], args[1], result);
case OP_BSDIV: case OP_BSDIV:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_sdiv(args[0], args[1], result); return mk_bv_sdiv(args[0], args[1], result);
case OP_BUDIV: case OP_BUDIV:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_udiv(args[0], args[1], result); return mk_bv_udiv(args[0], args[1], result);
case OP_BSREM: case OP_BSREM:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_srem(args[0], args[1], result); return mk_bv_srem(args[0], args[1], result);
case OP_BUREM: case OP_BUREM:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_urem(args[0], args[1], result); return mk_bv_urem(args[0], args[1], result);
case OP_BSMOD: case OP_BSMOD:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_smod(args[0], args[1], result); return mk_bv_smod(args[0], args[1], result);
case OP_BSDIV_I: case OP_BSDIV_I:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_sdiv_i(args[0], args[1], result); return mk_bv_sdiv_i(args[0], args[1], result);
case OP_BUDIV_I: case OP_BUDIV_I:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_udiv_i(args[0], args[1], result); return mk_bv_udiv_i(args[0], args[1], result);
case OP_BSREM_I: case OP_BSREM_I:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_srem_i(args[0], args[1], result); return mk_bv_srem_i(args[0], args[1], result);
case OP_BUREM_I: case OP_BUREM_I:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_urem_i(args[0], args[1], result); return mk_bv_urem_i(args[0], args[1], result);
case OP_BSMOD_I: case OP_BSMOD_I:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_smod_i(args[0], args[1], result); return mk_bv_smod_i(args[0], args[1], result);
case OP_CONCAT: case OP_CONCAT:
return mk_concat(num_args, args, result); return mk_concat(num_args, args, result);
case OP_EXTRACT: case OP_EXTRACT:
@ -193,10 +193,10 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
case OP_BXNOR: case OP_BXNOR:
return mk_bv_xnor(num_args, args, result); return mk_bv_xnor(num_args, args, result);
case OP_ROTATE_LEFT: case OP_ROTATE_LEFT:
SASSERT(num_args == 1); SASSERT(num_args == 1);
return mk_bv_rotate_left(f->get_parameter(0).get_int(), args[0], result); return mk_bv_rotate_left(f->get_parameter(0).get_int(), args[0], result);
case OP_ROTATE_RIGHT: case OP_ROTATE_RIGHT:
SASSERT(num_args == 1); SASSERT(num_args == 1);
return mk_bv_rotate_right(f->get_parameter(0).get_int(), args[0], result); return mk_bv_rotate_right(f->get_parameter(0).get_int(), args[0], result);
case OP_EXT_ROTATE_LEFT: case OP_EXT_ROTATE_LEFT:
SASSERT(num_args == 2); SASSERT(num_args == 2);
@ -210,14 +210,14 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
case OP_INT2BV: case OP_INT2BV:
SASSERT(num_args == 1); SASSERT(num_args == 1);
return mk_int2bv(m_util.get_bv_size(f->get_range()), args[0], result); return mk_int2bv(m_util.get_bv_size(f->get_range()), args[0], result);
case OP_BREDOR: case OP_BREDOR:
SASSERT(num_args == 1); SASSERT(num_args == 1);
return mk_bv_redor(args[0], result); return mk_bv_redor(args[0], result);
case OP_BREDAND: case OP_BREDAND:
SASSERT(num_args == 1); SASSERT(num_args == 1);
return mk_bv_redand(args[0], result); return mk_bv_redand(args[0], result);
case OP_BCOMP: case OP_BCOMP:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_bv_comp(args[0], args[1], result); return mk_bv_comp(args[0], args[1], result);
case OP_MKBV: case OP_MKBV:
return mk_mkbv(num_args, args, result); return mk_mkbv(num_args, args, result);
@ -232,7 +232,7 @@ br_status bv_rewriter::mk_ule(expr * a, expr * b, expr_ref & result) {
br_status bv_rewriter::mk_uge(expr * a, expr * b, expr_ref & result) { br_status bv_rewriter::mk_uge(expr * a, expr * b, expr_ref & result) {
br_status st = mk_ule(b, a, result); br_status st = mk_ule(b, a, result);
if (st != BR_FAILED) if (st != BR_FAILED)
return st; return st;
result = m_util.mk_ule(b, a); result = m_util.mk_ule(b, a);
return BR_DONE; return BR_DONE;
@ -249,7 +249,7 @@ br_status bv_rewriter::mk_sle(expr * a, expr * b, expr_ref & result) {
br_status bv_rewriter::mk_sge(expr * a, expr * b, expr_ref & result) { br_status bv_rewriter::mk_sge(expr * a, expr * b, expr_ref & result) {
br_status st = mk_sle(b, a, result); br_status st = mk_sle(b, a, result);
if (st != BR_FAILED) if (st != BR_FAILED)
return st; return st;
result = m_util.mk_sle(b, a); result = m_util.mk_sle(b, a);
return BR_DONE; return BR_DONE;
@ -272,7 +272,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
return BR_DONE; return BR_DONE;
} }
if (is_num1) if (is_num1)
r1 = m_util.norm(r1, sz, is_signed); r1 = m_util.norm(r1, sz, is_signed);
if (is_num2) if (is_num2)
r2 = m_util.norm(r2, sz, is_signed); r2 = m_util.norm(r2, sz, is_signed);
@ -322,7 +322,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
#if 0 #if 0
if (!is_signed && m_util.is_concat(b) && to_app(b)->get_num_args() == 2 && m_util.is_zero(to_app(b)->get_arg(0))) { if (!is_signed && m_util.is_concat(b) && to_app(b)->get_num_args() == 2 && m_util.is_zero(to_app(b)->get_arg(0))) {
// //
// a <=_u (concat 0 c) ---> a[h:l] = 0 && a[l-1:0] <=_u c // a <=_u (concat 0 c) ---> a[h:l] = 0 && a[l-1:0] <=_u c
// //
expr * b_1 = to_app(b)->get_arg(0); expr * b_1 = to_app(b)->get_arg(0);
@ -337,9 +337,9 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
if (!is_signed) { if (!is_signed) {
// Extended version of the rule above using is_zero_bit. // Extended version of the rule above using is_zero_bit.
// It also catches examples atoms such as: // It also catches examples atoms such as:
// //
// a <=_u #x000f // a <=_u #x000f
// //
unsigned bv_sz = m_util.get_bv_size(b); unsigned bv_sz = m_util.get_bv_size(b);
unsigned i = bv_sz; unsigned i = bv_sz;
unsigned first_non_zero = UINT_MAX; unsigned first_non_zero = UINT_MAX;
@ -350,7 +350,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
break; break;
} }
} }
if (first_non_zero == UINT_MAX) { if (first_non_zero == UINT_MAX) {
// all bits are zero // all bits are zero
result = m().mk_eq(a, m_util.mk_numeral(numeral(0), bv_sz)); result = m().mk_eq(a, m_util.mk_numeral(numeral(0), bv_sz));
@ -361,7 +361,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
m_util.mk_ule(m_mk_extract(first_non_zero, 0, a), m_mk_extract(first_non_zero, 0, b))); m_util.mk_ule(m_mk_extract(first_non_zero, 0, a), m_mk_extract(first_non_zero, 0, b)));
return BR_REWRITE3; return BR_REWRITE3;
} }
} }
#endif #endif
@ -385,7 +385,7 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
result = arg; result = arg;
return BR_DONE; return BR_DONE;
} }
numeral v; numeral v;
if (is_numeral(arg, v, sz)) { if (is_numeral(arg, v, sz)) {
sz = high - low + 1; sz = high - low + 1;
@ -420,7 +420,7 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
if (idx > high) if (idx > high)
continue; continue;
// found first argument // found first argument
if (idx <= low) { if (idx <= low) {
// result is a fragment of this argument // result is a fragment of this argument
if (low == idx && high - idx == curr_sz - 1) { if (low == idx && high - idx == curr_sz - 1) {
result = curr; result = curr;
@ -486,13 +486,13 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
m_mk_extract(high, low, to_app(arg)->get_arg(2))); m_mk_extract(high, low, to_app(arg)->get_arg(2)));
return BR_REWRITE2; return BR_REWRITE2;
} }
return BR_FAILED; return BR_FAILED;
} }
br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
numeral r1, r2; numeral r1, r2;
unsigned bv_size = get_bv_size(arg1); unsigned bv_size = get_bv_size(arg1);
unsigned sz; unsigned sz;
if (is_numeral(arg2, r2, sz)) { if (is_numeral(arg2, r2, sz)) {
@ -501,9 +501,9 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
result = arg1; result = arg1;
return BR_DONE; return BR_DONE;
} }
if (r2 >= numeral(bv_size)) { if (r2 >= numeral(bv_size)) {
result = mk_numeral(0, bv_size); result = mk_numeral(0, bv_size);
return BR_DONE; return BR_DONE;
} }
@ -511,7 +511,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
if (bv_size <= 64) { if (bv_size <= 64) {
SASSERT(r1.is_uint64() && r2.is_uint64()); SASSERT(r1.is_uint64() && r2.is_uint64());
SASSERT(r2.get_uint64() < bv_size); SASSERT(r2.get_uint64() < bv_size);
uint64 r = shift_left(r1.get_uint64(), r2.get_uint64()); uint64 r = shift_left(r1.get_uint64(), r2.get_uint64());
numeral rn(r, numeral::ui64()); numeral rn(r, numeral::ui64());
rn = m_util.norm(rn, bv_size); rn = m_util.norm(rn, bv_size);
@ -519,7 +519,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
return BR_DONE; return BR_DONE;
} }
SASSERT(r2 < numeral(bv_size)); SASSERT(r2 < numeral(bv_size));
SASSERT(r2.is_unsigned()); SASSERT(r2.is_unsigned());
r1 = m_util.norm(r1 * rational::power_of_two(r2.get_unsigned()), bv_size); r1 = m_util.norm(r1 * rational::power_of_two(r2.get_unsigned()), bv_size);
@ -539,10 +539,10 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
return BR_FAILED; return BR_FAILED;
} }
br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) { br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) {
numeral r1, r2; numeral r1, r2;
unsigned bv_size = get_bv_size(arg1); unsigned bv_size = get_bv_size(arg1);
unsigned sz; unsigned sz;
if (is_numeral(arg2, r2, sz)) { if (is_numeral(arg2, r2, sz)) {
@ -551,15 +551,15 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) {
result = arg1; result = arg1;
return BR_DONE; return BR_DONE;
} }
if (r2 >= numeral(bv_size)) { if (r2 >= numeral(bv_size)) {
result = mk_numeral(0, bv_size); result = mk_numeral(0, bv_size);
return BR_DONE; return BR_DONE;
} }
if (is_numeral(arg1, r1, sz)) { if (is_numeral(arg1, r1, sz)) {
if (bv_size <= 64) { if (bv_size <= 64) {
SASSERT(r1.is_uint64()); SASSERT(r1.is_uint64());
SASSERT(r2.is_uint64()); SASSERT(r2.is_uint64());
uint64 r = shift_right(r1.get_uint64(), r2.get_uint64()); uint64 r = shift_right(r1.get_uint64(), r2.get_uint64());
numeral rn(r, numeral::ui64()); numeral rn(r, numeral::ui64());
@ -574,7 +574,7 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) {
result = mk_numeral(r1, bv_size); result = mk_numeral(r1, bv_size);
return BR_DONE; return BR_DONE;
} }
SASSERT(r2.is_pos()); SASSERT(r2.is_pos());
SASSERT(r2 < numeral(bv_size)); SASSERT(r2 < numeral(bv_size));
// (bvlshr x k) -> (concat bv0:k (extract [n-1:k] x)) // (bvlshr x k) -> (concat bv0:k (extract [n-1:k] x))
@ -652,13 +652,13 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) {
result = mk_numeral(r1, bv_size); result = mk_numeral(r1, bv_size);
return BR_DONE; return BR_DONE;
} }
// (bvashr (bvashr x r1) r2) --> (bvashr x r1+r2) // (bvashr (bvashr x r1) r2) --> (bvashr x r1+r2)
if (is_num2 && m_util.is_bv_ashr(arg1) && is_numeral(to_app(arg1)->get_arg(1), r1, bv_size)) { if (is_num2 && m_util.is_bv_ashr(arg1) && is_numeral(to_app(arg1)->get_arg(1), r1, bv_size)) {
r1 += r2; r1 += r2;
if (r1 > numeral(bv_size)) if (r1 > numeral(bv_size))
r1 = numeral(bv_size); r1 = numeral(bv_size);
result = m().mk_app(get_fid(), OP_BASHR, result = m().mk_app(get_fid(), OP_BASHR,
to_app(arg1)->get_arg(0), to_app(arg1)->get_arg(0),
mk_numeral(r1, bv_size)); mk_numeral(r1, bv_size));
return BR_REWRITE1; // not really needed at this time. return BR_REWRITE1; // not really needed at this time.
@ -694,7 +694,7 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e
if (r2.is_zero()) { if (r2.is_zero()) {
if (!hi_div0) { if (!hi_div0) {
result = m().mk_app(get_fid(), OP_BSDIV0, arg1); result = m().mk_app(get_fid(), OP_BSDIV0, arg1);
return BR_DONE; return BR_REWRITE1;
} }
else { else {
// The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff) // The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff)
@ -709,13 +709,13 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e
result = arg1; result = arg1;
return BR_DONE; return BR_DONE;
} }
if (!r2.is_zero() && is_numeral(arg1, r1, bv_size)) { if (!r2.is_zero() && is_numeral(arg1, r1, bv_size)) {
r1 = m_util.norm(r1, bv_size, true); r1 = m_util.norm(r1, bv_size, true);
result = mk_numeral(machine_div(r1, r2), bv_size); result = mk_numeral(machine_div(r1, r2), bv_size);
return BR_DONE; return BR_DONE;
} }
result = m().mk_app(get_fid(), OP_BSDIV_I, arg1, arg2); result = m().mk_app(get_fid(), OP_BSDIV_I, arg1, arg2);
return BR_DONE; return BR_DONE;
} }
@ -735,9 +735,9 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e
br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result) { br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result) {
numeral r1, r2; numeral r1, r2;
unsigned bv_size; unsigned bv_size;
TRACE("bv_udiv", tout << "hi_div0: " << hi_div0 << "\n";); TRACE("bv_udiv", tout << "hi_div0: " << hi_div0 << "\n";);
TRACE("udiv2mul", tout << mk_ismt2_pp(arg2, m()) << " udiv2mul: " << m_udiv2mul << "\n";); TRACE("udiv2mul", tout << mk_ismt2_pp(arg2, m()) << " udiv2mul: " << m_udiv2mul << "\n";);
if (is_numeral(arg2, r2, bv_size)) { if (is_numeral(arg2, r2, bv_size)) {
@ -745,13 +745,13 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
if (r2.is_zero()) { if (r2.is_zero()) {
if (!hi_div0) { if (!hi_div0) {
result = m().mk_app(get_fid(), OP_BUDIV0, arg1); result = m().mk_app(get_fid(), OP_BUDIV0, arg1);
return BR_DONE; return BR_REWRITE1;
} }
else { else {
// The "hardware interpretation" for (bvudiv x 0) is #xffff // The "hardware interpretation" for (bvudiv x 0) is #xffff
result = mk_numeral(rational::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; return BR_DONE;
} }
} }
@ -765,7 +765,7 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
result = mk_numeral(machine_div(r1, r2), bv_size); result = mk_numeral(machine_div(r1, r2), bv_size);
return BR_DONE; return BR_DONE;
} }
unsigned shift; unsigned shift;
if (r2.is_power_of_two(shift)) { if (r2.is_power_of_two(shift)) {
result = m().mk_app(get_fid(), OP_BLSHR, arg1, mk_numeral(shift, bv_size)); result = m().mk_app(get_fid(), OP_BLSHR, arg1, mk_numeral(shift, bv_size));
@ -808,7 +808,7 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e
if (r2.is_zero()) { if (r2.is_zero()) {
if (!hi_div0) { if (!hi_div0) {
result = m().mk_app(get_fid(), OP_BSREM0, arg1); result = m().mk_app(get_fid(), OP_BSREM0, arg1);
return BR_DONE; return BR_REWRITE1;
} }
else { else {
// The "hardware interpretation" for (bvsrem x 0) is x // The "hardware interpretation" for (bvsrem x 0) is x
@ -821,13 +821,13 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e
result = mk_numeral(0, bv_size); result = mk_numeral(0, bv_size);
return BR_DONE; return BR_DONE;
} }
if (!r2.is_zero() && is_numeral(arg1, r1, bv_size)) { if (!r2.is_zero() && is_numeral(arg1, r1, bv_size)) {
r1 = m_util.norm(r1, bv_size, true); r1 = m_util.norm(r1, bv_size, true);
result = mk_numeral(r1 % r2, bv_size); result = mk_numeral(r1 % r2, bv_size);
return BR_DONE; return BR_DONE;
} }
result = m().mk_app(get_fid(), OP_BSREM_I, arg1, arg2); result = m().mk_app(get_fid(), OP_BSREM_I, arg1, arg2);
return BR_DONE; return BR_DONE;
} }
@ -890,7 +890,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
result = mk_numeral(0, bv_size); result = mk_numeral(0, bv_size);
return BR_DONE; return BR_DONE;
} }
if (!r2.is_zero() && is_num1) { if (!r2.is_zero() && is_num1) {
r1 = m_util.norm(r1, bv_size); r1 = m_util.norm(r1, bv_size);
r1 %= r2; r1 %= r2;
@ -907,7 +907,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
result = m_util.mk_concat(2, args); result = m_util.mk_concat(2, args);
return BR_REWRITE2; return BR_REWRITE2;
} }
result = m().mk_app(get_fid(), OP_BUREM_I, arg1, arg2); result = m().mk_app(get_fid(), OP_BUREM_I, arg1, arg2);
return BR_DONE; return BR_DONE;
} }
@ -921,7 +921,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
zero); zero);
return BR_REWRITE2; return BR_REWRITE2;
} }
// urem(x - 1, x) ==> ite(x = 0, urem0(x-1), x - 1) ==> ite(x = 0, urem0(-1), x - 1) // urem(x - 1, x) ==> ite(x = 0, urem0(x-1), x - 1) ==> ite(x = 0, urem0(-1), x - 1)
expr * x; expr * x;
if (is_x_minus_one(arg1, x) && x == arg2) { if (is_x_minus_one(arg1, x) && x == arg2) {
@ -942,7 +942,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
result = zero; result = zero;
return BR_DONE; return BR_DONE;
} }
// urem(x - 1, x) --> x - 1 // urem(x - 1, x) --> x - 1
expr * x; expr * x;
if (is_x_minus_one(arg1, x) && x == arg2) { if (is_x_minus_one(arg1, x) && x == arg2) {
@ -986,7 +986,7 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e
result = arg1; result = arg1;
return BR_DONE; return BR_DONE;
} }
if (is_num1) { if (is_num1) {
numeral abs_r1 = m_util.norm(abs(r1), bv_size); numeral abs_r1 = m_util.norm(abs(r1), bv_size);
numeral abs_r2 = m_util.norm(abs(r2), bv_size); numeral abs_r2 = m_util.norm(abs(r2), bv_size);
@ -1012,7 +1012,7 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e
return BR_REWRITE2; return BR_REWRITE2;
} }
} }
if (hi_div0) { if (hi_div0) {
result = m().mk_app(get_fid(), OP_BSMOD_I, arg1, arg2); result = m().mk_app(get_fid(), OP_BSMOD_I, arg1, arg2);
return BR_DONE; return BR_DONE;
@ -1028,13 +1028,13 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e
br_status bv_rewriter::mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result) { br_status bv_rewriter::mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result) {
numeral val; numeral val;
bool is_int; bool is_int;
if (m_autil.is_numeral(arg, val, is_int)) { if (m_autil.is_numeral(arg, val, is_int)) {
val = m_util.norm(val, bv_size); val = m_util.norm(val, bv_size);
result = mk_numeral(val, bv_size); result = mk_numeral(val, bv_size);
return BR_DONE; return BR_DONE;
} }
// (int2bv (bv2int x)) --> x // (int2bv (bv2int x)) --> x
if (m_util.is_bv2int(arg) && bv_size == get_bv_size(to_app(arg)->get_arg(0))) { if (m_util.is_bv2int(arg) && bv_size == get_bv_size(to_app(arg)->get_arg(0))) {
result = to_app(arg)->get_arg(0); result = to_app(arg)->get_arg(0);
@ -1051,7 +1051,7 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) {
result = m_autil.mk_numeral(v, true); result = m_autil.mk_numeral(v, true);
return BR_DONE; return BR_DONE;
} }
// TODO: add other simplifications // TODO: add other simplifications
return BR_FAILED; return BR_FAILED;
@ -1068,7 +1068,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
expr * arg = args[i]; expr * arg = args[i];
expr * prev = 0; expr * prev = 0;
if (i > 0) if (i > 0)
prev = new_args.back(); prev = new_args.back();
if (is_numeral(arg, v1, sz1) && prev != 0 && is_numeral(prev, v2, sz2)) { if (is_numeral(arg, v1, sz1) && prev != 0 && is_numeral(prev, v2, sz2)) {
v2 *= rational::power_of_two(sz1); v2 *= rational::power_of_two(sz1);
@ -1084,7 +1084,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
} }
expanded = true; expanded = true;
} }
else if (m_util.is_extract(arg) && else if (m_util.is_extract(arg) &&
prev != 0 && prev != 0 &&
m_util.is_extract(prev) && m_util.is_extract(prev) &&
to_app(arg)->get_arg(0) == to_app(prev)->get_arg(0) && to_app(arg)->get_arg(0) == to_app(prev)->get_arg(0) &&
@ -1101,7 +1101,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
new_args.push_back(arg); new_args.push_back(arg);
} }
} }
if (!fused_numeral && !expanded && !fused_extract) if (!fused_numeral && !expanded && !fused_extract)
return BR_FAILED; return BR_FAILED;
SASSERT(!new_args.empty()); SASSERT(!new_args.empty());
if (new_args.size() == 1) { if (new_args.size() == 1) {
@ -1144,18 +1144,18 @@ br_status bv_rewriter::mk_sign_extend(unsigned n, expr * arg, expr_ref & result)
result = mk_numeral(r, result_bv_size); result = mk_numeral(r, result_bv_size);
return BR_DONE; return BR_DONE;
} }
if (m_elim_sign_ext) { if (m_elim_sign_ext) {
unsigned sz = get_bv_size(arg); unsigned sz = get_bv_size(arg);
expr * sign = m_mk_extract(sz-1, sz-1, arg); expr * sign = m_mk_extract(sz-1, sz-1, arg);
ptr_buffer<expr> args; ptr_buffer<expr> args;
for (unsigned i = 0; i < n; i++) for (unsigned i = 0; i < n; i++)
args.push_back(sign); args.push_back(sign);
args.push_back(arg); args.push_back(arg);
result = m_util.mk_concat(args.size(), args.c_ptr()); result = m_util.mk_concat(args.size(), args.c_ptr());
return BR_REWRITE2; return BR_REWRITE2;
} }
return BR_FAILED; return BR_FAILED;
} }
@ -1185,7 +1185,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
expr * arg = args[i]; expr * arg = args[i];
if (m_util.is_bv_or(arg)) { if (m_util.is_bv_or(arg)) {
unsigned num2 = to_app(arg)->get_num_args(); unsigned num2 = to_app(arg)->get_num_args();
for (unsigned j = 0; j < num2; j++) for (unsigned j = 0; j < num2; j++)
flat_args.push_back(to_app(arg)->get_arg(j)); flat_args.push_back(to_app(arg)->get_arg(j));
} }
else { else {
@ -1244,12 +1244,12 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
result = mk_numeral(v1, sz); result = mk_numeral(v1, sz);
return BR_DONE; return BR_DONE;
} }
// Simplifications of the form: // Simplifications of the form:
// (bvor (concat x #x00) (concat #x00 y)) --> (concat x y) // (bvor (concat x #x00) (concat #x00 y)) --> (concat x y)
if (new_args.size() == 2 && if (new_args.size() == 2 &&
num_coeffs == 0 && num_coeffs == 0 &&
m_util.is_concat(new_args[0]) && m_util.is_concat(new_args[0]) &&
m_util.is_concat(new_args[1])) { m_util.is_concat(new_args[1])) {
app * concat1 = to_app(new_args[0]); app * concat1 = to_app(new_args[0]);
app * concat2 = to_app(new_args[1]); app * concat2 = to_app(new_args[1]);
@ -1311,8 +1311,8 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
} }
std::reverse(exs.begin(), exs.end()); std::reverse(exs.begin(), exs.end());
result = m_util.mk_concat(exs.size(), exs.c_ptr()); result = m_util.mk_concat(exs.size(), exs.c_ptr());
TRACE("mask_bug", TRACE("mask_bug",
tout << "(assert (distinct (bvor (_ bv" << old_v1 << " " << sz << ")\n" << mk_ismt2_pp(t, m()) << ")\n"; tout << "(assert (distinct (bvor (_ bv" << old_v1 << " " << sz << ")\n" << mk_ismt2_pp(t, m()) << ")\n";
tout << mk_ismt2_pp(result, m()) << "))\n";); tout << mk_ismt2_pp(result, m()) << "))\n";);
return BR_REWRITE2; return BR_REWRITE2;
} }
@ -1324,7 +1324,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
if (!v1.is_zero()) { if (!v1.is_zero()) {
new_args.push_back(mk_numeral(v1, sz)); new_args.push_back(mk_numeral(v1, sz));
} }
switch (new_args.size()) { switch (new_args.size()) {
case 0: case 0:
result = mk_numeral(0, sz); result = mk_numeral(0, sz);
@ -1354,7 +1354,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
expr * arg = args[i]; expr * arg = args[i];
if (m_util.is_bv_xor(arg)) { if (m_util.is_bv_xor(arg)) {
unsigned num2 = to_app(arg)->get_num_args(); unsigned num2 = to_app(arg)->get_num_args();
for (unsigned j = 0; j < num2; j++) for (unsigned j = 0; j < num2; j++)
flat_args.push_back(to_app(arg)->get_arg(j)); flat_args.push_back(to_app(arg)->get_arg(j));
} }
else { else {
@ -1367,7 +1367,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
args = flat_args.c_ptr(); args = flat_args.c_ptr();
} }
} }
expr_fast_mark1 pos_args; expr_fast_mark1 pos_args;
expr_fast_mark2 neg_args; expr_fast_mark2 neg_args;
bool merged = false; bool merged = false;
@ -1380,7 +1380,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
num_coeffs++; num_coeffs++;
continue; continue;
} }
if (m_util.is_bv_not(arg)) { if (m_util.is_bv_not(arg)) {
expr * atom = to_app(arg)->get_arg(0); expr * atom = to_app(arg)->get_arg(0);
if (neg_args.is_marked(atom)) { if (neg_args.is_marked(atom)) {
@ -1411,14 +1411,14 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
} }
} }
} }
// XOR is a mask // XOR is a mask
// All arguments but one is a numeral. // All arguments but one is a numeral.
// //
// Apply a transformation of the form: // Apply a transformation of the form:
// //
// (bvxor a 0011) --> (concat ((_ extract 3 2) a) ((_ extract 1 0) (bvnot a))) // (bvxor a 0011) --> (concat ((_ extract 3 2) a) ((_ extract 1 0) (bvnot a)))
// //
if (!v1.is_zero() && num_coeffs == num - 1) { if (!v1.is_zero() && num_coeffs == num - 1) {
// find argument that is not a numeral // find argument that is not a numeral
expr * t = 0; expr * t = 0;
@ -1453,12 +1453,12 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
} }
} }
std::reverse(exs.c_ptr(), exs.c_ptr() + exs.size()); std::reverse(exs.c_ptr(), exs.c_ptr() + exs.size());
if (exs.size() == 1) if (exs.size() == 1)
result = exs[0]; result = exs[0];
else else
result = m_util.mk_concat(exs.size(), exs.c_ptr()); result = m_util.mk_concat(exs.size(), exs.c_ptr());
return BR_REWRITE3; return BR_REWRITE3;
} }
if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (rational::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)))) &&
(!m_bv_sort_ac || is_sorted(num, args))) (!m_bv_sort_ac || is_sorted(num, args)))
@ -1487,7 +1487,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
pos_args.mark(arg, false); pos_args.mark(arg, false);
} }
} }
switch (new_args.size()) { switch (new_args.size()) {
case 0: case 0:
result = mk_numeral(0, sz); result = mk_numeral(0, sz);
@ -1653,7 +1653,7 @@ br_status bv_rewriter::mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result) {
br_status bv_rewriter::mk_bv_add(unsigned num_args, expr * const * args, expr_ref & result) { br_status bv_rewriter::mk_bv_add(unsigned num_args, expr * const * args, expr_ref & result) {
br_status st = mk_add_core(num_args, args, result); br_status st = mk_add_core(num_args, args, result);
if (st != BR_FAILED && st != BR_DONE) if (st != BR_FAILED && st != BR_DONE)
return st; return st;
#if 0 #if 0
expr * x; expr * x;
@ -1673,14 +1673,14 @@ br_status bv_rewriter::mk_bv_add(unsigned num_args, expr * const * args, expr_re
return st; return st;
if (!m_util.is_concat(y) && !is_numeral(y)) if (!m_util.is_concat(y) && !is_numeral(y))
return st; return st;
unsigned sz = get_bv_size(x); unsigned sz = get_bv_size(x);
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
if (!is_zero_bit(x,i) && !is_zero_bit(y,i)) if (!is_zero_bit(x,i) && !is_zero_bit(y,i))
return st; return st;
} }
result = m().mk_app(get_fid(), OP_BOR, x, y); result = m().mk_app(get_fid(), OP_BOR, x, y);
return BR_REWRITE1; return BR_REWRITE1;
#else #else
@ -1747,7 +1747,7 @@ bool bv_rewriter::is_zero_bit(expr * x, unsigned idx) {
br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_ref & result) { br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_ref & result) {
br_status st = mk_mul_core(num_args, args, result); br_status st = mk_mul_core(num_args, args, result);
if (st != BR_FAILED && st != BR_DONE) if (st != BR_FAILED && st != BR_DONE)
return st; return st;
expr * x; expr * x;
expr * y; expr * y;
@ -1761,7 +1761,7 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re
else { else {
return st; return st;
} }
if (m_mul2concat) { if (m_mul2concat) {
numeral v; numeral v;
unsigned bv_size; unsigned bv_size;
@ -1810,12 +1810,12 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
result = m().mk_eq(to_app(lhs)->get_arg(0), mk_numeral(numeral(1) - v, 1)); result = m().mk_eq(to_app(lhs)->get_arg(0), mk_numeral(numeral(1) - v, 1));
return BR_REWRITE1; return BR_REWRITE1;
} }
bool is_one = v.is_one(); bool is_one = v.is_one();
expr_ref bit1(m()); expr_ref bit1(m());
bit1 = is_one ? rhs : mk_numeral(numeral(1), 1); bit1 = is_one ? rhs : mk_numeral(numeral(1), 1);
if (m_util.is_bv_or(lhs)) { if (m_util.is_bv_or(lhs)) {
ptr_buffer<expr> new_args; ptr_buffer<expr> new_args;
unsigned num = to_app(lhs)->get_num_args(); unsigned num = to_app(lhs)->get_num_args();
@ -1831,8 +1831,8 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
return BR_REWRITE3; return BR_REWRITE3;
} }
} }
if (m_util.is_bv_xor(lhs)) { if (m_util.is_bv_xor(lhs)) {
ptr_buffer<expr> new_args; ptr_buffer<expr> new_args;
unsigned num = to_app(lhs)->get_num_args(); unsigned num = to_app(lhs)->get_num_args();
@ -1849,7 +1849,7 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
return BR_REWRITE3; return BR_REWRITE3;
} }
} }
return BR_FAILED; return BR_FAILED;
} }
@ -1861,14 +1861,14 @@ br_status bv_rewriter::mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & resu
TRACE("blast_eq_value", tout << "sz: " << sz << "\n" << mk_ismt2_pp(lhs, m()) << "\n";); TRACE("blast_eq_value", tout << "sz: " << sz << "\n" << mk_ismt2_pp(lhs, m()) << "\n";);
if (is_numeral(lhs)) if (is_numeral(lhs))
std::swap(lhs, rhs); std::swap(lhs, rhs);
numeral v; numeral v;
if (!is_numeral(rhs, v, sz)) if (!is_numeral(rhs, v, sz))
return BR_FAILED; return BR_FAILED;
if (!m_util.is_bv_or(lhs) && !m_util.is_bv_xor(lhs) && !m_util.is_bv_not(lhs)) if (!m_util.is_bv_or(lhs) && !m_util.is_bv_xor(lhs) && !m_util.is_bv_not(lhs))
return BR_FAILED; return BR_FAILED;
numeral two(2); numeral two(2);
ptr_buffer<expr> new_args; ptr_buffer<expr> new_args;
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
@ -1888,7 +1888,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) {
if (m_util.is_concat(lhs)) { if (m_util.is_concat(lhs)) {
num1 = to_app(lhs)->get_num_args(); num1 = to_app(lhs)->get_num_args();
args1 = to_app(lhs)->get_args(); args1 = to_app(lhs)->get_args();
} }
else { else {
num1 = 1; num1 = 1;
@ -1897,7 +1897,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) {
if (m_util.is_concat(rhs)) { if (m_util.is_concat(rhs)) {
num2 = to_app(rhs)->get_num_args(); num2 = to_app(rhs)->get_num_args();
args2 = to_app(rhs)->get_args(); args2 = to_app(rhs)->get_args();
} }
else { else {
num2 = 1; num2 = 1;
@ -1930,7 +1930,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) {
new_eqs.push_back(m().mk_eq(m_mk_extract(sz1 - 1, low1, arg1), new_eqs.push_back(m().mk_eq(m_mk_extract(sz1 - 1, low1, arg1),
m_mk_extract(rsz1 + low2 - 1, low2, arg2))); m_mk_extract(rsz1 + low2 - 1, low2, arg2)));
low1 = 0; low1 = 0;
low2 += rsz1; low2 += rsz1;
--i1; --i1;
} }
else { else {
@ -1948,8 +1948,8 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) {
} }
bool bv_rewriter::is_concat_split_target(expr * t) const { bool bv_rewriter::is_concat_split_target(expr * t) const {
return return
m_split_concat_eq || m_split_concat_eq ||
m_util.is_concat(t) || m_util.is_concat(t) ||
m_util.is_numeral(t) || m_util.is_numeral(t) ||
m_util.is_bv_or(t); m_util.is_bv_or(t);
@ -1964,7 +1964,7 @@ void bv_rewriter::mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & r
SASSERT(is_numeral(c)); SASSERT(is_numeral(c));
if (is_minus_one_times_t(t1)) if (is_minus_one_times_t(t1))
result = m().mk_eq(t2, m_util.mk_bv_sub(c, t1)); result = m().mk_eq(t2, m_util.mk_bv_sub(c, t1));
else else
result = m().mk_eq(t1, m_util.mk_bv_sub(c, t2)); result = m().mk_eq(t1, m_util.mk_bv_sub(c, t2));
} }
@ -2024,14 +2024,14 @@ bool bv_rewriter::has_numeral(app* a) const {
} }
br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) { br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
expr * c, * x; expr * c, * x;
numeral c_val, c_inv_val; numeral c_val, c_inv_val;
unsigned sz; unsigned sz;
if (m_util.is_bv_mul(lhs, c, x) && if (m_util.is_bv_mul(lhs, c, x) &&
m_util.is_numeral(c, c_val, sz) && m_util.is_numeral(c, c_val, sz) &&
m_util.mult_inverse(c_val, sz, c_inv_val)) { m_util.mult_inverse(c_val, sz, c_inv_val)) {
SASSERT(m_util.norm(c_val * c_inv_val, sz).is_one()); SASSERT(m_util.norm(c_val * c_inv_val, sz).is_one());
numeral rhs_val; numeral rhs_val;
@ -2048,7 +2048,7 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
if (m_util.is_bv_mul(rhs, c2, x2) && m_util.is_numeral(c2, c2_val, sz)) { if (m_util.is_bv_mul(rhs, c2, x2) && m_util.is_numeral(c2, c2_val, sz)) {
// x = c_inv * c2 * x2 // x = c_inv * c2 * x2
numeral new_c2 = m_util.norm(c_inv_val * c2_val, sz); numeral new_c2 = m_util.norm(c_inv_val * c2_val, sz);
if (new_c2.is_one()) if (new_c2.is_one())
result = m().mk_eq(x, x2); result = m().mk_eq(x, x2);
else else
result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val * c2_val, sz), x2)); result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val * c2_val, sz), x2));
@ -2077,7 +2077,7 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
} }
} }
if (found) { if (found) {
result = m().mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz), result = m().mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz),
m_util.mk_bv_mul(m_util.mk_numeral(c2_inv_val, sz), rhs)); m_util.mk_bv_mul(m_util.mk_numeral(c2_inv_val, sz), rhs));
return BR_REWRITE3; return BR_REWRITE3;
} }
@ -2095,7 +2095,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
result = m().mk_false(); result = m().mk_false();
return BR_DONE; return BR_DONE;
} }
bool swapped = false; bool swapped = false;
if (is_numeral(lhs)) { if (is_numeral(lhs)) {
swapped = true; swapped = true;
@ -2120,7 +2120,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result,m()) << "\n";); TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result,m()) << "\n";);
return st; return st;
} }
if (m_blast_eq_value) { if (m_blast_eq_value) {
st = mk_blast_eq_value(lhs, rhs, result); st = mk_blast_eq_value(lhs, rhs, result);
if (st != BR_FAILED) if (st != BR_FAILED)
@ -2142,10 +2142,10 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
new_lhs = lhs; new_lhs = lhs;
new_rhs = rhs; new_rhs = rhs;
} }
lhs = new_lhs; lhs = new_lhs;
rhs = new_rhs; rhs = new_rhs;
// Try to rewrite t1 + t2 = c --> t1 = c - t2 // Try to rewrite t1 + t2 = c --> t1 = c - t2
// Reason: it is much cheaper to bit-blast. // Reason: it is much cheaper to bit-blast.
if (isolate_term(lhs, rhs, result)) { if (isolate_term(lhs, rhs, result)) {
return BR_REWRITE2; return BR_REWRITE2;
@ -2155,7 +2155,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
} }
if (st != BR_FAILED) { if (st != BR_FAILED) {
result = m().mk_eq(lhs, rhs); result = m().mk_eq(lhs, rhs);
return BR_DONE; return BR_DONE;
} }
} }

6
src/ast/rewriter/bv_rewriter.h
View file

@ -155,7 +155,7 @@ public:
void updt_params(params_ref const & p); void updt_params(params_ref const & p);
static void get_param_descrs(param_descrs & r); static void get_param_descrs(param_descrs & r);
void set_mkbv2num(bool f) { m_mkbv2num = f; } void set_mkbv2num(bool f) { m_mkbv2num = f; }
unsigned get_bv_size(expr * t) const {return m_util.get_bv_size(t); } unsigned get_bv_size(expr * t) const {return m_util.get_bv_size(t); }
@ -164,7 +164,7 @@ public:
bool is_bv(expr * t) const { return m_util.is_bv(t); } bool is_bv(expr * t) const { return m_util.is_bv(t); }
expr * mk_numeral(numeral const & v, unsigned sz) { return m_util.mk_numeral(v, sz); } expr * mk_numeral(numeral const & v, unsigned sz) { return m_util.mk_numeral(v, sz); }
expr * mk_numeral(unsigned v, unsigned sz) { return m_util.mk_numeral(numeral(v), sz); } expr * mk_numeral(unsigned v, unsigned sz) { return m_util.mk_numeral(numeral(v), sz); }
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
if (mk_app_core(f, num_args, args, result) == BR_FAILED) if (mk_app_core(f, num_args, args, result) == BR_FAILED)
@ -174,6 +174,8 @@ public:
br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
bool hi_div0() const { return m_hi_div0; } bool hi_div0() const { return m_hi_div0; }
bv_util & get_util() { return m_util; }
}; };
#endif #endif

32
src/model/model_evaluator.cpp
View file

@ -49,9 +49,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
evaluator_cfg(ast_manager & m, model & md, params_ref const & p): evaluator_cfg(ast_manager & m, model & md, params_ref const & p):
m_model(md), m_model(md),
m_b_rw(m), m_b_rw(m),
// We must allow customers to set parameters for arithmetic rewriter/evaluator. // We must allow customers to set parameters for arithmetic rewriter/evaluator.
// In particular, the maximum degree of algebraic numbers that will be evaluated. // In particular, the maximum degree of algebraic numbers that will be evaluated.
m_a_rw(m, p), m_a_rw(m, p),
m_bv_rw(m), m_bv_rw(m),
// See comment above. We want to allow customers to set :sort-store // See comment above. We want to allow customers to set :sort-store
m_ar_rw(m, p), m_ar_rw(m, p),
@ -73,7 +73,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
m_model_completion = p.completion(); m_model_completion = p.completion();
m_cache = p.cache(); m_cache = p.cache();
} }
ast_manager & m() const { return m_model.get_manager(); } ast_manager & m() const { return m_model.get_manager(); }
bool evaluate(func_decl* f, unsigned num, expr * const * args, expr_ref & result) { bool evaluate(func_decl* f, unsigned num, expr * const * args, expr_ref & result) {
@ -89,11 +89,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
SASSERT(fi->get_arity() == num); SASSERT(fi->get_arity() == num);
bool actuals_are_values = true; bool actuals_are_values = true;
for (unsigned i = 0; actuals_are_values && i < num; i++) { for (unsigned i = 0; actuals_are_values && i < num; i++) {
actuals_are_values = m().is_value(args[i]); actuals_are_values = m().is_value(args[i]);
} }
if (!actuals_are_values) if (!actuals_are_values)
return false; // let get_macro handle it return false; // let get_macro handle it
@ -115,7 +115,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
result = val; result = val;
return BR_DONE; return BR_DONE;
} }
if (m_model_completion) { if (m_model_completion) {
sort * s = f->get_range(); sort * s = f->get_range();
expr * val = m_model.get_some_value(s); expr * val = m_model.get_some_value(s);
@ -154,7 +154,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
st = m_a_rw.mk_app_core(f, num, args, result); st = m_a_rw.mk_app_core(f, num, args, result);
else if (fid == m_bv_rw.get_fid()) else if (fid == m_bv_rw.get_fid())
st = m_bv_rw.mk_app_core(f, num, args, result); st = m_bv_rw.mk_app_core(f, num, args, result);
else if (fid == m_ar_rw.get_fid()) else if (fid == m_ar_rw.get_fid())
st = m_ar_rw.mk_app_core(f, num, args, result); st = m_ar_rw.mk_app_core(f, num, args, result);
else if (fid == m_dt_rw.get_fid()) else if (fid == m_dt_rw.get_fid())
st = m_dt_rw.mk_app_core(f, num, args, result); st = m_dt_rw.mk_app_core(f, num, args, result);
@ -180,9 +180,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
return st; return st;
} }
bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
func_interp * fi = m_model.get_func_interp(f); func_interp * fi = m_model.get_func_interp(f);
if (fi != 0) { if (fi != 0) {
if (fi->is_partial()) { if (fi->is_partial()) {
if (m_model_completion) { if (m_model_completion) {
@ -193,13 +194,16 @@ struct evaluator_cfg : public default_rewriter_cfg {
else { else {
return false; return false;
} }
} }
def = fi->get_interp(); def = fi->get_interp();
SASSERT(def != 0); SASSERT(def != 0);
return true; return true;
} }
if (f->get_family_id() == null_family_id && m_model_completion) { if (m_model_completion &&
(f->get_family_id() == null_family_id ||
m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f)))
{
sort * s = f->get_range(); sort * s = f->get_range();
expr * val = m_model.get_some_value(s); expr * val = m_model.get_some_value(s);
func_interp * new_fi = alloc(func_interp, m(), f->get_arity()); func_interp * new_fi = alloc(func_interp, m(), f->get_arity());
@ -211,8 +215,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
return false; return false;
} }
bool max_steps_exceeded(unsigned num_steps) const { bool max_steps_exceeded(unsigned num_steps) const {
cooperate("model evaluator"); cooperate("model evaluator");
if (memory::get_allocation_size() > m_max_memory) if (memory::get_allocation_size() > m_max_memory)
throw rewriter_exception(Z3_MAX_MEMORY_MSG); throw rewriter_exception(Z3_MAX_MEMORY_MSG);
@ -228,7 +232,7 @@ template class rewriter_tpl<evaluator_cfg>;
struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> { struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
evaluator_cfg m_cfg; evaluator_cfg m_cfg;
imp(model & md, params_ref const & p): imp(model & md, params_ref const & p):
rewriter_tpl<evaluator_cfg>(md.get_manager(), rewriter_tpl<evaluator_cfg>(md.get_manager(),
false, // no proofs for evaluator false, // no proofs for evaluator
m_cfg), m_cfg),
m_cfg(md.get_manager(), md, p) { m_cfg(md.get_manager(), md, p) {

2
src/util/debug.cpp
View file

@ -76,7 +76,7 @@ void invoke_gdb() {
for (;;) { for (;;) {
std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n"; std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n";
char result; char result;
bool ok = (std::cin >> result); bool ok = bool(std::cin >> result);
if (!ok) exit(ERR_INTERNAL_FATAL); // happens if std::cin is eof or unattached. if (!ok) exit(ERR_INTERNAL_FATAL); // happens if std::cin is eof or unattached.
switch(result) { switch(result) {
case 'C': case 'C':