From 88d11c93817a7a46fd465a86fadf537933d20324 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 25 Jan 2023 12:34:01 +0100 Subject: [PATCH] skip always-true constraints --- src/math/polysat/solver.cpp | 35 ++++++++++++++++++++++------------- 1 file changed, 22 insertions(+), 13 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 58ca46b5b..8942dd160 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -162,25 +162,34 @@ namespace polysat { SASSERT(dep == null_dependency && "track dependencies is TODO"); return; case l_true: - // constraint c is already asserted + // constraint c is already asserted => ignore SASSERT(m_bvars.level(lit) <= m_level); - break; + return; case l_undef: - if (c.is_always_false()) { - LOG("Always false: " << c); - // asserted an always-false constraint - set_conflict_at_base_level(); - return; - } - m_bvars.assumption(lit, m_level, dep); - m_trail.push_back(trail_instr_t::assign_bool_i); - m_search.push_boolean(lit); - if (c.is_currently_false(*this)) - set_conflict(c); break; default: UNREACHABLE(); } + switch (c.eval()) { + case l_false: + // asserted an always-false constraint => conflict at base level + LOG("Always false: " << c); + set_conflict_at_base_level(); + SASSERT(dep == null_dependency && "track dependencies is TODO"); + return; + case l_true: + // asserted an always-true constraint => ignore + return; + case l_undef: + break; + default: + UNREACHABLE(); + } + m_bvars.assumption(lit, m_level, dep); + m_trail.push_back(trail_instr_t::assign_bool_i); + m_search.push_boolean(lit); + if (c.is_currently_false(*this)) + set_conflict(c); #if ENABLE_LINEAR_SOLVER m_linear_solver.new_constraint(*c.get()); #endif