From 1a3fe1edd3a9d13d5b3bc672c994f1374c23a226 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 Sep 2018 13:43:38 -0700 Subject: [PATCH] merge Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 2 ++ src/smt/theory_arith_core.h | 15 +++++++++++++ src/smt/theory_lra.cpp | 45 ++++++++++++++++++++++++++++--------- src/smt/theory_lra.h | 3 +++ 4 files changed, 55 insertions(+), 10 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 4b3ee52f6..a2c6c1191 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -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); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 67271ad4f..bce029753 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3302,6 +3302,21 @@ namespace smt { return b && to_expr(b->get_value(), is_int(v), r); } + + template + bool theory_arith::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 + bool theory_arith::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 diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index f8e2f9fe1..fd2dc0da2 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -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); diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h index 074b11ba7..23adaa557 100644 --- a/src/smt/theory_lra.h +++ b/src/smt/theory_lra.h @@ -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;