mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
rename
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
620204bbb4
commit
d0d06c288a
|
@ -1176,16 +1176,21 @@ namespace lp {
|
|||
return rp.x + m_delta * rp.y;
|
||||
}
|
||||
|
||||
mpq lar_solver::get_value(tv const& t) const {
|
||||
mpq lar_solver::get_tv_value(tv const& t) const {
|
||||
if (t.is_var())
|
||||
return get_value(t.column());
|
||||
#if 0
|
||||
unsigned term_j = 0;
|
||||
if (m_var_register.term_is_used(t.id(), term_j))
|
||||
return get_value(column_index(term_j));
|
||||
#endif
|
||||
mpq r(0);
|
||||
for (const auto& p : get_term(t))
|
||||
r += p.coeff() * get_value(p.column());
|
||||
return r;
|
||||
}
|
||||
|
||||
impq lar_solver::get_ivalue(tv const& t) const {
|
||||
impq lar_solver::get_tv_ivalue(tv const& t) const {
|
||||
if (t.is_var())
|
||||
return get_ivalue(t.column());
|
||||
impq r;
|
||||
|
|
|
@ -524,8 +524,8 @@ public:
|
|||
std::ostream& print_values(std::ostream& out) const;
|
||||
bool init_model() const;
|
||||
mpq get_value(column_index const& j) const;
|
||||
mpq get_value(tv const& t) const;
|
||||
impq get_ivalue(tv const& t) const;
|
||||
mpq get_tv_value(tv const& t) const;
|
||||
impq get_tv_ivalue(tv const& t) const;
|
||||
void get_model(std::unordered_map<var_index, mpq> & variable_values) const;
|
||||
void get_rid_of_inf_eps();
|
||||
void get_model_do_not_care_about_diff_vars(std::unordered_map<var_index, mpq> & variable_values) const;
|
||||
|
|
|
@ -794,11 +794,11 @@ namespace arith {
|
|||
|
||||
lp::impq solver::get_ivalue(theory_var v) const {
|
||||
SASSERT(is_registered_var(v));
|
||||
return m_solver->get_ivalue(get_tv(v));
|
||||
return m_solver->get_tv_ivalue(get_tv(v));
|
||||
}
|
||||
|
||||
rational solver::get_value(theory_var v) const {
|
||||
return is_registered_var(v) ? m_solver->get_value(get_tv(v)) : rational::zero();
|
||||
return is_registered_var(v) ? m_solver->get_tv_value(get_tv(v)) : rational::zero();
|
||||
}
|
||||
|
||||
void solver::random_update() {
|
||||
|
|
|
@ -1409,11 +1409,11 @@ public:
|
|||
|
||||
lp::impq get_ivalue(theory_var v) const {
|
||||
SASSERT(is_registered_var(v));
|
||||
return lp().get_ivalue(get_tv(v));
|
||||
return lp().get_tv_ivalue(get_tv(v));
|
||||
}
|
||||
|
||||
rational get_value(theory_var v) const {
|
||||
return is_registered_var(v) ? lp().get_value(get_tv(v)) : rational::zero();
|
||||
return is_registered_var(v) ? lp().get_tv_value(get_tv(v)) : rational::zero();
|
||||
}
|
||||
|
||||
bool m_model_is_initialized{ false };
|
||||
|
|
Loading…
Reference in a new issue