add context::internalize() API that takes multiple expressions at once (#4488)

src/smt/smt_context.h

@@ -741,7 +741,12 @@ namespace smt {
 
         bool should_internalize_rec(expr* e) const;
 
-        void top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs);
+        void top_sort_expr(expr* const* exprs, unsigned num_exprs, svector<expr_bool_pair> & sorted_exprs);
+
+        void internalize_rec(expr * n, bool gate_ctx);
+
+        void internalize_deep(expr * n);
+        void internalize_deep(expr* const* n, unsigned num_exprs);
 
         void assert_default(expr * n, proof * pr);
 
@@ -868,6 +873,7 @@ namespace smt {
         void ensure_internalized(expr* e);
 
         void internalize(expr * n, bool gate_ctx);
+        void internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx);
 
         void internalize(expr * n, bool gate_ctx, unsigned generation);
 
@@ -906,10 +912,6 @@ namespace smt {
 
     public:
 
-        void internalize_rec(expr * n, bool gate_ctx);
-
-        void internalize_deep(expr * n);
-
         // helper function for trail
         void undo_th_case_split(literal l);
 

src/smt/smt_internalizer.cpp

@@ -152,11 +152,9 @@ namespace smt {
         return visited;
     }
 
-    void context::top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs) {
+    void context::top_sort_expr(expr* const* exprs, unsigned num_exprs, svector<expr_bool_pair> & sorted_exprs) {
-        ts_todo.reset();
         tcolors.reset();
         fcolors.reset();
-        ts_todo.push_back(expr_bool_pair(n, true));
         while (!ts_todo.empty()) {
             expr_bool_pair & p = ts_todo.back();
             expr * curr        = p.first;
@@ -166,12 +164,14 @@ namespace smt {
                 set_color(tcolors, fcolors, curr, gate_ctx, Grey);
                 ts_visit_children(curr, gate_ctx, ts_todo);
                 break;
-            case Grey:
+            case Grey: {
                 SASSERT(ts_visit_children(curr, gate_ctx, ts_todo));
                 set_color(tcolors, fcolors, curr, gate_ctx, Black);
-                if (n != curr && !m.is_not(curr))
+                auto end = exprs + num_exprs;
+                if (std::find(exprs, end, curr) == end && !m.is_not(curr) && should_internalize_rec(curr))
                     sorted_exprs.push_back(expr_bool_pair(curr, gate_ctx));
                 break;
+            }
             case Black:
                 ts_todo.pop_back();
                 break;
@@ -189,23 +189,33 @@ namespace smt {
             to_app(e)->get_family_id() == null_family_id || 
             to_app(e)->get_family_id() == m.get_basic_family_id();
     }
-            
+
-    void context::internalize_deep(expr* n) {
+    void context::internalize_deep(expr* const* exprs, unsigned num_exprs) {
-        if (!e_internalized(n) && ::get_depth(n) > DEEP_EXPR_THRESHOLD && should_internalize_rec(n)) {
+        ts_todo.reset();
-            // if the expression is deep, then execute topological sort to avoid
+        for (unsigned i = 0; i < num_exprs; ++i) {
-            // stack overflow.
+            expr * n = exprs[i];
-            // a caveat is that theory internalizers do rely on recursive descent so
+            if (!e_internalized(n) && ::get_depth(n) > DEEP_EXPR_THRESHOLD && should_internalize_rec(n)) {
-            // internalization over these follows top-down
+                // if the expression is deep, then execute topological sort to avoid
-            TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m););
+                // stack overflow.
-            svector<expr_bool_pair> sorted_exprs;
+                // a caveat is that theory internalizers do rely on recursive descent so
-            top_sort_expr(n, sorted_exprs);
+                // internalization over these follows top-down
-            TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; );
+                TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m););
-            for (auto & kv : sorted_exprs) {
+                ts_todo.push_back(expr_bool_pair(n, true));
-                expr* e = kv.first;
-                if (should_internalize_rec(e)) 
-                    internalize_rec(e, kv.second);
             }
         }
+
+        svector<expr_bool_pair> sorted_exprs;
+        top_sort_expr(exprs, num_exprs, sorted_exprs);
+        TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; );
+        for (auto & kv : sorted_exprs) {
+            expr* e = kv.first;
+            SASSERT(should_internalize_rec(e));
+            internalize_rec(e, kv.second);
+        }
+    }
+    void context::internalize_deep(expr* n) {
+        expr * v[1] = { n };
+        internalize_deep(v, 1);
     }
  
     /**
@@ -343,6 +353,13 @@ namespace smt {
         internalize_rec(n, gate_ctx);
     }
 
+    void context::internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx) {
+        internalize_deep(exprs, num_exprs);
+        for (unsigned i = 0; i < num_exprs; ++i) {
+            internalize_rec(exprs[i], gate_ctx);
+        }
+    }
+
     void context::internalize_rec(expr * n, bool gate_ctx) {
         TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m) << "\n";);
         TRACE("internalize_bug", tout << "internalizing:\n" << mk_bounded_pp(n, m) << "\n";);

src/smt/theory_array_full.cpp

@@ -398,7 +398,7 @@ namespace smt {
         if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n)){
             return;
         }
-        if (!ctx.e_internalized(n)) ctx.internalize(n, false);;
+        ctx.ensure_internalized(n);
         enode* node = ctx.get_enode(n);
         if (is_select(n)) {
             enode * arg = ctx.get_enode(n->get_arg(0));

src/smt/theory_bv.cpp

@@ -23,6 +23,7 @@ Revision History:
 #include "ast/bv_decl_plugin.h"
 #include "smt/smt_model_generator.h"
 #include "util/stats.h"
+#include "util/vector.h"
 
 #define WATCH_DISEQ 0
 
@@ -142,9 +143,7 @@ namespace smt {
     }
 
     void theory_bv::process_args(app * n) {
-        for (expr* arg : *n) {
+        ctx.internalize(n->get_args(), n->get_num_args(), false);
-            ctx.internalize(arg, false);
-        }
     }
 
     enode * theory_bv::mk_enode(app * n) {
@@ -312,13 +311,16 @@ namespace smt {
         unsigned sz             = bits.size();
         SASSERT(get_bv_size(n) == sz);
         m_bits[v].reset();
+
+        ptr_vector<expr> bits_exprs;
+        for (unsigned i = 0; i < sz; ++i)
+            bits_exprs.push_back(bits.get(i));
+        ctx.internalize(bits_exprs.c_ptr(), sz, true);
+
         for (unsigned i = 0; i < sz; i++) {
             expr * bit          = bits.get(i);
-            expr_ref s_bit(m);
+            literal l           = ctx.get_literal(bit);
-            simplify_bit(bit, s_bit);
+            TRACE("init_bits", tout << "bit " << i << " of #" << n->get_owner_id() << "\n" << mk_ll_pp(bit, m) << "\n";);
-            ctx.internalize(s_bit, true);
-            literal l           = ctx.get_literal(s_bit.get());
-            TRACE("init_bits", tout << "bit " << i << " of #" << n->get_owner_id() << "\n" << mk_ll_pp(s_bit, m) << "\n";);
             add_bit(v, l);
         }
         find_wpos(v);
@@ -983,9 +985,7 @@ namespace smt {
     }
 
     bool theory_bv::internalize_carry(app * n, bool gate_ctx) {
-        ctx.internalize(n->get_arg(0), true);
+        ctx.internalize(n->get_args(), 3, true);
-        ctx.internalize(n->get_arg(1), true);
-        ctx.internalize(n->get_arg(2), true);
         bool is_new_var = false;
         bool_var v;
         if (!ctx.b_internalized(n)) {
@@ -1016,9 +1016,7 @@ namespace smt {
     }
 
     bool theory_bv::internalize_xor3(app * n, bool gate_ctx) {
-        ctx.internalize(n->get_arg(0), true);
+        ctx.internalize(n->get_args(), 3, true);
-        ctx.internalize(n->get_arg(1), true);
-        ctx.internalize(n->get_arg(2), true);
         bool is_new_var = false;
         bool_var v;
         if (!ctx.b_internalized(n)) {

src/smt/theory_fpa.cpp

@@ -415,9 +415,7 @@ namespace smt {
         if (ctx.b_internalized(atom))
             return true;
 
-        unsigned num_args = atom->get_num_args();
+        ctx.internalize(atom->get_args(), atom->get_num_args(), false);
-        for (unsigned i = 0; i < num_args; i++)
-            ctx.internalize(atom->get_arg(i), false);
 
         literal l(ctx.mk_bool_var(atom));
         ctx.set_var_theory(l.var(), get_id());
@@ -436,9 +434,7 @@ namespace smt {
         SASSERT(term->get_family_id() == get_family_id());
         SASSERT(!ctx.e_internalized(term));
 
-        unsigned num_args = term->get_num_args();
+        ctx.internalize(term->get_args(), term->get_num_args(), false);
-        for (unsigned i = 0; i < num_args; i++)
-            ctx.internalize(term->get_arg(i), false);
 
         enode * e = ctx.mk_enode(term, false, false, true);
 
@@ -697,9 +693,7 @@ namespace smt {
     }
 
     enode* theory_fpa::ensure_enode(expr* e) {
-        if (!ctx.e_internalized(e)) {
+        ctx.ensure_internalized(e);
-            ctx.internalize(e, false);
-        }
         enode* n = ctx.get_enode(e);
         ctx.mark_as_relevant(n);
         return n;