use propagation filter

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

src/ast/for_each_expr.cpp

@@ -109,3 +109,67 @@ bool subterms::iterator::operator!=(iterator const& other) const {
     return !(*this == other);
 }
 
+
+subterms_postorder::subterms_postorder(expr_ref_vector const& es): m_es(es) {}
+subterms_postorder::subterms_postorder(expr_ref& e) : m_es(e.m()) { m_es.push_back(e); }
+subterms_postorder::iterator subterms_postorder::begin() { return iterator(*this, true); }
+subterms_postorder::iterator subterms_postorder::end() { return iterator(*this, false); }
+subterms_postorder::iterator::iterator(subterms_postorder& f, bool start): m_es(f.m_es) {
+    if (!start) m_es.reset();
+    next();
+}
+expr* subterms_postorder::iterator::operator*() {
+    return m_es.back();
+}
+subterms_postorder::iterator subterms_postorder::iterator::operator++(int) {
+    iterator tmp = *this;
+    ++*this;
+    return tmp;
+}
+
+void subterms_postorder::iterator::next() {
+    while (!m_es.empty()) {
+        expr* e = m_es.back();
+        if (m_visited.is_marked(e)) {
+            m_es.pop_back();
+            continue;
+        }
+        bool all_visited = true;
+        if (is_app(e)) {
+            for (expr* arg : *to_app(e)) {
+                if (!m_visited.is_marked(arg)) {
+                    m_es.push_back(arg);
+                    all_visited = false;
+                }
+            }
+        }
+        if (all_visited) {
+            m_visited.mark(e, true);
+            break;
+        }
+    }
+
+}
+
+subterms_postorder::iterator& subterms_postorder::iterator::operator++() {
+    expr* e = m_es.back();
+    next();
+    return *this;
+}
+
+bool subterms_postorder::iterator::operator==(iterator const& other) const {
+    // ignore state of visited
+    if (other.m_es.size() != m_es.size()) {
+        return false;
+    }
+    for (unsigned i = m_es.size(); i-- > 0; ) {
+        if (m_es.get(i) != other.m_es.get(i))
+            return false;
+    }
+    return true;
+}
+
+bool subterms_postorder::iterator::operator!=(iterator const& other) const {
+    return !(*this == other);
+}
+

src/ast/for_each_expr.h

@@ -167,6 +167,7 @@ unsigned get_num_exprs(expr * n, expr_fast_mark1 & visited);
 
 bool has_skolem_functions(expr * n);
 
+// pre-order traversal of subterms
 class subterms {
     expr_ref_vector m_es;
 public:
@@ -187,5 +188,26 @@ class subterms {
     iterator end();
 };
 
+class subterms_postorder {
+    expr_ref_vector m_es;
+public:
+    class iterator {
+        expr_ref_vector m_es;
+        expr_mark       m_visited, m_seen; 
+        void next();
+    public:
+        iterator(subterms_postorder& f, bool start);
+        expr* operator*();
+        iterator operator++(int);
+        iterator& operator++();
+        bool operator==(iterator const& other) const;
+        bool operator!=(iterator const& other) const;
+    };
+    subterms_postorder(expr_ref_vector const& es);
+    subterms_postorder(expr_ref& e);
+    iterator begin();
+    iterator end();
+};
+
 #endif /* FOR_EACH_EXPR_H_ */
 

src/sat/sat_solver.cpp

@@ -388,15 +388,15 @@ namespace sat {
         m_touched[l1.var()] = m_touch_index;
         m_touched[l2.var()] = m_touch_index;
 
-        if (find_binary_watch(get_wlist(~l1), ~l2) && value(l1) == l_undef) {
+        if (learned && find_binary_watch(get_wlist(~l1), ~l2) && value(l1) == l_undef) {
             assign_unit(l1);
             return;
         }
-        if (find_binary_watch(get_wlist(~l2), ~l1) && value(l2) == l_undef) {
+        if (learned && find_binary_watch(get_wlist(~l2), ~l1) && value(l2) == l_undef) {
             assign_unit(l2);
             return;
         }
-        watched* w0 = find_binary_watch(get_wlist(~l1), l2);
+        watched* w0 = learned ? find_binary_watch(get_wlist(~l1), l2) : nullptr;
         if (w0) {
             TRACE("sat", tout << "found binary " << l1 << " " << l2 << "\n";);
             if (w0->is_learned() && !learned) {

src/smt/smt_model_finder.cpp

@@ -483,7 +483,7 @@ namespace smt {
             }
 
             void set_context(context * ctx) {
-                SASSERT(m_context==0);
+                SASSERT(m_context== nullptr);
                 m_context = ctx;
             }
 
@@ -1065,12 +1065,14 @@ namespace smt {
 
             void mk_inverse(node * n) {
                 SASSERT(n->is_root());
-                instantiation_set * s                 = n->get_instantiation_set();
+                instantiation_set * s = n->get_instantiation_set();
                 s->mk_inverse(*this);
             }
 
             void mk_inverses() {
-                for (node * n : m_root_nodes) {
+                unsigned offset = m_context->get_random_value();
+                for (unsigned i = m_root_nodes.size(); i-- > 0; ) {
+                    node* n = m_root_nodes[(i + offset) % m_root_nodes.size()];
                     SASSERT(n->is_root());
                     mk_inverse(n);
                 }
@@ -1838,7 +1840,7 @@ namespace smt {
                 for (qinfo* qi : m_qinfo_vect)
                     qi->populate_inst_sets(m_flat_q, m_the_one, *m_uvar_inst_sets, ctx);
                 for (instantiation_set * s : *m_uvar_inst_sets) {
-                    if (s != nullptr)
+                    if (s != nullptr) 
                         s->mk_inverse(ev);
                 }
             }