Merge remote-tracking branch 'upstream/master' into regex-develop

src/smt/smt_context.cpp

@@ -3951,7 +3951,7 @@ namespace smt {
 #if 0
             {
                 static unsigned counter = 0;
-                static uint64 total = 0;
+                static uint64_t total = 0;
                 static unsigned max = 0;
                 counter++;
                 total += num_lits;

src/smt/smt_enode.h

@@ -216,6 +216,15 @@ namespace smt {
             return m_args;
         }
 
+        class args {
+            enode const& n;
+        public:
+            args(enode const& n):n(n) {}
+            args(enode const* n):n(*n) {}
+            enode_vector::const_iterator begin() const { return n.get_args(); }
+            enode_vector::const_iterator end() const { return n.get_args() + n.get_num_args(); }
+        };
+
         // unsigned get_id() const { 
         //    return m_id; 
         // }
@@ -285,6 +294,16 @@ namespace smt {
             return m_commutative;
         }
 
+        class parents {
+            enode const& n;
+        public:
+            parents(enode const& _n):n(_n) {}
+            parents(enode const* _n):n(*_n) {}
+            enode_vector::const_iterator begin() const { return n.begin_parents(); }
+            enode_vector::const_iterator end() const { return n.end_parents(); }
+        };
+
+
         unsigned get_num_parents() const {
             return m_parents.size();
         }

src/smt/smt_types.h

@@ -21,6 +21,7 @@ Revision History:
 
 #include "util/list.h"
 #include "util/vector.h"
+#include "util/hashtable.h"
 #include "util/lbool.h"
 
 class model;

src/smt/theory_datatype.cpp

@@ -36,6 +36,41 @@ namespace smt {
         theory_id get_from_theory() const override { return null_theory_id; }
     };
 
+    theory_datatype::final_check_st::final_check_st(theory_datatype * th) : th(th) {
+        SASSERT(th->m_to_unmark.empty());
+        SASSERT(th->m_to_unmark2.empty());
+        th->m_used_eqs.reset();
+        th->m_stack.reset();
+        th->m_parent.reset();
+    }
+
+    theory_datatype::final_check_st::~final_check_st() {
+        unmark_enodes(th->m_to_unmark.size(), th->m_to_unmark.c_ptr());
+        unmark_enodes2(th->m_to_unmark2.size(), th->m_to_unmark2.c_ptr());
+        th->m_to_unmark.reset();
+        th->m_to_unmark2.reset();
+        th->m_used_eqs.reset();
+        th->m_stack.reset();
+        th->m_parent.reset();
+    }   
+    
+    void theory_datatype::oc_mark_on_stack(enode * n) {
+        n = n->get_root();
+        n->set_mark();
+        m_to_unmark.push_back(n); 
+    }
+
+    void theory_datatype::oc_mark_cycle_free(enode * n) {
+        n = n->get_root();
+        n->set_mark2();
+        m_to_unmark2.push_back(n); 
+    }
+
+    void theory_datatype::oc_push_stack(enode * n) {
+        m_stack.push_back(std::make_pair(EXIT, n));
+        m_stack.push_back(std::make_pair(ENTER, n));
+    }
+
 
     theory* theory_datatype::mk_fresh(context* new_ctx) { 
         return alloc(theory_datatype, new_ctx->get_manager(), m_params); 
@@ -389,10 +424,11 @@ namespace smt {
     final_check_status theory_datatype::final_check_eh() {
         int num_vars = get_num_vars();
         final_check_status r = FC_DONE;
+        final_check_st _guard(this); // RAII for managing state
         for (int v = 0; v < num_vars; v++) {
             if (v == static_cast<int>(m_find.find(v))) {
                 enode * node = get_enode(v);
-                if (occurs_check(node)) {
+                if (!oc_cycle_free(node) && occurs_check(node)) {
                     // conflict was detected... 
                     // return...
                     return FC_CONTINUE;
@@ -410,6 +446,73 @@ namespace smt {
         return r;
     }
 
+    // Assuming `app` is equal to a constructor term, return the constructor enode
+    inline enode * theory_datatype::oc_get_cstor(enode * app) {
+        theory_var v = app->get_root()->get_th_var(get_id());
+        SASSERT(v != null_theory_var);
+        v = m_find.find(v);
+        var_data * d = m_var_data[v];
+        SASSERT(d->m_constructor);
+        return d->m_constructor;
+    }
+
+    // explain the cycle root -> ... -> app -> root
+    void theory_datatype::occurs_check_explain(enode * app, enode * root) {
+        TRACE("datatype", tout << "occurs_check_explain " << mk_bounded_pp(app->get_owner(), get_manager()) << " <-> " << mk_bounded_pp(root->get_owner(), get_manager()) << "\n";);
+        enode* app_parent = nullptr;
+
+        // first: explain that root=v, given that app=cstor(…,v,…)
+        for (enode * arg : enode::args(oc_get_cstor(app))) {
+            // found an argument which is equal to root
+            if (arg->get_root() == root->get_root()) {
+                if (arg != root)
+                    m_used_eqs.push_back(enode_pair(arg, root));
+                break;
+            }
+        }
+
+        // now explain app=cstor(..,v,..) where v=root, and recurse with parent of app
+        while (app->get_root() != root->get_root()) {
+            enode * app_cstor = oc_get_cstor(app);
+            if (app != app_cstor)
+                m_used_eqs.push_back(enode_pair(app, app_cstor));
+            app_parent = m_parent[app->get_root()];
+            app = app_parent;
+        }
+        
+        SASSERT(app->get_root() == root->get_root());
+        if (app != root)
+            m_used_eqs.push_back(enode_pair(app, root));
+    }
+
+    // start exploring subgraph below `app`
+    bool theory_datatype::occurs_check_enter(enode * app) {
+        oc_mark_on_stack(app);
+        theory_var v = app->get_root()->get_th_var(get_id());
+        if (v != null_theory_var) {
+            v = m_find.find(v);
+            var_data * d = m_var_data[v];
+            if (d->m_constructor) {
+                for (enode * arg : enode::args(d->m_constructor)) {
+                    if (oc_cycle_free(arg)) {
+                        continue;
+                    }
+                    if (oc_on_stack(arg)) {
+                        // arg was explored before app, and is still on the stack: cycle
+                        occurs_check_explain(app, arg);
+                        return true;
+                    }
+                    // explore `arg` (with parent `app`)
+                    if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) {
+                        m_parent.insert(arg->get_root(), app);
+                        oc_push_stack(arg);
+                    }
+                }
+            }
+        }
+        return false;
+    }
+
     /**
        \brief Check if n can be reached starting from n and following equalities and constructors.
        For example, occur_check(a1) returns true in the following set of equalities:
@@ -418,17 +521,39 @@ namespace smt {
        a3 = cons(v3, a1)
     */
     bool theory_datatype::occurs_check(enode * n) {
-        TRACE("datatype", tout << "occurs check: #" << n->get_owner_id() << "\n";);
-        m_to_unmark.reset();
-        m_used_eqs.reset();
-        m_main   = n;
-        bool res = occurs_check_core(m_main);
-        unmark_enodes(m_to_unmark.size(), m_to_unmark.c_ptr());
+        TRACE("datatype", tout << "occurs check: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), get_manager()) << "\n";);
+        m_stats.m_occurs_check++;
+
+        bool res = false;
+        oc_push_stack(n);
+
+        // DFS traversal from `n`. Look at top element and explore it.
+        while (!res && !m_stack.empty()) {
+            stack_op op = m_stack.back().first;
+            enode * app = m_stack.back().second;
+            m_stack.pop_back();
+
+            if (oc_cycle_free(app)) continue;
+
+            TRACE("datatype", tout << "occurs check loop: #" << app->get_owner_id() << " " << mk_bounded_pp(app->get_owner(), get_manager()) << (op==ENTER?" enter":" exit")<< "\n";);
+
+            switch (op) {
+            case ENTER:
+              res = occurs_check_enter(app);
+              break;
+
+            case EXIT:
+              oc_mark_cycle_free(app);
+              break;
+            }
+        }
+
         if (res) {
+            // m_used_eqs should contain conflict
             context & ctx = get_context();
             region & r    = ctx.get_region();
             ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, m_used_eqs.size(), m_used_eqs.c_ptr())));
-            TRACE("occurs_check",
+            TRACE("datatype",
                   tout << "occurs_check: true\n";
                   for (enode_pair const& p : m_used_eqs) {
                       tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n";
@@ -437,48 +562,6 @@ namespace smt {
         }
         return res;
     }
-
-    /**
-       \brief Auxiliary method for occurs_check.
-       TODO: improve performance.
-    */
-    bool theory_datatype::occurs_check_core(enode * app) {
-        if (app->is_marked())
-            return false;
-        
-        m_stats.m_occurs_check++;
-        app->set_mark();
-        m_to_unmark.push_back(app);
-        
-        TRACE("datatype", tout << "occurs check_core: #" << app->get_owner_id() << " #" << m_main->get_owner_id() << "\n";);
-
-        theory_var v = app->get_root()->get_th_var(get_id());
-        if (v != null_theory_var) {
-            v = m_find.find(v);
-            var_data * d = m_var_data[v];
-            if (d->m_constructor) {
-                if (app != d->m_constructor)
-                    m_used_eqs.push_back(enode_pair(app, d->m_constructor));
-                unsigned num_args = d->m_constructor->get_num_args();
-                for (unsigned i = 0; i < num_args; i++) {
-                    enode * arg = d->m_constructor->get_arg(i);
-                    if (arg->get_root() == m_main->get_root()) {
-                        if (arg != m_main)
-                            m_used_eqs.push_back(enode_pair(arg, m_main));
-                        return true;
-                    }
-                    if (m_util.is_datatype(get_manager().get_sort(arg->get_owner())) && occurs_check_core(arg))
-                        return true;
-                }
-                if (app != d->m_constructor) {
-                    SASSERT(m_used_eqs.back().first  == app);
-                    SASSERT(m_used_eqs.back().second == d->m_constructor);
-                    m_used_eqs.pop_back();
-                }
-            }
-        }
-        return false;
-    }
         
     void theory_datatype::reset_eh() {
         m_trail_stack.reset();

src/smt/theory_datatype.h

@@ -26,7 +26,6 @@ Revision History:
 #include "smt/proto_model/datatype_factory.h"
 
 namespace smt {
-    
     class theory_datatype : public theory {
         typedef trail_stack<theory_datatype> th_trail_stack;
         typedef union_find<theory_datatype>  th_union_find;
@@ -73,11 +72,36 @@ namespace smt {
         void propagate_recognizer(theory_var v, enode * r);
         void sign_recognizer_conflict(enode * c, enode * r);
 
-        ptr_vector<enode>    m_to_unmark;
-        enode_pair_vector    m_used_eqs;
-        enode *              m_main;
+        typedef enum { ENTER, EXIT } stack_op;
+        typedef map<enode*, enode*, obj_ptr_hash<enode>, ptr_eq<enode> > parent_tbl;
+        typedef std::pair<stack_op, enode*> stack_entry;
+
+        ptr_vector<enode>     m_to_unmark;
+        ptr_vector<enode>     m_to_unmark2;
+        enode_pair_vector     m_used_eqs; // conflict, if any
+        parent_tbl            m_parent; // parent explanation for occurs_check
+        svector<stack_entry>  m_stack; // stack for DFS for occurs_check
+
+        void oc_mark_on_stack(enode * n);
+        bool oc_on_stack(enode * n) const { return n->get_root()->is_marked(); }
+
+        void oc_mark_cycle_free(enode * n);
+        bool oc_cycle_free(enode * n) const { return n->get_root()->is_marked2(); }
+
+        void oc_push_stack(enode * n);
+
+        // class for managing state of final_check
+        class final_check_st {
+            theory_datatype * th;
+        public:
+            final_check_st(theory_datatype * th);
+            ~final_check_st();
+        };
+
+        enode * oc_get_cstor(enode * n);
         bool occurs_check(enode * n);
-        bool occurs_check_core(enode * n);
+        bool occurs_check_enter(enode * n);
+        void occurs_check_explain(enode * top, enode * root);
 
         void mk_split(theory_var v);
 

src/smt/theory_dl.cpp

@@ -182,7 +182,7 @@ namespace smt {
                 
                 if (n->get_decl() != v) {
                     expr* rep = m().mk_app(r, n);
-                    uint64 vl;
+                    uint64_t vl;
                     if (u().is_numeral_ext(n, vl)) {
                         assert_cnstr(m().mk_eq(rep, mk_bv_constant(vl, s)));
                     }
@@ -237,12 +237,12 @@ namespace smt {
             return true;
         }
 
-        app* mk_bv_constant(uint64 val, sort* s) {
+        app* mk_bv_constant(uint64_t val, sort* s) {
             return b().mk_numeral(rational(val, rational::ui64()), 64);
         }
 
         app* max_value(sort* s) {
-            uint64 sz;
+            uint64_t sz;
             VERIFY(u().try_get_size(s, sz));
             SASSERT(sz > 0);
             return mk_bv_constant(sz-1, s);

src/smt/theory_pb.cpp

@@ -446,7 +446,16 @@ namespace smt {
             expr* arg = atom->get_arg(i);
             literal l = compile_arg(arg);
             numeral c = m_util.get_coeff(atom, i);
-            args.push_back(std::make_pair(l, c));
+            switch (ctx.get_assignment(l)) {
+            case l_true: 
+                k -= c;
+                break;
+            case l_false:
+                break;
+            default:
+                args.push_back(std::make_pair(l, c));
+                break;
+            }
         }
         if (m_util.is_at_most_k(atom) || m_util.is_le(atom)) {
             // turn W <= k into -W >= -k
@@ -458,7 +467,7 @@ namespace smt {
         else {
             SASSERT(m_util.is_at_least_k(atom) || m_util.is_ge(atom) || m_util.is_eq(atom));
         }
-        TRACE("pb", display(tout, *c););        
+        TRACE("pb", display(tout, *c, true););        
         //app_ref fml1(m), fml2(m);
         //fml1 = c->to_expr(ctx, m);
         c->unique();