Add level to conflict

- reset conflict at correct level when popping user scopes
- functions as flag when handling inconsistent input (e.g., opposite literals)
- now all constraints in the conflict core should have bvalue == l_true

src/math/polysat/conflict.cpp

@@ -140,10 +140,14 @@ namespace polysat {
     }
 
     bool conflict::empty() const {
-        return m_literals.empty()
+        bool const is_empty = (m_level == UINT_MAX);
-            && m_vars.empty()
+        if (is_empty) {
-            && m_bail_vars.empty()
+            SASSERT(m_literals.empty());
-            && m_lemmas.empty();
+            SASSERT(m_vars.empty());
+            SASSERT(m_bail_vars.empty());
+            SASSERT(m_lemmas.empty());
+        }
+        return is_empty;
     }
 
     void conflict::reset() {
@@ -154,6 +158,7 @@ namespace polysat {
         m_var_occurrences.reset();
         m_lemmas.reset();
         m_kind = conflict_kind_t::ok;
+        m_level = UINT_MAX;
         SASSERT(empty());
     }
 
@@ -182,7 +187,6 @@ namespace polysat {
             return true;
         case conflict_kind_t::backtrack:
             return pvar_occurs_in_constraints(v) || m_relevant_vars.contains(v);
-            // return m_relevant_vars.contains(v);
         case conflict_kind_t::backjump:
             UNREACHABLE();  // we don't follow the regular loop when backjumping
             return false;
@@ -195,8 +199,30 @@ namespace polysat {
         return contains(lit) || contains(~lit);
     }
 
+    void conflict::init_at_base_level() {
+        SASSERT(empty());
+        SASSERT(s.at_base_level());
+        m_level = s.m_level;
+        SASSERT(!empty());
+    }
+
     void conflict::init(signed_constraint c) {
         SASSERT(empty());
+        m_level = s.m_level;
+        /*
+        // NOTE: c.is_always_false() may happen e.g. if we add an always false constraint in the input
+        if (c.is_always_false()) {
+            SASSERT(c.bvalue(s) == l_true);
+            SASSERT(s.m_bvars.is_assumption(c.blit()));
+            SASSERT(s.at_base_level());
+            // TODO: this kind of constraint should be handled when it is being added to the solver.
+            return;
+        }
+        if (c.bvalue(s) == l_false && s.at_base_level()) {
+            // We have opposite literals in the input.
+            return;
+        }
+        */
         set_impl(c);
         logger().begin_conflict();
     }
@@ -238,6 +264,7 @@ namespace polysat {
         //     return;
         // LOG("Conflict: " << cl);
         SASSERT(empty());
+        m_level = s.m_level;
         for (auto lit : cl) {
             auto c = s.lit2cnstr(lit);
             SASSERT(c.bvalue(s) == l_false);
@@ -248,6 +275,8 @@ namespace polysat {
     }
 
     void conflict::init(pvar v, bool by_viable_fallback) {
+        SASSERT(empty());
+        m_level = s.m_level;
         if (by_viable_fallback) {
             logger().begin_conflict(header_with_var("unsat core from viable fallback for v", v));
             // Conflict detected by viable fallback:
@@ -264,6 +293,7 @@ namespace polysat {
             //       but each branch exclude the current assignment.
             //       in those cases we will (additionally?) need an abstraction that is asserting to make sure viable is updated properly.
         }
+        SASSERT(!empty());
     }
 
     bool conflict::contains(sat::literal lit) const {
@@ -276,7 +306,8 @@ namespace polysat {
             return;
         if (c.is_always_true())
             return;
-        LOG("Inserting: " << c);
+        LOG("Inserting " << lit_pp(s, c));
+        SASSERT(c.bvalue(s) == l_true);
         SASSERT(!c.is_always_false());  // if we added c, the core would be a tautology
         SASSERT(!c->vars().empty());
         m_literals.insert(c.blit().index());
@@ -424,9 +455,12 @@ namespace polysat {
         LOG("core: " << *this);
         clause_builder lemma(s);
 
-        // TODO: is this sound, doing it for each constraint separately?
+#if 0
-        for (auto c : *this)
+        if (m_literals.size() == 1) {
+            auto c = *begin();
             minimize_vars(c);
+        }
+#endif
 
         for (auto c : *this)
             lemma.push(~c);

src/math/polysat/conflict.h

@@ -32,6 +32,7 @@ Notes:
 
     - All literals should be assigned in the stack prior to their use;
       or justified by one of the side lemmas.
+      (thus: all literals in the core must have bvalue == l_true)
 
     l <- D => l,       < Vars, { l } u C >   ===>   < Vars, C u D >
     l <- ?,            < Vars, { l } u C >   ===>   ~l <- (C & Vars = value(Vars) => ~l)
@@ -112,6 +113,9 @@ namespace polysat {
 
         conflict_kind_t m_kind = conflict_kind_t::ok;
 
+        // Level at which the conflict was discovered
+        unsigned m_level = UINT_MAX;
+
         void set_impl(signed_constraint c);
         bool minimize_vars(signed_constraint c);
 
@@ -131,6 +135,8 @@ namespace polysat {
         uint_set const& vars() const { return m_vars; }
         uint_set const& bail_vars() const { return m_bail_vars; }
 
+        unsigned level() const { return m_level; }
+
         conflict_kind_t kind() const { return m_kind; }
         bool is_bailout() const { return m_kind == conflict_kind_t::bailout; }
         bool is_backtracking() const { return m_kind == conflict_kind_t::backtrack; }
@@ -142,6 +148,8 @@ namespace polysat {
         bool is_relevant_pvar(pvar v) const;
         bool is_relevant(sat::literal lit) const;
 
+        /** conflict due to obvious input inconsistency */
+        void init_at_base_level();
         /** conflict because the constraint c is false under current variable assignment */
         void init(signed_constraint c);
         /** boolean conflict with the given clause */

src/math/polysat/solver.cpp

@@ -185,14 +185,21 @@ namespace polysat {
         LOG("New constraint: " << c);
         switch (m_bvars.value(lit)) {
         case l_false:
-            set_conflict(c);
+            // Input literal contradicts current boolean state (e.g., opposite literals in the input)
+            // => conflict only flags the inconsistency
+            set_conflict_at_base_level();
             SASSERT(dep == null_dependency && "track dependencies is TODO");
-            break;
+            return;
         case l_true:
             // constraint c is already asserted
             SASSERT(m_bvars.level(lit) <= m_level);
             break;
         case l_undef:
+            if (c.is_always_false()) {
+                // 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);
@@ -915,9 +922,10 @@ namespace polysat {
     }
 
     void solver::pop(unsigned num_scopes) {
-        unsigned base_level = m_base_levels[m_base_levels.size() - num_scopes];
+        unsigned const base_level = m_base_levels[m_base_levels.size() - num_scopes];
-        LOG("Pop " << num_scopes << " user scopes; lowest popped level = " << base_level << "; current level = " << m_level);
+        LOG("Pop " << num_scopes << " user scopes");
         pop_levels(m_level - base_level + 1);
+        if (m_level < m_conflict.level())
             m_conflict.reset();
         m_base_levels.shrink(m_base_levels.size() - num_scopes);
     }

src/math/polysat/solver.h

@@ -185,6 +185,7 @@ namespace polysat {
         void erase_pwatch(pvar v, constraint* c);
         void erase_pwatch(constraint* c);
 
+        void set_conflict_at_base_level() { m_conflict.init_at_base_level(); }
         void set_conflict(signed_constraint c) { m_conflict.init(c); }
         void set_conflict(clause& cl) { m_conflict.init(cl); }
         void set_conflict(pvar v, bool by_viable_fallback) { m_conflict.init(v, by_viable_fallback); }
@@ -428,6 +429,7 @@ namespace polysat {
         solver const& s;
         sat::literal lit;
     public:
+        lit_pp(solver const& s, signed_constraint c): s(s), lit(c.blit()) {}
         lit_pp(solver const& s, sat::literal lit): s(s), lit(lit) {}
         std::ostream& display(std::ostream& out) const;
     };

src/test/polysat.cpp

@@ -1121,18 +1121,25 @@ namespace polysat {
             }
         }
 
-        // Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases
+        static void test_pop_conflict() {
-        // NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later)
+            scoped_solver s(__func__);
-        // static void test_mixed_vars() {
+            auto a = s.var(s.add_var(32));
-        //     scoped_solver s(__func__);
+            s.add_ule(a, 5);
-        //     auto a = s.var(s.add_var(2));
+            s.push();
-        //     auto b = s.var(s.add_var(4));
+            s.add_ult(5, a);
-        //     auto c = s.var(s.add_var(2));
+            s.push();
-        //     s.add_eq(a + 2*c + 4);
+            s.add_ule(1, a);
-        //     s.add_eq(3*b + 4);
+            s.check();
-        //     s.check();
+            s.expect_unsat();
-        //     // Expected result:
+            s.pop();
-        // }
+            s.check();
+            s.expect_unsat();
+            s.pop();
+            s.add_ult(4, a);
+            // s.add_ule(100, a);
+            s.check();
+            s.expect_sat({{a, 5}});
+        }
 
     };  // class test_polysat