mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-16 13:43:38 -07:00
parent 286126dde9
commit 1a3fe1edd3
4 changed files with 55 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_arith.h
View file

@ -1071,6 +1071,8 @@ namespace smt {
bool get_lower(enode* n, expr_ref& r);
bool get_upper(enode* n, expr_ref& r);
bool get_lower(enode* n, rational& r, bool &is_strict);
bool get_upper(enode* n, rational& r, bool &is_strict);
bool to_expr(inf_numeral const& val, bool is_int, expr_ref& r);

15
src/smt/theory_arith_core.h
View file

@ -3302,6 +3302,21 @@ namespace smt {
return b && to_expr(b->get_value(), is_int(v), r);
}
template<typename Ext>
bool theory_arith<Ext>::get_lower(enode * n, rational& r, bool& is_strict) {
theory_var v = n->get_th_var(get_id());
bound* b = (v == null_theory_var) ? nullptr : lower(v);
return b && (r = b->get_value().get_rational().to_rational(), is_strict = b->get_value().get_infinitesimal().is_pos(), true);
}
template<typename Ext>
bool theory_arith<Ext>::get_upper(enode * n, rational& r, bool& is_strict) {
theory_var v = n->get_th_var(get_id());
bound* b = (v == null_theory_var) ? nullptr : upper(v);
return b && (r = b->get_value().get_rational().to_rational(), is_strict = b->get_value().get_infinitesimal().is_neg(), true);
}
// -----------------------------------
//
// Backtracking

45
src/smt/theory_lra.cpp
View file

@ -2963,13 +2963,22 @@ public:
}
}
bool get_value(enode* n, expr_ref& r) {
bool get_value(enode* n, rational& val) {
theory_var v = n->get_th_var(get_id());
if (!can_get_bound(v)) return false;
lp::var_index vi = m_theory_var2var_index[v];
rational val;
if (m_solver->has_value(vi, val)) {
if (is_int(n) && !val.is_int()) return false;
return true;
}
else {
return false;
}
}
bool get_value(enode* n, expr_ref& r) {
rational val;
if (get_value(n, val)) {
r = a.mk_numeral(val, is_int(n));
return true;
}
@ -2978,7 +2987,7 @@ public:
}
}
bool get_lower(enode* n, expr_ref& r) {
bool get_lower(enode* n, rational& val, bool& is_strict) {
theory_var v = n->get_th_var(get_id());
if (!can_get_bound(v)) {
TRACE("arith", tout << "cannot get lower for " << v << "\n";);
@ -2986,29 +2995,36 @@ public:
}
lp::var_index vi = m_theory_var2var_index[v];
lp::constraint_index ci;
rational val;
return m_solver->has_lower_bound(vi, ci, val, is_strict);
}
bool get_lower(enode* n, expr_ref& r) {
bool is_strict;
if (m_solver->has_lower_bound(vi, ci, val, is_strict)) {
rational val;
if (get_lower(n, val, is_strict) && !is_strict) {
r = a.mk_numeral(val, is_int(n));
return true;
}
TRACE("arith", m_solver->print_constraints(tout << "does not have lower bound " << vi << "\n"););
return false;
}
bool get_upper(enode* n, expr_ref& r) {
bool get_upper(enode* n, rational& val, bool& is_strict) {
theory_var v = n->get_th_var(get_id());
if (!can_get_bound(v))
return false;
lp::var_index vi = m_theory_var2var_index[v];
lp::constraint_index ci;
rational val;
return m_solver->has_upper_bound(vi, ci, val, is_strict);
}
bool get_upper(enode* n, expr_ref& r) {
bool is_strict;
if (m_solver->has_upper_bound(vi, ci, val, is_strict)) {
rational val;
if (get_upper(n, val, is_strict) && !is_strict) {
r = a.mk_numeral(val, is_int(n));
return true;
}
TRACE("arith", m_solver->print_constraints(tout << "does not have upper bound " << vi << "\n"););
return false;
}
@ -3439,6 +3455,9 @@ void theory_lra::init_model(model_generator & m) {
model_value_proc * theory_lra::mk_value(enode * n, model_generator & mg) {
return m_imp->mk_value(n, mg);
}
bool theory_lra::get_value(enode* n, rational& r) {
return m_imp->get_value(n, r);
}
bool theory_lra::get_value(enode* n, expr_ref& r) {
return m_imp->get_value(n, r);
}
@ -3448,6 +3467,12 @@ bool theory_lra::get_lower(enode* n, expr_ref& r) {
bool theory_lra::get_upper(enode* n, expr_ref& r) {
return m_imp->get_upper(n, r);
}
bool theory_lra::get_lower(enode* n, rational& r, bool& is_strict) {
return m_imp->get_lower(n, r, is_strict);
}
bool theory_lra::get_upper(enode* n, rational& r, bool& is_strict) {
return m_imp->get_upper(n, r, is_strict);
}
bool theory_lra::validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const {
return m_imp->validate_eq_in_model(v1, v2, is_true);

3
src/smt/theory_lra.h
View file

@ -78,8 +78,11 @@ namespace smt {
model_value_proc * mk_value(enode * n, model_generator & mg) override;
bool get_value(enode* n, expr_ref& r) override;
bool get_value(enode* n, rational& r);
bool get_lower(enode* n, expr_ref& r);
bool get_upper(enode* n, expr_ref& r);
bool get_lower(enode* n, rational& r, bool& is_strict);
bool get_upper(enode* n, rational& r, bool& is_strict);
bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const override;