From 8d3c3ede39def392db8aeed7a028888c3f50f1a7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Dec 2021 12:40:44 -0800 Subject: [PATCH 1/2] save Signed-off-by: Nikolaj Bjorner --- src/math/polysat/search_state.cpp | 2 +- src/math/polysat/viable.cpp | 2 +- src/test/polysat.cpp | 11 +++++++++-- 3 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp index 356506be0..dd9b526b8 100644 --- a/src/math/polysat/search_state.cpp +++ b/src/math/polysat/search_state.cpp @@ -61,7 +61,7 @@ namespace polysat { void search_state::pop() { auto const& item = m_items.back(); - if (item.is_assignment() && item.var() == m_assignment.back().first) + if (item.is_assignment() && !m_assignment.empty() && item.var() == m_assignment.back().first) m_assignment.pop_back(); m_items.pop_back(); } diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 362054e59..c09330009 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -190,7 +190,7 @@ namespace polysat { lo = val; } SASSERT(hi <= s.var2pdd(v).max_value()); - LOG("forbidden interval [" << lo << ", " << hi << "[\n"); + LOG("forbidden interval " << e->interval << " - " << val << " " << coeff_val << " [" << lo << ", " << hi << "["); entry* ne = alloc_entry(); ne->src = e->src; ne->side_cond = e->side_cond; diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 51e2567d3..65cac43f4 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -1065,10 +1065,17 @@ namespace polysat { void tst_polysat() { - - polysat::test_l5(); + polysat::test_ineq_axiom1(); + polysat::test_ineq_axiom2(); + polysat::test_ineq_axiom3(); + polysat::test_ineq_axiom4(); + polysat::test_ineq_axiom5(); + polysat::test_ineq_axiom6(); return; + polysat::test_ineq_basic4(); + //return; + polysat::test_ineq_basic6(); // polysat::test_monot_bounds(8); From ed9c0b84f668548ee1c11f14185b08333baa6f72 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Dec 2021 08:25:24 -0800 Subject: [PATCH 2/2] na Signed-off-by: Nikolaj Bjorner --- src/math/polysat/saturation.cpp | 4 ++-- src/math/polysat/solver.cpp | 11 +++++++---- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 23b4c1f8e..436eb7130 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -33,7 +33,7 @@ namespace polysat { for (auto c1 : core) { if (!c1->is_ule()) continue; - if (!c1.is_currently_false(s)) + if (c1.is_currently_true(s)) continue; auto c = c1.as_inequality(); if (try_ugt_x(v, core, c)) @@ -70,7 +70,7 @@ namespace polysat { SASSERT(!crit1.is_currently_true(s)); LOG("critical " << m_rule << " " << crit1); - LOG("consequent " << c << " value: " << c.bvalue(s) << " " << c.is_currently_false(s) << " " << core.contains(~c)); + LOG("consequent " << c << " value: " << c.bvalue(s) << " is-false: " << c.is_currently_false(s) << " " << core.contains(~c)); // ensure new core is a conflict diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 394f441a0..4c5031e9a 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -469,12 +469,15 @@ namespace polysat { ++m_stats.m_num_conflicts; SASSERT(is_conflict()); - + if (m_conflict.conflict_var() != null_var) { + pvar v = m_conflict.conflict_var(); // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack. - VERIFY(m_viable.resolve(m_conflict.conflict_var(), m_conflict)); - // TBD: make sure last value decision is blocked by this conflict. - // A conflict in test_l5 reverts v1 = 2 more than once. + VERIFY(m_viable.resolve(v, m_conflict)); + // TBD: saturate resulting conflict to get better lemmas. + LOG("try-saturate"); + m_conflict.try_saturate(v); + LOG("end-try-saturate"); } search_iterator search_it(m_search);