fixup registration with new terms during internalization

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Jan 12, 2025 · 97acf71 · 97acf71
1 parent d3183fa
commit 97acf71
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 2 deletions.
diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
@@ -110,7 +110,8 @@ namespace sls {
     template<typename num_t>
     arith_base<num_t>::arith_base(context& ctx) :
         plugin(ctx),
-        a(m) {
+        a(m),
+        m_new_terms(m) {
         m_fid = a.get_family_id();
     }
 
@@ -807,14 +808,18 @@ namespace sls {
         }
         else if (a.is_mul(e, x, y) && a.is_add(y, z, u)) {
             expr_ref t(a.mk_mul(x, z), m);
+            m_new_terms.push_back(t);
             add_args(term, t, coeff);
             t = a.mk_mul(x, u);
+            m_new_terms.push_back(t);
             add_args(term, t, coeff);
         }
         else if (a.is_mul(e, x, y) && a.is_add(x, z, u)) {
             expr_ref t(a.mk_mul(y, z), m);
+            m_new_terms.push_back(t);
             add_args(term, t, coeff);
             t = a.mk_mul(y, u);
+            m_new_terms.push_back(t);
             add_args(term, t, coeff);
         }
         else if (a.is_mul(e)) {
@@ -1006,7 +1011,14 @@ namespace sls {
         else {
             SASSERT(!a.is_arith_expr(e));
         }
-
+        add_new_terms();        
+    }
+
+    template<typename num_t>
+    void arith_base<num_t>::add_new_terms() {
+        for (unsigned i = 0; i < m_new_terms.size(); ++i)
+            ctx.add_new_term(m_new_terms.get(i));
+        m_new_terms.reset();
     }
 
     template<typename num_t>
@@ -1968,6 +1980,7 @@ namespace sls {
             for (auto arg : *e)
                 if (a.is_int_real(arg))
                     mk_term(arg);
+        add_new_terms();
     }
 
     template<typename num_t>

diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h
@@ -191,6 +191,7 @@ namespace sls {
         vector<mul_def>              m_muls;
         vector<add_def>              m_adds;
         vector<op_def>               m_ops;
+        expr_ref_vector              m_new_terms;
         unsigned_vector              m_expr2var;
         svector<double>              m_probs;
         bool                         m_dscore_mode = false;
@@ -281,6 +282,7 @@ namespace sls {
         void add_args(linear_term& term, expr* e, num_t const& sign);
         ineq& new_ineq(ineq_kind op, num_t const& bound);
         void init_ineq(sat::bool_var bv, ineq& i);
+        void add_new_terms();
         num_t divide(var_t v, num_t const& delta, num_t const& coeff);
         num_t divide_floor(var_t v, num_t const& a, num_t const& b);
         num_t divide_ceil(var_t v, num_t const& a, num_t const& b);

diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
@@ -175,6 +175,7 @@ namespace sls {
         bool is_true(sat::bool_var v) const { return s.is_true(sat::literal(v, false)); }
         expr* atom(sat::bool_var v) { return m_atoms.get(v, nullptr); }
         expr* term(unsigned id) const { return m_allterms.get(id); }
+        void add_new_term(expr* e) { register_terms(e); }
         sat::bool_var atom2bool_var(expr* e) const { return m_atom2bool_var.get(e->get_id(), sat::null_bool_var); }
         sat::literal mk_literal(expr* e);
         void add_input_assertion(expr* f) { add_assertion(f, true); }