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 very basic unit tests

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-14 05:03:44 -07:00
parent de66c12b93
commit a45687d5db
1 changed files with 47 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

55
src/test/polysat.cpp
View file

@ -12,31 +12,65 @@ namespace polysat {
struct scoped_solver : public solver_scope, public solver {
scoped_solver(): solver(stack, lim) {}
void check() {
std::cout << check_sat() << "\n";
statistics st;
collect_statistics(st);
std::cout << st << "\n";
std::cout << *this << "\n";
}
};
/**
* most basic linear equation solving.
* they should be solvable.
* they also illustrate some limitations of basic solver even if it solves them.
* Example
* the value to a + 1 = 0 is fixed at 3, there should be no search.
*/
static void test_l1() {
scoped_solver s;
auto a = s.var(s.add_var(2));
s.add_eq(a + 1);
s.check();
}
static void test_l2() {
scoped_solver s;
auto a = s.var(s.add_var(2));
auto b = s.var(s.add_var(2));
s.add_eq(2*a + b + 1);
s.add_eq(2*b + a);
s.check();
}
/**
* This one is unsat because a*a*(a*a - 1)
* is 0 for all values of a.
*/
static void test_eq1() {
static void test_p1() {
scoped_solver s;
auto a = s.var(s.add_var(2));
auto p = a*a*(a*a - 1) + 1;
s.add_eq(p);
std::cout << s.check_sat() << "\n";
s.check();
}
/**
* has solution a = 3
*/
static void test_eq2() {
static void test_p2() {
scoped_solver s;
auto a = s.var(s.add_var(2));
auto p = a*(a-1) + 2;
s.add_eq(p);
std::cout << s.check_sat() << "\n";
s.check();
}
/**
* Check unsat of:
* u = v*q + r
@ -52,7 +86,7 @@ namespace polysat {
s.add_eq(u - (v*q) - r, 0);
s.add_ult(r, u, 0);
s.add_ult(u, v*q, 0);
std::cout << s.check_sat() << "\n";
s.check();
}
/**
@ -74,7 +108,7 @@ namespace polysat {
s.add_eq(n*q2 + r2 - c*a + c*b);
s.add_ult(r2, n);
s.add_diseq(n);
std::cout << s.check_sat() << "\n";
s.check();
}
// convert assertions into internal solver state
@ -86,10 +120,15 @@ namespace polysat {
void tst_polysat() {
polysat::test_eq1();
polysat::test_eq2();
polysat::test_l1();
polysat::test_l2();
#if 0
// worry about this later
polysat::test_p1();
polysat::test_p2();
polysat::test_ineq1();
polysat::test_ineq2();
#endif
}
// TBD also add test that loads from a file and runs the polysat engine.