mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-06 03:52:24 +00:00
Code Activity

better state

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-11-13 14:52:42 -10:00
parent f49f5376b0
commit a512005d5c
3 changed files with 260 additions and 86 deletions
Download patch file Download diff file Expand all files Collapse all files

75
src/test/nlsat.cpp
View file

@ -25,6 +25,7 @@ Notes:
#include "math/polynomial/polynomial_cache.h"
#include "util/rlimit.h"
#include <iostream>
#include <vector>
nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1,
nlsat::interval_set_ref const & s2,
@ -330,6 +331,16 @@ static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsig
std::cout << ")\n";
}
static bool literal_holds(nlsat::solver& s, nlsat::evaluator& eval, nlsat::literal l) {
if (l == nlsat::true_literal)
return true;
if (l == nlsat::false_literal)
return false;
nlsat::atom* a = s.bool_var2atom(l.var());
ENSURE(a != nullptr);
return eval.eval(a, l.sign());
}
static nlsat::literal mk_gt(nlsat::solver& s, nlsat::poly* p) {
nlsat::poly * _p[1] = { p };
bool is_even[1] = { false };
@ -349,6 +360,67 @@ static nlsat::literal mk_eq(nlsat::solver& s, nlsat::poly* p) {
return s.mk_ineq_literal(nlsat::atom::EQ, 1, _p, is_even);
}
static void set_assignment_value(nlsat::assignment& as, anum_manager& am, nlsat::var v, rational const& val) {
scoped_anum tmp(am);
am.set(tmp, val.to_mpq());
as.set(v, tmp);
}
static void tst_vandermond() {
params_ref ps;
reslimit rlim;
nlsat::solver s(rlim, ps, false);
nlsat::pmanager& pm = s.pm();
anum_manager & am = s.am();
nlsat::assignment as(am);
scoped_anum zero(am), one(am), two(am), three(am);
nlsat::explain& ex = s.get_explain();
nlsat::var x0 = s.mk_var(false);
nlsat::var x1 = s.mk_var(false);
nlsat::var x2 = s.mk_var(false);
nlsat::var x3 = s.mk_var(false);
am.set(one, 1);
am.set(two, 2);
as.set(x0, one);
as.set(x1, two);
as.set(x2, three);
polynomial_ref _x0(pm), _x1(pm), _x2(pm);
_x0 = pm.mk_polynomial(x0);
_x1 = pm.mk_polynomial(x1);
_x2 = pm.mk_polynomial(x2);
polynomial_ref x0_sq(pm), x1_sq(pm), x2_sq(pm);
x0_sq = _x0 * _x0;
x1_sq = _x1 * _x1;
x2_sq = _x2 * _x2;
polynomial_ref vandermonde_flat(pm);
vandermonde_flat =
(_x1 * x2_sq) -
(x1_sq * _x2) +
(_x0 * x1_sq) -
(x0_sq * _x1) +
(x0_sq * _x2) -
(_x0 * x2_sq);
polynomial_ref vandermonde_factored(pm);
vandermonde_factored = (_x1 - _x0) * (_x2 - _x0) * (_x2 - _x1);
std::cout << "vandermonde_factored:" << vandermonde_factored << "\n";
polynomial_ref diff(pm);
diff = vandermonde_flat - vandermonde_factored;
ENSURE(pm.is_zero(diff.get()));
pm.display(std::cout << "vandermonde(flat): ", vandermonde_flat);
std::cout << "\n";
nlsat::scoped_literal_vector lits(s);
lits.push_back(mk_gt(s, vandermonde_flat));
s.set_rvalues(as);
project(s, ex, x2, lits.size(), lits.data());
as.set(x2, (one + two)/2);
std::cout << am.eval_sign_at(vandermonde_flat, as) << "\n";
;}
static void tst6() {
params_ref ps;
reslimit rlim;
@ -726,6 +798,9 @@ void tst_nlsat_mv() {
nlsat::assignment assignment(am);
nlsat::explain& ex = s.get_explain();
tst_vandermond();
return;
// Regression: reproduce lemma 114 where main_operator adds spurious bounds.
nlsat::var x0 = s.mk_var(false);
nlsat::var x1 = s.mk_var(false);