fix #2773 fix #2774

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

src/smt/smt_context.cpp

@@ -2820,14 +2820,15 @@ namespace smt {
     /**
        \brief Auxiliary method for #already_internalized_theory.
     */
-    bool context::already_internalized_theory_core(theory * th, expr_ref_vector const & s) const {
+    bool context::already_internalized_theory_core(theory * th, expr_ref_vector const & s) const {        
         expr_mark visited;
         family_id fid = th->get_id();
         unsigned sz = s.size();
         for (unsigned i = 0; i < sz; i++) {
             expr * n = s.get(i);
-            if (uses_theory(n, fid, visited))
+            if (uses_theory(n, fid, visited)) {
                 return true;
+            }
         }
         return false;
     }
@@ -2838,6 +2839,7 @@ namespace smt {
             dealloc(th);
             return; // context already has a theory for the given family id.
         }
+        TRACE("internalize", tout << this << " " << th->get_family_id() << "\n";);
         SASSERT(std::find(m_theory_set.begin(), m_theory_set.end(), th) == m_theory_set.end());
         SASSERT(!already_internalized_theory(th));
         th->init(this);

src/smt/smt_context.h

@@ -1598,8 +1598,6 @@ namespace smt {
                 m_case_split_queue->internalize_instance_eh(body, generation);
         }
 
-        bool already_internalized() const { return m_e_internalized_stack.size() > 2 || m_b_internalized_stack.size() > 1; }
-
         unsigned get_unsat_core_size() const {
             return m_unsat_core.size();
         }

src/smt/smt_setup.cpp

@@ -49,8 +49,8 @@ namespace smt {
     }
 
     void setup::operator()(config_mode cm) {
+        TRACE("internalize", tout << "setup " << &m_context << "\n";);
         SASSERT(m_context.get_scope_level() == 0);
-        SASSERT(!m_context.already_internalized());
         SASSERT(!m_already_configured);
         // if (m_params.m_mbqi && m_params.m_model_compact) {
         //    warning_msg("ignoring MODEL_COMPACT=true because it cannot be used with MBQI=true");

src/smt/theory_dense_diff_logic_def.h

@@ -184,6 +184,7 @@ namespace smt {
             std::swap(source, target);
             offset.neg();
         }
+		if (ctx.b_internalized(n)) return true;
         bool_var bv = ctx.mk_bool_var(n);
         ctx.set_var_theory(bv, get_id());
         atom * a    = alloc(atom, bv, source, target, offset);

src/smt/theory_diff_logic.h

@@ -375,7 +375,9 @@ namespace smt {
 
         void get_implied_bound_antecedents(edge_id bridge_edge, edge_id subsumed_edge, conflict_resolution & cr);
 
-        theory_var get_zero(bool is_int) const { return is_int ? m_izero : m_rzero; }
+        void init_zero();
+
+        theory_var get_zero(bool is_int) { init_zero(); return is_int ? m_izero : m_rzero; }
 
         void inc_conflicts();
 

src/smt/theory_diff_logic_def.h

@@ -66,17 +66,6 @@ void theory_diff_logic<Ext>::nc_functor::reset() {
 template<typename Ext>
 void theory_diff_logic<Ext>::init(context * ctx) {
     theory::init(ctx);
-    app* zero;
-    enode* e;
-    zero = m_util.mk_numeral(rational(0), true);
-    e = ctx->mk_enode(zero, false, false, true);
-    SASSERT(!is_attached_to_var(e));
-    m_izero = mk_var(e);
-
-    zero = m_util.mk_numeral(rational(0), false);
-    e = ctx->mk_enode(zero, false, false, true);
-    SASSERT(!is_attached_to_var(e));
-    m_rzero = mk_var(e);
 }
 
 
@@ -220,6 +209,7 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
         k.neg();
     }
 
+	if (ctx.b_internalized(n)) return true;
     bv = ctx.mk_bool_var(n);
     ctx.set_var_theory(bv, get_id());
     literal l(bv);
@@ -365,8 +355,8 @@ final_check_status theory_diff_logic<Ext>::final_check_eh() {
 
     TRACE("arith_final", display(tout); );
     // either will already be zero (as we don't do mixed constraints).
-    m_graph.set_to_zero(m_izero);
-    m_graph.set_to_zero(m_rzero);
+    m_graph.set_to_zero(get_zero(true));
+    m_graph.set_to_zero(get_zero(false));
     SASSERT(is_consistent());
     if (m_non_diff_logic_exprs) {
         return FC_GIVEUP; 
@@ -810,14 +800,12 @@ theory_var theory_diff_logic<Ext>::mk_var(app* n) {
     context & ctx = get_context();
     enode* e = nullptr;
     theory_var v = null_theory_var;
-    if (ctx.e_internalized(n)) {
-        e = ctx.get_enode(n);
-        v = e->get_th_var(get_id());
-    }
-    else {
-        ctx.internalize(n, false);
-        e = ctx.get_enode(n);
-    }
+	if (!ctx.e_internalized(n)) {
+		ctx.internalize(n, false);
+	}
+    e = ctx.get_enode(n);
+    v = e->get_th_var(get_id());
+
     if (v == null_theory_var) {
         v = mk_var(e);
     }      
@@ -1391,6 +1379,22 @@ theory* theory_diff_logic<Ext>::mk_fresh(context* new_ctx) {
     return alloc(theory_diff_logic<Ext>, new_ctx->get_manager(), m_params); 
 }
 
+template<typename Ext>
+void theory_diff_logic<Ext>::init_zero() {
+    if (m_izero != null_theory_var) return;
+    context & ctx = get_context();
+    app* zero;
+    enode* e;
+    zero = m_util.mk_numeral(rational(0), true);
+    e = ctx.mk_enode(zero, false, false, true);
+    SASSERT(!is_attached_to_var(e));
+    m_izero = mk_var(e);
+
+    zero = m_util.mk_numeral(rational(0), false);
+    e = ctx.mk_enode(zero, false, false, true);
+    SASSERT(!is_attached_to_var(e));
+    m_rzero = mk_var(e);   
+}
 
 #endif /* THEORY_DIFF_LOGIC_DEF_H_ */
 

src/smt/theory_utvpi.h

@@ -299,9 +299,11 @@ namespace smt {
 
         void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just);
         
-        th_var get_zero(sort* s) const { return m_zero; }
+        th_var get_zero(sort* s) { init_zero(); return m_zero; }
 
-        th_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); }
+        th_var get_zero(expr* e) { return get_zero(get_manager().get_sort(e)); }
+
+        void init_zero();
 
         void inc_conflicts();
 

src/smt/theory_utvpi_def.h

@@ -259,7 +259,14 @@ namespace smt {
     template<typename Ext>
     void theory_utvpi<Ext>::init(context* ctx) {
         theory::init(ctx);
-        m_zero  = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), true), false, false, true));
+        m_zero = null_theory_var;
+    }
+
+    template<typename Ext>
+    void theory_utvpi<Ext>::init_zero() {
+        if (m_zero == null_theory_var) {
+            m_zero  = mk_var(get_context().mk_enode(a.mk_numeral(rational(0), true), false, false, true));
+        }
     }
 
     /**
@@ -553,7 +560,7 @@ namespace smt {
         theory_var v = null_theory_var;
         context& ctx = get_context();
         if (r.is_zero()) {            
-            v = m_zero;
+            v = get_zero(n);
         }
         else if (ctx.e_internalized(n)) {
             enode* e = ctx.get_enode(n);
@@ -775,6 +782,7 @@ namespace smt {
         m_factory = alloc(arith_factory, get_manager());
         m.register_factory(m_factory);
         enforce_parity();
+        init_zero();
         m_graph.set_to_zero(to_var(m_zero), neg(to_var(m_zero)));
         compute_delta();   
         DEBUG_CODE(model_validate(););