mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

quot_rem needs additional constraint: quot <= a

Browse source
This commit is contained in:
Jakob Rath 2022-01-12 13:44:30 +01:00
parent e0e03b3fc5
commit 3895d8d6bb
2 changed files with 37 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/solver.cpp
View file

@ -132,6 +132,7 @@ namespace polysat {
add_eq(b * quot + rem - a);
add_noovfl(b, quot);
add_clause(eq(b), ult(rem, b), false);
add_ule(quot, a);
return std::tuple<pdd, pdd>(quot, rem);
}

36
src/test/polysat.cpp
View file

@ -952,6 +952,38 @@ public:
}
}
static void test_quot_rem_incomplete() {
unsigned bw = 4;
scoped_solver s(__func__);
s.set_max_conflicts(5);
auto quot = s.var(s.add_var(bw));
auto rem = s.var(s.add_var(bw));
auto a = s.value(rational(2), bw);
auto b = s.value(rational(5), bw);
// Incomplete axiomatization of quotient/remainder.
// quot_rem(2, 5) should have single solution (0, 2),
// but with the usual axioms we also get (3, 3).
s.add_eq(b * quot + rem - a);
s.add_noovfl(b, quot);
s.add_ult(rem, b);
// To force a solution that's different from the correct one.
s.add_diseq(quot - 0);
s.check();
s.expect_sat({{quot, 3}, {rem, 3}});
}
static void test_quot_rem_fixed() {
unsigned bw = 4;
scoped_solver s(__func__);
s.set_max_conflicts(5);
auto a = s.value(rational(2), bw);
auto b = s.value(rational(5), bw);
auto [quot, rem] = s.quot_rem(a, b);
s.add_diseq(quot - 0); // to force a solution that's different from the correct one
s.check();
s.expect_unsat();
}
static void test_quot_rem(unsigned bw = 32) {
scoped_solver s(__func__);
s.set_max_conflicts(5);
@ -1171,6 +1203,10 @@ public:
void tst_polysat() {
using namespace polysat;
test_polysat::test_quot_rem_incomplete();
test_polysat::test_quot_rem_fixed();
return;
test_polysat::test_band();
return;