disable cancelation during propagation at base level

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

src/model/func_interp.cpp

@@ -203,7 +203,7 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) {
            }
            tout << "Old: " << mk_ismt2_pp(get_entry(args)->get_result(), m_manager) << "\n";
            );
-    SASSERT(get_entry(args) == 0);
+    SASSERT(get_entry(args) == nullptr);
     func_entry * new_entry = func_entry::mk(m_manager, m_arity, args, r);
     if (!new_entry->args_are_values())
         m_args_are_values = false;

src/smt/smt_cg_table.cpp

@@ -22,81 +22,6 @@ Revision History:
 
 namespace smt {
 
-#if 0
-    unsigned cg_table::cg_hash::operator()(enode * n) const {
-        if (n->is_commutative()) {
-            return  combine_hash(n->get_decl_id(), 
-                                 n->get_arg(0)->get_root()->hash() *
-                                 n->get_arg(1)->get_root()->hash());
-        }
-        else {
-            unsigned num = n->get_num_args();
-            switch (num) {
-            case 0: UNREACHABLE(); return 0;
-            case 1: 
-                return combine_hash(n->get_decl_id(), n->get_arg(0)->get_root()->hash());
-            case 2: {
-                unsigned a = n->get_decl_id();
-                unsigned b = n->get_arg(0)->get_root()->hash();
-                unsigned c = n->get_arg(1)->get_root()->hash();
-                mix(a,b,c);
-                return c;
-            }
-            default:
-                return get_composite_hash<enode *, cg_khasher, cg_chasher>(n, n->get_num_args(), m_khasher, m_chasher);
-            }
-        }
-    }
-
-    bool cg_table::cg_eq::operator()(enode * n1, enode * n2) const {
-#if 0
-        static unsigned counter = 0;
-        static unsigned failed  = 0;
-        bool r = congruent(n1, n2, m_commutativity);
-        if (!r) 
-            failed++;
-        counter++;
-        if (counter % 100000 == 0) 
-            std::cout << "cg_eq: " << counter << " " << failed << "\n";
-        return r;
-#else
-        return congruent(n1, n2, m_commutativity);
-#endif
-    }
-    
-    cg_table::cg_table(ast_manager & m):
-        m_manager(m),
-        m_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, cg_hash(), cg_eq(m_commutativity)) {
-    }
-    
-    void cg_table::display(std::ostream & out) const {
-        out << "congruence table:\n";
-        for (enode * n : m_table) {
-            out << mk_pp(n->get_owner(), m_manager) << "\n";
-        }
-    }
-
-    void cg_table::display_compact(std::ostream & out) const {
-        if (!m_table.empty()) {
-            out << "congruence table:\n";
-            for (enode * n : m_table) {
-                out << "#" << n->get_owner()->get_id() << " ";
-            }
-            out << "\n";
-        }
-    }
-
-#ifdef Z3DEBUG
-    bool cg_table::check_invariant() const {
-        for (enode * n : m_table) {
-            CTRACE("cg_table", !contains_ptr(n), tout << "#" << n->get_owner_id() << "\n";);
-            SASSERT(contains_ptr(n));
-        }
-        return true;
-    }
-#endif
-
-#else
     // one table per func_decl implementation
     unsigned cg_table::cg_hash::operator()(enode * n) const {
         SASSERT(n->get_decl()->is_flat_associative() || n->get_num_args() >= 3);
@@ -222,18 +147,116 @@ namespace smt {
     }
 
     void cg_table::display(std::ostream & out) const {
+        for (auto const& kv : m_func_decl2id) {
+            void * t = m_tables[kv.m_value];
+            out << mk_pp(kv.m_key, m_manager) << ": ";
+            switch (GET_TAG(t)) {
+            case UNARY: 
+                display_unary(out, t);
+                break;            
+            case BINARY: 
+                display_binary(out, t);
+                break;
+            case BINARY_COMM: 
+                display_binary_comm(out, t);
+                break;            
+            case NARY: 
+                display_nary(out, t);
+                break;
             }
+        }        
+    }
+
+    void cg_table::display_binary(std::ostream& out, void* t) const {
+        binary_table* tb = UNTAG(binary_table*, t);
+        out << "b ";
+        for (enode* n : *tb) {
+            out << n->get_owner_id() << " " << cg_binary_hash()(n) << " ";
+        }
+        out << "\n";
+    }
+    
+    void cg_table::display_binary_comm(std::ostream& out, void* t) const {
+        comm_table* tb = UNTAG(comm_table*, t);
+        out << "bc ";
+        for (enode* n : *tb) {
+            out << n->get_owner_id() << " ";
+        }
+        out << "\n";
+    }
+    
+    void cg_table::display_unary(std::ostream& out, void* t) const {
+        unary_table* tb = UNTAG(unary_table*, t);
+        out << "un ";
+        for (enode* n : *tb) {
+            out << n->get_owner_id() << " ";
+        }
+        out << "\n";
+    }
+    
+    void cg_table::display_nary(std::ostream& out, void* t) const {
+        table* tb = UNTAG(table*, t);
+        out << "nary ";
+        for (enode* n : *tb) {
+            out << n->get_owner_id() << " ";
+        }
+        out << "\n";
+    }
+
+
+    enode_bool_pair cg_table::insert(enode * n) {
+        // it doesn't make sense to insert a constant.
+        SASSERT(n->get_num_args() > 0);
+        SASSERT(!m_manager.is_and(n->get_owner()));
+        SASSERT(!m_manager.is_or(n->get_owner()));
+        enode * n_prime;
+        void * t = get_table(n); 
+        switch (static_cast<table_kind>(GET_TAG(t))) {
+        case UNARY:
+            n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n);
+            return enode_bool_pair(n_prime, false);
+        case BINARY:
+            n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n);
+            TRACE("cg_table", tout << "insert: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " inserted: " << (n == n_prime) << " " << n_prime->get_owner_id() << "\n";
+                  display_binary(tout, t); tout << "contains_ptr: " << contains_ptr(n) << "\n";); 
+            return enode_bool_pair(n_prime, false);
+        case BINARY_COMM:
+            m_commutativity = false;
+            n_prime = UNTAG(comm_table*, t)->insert_if_not_there(n);
+            return enode_bool_pair(n_prime, m_commutativity);
+        default:
+            n_prime = UNTAG(table*, t)->insert_if_not_there(n);
+            return enode_bool_pair(n_prime, false);
+        }
+    }
+
+    void cg_table::erase(enode * n) {
+        SASSERT(n->get_num_args() > 0);
+        void * t = get_table(n); 
+        switch (static_cast<table_kind>(GET_TAG(t))) {
+        case UNARY:
+            UNTAG(unary_table*, t)->erase(n);
+            break;
+        case BINARY:
+            TRACE("cg_table", tout << "erase: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " contains: " << contains_ptr(n) << "\n";);
+            UNTAG(binary_table*, t)->erase(n);
+            break;
+        case BINARY_COMM:
+            UNTAG(comm_table*, t)->erase(n);
+            break;
+        default:
+            UNTAG(table*, t)->erase(n);
+            break;
+        }
+    }
+
 
     void cg_table::display_compact(std::ostream & out) const {
     }
 
-#ifdef Z3DEBUG
     bool cg_table::check_invariant() const {
         return true;
     }
-#endif
-
-#endif
 
 };
 

