From 49590e0e01545330bd296b558e4f4669240bd0dd Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 23 Sep 2022 16:45:56 +0200 Subject: [PATCH] Conflict from viable_fallback also depends on the current assignment --- src/math/polysat/conflict.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 62776ee48..40b7e6d1a 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -251,10 +251,19 @@ namespace polysat { if (by_viable_fallback) { logger().begin_conflict(header_with_var("unsat core from viable fallback for v", v)); // Conflict detected by viable fallback: - // initial conflict is the unsat core of the univariate solver + // initial conflict is the unsat core of the univariate solver, + // and the assignment (under which the constraints are univariate in v) + // TODO: + // - currently we add variables directly, which is sound: + // e.g.: v^2 + w^2 == 0; w := 1 + // - but we could use side constraints on the coefficients instead (coefficients when viewed as polynomial over v): + // e.g.: v^2 + w^2 == 0; w^2 == 1 signed_constraints unsat_core = s.m_viable_fallback.unsat_core(v); - for (auto c : unsat_core) + for (auto c : unsat_core) { insert(c); + insert_vars(c); + } + SASSERT(!m_vars.contains(v)); // TODO: apply conflict resolution plugins here too? } else { logger().begin_conflict(header_with_var("forbidden interval lemma for v", v));