mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e1ece7e968
commit
198622b61a
|
@ -308,7 +308,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void context::assign_core(literal l, b_justification j, bool decision) {
|
||||
TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
|
||||
CTRACE("assign_core", l.var() == 1573 || l.var() == 1253, tout << (decision?"decision: ":"propagating: ") << l << " ";
|
||||
display_literal_smt2(tout, l); tout << " level: " << m_scope_lvl << "\n";
|
||||
display(tout, j););
|
||||
m_assigned_literals.push_back(l);
|
||||
|
@ -2066,6 +2066,7 @@ namespace smt {
|
|||
while (i != old_lim) {
|
||||
--i;
|
||||
literal l = m_assigned_literals[i];
|
||||
CTRACE("assign_core", l.var() == 1573 || l.var() == 1253, tout << "unassign " << l << "\n";);
|
||||
m_assignment[l.index()] = l_undef;
|
||||
m_assignment[(~l).index()] = l_undef;
|
||||
bool_var v = l.var();
|
||||
|
|
|
@ -1286,7 +1286,7 @@ namespace smt {
|
|||
continue;
|
||||
}
|
||||
theory_var v2 = next(v);
|
||||
TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << "\n";);
|
||||
TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << " " << ctx.get_scope_level() << "\n";);
|
||||
literal antecedent = bit;
|
||||
|
||||
if (val == l_false) {
|
||||
|
@ -1298,7 +1298,7 @@ namespace smt {
|
|||
SASSERT(bit != ~bit2);
|
||||
lbool val2 = ctx.get_assignment(bit2);
|
||||
TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";);
|
||||
TRACE("bv", tout << bit << " " << bit2 << " " << val << " " << val2 << "\n";);
|
||||
TRACE("bv", tout << bit << " -> " << bit2 << " " << val << " -> " << val2 << " " << ctx.get_scope_level() << "\n";);
|
||||
|
||||
if (val != val2) {
|
||||
literal consequent = bit2;
|
||||
|
@ -1432,7 +1432,6 @@ namespace smt {
|
|||
|
||||
void theory_bv::pop_scope_eh(unsigned num_scopes) {
|
||||
m_trail_stack.pop_scope(num_scopes);
|
||||
TRACE("bv", m_find.display(tout << num_scopes << " @ " << get_context().get_scope_level() << "\n"););
|
||||
unsigned num_old_vars = get_old_num_vars(num_scopes);
|
||||
m_bits.shrink(num_old_vars);
|
||||
m_wpos.shrink(num_old_vars);
|
||||
|
@ -1448,6 +1447,8 @@ namespace smt {
|
|||
m_diseq_watch_lim.shrink(m_diseq_watch_lim.size()-num_scopes);
|
||||
#endif
|
||||
theory::pop_scope_eh(num_scopes);
|
||||
TRACE("bv", m_find.display(tout << get_context().get_scope_level() << " - "
|
||||
<< num_scopes << " = " << (get_context().get_scope_level() - num_scopes) << "\n"););
|
||||
}
|
||||
|
||||
final_check_status theory_bv::final_check_eh() {
|
||||
|
|
|
@ -1634,6 +1634,9 @@ public:
|
|||
if (vars.empty()) {
|
||||
return false;
|
||||
}
|
||||
if (!m_use_nra_model) {
|
||||
lp().random_update(vars.size(), vars.c_ptr());
|
||||
}
|
||||
init_variable_values();
|
||||
TRACE("arith",
|
||||
for (theory_var v = 0; v < sz; ++v) {
|
||||
|
@ -1642,9 +1645,6 @@ public:
|
|||
}
|
||||
}
|
||||
tout << "\n"; );
|
||||
if (!m_use_nra_model) {
|
||||
lp().random_update(vars.size(), vars.c_ptr());
|
||||
}
|
||||
m_model_eqs.reset();
|
||||
TRACE("arith", display(tout););
|
||||
|
||||
|
|
Loading…
Reference in a new issue