src/smt/smt_cg_table.h

@@ -27,89 +27,6 @@ namespace smt {
 
     typedef std::pair<enode *, bool> enode_bool_pair;
     
-#if 0
-    /**
-       \brief Congruence table.
-    */
-    class cg_table {
-        struct cg_khasher {
-            unsigned operator()(enode const * n) const { return n->get_decl_id(); }
-        };
-
-        struct cg_chasher {
-            unsigned operator()(enode const * n, unsigned idx) const { 
-                return n->get_arg(idx)->get_root()->hash();
-            }
-        };
-
-        struct cg_hash {
-            cg_khasher m_khasher;
-            cg_chasher m_chasher;
-        public:
-            unsigned operator()(enode * n) const;
-        };
-
-        struct cg_eq {
-            bool & m_commutativity; 
-            cg_eq(bool & comm):m_commutativity(comm) {}
-            bool operator()(enode * n1, enode * n2) const;
-        };
-
-        typedef ptr_hashtable<enode, cg_hash, cg_eq> table;
-
-        ast_manager &             m_manager;
-        bool                      m_commutativity; //!< true if the last found congruence used commutativity
-        table                     m_table;
-    public:
-        cg_table(ast_manager & m);
-
-        /**
-           \brief Try to insert n into the table. If the table already
-           contains an element n' congruent to n, then do nothing and
-           return n' and a boolean indicating whether n and n' are congruence
-           modulo commutativity, otherwise insert n and return (n,false).
-        */
-        enode_bool_pair insert(enode * n) {
-            // it doesn't make sense to insert a constant.
-            SASSERT(n->get_num_args() > 0);
-            m_commutativity = false;
-            enode * n_prime = m_table.insert_if_not_there(n); 
-            SASSERT(contains(n));
-            return enode_bool_pair(n_prime, m_commutativity);
-        }
-
-        void erase(enode * n) {
-            SASSERT(n->get_num_args() > 0);
-            m_table.erase(n);
-            SASSERT(!contains(n));
-        }
-
-        bool contains(enode * n) const {
-            return m_table.contains(n);
-        }
-
-        enode * find(enode * n) const {
-            enode * r = 0;
-            return m_table.find(n, r) ? r : 0;
-        }
-
-        bool contains_ptr(enode * n) const {
-            enode * n_prime;
-            return m_table.find(n, n_prime) && n == n_prime;
-        }
-
-        void reset() {
-            m_table.reset();
-        }
-
-        void display(std::ostream & out) const;
-
-        void display_compact(std::ostream & out) const;
-#ifdef Z3DEBUG
-        bool check_invariant() const;
-#endif
-    };
-#else 
     // one table per function symbol
 
     /**
@@ -137,9 +54,6 @@ namespace smt {
         struct cg_binary_hash {
             unsigned operator()(enode * n) const {
                 SASSERT(n->get_num_args() == 2);
-                // too many collisions
-                // unsigned r = 17 + n->get_arg(0)->get_root()->hash();
-                // return r * 31 + n->get_arg(1)->get_root()->hash();
                 return combine_hash(n->get_arg(0)->get_root()->hash(), n->get_arg(1)->get_root()->hash());
             }
         };
@@ -149,23 +63,9 @@ namespace smt {
                 SASSERT(n1->get_num_args() == 2);
                 SASSERT(n2->get_num_args() == 2);
                 SASSERT(n1->get_decl() == n2->get_decl());
-#if 1
                 return 
                     n1->get_arg(0)->get_root() == n2->get_arg(0)->get_root() &&
                     n1->get_arg(1)->get_root() == n2->get_arg(1)->get_root();
-#else
-                bool r = 
-                    n1->get_arg(0)->get_root() == n2->get_arg(0)->get_root() &&
-                    n1->get_arg(1)->get_root() == n2->get_arg(1)->get_root();
-                static unsigned counter = 0;
-                static unsigned failed  = 0;
-                if (!r) 
-                    failed++;
-                counter++;
-                if (counter % 100000 == 0) 
-                    std::cerr << "[cg_eq] " << counter << " " << failed << "\n";
-                return r;
-#endif
             }
         };
 
@@ -249,48 +149,9 @@ namespace smt {
            return n' and a boolean indicating whether n and n' are congruence
            modulo commutativity, otherwise insert n and return (n,false).
         */
-        enode_bool_pair insert(enode * n) {
+        enode_bool_pair insert(enode * n);
-            // it doesn't make sense to insert a constant.
-            SASSERT(n->get_num_args() > 0);
-            SASSERT(!m_manager.is_and(n->get_owner()));
-            SASSERT(!m_manager.is_or(n->get_owner()));
-            enode * n_prime;
-            void * t = get_table(n); 
-            switch (static_cast<table_kind>(GET_TAG(t))) {
-            case UNARY:
-                n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n);
-                return enode_bool_pair(n_prime, false);
-            case BINARY:
-                n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n);
-                return enode_bool_pair(n_prime, false);
-            case BINARY_COMM:
-                m_commutativity = false;
-                n_prime = UNTAG(comm_table*, t)->insert_if_not_there(n);
-                return enode_bool_pair(n_prime, m_commutativity);
-            default:
-                n_prime = UNTAG(table*, t)->insert_if_not_there(n);
-                return enode_bool_pair(n_prime, false);
-            }
-        }
 
