handle empty clauses created as lemmas as unsat state.

add unit tests

src/math/dd/dd_pdd.cpp

@@ -1643,6 +1643,13 @@ namespace dd {
         return *this; 
     }
 
+    pdd& pdd::operator=(unsigned k) {
+        m.dec_ref(root);
+        root = m.mk_val(k).root;
+        m.inc_ref(root);
+        return *this;
+    }
+
     std::ostream& operator<<(std::ostream& out, pdd const& b) { return b.display(out); }
 
     void pdd_iterator::next() {

src/math/dd/dd_pdd.h

@@ -386,6 +386,7 @@ namespace dd {
         pdd(pdd const& other): root(other.root), m(other.m) { m.inc_ref(root); }
         pdd(pdd && other) noexcept : root(0), m(other.m) { std::swap(root, other.root); }
         pdd& operator=(pdd const& other);
+        pdd& operator=(unsigned k);
         ~pdd() { m.dec_ref(root); }
         pdd lo() const { return pdd(m.lo(root), m); }
         pdd hi() const { return pdd(m.hi(root), m); }

src/math/polysat/clause.cpp

@@ -51,6 +51,14 @@ namespace polysat {
                 out << " \\/ ";
             out << lit;
         }
+        if (m_dep) {
+            ptr_vector<p_dependency> todo;
+            todo.push_back(m_dep.get());
+            vector<unsigned, false> vs;
+            poly_dep_manager::linearize_todo(todo, vs);
+            out << " deps ...";
+     //       out << "| " << vs;
+        }
         return out;
     }
 

src/math/polysat/conflict_core.cpp

@@ -215,7 +215,7 @@ namespace polysat {
             s().assign_bool(s().level(*lemma), c.blit(), lemma.get(), nullptr);
     }
 
-    clause_builder conflict_core::build_core_lemma() {
+    clause_builder conflict_core::build_lemma() {
         LOG_H3("Build lemma from core");
         LOG("core: " << *this);
         clause_builder lemma(s());
@@ -243,9 +243,6 @@ namespace polysat {
         return lemma;
     }
 
-    clause_builder conflict_core::build_lemma() {
-        return build_core_lemma();
-    }
 
     bool conflict_core::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {
         // NOTE:

src/math/polysat/conflict_core.h

@@ -105,7 +105,6 @@ namespace polysat {
 
         /** Convert the core into a lemma to be learned. */
         clause_builder build_lemma();
-        clause_builder build_core_lemma();
 
         bool try_eliminate(pvar v);
         bool try_saturate(pvar v);

src/math/polysat/solver.cpp

@@ -57,7 +57,7 @@ namespace polysat {
             (m_stats.m_num_decisions < m_max_decisions);
     }
    
-    lbool solver::check_sat() { 
+    lbool solver::check_sat() {         
         LOG("Starting");
         while (inc()) {
             m_stats.m_num_iterations++;
@@ -520,7 +520,7 @@ namespace polysat {
         LOG_H3("resolve_bool: " << lit << " " << other);
         m_conflict.resolve(m_constraints, var, other);
     }
-
+    
     void solver::report_unsat() {
         backjump(base_level());
         SASSERT(!m_conflict.empty());
@@ -565,9 +565,11 @@ namespace polysat {
                 return;
             case l_false:
                 continue;
-            default:
-                if (lit2cnstr(lit).is_currently_false(*this))
+            default:                
+                if (lit2cnstr(lit).is_currently_false(*this)) {
+                    num_choices++;
                     continue;
+                }
                 break;
             }
             num_choices++;
@@ -601,6 +603,10 @@ namespace polysat {
         SASSERT(m_justification[v].is_decision());
 
         clause_ref lemma = m_conflict.build_lemma().build();
+        if (lemma->empty()) {
+            report_unsat();
+            return;
+        }
         m_conflict.reset();
 
         backjump(get_level(v) - 1);
@@ -644,7 +650,7 @@ namespace polysat {
         //      again L is in core, unless we core-reduced it away
 
         clause_builder reason_builder = m_conflict.build_lemma();
-        m_conflict.reset();
+        
 
         bool contains_lit = std::find(reason_builder.begin(), reason_builder.end(), ~lit);
         if (!contains_lit) {
@@ -662,6 +668,12 @@ namespace polysat {
         }
         clause_ref reason = reason_builder.build();
 
+        if (reason->empty()) {
+            report_unsat();
+            return;
+        }
+        m_conflict.reset();
+
         std::cout << "reason " << *reason << "\n";
 
         // The lemma where 'lit' comes from.
@@ -751,6 +763,8 @@ namespace polysat {
             LOG("   Literal " << lit << " is: " << lit2cnstr(lit));
             SASSERT(m_bvars.value(lit) != l_true);
         }
+        if (lemma.empty())
+            std::cout << lemma << "\n";
         SASSERT(!lemma.empty());
         m_constraints.store(&lemma, *this);
         if (lemma.size() == 1) {

src/math/polysat/ule_constraint.cpp

@@ -31,6 +31,20 @@ Notes:
 
 namespace polysat {
 
+    ule_constraint::ule_constraint(constraint_manager& m, pdd const& l, pdd const& r) :
+        constraint(m, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
+        m_vars.append(l.free_vars());
+        for (auto v : r.free_vars())
+            if (!m_vars.contains(v))
+                m_vars.push_back(v);
+        if (m_lhs.is_val() && m_rhs.is_val()) {
+            if (m_lhs.val() <= m_rhs.val())
+                m_lhs = m_rhs = 0;
+            else
+                m_lhs = 1, m_rhs = 0;
+        }
+    }
+
     std::ostream& ule_constraint::display(std::ostream& out, lbool status) const {
         out << m_lhs;
         if (is_eq() && status == l_true) out << " == ";

src/math/polysat/ule_constraint.h

@@ -23,13 +23,7 @@ namespace polysat {
         pdd m_lhs;
         pdd m_rhs;
 
-        ule_constraint(constraint_manager& m, pdd const& l, pdd const& r):
-            constraint(m, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
-            m_vars.append(l.free_vars());
-            for (auto v : r.free_vars())
-                if (!m_vars.contains(v))
-                    m_vars.push_back(v);
-        }
+        ule_constraint(constraint_manager& m, pdd const& l, pdd const& r);
 
     public:
         ~ule_constraint() override {}

src/test/polysat.cpp

@@ -722,6 +722,18 @@ namespace polysat {
         s.expect_unsat();
     }
 
+    void permute_args(unsigned k, pdd& a, pdd& b, pdd& c) {
+        SASSERT(k < 6);
+        unsigned i = k % 3;
+        unsigned j = i % 2;
+        if (i == 1)
+            std::swap(a, b);
+        else if (i == 2)
+            std::swap(a, c);
+        if (j == 1)
+            std::swap(b, c);
+    }
+
     // xy < xz and !Omega(x*y) => y < z
     static void test_ineq_axiom1(unsigned bw = 32) {
         auto const bound = rational::power_of_two(bw-1);
@@ -751,53 +763,37 @@ namespace polysat {
             s.expect_unsat();
         }
 
-        for (unsigned i = 0; i < 3; ++i) {
-            for (unsigned j = 0; j < 2; ++j) {
-                scoped_solver s(__func__);
-                auto a = s.var(s.add_var(bw));
-                auto b = s.var(s.add_var(bw));
-                auto c = s.var(s.add_var(bw));
-                auto x = a, y = b, z = c;
-                if (i == 1)
-                    std::swap(x, y);
-                else if (i == 2)
-                    std::swap(x, z);
-                if (j == 1)
-                    std::swap(y, z);
-                s.add_ult(x * y, x * z);
-                s.add_ule(z, y);
-                s.add_ult(x, bound);
-                s.add_ult(y, bound);
-                s.check();
-                s.expect_unsat();
-            }
+        for (unsigned i = 0; i < 6; ++i) {
+            scoped_solver s(__func__);
+            auto x = s.var(s.add_var(bw));
+            auto y = s.var(s.add_var(bw));
+            auto z = s.var(s.add_var(bw));
+            permute_args(i, x, y, z);
+            s.add_ult(x * y, x * z);
+            s.add_ule(z, y);
+            s.add_ult(x, bound);
+            s.add_ult(y, bound);
+            s.check();
+            s.expect_unsat();
         }
     }
 
     // xy <= xz & !Omega(x*y) => y <= z or x = 0
     static void test_ineq_axiom2(unsigned bw = 32) {
         auto const bound = rational::power_of_two(bw - 1);
-        for (unsigned i = 0; i < 3; ++i) {
-            for (unsigned j = 0; j < 2; ++j) {
-                scoped_solver s(__func__);
-                auto a = s.var(s.add_var(bw));
-                auto b = s.var(s.add_var(bw));
-                auto c = s.var(s.add_var(bw));
-                auto x = a, y = b, z = c;
-                if (i == 1)
-                    std::swap(x, y);
-                else if (i == 2)
-                    std::swap(x, z);
-                if (j == 1)
-                    std::swap(y, z);
-                s.add_ult(x * y, x * z);
-                s.add_ult(z, y);
-                s.add_ult(x, bound);
-                s.add_ult(y, bound);
-                s.add_diseq(x);
-                s.check();
-                s.expect_unsat();
-            }
+        for (unsigned i = 0; i < 6; ++i) {
+            scoped_solver s(__func__);
+            auto x = s.var(s.add_var(bw));
+            auto y = s.var(s.add_var(bw));
+            auto z = s.var(s.add_var(bw));
+            permute_args(i, x, y, z);
+            s.add_ult(x * y, x * z);
+            s.add_ult(z, y);
+            s.add_ult(x, bound);
+            s.add_ult(y, bound);
+            s.add_diseq(x);
+            s.check();
+            s.expect_unsat();
         }
     }
 

src/util/dependency.h

@@ -47,6 +47,28 @@ public:
         value const& leaf_value() const { SASSERT(is_leaf()); return static_cast<leaf const*>(this)->m_value; }
     };
 
+    static void linearize_todo(ptr_vector<dependency>& todo, vector<value, false>& vs) {
+        unsigned qhead = 0;
+        while (qhead < todo.size()) {
+            dependency* d = todo[qhead];
+            qhead++;
+            if (d->is_leaf()) {
+                vs.push_back(to_leaf(d)->m_value);
+            }
+            else {
+                for (unsigned i = 0; i < 2; i++) {
+                    dependency* child = to_join(d)->m_children[i];
+                    if (!child->is_marked()) {
+                        todo.push_back(child);
+                        child->mark();
+                    }
+                }
+            }
+        }
+        for (auto* d : todo)
+            d->unmark();
+    }
+
 private:
     struct join : public dependency {
         dependency *    m_children[2];
@@ -191,26 +213,7 @@ public:
         return false;
     }
 
-    void linearize(vector<value, false>& vs) {
-        unsigned qhead = 0;
-        while (qhead < m_todo.size()) {
-            dependency * d = m_todo[qhead];
-            qhead++;
-            if (d->is_leaf()) {
-                vs.push_back(to_leaf(d)->m_value);
-            }
-            else {
-                for (unsigned i = 0; i < 2; i++) {
-                    dependency * child = to_join(d)->m_children[i];
-                    if (!child->is_marked()) {
-                        m_todo.push_back(child);
-                        child->mark();
-                    }
-                }
-            }
-        }
-        unmark_todo();
-    }
+
 
     void linearize(dependency * d, vector<value, false> & vs) {
         if (!d) 
@@ -218,7 +221,7 @@ public:
         m_todo.reset();
         d->mark();
         m_todo.push_back(d);
-        linearize(vs);
+        linearize_todo(m_todo, vs);
     }
 
     void linearize(ptr_vector<dependency>& deps, vector<value, false> & vs) {
@@ -231,7 +234,7 @@ public:
                 m_todo.push_back(d);
             }
         }
-        linearize(vs);
+        linearize_todo(m_todo, vs);
     }
 };