tune based on test_l5

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

src/math/polysat/explain.cpp

@@ -54,7 +54,7 @@ namespace polysat {
         // after some variable decision was already processed. Then the 
         // behavior of evaluating literals "is_currently_true" and bvalue
         // uses the full search stack
-#if 0
+#if 1
         for (auto si : s.m_search) {
             if (!si.is_boolean())
                 continue;

src/math/polysat/search_state.cpp

@@ -17,9 +17,13 @@ Author:
 namespace polysat {
 
     std::ostream& search_state::display(search_item const& item, std::ostream& out) const {
+        rational r;
         switch (item.kind()) {
         case search_item_k::assignment:
-            return out << "v" << item.var() << " := " << value(item.var());
+            if (value(item.var(), r))
+                return out << "v" << item.var() << " := " << r;
+            else
+                return out << "v" << item.var() << " := *";
         case search_item_k::boolean:
             return out << item.lit();
         }
@@ -33,12 +37,13 @@ namespace polysat {
         return out;        
     }
 
-    rational search_state::value(pvar v) const {
+    bool search_state::value(pvar v, rational& val) const {
         for (auto const& [p, r] : m_assignment)
-            if (v == p)
+            if (v == p) {
-                return r;
+                val = r;
-        UNREACHABLE();
+                return true;
-        return rational::zero();
+            }
+        return false;
     }   
 
     void search_state::push_assignment(pvar p, rational const& r) {
@@ -46,13 +51,17 @@ namespace polysat {
         m_assignment.push_back({p, r});
     }
 
+    void search_state::pop_asssignment() {
+        m_assignment.pop_back();
+    }
+
     void search_state::push_boolean(sat::literal lit) {
         m_items.push_back(search_item::boolean(lit));
     }
 
     void search_state::pop() {
         auto const& item = m_items.back();
-        if (item.is_assignment()) 
+        if (item.is_assignment() && item.var() == m_assignment.back().first) 
             m_assignment.pop_back();        
         m_items.pop_back();
     }

src/math/polysat/search_state.h

@@ -50,7 +50,7 @@ namespace polysat {
         vector<search_item> m_items;
         assignment_t        m_assignment;  // First-order part of the search state
         
-        rational value(pvar v) const;
+        bool value(pvar v, rational& r) const;
 
     public:
         unsigned size() const { return m_items.size(); }
@@ -63,6 +63,8 @@ namespace polysat {
         void push_boolean(sat::literal lit);
         void pop();
 
+        void pop_asssignment();
+
         using const_iterator = decltype(m_items)::const_iterator;
         const_iterator begin() const { return m_items.begin(); }
         const_iterator end() const { return m_items.end(); }

src/math/polysat/solver.cpp

@@ -486,14 +486,17 @@ namespace polysat {
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();
-                if (!m_conflict.is_pmarked(v) && !m_conflict.is_bailout())
+                if (!m_conflict.is_pmarked(v) && !m_conflict.is_bailout()) {
+                    m_search.pop_asssignment();
                     continue;
+                }
                 justification& j = m_justification[v];
                 LOG("Justification: " << j);
                 if (j.level() > base_level() && !resolve_value(v) && j.is_decision()) {
                     revert_decision(v);
                     return;
                 }
+                m_search.pop_asssignment();
             }
             else {
                 // Resolve over boolean literal
@@ -714,9 +717,11 @@ namespace polysat {
         assign_decision(lit, lemma);
     }
 
-    unsigned solver::level(clause const& cl) {
+    unsigned solver::level(sat::literal lit0, clause const& cl) {
         unsigned lvl = base_level();
         for (auto lit : cl) {
+            if (lit == lit0)
+                continue;
             auto c = lit2cnstr(lit);
             if (m_bvars.is_false(lit) || c.is_currently_false(*this))
                 lvl = std::max(lvl, c.level(*this));
@@ -725,7 +730,7 @@ namespace polysat {
     }
 
     void solver::assign_propagate(sat::literal lit, clause& reason) {
-        m_bvars.propagate(lit, level(reason), reason);
+        m_bvars.propagate(lit, level(lit, reason), reason);
         m_trail.push_back(trail_instr_t::assign_bool_i);
         m_search.push_boolean(lit);
     }

src/math/polysat/solver.h

@@ -146,7 +146,7 @@ namespace polysat {
         void deactivate_constraint(signed_constraint c);
         void decide_bool(clause& lemma);
         void decide_bool(sat::literal lit, clause* lemma);
-        unsigned level(clause const& cl);
+        unsigned level(sat::literal lit, clause const& cl);
 
         void assign_core(pvar v, rational const& val, justification const& j);
         bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }