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 @@ public:
     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);
                 }
             }

src/tactic/fd_solver/smtfd_solver.cpp

@@ -512,6 +512,7 @@ namespace smtfd {
         }
 
         expr_ref eval_abs(expr* t) { return m_context.get_model()(m_abs.abs(t)); }
+        bool is_true_abs(expr* t) { return m_context.get_model().is_true(m_abs.abs(t)); }
         
         expr* value_of(f_app const& f) const { return m_values[f.m_val_offset + f.m_t->get_num_args()]; }
 
@@ -559,10 +560,10 @@ namespace smtfd {
         std::ostream& display(std::ostream& out, table& t) {
             out << "table\n";
             for (auto const& k : t) {
-                out << "key: " << mk_pp(k.m_f, m) << "\nterm: " << mk_pp(k.m_t, m) << "\n";
+                out << "key: " << mk_bounded_pp(k.m_f, m, 2) << "\nterm: " << mk_bounded_pp(k.m_t, m, 2) << "\n";
                 out << "args:\n";
                 for (unsigned i = 0; i <= k.m_t->get_num_args(); ++i) {
-                    out << mk_pp(m_values.get(k.m_val_offset + i), m) << "\n";
+                    out << mk_bounded_pp(m_values.get(k.m_val_offset + i), m, 3) << "\n";
                 }
                 out << "\n";
             }
@@ -855,12 +856,47 @@ namespace smtfd {
     };
 
     class ar_plugin : public theory_plugin {
-        array_util m_autil;
+        array_util      m_autil;
+        unsigned_vector m_num_stores;
+
+        // count number of equivalent stores
+        void update_lambda(expr* t) {
+            if (m_autil.is_store(t)) {
+                expr_ref tV = eval_abs(t);
+                inc_lambda(tV);
+            }
+        }
+
+        unsigned get_lambda(expr* tV) {
+            unsigned id = tV->get_id();
+            if (id >= m_num_stores.size()) {
+                m_num_stores.resize(id + 1, 0);
+            }
+            return m_num_stores[id];
+        }
+
+        void inc_lambda(expr* tV) {
+            unsigned id = tV->get_id();
+            if (id >= m_num_stores.size()) {
+                m_num_stores.resize(id + 1, 0);
+            }
+            if (0 == m_num_stores[id]++) {
+                m_pinned.push_back(tV);
+            }
+        }
+
+        void insert_select(app* t) {
+            expr* a = t->get_arg(0);
+            expr_ref vA = eval_abs(a);
+            check_congruence(vA, t);
+        }
 
         void check_select(app* t) {
             expr* a = t->get_arg(0);
-            expr_ref vA = eval_abs(a);
-            enforce_congruence(vA, t);                     
+            if (!m_autil.is_store(a)) {
+                expr_ref vA = eval_abs(a);
+                enforce_congruence(vA, t);    
+            }                 
         }
 
         // check that (select(t, t.args) = t.value)
@@ -879,9 +915,41 @@ namespace smtfd {
             if (val1 != val2) {
                 TRACE("smtfd", tout << "select/store: " << mk_bounded_pp(t, m, 2) << "\n";);
                 add_lemma(m.mk_eq(sel, stored_value));
+                m_pinned.push_back(sel);
+                insert_select(sel);
+            }
+        }
+
+        // store(A, i, v)[j] = A[i] or i = j
+        void check_select_store(app * t) {
+            SASSERT(m_autil.is_select(t));
+            if (!m_autil.is_store(t->get_arg(0))) {
+                return;
+            }
+            app* store = to_app(t->get_arg(0));
+            expr* a = store->get_arg(0);
+            expr_ref_vector eqs(m);
+            m_args.reset();
+            m_args.push_back(a);
+            bool all_eq = true;
+            for (unsigned i = 1; i < t->get_num_args(); ++i) {
+                expr_ref v1 = eval_abs(t->get_arg(i));
+                expr_ref v2 = eval_abs(store->get_arg(i));
+                if (v1 != v2) all_eq = false;
+                m_args.push_back(t->get_arg(i));
+                eqs.push_back(m.mk_eq(t->get_arg(i), store->get_arg(i)));
+            }
+            if (all_eq) return;
+            
+            app_ref sel(m_autil.mk_select(m_args), m);
+            expr_ref val1 = eval_abs(sel);
+            expr_ref val2 = eval_abs(t);
+            if (val1 != val2) {
+                TRACE("smtfd", tout << "select/store: " << mk_bounded_pp(t, m, 2) << "\n";);                
+                add_lemma(m.mk_or(m.mk_eq(sel, t), mk_and(eqs)));
+                m_pinned.push_back(sel);
+                insert_select(sel);
             }
-            m_pinned.push_back(sel);
-            check_select(sel);
         }
 
         /** 
@@ -897,7 +965,7 @@ namespace smtfd {
             where j is in tableA and value equal to some index in tableT
 
         */
-        void check_store1(app* t) {
+        void check_store2(app* t) {
             SASSERT(m_autil.is_store(t));
 
             expr* arg = t->get_arg(0);
@@ -915,7 +983,7 @@ namespace smtfd {
             for (unsigned i = 0; i + 1 < t->get_num_args(); ++i) {
                 m_vargs.push_back(eval_abs(t->get_arg(i)));
             }            
-            reconcile_stores(t, tT, tA);
+            reconcile_stores(t, vT, tT, vA, tA);
         }
         
         //
@@ -923,25 +991,42 @@ namespace smtfd {
         // T[j] = w: i = j or A[j] = T[j]
         // A[j] = w: i = j or T[j] = A[j]
         // 
-        void reconcile_stores(app* t, table& tT, table& tA) {
+        void reconcile_stores(app* t, expr* vT, table& tT, expr* vA, table& tA) {
+            unsigned r = 0;
+            if (get_lambda(vA) <= 1) {
+                return;
+            }
+            inc_lambda(vT);
             for (auto& fA : tA) {
                 f_app fT;
                 if (m_context.at_max()) {
                     break;
                 }
                 if (!tT.find(fA, fT) || (value_of(fA) != value_of(fT) && !eq(m_vargs, fA))) {
+                    TRACE("smtfd", tout << "found: " << tT.find(fA, fT) << "\n";);
                     add_select_store_axiom(t, fA);
+                    ++r;
                 }
             }            
+#if 0
+    // only up-propagation really needed.
             for (auto& fT : tT) {
                 f_app fA;
                 if (m_context.at_max()) {
                     break;
                 }
                 if (!tA.find(fT, fA)) {
+                    TRACE("smtfd", tout << "not found\n";);
                     add_select_store_axiom(t, fT);
+                    ++r;
                 }
             }
+#endif
+            if (r > 0 && false) {
+                std::cout << r << " " << mk_bounded_pp(t, m, 3) << "\n"; 
+                display(std::cout, tT); 
+                display(std::cout, tA);
+            }
         }
 
         void add_select_store_axiom(app* t, f_app& f) {
@@ -956,8 +1041,10 @@ namespace smtfd {
             expr_ref sel1(m_autil.mk_select(m_args), m);
             m_args[0] = a;
             expr_ref sel2(m_autil.mk_select(m_args), m);
-            TRACE("smtfd", tout << mk_bounded_pp(t, m, 2) << "\n";);
-            add_lemma(m.mk_or(eq, m.mk_eq(sel1, sel2)));
+            expr_ref fml(m.mk_or(eq, m.mk_eq(sel1, sel2)), m);
+            if (!is_true_abs(fml)) {
+                add_lemma(fml);
+            }
         }
 
         bool same_array_sort(f_app const& fA, f_app const& fT) const {
@@ -1080,26 +1167,36 @@ namespace smtfd {
             theory_plugin(context),
             m_autil(m)
         {}
+
+        void reset() override {
+            theory_plugin::reset();
+            m_num_stores.reset();
+        }
         
         void check_term(expr* t, unsigned round) override {
-            TRACE("smtfd", tout << mk_bounded_pp(t, m, 2) << "\n";);
             switch (round) {
             case 0:
                 if (m_autil.is_select(t)) {
-                    check_select(to_app(t));
+                    insert_select(to_app(t));
                 }
-                if (m_autil.is_store(t)) {
+                else if (m_autil.is_store(t)) {
+                    update_lambda(t);
                     check_store0(to_app(t));
                 }
                 break;
             case 1:
-                if (m_autil.is_store(t)) {
-                    check_store1(to_app(t));
+                if (m_autil.is_select(t)) {
+                    check_select(to_app(t));
                 }
                 else {
                     beta_reduce(t);
                 }
                 break;
+            case 2:
+                if (m_autil.is_store(t)) {
+                    check_store2(to_app(t));
+                }
+                break;
             default:
                 break;
             }
@@ -1165,7 +1262,7 @@ namespace smtfd {
             }
         }
 
-        unsigned max_rounds() override { return 2; }
+        unsigned max_rounds() override { return 3; }
 
         void global_check(expr_ref_vector const& core) override {  
             expr_mark seen;
@@ -1667,8 +1764,8 @@ namespace smtfd {
         }
 
         void flush_atom_defs() {
+            TRACE("smtfd", for (expr* f : m_abs.atom_defs()) tout << mk_bounded_pp(f, m, 4) << "\n";);
             for (expr* f : m_abs.atom_defs()) {
-                TRACE("smtfd", tout << mk_bounded_pp(f, m, 4) << "\n";);
                 m_fd_sat_solver->assert_expr(f);
                 m_fd_core_solver->assert_expr(f);
             }
@@ -1809,11 +1906,14 @@ namespace smtfd {
                     ++round;
                     continue;
                 }
+                IF_VERBOSE(1, verbose_stream() << "(smtfd-round " << round << " " << m_context.size() << ")\n");
                 round = 0;
+                TRACE("smtfd_verbose", 
+                      for (expr* f : m_context) tout << "refine " << mk_bounded_pp(f, m, 3) << "\n";
+                      m_context.display(tout););
                 for (expr* f : m_context) {
-                    TRACE("smtfd_verbose", tout << "refine " << mk_bounded_pp(f, m, 3) << "\n";);
                     core.push_back(f);
-                }
+                }                
                 m_stats.m_num_lemmas += m_context.size();
                 r = check_abs(core.size(), core.c_ptr());
                 update_reason_unknown(r, m_fd_sat_solver);
@@ -1846,7 +1946,7 @@ namespace smtfd {
                 m_fd_core_solver->updt_params(p);  
                 m_smt_solver->updt_params(p);  
             }
-            m_context.set_max_lemmas(p.get_uint("max-lemmas", 100));
+            m_context.set_max_lemmas(UINT_MAX); // p.get_uint("max-lemmas", 100));
         }        
 
         void collect_param_descrs(param_descrs & r) override {