mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
This commit is contained in:
parent
02644b5b71
commit
ed9341e3b0
|
@ -745,7 +745,7 @@ namespace euf {
|
|||
out << "] ";
|
||||
}
|
||||
if (n->value() != l_undef)
|
||||
out << "[v" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] ";
|
||||
out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] ";
|
||||
if (n->has_th_vars()) {
|
||||
out << "[t";
|
||||
for (auto v : enode_th_vars(n))
|
||||
|
|
|
@ -50,7 +50,7 @@ namespace arith {
|
|||
scoped_anum an(m_nla->am());
|
||||
m_nla->am().display(out << " = ", nl_value(v, an));
|
||||
}
|
||||
else if (can_get_value(v))
|
||||
else if (can_get_value(v) && !m_solver->has_changed_columns())
|
||||
out << " = " << get_value(v);
|
||||
if (is_int(v))
|
||||
out << ", int";
|
||||
|
|
|
@ -384,7 +384,7 @@ namespace arith {
|
|||
|
||||
obj_map<expr, expr*> m_predicate2term;
|
||||
obj_map<expr, bound_info> m_term2bound_info;
|
||||
bool m_model_is_initialized{ false };
|
||||
bool m_model_is_initialized = false;
|
||||
|
||||
unsigned small_lemma_size() const { return get_config().m_arith_small_lemma_size; }
|
||||
bool propagate_eqs() const { return get_config().m_arith_propagate_eqs && m_num_conflicts < get_config().m_arith_propagation_threshold; }
|
||||
|
|
|
@ -278,6 +278,7 @@ namespace euf {
|
|||
}
|
||||
else {
|
||||
sat::bool_var v = si.to_bool_var(c);
|
||||
s().set_external(v);
|
||||
VERIFY(v != sat::null_bool_var);
|
||||
VERIFY(s().is_external(v));
|
||||
SASSERT(v != sat::null_bool_var);
|
||||
|
|
|
@ -352,6 +352,7 @@ namespace euf {
|
|||
sat::literal attach_lit(sat::literal lit, expr* e);
|
||||
void unhandled_function(func_decl* f);
|
||||
th_rewriter& get_rewriter() { return m_rewriter; }
|
||||
void rewrite(expr_ref& e) { m_rewriter(e); }
|
||||
bool is_shared(euf::enode* n) const;
|
||||
|
||||
// relevancy
|
||||
|
|
|
@ -213,6 +213,7 @@ namespace q {
|
|||
sat::literal qlit = ctx.expr2literal(q);
|
||||
if (is_exists(q))
|
||||
qlit.neg();
|
||||
ctx.rewrite(proj);
|
||||
TRACE("q", tout << "project: " << proj << "\n";);
|
||||
++m_stats.m_num_instantiations;
|
||||
unsigned generation = ctx.get_max_generation(proj);
|
||||
|
|
Loading…
Reference in a new issue