mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

fix #2777

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-12-03 13:53:59 +01:00
parent b35ec49b40
commit 7f61d08496
5 changed files with 27 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/diff_logic.h
View file

@ -315,7 +315,7 @@ private:
typename assignment_stack::iterator begin = m_assignment_stack.begin(); typename assignment_stack::iterator begin = m_assignment_stack.begin();
while (it != begin) { while (it != begin) {
--it; --it;
TRACE("diff_logic_bug", tout << "undo assignment: " << it->get_var() << " " << it->get_old_value() << "\n";); TRACE("dl_bug", tout << "undo assignment: " << it->get_var() << " " << it->get_old_value() << "\n";);
m_assignment[it->get_var()] = it->get_old_value(); m_assignment[it->get_var()] = it->get_old_value();
} }
m_assignment_stack.reset(); m_assignment_stack.reset();
@ -371,7 +371,7 @@ private:
SASSERT(m_gamma[target].is_neg()); SASSERT(m_gamma[target].is_neg());
acc_assignment(target, gamma); acc_assignment(target, gamma);
TRACE("arith", tout << id << "\n";); TRACE("arith", display(tout << id << "\n"););
dl_var source = target; dl_var source = target;
while (true) { while (true) {
@ -467,7 +467,7 @@ public:
// The graph does not have control over the ids assigned by the theory. // The graph does not have control over the ids assigned by the theory.
// That is init_var receives the id as an argument. // That is init_var receives the id as an argument.
void init_var(dl_var v) { void init_var(dl_var v) {
TRACE("diff_logic_bug", tout << "init_var " << v << "\n";); TRACE("dl_bug", tout << "init_var " << v << "\n";);
if (static_cast<unsigned>(v) < m_out_edges.size() && (!m_out_edges[v].empty() || !m_in_edges[v].empty())) { if (static_cast<unsigned>(v) < m_out_edges.size() && (!m_out_edges[v].empty() || !m_in_edges[v].empty())) {
return; return;
} }
@ -485,7 +485,7 @@ public:
} }
m_assignment[v].reset(); m_assignment[v].reset();
SASSERT(static_cast<unsigned>(v) < m_heap.get_bounds()); SASSERT(static_cast<unsigned>(v) < m_heap.get_bounds());
TRACE("diff_logic_bug", tout << "init_var " << v << ", m_assignment[v]: " << m_assignment[v] << "\n";); TRACE("dl_bug", tout << "init_var " << v << ", m_assignment[v]: " << m_assignment[v] << "\n";);
SASSERT(m_assignment[v].is_zero()); SASSERT(m_assignment[v].is_zero());
SASSERT(m_out_edges[v].empty()); SASSERT(m_out_edges[v].empty());
SASSERT(m_in_edges[v].empty()); SASSERT(m_in_edges[v].empty());
@ -934,7 +934,7 @@ private:
// m_assignment[v] += inc // m_assignment[v] += inc
// This method also stores the old value of v in the assignment stack. // This method also stores the old value of v in the assignment stack.
void acc_assignment(dl_var v, const numeral & inc) { void acc_assignment(dl_var v, const numeral & inc) {
TRACE("diff_logic_bug", tout << "update v: " << v << " += " << inc << " m_assignment[v] " << m_assignment[v] << "\n";); TRACE("dl_bug", tout << "update v: " << v << " += " << inc << " m_assignment[v] " << m_assignment[v] << "\n";);
m_assignment_stack.push_back(assignment_trail(v, m_assignment[v])); m_assignment_stack.push_back(assignment_trail(v, m_assignment[v]));
m_assignment[v] += inc; m_assignment[v] += inc;
} }

2
src/smt/theory_diff_logic.h
View file

@ -377,7 +377,7 @@ namespace smt {
void init_zero(); void init_zero();
theory_var get_zero(bool is_int) { init_zero(); return is_int ? m_izero : m_rzero; } theory_var get_zero(bool is_int) { return is_int ? m_izero : m_rzero; }
void inc_conflicts(); void inc_conflicts();

35
src/smt/theory_diff_logic_def.h
View file

@ -66,6 +66,7 @@ void theory_diff_logic<Ext>::nc_functor::reset() {
template<typename Ext> template<typename Ext>
void theory_diff_logic<Ext>::init(context * ctx) { void theory_diff_logic<Ext>::init(context * ctx) {
theory::init(ctx); theory::init(ctx);
init_zero();
} }
@ -192,10 +193,10 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
found_non_diff_logic_expr(n); found_non_diff_logic_expr(n);
return false; return false;
} }
SASSERT(m_signs.size() == m_terms.size()); SASSERT(m_signs.size() == m_terms.size());
if (m_terms.size() == 2 && m_signs[0] != m_signs[1]) { if (m_terms.size() == 2 && m_signs[0] != m_signs[1]) {
app* a = m_terms.get(0), *b = m_terms.get(1); app* a = m_terms.get(0), *b = m_terms.get(1);
bool sign0 = m_signs[0]; bool sign0 = m_signs[0];
target = mk_var(a); target = mk_var(a);
source = mk_var(b); source = mk_var(b);
if (!sign0) { if (!sign0) {
@ -212,7 +213,7 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
k.neg(); k.neg();
} }
if (ctx.b_internalized(n)) return true; if (ctx.b_internalized(n)) return true;
bv = ctx.mk_bool_var(n); bv = ctx.mk_bool_var(n);
ctx.set_var_theory(bv, get_id()); ctx.set_var_theory(bv, get_id());
literal l(bv); literal l(bv);
@ -318,7 +319,7 @@ void theory_diff_logic<Ext>::collect_statistics(::statistics & st) const {
template<typename Ext> template<typename Ext>
void theory_diff_logic<Ext>::push_scope_eh() { void theory_diff_logic<Ext>::push_scope_eh() {
TRACE("arith", tout << "push\n";);
theory::push_scope_eh(); theory::push_scope_eh();
m_graph.push(); m_graph.push();
m_scopes.push_back(scope()); m_scopes.push_back(scope());
@ -330,6 +331,7 @@ void theory_diff_logic<Ext>::push_scope_eh() {
template<typename Ext> template<typename Ext>
void theory_diff_logic<Ext>::pop_scope_eh(unsigned num_scopes) { void theory_diff_logic<Ext>::pop_scope_eh(unsigned num_scopes) {
TRACE("arith", tout << "pop " << num_scopes << "\n";);
unsigned lvl = m_scopes.size(); unsigned lvl = m_scopes.size();
SASSERT(num_scopes <= lvl); SASSERT(num_scopes <= lvl);
unsigned new_lvl = lvl - num_scopes; unsigned new_lvl = lvl - num_scopes;
@ -803,9 +805,9 @@ theory_var theory_diff_logic<Ext>::mk_var(app* n) {
context & ctx = get_context(); context & ctx = get_context();
enode* e = nullptr; enode* e = nullptr;
theory_var v = null_theory_var; theory_var v = null_theory_var;
if (!ctx.e_internalized(n)) { if (!ctx.e_internalized(n)) {
ctx.internalize(n, false); ctx.internalize(n, false);
} }
e = ctx.get_enode(n); e = ctx.get_enode(n);
v = e->get_th_var(get_id()); v = e->get_th_var(get_id());
@ -1154,9 +1156,9 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
// add objective function as row. // add objective function as row.
coeffs.reset(); coeffs.reset();
vars.reset(); vars.reset();
for (unsigned i = 0; i < objective.size(); ++i) { for (auto const& o : objective) {
coeffs.push_back(objective[i].second.to_mpq()); coeffs.push_back(o.second.to_mpq());
vars.push_back(node2simplex(objective[i].first)); vars.push_back(node2simplex(o.first));
} }
coeffs.push_back(mpq(1)); coeffs.push_back(mpq(1));
vars.push_back(w); vars.push_back(w);
@ -1169,11 +1171,11 @@ template<typename Ext>
typename theory_diff_logic<Ext>::inf_eps theory_diff_logic<Ext>::value(theory_var v) { typename theory_diff_logic<Ext>::inf_eps theory_diff_logic<Ext>::value(theory_var v) {
objective_term const& objective = m_objectives[v]; objective_term const& objective = m_objectives[v];
inf_eps r = inf_eps(m_objective_consts[v]); inf_eps r = inf_eps(m_objective_consts[v]);
for (unsigned i = 0; i < objective.size(); ++i) { for (auto const& o : objective) {
numeral n = m_graph.get_assignment(v); numeral n = m_graph.get_assignment(v);
rational r1 = n.get_rational().to_rational(); rational r1 = n.get_rational().to_rational();
rational r2 = n.get_infinitesimal().to_rational(); rational r2 = n.get_infinitesimal().to_rational();
r += objective[i].second * inf_eps(rational(0), inf_rational(r1, r2)); r += o.second * inf_eps(rational(0), inf_rational(r1, r2));
} }
return r; return r;
} }
@ -1190,9 +1192,9 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
TRACE("arith", TRACE("arith",
objective_term const& objective = m_objectives[v]; objective_term const& objective = m_objectives[v];
for (unsigned i = 0; i < objective.size(); ++i) { for (auto const& o : objective) {
tout << "Coefficient " << objective[i].second tout << "Coefficient " << o.second
<< " of theory_var " << objective[i].first << "\n"; << " of theory_var " << o.first << "\n";
} }
tout << "Free coefficient " << m_objective_consts[v] << "\n"; tout << "Free coefficient " << m_objective_consts[v] << "\n";
); );
@ -1385,6 +1387,7 @@ theory* theory_diff_logic<Ext>::mk_fresh(context* new_ctx) {
template<typename Ext> template<typename Ext>
void theory_diff_logic<Ext>::init_zero() { void theory_diff_logic<Ext>::init_zero() {
if (m_izero != null_theory_var) return; if (m_izero != null_theory_var) return;
TRACE("arith", tout << "init zero\n";);
context & ctx = get_context(); context & ctx = get_context();
app* zero; app* zero;
enode* e; enode* e;

2
src/smt/theory_utvpi.h
View file

@ -299,7 +299,7 @@ namespace smt {
void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just); void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just);
th_var get_zero(sort* s) { init_zero(); return a.is_int(s) ? m_izero : m_rzero; } th_var get_zero(sort* s) { return a.is_int(s) ? m_izero : m_rzero; }
th_var get_zero(expr* e) { return get_zero(get_manager().get_sort(e)); } th_var get_zero(expr* e) { return get_zero(get_manager().get_sort(e)); }

1
src/smt/theory_utvpi_def.h
View file

@ -261,6 +261,7 @@ namespace smt {
template<typename Ext> template<typename Ext>
void theory_utvpi<Ext>::init(context* ctx) { void theory_utvpi<Ext>::init(context* ctx) {
theory::init(ctx); theory::init(ctx);
init_zero();
} }
template<typename Ext> template<typename Ext>