From 681293c23f600b582e2138fd0f2dd25a5f4c3767 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 26 Jul 2023 09:47:55 +0200 Subject: [PATCH] use slicing conflict clause --- src/math/polysat/solver.cpp | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 72b81e455..d4a8f00ac 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -353,15 +353,7 @@ namespace polysat { } if (m_slicing.is_conflict()) { SASSERT(!is_conflict()); - sat::literal_vector lits; - unsigned_vector vars; - m_slicing.explain(lits, vars); - clause_builder cb(*this, "slicing"); - for (sat::literal lit : lits) - cb.insert(~lit); - for (pvar v : vars) - cb.insert_eval(~eq(var(v), get_value(v))); - add_clause(cb.build()); + add_clause(m_slicing.build_conflict_clause()); SASSERT(is_conflict()); } } // while (can_propagate_search())