mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

#5324

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-07 10:59:10 -07:00
parent 5d3f48cc8d
commit d8905885ed
3 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -73,6 +73,8 @@ namespace bv {
SASSERT(e->get_num_args() >= 2);
expr_ref_vector args(m);
euf::enode* n = expr2enode(e);
if (!reflect())
return false;
auto r1 = eval_bv(n);
auto r2 = eval_args(n, args);
if (r1 == r2)
@ -356,6 +358,8 @@ namespace bv {
return internalize_mode::no_delay_i;
if (!get_config().m_bv_delay)
return internalize_mode::no_delay_i;
if (!reflect())
return internalize_mode::no_delay_i;
internalize_mode mode;
switch (to_app(e)->get_decl_kind()) {
case OP_BMUL:

2
src/sat/smt/bv_internalize.cpp
View file

@ -137,7 +137,7 @@ namespace bv {
return true;
SASSERT(!n || !n->is_attached_to(get_id()));
bool suppress_args = !get_config().m_bv_reflect && !m.is_considered_uninterpreted(a->get_decl());
bool suppress_args = !reflect() && !m.is_considered_uninterpreted(a->get_decl());
if (!n)
n = mk_enode(e, suppress_args);

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

@ -259,6 +259,7 @@ namespace bv {
void assert_bv2int_axiom(app * n);
void assert_int2bv_axiom(app* n);
void assert_ackerman(theory_var v1, theory_var v2);
bool reflect() const { return get_config().m_bv_reflect; }
// delay internalize
enum class internalize_mode {