mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix #2779

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-12-03 14:49:58 +01:00
parent 7f61d08496
commit eec153bb57
4 changed files with 22 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/qe/qsat.cpp
View file

@ -520,6 +520,7 @@ namespace qe {
if ((m.is_true(val_a) && m.is_false(val_b)) || if ((m.is_true(val_a) && m.is_false(val_b)) ||
(m.is_false(val_a) && m.is_true(val_b))) { (m.is_false(val_a) && m.is_true(val_b))) {
TRACE("qe", TRACE("qe",
tout << model << "\n";
tout << mk_pp(a, m) << " := " << val_a << "\n"; tout << mk_pp(a, m) << " := " << val_a << "\n";
tout << mk_pp(b, m) << " := " << val_b << "\n"; tout << mk_pp(b, m) << " := " << val_b << "\n";
tout << m_elevel.find(a) << "\n";); tout << m_elevel.find(a) << "\n";);

18
src/smt/diff_logic.h
View file

@ -915,6 +915,24 @@ public:
// so the graph is disconnected. // so the graph is disconnected.
// assumption: the current assignment is feasible. // assumption: the current assignment is feasible.
// //
void set_to_zero(unsigned n, dl_var const* vs) {
for (unsigned i = 0; i < n; ++i) {
dl_var v = vs[i];
if (!m_assignment[v].is_zero()) {
set_to_zero(v);
for (unsigned j = 0; j < n; ++j) {
dl_var w = vs[j];
if (!m_assignment[w].is_zero()) {
enable_edge(add_edge(v, w, numeral(0), explanation()));
enable_edge(add_edge(w, v, numeral(0), explanation()));
SASSERT(is_feasible());
}
}
return;
}
}
}
void set_to_zero(dl_var v, dl_var w) { void set_to_zero(dl_var v, dl_var w) {
if (!m_assignment[v].is_zero()) { if (!m_assignment[v].is_zero()) {
set_to_zero(v); set_to_zero(v);

3
src/smt/theory_diff_logic_def.h
View file

@ -360,8 +360,7 @@ final_check_status theory_diff_logic<Ext>::final_check_eh() {
TRACE("arith_final", display(tout); ); TRACE("arith_final", display(tout); );
// either will already be zero (as we don't do mixed constraints). // either will already be zero (as we don't do mixed constraints).
m_graph.set_to_zero(get_zero(true)); m_graph.set_to_zero(get_zero(true), get_zero(false));
m_graph.set_to_zero(get_zero(false));
SASSERT(is_consistent()); SASSERT(is_consistent());
if (m_non_diff_logic_exprs) { if (m_non_diff_logic_exprs) {
return FC_GIVEUP; return FC_GIVEUP;

4
src/smt/theory_utvpi_def.h
View file

@ -786,8 +786,8 @@ namespace smt {
m.register_factory(m_factory); m.register_factory(m_factory);
enforce_parity(); enforce_parity();
init_zero(); init_zero();
m_graph.set_to_zero(to_var(m_izero), neg(to_var(m_izero))); dl_var vs[4] = { to_var(m_izero), neg(to_var(m_izero)), to_var(m_rzero), neg(to_var(m_rzero)) };
m_graph.set_to_zero(to_var(m_rzero), neg(to_var(m_rzero))); m_graph.set_to_zero(4, vs);
compute_delta(); compute_delta();
DEBUG_CODE(model_validate();); DEBUG_CODE(model_validate(););
} }