mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 12:50:32 +00:00
Code Activity

fixup registration with new terms during internalization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-12 14:12:02 -08:00
parent d3183fafc7
commit 97acf71d2d
3 changed files with 18 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/ast/sls/sls_arith_base.cpp
View file

@ -110,7 +110,8 @@ namespace sls {
template<typename num_t> template<typename num_t>
arith_base<num_t>::arith_base(context& ctx) : arith_base<num_t>::arith_base(context& ctx) :
plugin(ctx), plugin(ctx),
a(m) { a(m),
m_new_terms(m) {
m_fid = a.get_family_id(); 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)) { else if (a.is_mul(e, x, y) && a.is_add(y, z, u)) {
expr_ref t(a.mk_mul(x, z), m); expr_ref t(a.mk_mul(x, z), m);
m_new_terms.push_back(t);
add_args(term, t, coeff); add_args(term, t, coeff);
t = a.mk_mul(x, u); t = a.mk_mul(x, u);
m_new_terms.push_back(t);
add_args(term, t, coeff); add_args(term, t, coeff);
} }
else if (a.is_mul(e, x, y) && a.is_add(x, z, u)) { else if (a.is_mul(e, x, y) && a.is_add(x, z, u)) {
expr_ref t(a.mk_mul(y, z), m); expr_ref t(a.mk_mul(y, z), m);
m_new_terms.push_back(t);
add_args(term, t, coeff); add_args(term, t, coeff);
t = a.mk_mul(y, u); t = a.mk_mul(y, u);
m_new_terms.push_back(t);
add_args(term, t, coeff); add_args(term, t, coeff);
} }
else if (a.is_mul(e)) { else if (a.is_mul(e)) {
@ -1006,7 +1011,14 @@ namespace sls {
else { else {
SASSERT(!a.is_arith_expr(e)); 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> template<typename num_t>
@ -1968,6 +1980,7 @@ namespace sls {
for (auto arg : *e) for (auto arg : *e)
if (a.is_int_real(arg)) if (a.is_int_real(arg))
mk_term(arg); mk_term(arg);
add_new_terms();
} }
template<typename num_t> template<typename num_t>

2
src/ast/sls/sls_arith_base.h
View file

@ -191,6 +191,7 @@ namespace sls {
vector<mul_def> m_muls; vector<mul_def> m_muls;
vector<add_def> m_adds; vector<add_def> m_adds;
vector<op_def> m_ops; vector<op_def> m_ops;
expr_ref_vector m_new_terms;
unsigned_vector m_expr2var; unsigned_vector m_expr2var;
svector<double> m_probs; svector<double> m_probs;
bool m_dscore_mode = false; bool m_dscore_mode = false;
@ -281,6 +282,7 @@ namespace sls {
void add_args(linear_term& term, expr* e, num_t const& sign); void add_args(linear_term& term, expr* e, num_t const& sign);
ineq& new_ineq(ineq_kind op, num_t const& bound); ineq& new_ineq(ineq_kind op, num_t const& bound);
void init_ineq(sat::bool_var bv, ineq& i); 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(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_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); num_t divide_ceil(var_t v, num_t const& a, num_t const& b);

1
src/ast/sls/sls_context.h
View file

@ -175,6 +175,7 @@ namespace sls {
bool is_true(sat::bool_var v) const { return s.is_true(sat::literal(v, false)); } 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* atom(sat::bool_var v) { return m_atoms.get(v, nullptr); }
expr* term(unsigned id) const { return m_allterms.get(id); } 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::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); sat::literal mk_literal(expr* e);
void add_input_assertion(expr* f) { add_assertion(f, true); } void add_input_assertion(expr* f) { add_assertion(f, true); }