Polysat: forbidden intervals updates (#5230)

* Pop assign_eh

* Fix scoped_ptr_vector constructors, add detach()

* Need to copy the returned lemma

* Add test

* Basic inequality tests

* Return disjunctive lemma to caller

src/math/polysat/constraint.h

@@ -62,6 +62,7 @@ namespace polysat {
         bool_var bvar() const { return m_bool_var; }
         bool sign() const { return m_sign; }
         void assign_eh(bool is_true) { m_status = (is_true ^ !m_sign) ? l_true : l_false; }
+        void unassign_eh() { m_status = l_undef; }
         bool is_positive() const { return m_status == l_true; }
         bool is_negative() const { return m_status == l_false; }
         bool is_undef() const { return m_status == l_undef; }
@@ -70,5 +71,26 @@ namespace polysat {
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
 
+    class clause {
+        scoped_ptr_vector<constraint> m_literals;
+    public:
+        clause() {}
+        clause(scoped_ptr_vector<constraint>&& literals): m_literals(std::move(literals)) {
+            SASSERT(std::all_of(m_literals.begin(), m_literals.end(), [](constraint* c) { return c != nullptr; }));
+            SASSERT(empty() || std::all_of(m_literals.begin(), m_literals.end(), [this](constraint* c) { return c->level() == level(); }));
+        }
+
+        bool empty() const { return m_literals.empty(); }
+        unsigned size() const { return m_literals.size(); }
+        constraint* operator[](unsigned idx) const { return m_literals[idx]; }
+
+        using const_iterator = typename scoped_ptr_vector<constraint>::const_iterator;
+        const_iterator begin() const { return m_literals.begin(); }
+        const_iterator end() const { return m_literals.end(); }
+
+        ptr_vector<constraint> detach() { return m_literals.detach(); }
+
+        unsigned level() const { SASSERT(!empty()); return m_literals[0]->level(); }
+    };
 
 }

src/math/polysat/forbidden_intervals.cpp

@@ -62,7 +62,7 @@ namespace polysat {
         return true;
     }
 
-    bool forbidden_intervals::explain(solver& s, ptr_vector<constraint> const& conflict, pvar v, scoped_ptr_vector<constraint>& out_lemma) {
+    bool forbidden_intervals::explain(solver& s, ptr_vector<constraint> const& conflict, pvar v, clause& out_lemma) {
 
         // Extract forbidden intervals from conflicting constraints
         vector<fi_record> records;
@@ -137,6 +137,7 @@ namespace polysat {
         // - the upper bound of each interval is contained in the next interval,
         // then the forbidden intervals cover the whole domain and we have a conflict.
         // We learn the negation of this conjunction.
+        scoped_ptr_vector<constraint> literals;
         for (unsigned seq_i = seq.size(); seq_i-- > 0; ) {
             unsigned const i = seq[seq_i];
             unsigned const next_i = seq[(seq_i+1) % seq.size()];
@@ -149,14 +150,15 @@ namespace polysat {
             auto const& rhs = next_hi - next_lo;
             constraint* c = constraint::ult(lemma_lvl, s.m_next_bvar++, neg_t, lhs, rhs, lemma_dep);
             LOG("constraint: " << *c);
-            out_lemma.push_back(c);
+            literals.push_back(c);
             // Side conditions
             // TODO: check whether the condition is subsumed by c?  maybe at the end do a "lemma reduction" step, to try and reduce branching?
             scoped_ptr<constraint>& cond = records[i].cond;
             if (cond)
-                out_lemma.push_back(cond.detach());
+                literals.push_back(cond.detach());
         }
 
+        out_lemma = std::move(literals);
         return true;
     }
 

src/math/polysat/forbidden_intervals.h

@@ -23,7 +23,7 @@ namespace polysat {
     class forbidden_intervals {
 
     public:
-        static bool explain(solver& s, ptr_vector<constraint> const& conflict, pvar v, scoped_ptr_vector<constraint>& out_lemma);
+        static bool explain(solver& s, ptr_vector<constraint> const& conflict, pvar v, clause& out_lemma);
 
     };
 }

src/math/polysat/solver.cpp

@@ -102,7 +102,8 @@ namespace polysat {
     }
     
     lbool solver::check_sat() { 
-        TRACE("polysat", tout << "check\n";);
+        LOG("Starting");
+        m_disjunctive_lemma.reset();
         while (m_lim.inc()) {
             LOG_H1("Next solving loop iteration");
             LOG("Free variables: " << m_free_vars);
@@ -114,7 +115,8 @@ namespace polysat {
                 }
             });
 
-            if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
+            if (pending_disjunctive_lemma()) { LOG_H2("UNDEF (handle lemma externally)"); return l_undef; }
+            else if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
             else if (is_conflict()) resolve_conflict();
             else if (can_propagate()) propagate();
             else if (!can_decide()) { LOG_H2("SAT"); return l_true; }
@@ -141,7 +143,6 @@ namespace polysat {
     void solver::del_var() {
         // TODO also remove v from all learned constraints.
         pvar v = m_viable.size() - 1;
-        m_free_vars.del_var_eh(v);
         m_viable.pop_back();
         m_cjust.pop_back();
         m_value.pop_back();
@@ -222,6 +223,8 @@ namespace polysat {
         }
         c->assign_eh(is_true);
         add_watch(*c);
+        m_assign_eh_history.push_back(v);
+        m_trail.push_back(trail_instr_t::assign_eh_i);
         c->narrow(*this);
     }
 
@@ -263,6 +266,7 @@ namespace polysat {
     }
 
     void solver::pop_levels(unsigned num_levels) {
+        LOG("Pop " << num_levels << " levels; current level is " << m_level);
         while (num_levels > 0) {
             switch (m_trail.back()) {
             case trail_instr_t::qhead_i: {
@@ -297,6 +301,14 @@ namespace polysat {
                 m_cjust_trail.pop_back();
                 break;
             }
+            case trail_instr_t::assign_eh_i: {
+                auto bvar = m_assign_eh_history.back();
+                constraint* c = get_bv2c(bvar);
+                erase_watch(*c);
+                c->unassign_eh();
+                m_assign_eh_history.pop_back();
+                break;
+            }
             default:
                 UNREACHABLE();
             }
@@ -375,7 +387,6 @@ namespace polysat {
             ++m_stats.m_num_decisions;
         else 
             ++m_stats.m_num_propagations;
-        TRACE("polysat", tout << "v" << v << " := " << val << " " << j << "\n";);
         LOG("pvar " << v << " := " << val << " by " << j);
         SASSERT(is_viable(v, val));
         m_value[v] = val;
@@ -385,15 +396,15 @@ namespace polysat {
     }
 
     void solver::set_conflict(constraint& c) { 
+        LOG("conflict: " << c);
         SASSERT(m_conflict.empty());
-        TRACE("polysat", tout << "conflict " << c << "\n";);
         m_conflict.push_back(&c); 
     }
 
     void solver::set_conflict(pvar v) {
         SASSERT(m_conflict.empty());
         m_conflict.append(m_cjust[v]);
-        TRACE("polysat", tout << "conflict "; for (auto* c : m_conflict) tout << *c << "\n";);
+        LOG("conflict for pvar " << v << ": " << m_conflict);
         if (m_cjust[v].empty())
             m_conflict.push_back(nullptr);
     }
@@ -440,14 +451,27 @@ namespace polysat {
 
         if (conflict_var != null_var) {
             LOG_H2("Conflict due to empty viable set for pvar " << conflict_var);
-            scoped_ptr_vector<constraint> disjunctive_lemma;
+            clause new_lemma;
-            if (forbidden_intervals::explain(*this, m_conflict, conflict_var, disjunctive_lemma)) {
+            if (forbidden_intervals::explain(*this, m_conflict, conflict_var, new_lemma)) {
-                LOG_H3("Learning disjunctive lemma"); // << disjunctive_lemma);
+                LOG_H3("Learning disjunctive lemma");
-                SASSERT(disjunctive_lemma.size() > 0);
+                SASSERT(new_lemma.size() > 0);
-                if (disjunctive_lemma.size() == 1) {
+                if (new_lemma.size() == 1) {
+                    lemma = new_lemma.detach()[0];
                     // TODO: continue normally?
                 } else {
-                    // TODO: solver needs to return l_undef and allow external handling of disjunctive lemma
+                    SASSERT(m_disjunctive_lemma.empty());
+                    reset_marks();
+                    for (constraint* c : new_lemma) {
+                        m_disjunctive_lemma.push_back(c->bvar());
+                        insert_bv2c(c->bvar(), c);
+                        for (auto v : c->vars())
+                            set_mark(v);
+                    }
+                    m_redundant_clauses.push_back(std::move(new_lemma));
+                    backtrack(m_search.size()-1, lemma);
+                    SASSERT(pending_disjunctive_lemma());
+                    m_conflict.reset();
+                    return;
                 }
             }
         }
@@ -635,13 +659,15 @@ namespace polysat {
     }
 
     void solver::push() {
+        LOG("Push user scope");
         push_level();
         m_base_levels.push_back(m_level);
     }
 
     void solver::pop(unsigned num_scopes) {
         unsigned base_level = m_base_levels[m_base_levels.size() - num_scopes];
-        pop_levels(m_level - base_level - 1);
+        LOG("Pop " << num_scopes << " user scopes; lowest popped level = " << base_level << "; current level = " << m_level);
+        pop_levels(m_level - base_level + 1);
     }
 
     bool solver::at_base_level() const {

src/math/polysat/solver.h

@@ -65,6 +65,10 @@ namespace polysat {
         // Per constraint state
         scoped_ptr_vector<constraint>   m_constraints;
         scoped_ptr_vector<constraint>   m_redundant;
+        vector<clause>                  m_redundant_clauses;
+
+        bool_var_vector          m_disjunctive_lemma;
+        bool_var_vector          m_assign_eh_history;
 
         // Map boolean variables to constraints
         bool_var                 m_next_bvar = 2;  // TODO: later, bool vars come from external supply
@@ -249,7 +253,8 @@ namespace polysat {
          * Returns the disjunctive lemma that should be learned,
          * or an empty vector if check_sat() terminated for a different reason.
          */
-        bool_var_vector get_lemma() { NOT_IMPLEMENTED_YET(); return {}; };
+        bool_var_vector get_lemma() { return m_disjunctive_lemma; }
+        bool pending_disjunctive_lemma() { return !m_disjunctive_lemma.empty(); }
 
         /**
          * retrieve unsat core dependencies

src/math/polysat/trail.h

@@ -22,7 +22,8 @@ namespace polysat {
         inc_level_i,
         viable_i,
         assign_i,
-        just_i
+        just_i,
+        assign_eh_i,
     };
 
     

src/test/polysat.cpp

@@ -16,7 +16,7 @@ namespace polysat {
             lbool result = check_sat();
             if (result != l_undef)
                 return result;
-            auto const& new_lemma = get_lemma();
+            auto const new_lemma = get_lemma();
             // Empty lemma => check_sat() terminated for another reason, e.g., resource limits
             if (new_lemma.empty())
                 return l_undef;
@@ -46,6 +46,24 @@ namespace polysat {
         }
     };
 
+
+    /**
+     * Testing the solver's internal state.
+     */
+
+    /// Creates two separate conflicts (from narrowing) before solving loop is started.
+    static void test_add_conflicts() {
+        scoped_solver s;
+        auto a = s.var(s.add_var(3));
+        auto b = s.var(s.add_var(3));
+        s.add_eq(a + 1);
+        s.add_eq(a + 2);
+        s.add_eq(b + 1);
+        s.add_eq(b + 2);
+        s.check();
+    }
+
+
     /**
      * most basic linear equation solving.
      * they should be solvable.
@@ -125,6 +143,73 @@ namespace polysat {
         s.check();
     }
 
+    // Unique solution: u = 5
+    static void test_ineq_basic1() {
+        scoped_solver s;
+        auto u = s.var(s.add_var(4));
+        auto zero = u - u;
+        s.add_ule(u, zero + 5);
+        s.add_ule(zero + 5, u);
+        s.check();
+    }
+
+    // Unsatisfiable
+    static void test_ineq_basic2() {
+        scoped_solver s;
+        auto u = s.var(s.add_var(4));
+        auto zero = u - u;
+        s.add_ult(u, zero + 5);
+        s.add_ule(zero + 5, u);
+        s.check();
+    }
+
+    // Solutions with u = v = w
+    static void test_ineq_basic3() {
+        scoped_solver s;
+        auto u = s.var(s.add_var(4));
+        auto v = s.var(s.add_var(4));
+        auto w = s.var(s.add_var(4));
+        s.add_ule(u, v);
+        s.add_ule(v, w);
+        s.add_ule(w, u);
+        s.check();
+    }
+
+    // Unsatisfiable
+    static void test_ineq_basic4() {
+        scoped_solver s;
+        auto u = s.var(s.add_var(4));
+        auto v = s.var(s.add_var(4));
+        auto w = s.var(s.add_var(4));
+        s.add_ule(u, v);
+        s.add_ult(v, w);
+        s.add_ule(w, u);
+        s.check();
+    }
+
+    // Satisfiable
+    // Without forbidden intervals, we just try values for u until it works
+    static void test_ineq_basic5() {
+        scoped_solver s;
+        auto u = s.var(s.add_var(4));
+        auto v = s.var(s.add_var(4));
+        auto zero = u - u;
+        s.add_ule(zero + 12, u + v);
+        s.add_ule(v, zero + 2);
+        s.check();
+    }
+
+    // Like 5 but the other forbidden interval will be the longest
+    static void test_ineq_basic6() {
+        scoped_solver s;
+        auto u = s.var(s.add_var(4));
+        auto v = s.var(s.add_var(4));
+        auto zero = u - u;
+        s.add_ule(zero + 14, u + v);
+        s.add_ule(v, zero + 2);
+        s.check();
+    }
+
 
     /**
      * Check unsat of:
@@ -290,6 +375,7 @@ namespace polysat {
 
 
 void tst_polysat() {
+    polysat::test_add_conflicts();
     polysat::test_l1();
     polysat::test_l2();
     polysat::test_l3();

src/util/scoped_ptr_vector.h

@@ -26,7 +26,22 @@ template<typename T>
 class scoped_ptr_vector {
     ptr_vector<T> m_vector;
 public:
+    scoped_ptr_vector() = default;
     ~scoped_ptr_vector() { reset(); }
+    scoped_ptr_vector(scoped_ptr_vector& other) = delete;
+    scoped_ptr_vector& operator=(scoped_ptr_vector& other) = delete;
+
+    scoped_ptr_vector(scoped_ptr_vector&& other) noexcept {
+        m_vector.swap(other.m_vector);
+    }
+    scoped_ptr_vector& operator=(scoped_ptr_vector&& other) {
+        if (this == &other)
+            return *this;
+        reset();
+        m_vector.swap(other.m_vector);
+        return *this;
+    }
+
     void reset() { std::for_each(m_vector.begin(), m_vector.end(), delete_proc<T>()); m_vector.reset(); }
     void push_back(T * ptr) { m_vector.push_back(ptr); }
     void pop_back() { SASSERT(!empty()); set(size()-1, nullptr); m_vector.pop_back(); }
@@ -65,7 +80,15 @@ public:
         ptr = m_vector.back();
         m_vector[m_vector.size()-1] = tmp;
     }
-    typename ptr_vector<T>::const_iterator begin() const { return m_vector.begin(); }
+
-    typename ptr_vector<T>::const_iterator end() const { return m_vector.end(); }
+    ptr_vector<T> detach() {
+        ptr_vector<T> tmp(std::move(m_vector));
+        SASSERT(m_vector.empty());
+        return tmp;
+    }
+
+    using const_iterator = typename ptr_vector<T>::const_iterator;
+    const_iterator begin() const { return m_vector.begin(); }
+    const_iterator end() const { return m_vector.end(); }
 };
 

src/util/vector.h

@@ -532,7 +532,7 @@ public:
         return m_data;
     }
 
-    void swap(vector & other) {
+    void swap(vector & other) noexcept {
         std::swap(m_data, other.m_data);
     }