From 342feeff03016d4be04b27eccd9af453a4093ace Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 29 Jun 2018 14:17:13 -0700 Subject: [PATCH] implement get_lower, get_upper in theory_lra.cpp Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 06d0730b7..120ce1517 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2612,12 +2612,26 @@ public: } bool get_lower(enode* n, expr_ref& r) { - NOT_IMPLEMENTED_YET(); + theory_var v = n->get_th_var(get_id()); + lp::constraint_index ci; + rational val; + bool is_strict; + if (m_solver->has_lower_bound(v, ci, val, is_strict)) { + r = a.mk_numeral(val, is_int(n)); + return true; + } return false; } bool get_upper(enode* n, expr_ref& r) { - NOT_IMPLEMENTED_YET(); + theory_var v = n->get_th_var(get_id()); + lp::constraint_index ci; + rational val; + bool is_strict; + if (m_solver->has_upper_bound(v, ci, val, is_strict)) { + r = a.mk_numeral(val, is_int(n)); + return true; + } return false; }