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

monotonicity unit tests (#5202)

Browse source 
* monotonicity unit tests

* indentation
This commit is contained in:
alexandernutz 2021-04-20 18:09:17 +02:00 • committed by GitHub
parent 4da1b7b03c
commit bc695a5a97
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 102 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

102
src/test/polysat.cpp
View file

@ -141,6 +141,108 @@ namespace polysat {
s.check();
}
/**
* Monotonicity example from certora (1)
* expected: unsat
*/
static void test_monot1() {
scoped_solver s;
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, tb2);
s.check();
}
/**
* Monotonicity example from certora (2)
* expected: unsat
*
* only difference to (1) is the inequality right before the check
*/
static void test_monot2() {
scoped_solver s;
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();
}
// 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)
// static void test_mixed_vars() {