-        void erase(enode * n) {
+        void erase(enode * n);
-            SASSERT(n->get_num_args() > 0);
-            void * t = get_table(n); 
-            switch (static_cast<table_kind>(GET_TAG(t))) {
-            case UNARY:
-                UNTAG(unary_table*, t)->erase(n);
-                break;
-            case BINARY:
-                UNTAG(binary_table*, t)->erase(n);
-                break;
-            case BINARY_COMM:
-                UNTAG(comm_table*, t)->erase(n);
-                break;
-            default:
-                UNTAG(table*, t)->erase(n);
-                break;
-            }
-        }
 
         bool contains(enode * n) const {
             SASSERT(n->get_num_args() > 0);
@@ -343,13 +204,19 @@ namespace smt {
 
         void display(std::ostream & out) const;
 
+        void display_binary(std::ostream& out, void* t) const;
+
+        void display_binary_comm(std::ostream& out, void* t) const;
+
+        void display_unary(std::ostream& out, void* t) const;
+
+        void display_nary(std::ostream& out, void* t) const;
+
         void display_compact(std::ostream & out) const;
-#ifdef Z3DEBUG
+
         bool check_invariant() const;
-#endif
     };
 
-#endif 
 };
 
 #endif /* SMT_CG_TABLE_H_ */

