mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

unit test for #2650

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-24 10:32:56 -07:00
parent 8125fb134f
commit 60dde9f3d5
2 changed files with 72 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/nlsat/nlsat_explain.cpp
View file

@ -707,15 +707,14 @@ namespace nlsat {
m_result = nullptr;
}
void add_root_literal(atom::kind k, var y, unsigned i, poly * p) {
polynomial_ref pr(p, m_pm);
TRACE("nlsat_explain",
display(tout << "x" << y << " " << k << "[" << i << "](", pr); tout << ")\n";);
if (!mk_linear_root(k, y, i, p) &&
//!mk_plinear_root(k, y, i, p) &&
!mk_quadratic_root(k, y, i, p)&&
true) {
!mk_quadratic_root(k, y, i, p)) {
bool_var b = m_solver.mk_root_atom(k, y, i, p);
literal l(b, true);
TRACE("nlsat_explain", tout << "adding literal\n"; display(tout, l); tout << "\n";);
@ -726,7 +725,7 @@ namespace nlsat {
/**
* literal can be expressed using a linear ineq_atom
*/
bool mk_linear_root(atom::kind k, var y, unsigned i, poly * p) {
bool mk_linear_root(atom::kind k, var y, unsigned i, poly * p) {
scoped_mpz c(m_pm.m());
if (m_pm.degree(p, y) == 1 && m_pm.const_coeff(p, y, 1, c)) {
SASSERT(!m_pm.m().is_zero(c));
@ -949,11 +948,9 @@ namespace nlsat {
}
if (!lower_inf) {
TRACE("nlsat_explain", tout << "lower_inf: " << lower_inf << " upper_inf: " << upper_inf << " " << p_lower << "\n";);
add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower);
}
if (!upper_inf) {
TRACE("nlsat_explain", tout << "lower_inf: " << lower_inf << " upper_inf: " << upper_inf << " " << p_upper << "\n";);
add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, i_upper, p_upper);
}
}
@ -1475,7 +1472,11 @@ namespace nlsat {
void operator()(unsigned num, literal const * ls, scoped_literal_vector & result) {
SASSERT(check_already_added());
SASSERT(num > 0);
TRACE("nlsat_explain", tout << "[explain] set of literals is infeasible in the current interpretation\n"; display(tout, num, ls) << "\n";);
TRACE("nlsat_explain",
tout << "[explain] set of literals is infeasible in the current interpretation\n";
display(tout, num, ls) << "\n";
m_assignment.display(tout);
);
m_result = &result;
process(num, ls);
reset_already_added();

63
src/test/nlsat.cpp
View file

@ -315,6 +315,20 @@ static void project(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned
std::cout << "\n";
}
static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) {
std::cout << "Project ";
nlsat::scoped_literal_vector result(s);
ex(num, lits, result);
std::cout << "(or";
for (auto l : result) {
s.display(std::cout << " ", l);
}
for (unsigned i = 0; i < num; ++i) {
s.display(std::cout << " ", ~lits[i]);
}
std::cout << ")\n";
}
static nlsat::literal mk_gt(nlsat::solver& s, nlsat::poly* p) {
nlsat::poly * _p[1] = { p };
bool is_even[1] = { false };
@ -695,7 +709,56 @@ static void tst10() {
std::cout << "\n";
}
static void tst11() {
params_ref ps;
reslimit rlim;
nlsat::solver s(rlim, ps, false);
anum_manager & am = s.am();
nlsat::pmanager & pm = s.pm();
nlsat::assignment as(am);
nlsat::explain& ex = s.get_explain();
nlsat::var x, y, z;
y = s.mk_var(false);
z = s.mk_var(false);
x = s.mk_var(false);
polynomial_ref p1(pm), p2(pm), _x(pm), _y(pm), _z(pm);
_x = pm.mk_polynomial(x);
_y = pm.mk_polynomial(y);
_z = pm.mk_polynomial(z);
nlsat::scoped_literal_vector lits(s);
scoped_anum zero(am), one(am), five(am);
am.set(zero, 0);
am.set(one, 1);
am.set(five, 5);
as.set(z, zero);
as.set(y, five);
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 - _y);
p2 = ((_x*_x) - (_x*_y));
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());
}
void tst_nlsat() {
tst11();
std::cout << "------------------\n";
return;
tst10();
std::cout << "------------------\n";
tst9();