n/a

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/smt/polysat/core.cpp

@@ -218,7 +218,7 @@ namespace polysat {
         
         // If no saturation propagation was possible, explain the conflict using the variable assignment.
         m_unsat_core = explain_eval(get_constraint(conflict_idx));
-        m_unsat_core.push_back(conflict_idx);
+        m_unsat_core.push_back(m_constraint_index[conflict_idx.id].d);
         propagate_unsat_core();
         return sat::check_result::CR_CONTINUE;
     }
@@ -229,11 +229,11 @@ namespace polysat {
     svector<pvar> core::find_conflict_variables(constraint_id idx) {
         svector<pvar> result;
         auto [sc, d, value] = m_constraint_index[idx.id];
-        unsigned lvl = d.level();
+        unsigned lvl = s.level(d);
         for (auto v : sc.vars()) {
             if (!is_assigned(v))
                 continue;
-            auto new_level = m_constraint_index[m_justification[v].id].d.level();
+            auto new_level = s.level(m_constraint_index[m_justification[v].id].d);
             if (new_level < lvl)
                 continue;
             if (new_level > lvl)
@@ -367,7 +367,7 @@ namespace polysat {
             s.propagate(d, eval_value != l_true, explain_eval(sc));
         else if (value != eval_value) {
             m_unsat_core = explain_eval(sc);
-            m_unsat_core.push_back(id);
+            m_unsat_core.push_back(m_constraint_index[id.id].d);
             propagate_unsat_core();
         }                   
     }
@@ -406,15 +406,14 @@ namespace polysat {
         };
         m_prop_queue.push_back(index);
         m_constraint_index[index.id].value = to_lbool(!sign);
-        m_constraint_index[index.id].d.set_level(level);
         s.trail().push(unassign(*this, index.id));
     }
 
-    constraint_id_vector core::explain_eval(signed_constraint const& sc) { 
+    dependency_vector core::explain_eval(signed_constraint const& sc) {
-        constraint_id_vector deps;
+        dependency_vector deps;
         for (auto v : sc.vars()) 
             if (is_assigned(v))
-                deps.push_back(m_justification[v]);
+                deps.push_back(m_constraint_index[m_justification[v].id].d);
         return deps;
     }
 

src/sat/smt/polysat/core.h

@@ -56,7 +56,7 @@ namespace polysat {
         unsigned m_qhead = 0;
         constraint_id_vector m_prop_queue;
         svector<constraint_info> m_constraint_index;  // index of constraints
-        constraint_id_vector m_unsat_core;
+        dependency_vector m_unsat_core;
         random_gen           m_rand;
 
 
@@ -84,13 +84,8 @@ namespace polysat {
         void propagate_unsat_core();
         void propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d);
 
-
-
-
         void add_watch(unsigned idx, unsigned var);
 
-
-
         sat::check_result final_check();
         svector<pvar> find_conflict_variables(constraint_id idx);
 
@@ -157,14 +152,14 @@ namespace polysat {
         * Saturation
         */
         signed_constraint get_constraint(constraint_id id);
-        constraint_id_vector const& unsat_core() const { return m_unsat_core; }
+        dependency_vector const& unsat_core() const { return m_unsat_core; }
         constraint_id_vector const& assigned_constraints() const { return m_prop_queue; }
         dependency get_dependency(constraint_id idx) const;
         dependency_vector get_dependencies(constraint_id_vector const& ids) const;
         lbool eval(constraint_id id);
-        dependency propagate(signed_constraint const& sc, constraint_id_vector const& ids) { return s.propagate(sc, ids); }
+        dependency propagate(signed_constraint const& sc, dependency_vector const& deps) { return s.propagate(sc, deps); }
         lbool eval(signed_constraint const& sc);
-        constraint_id_vector explain_eval(signed_constraint const& sc);
+        dependency_vector explain_eval(signed_constraint const& sc);
         bool inconsistent() const;
 
         /*

src/sat/smt/polysat/saturation.cpp

@@ -60,7 +60,7 @@ namespace polysat {
     }
 
     void saturation::propagate(signed_constraint const& sc, std::initializer_list<constraint_id> const& premises) {
-        c.propagate(sc, constraint_id_vector(premises));        
+        // c.propagate(sc, constraint_id_vector(premises));        
     }
 
     void saturation::add_clause(char const* name, clause const& cs, bool is_redundant) { 
@@ -84,17 +84,6 @@ namespace polysat {
         SASSERT(c.inconsistent());
     }
 
-    bool saturation::match_core(std::function<bool(signed_constraint const& sc)> const& p, constraint_id& id_out) {
-        for (auto id : c.unsat_core()) {
-            auto sc = c.get_constraint(id);
-            if (p(sc)) {
-                id_out = id;
-                return true;
-            }
-        }
-        return false;
-    }
-
     bool saturation::match_constraints(std::function<bool(signed_constraint const& sc)> const& p, constraint_id& id_out) {
         for (auto id : c.assigned_constraints()) {
             auto sc = c.get_constraint(id);
@@ -110,21 +99,6 @@ namespace polysat {
         return is_strict ? c.cs().ult(x, y) : c.cs().ule(x, y);
     }
 
-    /**
-     * TODO: this does not belong in saturation, but on the fly? 
-     * p <= q, q <= p => p = q
-     */
-    void saturation::propagate_infer_equality(pvar x, inequality const& i) {
-        if (i.is_strict())
-            return;
-        if (i.lhs().degree(x) == 0 && i.rhs().degree(x) == 0)
-            return;
-        constraint_id id;
-        if (!match_core([&](auto const& sc) { return sc.is_ule() && !sc.sign() && sc.to_ule().lhs() == i.rhs() && sc.to_ule().rhs() == i.lhs(); }, id))
-            return;
-        c.propagate(c.eq(i.lhs(), i.rhs()), { id, i.id() });     
-    }
-
     /**
      * Implement the inferences
      *  [x] yx < zx   ==>  Ω*(x,y) \/ y < z

src/sat/smt/polysat/saturation.h

@@ -60,8 +60,6 @@ namespace polysat {
             constraint_filter end() const { return constraint_filter(c, m_filter, c.assigned_constraints().size()); }
         };
         
-
-        bool match_core(std::function<bool(signed_constraint const& sc)> const& p, constraint_id& id);
         bool match_constraints(std::function<bool(signed_constraint const& sc)> const& p, constraint_id& id);
 
         void propagate_infer_equality(pvar x, inequality const& a_l_b);

src/sat/smt/polysat/types.h

@@ -38,12 +38,11 @@ namespace polysat {
     class dependency {
         struct axiom_t {};
         std::variant<axiom_t, sat::literal, theory_var_pair, offset_claim> m_data;
-        unsigned m_level;
+        dependency(): m_data(axiom_t()) {}
-        dependency(): m_data(axiom_t()), m_level(0) {}
     public:
-        dependency(sat::literal lit, unsigned level) : m_data(lit), m_level(level) {}
+        dependency(sat::literal lit) : m_data(lit){}
-        dependency(theory_var v1, theory_var v2, unsigned level) : m_data(std::make_pair(v1, v2)), m_level(level) {} 
+        dependency(theory_var v1, theory_var v2) : m_data(std::make_pair(v1, v2)) {} 
-        dependency(offset_claim const& c, unsigned level) : m_data(c), m_level(level) {}
+        dependency(offset_claim const& c) : m_data(c) {}
         static dependency axiom() { return dependency(); } 
         bool is_null() const { return is_literal() && *std::get_if<sat::literal>(&m_data) == sat::null_literal; }
         bool is_axiom() const { return std::holds_alternative<axiom_t>(m_data); }
@@ -53,25 +52,23 @@ namespace polysat {
         sat::literal literal() const { SASSERT(is_literal()); return *std::get_if<sat::literal>(&m_data); }
         theory_var_pair eq() const { SASSERT(!is_literal()); return *std::get_if<theory_var_pair>(&m_data); }
         offset_claim offset() const { return *std::get_if<offset_claim>(&m_data); }
-        unsigned level() const { return m_level; }
+        dependency operator~() const { SASSERT(is_literal()); return dependency(~literal()); }
-        void set_level(unsigned level) { m_level = level; }
-        dependency operator~() const { SASSERT(is_literal()); return dependency(~literal(), level()); }
     };
 
-    inline const dependency null_dependency = dependency(sat::null_literal, UINT_MAX);
+    inline const dependency null_dependency = dependency(sat::null_literal);
 
     inline std::ostream& operator<<(std::ostream& out, dependency d) {
         if (d.is_null())
             return out << "null";
         else if (d.is_axiom())
-            return out << "axiom@" << d.level();
+            return out << "axiom";
         else if (d.is_literal())
-            return out << d.literal() << "@" << d.level();
+            return out << d.literal();
         else if (d.is_eq())
-            return out << "v" << d.eq().first << " == v" << d.eq().second << "@" << d.level();
+            return out << "v" << d.eq().first << " == v" << d.eq().second;
         else {
             auto [v1, v2, offset] = d.offset();
-            return out << "v" << v1 << " == v" << v2 << " offset " << offset << "@" << d.level();
+            return out << "v" << v1 << " == v" << v2 << " offset " << offset;
         }
     }
 
@@ -114,15 +111,16 @@ namespace polysat {
         virtual ~solver_interface() {}
         virtual void add_eq_literal(pvar v, rational const& val) = 0;
         virtual bool add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool redundant) = 0;
-        virtual void set_conflict(constraint_id_vector const& core) = 0;
+        virtual void set_conflict(dependency_vector const& core) = 0;
-        virtual dependency propagate(signed_constraint sc, constraint_id_vector const& deps) = 0;
+        virtual dependency propagate(signed_constraint sc, dependency_vector const& deps) = 0;
-        virtual void propagate(dependency const& d, bool sign, constraint_id_vector const& deps) = 0;
+        virtual void propagate(dependency const& d, bool sign, dependency_vector const& deps) = 0;
         virtual trail_stack& trail() = 0;
         virtual bool inconsistent() const = 0;
         virtual void get_bitvector_suffixes(pvar v, offset_slices& out) = 0;
         virtual void get_bitvector_sub_slices(pvar v, offset_slices& out) = 0;
         virtual void get_bitvector_super_slices(pvar v, offset_slices& out) = 0;
         virtual void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits) = 0;
+        virtual unsigned level(dependency const& d) = 0;
     };
 
 }

src/sat/smt/polysat/viable.cpp

@@ -466,12 +466,12 @@ namespace polysat {
     /*
     * Explain why the current variable is not viable or signleton.
     */
-    constraint_id_vector viable::explain() { 
+    dependency_vector viable::explain() {
-        constraint_id_vector result;
+        dependency_vector result;
         for (auto e : m_explain) {
             auto index = e->constraint_index;
             auto const& [sc, d, value] = c.m_constraint_index[index];
-            result.push_back({ index });
+            result.push_back(d);
             result.append(c.explain_eval(sc));
         }
         // TODO: explaination for fixed bits

src/sat/smt/polysat/viable.h

@@ -261,7 +261,7 @@ namespace polysat {
         /*
         * Explain why the current variable is not viable or signleton.
         */
-        constraint_id_vector explain();
+        dependency_vector explain();
 
         /*
         * flag whether there is a forbidden interval core

src/sat/smt/polysat_internalize.cpp

@@ -182,7 +182,7 @@ namespace polysat {
         if (get_bv2a(bv))
             return;
         sat::literal lit(bv, false);
-        auto index = m_core.register_constraint(sc, dependency(lit, 0));
+        auto index = m_core.register_constraint(sc, dependency(lit));
         auto a = new (get_region()) atom(bv, index);
         insert_bv2a(bv, a);
         ctx.push(mk_atom_trail(bv, *this));

src/sat/smt/polysat_solver.cpp

@@ -105,9 +105,7 @@ namespace polysat {
         m_core.assign_eh(a->m_index, l.sign(), s().lvl(l));
     }
 
-    // TBD: add also lemma
+    void solver::set_conflict(dependency_vector const& deps) {
-    void solver::set_conflict(constraint_id_vector const& core) {
-        auto deps = m_core.get_dependencies(core);
         auto [lits, eqs] = explain_deps(deps);
         auto ex = euf::th_explain::conflict(*this, lits, eqs, nullptr);
         ctx.set_conflict(ex);
@@ -164,7 +162,7 @@ namespace polysat {
         auto sc = m_core.eq(p, q);        
         m_var_eqs.setx(m_var_eqs_head, {v1, v2}, {v1, v2});
         ctx.push(value_trail<unsigned>(m_var_eqs_head));    
-        auto d = dependency(v1, v2, s().scope_lvl());
+        auto d = dependency(v1, v2);
         constraint_id id = m_core.register_constraint(sc, d);
         m_core.assign_eh(id, false, s().scope_lvl()); 
         m_var_eqs_head++;
@@ -179,7 +177,7 @@ namespace polysat {
         pdd q = var2pdd(v2);
         auto sc = ~m_core.eq(p, q);
         sat::literal neq = ~expr2literal(ne.eq());
-        auto d = dependency(neq, s().lvl(neq));
+        auto d = dependency(neq);
         auto id = m_core.register_constraint(sc, d);
         TRACE("bv", tout << neq << " := " << s().value(neq) << " @" << s().scope_lvl() << "\n");
         m_core.assign_eh(id, false, s().lvl(neq));
@@ -189,27 +187,47 @@ namespace polysat {
     // The polysat::solver takes care of translating signed constraints into expressions, which translate into literals.
     // Everything goes over expressions/literals. polysat::core is not responsible for replaying expressions. 
     
-    dependency solver::propagate(signed_constraint sc, constraint_id_vector const& cs) {
+    dependency solver::propagate(signed_constraint sc, dependency_vector const& deps) {
         sat::literal lit = ctx.mk_literal(constraint2expr(sc));        
         if (s().value(lit) == l_true)
-            return dependency(lit, s().lvl(lit));
+            return dependency(lit);
-        auto deps = m_core.get_dependencies(cs);
         auto [core, eqs] = explain_deps(deps);
         auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr);        
-        unsigned level = 0;
-        for (auto c : core)
-            level = std::max(level, s().lvl(c));
-        sat::literal_vector eqlits;
-        for (auto [n1, n2] : eqs) 
-            ctx.get_eq_antecedents(n1, n2, eqlits);
-        for (auto lit : eqlits)
-            level = std::max(level, s().lvl(lit));
         ctx.propagate(lit, ex);
-        return dependency(lit, level); 
+        return dependency(lit); 
     }
 
-    void solver::propagate(dependency const& d, bool sign, constraint_id_vector const& cs) {
+    unsigned solver::level(dependency const& d) {
-        auto deps = m_core.get_dependencies(cs);
+        if (d.is_literal())
+            return s().lvl(d.literal());
+        else if (d.is_eq()) {
+            auto [v1, v2] = d.eq();
+            sat::literal_vector lits;
+            ctx.get_eq_antecedents(var2enode(v1), var2enode(v2), lits);
+            unsigned level = 0;
+            for (auto lit : lits)
+                level = std::max(level, s().lvl(lit));
+            return level;
+        }
+        else if (d.is_offset_claim()) {
+            auto [v, w, offset] = d.offset();
+            sat::literal_vector lits;
+            std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
+                ctx.get_eq_antecedents(a, b, lits);                
+                };
+            explain_slice(v, w, offset, consume);
+            unsigned level = 0;
+            for (auto lit : lits)
+                level = std::max(level, s().lvl(lit));
+            return level;
+        }
+        else {
+            SASSERT(d.is_axiom());
+            return 0;
+        }
+    }
+
+    void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps) {
         auto [core, eqs] = explain_deps(deps);
         if (d.is_literal()) {
             auto lit = d.literal();

src/sat/smt/polysat_solver.h

@@ -166,16 +166,17 @@ namespace polysat {
 
         // callbacks from core
         void add_eq_literal(pvar v, rational const& val) override;
-        void set_conflict(constraint_id_vector const& core) override;
+        void set_conflict(dependency_vector const& core) override;
         bool add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool redundant) override;
-        dependency propagate(signed_constraint sc, constraint_id_vector const& deps) override;
+        dependency propagate(signed_constraint sc, dependency_vector const& deps) override;
-        void propagate(dependency const& d, bool sign, constraint_id_vector const& deps) override;
+        void propagate(dependency const& d, bool sign, dependency_vector const& deps) override;
         trail_stack& trail() override;
         bool inconsistent() const override;
         void get_bitvector_sub_slices(pvar v, offset_slices& out) override;
         void get_bitvector_super_slices(pvar v, offset_slices& out) override;
         void get_bitvector_suffixes(pvar v, offset_slices& out) override;
         void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits) override;
+        unsigned level(dependency const& d) override;
         dependency explain_slice(pvar v, pvar w, unsigned offset);
 
         bool add_axiom(char const* name, constraint_or_dependency_list const& clause, bool redundant) {