src/smt/smt_context.cpp

@@ -86,7 +86,8 @@ namespace smt {
         m_generation(0),
         m_last_search_result(l_undef),
         m_last_search_failure(UNKNOWN),
-        m_searching(false) {
+        m_searching(false),
+        m_propagating(false) {
 
         SASSERT(m_scope_lvl == 0);
         SASSERT(m_base_lvl == 0);
@@ -131,8 +132,13 @@ namespace smt {
         return literal(v, lit.sign());
     }
 
+    /**
+       \brief retrieve flag for when cancelation is possible.
+       Cancelation is not safe during propagation at base level because
+       congruences cannot be retracted to a consistent state.
+     */
     bool context::get_cancel_flag() {
-        return !m_manager.limit().inc();
+        return !m_manager.limit().inc() && !(at_base_level() && m_propagating);
     }
 
     void context::updt_params(params_ref const& p) {
@@ -548,14 +554,10 @@ namespace smt {
                 mark_as_relevant(r1);
             }
 
-            TRACE("add_eq", tout << "to trail\n";);
-
             push_trail(add_eq_trail(r1, n1, r2->get_num_parents()));
 
-            TRACE("add_eq", tout << "qmanager add_eq\n";);
             m_qmanager->add_eq_eh(r1, r2);
 
-            TRACE("add_eq", tout << "merge theory_vars\n";);
             merge_theory_vars(n2, n1, js);
 
             // 'Proof' tree
@@ -571,25 +573,6 @@ namespace smt {
             // r1 -> ..  -> n1 -> n2 -> ... -> r2
 
 
-#if 0
-            {
-                static unsigned counter      = 0;
-                static unsigned num_adds     = 0;
-                static unsigned num_bad_adds = 0;
-                num_adds++;
-                if (r1->get_class_size() <= r2->get_class_size() &&
-                    r1->m_parents.size() > r2->m_parents.size()) {
-                    num_bad_adds++;
-                }
-                if (num_adds % 100000 == 0) {
-                    verbose_stream() << "[add-eq]: " << num_bad_adds << " " << num_adds << " "
-                                     << static_cast<double>(num_bad_adds)/static_cast<double>(num_adds) << "\n";
-                }
-            }
-#endif
-
-
-            TRACE("add_eq", tout << "remove_parents_from_cg_table\n";);
             remove_parents_from_cg_table(r1);
 
             enode * curr = r1;
@@ -600,11 +583,8 @@ namespace smt {
             while(curr != r1);
 
             SASSERT(r1->get_root() == r2);
-
-            TRACE("add_eq", tout << "reinsert_parents_into_cg_table\n";);
             reinsert_parents_into_cg_table(r1, r2, n1, n2, js);
 
-            TRACE("add_eq", tout << "propagate_bool_enode_assignment\n";);
             if (n2->is_bool())
                 propagate_bool_enode_assignment(r1, r2, n1, n2);
 
@@ -632,25 +612,21 @@ namespace smt {
     void context::remove_parents_from_cg_table(enode * r1) {
         // Remove parents from the congruence table
         for (enode * parent : enode::parents(r1)) {
-#if 0
+            CTRACE("add_eq", !parent->is_marked() && parent->is_cgc_enabled() && parent->is_true_eq() && m_cg_table.contains_ptr(parent), tout << parent->get_owner_id() << "\n";);
-            {
+            CTRACE("add_eq", !parent->is_marked() && parent->is_cgc_enabled() && !parent->is_true_eq() &&  parent->is_cgr() && !m_cg_table.contains_ptr(parent), 
-                static unsigned num_eqs = 0;
+                   tout << "cgr !contains " << parent->get_owner_id() << " " << mk_pp(parent->get_decl(), m_manager) << "\n";
-                static unsigned num_parents = 0;
+                   for (enode* n : enode::args(parent))  tout << n->get_root()->get_owner_id() << " " << n->get_root()->hash() << " ";
-                static unsigned counter = 0;
+                   tout << "\n";
-                if (parent->is_eq())
+                   tout << "contains: " << m_cg_table.contains(parent) << "\n";
-                    num_eqs++;
+                   if (m_cg_table.contains(parent)) {
-                num_parents++;
+                       tout << "owner: " << m_cg_table.find(parent)->get_owner_id() << "\n";
-                if (num_parents % 100000 == 0) {
-                    verbose_stream() << "[remove-cg] " << num_eqs << " " << num_parents << " "
-                              << static_cast<double>(num_eqs)/static_cast<double>(num_parents) << "\n";
                    }
-            }
+                   m_cg_table.display(tout);
-#endif
+                   );
-            SASSERT(parent->is_marked() || !parent->is_cgc_enabled() ||
+            CTRACE("add_eq", !parent->is_marked() && parent->is_cgc_enabled() && !parent->is_true_eq() && !parent->is_cgr() &&  m_cg_table.contains_ptr(parent), tout << "!cgr contains " << parent->get_owner_id() << "\n";);
-                    (!parent->is_true_eq() && parent->is_cgr() == m_cg_table.contains_ptr(parent)) ||
+            SASSERT(parent->is_marked() || !parent->is_cgc_enabled() ||  parent->is_true_eq() || parent->is_cgr() == m_cg_table.contains_ptr(parent));
-                    (parent->is_true_eq() && !m_cg_table.contains_ptr(parent)));
+            SASSERT(parent->is_marked() || !parent->is_cgc_enabled() || !parent->is_true_eq() || !m_cg_table.contains_ptr(parent));
             if (!parent->is_marked() && parent->is_cgr() && !parent->is_true_eq()) {
-                TRACE("add_eq_parents", tout << "add_eq removing: #" << parent->get_owner_id() << "\n";);
                 SASSERT(!parent->is_cgc_enabled() || m_cg_table.contains_ptr(parent));
                 parent->set_mark();
                 if (parent->is_cgc_enabled()) {
@@ -704,7 +680,6 @@ namespace smt {
                 enode_bool_pair pair = m_cg_table.insert(parent);
                 enode * parent_prime = pair.first;
                 if (parent_prime == parent) {
-                    TRACE("add_eq_parents", tout << "add_eq reinserting: #" << parent->get_owner_id() << "\n";);
                     SASSERT(parent);
                     SASSERT(parent->is_cgr());
                     SASSERT(m_cg_table.contains_ptr(parent));
@@ -983,7 +958,6 @@ namespace smt {
         for (; it != end; ++it) {
             enode * parent = *it;
             if (parent->is_cgc_enabled()) {
-                TRACE("add_eq_parents", tout << "removing: #" << parent->get_owner_id() << "\n";);
                 CTRACE("add_eq", !parent->is_cgr() || !m_cg_table.contains_ptr(parent),
                        tout << "old num_parents: " << r2_num_parents << ", num_parents: " << r2->m_parents.size() << ", parent: #" <<
                        parent->get_owner_id() << ", parents: \n";
@@ -1016,9 +990,8 @@ namespace smt {
                     (parent == cg ||           // parent was root of the congruence class before and after the merge
                      !congruent(parent, cg)    // parent was root of the congruence class before but not after the merge
                      )) {
-                    TRACE("add_eq_parents", tout << "trying to reinsert\n";);
+                    enode_bool_pair p = m_cg_table.insert(parent);
-                    m_cg_table.insert(parent);
+                    parent->m_cg = p.first;
-                    parent->m_cg         = parent;
                 }
             }
         }
@@ -1353,13 +1326,14 @@ namespace smt {
        \remark The method assign_eq adds a new entry on this queue.
     */
     bool context::propagate_eqs() {
-        TRACE("add_eq", tout << m_eq_propagation_queue.size() << "\n";);
+        unsigned i = 0;
-        for (unsigned i = 0; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) {
+        for (; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) {
             new_eq & entry = m_eq_propagation_queue[i];
             add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification);
             if (inconsistent())
                 return false;
         }
+        TRACE("add_eq", tout << m_eq_propagation_queue.size() << " " << i << "\n";);
         m_eq_propagation_queue.reset();
         return true;
     }
@@ -1728,6 +1702,7 @@ namespace smt {
     }
 
     bool context::propagate() {
+        flet<bool> _prop(m_propagating, true);
         TRACE("propagate", tout << "propagating... " << m_qhead << ":" << m_assigned_literals.size() << "\n";);
         while (true) {
             if (inconsistent())
@@ -4449,7 +4424,7 @@ namespace smt {
 
     void context::add_rec_funs_to_model() {
         ast_manager& m = m_manager;
-        SASSERT(m_model);
+        if (!m_model) return;
         for (unsigned i = 0; !get_cancel_flag() && i < m_asserted_formulas.get_num_formulas(); ++i) {
             expr* e = m_asserted_formulas.get_formula(i);
             if (is_quantifier(e)) {

src/smt/smt_context.h

@@ -923,6 +923,7 @@ namespace smt {
         failure            m_last_search_failure;
         ptr_vector<theory> m_incomplete_theories; //!< theories that failed to produce a model
         bool               m_searching;
+        bool               m_propagating;
         unsigned           m_num_conflicts;
         unsigned           m_num_conflicts_since_restart;
         unsigned           m_num_conflicts_since_lemma_gc;

src/smt/smt_model_generator.cpp

@@ -427,15 +427,9 @@ namespace smt {
                       }
                       tout << "\n";
                       tout << "value: #" << n->get_owner_id() << "\n" << mk_ismt2_pp(result, m_manager) << "\n";);
-                if (m_context->get_last_search_failure() == smt::THEORY) {
-                    // if the theory solvers are incomplete, then we cannot assume the e-graph is close under congruence
                 if (fi->get_entry(args.c_ptr()) == nullptr)
                     fi->insert_new_entry(args.c_ptr(), result);
             }
-                else {
-                    fi->insert_new_entry(args.c_ptr(), result);
-                }
-            }
         }
     }
 

src/util/trace.cpp

@@ -20,6 +20,7 @@ Revision History:
 #include "util/str_hashtable.h"
 
 #ifdef _TRACE
+
 std::ofstream tout(".z3-trace"); 
 
 static bool g_enable_all_trace_tags = false;