mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

remove shared attribute

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-07-15 14:46:55 -07:00
parent 04ad63c732
commit cc208394c3
2 changed files with 0 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -346,11 +346,6 @@ namespace sls {
SASSERT(dtt(sign(bv), ineq) == 0); SASSERT(dtt(sign(bv), ineq) == 0);
} }
vi.m_value = new_value; vi.m_value = new_value;
if (vi.m_shared) {
sort* s = vi.m_sort == var_sort::INT ? a.mk_int() : a.mk_real();
expr_ref num = from_num(s, new_value);
ctx.set_value(vi.m_expr, num);
}
for (auto idx : vi.m_muls) { for (auto idx : vi.m_muls) {
auto const& [w, coeff, monomial] = m_muls[idx]; auto const& [w, coeff, monomial] = m_muls[idx];
ctx.new_value_eh(m_vars[w].m_expr); ctx.new_value_eh(m_vars[w].m_expr);

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

@ -67,7 +67,6 @@ namespace sls {
expr* m_expr; expr* m_expr;
num_t m_value{ 0 }; num_t m_value{ 0 };
num_t m_best_value{ 0 }; num_t m_best_value{ 0 };
bool m_shared = false;
var_sort m_sort; var_sort m_sort;
arith_op_kind m_op = arith_op_kind::LAST_ARITH_OP; arith_op_kind m_op = arith_op_kind::LAST_ARITH_OP;
unsigned m_def_idx = UINT_MAX; unsigned m_def_idx = UINT_MAX;