mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

add find_two

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-17 19:41:09 -08:00
parent 3c035daaa6
commit 4e8bd4425f
3 changed files with 45 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -147,9 +147,15 @@ namespace polysat {
reset_cache();
if (sign)
e = m.mk_not(e);
expr* a = m.mk_const(m.mk_const_decl(symbol(dep), m.mk_bool_sort()));
s->assert_expr(e, a);
IF_VERBOSE(10, verbose_stream() << "(assert (! " << expr_ref(e, m) << " :named " << expr_ref(a, m) << "))\n");
if (dep == null_dep) {
s->assert_expr(e);
IF_VERBOSE(10, verbose_stream() << "(assert " << expr_ref(e, m) << ")\n");
}
else {
expr* a = m.mk_const(m.mk_const_decl(symbol(dep), m.mk_bool_sort()));
s->assert_expr(e, a);
IF_VERBOSE(10, verbose_stream() << "(assert (! " << expr_ref(e, m) << " :named " << expr_ref(a, m) << "))\n");
}
}
void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override {
@ -245,7 +251,7 @@ namespace polysat {
// try reducing val by setting bits to 0, starting at the msb.
for (unsigned k = bit_width; k-- > 0; ) {
if (!val.get_bit(k)) {
add_bit0(k, 0);
add_bit0(k, null_dep);
continue;
}
// try decreasing k-th bit
@ -258,9 +264,9 @@ namespace polysat {
}
pop(1);
if (result == l_true)
add_bit0(k, 0);
add_bit0(k, null_dep);
else if (result == l_false)
add_bit1(k, 0);
add_bit1(k, null_dep);
else
return false;
}
@ -287,9 +293,9 @@ namespace polysat {
}
pop(1);
if (result == l_true)
add_bit1(k, 0);
add_bit1(k, null_dep);
else if (result == l_false)
add_bit0(k, 0);
add_bit0(k, null_dep);
else
return false;
}
@ -297,6 +303,26 @@ namespace polysat {
return true;
}
bool find_two(rational& out1, rational& out2) {
out1 = model();
bool ok = true;
push();
add(m.mk_eq(mk_numeral(out1), x), true, null_dep);
switch (check()) {
case l_true:
out2 = model();
break;
case l_false:
out2 = out1;
break;
default:
ok = false;
break;
}
pop(1);
return ok;
}
std::ostream& display(std::ostream& out) const override {
return out << *s;
}

10
src/math/polysat/univariate/univariate_solver.h
View file

@ -35,6 +35,8 @@ namespace polysat {
/// e.g., the vector [ c, b, a ] represents a*x^2 + b*x + c.
using univariate = vector<rational>;
const dep_t null_dep = UINT_MAX;
virtual ~univariate_solver() = default;
virtual void push() = 0;
@ -70,6 +72,14 @@ namespace polysat {
*/
virtual bool find_max(rational& out_max) = 0;
/**
* Find up to two viable values.
*
* Precondition: check() returned l_true
* returns: true on success, false on resource out
*/
virtual bool find_two(rational& out1, rational& out2) = 0;
virtual void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
virtual void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
virtual void add_smul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;

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

@ -799,11 +799,7 @@ namespace polysat {
}
lbool viable::query_find_fallback(pvar v, univariate_solver& us, rational& lo, rational& hi) {
if (!us.find_min(lo))
return l_undef;
if (!us.find_max(hi))
return l_undef;
return l_true;
return us.find_two(lo, hi) ? l_true : l_undef;
}
lbool viable::query_min_fallback(pvar v, univariate_solver& us, rational& lo) {