mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 23:33:41 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Jakob Rath 2023-02-20 16:13:55 +01:00
parent d5ce9b3d5e
commit 4cca164bb4
2 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/viable.cpp
View file

@ -835,7 +835,7 @@ namespace {
do { do {
found = false; found = false;
do { do {
if (!e->refined) { if (!e->refined && e->side_cond.empty()) {
auto const& lo = e->interval.lo(); auto const& lo = e->interval.lo();
auto const& hi = e->interval.hi(); auto const& hi = e->interval.hi();
if (lo.is_val() && hi.is_val()) { if (lo.is_val() && hi.is_val()) {
@ -869,7 +869,7 @@ namespace {
do { do {
found = false; found = false;
do { do {
if (!e->refined) { if (!e->refined && e->side_cond.empty()) {
auto const& lo = e->interval.lo(); auto const& lo = e->interval.lo();
auto const& hi = e->interval.hi(); auto const& hi = e->interval.hi();
if (lo.is_val() && hi.is_val()) { if (lo.is_val() && hi.is_val()) {

6
src/math/polysat/viable.h
View file

@ -188,13 +188,15 @@ namespace polysat {
/** /**
* Query for an upper bound literal for v together with justification. * Query for an upper bound literal for v together with justification.
* @return true if a non-trivial upper bound is found, return justifying constraint. * On success, the conjunction of out_c implies v <= out_hi.
* @return true if a non-trivial upper bound is found, return justifying constraints.
*/ */
bool has_upper_bound(pvar v, rational& out_hi, vector<signed_constraint>& out_c); bool has_upper_bound(pvar v, rational& out_hi, vector<signed_constraint>& out_c);
/** /**
* Query for an lower bound literal for v together with justification. * Query for an lower bound literal for v together with justification.
* @return true if a non-trivial lower bound is found, return justifying constraint. * On success, the conjunction of out_c implies v >= out_hi.
* @return true if a non-trivial lower bound is found, return justifying constraints.
*/ */
bool has_lower_bound(pvar v, rational& out_lo, vector<signed_constraint>& out_c); bool has_lower_bound(pvar v, rational& out_lo, vector<signed_constraint>& out_c);