Re-integrate forbidden intervals

src/math/polysat/conflict_core.cpp

@@ -17,6 +17,7 @@ Author:
 #include "math/polysat/log.h"
 #include "math/polysat/log_helper.h"
 #include "math/polysat/explain.h"
+#include "math/polysat/forbidden_intervals.h"
 #include "math/polysat/saturation.h"
 #include "math/polysat/variable_elimination.h"
 #include <algorithm>
@@ -252,6 +253,15 @@ namespace polysat {
             m_solver->assign_core(v, m_solver->m_value[v], justification::propagation(m_solver->m_level));
         }
         */
+       if (conflict_var() == v) {
+           clause_builder lemma(s());
+           forbidden_intervals fi;
+           if (fi.perform(s(), v, *this, lemma)) {
+               set_bailout();
+               m_bailout_lemma = std::move(lemma);
+               return true;
+           }
+       }
 
         for (auto c : cjust_v)
             insert(c);

src/math/polysat/conflict_core.h

@@ -42,6 +42,7 @@ namespace polysat {
         std::optional<clause_builder> m_bailout_lemma;
 
         solver* m_solver = nullptr;
+        solver& s() { return *m_solver; }
         constraint_manager& cm();
         scoped_ptr_vector<explainer> ex_engines;
         scoped_ptr_vector<variable_elimination_engine> ve_engines;

src/math/polysat/forbidden_intervals.h

@@ -16,7 +16,6 @@ Author:
 #pragma once
 #include "math/polysat/constraint.h"
 #include "math/polysat/solver.h"
-#include "math/polysat/variable_elimination.h"
 
 namespace polysat {
 

src/math/polysat/solver.cpp

@@ -516,20 +516,6 @@ namespace polysat {
 
     /** Conflict resolution case where propagation 'v := ...' is on top of the stack */
     void solver::resolve_value(pvar v) {
-        // SASSERT(m_justification[v].is_propagation());   // doesn't hold if we enter because of conflict_var
-        // Conceptually:
-        // - Value Resolution
-        // - Variable Elimination
-        // - if VE isn't possible, try to derive new constraints using core saturation
-
-        // m_conflict.set_var(v);
-
-        // TODO:
-        // 1. try "perfect" rules if any match, e.g., poly superposition allows us to eliminate variable immediately if it works
-        // 2. if none match, then apply any saturation rules that do
-        // 3. following saturation, check if we can apply other variable elimination
-        // 4. fallback lemma if we have to (collect decisions)
-
         if (m_conflict.is_bailout()) {
             for (auto c : m_cjust[v])
                 m_conflict.insert(c);