mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 20:50:50 +00:00
Code Activity

bv

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-26 11:26:59 -07:00
parent 81c3966331
commit 20be286391
4 changed files with 3 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/smt/array_model.cpp
View file

@ -23,7 +23,6 @@ namespace array {
void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) { void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
std::cout << "add-dep " << mk_bounded_pp(n->get_expr(), m) << "\n";
if (!a.is_array(n->get_expr())) { if (!a.is_array(n->get_expr())) {
dep.insert(n, nullptr); dep.insert(n, nullptr);
return; return;

7
src/sat/smt/bv_delay_internalize.cpp
View file

@ -180,7 +180,6 @@ namespace bv {
set_delay_internalize(r, internalize_mode::init_bits_only_i); // do not bit-blast this multiplier. set_delay_internalize(r, internalize_mode::init_bits_only_i); // do not bit-blast this multiplier.
expr_ref eq(m.mk_eq(r, arg_value), m); expr_ref eq(m.mk_eq(r, arg_value), m);
args[i] = n->get_arg(i); args[i] = n->get_arg(i);
std::cout << eq << "@" << s().scope_lvl() << "\n";
add_unit(b_internalize(eq)); add_unit(b_internalize(eq));
} }
return false; return false;
@ -299,8 +298,6 @@ namespace bv {
set_delay_internalize(rhs, internalize_mode::no_delay_i); set_delay_internalize(rhs, internalize_mode::no_delay_i);
expr_ref eq(m.mk_eq(lhs, rhs), m); expr_ref eq(m.mk_eq(lhs, rhs), m);
add_unit(b_internalize(eq)); add_unit(b_internalize(eq));
TRACE("bv", tout << "low-bits: " << eq << "\n";);
std::cout << "low bits\n";
return false; return false;
} }
@ -321,7 +318,10 @@ namespace bv {
}; };
/** /**
<<<<<<< HEAD
=======
>>>>>>> 055902df2... bv
* The i'th bit in xs is 1 if the least significant bit of x is i or lower. * The i'th bit in xs is 1 if the least significant bit of x is i or lower.
*/ */
void solver::encode_lsb_tail(expr* x, expr_ref_vector& xs) { void solver::encode_lsb_tail(expr* x, expr_ref_vector& xs) {
@ -388,7 +388,6 @@ namespace bv {
auto r2 = eval_args(n, args); auto r2 = eval_args(n, args);
if (r1 == r2) if (r1 == r2)
return true; return true;
if (m_cheap_axioms) if (m_cheap_axioms)
return true; return true;
set_delay_internalize(a, internalize_mode::no_delay_i); set_delay_internalize(a, internalize_mode::no_delay_i);

1
src/sat/smt/bv_solver.cpp
View file

@ -500,7 +500,6 @@ namespace bv {
svector<std::pair<expr*, internalize_mode>> delay; svector<std::pair<expr*, internalize_mode>> delay;
for (auto kv : m_delay_internalize) for (auto kv : m_delay_internalize)
delay.push_back(std::make_pair(kv.m_key, kv.m_value)); delay.push_back(std::make_pair(kv.m_key, kv.m_value));
flet<bool> _cheap1(m_cheap_axioms, true); flet<bool> _cheap1(m_cheap_axioms, true);
for (auto kv : delay) for (auto kv : delay)
if (!check_delay_internalized(kv.first)) if (!check_delay_internalized(kv.first))

1
src/sat/smt/bv_solver.h
View file

@ -272,7 +272,6 @@ namespace bv {
bool check_mul_zero(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2); bool check_mul_zero(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2);
bool check_mul_one(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2); bool check_mul_one(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2);
bool check_mul_low_bits(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2); bool check_mul_low_bits(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2);
bool check_umul_no_overflow(app* n, expr_ref_vector const& arg_values, expr* value); bool check_umul_no_overflow(app* n, expr_ref_vector const& arg_values, expr* value);
bool check_bv_eval(euf::enode* n); bool check_bv_eval(euf::enode* n);
bool check_bool_eval(euf::enode* n); bool check_bool_eval(euf::enode* n);