mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

implement get_lower, get_upper in theory_lra.cpp

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-06-29 14:17:13 -07:00
parent da44ad7e6f
commit 342feeff03
1 changed files with 16 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_lra.cpp
View file

@ -2612,12 +2612,26 @@ public:
} }
bool get_lower(enode* n, expr_ref& r) { 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; return false;
} }
bool get_upper(enode* n, expr_ref& r) { 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; return false;
} }