Skip to content

Commit

Permalink
use get_value/get_ivalue API instead of self-rolled from arith_solver
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Nov 3, 2020
1 parent ee12e3f commit 5335097
Show file tree
Hide file tree
Showing 4 changed files with 23 additions and 90 deletions.
4 changes: 2 additions & 2 deletions src/sat/smt/arith_axioms.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -399,7 +399,7 @@ namespace arith {
theory_var v = mk_evar(n);
theory_var v1 = mk_evar(p);

if (!can_get_ivalue(v1))
if (!is_registered_var(v1))
continue;
lp::impq r1 = get_ivalue(v1);
rational r2;
Expand All @@ -419,7 +419,7 @@ namespace arith {
TRACE("arith", tout << "unbounded " << expr_ref(n, m) << "\n";);
continue;
}
if (!can_get_ivalue(v))
if (!is_registered_var(v))
continue;
lp::impq val_v = get_ivalue(v);
if (val_v.y.is_zero() && val_v.x == div(r1.x, r2)) continue;
Expand Down
11 changes: 7 additions & 4 deletions src/sat/smt/arith_diagnostics.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,13 +52,16 @@ namespace arith {
out << "null";
else
out << (t.is_term() ? "t" : "j") << vi;
if (m_nla && m_nla->use_nra_model() && can_get_ivalue(v)) {
if (m_nla && m_nla->use_nra_model() && is_registered_var(v)) {
scoped_anum an(m_nla->am());
m_nla->am().display(out << " = ", nl_value(v, an));
}
else if (can_get_value(v)) out << " = " << get_value(v);
if (is_int(v)) out << ", int";
if (ctx.is_shared(var2enode(v))) out << ", shared";
else if (m_model_is_initialized && is_registered_var(v))
out << " = " << get_value(v);
if (is_int(v))
out << ", int";
if (ctx.is_shared(var2enode(v)))
out << ", shared";
}
out << " := " << mk_bounded_pp(var2expr(v), m) << "\n";
}
Expand Down
88 changes: 11 additions & 77 deletions src/sat/smt/arith_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,6 @@ namespace arith {
m_bound_terms(m),
m_bound_predicate(m)
{
reset_variable_values();
m_solver = alloc(lp::lar_solver);

smt_params_helper lpar(ctx.s().params());
Expand Down Expand Up @@ -751,18 +750,15 @@ namespace arith {
bound_prop_mode::BP_NONE;
}

void solver::init_variable_values() {
reset_variable_values();
void solver::init_model() {
if (m.inc() && m_solver.get() && get_num_vars() > 0) {
TRACE("arith", display(tout << "update variable values\n"););
lp().get_model(m_variable_values);
ctx.push(value_trail<euf::solver, bool>(m_model_is_initialized));
m_model_is_initialized = true;
lp().init_model();
}
}

void solver::reset_variable_values() {
m_variable_values.clear();
}

lbool solver::get_phase(bool_var v) {
api_bound* b;
if (!m_bool_var2bound.find(v, b)) {
Expand All @@ -786,87 +782,25 @@ namespace arith {
return lp().compare_values(vi, k, b->get_value()) ? l_true : l_false;
}

bool solver::can_get_value(theory_var v) const {
return can_get_bound(v) && !m_variable_values.empty();
}

bool solver::can_get_bound(theory_var v) const {
bool solver::is_registered_var(theory_var v) const {
return v != euf::null_theory_var && lp().external_is_used(v);
}

bool solver::can_get_ivalue(theory_var v) const {
return can_get_bound(v);
}

void solver::ensure_column(theory_var v) {
SASSERT(!is_bool(v));
if (!lp().external_is_used(v))
register_theory_var_in_lar_solver(v);
}

lp::impq solver::get_ivalue(theory_var v) const {
SASSERT(can_get_ivalue(v));
auto t = get_tv(v);
if (!t.is_term())
return lp().get_column_value(t.id());
m_todo_terms.push_back(std::make_pair(t, rational::one()));
lp::impq result(0);
while (!m_todo_terms.empty()) {
t = m_todo_terms.back().first;
rational coeff = m_todo_terms.back().second;
m_todo_terms.pop_back();
if (t.is_term()) {
const lp::lar_term& term = lp().get_term(t);
for (const auto& i : term) {
m_todo_terms.push_back(std::make_pair(lp().column2tv(i.column()), coeff * i.coeff()));
}
}
else {
result += lp().get_column_value(t.id()) * coeff;
}
}
return result;
SASSERT(is_registered_var(v));
return m_solver->get_ivalue(get_tv(v));
}

rational solver::get_value(theory_var v) const {
if (v == euf::null_theory_var || !lp().external_is_used(v)) {
if (v == euf::null_theory_var || !lp().external_is_used(v))
return rational::zero();
}

auto t = get_tv(v);
if (m_variable_values.count(t.index()) > 0)
return m_variable_values[t.index()];

if (!t.is_term() && lp().is_fixed(t.id()))
return lp().column_lower_bound(t.id()).x;

if (!t.is_term())
return rational::zero();

m_todo_terms.push_back(std::make_pair(t, rational::one()));
rational result(0);
while (!m_todo_terms.empty()) {
auto t2 = m_todo_terms.back().first;
rational coeff = m_todo_terms.back().second;
m_todo_terms.pop_back();
if (t2.is_term()) {
const lp::lar_term& term = lp().get_term(t2);
for (const auto& i : term) {
auto tv = lp().column2tv(i.column());
if (m_variable_values.count(tv.index()) > 0) {
result += m_variable_values[tv.index()] * coeff * i.coeff();
}
else {
m_todo_terms.push_back(std::make_pair(tv, coeff * i.coeff()));
}
}
}
else {
result += m_variable_values[t2.index()] * coeff;
}
}
m_variable_values[t.index()] = result;
return result;
return m_solver->get_value(get_tv(v));
}

void solver::random_update() {
Expand Down Expand Up @@ -915,7 +849,7 @@ namespace arith {
if (!ctx.is_shared(var2enode(v)))
continue;
ensure_column(v);
if (!can_get_ivalue(v))
if (!is_registered_var(v))
continue;
theory_var other = m_model_eqs.insert_if_not_there(v);
TRACE("arith", tout << "insert: v" << v << " := " << get_value(v) << " found: v" << other << "\n";);
Expand Down Expand Up @@ -977,8 +911,8 @@ namespace arith {

sat::check_result solver::check() {
force_push();
m_model_is_initialized = false;
flet<bool> _is_learned(m_is_redundant, true);
reset_variable_values();
IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
SASSERT(lp().ax_is_correct());

Expand Down
10 changes: 3 additions & 7 deletions src/sat/smt/arith_solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,6 @@ namespace arith {
vector<rational> m_columns;
var_coeffs m_left_side; // constraint left side

mutable std::unordered_map<lpvar, rational> m_variable_values; // current model
lpvar m_one_var { UINT_MAX };
lpvar m_zero_var { UINT_MAX };
lpvar m_rone_var { UINT_MAX };
Expand Down Expand Up @@ -332,12 +331,8 @@ namespace arith {
bool all_zeros(vector<rational> const& v) const;

bound_prop_mode propagation_mode() const;
void init_variable_values();
void reset_variable_values();

bool can_get_value(theory_var v) const;
bool can_get_bound(theory_var v) const;
bool can_get_ivalue(theory_var v) const;
bool is_registered_var(theory_var v) const;
void ensure_column(theory_var v);
lp::impq get_ivalue(theory_var v) const;
rational get_value(theory_var v) const;
Expand Down Expand Up @@ -378,6 +373,7 @@ namespace arith {

obj_map<expr, expr*> m_predicate2term;
obj_map<expr, bound_info> m_term2bound_info;
bool m_model_is_initialized{ false };

bool use_bounded_expansion() const { return get_config().m_arith_bounded_expansion; }
unsigned small_lemma_size() const { return get_config().m_arith_small_lemma_size; }
Expand Down Expand Up @@ -428,7 +424,7 @@ namespace arith {
void new_eq_eh(euf::th_eq const& eq) override { mk_eq_axiom(true, eq); }
void new_diseq_eh(euf::th_eq const& de) override { mk_eq_axiom(false, de); }
bool unit_propagate() override;
void init_model() override { init_variable_values(); }
void init_model() override;
void finalize_model(model& mdl) override { DEBUG_CODE(dbg_finalize_model(mdl);); }
void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
Expand Down

0 comments on commit 5335097

Please sign in to comment.