remaining issue fixes

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

src/math/dd/dd_pdd.cpp

@@ -253,7 +253,7 @@ namespace dd {
     }
 
     pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) {
-        bool first = true;
+        unsigned count = 0;
         SASSERT(well_formed());
         scoped_push _sp(*this);
         while (true) {
@@ -262,8 +262,9 @@ namespace dd {
             }
             catch (const mem_out &) {
                 try_gc();
-                if (!first) throw;
+                if (count > 0)
-                first = false;
+                    m_max_num_nodes *= 2;
+                count++;
             }
         }
         SASSERT(well_formed());
@@ -514,7 +515,7 @@ namespace dd {
         if (m_semantics == mod2_e) {
             return a;
         }
-        bool first = true;
+        unsigned count = 0;
         SASSERT(well_formed());
         scoped_push _sp(*this);
         while (true) {
@@ -523,8 +524,9 @@ namespace dd {
             }
             catch (const mem_out &) {
                 try_gc();
-                if (!first) throw;
+                if (count > 0)
-                first = false;
+                    m_max_num_nodes *= 2;
+                ++count;                
             }
         }
         SASSERT(well_formed());        
@@ -572,7 +574,7 @@ namespace dd {
             return true;
         }
         SASSERT(c.is_int());
-        bool first = true;
+        unsigned count = 0;
         SASSERT(well_formed());
         scoped_push _sp(*this);
         while (true) {
@@ -585,8 +587,9 @@ namespace dd {
             }
             catch (const mem_out &) {
                 try_gc();
-                if (!first) throw;
+                if (count > 0)
-                first = false;
+                    m_max_num_nodes *= 2;
+                ++count;
             }
         }
     }
@@ -1363,9 +1366,8 @@ namespace dd {
             e->get_data().m_refcount = 0;      
         }
         if (do_gc) {
-            if (m_nodes.size() > m_max_num_nodes) {
+            if (m_nodes.size() > m_max_num_nodes) 
                 throw mem_out();            
-            }
             alloc_free_nodes(m_nodes.size()/2);
         }
         SASSERT(e->get_data().m_lo == n.m_lo);

src/math/polysat/constraint_manager.cpp

@@ -149,7 +149,8 @@ namespace polysat {
         s.m_bvars.watch(cl[1]).push_back(&cl);
 
         if (s.m_bvars.is_true(cl[0])) 
-            return false;
+            return !is_chronological(cl);
+        
         SASSERT(!s.m_bvars.is_true(cl[1]));
         if (!s.m_bvars.is_false(cl[1])) {
             SASSERT(!s.m_bvars.is_assigned(cl[0]) && !s.m_bvars.is_assigned(cl[1]));
@@ -169,6 +170,20 @@ namespace polysat {
         s.m_bvars.watch(cl[1]).erase(&cl);
     }
 
+    // return false if the level of cl[0] is above the level of all 
+    // other literals in cl. In this case cl[0] is obtained by unit propagation
+    // at a lower level.
+    bool constraint_manager::is_chronological(clause const& cl) const {
+        unsigned level = s.m_bvars.level(cl[0]);
+        for (unsigned i = 1; i < cl.size(); ++i) {
+            if (!s.m_bvars.is_false(cl[i]))
+                return true;
+            if (level <= s.m_bvars.level(cl[i]))
+                return true;
+        }
+        return false;
+    }
+
     constraint_manager::~constraint_manager() {
         // Release explicitly to check for leftover references in debug mode,
         // and to make sure all constraints are destructed before the bvar->constraint mapping.

src/math/polysat/constraint_manager.h

@@ -83,6 +83,8 @@ namespace polysat {
         void ensure_bvar(constraint* c);
         void erase_bvar(constraint* c);
 
+        bool is_chronological(clause const& c) const;
+        
         signed_constraint mk_op_constraint(op_constraint::code op, pdd const& p, pdd const& q, pdd const& r);
         pdd mk_op_term(op_constraint::code op, pdd const& p, pdd const& q);
 

src/math/polysat/solver.cpp

@@ -28,7 +28,7 @@ Author:
 // Lemmas are written into the folder "dbg-lemmas", and only if that folder already exists.
 #define ENABLE_LEMMA_VALIDITY_CHECK 0
 
-#define ENABLE_REINIT_STACK 0
+#define ENABLE_REINIT_STACK 1
 
 namespace polysat {