Add forbidden interval lemma separately

src/math/polysat/clause_builder.cpp

@@ -55,7 +55,7 @@ namespace polysat {
 
 
     void clause_builder::push(sat::literal lit) {
-        push(m_solver->m_constraints.lookup(lit));
+        push(m_solver->lit2cnstr(lit));
     }
 
     void clause_builder::push(signed_constraint c) {
@@ -73,4 +73,15 @@ namespace polysat {
 #endif
         m_literals.push_back(c.blit());
     }
+
+    void clause_builder::insert_eval(sat::literal lit) {
+        insert_eval(m_solver->lit2cnstr(lit));
+    }
+
+    void clause_builder::insert_eval(signed_constraint c) {
+        if (c.bvalue(*m_solver) == l_undef) {
+            m_solver->assign_eval(~c.blit());
+        }
+        push(c);
+    }
 }

src/math/polysat/clause_builder.h

@@ -43,9 +43,21 @@ namespace polysat {
         /// Returns nullptr if the clause is a tautology and should not be added to the solver.
         clause_ref build();
 
+        /// Insert constraints into the clause.
         void push(sat::literal lit);
         void push(signed_constraint c);
         void push(inequality const& i) { push(i.as_signed_constraint()); }
+        // TODO: remove push
+        void insert(sat::literal lit) { push(lit); }
+        void insert(signed_constraint c) { push(c); }
+        void insert(inequality const& i) { insert(i.as_signed_constraint()); }
+
+        /// Inserting constraints into the clause.
+        /// If they are not yet on the search stack, add them as evaluated to false.
+        /// \pre Constraint must be false in the current assignment.
+        void insert_eval(sat::literal lit);
+        void insert_eval(signed_constraint c);
+        void insert_eval(inequality const& i) { insert_eval(i.as_signed_constraint()); }
 
         using const_iterator = decltype(m_literals)::const_iterator;
         const_iterator begin() const { return m_literals.begin(); }

src/math/polysat/conflict.cpp

@@ -253,11 +253,6 @@ namespace polysat {
         }
         else {
             logger().begin_conflict(header_with_var("forbidden interval lemma for v", v));
-            // set_backtrack();  // TODO: add the FI-lemma as a side lemma.
-            //                            The FI-lemma should not be the new core, because that will break variable dependencies.
-            //                            Alternatively, we'll need different types of variable dependencies. (one where v=n is in the core, another which only ensures that we don't skip v during backtracking).
-            //                            But since we now also propagate evaluated literals at the right (earlier) levels,
-            //                            we don't need to follow the variable assignments backwards to find the backjumping level for the FI-lemma.
             VERIFY(s.m_viable.resolve(v, *this));
         }
         SASSERT(!empty());
@@ -320,9 +315,10 @@ namespace polysat {
     void conflict::add_lemma(clause_ref lemma) {
         SASSERT(lemma);
         lemma->set_redundant(true);
-        LOG("Side lemma: " << *lemma);
+        LOG_H3("Side lemma: " << *lemma);
         for (sat::literal lit : *lemma) {
-            LOG("   " << lit_pp(s, lit));
+            LOG(lit_pp(s, lit));
+            SASSERT(s.m_bvars.value(lit) != l_true);
         }
         // TODO: call clause simplifier here?
         //       maybe it reduces the level we have to consider.
@@ -351,6 +347,7 @@ namespace polysat {
         }
         if (has_unassigned)
             jump_level = max_level;
+        LOG("Jump level: " << jump_level);
         m_max_jump_level = std::min(m_max_jump_level, jump_level);
         m_lemmas.push_back(std::move(lemma));
         // If possible, we should set the new constraint to l_true;

src/math/polysat/solver.cpp

@@ -959,8 +959,10 @@ namespace polysat {
 
     void solver::assign_eval(sat::literal lit) {
         // SASSERT(lit2cnstr(lit).is_currently_true(*this));  // "morally" this should hold, but currently fails because of pop_assignment during resolve_conflict
+        SASSERT(!lit2cnstr(lit).is_currently_false(*this));
         unsigned level = 0;
         // NOTE: constraint may be evaluated even if some variables are still unassigned (e.g., 0*x doesn't depend on x).
+        // TODO: level might be too low! because pop_assignment may already have removed necessary variables (cf. comment on assertion above).
         for (auto v : lit2cnstr(lit)->vars())
             if (is_assigned(v))
                 level = std::max(get_level(v), level);

src/math/polysat/viable.cpp

@@ -643,6 +643,7 @@ namespace polysat {
         // If there is a full interval, all others would have been removed
         SASSERT(!e->interval.is_full() || e->next() == e);
         SASSERT(e->interval.is_full() || all_of(*e, [](entry const& f) { return !f.interval.is_full(); }));
+        clause_builder lemma(s);
         do {
             // Build constraint: upper bound of each interval is not contained in the next interval,
             // using the equivalence:  t \in [l;h[  <=>  t-l < h-l
@@ -694,26 +695,19 @@ namespace polysat {
                 auto lhs = hi - next_lo;
                 auto rhs = next_hi - next_lo;
                 signed_constraint c = s.m_constraints.ult(lhs, rhs);
-                core.insert_eval(c);
+                lemma.insert_eval(~c);
             }
             for (auto sc : e->side_cond)
-                core.insert_eval(sc);
+                lemma.insert_eval(~sc);
+            lemma.insert(~e->src);
             core.insert(e->src);
             e = n;
         }
         while (e != first);
+
+        SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false; }));
+        core.add_lemma(lemma.build());
         core.logger().log(inf_fi(*this, v));
-
-        // TODO: should not be here, too general
-        for (auto c : core) {
-            if (c.bvalue(s) == l_false) {
-                UNREACHABLE();  // an invariant of the new conflict state is that bvalue of all inserted constraints is l_true (cf. assertion in conflict::insert)
-                core.set(~c);
-                core.logger().log("");
-                break;
-            }
-        }
-
         return true;
     }
 

src/math/polysat/viable.h

@@ -108,9 +108,10 @@ namespace polysat {
         dd::find_t find_viable(pvar v, rational & val);
 
         /**
-        * Retrieve the unsat core for v.
+         * Retrieve the unsat core for v,
-        * \pre there are no viable values for v
+         * and add the forbidden interval lemma for v (which eliminates v from the unsat core).
-        */
+         * \pre there are no viable values for v
+         */
         bool resolve(pvar v, conflict& core);
 
         /** Log all viable values for the given variable.