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

dbg

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-15 00:48:36 -07:00
parent 6af314c6d9
commit 30e9f24fa3
2 changed files with 14 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/math/polysat/fixplex_def.h
View file

@ -138,6 +138,7 @@ namespace polysat {
M.ensure_var(m_vars.size()); M.ensure_var(m_vars.size());
m_vars.push_back(var_info()); m_vars.push_back(var_info());
m_union_find.mk_var(); m_union_find.mk_var();
m_var2ineqs.push_back(unsigned_vector());
} }
if (m_to_patch.get_bounds() <= v) if (m_to_patch.get_bounds() <= v)
m_to_patch.set_bounds(2 * v + 1); m_to_patch.set_bounds(2 * v + 1);
@ -170,8 +171,11 @@ namespace polysat {
return l_true; return l_true;
if (!propagate_row_bounds()) if (!propagate_row_bounds())
return l_false; return l_false;
if (!propagate_row_eqs())
return l_false;
if (!patch()) if (!patch())
return l_undef; return l_undef;
++num_iterations; ++num_iterations;
SASSERT(well_formed()); SASSERT(well_formed());
} }
@ -627,7 +631,6 @@ namespace polysat {
ensure_var(v); ensure_var(v);
ensure_var(w); ensure_var(w);
unsigned idx = m_ineqs.size(); unsigned idx = m_ineqs.size();
m_var2ineqs.reserve(std::max(v, w) + 1);
m_var2ineqs[v].push_back(idx); m_var2ineqs[v].push_back(idx);
m_var2ineqs[w].push_back(idx); m_var2ineqs[w].push_back(idx);
touch_var(v); touch_var(v);
@ -1068,6 +1071,8 @@ namespace polysat {
template<typename Ext> template<typename Ext>
bool fixplex<Ext>::propagate_row_eqs() { bool fixplex<Ext>::propagate_row_eqs() {
if (!m_to_patch.empty())
return true;
for (unsigned i : m_eq_rows) for (unsigned i : m_eq_rows)
get_offset_eqs(row(i)); get_offset_eqs(row(i));
m_eq_rows.reset(); m_eq_rows.reset();
@ -1162,9 +1167,12 @@ namespace polysat {
template<typename Ext> template<typename Ext>
bool fixplex<Ext>::propagate_row_bounds() { bool fixplex<Ext>::propagate_row_bounds() {
return true;
// TBD
if (inconsistent()) if (inconsistent())
return false; return false;
if (!m_to_patch.empty())
return true;
for (unsigned i : m_bound_rows) for (unsigned i : m_bound_rows)
if (!propagate_row(row(i))) if (!propagate_row(row(i)))
return false; return false;

5
src/test/fixplex.cpp
View file

@ -579,11 +579,10 @@ namespace polysat {
void tst_fixplex() { void tst_fixplex() {
polysat::test_ineqs(); polysat::test_lps();
return; return;
polysat::test_lps(); polysat::test_ineqs();
polysat::test_ineq_propagation1(); polysat::test_ineq_propagation1();
polysat::test_ineq_propagation2(); polysat::test_ineq_propagation2();