mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

add unit test based on #2658

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-25 18:07:35 -07:00
parent be99d3d450
commit 376d2c1ed4
1 changed files with 23 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/test/nlsat.cpp
View file

@ -335,6 +335,13 @@ static nlsat::literal mk_gt(nlsat::solver& s, nlsat::poly* p) {
return s.mk_ineq_literal(nlsat::atom::GT, 1, _p, is_even);
}
static nlsat::literal mk_lt(nlsat::solver& s, nlsat::poly* p) {
nlsat::poly * _p[1] = { p };
bool is_even[1] = { false };
return s.mk_ineq_literal(nlsat::atom::LT, 1, _p, is_even);
}
static nlsat::literal mk_eq(nlsat::solver& s, nlsat::poly* p) {
nlsat::poly * _p[1] = { p };
bool is_even[1] = { false };
@ -736,15 +743,28 @@ static void tst11() {
as.set(x, five);
s.set_rvalues(as);
p1 = (_x - _y);
p2 = ((_x*_x) - (_x*_y) - _z);
lits.reset();
lits.push_back(mk_gt(s, p1));
lits.push_back(mk_eq(s, p2));
project_fa(s, ex, x, 2, lits.c_ptr());
// return;
p1 = ((_x * _x) - (2 * _y * _x) - _z + (_y *_y));
p2 = _x + _y;
as.set(_x, one);
as.set(_y, zero);
as.set(_z, one);
lits.reset();
lits.push_back(mk_lt(s, p1));
lits.push_back(mk_eq(s, p2));
project_fa(s, ex, x, 2, lits.c_ptr());
return;
as.set(z, zero);
as.set(y, five);
as.set(x, five);
p1 = (_x - _y);
p2 = ((_x*_x) - (_x*_y));
lits.reset();
@ -753,6 +773,7 @@ static void tst11() {
project_fa(s, ex, x, 2, lits.c_ptr());
}
void tst_nlsat() {