mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-07 08:21:56 +00:00
Code Activity

make the two monotonicity tests into one using push/pop; fix division modelling (#5220)

Browse source 
* make the two monotonicity tests into one using push/pop

* whitespace...

* proper division modelling for monotonicity test -- overflow checks still missing, though

* double bitwidth for overflow checking in monotonicity example
This commit is contained in:
alexandernutz 2021-05-20 19:00:13 +02:00 • committed by GitHub
parent 973a32a015
commit 8a5addd891
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 41 additions and 60 deletions
Download patch file Download diff file Expand all files Collapse all files

99
src/test/polysat.cpp
View file

@ -346,108 +346,89 @@ namespace polysat {
/** /**
* Monotonicity example from certora (1) * Monotonicity example from certora
* expected: unsat
*/ */
static void test_monot1() { static void test_monot() {
scoped_solver s(__func__); scoped_solver s(__func__);
auto bw = 5;
auto baseBw = 5;
auto max_int_const = 31; // (2^5 - 1) -- change this if you change baseBw
auto bw = 2 * baseBw;
auto max_int = s.var(s.add_var(bw));
s.add_eq(max_int - max_int_const);
auto tb1 = s.var(s.add_var(bw)); auto tb1 = s.var(s.add_var(bw));
s.add_ule(tb1, max_int);
auto tb2 = s.var(s.add_var(bw)); auto tb2 = s.var(s.add_var(bw));
s.add_ule(tb2, max_int);
auto a = s.var(s.add_var(bw)); auto a = s.var(s.add_var(bw));
s.add_ule(a, max_int);
auto v = s.var(s.add_var(bw)); auto v = s.var(s.add_var(bw));
s.add_ule(v, max_int);
auto base1 = s.var(s.add_var(bw)); auto base1 = s.var(s.add_var(bw));
s.add_ule(base1, max_int);
auto base2 = s.var(s.add_var(bw)); auto base2 = s.var(s.add_var(bw));
s.add_ule(base2, max_int);
auto elastic1 = s.var(s.add_var(bw)); auto elastic1 = s.var(s.add_var(bw));
s.add_ule(elastic1, max_int);
auto elastic2 = s.var(s.add_var(bw)); auto elastic2 = s.var(s.add_var(bw));
s.add_ule(elastic2, max_int);
auto err = s.var(s.add_var(bw)); auto err = s.var(s.add_var(bw));
s.add_ule(err, max_int);
auto zero = a - a;
auto rem1 = s.var(s.add_var(bw)); auto rem1 = s.var(s.add_var(bw));
auto quot2 = s.var(s.add_var(bw)); auto quot2 = s.var(s.add_var(bw));
s.add_ule(quot2, max_int);
auto rem2 = s.var(s.add_var(bw)); auto rem2 = s.var(s.add_var(bw));
auto rem3 = s.var(s.add_var(bw)); auto rem3 = s.var(s.add_var(bw));
auto quot4 = s.var(s.add_var(bw)); auto quot4 = s.var(s.add_var(bw));
s.add_ule(quot4, max_int);
auto rem4 = s.var(s.add_var(bw)); auto rem4 = s.var(s.add_var(bw));
s.add_diseq(elastic1); s.add_diseq(elastic1);
// tb1 = (v * base1) / elastic1; // division: tb1 = (v * base1) / elastic1;
s.add_eq((tb1 * elastic1) + rem1 - (v * base1)); s.add_eq((tb1 * elastic1) + rem1 - (v * base1));
s.add_ult(rem1, elastic1);
s.add_ule((tb1 * elastic1), max_int);
// quot2 = (a * base1) / elastic1 // division: quot2 = (a * base1) / elastic1
s.add_eq((quot2 * elastic1) + rem2 - (a * base1)); s.add_eq((quot2 * elastic1) + rem2 - (a * base1));
s.add_ult(rem2, elastic1);
s.add_ule((quot2 * elastic1), max_int);
s.add_eq(base1 + quot2 - base2); s.add_eq(base1 + quot2 - base2);
s.add_eq(elastic1 + a - elastic2); s.add_eq(elastic1 + a - elastic2);
// tb2 = ((v * base2) / elastic2); // division: tb2 = ((v * base2) / elastic2);
s.add_eq((tb2 * elastic2) + rem3 - (v * base2)); s.add_eq((tb2 * elastic2) + rem3 - (v * base2));
s.add_ult(rem3, elastic2);
s.add_ule((tb2 * elastic2), max_int);
// quot4 = v / (elastic1 + a); // division: quot4 = v / elastic2;
s.add_eq((quot4 * (elastic1 + a)) + rem4 - v); s.add_eq((quot4 * elastic2) + rem4 - v);
s.add_ult(rem4, elastic2);
s.add_ule((quot4 * elastic2), max_int);
s.add_eq(quot4 + 1 - err); s.add_eq(quot4 + 1 - err);
s.push();
s.add_ult(tb1, tb2); s.add_ult(tb1, tb2);
s.check(); s.check();
s.expect_unsat(); s.expect_unsat();
} s.pop();
/** s.push();
* Monotonicity example from certora (2) s.add_ult(tb2 + err, tb1);
* expected: unsat
*
* only difference to (1) is the inequality right before the check
*/
static void test_monot2() {
scoped_solver s(__func__);
auto bw = 5;
auto tb1 = s.var(s.add_var(bw));
auto tb2 = s.var(s.add_var(bw));
auto a = s.var(s.add_var(bw));
auto v = s.var(s.add_var(bw));
auto base1 = s.var(s.add_var(bw));
auto base2 = s.var(s.add_var(bw));
auto elastic1 = s.var(s.add_var(bw));
auto elastic2 = s.var(s.add_var(bw));
auto err = s.var(s.add_var(bw));
auto rem1 = s.var(s.add_var(bw));
auto quot2 = s.var(s.add_var(bw));
auto rem2 = s.var(s.add_var(bw));
auto rem3 = s.var(s.add_var(bw));
auto quot4 = s.var(s.add_var(bw));
auto rem4 = s.var(s.add_var(bw));
s.add_diseq(elastic1);
// tb1 = (v * base1) / elastic1;
s.add_eq((tb1 * elastic1) + rem1 - (v * base1));
// quot2 = (a * base1) / elastic1
s.add_eq((quot2 * elastic1) + rem2 - (a * base1));
s.add_eq(base1 + quot2 - base2);
s.add_eq(elastic1 + a - elastic2);
// tb2 = ((v * base2) / elastic2);
s.add_eq((tb2 * elastic2) + rem3 - (v * base2));
// quot4 = v / (elastic1 + a);
s.add_eq((quot4 * (elastic1 + a)) + rem4 - v);
s.add_eq(quot4 + 1 - err);
s.add_ult(tb1 + err, tb2);
s.check(); s.check();
s.expect_unsat(); s.expect_unsat();
s.pop();
} }
// Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases // Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases
// NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later) // NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later)
// static void test_mixed_vars() { // static void test_mixed_vars() {