adding a new toy for Clemens

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Dec 17, 2021 · 9c8800b · 9c8800b
1 parent 6963451
commit 9c8800b
Show file tree

Hide file tree

Showing 8 changed files with 74 additions and 13 deletions.
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
@@ -1729,10 +1729,10 @@ namespace smt {
             return m_user_propagator->add_expr(e);
         }
 
-        void user_propagate_register_declared(user_propagator::register_created_eh_t& r) {
+        void user_propagate_register_created(user_propagator::register_created_eh_t& r) {
             if (!m_user_propagator)
                 throw default_exception("user propagator must be initialized");
-            m_user_propagator->register_declared(r);
+            m_user_propagator->register_created(r);
         }
 
         func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {

diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
@@ -249,8 +249,8 @@ namespace smt {
             return m_kernel.user_propagate_register(e);
         }
 
-        void user_propagate_register_declared(user_propagator::register_created_eh_t& r) {
-            m_kernel.user_propagate_register_declared(r);
+        void user_propagate_register_created(user_propagator::register_created_eh_t& r) {
+            m_kernel.user_propagate_register_created(r);
         }
 
         func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
@@ -305,7 +305,6 @@ namespace smt {
         return m_imp->get_formula(i);
     }
 
-
     void kernel::push() {
         m_imp->push();
     }
@@ -485,8 +484,8 @@ namespace smt {
         return m_imp->user_propagate_register(e);
     }        
 
-    void kernel::user_propagate_register_declared(user_propagator::register_created_eh_t& r) {
-        m_imp->user_propagate_register_declared(r);
+    void kernel::user_propagate_register_created(user_propagator::register_created_eh_t& r) {
+        m_imp->user_propagate_register_created(r);
     }
 
     func_decl* kernel::user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {

diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
@@ -303,7 +303,7 @@ namespace smt {
 
         unsigned user_propagate_register(expr* e);
 
-        void user_propagate_register_declared(user_propagator::register_created_eh_t& r);
+        void user_propagate_register_created(user_propagator::register_created_eh_t& r);
 
         func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range);
 

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
@@ -241,6 +241,14 @@ namespace {
             return m_context.user_propagate_register(e);
         }
 
+        void user_propagate_register_created(user_propagator::register_created_eh_t& c) override {
+            m_context.user_propagate_register_created(c);
+        }
+
+        func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
+            return m_context.user_propagate_declare(name, n, domain, range);
+        }
+
         struct scoped_minimize_core {
             smt_solver& s;
             expr_ref_vector m_assumptions;

diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
@@ -319,15 +319,21 @@ class smt_tactic : public tactic {
     user_propagator::final_eh_t m_final_eh;
     user_propagator::eq_eh_t    m_eq_eh;
     user_propagator::eq_eh_t    m_diseq_eh;
+    user_propagator::register_created_eh_t m_created_eh;
+
     expr_ref_vector             m_vars;
     unsigned_vector             m_var2internal;
     unsigned_vector             m_internal2var;
+    unsigned_vector             m_limit;    
+
 
+    user_propagator::push_eh_t  i_push_eh;
+    user_propagator::pop_eh_t   i_pop_eh;
     user_propagator::fixed_eh_t i_fixed_eh;
     user_propagator::final_eh_t i_final_eh;
     user_propagator::eq_eh_t    i_eq_eh;
     user_propagator::eq_eh_t    i_diseq_eh;
-
+    user_propagator::register_created_eh_t i_created_eh;
 
 
     struct callback : public user_propagator::callback {
@@ -403,15 +409,43 @@ class smt_tactic : public tactic {
         m_ctx->user_propagate_register_diseq(i_diseq_eh);
     }
 
+    void init_i_created_eh() {
+        if (!m_created_eh)
+            return;
+        i_created_eh = [this](void* ctx, user_propagator::callback* cb, expr* e, unsigned i) {
+            unsigned j = m_vars.size();
+            m_vars.push_back(e);
+            m_internal2var.setx(i, j, 0);
+            m_var2internal.setx(j, i, 0);
+        };
+        m_ctx->user_propagate_register_created(i_created_eh);
+    }
+
+    void init_i_push_pop() {
+        i_push_eh = [this](void* ctx) {
+            m_limit.push_back(m_vars.size());
+            m_push_eh(ctx);
+        };
+        i_pop_eh = [this](void* ctx, unsigned n) {
+            unsigned old_sz = m_limit.size() - n;
+            unsigned num_vars = m_limit[old_sz];            
+            m_vars.shrink(num_vars);            
+            m_limit.shrink(old_sz);
+            m_pop_eh(ctx, n);            
+        };
+    }
+
 
     void user_propagate_delay_init() {
         if (!m_user_ctx)
             return;
-        m_ctx->user_propagate_init(m_user_ctx, m_push_eh, m_pop_eh, m_fresh_eh);
+        init_i_push_pop();
+        m_ctx->user_propagate_init(m_user_ctx, i_push_eh, i_pop_eh, m_fresh_eh);
         init_i_fixed_eh();
         init_i_final_eh();
         init_i_eq_eh();
         init_i_diseq_eh();
+        init_i_created_eh();
 
         unsigned i = 0;
         for (expr* v : m_vars) {
@@ -463,6 +497,14 @@ class smt_tactic : public tactic {
         m_vars.push_back(e);
         return m_vars.size() - 1;
     }
+
+    func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override {
+        return m_ctx->user_propagate_declare(name, n, domain, range);
+    }
+
+    void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override {
+        m_ctx->user_propagate_register_created(created_eh);
+    }
 };
 
 static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) {

diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
@@ -189,8 +189,12 @@ bool theory_user_propagator::internalize_atom(app* atom, bool gate_ctx) {
 }
 
 bool theory_user_propagator::internalize_term(app* term)  { 
-    NOT_IMPLEMENTED_YET();
-    return false;    
+    for (auto arg : *term)
+        ensure_enode(arg);
+    unsigned v = add_expr(term);
+    if (m_created_eh)
+        m_created_eh(m_user_context, this, term, v);
+    return true;
 }
 
 void theory_user_propagator::collect_statistics(::statistics & st) const {

diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h
@@ -96,7 +96,7 @@ namespace smt {
         void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; }
         void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; }
         void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; }
-        void register_declared(user_propagator::register_created_eh_t& created_eh) { m_created_eh = created_eh; }
+        void register_created(user_propagator::register_created_eh_t& created_eh) { m_created_eh = created_eh; }
         func_decl* declare(symbol const& name, unsigned n, sort* const* domain, sort* range);
 
         bool has_fixed() const { return (bool)m_fixed_eh; }

diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
@@ -200,6 +200,14 @@ class and_then_tactical : public binary_tactical {
         m_t2->user_propagate_clear();
     }
 
+    void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override {
+        m_t2->user_propagate_register_created(created_eh);
+    }
+
+    func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override {
+        return m_t2->user_propagate_declare(name, n, domain, range);
+    }
+
 };
 
 tactic * and_then(tactic * t1, tactic * t2) {