fixing #4670 (#4682)

* fixing #4670 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * init Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * arrays Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * arrays Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * arrays Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Sep 10, 2020 · cfa7c73 · cfa7c73
1 parent ee00542
commit cfa7c73
Show file tree

Hide file tree

Showing 48 changed files with 1,591 additions and 359 deletions.
diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
@@ -161,6 +161,8 @@ class array_recognizers {
     bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
     bool is_set_has_size(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_HAS_SIZE); }
     bool is_set_card(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_CARD); }
+    bool is_default(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_DEFAULT); }
+    bool is_default(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_DEFAULT); }
     bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); }
     func_decl * get_as_array_func_decl(expr * n) const;
     func_decl * get_as_array_func_decl(func_decl* f) const;
@@ -199,6 +201,10 @@ class array_util : public array_recognizers {
         return mk_select(args.size(), args.c_ptr());
     }
 
+    app * mk_select(ptr_buffer<expr> const& args) {
+        return mk_select(args.size(), args.c_ptr());
+    }
+
     app * mk_select(expr_ref_vector const& args) {
         return mk_select(args.size(), args.c_ptr());
     }

diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
@@ -53,7 +53,7 @@ namespace datatype {
         symbol    m_name;
         sort_ref  m_range;
         unsigned m_index;    // reference to recursive data-type may only get resolved after all mutually recursive data-types are procssed.
-        constructor* m_constructor;
+        constructor* m_constructor{ nullptr };
     public:
         accessor(ast_manager& m, symbol const& n, sort* range):
             m_name(n),

diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
@@ -71,7 +71,7 @@ namespace euf {
     }
 
     bool egraph::is_equality(enode* p) const {
-        return m.is_eq(p->get_owner());
+        return m.is_eq(p->get_expr());
     }
 
     void egraph::force_push() {
@@ -112,7 +112,7 @@ namespace euf {
             update_children(n);
         }
         else {
-            SASSERT(r->get_owner() != n->get_owner());
+            SASSERT(r->get_expr() != n->get_expr());
             merge_justification(n, r, justification::congruence(p.second));
             std::swap(n->m_next, r->m_next);
             n->m_root = r;
@@ -191,7 +191,7 @@ namespace euf {
         auto undo_node = [&](enode* n) {
             if (n->num_args() > 1)
                 m_table.erase(n);
-            m_expr2enode[n->get_owner_id()] = nullptr;
+            m_expr2enode[n->get_expr_id()] = nullptr;
             n->~enode();
             m_nodes.pop_back();
             m_exprs.pop_back();
@@ -243,8 +243,8 @@ namespace euf {
     }
 
     void egraph::merge(enode* n1, enode* n2, justification j) {
-        SASSERT(m.get_sort(n1->get_owner()) == m.get_sort(n2->get_owner()));
-        TRACE("euf", tout << n1->get_owner_id() << " == " << n2->get_owner_id() << "\n";);
+        SASSERT(m.get_sort(n1->get_expr()) == m.get_sort(n2->get_expr()));
+        TRACE("euf", tout << n1->get_expr_id() << " == " << n2->get_expr_id() << "\n";);
         force_push();
         enode* r1 = n1->get_root();
         enode* r2 = n2->get_root();
@@ -259,7 +259,7 @@ namespace euf {
             std::swap(r1, r2);
             std::swap(n1, n2);
         }
-        if ((m.is_true(r2->get_owner()) || m.is_false(r2->get_owner())) && j.is_congruence()) {
+        if ((m.is_true(r2->get_expr()) || m.is_false(r2->get_expr())) && j.is_congruence()) {
             add_literal(n1, false);
         }
         for (enode* p : enode_parents(n1)) 
@@ -357,10 +357,10 @@ namespace euf {
        explanations up to the least common ancestors.
      */
     void egraph::push_congruence(enode* n1, enode* n2, bool comm) {
-        SASSERT(is_app(n1->get_owner()));
+        SASSERT(is_app(n1->get_expr()));
         SASSERT(n1->get_decl() == n2->get_decl());
         if (m_used_cc) 
-            m_used_cc(to_app(n1->get_owner()), to_app(n2->get_owner()));
+            m_used_cc(to_app(n1->get_expr()), to_app(n2->get_expr()));
         if (comm && 
             n1->get_arg(0)->get_root() == n2->get_arg(1)->get_root() &&
             n1->get_arg(1)->get_root() == n2->get_arg(0)->get_root()) {
@@ -428,7 +428,7 @@ namespace euf {
         push_to_lca(a, lca);
         push_to_lca(b, lca);
         if (m_used_eq)
-            m_used_eq(a->get_owner(), b->get_owner(), lca->get_owner());
+            m_used_eq(a->get_expr(), b->get_expr(), lca->get_expr());
         explain_todo(justifications);
     }
 
@@ -449,10 +449,10 @@ namespace euf {
     }
 
     std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
-        out << n->get_owner_id() << " := ";
+        out << n->get_expr_id() << " := ";
         if (!n->is_root()) 
-            out << "[" << n->get_root()->get_owner_id() << "] ";
-        expr* f = n->get_owner();
+            out << "[" << n->get_root()->get_expr_id() << "] ";
+        expr* f = n->get_expr();
         if (is_app(f))
             out << mk_bounded_pp(f, m, 1);
         else if (is_quantifier(f))
@@ -463,7 +463,7 @@ namespace euf {
         if (!n->m_parents.empty()) {
             out << "    ";
             for (enode* p : enode_parents(n))
-                out << p->get_owner_id() << " ";
+                out << p->get_expr_id() << " ";
             out << "\n";
         }
         if (n->has_th_vars()) {
@@ -505,7 +505,7 @@ namespace euf {
             SASSERT(!n1->has_th_vars());
             args.reset();
             for (unsigned j = 0; j < n1->num_args(); ++j) 
-                args.push_back(old_expr2new_enode[n1->get_arg(j)->get_owner_id()]);
+                args.push_back(old_expr2new_enode[n1->get_arg(j)->get_expr_id()]);
             expr*  e2 = tr(e1);
             enode* n2 = mk(e2, args.size(), args.c_ptr());
             old_expr2new_enode.setx(e1->get_id(), n2, nullptr);
@@ -514,10 +514,10 @@ namespace euf {
             enode* n1 = src.m_nodes[i];
             enode* n1t = n1->m_target;      
             enode* n2 = m_nodes[i];
-            enode* n2t = n1t ? old_expr2new_enode[n1->get_owner_id()] : nullptr;
+            enode* n2t = n1t ? old_expr2new_enode[n1->get_expr_id()] : nullptr;
             SASSERT(!n1t || n2t);
-            SASSERT(!n1t || src.m.get_sort(n1->get_owner()) == src.m.get_sort(n1t->get_owner()));
-            SASSERT(!n1t || m.get_sort(n2->get_owner()) == m.get_sort(n2t->get_owner()));
+            SASSERT(!n1t || src.m.get_sort(n1->get_expr()) == src.m.get_sort(n1t->get_expr()));
+            SASSERT(!n1t || m.get_sort(n2->get_expr()) == m.get_sort(n2t->get_expr()));
             if (n1t && n2->get_root() != n2t->get_root()) 
                 merge(n2, n2t, n1->m_justification.copy(copy_justification));
         }

diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
@@ -68,7 +68,7 @@ namespace euf {
             struct new_th_eq_qhead {};
             struct new_lits_qhead {};
             struct inconsistent {};
-            enum tag_t { is_set_parent, is_add_node, is_toggle_merge, 
+            enum class tag_t { is_set_parent, is_add_node, is_toggle_merge, 
                          is_add_th_var, is_replace_th_var, is_new_lit, is_new_th_eq,
                          is_new_th_eq_qhead, is_new_lits_qhead, is_inconsistent };
             tag_t  tag;

diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h
@@ -36,7 +36,7 @@ namespace euf {
     const theory_id null_theory_id = -1;
 
     class enode {
-        expr*         m_owner{ nullptr };
+        expr*         m_expr{ nullptr };
         bool          m_mark1 { false };
         bool          m_mark2 { false };
         bool          m_commutative { false };
@@ -69,14 +69,14 @@ namespace euf {
             SASSERT(num_args <= (is_app(f) ? to_app(f)->get_num_args() : 0));
             void* mem = r.allocate(get_enode_size(num_args));
             enode* n = new (mem) enode();
-            n->m_owner = f;
+            n->m_expr = f;
             n->m_next = n;
             n->m_root = n;
             n->m_commutative = num_args == 2 && is_app(f) && to_app(f)->get_decl()->is_commutative();
             n->m_num_args = num_args;
             n->m_merge_enabled = true;
             for (unsigned i = 0; i < num_args; ++i) {
-                SASSERT(to_app(f)->get_arg(i) == args[i]->get_owner());
+                SASSERT(to_app(f)->get_arg(i) == args[i]->get_expr());
                 n->m_args[i] = args[i];
             }
             return n;
@@ -112,8 +112,7 @@ namespace euf {
         bool merge_enabled() { return m_merge_enabled; }
 
         enode* get_arg(unsigned i) const { SASSERT(i < num_args()); return m_args[i]; }        
-        unsigned hash() const { return m_owner->hash(); }
-        func_decl* get_decl() const { return is_app(m_owner) ? to_app(m_owner)->get_decl() : nullptr; } 
+        unsigned hash() const { return m_expr->hash(); }
         unsigned get_table_id() const { return m_table_id; }
         void     set_table_id(unsigned t) { m_table_id = t; }
 
@@ -143,9 +142,11 @@ namespace euf {
         unsigned class_size() const { return m_class_size; }
         bool is_root() const { return m_root == this; }
         enode* get_root() const { return m_root; }
-        expr*  get_owner() const { return m_owner; }
-        unsigned get_owner_id() const { return m_owner->get_id(); }
-        unsigned get_root_id() const { return m_root->m_owner->get_id(); }
+        expr*  get_expr() const { return m_expr; }
+        app*  get_app() const { return to_app(m_expr); }
+        func_decl* get_decl() const { return is_app(m_expr) ? to_app(m_expr)->get_decl() : nullptr; }
+        unsigned get_expr_id() const { return m_expr->get_id(); }
+        unsigned get_root_id() const { return m_root->m_expr->get_id(); }
         theory_var get_th_var(theory_id id) const { return m_th_vars.find(id); }
         bool is_attached_to(theory_id id) const { return get_th_var(id) != null_theory_var; }
         bool has_th_vars() const { return !m_th_vars.empty(); }
@@ -201,14 +202,15 @@ namespace euf {
         iterator end() const { return iterator(&n, &n); }
     };
 
+
     class enode_th_vars {
         enode& n;
     public:
         class iterator {
             th_var_list* m_th_vars;
         public:
             iterator(th_var_list* n) : m_th_vars(n) {}
-            th_var_list operator*() { return *m_th_vars; }
+            th_var_list const& operator*() { return *m_th_vars; }
             iterator& operator++() { m_th_vars = m_th_vars->get_next(); return *this; }
             iterator operator++(int) { iterator tmp = *this; ++* this; return tmp; }
             bool operator==(iterator const& other) const { return m_th_vars == other.m_th_vars; }

diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp
@@ -169,7 +169,7 @@ namespace euf {
         binary_table* tb = UNTAG(binary_table*, t);
         out << "b ";
         for (enode* n : *tb) {
-            out << n->get_owner_id() << " ";
+            out << n->get_expr_id() << " ";
         }
         out << "\n";
     }
@@ -178,7 +178,7 @@ namespace euf {
         comm_table* tb = UNTAG(comm_table*, t);
         out << "bc ";
         for (enode* n : *tb) {
-            out << n->get_owner_id() << " ";
+            out << n->get_expr_id() << " ";
         }
         out << "\n";
     }
@@ -187,7 +187,7 @@ namespace euf {
         unary_table* tb = UNTAG(unary_table*, t);
         out << "un ";
         for (enode* n : *tb) {
-            out << n->get_owner_id() << " ";
+            out << n->get_expr_id() << " ";
         }
         out << "\n";
     }
@@ -196,7 +196,7 @@ namespace euf {
         table* tb = UNTAG(table*, t);
         out << "nary ";
         for (enode* n : *tb) {
-            out << n->get_owner_id() << " ";
+            out << n->get_expr_id() << " ";
         }
         out << "\n";
     }
@@ -205,8 +205,8 @@ namespace euf {
     enode_bool_pair etable::insert(enode * n) {
         // it doesn't make sense to insert a constant.
         SASSERT(n->num_args() > 0);
-        SASSERT(!m_manager.is_and(n->get_owner()));
-        SASSERT(!m_manager.is_or(n->get_owner()));
+        SASSERT(!m_manager.is_and(n->get_expr()));
+        SASSERT(!m_manager.is_or(n->get_expr()));
         enode * n_prime;
         void * t = get_table(n); 
         switch (static_cast<table_kind>(GET_TAG(t))) {
@@ -215,7 +215,7 @@ namespace euf {
             return enode_bool_pair(n_prime, false);
         case BINARY:
             n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n);
-            TRACE("euf", tout << "insert: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " inserted: " << (n == n_prime) << " " << n_prime->get_owner_id() << "\n";
+            TRACE("euf", tout << "insert: " << n->get_expr_id() << " " << cg_binary_hash()(n) << " inserted: " << (n == n_prime) << " " << n_prime->get_expr_id() << "\n";
                   display_binary(tout, t); tout << "contains_ptr: " << contains_ptr(n) << "\n";); 
             return enode_bool_pair(n_prime, false);
         case BINARY_COMM:
@@ -236,7 +236,7 @@ namespace euf {
             UNTAG(unary_table*, t)->erase(n);
             break;
         case BINARY:
-            TRACE("euf", tout << "erase: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " contains: " << contains_ptr(n) << "\n";);
+            TRACE("euf", tout << "erase: " << n->get_expr_id() << " " << cg_binary_hash()(n) << " contains: " << contains_ptr(n) << "\n";);
             UNTAG(binary_table*, t)->erase(n);
             break;
         case BINARY_COMM:

diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h
@@ -150,9 +150,9 @@ class var_shifter_core : public rewriter_core {
        - (VAR i + s2) if i < b 
 */
 class var_shifter : public var_shifter_core {
-    unsigned  m_bound;
-    unsigned  m_shift1;
-    unsigned  m_shift2;
+    unsigned  m_bound  { 0 };
+    unsigned  m_shift1 { 0 };
+    unsigned  m_shift2 { 0 };
     void process_var(var * v) override;
 public:
     var_shifter(ast_manager & m):var_shifter_core(m) {}

diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp
@@ -453,10 +453,8 @@ namespace datalog {
         }
 
         void display(std::ostream& out) const {
-            u_map<ddnf_mgr*>::iterator it = m_mgrs.begin(), end = m_mgrs.end();
-            for (; it != end; ++it) {
-                it->m_value->display(out);
-            }
+            for (auto const& kv : m_mgrs)
+                kv.m_value->display(out);
         }
 
     private:
@@ -558,13 +556,9 @@ namespace datalog {
             m_todo.reset();
             m_cache.reset();
             m_expr2tbv.reset();
-            datalog::rule_set::iterator it  = rules.begin();
-            datalog::rule_set::iterator end = rules.end();
-            for (; it != end; ++it) {
-                if (!pre_process_rule(**it)) {
+            for (auto* r : rules) 
+                if (!pre_process_rule(*r)) 
                     return false;
-                }
-            }
             return true;
         }
 

diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
@@ -176,6 +176,7 @@ tbv* tbv_manager::allocate(rational const& r) {
     return v;
 }
 void tbv_manager::deallocate(tbv* bv) {
+#if 0
     DEBUG_CODE(
         if (!allocated_tbvs.contains(bv)) {
             std::cout << "double deallocate: " << bv << "\n";
@@ -185,6 +186,7 @@ void tbv_manager::deallocate(tbv* bv) {
             TRACE("doc", tout << "deallocate: " << bv << "\n";);
         }
         allocated_tbvs.erase(bv););
+#endif
     m.deallocate(bv);
 }    
 void tbv_manager::copy(tbv& dst, tbv const& src) const {

diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h
@@ -102,6 +102,9 @@ class tbv: private fixed_bit_vector {
         bool operator()(tbv const& d1, tbv const& d2) const {
             return m.equals(d1, d2);
         }
+        bool operator()(tbv const* d1, tbv const* d2) const {
+            return m.equals(*d1, *d2);
+        }
     };
 
     struct hash {
@@ -110,6 +113,9 @@ class tbv: private fixed_bit_vector {
         unsigned operator()(tbv const& d) const {
             return m.hash(d);
         }
+        unsigned operator()(tbv const* d) const {
+            return m.hash(*d);
+        }
     };
 
 

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
@@ -387,6 +387,7 @@ namespace opt {
 
     void context::get_model_core(model_ref& mdl) {
         mdl = m_model;
+        CTRACE("opt", mdl, tout << *mdl;);
         fix_model(mdl);
         if (mdl) mdl->set_model_completion(true);
         CTRACE("opt", mdl, tout << *mdl;);