From 022c06f75d18b702a314fdb9d3f974e264f6a7fe Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 18 Nov 2022 15:14:38 +0100
Subject: [PATCH 01/21] pdd::subst_get

---
 src/math/dd/dd_pdd.cpp | 15 ++++++++++++++-
 src/math/dd/dd_pdd.h   |  6 ++++--
 src/test/pdd.cpp       | 33 +++++++++++++++++++++++++++++++++
 3 files changed, 51 insertions(+), 3 deletions(-)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 39575bb66..edf582e19 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -185,7 +185,20 @@ namespace dd {
         pdd v_val = mk_var(v) + val;
         return pdd(apply(s.root, v_val.root, pdd_subst_add_op), this);
     }
-    
+
+    bool pdd_manager::subst_get(pdd const& s, unsigned v, rational& out_val) {
+        unsigned level_v = m_var2level[v];
+        PDD p = s.root;
+        while (/* !is_val(p) && */ level(p) > level_v) {
+            SASSERT(is_val(lo(p)));
+            p = hi(p);
+        }
+        if (!is_val(p) && level(p) == level_v) {
+            out_val = val(lo(p));
+            return true;
+        }
+        return false;
+    }
 
     pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) {
         bool first = true;
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 6c7497461..506a9b853 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -10,7 +10,7 @@ Abstract:
     Poly DD package
 
     It is a mild variant of ZDDs. 
-    In PDDs arithmetic is either standard or using mod 2 (over GF2).
+    In PDDs arithmetic is either standard or using mod 2^n.
 
     Non-leaf nodes are of the form x*hi + lo
     where 
@@ -343,6 +343,7 @@ namespace dd {
         pdd subst_val(pdd const& a, unsigned v, rational const& val);
         pdd subst_val(pdd const& a, pdd const& s);
         pdd subst_add(pdd const& s, unsigned v, rational const& val);
+        bool subst_get(pdd const& s, unsigned v, rational& out_val);
         bool resolve(unsigned v, pdd const& p, pdd const& q, pdd& r);
         pdd reduce(unsigned v, pdd const& a, pdd const& b);
         void quot_rem(pdd const& a, pdd const& b, pdd& q, pdd& r);
@@ -459,7 +460,8 @@ namespace dd {
         pdd subst_val0(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val0(*this, s); }
         pdd subst_val(pdd const& s) const { return m.subst_val(*this, s); }
         pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }
-        pdd subst_add(unsigned var, rational const& val) { return m.subst_add(*this, var, val); }
+        pdd subst_add(unsigned var, rational const& val) const { return m.subst_add(*this, var, val); }
+        bool subst_get(unsigned var, rational& out_val) const { return m.subst_get(*this, var, out_val); }
 
         /**
          * \brief substitute variable v by r.
diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp
index a0946d81d..0c9b0f85c 100644
--- a/src/test/pdd.cpp
+++ b/src/test/pdd.cpp
@@ -571,6 +571,38 @@ public:
         }
     }
 
+    static void subst_get() {
+        std::cout << "subst_get\n";
+        pdd_manager m(4, pdd_manager::mod2N_e, 32);
+
+        unsigned const va = 0;
+        unsigned const vb = 1;
+        unsigned const vc = 2;
+        unsigned const vd = 3;
+
+        rational val;
+        pdd s = m.one();
+        std::cout << s << "\n";
+        VERIFY(!s.subst_get(va, val));
+        VERIFY(!s.subst_get(vb, val));
+        VERIFY(!s.subst_get(vc, val));
+        VERIFY(!s.subst_get(vd, val));
+
+        s = s.subst_add(va, rational(5));
+        std::cout << s << "\n";
+        VERIFY(s.subst_get(va, val) && val == 5);
+        VERIFY(!s.subst_get(vb, val));
+        VERIFY(!s.subst_get(vc, val));
+        VERIFY(!s.subst_get(vd, val));
+
+        s = s.subst_add(vc, rational(7));
+        std::cout << s << "\n";
+        VERIFY(s.subst_get(va, val) && val == 5);
+        VERIFY(!s.subst_get(vb, val));
+        VERIFY(s.subst_get(vc, val) && val == 7);
+        VERIFY(!s.subst_get(vd, val));
+    }
+
     static void univariate() {
         std::cout << "univariate\n";
         pdd_manager m(4, pdd_manager::mod2N_e, 4);
@@ -671,6 +703,7 @@ void tst_pdd() {
     dd::test::binary_resolve();
     dd::test::pow();
     dd::test::subst_val();
+    dd::test::subst_get();
     dd::test::univariate();
     dd::test::factors();
 }

From 6e72a97727073f7b1f37c37aa2b7b45a5797c944 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 21 Nov 2022 17:25:15 +0100
Subject: [PATCH 02/21] Refactor assignment and search state

---
 src/math/polysat/CMakeLists.txt           |   1 +
 src/math/polysat/assignment.cpp           | 107 ++++++++++++++++++++
 src/math/polysat/assignment.h             | 114 ++++++++++++++++++++++
 src/math/polysat/boolean.h                |   3 -
 src/math/polysat/constraint.cpp           |   4 +
 src/math/polysat/constraint.h             |  12 +--
 src/math/polysat/op_constraint.cpp        |   8 +-
 src/math/polysat/op_constraint.h          |   3 +-
 src/math/polysat/search_state.cpp         |  33 ++-----
 src/math/polysat/search_state.h           |  96 +++---------------
 src/math/polysat/simplify_clause.cpp      |   6 +-
 src/math/polysat/smul_fl_constraint.h     |   3 +-
 src/math/polysat/solver.cpp               |  69 +++++++------
 src/math/polysat/solver.h                 |  15 +--
 src/math/polysat/superposition.cpp        |   6 +-
 src/math/polysat/types.h                  |   3 +
 src/math/polysat/ule_constraint.cpp       |  24 ++---
 src/math/polysat/ule_constraint.h         |   3 +-
 src/math/polysat/umul_ovfl_constraint.cpp |   4 +-
 src/math/polysat/umul_ovfl_constraint.h   |   3 +-
 src/math/polysat/variable_elimination.cpp |  18 ++--
 src/math/polysat/variable_elimination.h   |   2 +-
 22 files changed, 326 insertions(+), 211 deletions(-)
 create mode 100644 src/math/polysat/assignment.cpp
 create mode 100644 src/math/polysat/assignment.h

diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt
index b7fc66903..5d4d3f3f5 100644
--- a/src/math/polysat/CMakeLists.txt
+++ b/src/math/polysat/CMakeLists.txt
@@ -1,5 +1,6 @@
 z3_add_component(polysat
   SOURCES
+    assignment.cpp
     boolean.cpp
     clause.cpp
     clause_builder.cpp
diff --git a/src/math/polysat/assignment.cpp b/src/math/polysat/assignment.cpp
new file mode 100644
index 000000000..70bbb55ed
--- /dev/null
+++ b/src/math/polysat/assignment.cpp
@@ -0,0 +1,107 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat substitution and assignment
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-06
+
+--*/
+
+#include "math/polysat/assignment.h"
+#include "math/polysat/solver.h"
+
+namespace polysat {
+
+    substitution::substitution(pdd p)
+        : m_subst(std::move(p)) { }
+
+    substitution::substitution(dd::pdd_manager& m)
+        : m_subst(m.one()) { }
+
+    substitution substitution::add(pvar var, rational const& value) const {
+        return {m_subst.subst_add(var, value)};
+    }
+
+    pdd substitution::apply_to(pdd const& p) const {
+        return p.subst_val(m_subst);
+    }
+
+    bool substitution::value(pvar var, rational& out_value) const {
+        return m_subst.subst_get(var, out_value);
+    }
+
+    assignment::assignment(solver& s)
+        : m_solver(&s) { }
+
+    assignment assignment::clone() const {
+        assignment a(s());
+        a.m_pairs = m_pairs;
+        a.m_subst.reserve(m_subst.size());
+        for (unsigned i = m_subst.size(); i-- > 0; )
+            if (m_subst[i])
+                a.m_subst.set(i, alloc(substitution, *m_subst[i]));
+        a.m_subst_trail = m_subst_trail;
+        return a;
+    }
+
+    substitution& assignment::subst(unsigned sz) {
+        return const_cast<substitution&>(std::as_const(*this).subst(sz));
+    }
+
+    substitution const& assignment::subst(unsigned sz) const {
+        m_subst.reserve(sz + 1);
+        if (!m_subst[sz])
+            m_subst.set(sz, alloc(substitution, s().sz2pdd(sz)));
+        return *m_subst[sz];
+    }
+
+    void assignment::push(pvar var, rational const& value) {
+        SASSERT(all_of(m_pairs, [var](assignment_item_t const& item) { return item.first != var; }));
+        m_pairs.push_back({var, value});
+        unsigned const sz = s().size(var);
+        substitution& sub = subst(sz);
+        m_subst_trail.push_back(sub);
+        sub = sub.add(var, value);
+        SASSERT_EQ(sub, *m_subst[sz]);
+    }
+
+    void assignment::pop() {
+        substitution& sub = m_subst_trail.back();
+        unsigned sz = sub.bit_width();
+        SASSERT_EQ(sz, s().size(m_pairs.back().first));
+        *m_subst[sz] = sub;
+        m_subst_trail.pop_back();
+        m_pairs.pop_back();
+    }
+
+    pdd assignment::apply_to(pdd const& p) const {
+        unsigned const sz = p.power_of_2();
+        return subst(sz).apply_to(p);
+    }
+
+    std::ostream& substitution::display(std::ostream& out) const {
+        char const* delim = "";
+        pdd p = m_subst;
+        while (!p.is_val()) {
+            SASSERT(p.lo().is_val());
+            out << delim << "v" << p.var() << " := " << p.lo();
+            delim = " ";
+            p = p.hi();
+        }
+        return out;
+    }
+
+    std::ostream& assignment::display(std::ostream& out) const {
+        char const* delim = "";
+        for (auto const& [var, value] : m_pairs) {
+            out << delim << assignment_pp(s(), var, value);
+            delim = " ";
+        }
+        return out;
+    }
+}
diff --git a/src/math/polysat/assignment.h b/src/math/polysat/assignment.h
new file mode 100644
index 000000000..db2e52b68
--- /dev/null
+++ b/src/math/polysat/assignment.h
@@ -0,0 +1,114 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat substitution and assignment
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-06
+
+--*/
+#pragma once
+#include "math/polysat/types.h"
+
+namespace polysat {
+
+    using assignment_item_t = std::pair<pvar, rational>;
+
+    class substitution_iterator {
+        pdd m_current;
+        substitution_iterator(pdd current) : m_current(std::move(current)) {}
+        friend class substitution;
+
+    public:
+        using value_type = assignment_item_t;
+        using difference_type = std::ptrdiff_t;
+        using pointer = value_type const*;
+        using reference = value_type const&;
+        using iterator_category = std::input_iterator_tag;
+
+        substitution_iterator& operator++() {
+            SASSERT(!m_current.is_val());
+            m_current = m_current.hi();
+            return *this;
+        }
+
+        value_type operator*() const {
+            SASSERT(!m_current.is_val());
+            return { m_current.var(), m_current.lo().val() };
+        }
+
+        bool operator==(substitution_iterator const& other) const { return m_current == other.m_current; }
+        bool operator!=(substitution_iterator const& other) const { return !operator==(other); }
+    };
+
+    /** Substitution for a single bit width. */
+    class substitution {
+        pdd m_subst;
+
+        substitution(pdd p);
+
+    public:
+        substitution(dd::pdd_manager& m);
+        substitution add(pvar var, rational const& value) const;
+        pdd apply_to(pdd const& p) const;
+
+        bool value(pvar var, rational& out_value) const;
+
+        bool empty() const { return m_subst.is_one(); }
+
+        pdd const& to_pdd() const { return m_subst; }
+        unsigned bit_width() const { return to_pdd().power_of_2(); }
+
+        bool operator==(substitution const& other) const { return &m_subst.manager() == &other.m_subst.manager() && m_subst == other.m_subst; }
+        bool operator!=(substitution const& other) const { return !operator==(other); }
+
+        std::ostream& display(std::ostream& out) const;
+
+        using const_iterator = substitution_iterator;
+        const_iterator begin() const { return {m_subst}; }
+        const_iterator end() const { return {m_subst.manager().one()}; }
+    };
+
+    /** Full variable assignment, may include variables of varying bit widths. */
+    class assignment {
+        solver*                                 m_solver;
+        vector<assignment_item_t>               m_pairs;  // TODO: do we still need this?
+        mutable scoped_ptr_vector<substitution> m_subst;
+        vector<substitution>                    m_subst_trail;
+
+        substitution& subst(unsigned sz);
+        solver& s() const { return *m_solver; }
+    public:
+        assignment(solver& s);
+        // prevent implicit copy, use clone() if you do need a copy
+        assignment(assignment const&) = delete;
+        assignment& operator=(assignment const&) = delete;
+        assignment(assignment&&) = default;
+        assignment& operator=(assignment&&) = default;
+        assignment clone() const;
+
+        void push(pvar var, rational const& value);
+        void pop();
+
+        pdd apply_to(pdd const& p) const;
+
+        bool empty() const { return pairs().empty(); }
+        substitution const& subst(unsigned sz) const;
+        vector<assignment_item_t> const& pairs() const { return m_pairs; }
+        using const_iterator = decltype(m_pairs)::const_iterator;
+        const_iterator begin() const { return pairs().begin(); }
+        const_iterator end() const { return pairs().end(); }
+
+        std::ostream& display(std::ostream& out) const;
+    };
+
+    using assignment_t = assignment;
+
+    inline std::ostream& operator<<(std::ostream& out, substitution const& sub) { return sub.display(out); }
+
+    inline std::ostream& operator<<(std::ostream& out, assignment const& a) { return a.display(out); }
+}
diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h
index b908d9773..948a2d278 100644
--- a/src/math/polysat/boolean.h
+++ b/src/math/polysat/boolean.h
@@ -12,12 +12,9 @@ Author:
 --*/
 #pragma once
 #include "math/polysat/types.h"
-#include "util/sat_literal.h"
 
 namespace polysat {
 
-    class clause;
-
     class bool_var_manager {
 
         enum class kind_t {
diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index 9cc8fe34e..89e2dd10b 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -24,6 +24,10 @@ Author:
 
 namespace polysat {
 
+    bool constraint::is_currently_false(solver& s, bool is_positive) const {
+        return is_currently_false(s.assignment(), is_positive);
+    }
+
     bool signed_constraint::is_eq() const {
         return is_positive() && m_constraint->is_eq();
     }
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index 03330c619..9b2b47b2a 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -15,7 +15,7 @@ Author:
 #include "math/polysat/boolean.h"
 #include "math/polysat/types.h"
 #include "math/polysat/interval.h"
-#include "math/polysat/search_state.h"
+#include "math/polysat/assignment.h"
 #include "math/polysat/univariate/univariate_solver.h"
 #include <iostream>
 
@@ -85,11 +85,11 @@ namespace polysat {
         virtual std::ostream& display(std::ostream& out) const = 0;
 
         virtual bool is_always_false(bool is_positive) const = 0;
-        virtual bool is_currently_false(solver& s, bool is_positive) const = 0;
-        virtual bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const = 0;
+        bool is_currently_false(solver& s, bool is_positive) const;
+        virtual bool is_currently_false(assignment const& a, bool is_positive) const = 0;
         bool is_always_true(bool is_positive) const { return is_always_false(!is_positive); }
         bool is_currently_true(solver& s, bool is_positive) const { return is_currently_false(s, !is_positive); }
-        bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const { return is_currently_false(s, sub, !is_positive); }
+        bool is_currently_true(assignment const& a, bool is_positive) const { return is_currently_false(a, !is_positive); }
 
         virtual void narrow(solver& s, bool is_positive, bool first) = 0;
         virtual inequality as_inequality(bool is_positive) const = 0;
@@ -155,8 +155,8 @@ namespace polysat {
         bool is_always_true() const { return get()->is_always_false(is_negative()); }
         bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); }
         bool is_currently_true(solver& s) const { return get()->is_currently_false(s, is_negative()); }
-        bool is_currently_false(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_positive()); }
-        bool is_currently_true(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_negative()); }
+        bool is_currently_false(assignment const& a) const { return get()->is_currently_false(a, is_positive()); }
+        bool is_currently_true(assignment const& a) const { return get()->is_currently_false(a, is_negative()); }
         lbool bvalue(solver& s) const;
         void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); }
         inequality as_inequality() const { return get()->as_inequality(is_positive()); }
diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp
index 2638ef1f5..61bf41d1f 100644
--- a/src/math/polysat/op_constraint.cpp
+++ b/src/math/polysat/op_constraint.cpp
@@ -80,12 +80,8 @@ namespace polysat {
         return is_always_false(is_positive, p(), q(), r());
     }
 
-    bool op_constraint::is_currently_false(solver& s, bool is_positive) const {
-        return is_always_false(is_positive, s.subst(p()), s.subst(q()), s.subst(r()));
-    }
-
-    bool op_constraint::is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const {
-        return is_always_false(is_positive, s.subst(sub, p()), s.subst(sub, q()), s.subst(sub, r()));
+    bool op_constraint::is_currently_false(assignment const& a, bool is_positive) const {
+        return is_always_false(is_positive, a.apply_to(p()), a.apply_to(q()), a.apply_to(r()));
     }
 
     std::ostream& op_constraint::display(std::ostream& out, lbool status) const {
diff --git a/src/math/polysat/op_constraint.h b/src/math/polysat/op_constraint.h
index 0f84d72a7..777db0f35 100644
--- a/src/math/polysat/op_constraint.h
+++ b/src/math/polysat/op_constraint.h
@@ -60,8 +60,7 @@ namespace polysat {
         std::ostream& display(std::ostream& out, lbool status) const override;
         std::ostream& display(std::ostream& out) const override;
         bool is_always_false(bool is_positive) const override;
-        bool is_currently_false(solver& s, bool is_positive) const override;
-        bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override;
+        bool is_currently_false(assignment const& a, bool is_positive) const override;
         void narrow(solver& s, bool is_positive, bool first) override;
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;
diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp
index d7966a026..6eb8e9131 100644
--- a/src/math/polysat/search_state.cpp
+++ b/src/math/polysat/search_state.cpp
@@ -8,7 +8,7 @@ Module Name:
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-19
-    Jakob Rath 2021-04-6
+    Jakob Rath 2021-04-06
 
 --*/
 
@@ -89,7 +89,7 @@ namespace polysat {
     std::ostream& search_state::display(std::ostream& out) const {
         for (auto const& item : m_items)
             display(item, out) << " ";
-        return out;        
+        return out;
     }
 
     bool search_state::value(pvar v, rational& val) const {
@@ -103,28 +103,7 @@ namespace polysat {
 
     void search_state::push_assignment(pvar p, rational const& r) {
         m_items.push_back(search_item::assignment(p));
-        m_assignment.push_back({p, r});
-        unsigned sz = s.size(p);
-        pdd& s = assignment(sz);
-        m_subst_trail.push_back(s);
-        s = s.subst_add(p, r);
-        SASSERT(s == *m_subst[sz]);
-    }
-
-    pdd& search_state::assignment(unsigned sz) const {
-        m_subst.reserve(sz + 1);
-        if (!m_subst[sz])
-            m_subst.set(sz, alloc(pdd, s.sz2pdd(sz).one()));
-        return *m_subst[sz];
-    }
-
-    void search_state::pop_assignment() {
-        m_assignment.pop_back();
-        pdd& s = m_subst_trail.back();
-        auto& m = s.manager();
-        unsigned sz = m.power_of_2();
-        *m_subst[sz] = s;
-        m_subst_trail.pop_back();
+        m_assignment.push(p, r);
     }
 
     void search_state::push_boolean(sat::literal lit) {
@@ -133,8 +112,10 @@ namespace polysat {
 
     void search_state::pop() {
         auto const& item = m_items.back();
-        if (item.is_assignment() && !m_assignment.empty() && item.var() == m_assignment.back().first) 
-            pop_assignment();
+        if (item.is_assignment()) {
+            SASSERT_EQ(item.var(), m_assignment.pairs().back().first);
+            m_assignment.pop();
+        }
         m_items.pop_back();
     }
 
diff --git a/src/math/polysat/search_state.h b/src/math/polysat/search_state.h
index 0958e7964..544f304f3 100644
--- a/src/math/polysat/search_state.h
+++ b/src/math/polysat/search_state.h
@@ -8,20 +8,15 @@ Module Name:
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-19
-    Jakob Rath 2021-04-6
+    Jakob Rath 2021-04-06
 
 --*/
 #pragma once
-#include "math/polysat/boolean.h"
 #include "math/polysat/types.h"
+#include "math/polysat/assignment.h"
 
 namespace polysat {
 
-    typedef std::pair<pvar, rational> assignment_item_t;
-    typedef vector<assignment_item_t> assignment_t;
-
-    class solver;
-
     enum class search_item_k
     {
         assignment,
@@ -46,7 +41,7 @@ namespace polysat {
         bool is_resolved() const { return m_resolved; }
         search_item_k kind() const { return m_kind; }
         pvar var() const { SASSERT(is_assignment()); return m_var; }
-        sat::literal lit() const { SASSERT(is_boolean()); return m_lit; }        
+        sat::literal lit() const { SASSERT(is_boolean()); return m_lit; }
         void set_resolved() { m_resolved = true; }
     };
 
@@ -54,27 +49,28 @@ namespace polysat {
         solver&             s;
 
         vector<search_item> m_items;
-        assignment_t        m_assignment;  // First-order part of the search state
-        mutable scoped_ptr_vector<pdd>         m_subst;
-        vector<pdd>         m_subst_trail;
+        assignment          m_assignment;
 
         bool value(pvar v, rational& r) const;
 
     public:
-        search_state(solver& s): s(s) {}
+        search_state(solver& s): s(s), m_assignment(s) {}
         unsigned size() const { return m_items.size(); }
         search_item const& back() const { return m_items.back(); }
         search_item const& operator[](unsigned i) const { return m_items[i]; }
 
         assignment_t const& assignment() const { return m_assignment; }
-        pdd& assignment(unsigned sz) const;        
+        substitution const& subst(unsigned sz) const { return m_assignment.subst(sz); }
+
+        // TODO: implement the following method if we actually need the assignments without resolved items already during conflict resolution
+        //       (no separate trail needed, just a second m_subst and an index into the trail, I think)
+        //       (update on set_resolved? might be one iteration too early, looking at the old solver::resolve_conflict loop)
+        substitution const& unresolved_assignment(unsigned sz) const;
 
         void push_assignment(pvar p, rational const& r);
         void push_boolean(sat::literal lit);
         void pop();
 
-        void pop_assignment();
-
         void set_resolved(unsigned i) { m_items[i].set_resolved(); }
 
         using const_iterator = decltype(m_items)::const_iterator;
@@ -106,74 +102,4 @@ namespace polysat {
 
     inline std::ostream& operator<<(std::ostream& out, search_item_pp const& p) { return p.verbose ? p.s.display_verbose(p.i, out) : p.s.display(p.i, out); }
 
-    // Go backwards over the search_state.
-    // If new entries are added during processing an item, they will be queued for processing next after the current item.
-    class search_iterator {
-
-        search_state*   m_search;
-
-        unsigned current;
-        unsigned first;  // highest index + 1
-
-        struct idx_range {
-            unsigned current;
-            unsigned first;  // highest index + 1
-        };
-        vector<idx_range>     m_index_stack;
-
-        void init() {
-            first = m_search->size();
-            current = first;  // we start one before the beginning
-        }
-
-        void try_push_block() {
-            if (first != m_search->size()) {
-                m_index_stack.push_back({current, first});
-                init();
-            }
-        }
-
-        void pop_block() {
-            current = m_index_stack.back().current;
-            // We don't restore 'first', otherwise 'next()' will immediately push a new block again.
-            // Instead, the current block is merged with the popped one.
-            m_index_stack.pop_back();
-        }
-
-        unsigned last() {
-            return m_index_stack.empty() ? 0 : m_index_stack.back().first;
-        }
-
-    public:
-        search_iterator(search_state& search):
-            m_search(&search) {
-            init();
-        }
-
-        void set_resolved() {
-            m_search->set_resolved(current);
-        }
-
-        search_item const& operator*() {
-            return (*m_search)[current];
-        }
-
-        bool next() {
-#if 1  // If you want to resolve over constraints that have been added during conflict resolution, enable this.
-            try_push_block();
-#endif
-            if (current > last()) {
-                --current;
-                return true;
-            }
-            else {
-                SASSERT(current == last());
-                if (m_index_stack.empty())
-                    return false;
-                pop_block();
-                return next();
-            }
-        }
-    };
-
 }
diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp
index 86ed73ac5..b7feac925 100644
--- a/src/math/polysat/simplify_clause.cpp
+++ b/src/math/polysat/simplify_clause.cpp
@@ -133,9 +133,9 @@ namespace polysat {
                 cl[j++] = cl[i];
             else {
                 DEBUG_CODE({
-                    auto a = s.assignment();
-                    a.push_back({v, k});
-                    SASSERT(s.lit2cnstr(lit).is_currently_false(s, a));
+                    auto a = s.assignment().clone();
+                    a.push(v, k);
+                    SASSERT(s.lit2cnstr(lit).is_currently_false(a));
                 });
             }
         }
diff --git a/src/math/polysat/smul_fl_constraint.h b/src/math/polysat/smul_fl_constraint.h
index dffd0be6b..f7388a2b6 100644
--- a/src/math/polysat/smul_fl_constraint.h
+++ b/src/math/polysat/smul_fl_constraint.h
@@ -36,8 +36,7 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override;
         bool is_always_false(bool is_positive) const override { return false; }
         void narrow(solver& s, bool is_positive, bool first) override;
-        bool is_currently_false(solver & s, bool is_positive) const override { return false; }
-        bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }
+        bool is_currently_false(assignment const& a, bool is_positive) const override { return false; }
 
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 615c9ec39..9b088b0c7 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -97,7 +97,7 @@ namespace polysat {
         return *m_pdd[sz];
     }
 
-    dd::pdd_manager& solver::var2pdd(pvar v) {
+    dd::pdd_manager& solver::var2pdd(pvar v) const {
         return sz2pdd(size(v));
     }
 
@@ -693,15 +693,14 @@ namespace polysat {
 
         SASSERT(is_conflict());
 
-        search_iterator search_it(m_search);
-        while (search_it.next()) {
-            auto& item = *search_it;
-            search_it.set_resolved();
+        for (unsigned i = m_search.size(); i-- > 0; ) {
+            auto& item = m_search[i];
+            m_search.set_resolved(i);
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();
                 if (!m_conflict.is_relevant_pvar(v)) {
-                    m_search.pop_assignment();
+                    // m_search.pop_assignment();
                     continue;
                 }
                 LOG_H2("Working on " << search_item_pp(m_search, item));
@@ -712,7 +711,7 @@ namespace polysat {
                     revert_decision(v);
                     return;
                 }
-                m_search.pop_assignment();
+                // m_search.pop_assignment();
             }
             else {
                 // Resolve over boolean literal
@@ -834,25 +833,17 @@ namespace polysat {
 
     void solver::backjump_and_learn(unsigned jump_level, clause& lemma) {
 #ifndef NDEBUG
-        assignment_t old_assignment;
-        // We can't use solver::assignment() here because we already used search_sate::pop_assignment().
-        // TODO: fix search_state design; it should show a consistent state.
-        search_iterator search_it(m_search);
-        while (search_it.next()) {
-            auto& item = *search_it;
-            if (item.is_assignment()) {
-                pvar v = item.var();
-                old_assignment.push_back({v, get_value(v)});
-            }
-        }
+        polysat::assignment old_assignment = assignment().clone();
         sat::literal_vector lemma_invariant_todo;
         SASSERT(lemma_invariant_part1(lemma, old_assignment, lemma_invariant_todo));
         // SASSERT(lemma_invariant(lemma, old_assignment));
 #endif
         clause_ref_vector side_lemmas = m_conflict.take_side_lemmas();
         sat::literal_vector narrow_queue = m_conflict.take_narrow_queue();
+
         m_conflict.reset();
         backjump(jump_level);
+
         for (sat::literal lit : narrow_queue) {
             switch (m_bvars.value(lit)) {
             case l_true:
@@ -899,10 +890,12 @@ namespace polysat {
         }
     }
 
-    bool solver::lemma_invariant_part1(clause const& lemma, assignment_t const& assignment, sat::literal_vector& out_todo) {
+    bool solver::lemma_invariant_part1(clause const& lemma, polysat::assignment const& a, sat::literal_vector& out_todo) {
         SASSERT(out_todo.empty());
         LOG("Lemma: " << lemma);
-        // LOG("assignment: " << assignment);
+        LOG("assignment: " << a);
+        // TODO: fix
+#if 0
         for (sat::literal lit : lemma) {
             auto const c = lit2cnstr(lit);
             bool const currently_false = c.is_currently_false(*this, assignment);
@@ -912,25 +905,42 @@ namespace polysat {
             else
                 SASSERT(m_bvars.value(lit) == l_false || currently_false);
         }
+#endif
         return true;
     }
 
     bool solver::lemma_invariant_part2(sat::literal_vector const& todo) {
+        LOG("todo: " << todo);
         // Check that undef literals are now propagated by the side lemmas.
+        //
+        // Unfortunately, this isn't always possible.
+        // Consider if the first side lemma contains a constraint that comes from a boolean decision:
+        //
+        //      76: v10 + v7 + -1*v0 + -1 == 0      [ l_true decide@5 pwatched active ]
+        //
+        // When we now backtrack behind the decision level of the literal, then we cannot propagate the side lemma,
+        // and some literals of the main lemma may still be undef at this point.
+        //
+        // So it seems that using constraints from a non-asserting lemma makes the new lemma also non-asserting (if it isn't already).
+#if 1
         for (sat::literal lit : todo)
             SASSERT(m_bvars.value(lit) == l_false);
+#endif
         return true;
     }
 
-    bool solver::lemma_invariant(clause const& lemma, assignment_t const& old_assignment) {
+    bool solver::lemma_invariant(clause const& lemma, polysat::assignment const& old_assignment) {
         LOG("Lemma: " << lemma);
         // LOG("old_assignment: " << old_assignment);
+        // TODO: fix
+#if 0
         for (sat::literal lit : lemma) {
             auto const c = lit2cnstr(lit);
             bool const currently_false = c.is_currently_false(*this, old_assignment);
             LOG("  " << lit_pp(*this, lit) << "    currently_false? " << currently_false);
             SASSERT(m_bvars.value(lit) == l_false || currently_false);
         }
+#endif
         return true;
     }
 
@@ -1167,9 +1177,7 @@ namespace polysat {
     }
 
     std::ostream& assignments_pp::display(std::ostream& out) const {
-        for (auto const& [var, val] : s.assignment())
-            out << assignment_pp(s, var, val) << " ";
-        return out;
+        return out << s.assignment();
     }
 
     std::ostream& assignment_pp::display(std::ostream& out) const {
@@ -1279,18 +1287,7 @@ namespace polysat {
     }
 
     pdd solver::subst(pdd const& p) const {
-        unsigned sz = p.manager().power_of_2();
-        pdd const& s = m_search.assignment(sz);
-        return p.subst_val(s);
-    }
-
-    pdd solver::subst(assignment_t const& sub, pdd const& p) const {
-        unsigned sz = p.manager().power_of_2();
-        pdd s = p.manager().mk_val(1);
-        for (auto const& [var, val] : sub)
-            if (size(var) == sz)
-                s = p.manager().subst_add(s, var, val);
-        return p.subst_val(s);
+        return assignment().apply_to(p);
     }
 
     /** Check that boolean assignment and constraint evaluation are consistent */
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index d95139e70..e1ed2a54c 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -31,6 +31,7 @@ Author:
 #include "math/polysat/justification.h"
 #include "math/polysat/linear_solver.h"
 #include "math/polysat/search_state.h"
+#include "math/polysat/assignment.h"
 #include "math/polysat/trail.h"
 #include "math/polysat/viable.h"
 #include "math/polysat/log.h"
@@ -58,6 +59,7 @@ namespace polysat {
             stats() { reset(); }
         };
 
+        friend class assignment;
         friend class constraint;
         friend class ule_constraint;
         friend class umul_ovfl_constraint;
@@ -125,8 +127,6 @@ namespace polysat {
         unsigned_vector          m_size;     // store size of variables (bit width)
 
         search_state             m_search;
-        assignment_t const& assignment() const { return m_search.assignment(); }
-        pdd subst(assignment_t const& sub, pdd const& p) const;
 
         unsigned                 m_qhead = 0; // next item to propagate (index into m_search)
         unsigned                 m_level = 0;
@@ -150,7 +150,6 @@ namespace polysat {
             m_qhead_trail.pop_back();
         }
 
-
         unsigned size(pvar v) const { return m_size[v]; }
 
         /**
@@ -161,7 +160,9 @@ namespace polysat {
         void del_var();
 
         dd::pdd_manager& sz2pdd(unsigned sz) const;
-        dd::pdd_manager& var2pdd(pvar v);
+        dd::pdd_manager& var2pdd(pvar v) const;
+
+        assignment const& assignment() const { return m_search.assignment(); }
 
         void push_level();
         void pop_levels(unsigned num_levels);
@@ -235,8 +236,8 @@ namespace polysat {
 
         bool invariant();
         static bool invariant(signed_constraints const& cs);
-        bool lemma_invariant(clause const& lemma, assignment_t const& assignment);
-        bool lemma_invariant_part1(clause const& lemma, assignment_t const& assignment, sat::literal_vector& out_todo);
+        bool lemma_invariant(clause const& lemma, polysat::assignment const& a);
+        bool lemma_invariant_part1(clause const& lemma, polysat::assignment const& a, sat::literal_vector& out_todo);
         bool lemma_invariant_part2(sat::literal_vector const& todo);
         bool wlist_invariant();
         bool assignment_invariant();
@@ -429,7 +430,7 @@ namespace polysat {
 
     };  // class solver
 
-    class assignments_pp {
+    class assignments_pp {  // TODO: can probably remove this now.
         solver const& s;
     public:
         assignments_pp(solver const& s): s(s) {}
diff --git a/src/math/polysat/superposition.cpp b/src/math/polysat/superposition.cpp
index d05718429..562e98536 100644
--- a/src/math/polysat/superposition.cpp
+++ b/src/math/polysat/superposition.cpp
@@ -15,8 +15,6 @@ Author:
 #include "math/polysat/log.h"
 #include "math/polysat/solver.h"
 
-// TODO: rename file
-
 namespace polysat {
 
     struct inference_sup : public inference {
@@ -37,8 +35,8 @@ namespace polysat {
         SASSERT(c1.is_currently_true(s));
         SASSERT(c2.is_currently_false(s));
         LOG_H3("Resolving upon v" << v);
-        LOG("c1: " << c1);
-        LOG("c2: " << c2);
+        LOG("c1: " << lit_pp(s, c1));
+        LOG("c2: " << lit_pp(s, c2));
         pdd a = c1.eq();
         pdd b = c2.eq();
         unsigned degree_a = a.degree();
diff --git a/src/math/polysat/types.h b/src/math/polysat/types.h
index e3c08434d..61dac4ea9 100644
--- a/src/math/polysat/types.h
+++ b/src/math/polysat/types.h
@@ -18,6 +18,7 @@ Author:
 #include "util/scoped_ptr_vector.h"
 #include "util/var_queue.h"
 #include "util/ref_vector.h"
+#include "util/sat_literal.h"
 #include "math/dd/dd_pdd.h"
 #include "math/dd/dd_bdd.h"
 #include "math/dd/dd_fdd.h"
@@ -25,6 +26,8 @@ Author:
 namespace polysat {
 
     class solver;
+    class clause;
+
     typedef dd::pdd pdd;
     typedef dd::bdd bdd;
     typedef dd::bddv bddv;
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index f2cde7c90..b5041f240 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -17,7 +17,7 @@ Notes:
 
    Rewrite rules to simplify expressions.
    In the following let k, k1, k2 be values.
-  
+
    - k1 <= k2       ==>   0 <= 0 if k1 <= k2
    - k1 <= k2       ==>   1 <= 0 if k1 >  k2
    - 0 <= p         ==>   0 <= 0
@@ -39,7 +39,7 @@ Notes:
 
 TODO: clause simplifications:
 
-   - p + k <= p  ==> p + k <= k & p != 0   for k != 0  
+   - p + k <= p  ==> p + k <= k & p != 0   for k != 0
    - p*q = 0     ==> p = 0 or q = 0        applies to any factoring
    - 2*p <= 2*q  ==> (p >= 2^n-1 & q < 2^n-1) or (p >= 2^n-1 = q >= 2^n-1 & p <= q)
                  ==> (p >= 2^n-1 => q < 2^n-1 or p <= q) &
@@ -50,7 +50,7 @@ TODO: clause simplifications:
 
 Note:
      case p <= p + k is already covered because we test (lhs - rhs).is_val()
-      
+
      It can be seen as an instance of lemma 5.2 of Supratik and John.
 
 --*/
@@ -168,7 +168,7 @@ namespace polysat {
     void ule_constraint::narrow(solver& s, bool is_positive, bool first) {
         auto p = s.subst(lhs());
         auto q = s.subst(rhs());
-        
+
         signed_constraint sc(this, is_positive);
 
         LOG_H3("Narrowing " << sc);
@@ -215,29 +215,23 @@ namespace polysat {
         return is_always_false(is_positive, lhs(), rhs());
     }
 
-    bool ule_constraint::is_currently_false(solver& s, bool is_positive) const {
-        auto p = s.subst(lhs());
-        auto q = s.subst(rhs());
-        return is_always_false(is_positive, p, q);
-    }
-
-    bool ule_constraint::is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const { 
-        auto p = s.subst(sub, lhs());
-        auto q = s.subst(sub, rhs());
+    bool ule_constraint::is_currently_false(assignment const& a, bool is_positive) const {
+        auto p = a.apply_to(lhs());
+        auto q = a.apply_to(rhs());
         return is_always_false(is_positive, p, q);
     }
 
     inequality ule_constraint::as_inequality(bool is_positive) const {
         if (is_positive)
             return inequality(lhs(), rhs(), false, this);
-        else 
+        else
             return inequality(rhs(), lhs(), true, this);
     }
 
     unsigned ule_constraint::hash() const {
     	return mk_mix(lhs().hash(), rhs().hash(), kind());
     }
-    
+
     bool ule_constraint::operator==(constraint const& other) const {
         return other.is_ule() && lhs() == other.to_ule().lhs() && rhs() == other.to_ule().rhs();
     }
diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h
index ddbb3cc96..ee09d1265 100644
--- a/src/math/polysat/ule_constraint.h
+++ b/src/math/polysat/ule_constraint.h
@@ -37,8 +37,7 @@ namespace polysat {
         std::ostream& display(std::ostream& out, lbool status) const override;
         std::ostream& display(std::ostream& out) const override;
         bool is_always_false(bool is_positive) const override;
-        bool is_currently_false(solver& s, bool is_positive) const override;
-        bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override;
+        bool is_currently_false(assignment const& a, bool is_positive) const override;
         void narrow(solver& s, bool is_positive, bool first) override;
         inequality as_inequality(bool is_positive) const override;
         unsigned hash() const override;
diff --git a/src/math/polysat/umul_ovfl_constraint.cpp b/src/math/polysat/umul_ovfl_constraint.cpp
index 2f11d23e6..ca802ca9e 100644
--- a/src/math/polysat/umul_ovfl_constraint.cpp
+++ b/src/math/polysat/umul_ovfl_constraint.cpp
@@ -77,8 +77,8 @@ namespace polysat {
         return is_always_false(is_positive, m_p, m_q);
     }
 
-    bool umul_ovfl_constraint::is_currently_false(solver& s, bool is_positive) const {
-        return is_always_false(is_positive, s.subst(p()), s.subst(q()));
+    bool umul_ovfl_constraint::is_currently_false(assignment const& a, bool is_positive) const {
+        return is_always_false(is_positive, a.apply_to(p()), a.apply_to(q()));
     }
 
     void umul_ovfl_constraint::narrow(solver& s, bool is_positive, bool first) {    
diff --git a/src/math/polysat/umul_ovfl_constraint.h b/src/math/polysat/umul_ovfl_constraint.h
index 53771ab4e..e4f52acb7 100644
--- a/src/math/polysat/umul_ovfl_constraint.h
+++ b/src/math/polysat/umul_ovfl_constraint.h
@@ -39,8 +39,7 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override;
         bool is_always_false(bool is_positive) const override;
         void narrow(solver& s, bool is_positive, bool first) override;
-        bool is_currently_false(solver & s, bool is_positive) const override;
-        bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }
+        bool is_currently_false(assignment const& a, bool is_positive) const override;
 
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;
diff --git a/src/math/polysat/variable_elimination.cpp b/src/math/polysat/variable_elimination.cpp
index 168490618..b7461c8d5 100644
--- a/src/math/polysat/variable_elimination.cpp
+++ b/src/math/polysat/variable_elimination.cpp
@@ -60,14 +60,14 @@ namespace polysat {
         LOG("lc: " << lc);
         LOG("rest: " << rest);
 
-        assignment_t a;
-        pdd const lcs = eval(lc, core, a);
+        substitution sub(m);
+        pdd const lcs = eval(lc, core, sub);
         LOG("lcs: " << lcs);
         pdd lci = m.zero();
         if (!inv(lcs, lci))
             return;
 
-        pdd const rs = s.subst(a, rest);
+        pdd const rs = sub.apply_to(rest);
         pdd const vs = -rs * lci;  // this is the polynomial that computes v
         LOG("vs: " << vs);
         SASSERT(!vs.free_vars().contains(v));
@@ -102,7 +102,7 @@ namespace polysat {
                 continue;
 
             clause_builder cb(s);
-            for (auto [w, wv] : a)
+            for (auto [w, wv] : sub)
                 cb.insert(~s.eq(s.var(w), wv));
             cb.insert(~c);
             cb.insert(~c_target);
@@ -112,19 +112,19 @@ namespace polysat {
     }
 
     // Evaluate p under assignments in the core.
-    pdd free_variable_elimination::eval(pdd const& p, conflict& core, assignment_t& out_assignment) {
+    pdd free_variable_elimination::eval(pdd const& p, conflict& core, substitution& out_sub) {
         // TODO: this should probably be a helper method on conflict.
         // TODO: recognize constraints of the form "v1 == 27" to be used in the assignment?
         //       (but maybe useful evaluations are always part of core.vars() anyway?)
 
-        assignment_t& a = out_assignment;
-        SASSERT(a.empty());
+        substitution& sub = out_sub;
+        SASSERT(sub.empty());
 
         for (auto v : p.free_vars())
             if (core.contains_pvar(v))
-                a.push_back({v, s.get_value(v)});
+                sub.add(v, s.get_value(v));
 
-        pdd q = s.subst(a, p);
+        pdd q = sub.apply_to(p);
 
         // TODO: like in the old conflict::minimize_vars, we can now try to remove unnecessary variables from a.
 
diff --git a/src/math/polysat/variable_elimination.h b/src/math/polysat/variable_elimination.h
index 3e9a99c30..e1efc828c 100644
--- a/src/math/polysat/variable_elimination.h
+++ b/src/math/polysat/variable_elimination.h
@@ -24,7 +24,7 @@ namespace polysat {
         solver& s;
         void find_lemma(pvar v, conflict& core);
         void find_lemma(pvar v, signed_constraint c, conflict& core);
-        pdd eval(pdd const& p, conflict& core, assignment_t& out_assignment);
+        pdd eval(pdd const& p, conflict& core, substitution& out_sub);
         bool inv(pdd const& p, pdd& out_p_inv);
     public:
         free_variable_elimination(solver& s): s(s) {}

From 33ea8d6e571557abee3842cd2b7f5b4e20cd0b0b Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 22 Nov 2022 13:40:29 +0100
Subject: [PATCH 03/21] viable conflict also depends on vars

---
 src/math/polysat/viable.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 5158d8adc..a327ea1e6 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -701,6 +701,7 @@ namespace polysat {
                 lemma.insert_eval(~sc);
             lemma.insert(~e->src);
             core.insert(e->src);
+            core.insert_vars(e->src);
             e = n;
         }
         while (e != first);

From a144a09ede2db3e79b0d1b61cfff8a7b7649c9eb Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 22 Nov 2022 13:42:31 +0100
Subject: [PATCH 04/21] Propagation must be justified by a prefix of Gamma

---
 src/math/polysat/solver.cpp | 10 ++++++++++
 src/math/polysat/solver.h   |  2 ++
 src/math/polysat/viable.cpp | 21 ++++++++++++++++++++-
 src/math/polysat/viable.h   |  2 ++
 4 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 9b088b0c7..8136421a7 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -981,6 +981,16 @@ namespace polysat {
         m_search.push_boolean(lit);
     }
 
+    /** Push c onto \Gamma, unless it is already true. */
+    void solver::try_assign_eval(signed_constraint c) {
+        sat::literal const lit = c.blit();
+        if (m_bvars.is_assigned(lit))
+            return;
+        if (c.is_always_true())
+            return;
+        assign_eval(lit);
+    }
+
     /**
     * Activate constraint immediately
     * Activation and de-activation of constraints follows the scope controlled by push/pop.
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index e1ed2a54c..ec1aead97 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -167,6 +167,8 @@ namespace polysat {
         void push_level();
         void pop_levels(unsigned num_levels);
 
+        void try_assign_eval(signed_constraint c);
+
         void assign_propagate(sat::literal lit, clause& reason);
         void assign_decision(sat::literal lit);
         void assign_eval(sat::literal lit);
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index a327ea1e6..75427201b 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -132,7 +132,7 @@ namespace polysat {
             rational val;
             switch (find_viable(v, val)) {
             case dd::find_t::singleton:
-                s.assign_propagate(v, val);
+                propagate(v, val);
                 prop = true;
                 break;
             case dd::find_t::empty:
@@ -150,6 +150,24 @@ namespace polysat {
         return prop;
     }
 
+    void viable::propagate(pvar v, rational const& val) {
+        // NOTE: all propagations must be justified by a prefix of \Gamma,
+        //       otherwise dependencies may be missed during conflict resolution.
+        //       The propagation reason for v := val consists of the following constraints:
+        //       - source constraint (already on \Gamma)
+        //       - side conditions
+        //       - i.lo() == i.lo_val() for each unit interval i
+        //       - i.hi() == i.hi_val() for each unit interval i
+        for (auto const& c : get_constraints(v)) {
+            s.try_assign_eval(c);
+        }
+        for (auto const& i : units(v)) {
+            s.try_assign_eval(s.eq(i.lo(), i.lo_val()));
+            s.try_assign_eval(s.eq(i.hi(), i.hi_val()));
+        }
+        s.assign_propagate(v, val);
+    }
+
     bool viable::intersect(pvar v, signed_constraint const& c) {
         entry* ne = alloc_entry();
         if (!m_forbidden_intervals.get_interval(c, v, *ne)) {
@@ -187,6 +205,7 @@ namespace polysat {
     }
 
     bool viable::intersect(pvar v, entry* ne) {
+        SASSERT(!s.is_assigned(v));
         entry* e = m_units[v];
         if (e && e->interval.is_full()) {
             m_alloc.push_back(ne);
diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h
index f1cd1e992..7e1097b10 100644
--- a/src/math/polysat/viable.h
+++ b/src/math/polysat/viable.h
@@ -63,6 +63,8 @@ namespace polysat {
 
         void insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k);
 
+        void propagate(pvar v, rational const& val);
+
     public:
         viable(solver& s);
 

From 85a633a3e0db26f9bc81d44adbc865abb138b9fd Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 22 Nov 2022 13:47:31 +0100
Subject: [PATCH 05/21] Update resolve_value

---
 src/math/polysat/conflict.cpp | 26 ++++++++++----------------
 src/math/polysat/solver.cpp   | 27 ++++++++++++++++-----------
 2 files changed, 26 insertions(+), 27 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index a483c2a29..13c5aa7c8 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -209,8 +209,7 @@ namespace polysat {
         }
         else {
             // Constraint c conflicts with the variable assignment
-            // SASSERT(c.bvalue(s) == l_true);  // "morally" the bvalue should always be true. But (at least for now) some literals may be undef when they are only justified by a side lemma.
-                                                // TODO: maybe we can set them to true (without putting them on the search stack). But need to make sure to set them to false when finalizing the conflict; and before backjumping/learning. (tag:true_by_side_lemma)
+            SASSERT_EQ(c.bvalue(s), l_true);
             SASSERT(c.is_currently_false(s));
             insert(c);
             insert_vars(c);
@@ -223,7 +222,7 @@ namespace polysat {
         m_level = s.m_level;
         for (auto lit : cl) {
             auto c = s.lit2cnstr(lit);
-            SASSERT(c.bvalue(s) == l_false);
+            SASSERT_EQ(c.bvalue(s), l_false);
             insert(~c);
         }
         SASSERT(!empty());
@@ -269,7 +268,7 @@ namespace polysat {
         if (c.is_always_true())
             return;
         LOG("Inserting " << lit_pp(s, c));
-        // SASSERT_EQ(c.bvalue(s), l_true);  // TODO: see comment in 'set_impl' (tag:true_by_side_lemma)
+        SASSERT_EQ(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());
@@ -433,27 +432,22 @@ namespace polysat {
 
     bool conflict::resolve_value(pvar v) {
         SASSERT(contains_pvar(v));
-        auto const& j = s.m_justification[v];
+        SASSERT(s.m_justification[v].is_propagation());
 
         s.inc_activity(v);
-        m_vars.remove(v);
 
-        if (j.is_propagation()) {
-            for (auto const& c : s.m_viable.get_constraints(v))
-                insert_eval(c);
-            for (auto const& i : s.m_viable.units(v)) {
-                insert_eval(s.eq(i.lo(), i.lo_val()));
-                insert_eval(s.eq(i.hi(), i.hi_val()));
-            }
+        m_vars.remove(v);
+        for (auto const& c : s.m_viable.get_constraints(v))
+            insert(c);
+        for (auto const& i : s.m_viable.units(v)) {
+            insert(s.eq(i.lo(), i.lo_val()));
+            insert(s.eq(i.hi(), i.hi_val()));
         }
         logger().log(inf_resolve_value(s, v));
 
         if (m_resolver->try_resolve_value(v, *this))
             return true;
 
-        // Need to keep the variable in case of decision
-        if (s.is_assigned(v) && j.is_decision())
-            m_vars.insert(v);
         return false;
     }
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 8136421a7..09a5c5784 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -700,18 +700,25 @@ namespace polysat {
                 // Resolve over variable assignment
                 pvar v = item.var();
                 if (!m_conflict.is_relevant_pvar(v)) {
-                    // m_search.pop_assignment();
                     continue;
                 }
                 LOG_H2("Working on " << search_item_pp(m_search, item));
                 LOG(m_justification[v]);
                 LOG("Conflict: " << m_conflict);
                 justification& j = m_justification[v];
-                if (j.level() > base_level() && !m_conflict.resolve_value(v) && j.is_decision()) {
+                if (j.is_decision()) {
+                    if (j.level() <= base_level())
+                        break;
                     revert_decision(v);
                     return;
                 }
-                // m_search.pop_assignment();
+                if (j.level() <= base_level())  // propagation level may be out of order (cf. replay)
+                    continue;
+                m_conflict.resolve_value(v);
+                // if (j.level() > base_level() &&  /* !m_conflict.resolve_value(v) && */ j.is_decision()) {
+                //     revert_decision(v);
+                //     return;
+                // }
             }
             else {
                 // Resolve over boolean literal
@@ -724,11 +731,10 @@ namespace polysat {
                 LOG(bool_justification_pp(m_bvars, lit));
                 LOG("Literal " << lit << " is " << lit2cnstr(lit));
                 LOG("Conflict: " << m_conflict);
-                if (m_bvars.level(var) <= base_level()) {
-                    // NOTE: the levels of boolean literals on the stack aren't always ordered by level (cf. replay functionality in pop_levels).
-                    //       Thus we can only skip base level literals here, instead of aborting the loop.
+                // NOTE: the levels of boolean literals on the stack aren't always ordered by level (cf. replay functionality in pop_levels).
+                //       Thus we can only skip base level literals here, instead of aborting the loop.
+                if (m_bvars.level(var) <= base_level())
                     continue;
-                }
                 SASSERT(!m_bvars.is_assumption(var));
                 if (m_bvars.is_decision(var)) {
                     revert_bool_decision(lit);
@@ -968,12 +974,11 @@ 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));
+        signed_constraint const c = lit2cnstr(lit);
+        SASSERT(c.is_currently_true(*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())
+        for (auto v : c->vars())
             if (is_assigned(v))
                 level = std::max(get_level(v), level);
         m_bvars.eval(lit, level);

From da762700d6c400a5cc2707f91bf4254d0e4b6080 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 22 Nov 2022 14:19:35 +0100
Subject: [PATCH 06/21] quot_rem

---
 src/math/polysat/constraint_manager.cpp | 35 ++++++++++++++++++++-----
 1 file changed, 29 insertions(+), 6 deletions(-)

diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index a6e99962d..0bcc4630a 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -276,10 +276,24 @@ namespace polysat {
     std::pair<pdd, pdd> constraint_manager::quot_rem(pdd const& a, pdd const& b) {
         auto& m = a.manager();
         unsigned sz = m.power_of_2();
-        if (a.is_val() && b.is_val()) {
-            // TODO: just evaluate?
+        if (b.is_zero()) {
+            // By SMT-LIB specification, b = 0 ==> q = -1, r = a.
+            return {m.mk_val(m.max_value()), a};
+        }
+        if (a.is_val() && b.is_val()) {
+            rational const av = a.val();
+            rational const bv = b.val();
+            SASSERT(!bv.is_zero());
+            rational rv;
+            rational qv = machine_div_rem(av, bv, rv);
+            pdd q = m.mk_val(qv);
+            pdd r = m.mk_val(rv);
+            SASSERT_EQ(a, b * q + r);
+            SASSERT(b.val()*q.val() + r.val() <= m.max_value());
+            SASSERT(r.val() <= (b*q+r).val());
+            SASSERT(r.val() < b.val());
+            return {std::move(q), std::move(r)};
         }
-
         constraint_dedup::quot_rem_args args({a, b});
         auto it = m_dedup.quot_rem_expr.find_iterator(args);
         if (it != m_dedup.quot_rem_expr.end())
@@ -292,18 +306,27 @@ namespace polysat {
         // Axioms for quotient/remainder:
         //      a = b*q + r
         //      multiplication does not overflow in b*q
-        //      addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r    (TODO: maybe the version with disjunction is easier for the solver; should compare later)
+        //      addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
         //      b ≠ 0  ==>  r < b
         //      b = 0  ==>  q = -1
         s.add_eq(a, b * q + r);
         s.add_umul_noovfl(b, q);
-        s.add_ule(r, b*q+r);
+        // r <= b*q+r
+        //  { apply equivalence:  p <= q  <=>  q-p <= -p-1 }
+        // b*q <= -r-1
+        s.add_ule(b*q, -r-1);
+#if 0
+        // b*q <= b*q+r
+        //  { apply equivalence:  p <= q  <=>  q-p <= -p-1 }
+        // r <= - b*q - 1
+        s.add_ule(r, -b*q-1);  // redundant, but may help propagation
+#endif
 
         auto c_eq = eq(b);
         s.add_clause(c_eq, ult(r, b), false);
         s.add_clause(~c_eq, eq(q + 1), false);
 
-        return {q, r};
+        return {std::move(q), std::move(r)};
     }
 
     pdd constraint_manager::bnot(pdd const& p) {

From e4999b07aaa19cd4ed27176fbc3d18f5202a67f8 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 22 Nov 2022 14:45:21 +0100
Subject: [PATCH 07/21] Remove active flag from constraint

Superseded by boolean assignment and pwatch
---
 src/math/polysat/constraint.h |  4 ----
 src/math/polysat/solver.cpp   | 30 ++++--------------------------
 src/math/polysat/solver.h     |  1 -
 3 files changed, 4 insertions(+), 31 deletions(-)

diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index 9b2b47b2a..978060c6c 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -59,7 +59,6 @@ namespace polysat {
         ckind_t             m_kind;
         unsigned_vector     m_vars;
         lbool               m_external_sign = l_undef;
-        bool                m_is_active = false;
         bool                m_is_pwatched = false;
         /** The boolean variable associated to this constraint */
         sat::bool_var       m_bvar = sat::null_bool_var;
@@ -114,9 +113,6 @@ namespace polysat {
         bool is_external() const { return m_external_sign != l_undef; }
         bool external_sign() const { SASSERT(is_external()); return m_external_sign == l_true; }
 
-        bool is_active() const { return m_is_active; }
-        void set_active(bool f) { m_is_active = f; }
-
         bool is_pwatched() const { return m_is_pwatched; }
         void set_pwatched(bool f) { m_is_pwatched = f; }
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 09a5c5784..7e521f826 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -208,10 +208,6 @@ namespace polysat {
         LOG_H2("Propagate bool " << lit << "@" << m_bvars.level(lit) << " " << m_level << " qhead: " << m_qhead);
         LOG("Literal " << lit_pp(*this, lit));
         signed_constraint c = lit2cnstr(lit);
-        SASSERT(c);
-        // TODO: review active and activate_constraint
-        if (c->is_active())
-            return;
         activate_constraint(c);
         auto& wlist = m_bvars.watch(~lit);
         unsigned i = 0, j = 0, sz = wlist.size();
@@ -262,11 +258,9 @@ namespace polysat {
                 return true;
             }
         }
-        // at most one poly variable remains unassigned.
+        // at most one pvar remains unassigned
         if (m_bvars.is_assigned(c->bvar())) {
             // constraint state: bool-propagated
-            // // constraint is active, propagate it
-            // SASSERT(c->is_active());   // TODO: what exactly does 'active' mean now ... use 'pwatched' and similar instead, to make meaning explicit?
             signed_constraint sc(c, m_bvars.value(c->bvar()) == l_true);
             if (c->vars().size() >= 2) {
                 unsigned other_v = c->var(1 - idx);
@@ -275,9 +269,7 @@ namespace polysat {
             }
             sc.narrow(*this, false);
         } else {
-            // constraint state: active but unassigned (bvalue undef, but pwatch is set and active; e.g., new constraints generated for lemmas)
-            // // constraint is not yet active, try to evaluate it
-            // SASSERT(!c->is_active());
+            // constraint state: active but unassigned (bvalue undef, but pwatch is set; e.g., new constraints generated for lemmas)
             if (c->vars().size() >= 2) {
                 unsigned other_v = c->var(1 - idx);
                 // Wait for the remaining variable to be assigned
@@ -423,7 +415,6 @@ namespace polysat {
             case trail_instr_t::pwatch_i: {
                 constraint* c = m_pwatch_trail.back();
                 erase_pwatch(c);
-                c->set_active(false);   // TODO: review meaning of "active"
                 m_pwatch_trail.pop_back();
                 break;
             }
@@ -475,9 +466,6 @@ namespace polysat {
                 LOG_V("Undo assign_bool_i: " << lit);
                 unsigned active_level = m_bvars.level(lit);
 
-                if (c->is_active())
-                    deactivate_constraint(c);
-
                 if (active_level <= target_level)
                     replay.push_back(lit);
                 else
@@ -922,7 +910,7 @@ namespace polysat {
         // Unfortunately, this isn't always possible.
         // Consider if the first side lemma contains a constraint that comes from a boolean decision:
         //
-        //      76: v10 + v7 + -1*v0 + -1 == 0      [ l_true decide@5 pwatched active ]
+        //      76: v10 + v7 + -1*v0 + -1 == 0      [ l_true decide@5 pwatched ]
         //
         // When we now backtrack behind the decision level of the literal, then we cannot propagate the side lemma,
         // and some literals of the main lemma may still be undef at this point.
@@ -1005,9 +993,7 @@ namespace polysat {
     void solver::activate_constraint(signed_constraint c) {
         SASSERT(c);
         LOG("Activating constraint: " << c);
-        SASSERT(m_bvars.value(c.blit()) == l_true);
-        SASSERT(!c->is_active());
-        c->set_active(true);
+        SASSERT_EQ(m_bvars.value(c.blit()), l_true);
         add_pwatch(c.get());
         if (c->vars().size() == 1)
             m_viable_fallback.push_constraint(c->var(0), c);
@@ -1017,12 +1003,6 @@ namespace polysat {
 #endif
     }
 
-    /// Deactivate constraint
-    void solver::deactivate_constraint(signed_constraint c) {
-        LOG_V("Deactivating constraint: " << c.blit());
-        c->set_active(false);
-    }
-
     void solver::backjump(unsigned new_level) {
         if (m_level != new_level) {
             LOG_H3("Backjumping to level " << new_level << " from level " << m_level);
@@ -1222,8 +1202,6 @@ namespace polysat {
         }
         if (c->is_pwatched())
             out << " pwatched";
-        if (c->is_active())
-            out << " active";
         if (c->is_external())
             out << " ext";
         out << " ]";
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index ec1aead97..6ca222b37 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -173,7 +173,6 @@ namespace polysat {
         void assign_decision(sat::literal lit);
         void assign_eval(sat::literal lit);
         void activate_constraint(signed_constraint c);
-        void deactivate_constraint(signed_constraint c);
         unsigned level(sat::literal lit, clause const& cl);
 
         void assign_propagate(pvar v, rational const& val);

From fdc186b204a49b11bc7ad815013b7b013ca6d4ad Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 12:19:03 +0100
Subject: [PATCH 08/21] Simplify constraint evaluation

---
 src/math/polysat/constraint.cpp           |  4 +-
 src/math/polysat/constraint.h             | 32 ++++++++++-----
 src/math/polysat/op_constraint.cpp        | 29 +++++---------
 src/math/polysat/op_constraint.h          |  7 +---
 src/math/polysat/smul_fl_constraint.cpp   | 14 +++----
 src/math/polysat/smul_fl_constraint.h     |  6 +--
 src/math/polysat/ule_constraint.cpp       | 48 ++++++++++-------------
 src/math/polysat/ule_constraint.h         |  8 ++--
 src/math/polysat/umul_ovfl_constraint.cpp | 48 +++++++++--------------
 src/math/polysat/umul_ovfl_constraint.h   | 12 +++---
 10 files changed, 95 insertions(+), 113 deletions(-)

diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index 89e2dd10b..c2c16c71b 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -24,8 +24,8 @@ Author:
 
 namespace polysat {
 
-    bool constraint::is_currently_false(solver& s, bool is_positive) const {
-        return is_currently_false(s.assignment(), is_positive);
+    lbool constraint::eval(solver const& s) const {
+        return eval(s.assignment());
     }
 
     bool signed_constraint::is_eq() const {
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index 978060c6c..27182f98f 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -83,12 +83,18 @@ namespace polysat {
         virtual std::ostream& display(std::ostream& out, lbool status) const = 0;
         virtual std::ostream& display(std::ostream& out) const = 0;
 
-        virtual bool is_always_false(bool is_positive) const = 0;
-        bool is_currently_false(solver& s, bool is_positive) const;
-        virtual bool is_currently_false(assignment const& a, bool is_positive) const = 0;
-        bool is_always_true(bool is_positive) const { return is_always_false(!is_positive); }
-        bool is_currently_true(solver& s, bool is_positive) const { return is_currently_false(s, !is_positive); }
-        bool is_currently_true(assignment const& a, bool is_positive) const { return is_currently_false(a, !is_positive); }
+        /** Evaluate the positive-polarity constraint under the empty assignment */
+        virtual lbool eval() const = 0;
+        /** Evaluate the positive-polarity constraint under the given assignment */
+        virtual lbool eval(assignment const& a) const = 0;
+        /** Evaluate the positive-polarity constraint under the solver's current assignment */
+        lbool eval(solver const& s) const;
+        bool is_always_true(bool is_positive) const { return eval() == to_lbool(is_positive); }
+        bool is_always_false(bool is_positive) const { return is_always_true(!is_positive); }
+        bool is_currently_true(assignment const& a, bool is_positive) const { return eval(a) == to_lbool(is_positive); }
+        bool is_currently_false(assignment const& a, bool is_positive) const { return is_currently_true(a, !is_positive); }
+        bool is_currently_true(solver const& s, bool is_positive) const { return eval(s) == to_lbool(is_positive); }
+        bool is_currently_false(solver const& s, bool is_positive) const { return is_currently_true(s, !is_positive); }
 
         virtual void narrow(solver& s, bool is_positive, bool first) = 0;
         virtual inequality as_inequality(bool is_positive) const = 0;
@@ -147,12 +153,18 @@ namespace polysat {
         bool is_positive() const { return m_positive; }
         bool is_negative() const { return !is_positive(); }
 
+        /** Evaluate the constraint under the empty assignment */
+        lbool eval() const { return is_positive() ? get()->eval() : ~get()->eval(); }
+        /** Evaluate the constraint under the given assignment */
+        lbool eval(assignment const& a) const  { return is_positive() ? get()->eval(a) : ~get()->eval(a); }
+        /** Evaluate the constraint under the solver's current assignment */
+        lbool eval(solver const& s) const  { return is_positive() ? get()->eval(s) : ~get()->eval(s); }
         bool is_always_false() const { return get()->is_always_false(is_positive()); }
-        bool is_always_true() const { return get()->is_always_false(is_negative()); }
-        bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); }
-        bool is_currently_true(solver& s) const { return get()->is_currently_false(s, is_negative()); }
+        bool is_always_true() const { return get()->is_always_true(is_positive()); }
         bool is_currently_false(assignment const& a) const { return get()->is_currently_false(a, is_positive()); }
-        bool is_currently_true(assignment const& a) const { return get()->is_currently_false(a, is_negative()); }
+        bool is_currently_true(assignment const& a) const { return get()->is_currently_true(a, is_positive()); }
+        bool is_currently_false(solver const& s) const { return get()->is_currently_false(s, is_positive()); }
+        bool is_currently_true(solver const& s) const { return get()->is_currently_true(s, is_positive()); }
         lbool bvalue(solver& s) const;
         void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); }
         inequality as_inequality() const { return get()->as_inequality(is_positive()); }
diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp
index 61bf41d1f..8f7df2316 100644
--- a/src/math/polysat/op_constraint.cpp
+++ b/src/math/polysat/op_constraint.cpp
@@ -51,6 +51,14 @@ namespace polysat {
         SASSERT(c != code::not_op);
     }
 
+    lbool op_constraint::eval() const {
+        return eval(p(), q(), r());
+    }
+
+    lbool op_constraint::eval(assignment const& a) const {
+        return eval(a.apply_to(p()), a.apply_to(q()), a.apply_to(r()));
+    }
+
     lbool op_constraint::eval(pdd const& p, pdd const& q, pdd const& r) const {
         switch (m_op) {
         case code::lshr_op:
@@ -64,26 +72,6 @@ namespace polysat {
         }
     }
 
-    bool op_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
-        switch (eval(p, q, r)) {
-        case l_true: return !is_positive;
-        case l_false: return is_positive;
-        default: return false;
-        }
-    }
-
-    bool op_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
-        return is_always_false(!is_positive, p, q, r);
-    }
-
-    bool op_constraint::is_always_false(bool is_positive) const {
-        return is_always_false(is_positive, p(), q(), r());
-    }
-
-    bool op_constraint::is_currently_false(assignment const& a, bool is_positive) const {
-        return is_always_false(is_positive, a.apply_to(p()), a.apply_to(q()), a.apply_to(r()));
-    }
-
     std::ostream& op_constraint::display(std::ostream& out, lbool status) const {
         switch (status) {
         case l_true: return display(out);
@@ -399,4 +387,5 @@ namespace polysat {
             break;
         }
     }
+
 }
diff --git a/src/math/polysat/op_constraint.h b/src/math/polysat/op_constraint.h
index 777db0f35..016cf1f29 100644
--- a/src/math/polysat/op_constraint.h
+++ b/src/math/polysat/op_constraint.h
@@ -38,9 +38,6 @@ namespace polysat {
         pdd m_r;
 
         op_constraint(constraint_manager& m, code c, pdd const& p, pdd const& q, pdd const& r);
-        void simplify() {}
-        bool is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const;
-        bool is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const;
         lbool eval(pdd const& p, pdd const& q, pdd const& r) const;
 
         void narrow_lshr(solver& s);
@@ -59,8 +56,8 @@ namespace polysat {
         pdd const& r() const { return m_r; }
         std::ostream& display(std::ostream& out, lbool status) const override;
         std::ostream& display(std::ostream& out) const override;
-        bool is_always_false(bool is_positive) const override;
-        bool is_currently_false(assignment const& a, bool is_positive) const override;
+        lbool eval() const override;
+        lbool eval(assignment const& a) const override;
         void narrow(solver& s, bool is_positive, bool first) override;
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;
diff --git a/src/math/polysat/smul_fl_constraint.cpp b/src/math/polysat/smul_fl_constraint.cpp
index 8a4474189..98f76fac1 100644
--- a/src/math/polysat/smul_fl_constraint.cpp
+++ b/src/math/polysat/smul_fl_constraint.cpp
@@ -40,7 +40,7 @@ namespace polysat {
         case l_true: return display(out);
         case l_false: return display(out << "~");
         case l_undef: return display(out << "?");
-        }       
+        }
         return out;
     }
 
@@ -48,12 +48,12 @@ namespace polysat {
         if (m_is_overflow)
             return out << "sovfl*(" << m_p << ", " << m_q << ")";
         else
-            return out << "sudfl*(" << m_p << ", " << m_q << ")";            
+            return out << "sudfl*(" << m_p << ", " << m_q << ")";
     }
 
     /**
      * TODO - verify the rules for small bit-widths.
-     * 
+     *
      *  sovfl(p,q) => p >= 2, q >= 2
      *  sovfl(p,q) => p >s 0 <=> q >s 0
      *  sovfl(p,q) & p >s 0 => p*q < 0 or ovfl(p,q)
@@ -67,8 +67,8 @@ namespace polysat {
      * sudfl(p, q) & p >s 0 => p*q > 0 or ovfl(p, -q)
      * sudfl(p, q) & q >s 0 => p*q > 0 or ovfl(-p, q)
      *
-     * ~sudfl(p, q) & p >s 0 & q <s 0 => ~ovfl(p, -q) & p*q <s 0 
-     * ~sudfl(p, q) & p <s 0 & q >s 0 => ~ovfl(-p, q) & p*q <s 0 
+     * ~sudfl(p, q) & p >s 0 & q <s 0 => ~ovfl(p, -q) & p*q <s 0
+     * ~sudfl(p, q) & p <s 0 & q >s 0 => ~ovfl(-p, q) & p*q <s 0
      */
     void smul_fl_constraint::narrow(solver& s, bool is_positive, bool first) {
         if (!first)
@@ -103,8 +103,8 @@ namespace polysat {
                 s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.umul_ovfl(p(), -q()), false);
                 s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.slt(p()*q(), 0), false);
                 s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.umul_ovfl(-p(), q()), false);
-                s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.slt(p()*q(), 0), false);                
-            }                
+                s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.slt(p()*q(), 0), false);
+            }
         }
     }
 
diff --git a/src/math/polysat/smul_fl_constraint.h b/src/math/polysat/smul_fl_constraint.h
index f7388a2b6..2177a90a1 100644
--- a/src/math/polysat/smul_fl_constraint.h
+++ b/src/math/polysat/smul_fl_constraint.h
@@ -26,7 +26,7 @@ namespace polysat {
 
         void simplify();
         smul_fl_constraint(constraint_manager& m, pdd const& p, pdd const& q, bool is_overflow);
-        
+
     public:
         ~smul_fl_constraint() override {}
         bool is_overflow() const { return m_is_overflow; }
@@ -34,9 +34,9 @@ namespace polysat {
         pdd const& q() const { return m_q; }
         std::ostream& display(std::ostream& out, lbool status) const override;
         std::ostream& display(std::ostream& out) const override;
-        bool is_always_false(bool is_positive) const override { return false; }
+        lbool eval() const override { return l_undef; }  // TODO
+        lbool eval(assignment const& a) const override { return l_undef; }  // TODO
         void narrow(solver& s, bool is_positive, bool first) override;
-        bool is_currently_false(assignment const& a, bool is_positive) const override { return false; }
 
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index b5041f240..61b50b0ce 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -189,36 +189,30 @@ namespace polysat {
         s.m_viable.intersect(p, q, sc);
     }
 
-    bool ule_constraint::is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) {
+    // Evaluate lhs <= rhs
+    lbool ule_constraint::eval(pdd const& lhs, pdd const& rhs) {
         // NOTE: don't assume simplifications here because we also call this on partially substituted constraints
-        if (is_positive) {
-            // lhs <= rhs
-            if (rhs.is_zero())
-                return lhs.is_never_zero();  // p <= 0 implies p == 0
-            return lhs.is_val() && rhs.is_val() && lhs.val() > rhs.val();
-        }
-        else {
-            // lhs > rhs
-            if (lhs.is_zero())
-                return true;  // 0 > ... is always false
-            if (lhs == rhs)
-                return true;  // p > p
-            if (rhs.is_max())
-                return true;  // p > -1
-            if (lhs.is_one() && rhs.is_never_zero())
-                return true;  // 1 > p implies p == 0
-            return lhs.is_val() && rhs.is_val() && lhs.val() <= rhs.val();
-        }
+        if (lhs.is_zero())
+            return l_true;      // 0 <= p
+        if (lhs == rhs)
+            return l_true;      // p <= p
+        if (rhs.is_max())
+            return l_true;      // p <= -1
+        if (rhs.is_zero() && lhs.is_never_zero())
+            return l_false;     // p <= 0 implies p == 0
+        if (lhs.is_one() && rhs.is_never_zero())
+            return l_true;      // 1 <= p implies p != 0
+        if (lhs.is_val() && rhs.is_val())
+            return to_lbool(lhs.val() <= rhs.val());
+        return l_undef;
+   }
+
+    lbool ule_constraint::eval() const {
+        return eval(lhs(), rhs());
     }
 
-    bool ule_constraint::is_always_false(bool is_positive) const {
-        return is_always_false(is_positive, lhs(), rhs());
-    }
-
-    bool ule_constraint::is_currently_false(assignment const& a, bool is_positive) const {
-        auto p = a.apply_to(lhs());
-        auto q = a.apply_to(rhs());
-        return is_always_false(is_positive, p, q);
+    lbool ule_constraint::eval(assignment const& a) const {
+        return eval(a.apply_to(lhs()), a.apply_to(rhs()));
     }
 
     inequality ule_constraint::as_inequality(bool is_positive) const {
diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h
index ee09d1265..052d82cde 100644
--- a/src/math/polysat/ule_constraint.h
+++ b/src/math/polysat/ule_constraint.h
@@ -27,7 +27,9 @@ namespace polysat {
 
         ule_constraint(constraint_manager& m, pdd const& l, pdd const& r);
         static void simplify(bool& is_positive, pdd& lhs, pdd& rhs);
-        static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs);
+        static bool is_always_true(bool is_positive, pdd const& lhs, pdd const& rhs) { return eval(lhs, rhs) == to_lbool(is_positive); }
+        static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) { return is_always_true(!is_positive, lhs, rhs); }
+        static lbool eval(pdd const& lhs, pdd const& rhs);
 
     public:
         ~ule_constraint() override {}
@@ -36,8 +38,8 @@ namespace polysat {
         static std::ostream& display(std::ostream& out, lbool status, pdd const& lhs, pdd const& rhs);
         std::ostream& display(std::ostream& out, lbool status) const override;
         std::ostream& display(std::ostream& out) const override;
-        bool is_always_false(bool is_positive) const override;
-        bool is_currently_false(assignment const& a, bool is_positive) const override;
+        lbool eval() const override;
+        lbool eval(assignment const& a) const override;
         void narrow(solver& s, bool is_positive, bool first) override;
         inequality as_inequality(bool is_positive) const override;
         unsigned hash() const override;
diff --git a/src/math/polysat/umul_ovfl_constraint.cpp b/src/math/polysat/umul_ovfl_constraint.cpp
index ca802ca9e..86c2eec3f 100644
--- a/src/math/polysat/umul_ovfl_constraint.cpp
+++ b/src/math/polysat/umul_ovfl_constraint.cpp
@@ -40,15 +40,15 @@ namespace polysat {
         case l_true: return display(out);
         case l_false: return display(out << "~");
         case l_undef: return display(out << "?");
-        }       
+        }
         return out;
     }
 
     std::ostream& umul_ovfl_constraint::display(std::ostream& out) const {
-        return out << "ovfl*(" << m_p << ", " << m_q << ")";       
+        return out << "ovfl*(" << m_p << ", " << m_q << ")";
     }
 
-    lbool umul_ovfl_constraint::eval(pdd const& p, pdd const& q) const {
+    lbool umul_ovfl_constraint::eval(pdd const& p, pdd const& q) {
         if (p.is_zero() || q.is_zero() || p.is_one() || q.is_one())
             return l_false;
 
@@ -61,30 +61,18 @@ namespace polysat {
         return l_undef;
     }
 
-    bool umul_ovfl_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q) const {
-        switch (eval(p, q)) {
-        case l_true: return !is_positive;
-        case l_false: return is_positive;
-        default: return false;
-        }
+    lbool umul_ovfl_constraint::eval() const {
+        return eval(p(), q());
     }
 
-    bool umul_ovfl_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q) const {
-        return is_always_false(!is_positive, p, q);
+    lbool umul_ovfl_constraint::eval(assignment const& a) const {
+        return eval(a.apply_to(p()), a.apply_to(q()));
     }
 
-    bool umul_ovfl_constraint::is_always_false(bool is_positive) const {
-        return is_always_false(is_positive, m_p, m_q);
-    }
-
-    bool umul_ovfl_constraint::is_currently_false(assignment const& a, bool is_positive) const {
-        return is_always_false(is_positive, a.apply_to(p()), a.apply_to(q()));
-    }
-
-    void umul_ovfl_constraint::narrow(solver& s, bool is_positive, bool first) {    
+    void umul_ovfl_constraint::narrow(solver& s, bool is_positive, bool first) {
         auto p1 = s.subst(p());
         auto q1 = s.subst(q());
-        
+
         if (is_always_false(is_positive, p1, q1)) {
             s.set_conflict({ this, is_positive });
             return;
@@ -94,19 +82,19 @@ namespace polysat {
 
         if (try_viable(s, is_positive, p(), q(), p1, q1))
             return;
-        
+
         if (narrow_bound(s, is_positive, p(), q(), p1, q1))
             return;
         if (narrow_bound(s, is_positive, q(), p(), q1, p1))
             return;
 
-        
+
     }
 
     /**
-    * if p constant, q, propagate inequality   
-    */
-    bool umul_ovfl_constraint::narrow_bound(solver& s, bool is_positive, 
+     * if p constant, q, propagate inequality
+     */
+    bool umul_ovfl_constraint::narrow_bound(solver& s, bool is_positive,
         pdd const& p0, pdd const& q0, pdd const& p, pdd const& q) {
 
         if (!p.is_val())
@@ -118,13 +106,13 @@ namespace polysat {
         auto bound = ceil((max + 1) / p.val());
 
         //
-        // the clause that explains bound <= q or bound > q 
-        // 
+        // the clause that explains bound <= q or bound > q
+        //
         // Ovfl(p, q)  & p <= p.val() => q >= bound
-        // ~Ovfl(p, q) & p >= p.val() => q < bound 
+        // ~Ovfl(p, q) & p >= p.val() => q < bound
         //
 
-        signed_constraint sc(this, is_positive);       
+        signed_constraint sc(this, is_positive);
         signed_constraint premise = is_positive ? s.ule(p0, p.val()) : s.ule(p.val(), p0);
         signed_constraint conseq = is_positive ? s.ule(bound, q0) : s.ult(q0, bound);
 
diff --git a/src/math/polysat/umul_ovfl_constraint.h b/src/math/polysat/umul_ovfl_constraint.h
index e4f52acb7..cdc932594 100644
--- a/src/math/polysat/umul_ovfl_constraint.h
+++ b/src/math/polysat/umul_ovfl_constraint.h
@@ -25,21 +25,21 @@ namespace polysat {
 
         umul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q);
         void simplify();
-        bool is_always_false(bool is_positive, pdd const& p, pdd const& q) const;
-        bool is_always_true(bool is_positive, pdd const& p, pdd const& q) const;
+        static bool is_always_true(bool is_positive, pdd const& p, pdd const& q) { return eval(p, q) == to_lbool(is_positive); }
+        static bool is_always_false(bool is_positive, pdd const& p, pdd const& q) { return is_always_true(!is_positive, p, q); }
+        static lbool eval(pdd const& p, pdd const& q);
         bool narrow_bound(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q);
         bool try_viable(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q);
-        lbool eval(pdd const& p, pdd const& q) const;
-        
+
     public:
         ~umul_ovfl_constraint() override {}
         pdd const& p() const { return m_p; }
         pdd const& q() const { return m_q; }
         std::ostream& display(std::ostream& out, lbool status) const override;
         std::ostream& display(std::ostream& out) const override;
-        bool is_always_false(bool is_positive) const override;
+        lbool eval() const override;
+        lbool eval(assignment const& a) const override;
         void narrow(solver& s, bool is_positive, bool first) override;
-        bool is_currently_false(assignment const& a, bool is_positive) const override;
 
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;

From 2787a2200751e9074d76fafad9ff5e36b6ee49ee Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 12:49:36 +0100
Subject: [PATCH 09/21] Backtrack/backjump based on accumulated lemmas

---
 src/math/polysat/conflict.cpp |  47 +------
 src/math/polysat/conflict.h   |  16 +--
 src/math/polysat/solver.cpp   | 222 ++++++++++++++++++++++------------
 src/math/polysat/solver.h     |  51 +++++++-
 4 files changed, 202 insertions(+), 134 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 13c5aa7c8..e7687a4c8 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -153,7 +153,6 @@ namespace polysat {
             SASSERT(m_vars_occurring.empty());
             SASSERT(m_lemmas.empty());
             SASSERT(m_narrow_queue.empty());
-            SASSERT_EQ(m_max_jump_level, UINT_MAX);
         }
         return is_empty;
     }
@@ -166,7 +165,6 @@ namespace polysat {
         m_lemmas.reset();
         m_narrow_queue.reset();
         m_level = UINT_MAX;
-        m_max_jump_level = UINT_MAX;
         SASSERT(empty());
     }
 
@@ -314,50 +312,13 @@ namespace polysat {
     void conflict::add_lemma(clause_ref lemma) {
         SASSERT(lemma);
         lemma->set_redundant(true);
-        LOG_H3("Side lemma: " << *lemma);
+        LOG_H3("Lemma: " << *lemma);
         for (sat::literal lit : *lemma) {
             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.
-
-        // Two kinds of side lemmas:
-        // 1. If all constraints are false, then the side lemma is an alternative conflict lemma.
-        //      => we should at least jump back to the second-highest level in the lemma (could be lower, if so justified by another lemma)
-        // 2. If there is an undef constraint, then it is is a justification for this new constraint.
-        //    (Can there be more than one undef constraint? Should not happen for these lemmas.)
-        //      => TODO: (unclear) jump at least to the max level in the lemma and hope the propagation helps there? or ignore it for jump level computation?
-        unsigned max_level = 0;  // highest level in lemma
-        unsigned jump_level = 0;  // second-highest level in lemma
-        bool has_unassigned = false;
-        for (sat::literal lit : *lemma) {
-            if (!s.m_bvars.is_assigned(lit)) {
-                has_unassigned = true;
-                continue;
-            }
-            unsigned const lit_level = s.m_bvars.level(lit);
-            if (lit_level > max_level) {
-                jump_level = max_level;
-                max_level = lit_level;
-            } else if (max_level > lit_level && lit_level > jump_level) {
-                jump_level = lit_level;
-            }
-        }
-        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;
-        // and re-enable the assertions marked with "tag:true_by_side_lemma".
-        // Or we adjust the conflict invariant:
-        // - l_true constraints is the default case as before,
-        // - l_undef constraints are new and justified by some side lemma, but
-        //   should be treated by the conflict resolution methods like l_true
-        //   constraints,
-        // - l_false constraints are disallowed in the conflict (as before).
-    }
+   }
 
     void conflict::remove(signed_constraint c) {
         SASSERT(contains(c));
@@ -475,7 +436,7 @@ namespace polysat {
         return lemma.build();
     }
 
-    clause_ref_vector conflict::take_side_lemmas() {
+    clause_ref_vector conflict::take_lemmas() {
 #ifndef NDEBUG
         on_scope_exit check_empty([this]() {
             SASSERT(m_lemmas.empty());
@@ -536,7 +497,7 @@ namespace polysat {
         for (auto v : m_vars)
             out << " v" << v;
         if (!m_lemmas.empty())
-            out << " side lemmas";
+            out << " lemmas";
         for (clause const* lemma : m_lemmas)
             out << " " << show_deref(lemma);
         return out;
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index d94046ca9..0062f8d38 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -91,11 +91,8 @@ namespace polysat {
         unsigned_vector m_var_occurrences;  // for each variable, the number of constraints in m_literals that contain it
         uint_set m_vars_occurring;          // set of variables that occur in at least one of the constraints in m_literals
 
-        // Additional lemmas that justify new constraints generated during conflict resolution
+        // Lemmas that been accumulated during conflict resolution
         clause_ref_vector m_lemmas;
-        // The maximal level on which none of the side lemmas is falsified.
-        // (If we backjump to a level higher than max_jump_level, at least one side lemma will be false.)
-        unsigned m_max_jump_level = UINT_MAX;
 
         // Store constraints that should be narrowed after backjumping.
         // This allows us to perform propagations that are missed by the two-watched-variables scheme,
@@ -189,15 +186,10 @@ namespace polysat {
         /** Convert the core into a lemma to be learned. */
         clause_ref build_lemma();
 
-        /** Move the accumulated side lemmas out of the conflict */
-        clause_ref_vector take_side_lemmas();
-        /**
-         * Backjump at least to this level (or possibly to a lower level),
-         * to ensure all side lemmas can be propagated.
-         */
-        unsigned max_jump_level() const { return m_max_jump_level; }
+        /** Move the accumulated lemmas out of the conflict */
+        clause_ref_vector take_lemmas();
 
-        clause_ref_vector const& side_lemmas() const { return m_lemmas; }
+        clause_ref_vector const& lemmas() const { return m_lemmas; }
 
         /** Move the literals to be narrowed out of the conflict */
         sat::literal_vector take_narrow_queue();
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 7e521f826..ae125bd72 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -462,7 +462,6 @@ namespace polysat {
             }
             case trail_instr_t::assign_bool_i: {
                 sat::literal lit = m_search.back().lit();
-                signed_constraint c = lit2cnstr(lit);
                 LOG_V("Undo assign_bool_i: " << lit);
                 unsigned active_level = m_bvars.level(lit);
 
@@ -693,7 +692,7 @@ namespace polysat {
                 LOG_H2("Working on " << search_item_pp(m_search, item));
                 LOG(m_justification[v]);
                 LOG("Conflict: " << m_conflict);
-                justification& j = m_justification[v];
+                justification const& j = m_justification[v];
                 if (j.is_decision()) {
                     if (j.level() <= base_level())
                         break;
@@ -703,10 +702,6 @@ namespace polysat {
                 if (j.level() <= base_level())  // propagation level may be out of order (cf. replay)
                     continue;
                 m_conflict.resolve_value(v);
-                // if (j.level() > base_level() &&  /* !m_conflict.resolve_value(v) && */ j.is_decision()) {
-                //     revert_decision(v);
-                //     return;
-                // }
             }
             else {
                 // Resolve over boolean literal
@@ -719,21 +714,23 @@ namespace polysat {
                 LOG(bool_justification_pp(m_bvars, lit));
                 LOG("Literal " << lit << " is " << lit2cnstr(lit));
                 LOG("Conflict: " << m_conflict);
+                SASSERT(!m_bvars.is_assumption(var));
+                if (m_bvars.is_decision(var)) {
+                    if (m_bvars.level(var) <= base_level())
+                        break;
+                    revert_bool_decision(lit);
+                    return;
+                }
                 // NOTE: the levels of boolean literals on the stack aren't always ordered by level (cf. replay functionality in pop_levels).
                 //       Thus we can only skip base level literals here, instead of aborting the loop.
                 if (m_bvars.level(var) <= base_level())
                     continue;
-                SASSERT(!m_bvars.is_assumption(var));
-                if (m_bvars.is_decision(var)) {
-                    revert_bool_decision(lit);
-                    return;
-                }
                 if (m_bvars.is_bool_propagation(var))
+                    // TODO: this could be a propagation at an earlier level.
+                    //       do we really want to resolve these eagerly?
                     m_conflict.resolve_bool(lit, *m_bvars.reason(lit));
-                else {
-                    SASSERT(m_bvars.is_evaluation(var));
+                else
                     m_conflict.resolve_with_assignment(lit);
-                }
             }
         }
         LOG("End of resolve_conflict loop");
@@ -784,6 +781,7 @@ namespace polysat {
      *
      */
     void solver::revert_decision(pvar v) {
+#if 0
         rational val = m_value[v];
         LOG_H2("Reverting decision: pvar " << v << " := " << val);
         SASSERT(m_justification[v].is_decision());
@@ -798,9 +796,13 @@ namespace polysat {
 
         unsigned jump_level = get_level(v) - 1;
         backjump_and_learn(jump_level, *lemma);
+#endif
+        unsigned max_jump_level = get_level(v) - 1;
+        backjump_and_learn(max_jump_level);
     }
 
     void solver::revert_bool_decision(sat::literal const lit) {
+#if 0
         LOG_H2("Reverting decision: " << lit_pp(*this, lit));
         sat::bool_var const var = lit.var();
 
@@ -823,16 +825,136 @@ namespace polysat {
         // If there is more than one undef choice left in that lemma,
         // then the next bdecide will take care of that (after all outstanding propagations).
         SASSERT(can_bdecide());
+#endif
+        unsigned max_jump_level = m_bvars.level(lit) - 1;
+        backjump_and_learn(max_jump_level);
     }
 
+    std::optional<lemma_score> solver::compute_lemma_score(clause const& lemma) {
+        unsigned max_level = 0;     // highest level in lemma
+        unsigned at_max_level = 0;  // how many literals at the highest level in lemma
+        unsigned snd_level = 0;     // second-highest level in lemma
+        for (sat::literal lit : lemma) {
+            SASSERT(m_bvars.is_assigned(lit));  // any new constraints should have been assign_eval'd
+            if (m_bvars.is_true(lit))  // may happen if we only use the clause to justify a new constraint; it is not a real lemma
+                return std::nullopt;
+
+            unsigned const lit_level = m_bvars.level(lit);
+            if (lit_level > max_level) {
+                snd_level = max_level;
+                max_level = lit_level;
+                at_max_level = 1;
+            } else if (lit_level == max_level) {
+                at_max_level++;
+            } else if (max_level > lit_level && lit_level > snd_level) {
+                snd_level = lit_level;
+            }
+        }
+        SASSERT(lemma.empty() || at_max_level > 0);
+        // The MCSAT paper distinguishes between "UIP clauses" and "semantic split clauses".
+        // It is the same as our distinction between "asserting" and "non-asserting" lemmas.
+        // - UIP clause: a single literal on the highest decision level in the lemma.
+        //               Do the standard backjumping known from SAT solving (back to second-highest level in the lemma, propagate it there).
+        // - Semantic split clause: multiple literals on the highest level in the lemma.
+        //                          Backtrack to "highest level - 1" and split on the lemma there.
+        // For now, we follow the same convention for computing the jump levels.
+        unsigned jump_level;
+        if (at_max_level <= 1)
+            jump_level = snd_level;
+        else
+            jump_level = (max_level == 0) ? 0 : (max_level - 1);
+        return {{jump_level, at_max_level}};
+    }
+
+    void solver::backjump_and_learn(unsigned max_jump_level) {
+        sat::literal_vector narrow_queue = m_conflict.take_narrow_queue();
+        clause_ref_vector lemmas = m_conflict.take_lemmas();
+
+        // Select the "best" lemma
+        // - lowest jump level
+        // - lowest number of literals at the highest level
+        // We must do so before backjump() when the search stack is still intact.
+        lemma_score best_score = lemma_score::max();
+        clause* best_lemma = nullptr;
+        for (clause* lemma : lemmas) {
+            m_simplify_clause.apply(*lemma);
+            auto score = compute_lemma_score(*lemma);
+            if (!score)
+                continue;
+            if (*score < best_score) {
+                best_score = *score;
+                best_lemma = lemma;
+            }
+        }
+        // In case no (good) lemma has been found, build the fallback lemma from the conflict state.
+        if (!best_lemma || best_score.jump_level() > max_jump_level) {
+            lemmas.push_back(m_conflict.build_lemma());
+            clause* lemma = lemmas.back();
+            m_simplify_clause.apply(*lemma);
+            auto score = compute_lemma_score(*lemma);
+            SASSERT(score);
+            best_score = *score;
+            best_lemma = lemma;
+        }
+        unsigned const jump_level = best_score.jump_level();
+
+        m_conflict.reset();
+        backjump(jump_level);
+
+        for (sat::literal lit : narrow_queue) {
+            LOG("Narrow queue: " << lit_pp(*this, lit));
+            switch (m_bvars.value(lit)) {
+            case l_true:
+                lit2cnstr(lit).narrow(*this, false);
+                break;
+            case l_false:
+                lit2cnstr(~lit).narrow(*this, false);
+                break;
+            case l_undef:
+                /* do nothing */
+                break;
+            default:
+                UNREACHABLE();
+            }
+        }
+
+        for (clause* lemma : lemmas) {
+            add_clause(*lemma);
+            // NOTE: currently, the backjump level is an overapproximation,
+            //       since the level of evaluated constraints may not be exact (see TODO in assign_eval).
+            // For this reason, we may actually get a conflict at this point
+            // (because the actual jump_level of the lemma may be lower that best_level.)
+            if (is_conflict()) {
+                // until this is fixed (if possible; and there may be other causes of conflict at this point),
+                // we just forget about the remaining lemmas and restart conflict analysis.
+                return;
+            }
+            SASSERT(!is_conflict());  // TODO: is this true in general? No lemma by itself should lead to a conflict here. But can there be conflicting asserting lemmas?
+        }
+
+        LOG("best_score: " << best_score);
+        LOG("best_lemma: " << *best_lemma);
+
+        if (best_score.literals_at_max_level() > 1) {
+            LOG("Main lemma is not asserting: " << *best_lemma);
+            SASSERT(!all_of(*best_lemma, [this](sat::literal lit) { return m_bvars.is_assigned(lit); }));
+            m_lemmas.push_back(best_lemma);
+            m_trail.push_back(trail_instr_t::add_lemma_i);
+            // TODO: currently we forget non-asserting lemmas when backjumping over them.
+            //       We surely don't want to keep them in m_lemmas because then we will start doing case splits
+            //       even if the lemma should instead be waiting for propagations.
+            //       We could instead watch its pvars and re-insert into m_lemmas when all but one are assigned.
+            //       The same could even be done in general for all lemmas, instead of distinguishing between
+            //       asserting and non-asserting lemmas.
+            //       (Note that the same lemma can be asserting in one branch of the search but non-asserting in another,
+            //       depending on which pvars are assigned.)
+            SASSERT(can_bdecide());
+        }
+    }  // backjump_and_learn
+
+#if 0
     void solver::backjump_and_learn(unsigned jump_level, clause& lemma) {
-#ifndef NDEBUG
-        polysat::assignment old_assignment = assignment().clone();
-        sat::literal_vector lemma_invariant_todo;
-        SASSERT(lemma_invariant_part1(lemma, old_assignment, lemma_invariant_todo));
-        // SASSERT(lemma_invariant(lemma, old_assignment));
-#endif
-        clause_ref_vector side_lemmas = m_conflict.take_side_lemmas();
+        clause_ref_vector lemmas = m_conflict.take_lemmas();
         sat::literal_vector narrow_queue = m_conflict.take_narrow_queue();
 
         m_conflict.reset();
@@ -853,14 +975,15 @@ namespace polysat {
                 UNREACHABLE();
             }
         }
-        for (auto cl : side_lemmas) {
+        for (clause* cl : lemmas) {
             m_simplify_clause.apply(*cl);
             add_clause(*cl);
         }
-        SASSERT(lemma_invariant_part2(lemma_invariant_todo));
         learn_lemma(lemma);
     }
+#endif
 
+#if 0
     void solver::learn_lemma(clause& lemma) {
         SASSERT(!lemma.empty());
         m_simplify_clause.apply(lemma);
@@ -883,60 +1006,7 @@ namespace polysat {
             SASSERT(can_bdecide());
         }
     }
-
-    bool solver::lemma_invariant_part1(clause const& lemma, polysat::assignment const& a, sat::literal_vector& out_todo) {
-        SASSERT(out_todo.empty());
-        LOG("Lemma: " << lemma);
-        LOG("assignment: " << a);
-        // TODO: fix
-#if 0
-        for (sat::literal lit : lemma) {
-            auto const c = lit2cnstr(lit);
-            bool const currently_false = c.is_currently_false(*this, assignment);
-            LOG("  " << lit_pp(*this, lit) << "    currently_false? " << currently_false);
-            if (!currently_false && m_bvars.value(lit) == l_undef)
-                out_todo.push_back(lit);  // undefs might only be set false after the side lemmas are propagated, so check them later.
-            else
-                SASSERT(m_bvars.value(lit) == l_false || currently_false);
-        }
 #endif
-        return true;
-    }
-
-    bool solver::lemma_invariant_part2(sat::literal_vector const& todo) {
-        LOG("todo: " << todo);
-        // Check that undef literals are now propagated by the side lemmas.
-        //
-        // Unfortunately, this isn't always possible.
-        // Consider if the first side lemma contains a constraint that comes from a boolean decision:
-        //
-        //      76: v10 + v7 + -1*v0 + -1 == 0      [ l_true decide@5 pwatched ]
-        //
-        // When we now backtrack behind the decision level of the literal, then we cannot propagate the side lemma,
-        // and some literals of the main lemma may still be undef at this point.
-        //
-        // So it seems that using constraints from a non-asserting lemma makes the new lemma also non-asserting (if it isn't already).
-#if 1
-        for (sat::literal lit : todo)
-            SASSERT(m_bvars.value(lit) == l_false);
-#endif
-        return true;
-    }
-
-    bool solver::lemma_invariant(clause const& lemma, polysat::assignment const& old_assignment) {
-        LOG("Lemma: " << lemma);
-        // LOG("old_assignment: " << old_assignment);
-        // TODO: fix
-#if 0
-        for (sat::literal lit : lemma) {
-            auto const c = lit2cnstr(lit);
-            bool const currently_false = c.is_currently_false(*this, old_assignment);
-            LOG("  " << lit_pp(*this, lit) << "    currently_false? " << currently_false);
-            SASSERT(m_bvars.value(lit) == l_false || currently_false);
-        }
-#endif
-        return true;
-    }
 
     unsigned solver::level(sat::literal lit0, clause const& cl) {
         unsigned lvl = 0;
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 6ca222b37..b4ed6fc6f 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -46,6 +46,52 @@ namespace polysat {
         bool        m_log_conflicts = false;
     };
 
+    /**
+     * A metric to evaluate lemmas from conflict analysis.
+     * Lower is better.
+     *
+     * Comparison criterion:
+     * - Lowest jump level has priority, because otherwise, some of the accumulated lemmas may still be false after backjumping.
+     * - To break ties on jump level, choose clause with the fewest literals at its highest decision level;
+     *   to limit case splits.
+     */
+    class lemma_score {
+        unsigned m_jump_level;
+        unsigned m_literals_at_max_level;
+
+    public:
+        lemma_score(unsigned jump_level, unsigned at_max_level)
+            : m_jump_level(jump_level), m_literals_at_max_level(at_max_level)
+        { }
+
+        unsigned jump_level() const { return m_jump_level; }
+        unsigned literals_at_max_level() const { return m_literals_at_max_level; }
+
+        static lemma_score max() {
+            return {UINT_MAX, UINT_MAX};
+        }
+
+        bool operator==(lemma_score const& other) const {
+            return m_jump_level == other.m_jump_level
+                && m_literals_at_max_level == other.m_literals_at_max_level;
+        }
+        bool operator!=(lemma_score const& other) const { return !operator==(other); }
+
+        bool operator<(lemma_score const& other) const {
+            return m_jump_level < other.m_jump_level
+                || (m_jump_level == other.m_jump_level && m_literals_at_max_level < other.m_literals_at_max_level);
+        }
+        bool operator>(lemma_score const& other) const { return other.operator<(*this); }
+        bool operator<=(lemma_score const& other) const { return operator==(other) || operator<(other); }
+        bool operator>=(lemma_score const& other) const { return operator==(other) || operator>(other); }
+
+        std::ostream& display(std::ostream& out) const {
+            return out << "jump_level=" << m_jump_level << " at_max_level=" << m_literals_at_max_level;
+        }
+    };
+
+    inline std::ostream& operator<<(std::ostream& out, lemma_score const& ls) { return ls.display(out); }
+
     class solver {
 
         struct stats {
@@ -214,6 +260,8 @@ namespace polysat {
         void revert_decision(pvar v);
         void revert_bool_decision(sat::literal lit);
         void backjump_and_learn(unsigned jump_level, clause& lemma);
+        void backjump_and_learn(unsigned max_jump_level);
+        std::optional<lemma_score> compute_lemma_score(clause const& lemma);
 
         // activity of variables based on standard VSIDS
         unsigned m_activity_inc = 128;
@@ -237,9 +285,6 @@ namespace polysat {
 
         bool invariant();
         static bool invariant(signed_constraints const& cs);
-        bool lemma_invariant(clause const& lemma, polysat::assignment const& a);
-        bool lemma_invariant_part1(clause const& lemma, polysat::assignment const& a, sat::literal_vector& out_todo);
-        bool lemma_invariant_part2(sat::literal_vector const& todo);
         bool wlist_invariant();
         bool assignment_invariant();
         bool verify_sat();

From 58c299dc33d755fc6f66a3c1a543932216d63cb6 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 13:21:58 +0100
Subject: [PATCH 10/21] fix assertion failure

---
 src/math/polysat/solver.cpp | 27 +++++++++++++++++----------
 1 file changed, 17 insertions(+), 10 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index ae125bd72..ec4491fff 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -693,14 +693,18 @@ namespace polysat {
                 LOG(m_justification[v]);
                 LOG("Conflict: " << m_conflict);
                 justification const& j = m_justification[v];
+                // NOTE: propagation level may be out of order (cf. replay), but decisions are always in order
+                if (j.level() <= base_level()) {
+                    if (j.is_decision()) {
+                        report_unsat();
+                        return;
+                    }
+                    continue;
+                }
                 if (j.is_decision()) {
-                    if (j.level() <= base_level())
-                        break;
                     revert_decision(v);
                     return;
                 }
-                if (j.level() <= base_level())  // propagation level may be out of order (cf. replay)
-                    continue;
                 m_conflict.resolve_value(v);
             }
             else {
@@ -714,17 +718,20 @@ namespace polysat {
                 LOG(bool_justification_pp(m_bvars, lit));
                 LOG("Literal " << lit << " is " << lit2cnstr(lit));
                 LOG("Conflict: " << m_conflict);
+                // NOTE: the levels of boolean literals on the stack aren't always ordered by level (cf. replay functionality in pop_levels).
+                //       Thus we can only skip base level literals here, instead of aborting the loop.
+                if (m_bvars.level(var) <= base_level()) {
+                    if (m_bvars.is_decision(var)) {
+                        report_unsat();  // decisions are always in order
+                        return;
+                    }
+                    continue;
+                }
                 SASSERT(!m_bvars.is_assumption(var));
                 if (m_bvars.is_decision(var)) {
-                    if (m_bvars.level(var) <= base_level())
-                        break;
                     revert_bool_decision(lit);
                     return;
                 }
-                // NOTE: the levels of boolean literals on the stack aren't always ordered by level (cf. replay functionality in pop_levels).
-                //       Thus we can only skip base level literals here, instead of aborting the loop.
-                if (m_bvars.level(var) <= base_level())
-                    continue;
                 if (m_bvars.is_bool_propagation(var))
                     // TODO: this could be a propagation at an earlier level.
                     //       do we really want to resolve these eagerly?

From 4224a14bdcb31bf5e4c56eba8fa447ef120af874 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 13:22:43 +0100
Subject: [PATCH 11/21] Need to re-check whether lemma was asserting

---
 src/math/polysat/solver.cpp | 40 +++++++++++++++++++++++++------------
 1 file changed, 27 insertions(+), 13 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index ec4491fff..0eb027e4f 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -943,19 +943,27 @@ namespace polysat {
         LOG("best_lemma: " << *best_lemma);
 
         if (best_score.literals_at_max_level() > 1) {
-            LOG("Main lemma is not asserting: " << *best_lemma);
-            SASSERT(!all_of(*best_lemma, [this](sat::literal lit) { return m_bvars.is_assigned(lit); }));
-            m_lemmas.push_back(best_lemma);
-            m_trail.push_back(trail_instr_t::add_lemma_i);
-            // TODO: currently we forget non-asserting lemmas when backjumping over them.
-            //       We surely don't want to keep them in m_lemmas because then we will start doing case splits
-            //       even if the lemma should instead be waiting for propagations.
-            //       We could instead watch its pvars and re-insert into m_lemmas when all but one are assigned.
-            //       The same could even be done in general for all lemmas, instead of distinguishing between
-            //       asserting and non-asserting lemmas.
-            //       (Note that the same lemma can be asserting in one branch of the search but non-asserting in another,
-            //       depending on which pvars are assigned.)
-            SASSERT(can_bdecide());
+            // NOTE: at this point it is possible that the best_lemma is non-asserting.
+            //       We need to double-check, because the backjump level may not be exact (see comment on checking is_conflict above).
+            bool const is_asserting = all_of(*best_lemma, [this](sat::literal lit) { return m_bvars.is_assigned(lit); });
+            if (!is_asserting) {
+                LOG_H3("Main lemma is not asserting: " << *best_lemma);
+                for (sat::literal lit : *best_lemma) {
+                    LOG(lit_pp(*this, lit));
+                    // SASSERT(m_bvars.value(lit) != l_true);
+                }
+                m_lemmas.push_back(best_lemma);
+                m_trail.push_back(trail_instr_t::add_lemma_i);
+                // TODO: currently we forget non-asserting lemmas when backjumping over them.
+                //       We surely don't want to keep them in m_lemmas because then we will start doing case splits
+                //       even if the lemma should instead be waiting for propagations.
+                //       We could instead watch its pvars and re-insert into m_lemmas when all but one are assigned.
+                //       The same could even be done in general for all lemmas, instead of distinguishing between
+                //       asserting and non-asserting lemmas.
+                //       (Note that the same lemma can be asserting in one branch of the search but non-asserting in another,
+                //       depending on which pvars are assigned.)
+                SASSERT(can_bdecide());
+            }
         }
     }  // backjump_and_learn
 
@@ -1046,6 +1054,12 @@ namespace polysat {
         for (auto v : c->vars())
             if (is_assigned(v))
                 level = std::max(get_level(v), level);
+        // TODO: the level computed here is not exact, because evaluation of constraints may not depend on all variables that occur in the constraint.
+        //       For example, consider x := 0 @ 1 and y := 0 @ 3. Then x*y == 0 eval@3, even though we can already evaluate it at level 1.
+        //       To get the exact level:
+        //       - consider the levels get_level(var) for var in c->vars().
+        //       - the maximum of these is the estimate we start with (and which we currently use)
+        //       - successively reduce the level, as long as the constraint still evaluates
         m_bvars.eval(lit, level);
         m_trail.push_back(trail_instr_t::assign_bool_i);
         m_search.push_boolean(lit);

From a39cce18cb85ce0aaa0e05cad3b541e6679ad68e Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 13:46:44 +0100
Subject: [PATCH 12/21] Fix another assertion

---
 src/math/polysat/boolean.cpp |  8 ++++----
 src/math/polysat/solver.cpp  | 13 ++++++++-----
 2 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp
index 043ae8c5c..999297bd1 100644
--- a/src/math/polysat/boolean.cpp
+++ b/src/math/polysat/boolean.cpp
@@ -66,25 +66,25 @@ namespace polysat {
     }
 
     void bool_var_manager::propagate(sat::literal lit, unsigned lvl, clause& reason) {
-        LOG("Propagate literal " << lit << " @ " << lvl << " by " << reason);
+        LOG("Propagate " << lit << " @ " << lvl << " by " << reason);
         assign(kind_t::bool_propagation, lit, lvl, &reason);
         SASSERT(is_bool_propagation(lit));
     }
 
     void bool_var_manager::eval(sat::literal lit, unsigned lvl) {
-        LOG_V("Eval literal " << lit << " @ " << lvl);
+        LOG_V("Evaluate " << lit << " @ " << lvl);
         assign(kind_t::evaluation, lit, lvl, nullptr);
         SASSERT(is_evaluation(lit));
     }
 
     void bool_var_manager::assumption(sat::literal lit, unsigned lvl, dependency dep) {
-        LOG("Asserted " << lit << " @ " << lvl);
+        LOG("Assert " << lit << " @ " << lvl);
         assign(kind_t::assumption, lit, lvl, nullptr, dep);
         SASSERT(is_assumption(lit));
     }
 
     void bool_var_manager::decision(sat::literal lit, unsigned lvl) {
-        LOG("Decided " << lit << " @ " << lvl);
+        LOG("Decide " << lit << " @ " << lvl);
         assign(kind_t::decision, lit, lvl, nullptr);
         SASSERT(is_decision(lit));
     }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 0eb027e4f..42c9ea9e8 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -518,7 +518,6 @@ namespace polysat {
     void solver::decide() {
         LOG_H2("Decide");
         SASSERT(can_decide());
-        SASSERT(can_pdecide());  // if !can_pdecide(), all boolean literals have been propagated...
         if (can_bdecide())
             bdecide();
         else
@@ -533,11 +532,17 @@ namespace polysat {
         };
 
         LOG_H2("Decide on non-asserting lemma: " << lemma);
+        for (sat::literal lit : lemma) {
+            LOG(lit_pp(*this, lit));
+        }
         sat::literal choice = sat::null_literal;
         for (sat::literal lit : lemma) {
             switch (m_bvars.value(lit)) {
             case l_true:
                 // Clause is satisfied; nothing to do here
+                // Happens when all other branches of the lemma have been tried.
+                // The last branch is entered due to propagation, while the lemma is still on the stack as a decision point.
+                LOG("Skip decision (clause already satisfied)");
                 return;
             case l_false:
                 break;
@@ -548,10 +553,9 @@ namespace polysat {
             }
         }
         LOG("Choice is " << lit_pp(*this, choice));
-        // SASSERT(2 <= count_if(lemma, [this](sat::literal lit) { return !m_bvars.is_assigned(lit); });
         SASSERT(choice != sat::null_literal);
-        // TODO: is the case after backtracking correct?
-        //       => the backtracking code has to handle this. making sure that the decision literal is set to false.
+        SASSERT(2 <= count_if(lemma, [this](sat::literal lit) { return !m_bvars.is_assigned(lit); }));
+        SASSERT(can_pdecide());  // if !can_pdecide(), all boolean literals have been evaluated
         push_level();
         assign_decision(choice);
     }
@@ -950,7 +954,6 @@ namespace polysat {
                 LOG_H3("Main lemma is not asserting: " << *best_lemma);
                 for (sat::literal lit : *best_lemma) {
                     LOG(lit_pp(*this, lit));
-                    // SASSERT(m_bvars.value(lit) != l_true);
                 }
                 m_lemmas.push_back(best_lemma);
                 m_trail.push_back(trail_instr_t::add_lemma_i);

From 0313f91dc20353c061234813154224d7d68a832a Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 14:55:41 +0100
Subject: [PATCH 13/21] fix

---
 src/math/polysat/inference_logger.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/inference_logger.cpp b/src/math/polysat/inference_logger.cpp
index 47c5f40c2..da0ac5cf6 100644
--- a/src/math/polysat/inference_logger.cpp
+++ b/src/math/polysat/inference_logger.cpp
@@ -73,8 +73,8 @@ namespace polysat {
             out_indent() << assignment_pp(s, v, s.get_value(v)) << "\n";
             m_used_vars.insert(v);
         }
-        for (clause* lemma : core.side_lemmas()) {
-            out_indent() << "Side lemma: " << *lemma << "\n";
+        for (clause* lemma : core.lemmas()) {
+            out_indent() << "Lemma: " << *lemma << "\n";
             for (sat::literal lit : *lemma)
                 out_indent() << "    " << lit_pp(s, lit) << "\n";
         }

From f51d5c2fe93950ca7a59e8b0ddfd5f9b9b4440df Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 15:00:31 +0100
Subject: [PATCH 14/21] Add note on potential replay problem

---
 src/math/polysat/solver.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 42c9ea9e8..3b8124438 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -496,6 +496,15 @@ namespace polysat {
                     //      when substituting polynomials, it will now take into account the replayed variables, which may itself depend on previous propagations.
                     //      will we get into trouble with cyclic dependencies?
                     //      But we do want to take into account variables that are assigned but not yet propagated.
+                    //      Possible solutions:
+                    //      - keep the replay queue outside of this method?
+                    //        prioritize putting stuff on the stack from the replay queue.
+                    //        this might however introduce new propagations in between? maybe that is ok?
+                    //      - when evaluating/narrowing instead of passing the full assignment,
+                    //        we pass a "dependency level" which is basically an index into the search stack.
+                    //        then we get an assignment up to that dependency level.
+                    //        each literal can only depend on entries with lower dependency level
+                    //        (that is the invariant that propagations are justified by a prefix of the search stack.)
                 }
                 else
                     static_assert(always_false<T>::value, "non-exhaustive visitor");

From bef1b9b429cbe2ee603b58e786650f88cee62728 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 15:11:27 +0100
Subject: [PATCH 15/21] Simplify

---
 src/math/polysat/solver.cpp | 33 +++++++++++++++++----------------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 3b8124438..fe68259b5 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -202,8 +202,8 @@ namespace polysat {
     }
 
     /**
-    * Propagate assignment to a Boolean variable
-    */
+     * Propagate assignment to a Boolean variable
+     */
     void solver::propagate(sat::literal lit) {
         LOG_H2("Propagate bool " << lit << "@" << m_bvars.level(lit) << " " << m_level << " qhead: " << m_qhead);
         LOG("Literal " << lit_pp(*this, lit));
@@ -220,8 +220,8 @@ namespace polysat {
     }
 
     /**
-    * Propagate assignment to a pvar
-    */
+     * Propagate assignment to a pvar
+     */
     void solver::propagate(pvar v) {
         LOG_H2("Propagate " << assignment_pp(*this, v, get_value(v)));
         SASSERT(!m_locked_wlist);
@@ -896,27 +896,28 @@ namespace polysat {
         // We must do so before backjump() when the search stack is still intact.
         lemma_score best_score = lemma_score::max();
         clause* best_lemma = nullptr;
-        for (clause* lemma : lemmas) {
+
+        auto appraise_lemma = [&](clause* lemma) {
             m_simplify_clause.apply(*lemma);
             auto score = compute_lemma_score(*lemma);
-            if (!score)
-                continue;
-            if (*score < best_score) {
+            if (score && *score < best_score) {
                 best_score = *score;
                 best_lemma = lemma;
             }
-        }
-        // In case no (good) lemma has been found, build the fallback lemma from the conflict state.
+        };
+
+        for (clause* lemma : lemmas)
+            appraise_lemma(lemma);
         if (!best_lemma || best_score.jump_level() > max_jump_level) {
+            // No (good) lemma has been found, so build the fallback lemma from the conflict state.
             lemmas.push_back(m_conflict.build_lemma());
-            clause* lemma = lemmas.back();
-            m_simplify_clause.apply(*lemma);
-            auto score = compute_lemma_score(*lemma);
-            SASSERT(score);
-            best_score = *score;
-            best_lemma = lemma;
+            appraise_lemma(lemmas.back());
         }
+        SASSERT(best_score < lemma_score::max());
+        SASSERT(best_lemma);
+
         unsigned const jump_level = best_score.jump_level();
+        SASSERT(jump_level <= max_jump_level);
 
         m_conflict.reset();
         backjump(jump_level);

From 76c106476cbed069d6ba2cfbf4d656b6d6faf4eb Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 16:53:26 +0100
Subject: [PATCH 16/21] superposition hotfix

---
 src/math/polysat/superposition.cpp | 29 +++++++----------------------
 1 file changed, 7 insertions(+), 22 deletions(-)

diff --git a/src/math/polysat/superposition.cpp b/src/math/polysat/superposition.cpp
index 562e98536..addb3c7a9 100644
--- a/src/math/polysat/superposition.cpp
+++ b/src/math/polysat/superposition.cpp
@@ -49,8 +49,6 @@ namespace polysat {
             return {};
         // Only keep result if the degree in c2 was reduced.
         // (this condition might be too strict, but we use it for now to prevent looping)
-        // TODO: check total degree; only keep if total degree smaller or equal.
-        //       can always do this if c1 is linear.
         if (b.degree(v) <= r.degree(v))
             return {};
         if (a.degree(v) <= r.degree(v))
@@ -74,7 +72,6 @@ namespace polysat {
             SASSERT(c1.is_currently_true(s));
             SASSERT(c2.is_currently_false(s));
             SASSERT_EQ(c1.bvalue(s), l_true);
-            // SASSERT_EQ(c2.bvalue(s), l_true);  // TODO: should always be l_true but currently it's not guaranteed if c2 was derived via side lemma (tag:true_by_side_lemma)
             SASSERT(c2.bvalue(s) != l_false);
 
             signed_constraint c = resolve1(v, c1, c2);
@@ -82,37 +79,25 @@ namespace polysat {
                 continue;
             SASSERT(c.is_currently_false(s));
 
-            // TODO: move this case distinction into conflict::add_lemma?
-            char const* inf_name = "?";
+            // char const* inf_name = "?";
             switch (c.bvalue(s)) {
             case l_false:
-                // new conflict state based on propagation and theory conflict
-                core.remove_all();
-                core.insert(c1);
-                core.insert(c2);
-                core.insert(~c);
-                core.log_inference(inference_sup("l_false", v, c2, c1));
+                core.add_lemma({c, ~c1, ~c2});
+                // core.log_inference(inference_sup("l_false", v, c2, c1));
                 return l_true;
             case l_undef:
-                inf_name = "l_undef";
-                // c evaluates to false,
-                // c should be unit-propagated to l_true by c1 /\ c2 ==> c
+                // inf_name = "l_undef";
                 core.add_lemma({c, ~c1, ~c2});
-                core.log_inference(inference_sup("l_undef lemma", v, c2, c1));
-                // SASSERT_EQ(l_true, c.bvalue(s));   // not true anymore (TODO: but it should be) (tag:true_by_side_lemma)
+                // core.log_inference(inference_sup("l_undef lemma", v, c2, c1));
                 break;
             case l_true:
-                // c is just another constraint on the search stack; could be equivalent or better
-                inf_name = "l_true";
                 break;
             default:
                 UNREACHABLE();
                 break;
             }
-
-            // c alone (+ variables) is now enough to represent the conflict.
-            core.set(c);
-            core.log_inference(inference_sup(inf_name, v, c2, c1));
+            // // c alone (+ variables) is now enough to represent the conflict.
+            // core.log_inference(inference_sup(inf_name, v, c2, c1));
             return c->contains_var(v) ? l_undef : l_true;
         }
         return l_false;

From 0e32077321103693bd49292752feb25a1e0c951e Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 16:54:22 +0100
Subject: [PATCH 17/21] Use insert_eval for potentially new constraints

---
 src/math/polysat/conflict.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index e7687a4c8..c999681c9 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -305,7 +305,7 @@ namespace polysat {
     void conflict::add_lemma(signed_constraint const* cs, size_t cs_len) {
         clause_builder cb(s);
         for (size_t i = 0; i < cs_len; ++i)
-            cb.insert(cs[i]);
+            cb.insert_eval(cs[i]);
         add_lemma(cb.build());
     }
 

From 558fd718c0cda40ab47e538e5a5bbb8a56ec3bb1 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 16:54:58 +0100
Subject: [PATCH 18/21] Current base level may be too high to deallocate clause

---
 src/math/polysat/constraint_manager.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index 0bcc4630a..a9bcba8f0 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -62,9 +62,11 @@ namespace polysat {
 
 
     void constraint_manager::register_clause(clause* cl) {
-        while (m_clauses.size() <= s.base_level())
+        unsigned clause_level = s.base_level();
+        clause_level = 0;  // TODO: s.base_level() may be too high, if the clause is propagated at an earlier level. For now just use 0.
+        while (m_clauses.size() <= clause_level)
             m_clauses.push_back({});
-        m_clauses[s.base_level()].push_back(cl);
+        m_clauses[clause_level].push_back(cl);
     }
 
     void constraint_manager::store(clause* cl, bool value_propagate) {

From 5c63a676341f67ac943355b7299a1d81207eda8f Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 16:59:26 +0100
Subject: [PATCH 19/21] disable for now

---
 src/math/polysat/conflict.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index c999681c9..10a35768f 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -71,8 +71,8 @@ namespace polysat {
         bool try_resolve_value(pvar v, conflict& core) {
             if (m_poly_sup.perform(v, core))
                 return true;
-            if (m_saturate.perform(v, core))
-                return true;
+            // if (m_saturate.perform(v, core))
+            //     return true;
             return false;
         }
 

From 3713f51c1566496f2c18a1730cc3d9849d521d40 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 17:01:11 +0100
Subject: [PATCH 20/21] Print unit test numbers

---
 src/test/polysat.cpp | 43 +++++++++++++++++++++++++++++++++++++------
 1 file changed, 37 insertions(+), 6 deletions(-)

diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 1dc6491fe..c8a75108f 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -90,6 +90,12 @@ namespace polysat {
         for (test_record const& r : recs)
             max_name_len = std::max(max_name_len, r.m_name.length());
 
+        size_t n_total = recs.size();
+        size_t n_sat = 0;
+        size_t n_unsat = 0;
+        size_t n_wrong = 0;
+        size_t n_error = 0;
+
         for (test_record const& r : recs) {
             out << r.m_name;
             if (r.m_index != 1)
@@ -111,15 +117,40 @@ namespace polysat {
             case l_false: out << "UNSAT "; break;
             }
             switch (r.m_result) {
-            case test_result::undefined: out << "???"; break;
-            case test_result::ok: out << "ok"; break;
-            case test_result::wrong_answer: out << color_red() << "wrong answer, expected " << r.m_expected << color_reset(); break;
-            case test_result::wrong_model: out << color_red() << "wrong model" << color_reset(); break;
-            case test_result::resource_out: out << color_yellow() << "resource out" << color_reset(); break;
-            case test_result::error: out << color_red() << "error: " << r.m_error_message << color_reset(); break;
+            case test_result::undefined:
+                out << "???";
+                break;
+            case test_result::ok:
+                out << "ok";
+                if (r.m_answer == l_true)
+                    n_sat++;
+                if (r.m_answer == l_false)
+                    n_unsat++;
+                break;
+            case test_result::wrong_answer:
+                out << color_red() << "wrong answer, expected " << r.m_expected << color_reset();
+                n_wrong++;
+                break;
+            case test_result::wrong_model:
+                out << color_red() << "wrong model" << color_reset();
+                n_wrong++;
+                break;
+            case test_result::resource_out:
+                out << color_yellow() << "resource out" << color_reset();
+                break;
+            case test_result::error:
+                out << color_red() << "error: " << r.m_error_message << color_reset();
+                n_error++;
+                break;
             }
             out << std::endl;
         }
+        out << n_total << " tests, " << (n_sat + n_unsat) << " ok (" << n_sat << " sat, " << n_unsat << " unsat)";
+        if (n_wrong)
+            out << ", " << color_red() << n_wrong << " wrong!" << color_reset();
+        if (n_error)
+            out << ", " << color_red() << n_error << " error" << color_reset();
+        out << std::endl;
     }
 
     // test resolve, factoring routines

From 3a92641ca00a27fa4d61c4a223f1fdca49ec991e Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 23 Nov 2022 17:02:15 +0100
Subject: [PATCH 21/21] Unit test: catch exceptions during instance setup

---
 src/test/polysat.cpp | 238 +++++++++++++++++++++++++------------------
 1 file changed, 140 insertions(+), 98 deletions(-)

diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index c8a75108f..45b5b0555 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -9,6 +9,17 @@
 namespace {
     using namespace dd;
 
+    template <typename... Args>
+    std::string concat(Args... args) {
+        std::stringstream s;
+        int dummy[sizeof...(Args)] = {
+            // use dummy initializer list to sequence stream writes, cf. https://en.cppreference.com/w/cpp/language/parameter_pack
+            (s << args, 0)...
+        };
+        (void)dummy;
+        return s.str();
+    }
+
     void permute_args(unsigned k, pdd& a, pdd& b, pdd& c) {
         SASSERT(k < 6);
         unsigned i = k % 3;
@@ -276,6 +287,29 @@ namespace polysat {
         }
     };
 
+    template <typename Test, typename... Args>
+    void run(Test tst, Args... args)
+    {
+        bool got_exception = false;
+        try {
+            tst(args...);
+        }
+        catch(z3_exception const& e) {
+            // TODO: collect in record
+            got_exception = true;
+        }
+        catch(std::exception const& e) {
+            // TODO: collect in record
+            got_exception = true;
+        }
+        catch(...) {
+            got_exception = true;
+        }
+        if (got_exception && !collect_test_records)
+            throw;
+    }
+
+    #define RUN(tst) run([]() { tst; })
 
     class test_polysat {
     public:
@@ -581,7 +615,7 @@ namespace polysat {
          * We do overflow checks by doubling the base bitwidth here.
          */
         static void test_monot(unsigned base_bw = 5) {
-            scoped_solver s(std::string{__func__} + "(" + std::to_string(base_bw) + ")");
+            scoped_solver s(concat(__func__, "(", base_bw, ")"));
 
             auto max_int_const = rational::power_of_two(base_bw) - 1;
 
@@ -1226,49 +1260,51 @@ namespace polysat {
             s.check();
         }
 
-        static void test_band(unsigned bw = 32) {
-            {
-                scoped_solver s(__func__);
-                auto p = s.var(s.add_var(bw));
-                auto q = s.var(s.add_var(bw));
-                s.add_diseq(p - s.band(p, q));
-                s.add_diseq(p - q);
-                s.check();
-                s.expect_sat();
-            }
-            {
-                scoped_solver s(__func__);
-                auto p = s.var(s.add_var(bw));
-                auto q = s.var(s.add_var(bw));
-                s.add_ult(p, s.band(p, q));
-                s.check();
-                s.expect_unsat();
-            }
-            {
-                scoped_solver s(__func__);
-                auto p = s.var(s.add_var(bw));
-                auto q = s.var(s.add_var(bw));
-                s.add_ult(q, s.band(p, q));
-                s.check();
-                s.expect_unsat();
-            }
-            {
-                scoped_solver s(__func__);
-                auto p = s.var(s.add_var(bw));
-                auto q = s.var(s.add_var(bw));
-                s.add_ule(p, s.band(p, q));
-                s.check();
-                s.expect_sat();
-            }
-            {
-                scoped_solver s(__func__);
-                auto p = s.var(s.add_var(bw));
-                auto q = s.var(s.add_var(bw));
-                s.add_ule(p, s.band(p, q));
-                s.add_diseq(p - s.band(p, q));
-                s.check();
-                s.expect_unsat();
-            }
+        static void test_band1(unsigned bw = 32) {
+            scoped_solver s(concat(__func__, " bw=", bw));
+            auto p = s.var(s.add_var(bw));
+            auto q = s.var(s.add_var(bw));
+            s.add_diseq(p - s.band(p, q));
+            s.add_diseq(p - q);
+            s.check();
+            s.expect_sat();
+        }
+
+        static void test_band2(unsigned bw = 32) {
+            scoped_solver s(concat(__func__, " bw=", bw));
+            auto p = s.var(s.add_var(bw));
+            auto q = s.var(s.add_var(bw));
+            s.add_ult(p, s.band(p, q));
+            s.check();
+            s.expect_unsat();
+        }
+
+        static void test_band3(unsigned bw = 32) {
+            scoped_solver s(concat(__func__, " bw=", bw));
+            auto p = s.var(s.add_var(bw));
+            auto q = s.var(s.add_var(bw));
+            s.add_ult(q, s.band(p, q));
+            s.check();
+            s.expect_unsat();
+        }
+
+        static void test_band4(unsigned bw = 32) {
+            scoped_solver s(concat(__func__, " bw=", bw));
+            auto p = s.var(s.add_var(bw));
+            auto q = s.var(s.add_var(bw));
+            s.add_ule(p, s.band(p, q));
+            s.check();
+            s.expect_sat();
+        }
+
+        static void test_band5(unsigned bw = 32) {
+            scoped_solver s(concat(__func__, " bw=", bw));
+            auto p = s.var(s.add_var(bw));
+            auto q = s.var(s.add_var(bw));
+            s.add_ule(p, s.band(p, q));
+            s.add_diseq(p - s.band(p, q));
+            s.check();
+            s.expect_unsat();
         }
 
         static void test_fi_zero() {
@@ -1475,10 +1511,15 @@ void tst_polysat() {
 
 #if 0  // Enable this block to run a single unit test with detailed output.
     collect_test_records = false;
+    // test_polysat::test_l2();
     // test_polysat::test_ineq1();
     // test_polysat::test_quot_rem();
-    test_polysat::test_ineq_non_axiom1(32, 3);
-    // test_polysat::test_monot(5);
+    // test_polysat::test_ineq_non_axiom1(32, 3);
+    // test_polysat::test_monot_bounds_full();
+    // test_polysat::test_band2();
+    // test_polysat::test_quot_rem_incomplete();
+    // test_polysat::test_monot();
+    test_polysat::test_fixed_point_arith_div_mul_inverse();
     return;
 #endif
 
@@ -1490,67 +1531,68 @@ void tst_polysat() {
         set_log_enabled(false);
     }
 
-    test_polysat::test_clause_simplify1();
+    RUN(test_polysat::test_clause_simplify1());
 
-    test_polysat::test_add_conflicts();  // ok
-    test_polysat::test_wlist();  // ok
-    test_polysat::test_cjust();  // uses viable_fallback; weak lemmas
-    // test_polysat::test_subst();  // TODO: resource limit; needs polynomial superposition
-    // test_polysat::test_subst_signed();
-    test_polysat::test_pop_conflict();  // ok now (had bad conflict/pop interaction)
+    RUN(test_polysat::test_add_conflicts());
+    RUN(test_polysat::test_wlist());
+    RUN(test_polysat::test_cjust());
+    // RUN(test_polysat::test_subst());
+    // RUN(test_polysat::test_subst_signed());
+    RUN(test_polysat::test_pop_conflict());
 
-    test_polysat::test_l1();   // ok
-    test_polysat::test_l2();   // ok but enumerates values
-    test_polysat::test_l3();   // ok
-    test_polysat::test_l4();   // ok now (had assertion failure in conflict::insert)
-    test_polysat::test_l4b();  // ok
-    test_polysat::test_l5();   // inefficient conflicts (needs equality reasoning)
-    test_polysat::test_l6();   // ok (refine-equal-lin)
+    RUN(test_polysat::test_l1());
+    RUN(test_polysat::test_l2());
+    RUN(test_polysat::test_l3());
+    RUN(test_polysat::test_l4());
+    RUN(test_polysat::test_l4b());
+    RUN(test_polysat::test_l5());
+    RUN(test_polysat::test_l6());
 
-    test_polysat::test_p1();    // ok (conflict @0 by viable_fallback)
-    test_polysat::test_p2();    // ok (viable_fallback finds the correct value)
-    test_polysat::test_p3();    // TODO: resource limit
+    RUN(test_polysat::test_p1());
+    RUN(test_polysat::test_p2());
+    RUN(test_polysat::test_p3());
 
-    test_polysat::test_ineq_basic1();  // ok
-    test_polysat::test_ineq_basic2();  // ok
-    test_polysat::test_ineq_basic3();  // ok
-    test_polysat::test_ineq_basic4();  // TODO: resource limit
-    test_polysat::test_ineq_basic5();  // works, but only because variable order changes after the conflict
-    //                                       TODO: non-asserting lemma
-    //                                       possible variable selection heuristic: start with the most restricted interval?
-    //                                       (if we have a restricted and non-restricted variable; we should probably pick the restricted one first. hoping that we can propagate and uncover restrictions on the other variable.)
-    test_polysat::test_ineq_basic6();  // same as ineq_basic5
+    RUN(test_polysat::test_ineq_basic1());
+    RUN(test_polysat::test_ineq_basic2());
+    RUN(test_polysat::test_ineq_basic3());
+    RUN(test_polysat::test_ineq_basic4());
+    RUN(test_polysat::test_ineq_basic5());
+    RUN(test_polysat::test_ineq_basic6());
 
-    test_polysat::test_var_minimize();  // works but var_minimized isn't used (UNSAT before lemma is created)
+    RUN(test_polysat::test_var_minimize()); // works but var_minimize isn't used (UNSAT before lemma is created)
 
-    test_polysat::test_ineq1();  // TODO: resource limit
-    test_polysat::test_ineq2();  // TODO: resource limit
-    test_polysat::test_monot();  // TODO: assertion failure; resource limit
-    test_polysat::test_monot_bounds(2);
-    test_polysat::test_monot_bounds(8);
-    test_polysat::test_monot_bounds();
-    test_polysat::test_monot_bounds_full();
-    test_polysat::test_monot_bounds_simple(8);
-    test_polysat::test_fixed_point_arith_div_mul_inverse();
+    RUN(test_polysat::test_ineq1());
+    RUN(test_polysat::test_ineq2());
+    RUN(test_polysat::test_monot());
+    RUN(test_polysat::test_monot_bounds(2));
+    RUN(test_polysat::test_monot_bounds(8));
+    RUN(test_polysat::test_monot_bounds());
+    RUN(test_polysat::test_monot_bounds_full());
+    RUN(test_polysat::test_monot_bounds_simple(8));
+    RUN(test_polysat::test_fixed_point_arith_div_mul_inverse());
 
-    test_polysat::test_ineq_axiom1();
-    test_polysat::test_ineq_axiom2();
-    test_polysat::test_ineq_axiom3();
-    test_polysat::test_ineq_axiom4();
-    test_polysat::test_ineq_axiom5();
-    test_polysat::test_ineq_axiom6();
-    test_polysat::test_ineq_non_axiom1();
-    test_polysat::test_ineq_non_axiom4();
+    RUN(test_polysat::test_ineq_axiom1());
+    RUN(test_polysat::test_ineq_axiom2());
+    RUN(test_polysat::test_ineq_axiom3());
+    RUN(test_polysat::test_ineq_axiom4());
+    RUN(test_polysat::test_ineq_axiom5());
+    RUN(test_polysat::test_ineq_axiom6());
+    RUN(test_polysat::test_ineq_non_axiom1());
+    RUN(test_polysat::test_ineq_non_axiom4());
 
-    test_polysat::test_quot_rem_incomplete();
-    test_polysat::test_quot_rem_fixed();
-    test_polysat::test_band();
-    test_polysat::test_quot_rem();
+    RUN(test_polysat::test_quot_rem_incomplete());
+    RUN(test_polysat::test_quot_rem_fixed());
+    RUN(test_polysat::test_band1());
+    RUN(test_polysat::test_band2());
+    RUN(test_polysat::test_band3());
+    RUN(test_polysat::test_band4());
+    RUN(test_polysat::test_band5());
+    RUN(test_polysat::test_quot_rem());
 
-    test_polysat::test_fi_zero();
-    test_polysat::test_fi_nonzero();
-    test_polysat::test_fi_nonmax();
-    test_polysat::test_fi_disequal_mild();
+    RUN(test_polysat::test_fi_zero());
+    RUN(test_polysat::test_fi_nonzero());
+    RUN(test_polysat::test_fi_nonmax());
+    RUN(test_polysat::test_fi_disequal_mild());
 
     // test_fi::exhaustive();
     // test_fi::randomized();