mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
move validation code to unit test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
f46c7f9bd9
commit
47342e5d0c
3 changed files with 185 additions and 237 deletions
|
|
@ -1,14 +1,180 @@
|
|||
#include "hilbert_basis.h"
|
||||
#include "hilbert_basis_validate.h"
|
||||
#include "ast_pp.h"
|
||||
#include "reg_decl_plugins.h"
|
||||
#include "arith_decl_plugin.h"
|
||||
#include "quant_tactics.h"
|
||||
#include "tactic.h"
|
||||
#include "tactic2solver.h"
|
||||
#include "solver.h"
|
||||
#include <signal.h>
|
||||
#include <time.h>
|
||||
#include <sstream>
|
||||
|
||||
|
||||
class hilbert_basis_validate {
|
||||
ast_manager& m;
|
||||
|
||||
void validate_solution(hilbert_basis& hb, vector<rational> const& v, bool is_initial);
|
||||
|
||||
public:
|
||||
|
||||
hilbert_basis_validate(ast_manager& m);
|
||||
|
||||
expr_ref mk_validate(hilbert_basis& hb);
|
||||
|
||||
};
|
||||
|
||||
|
||||
hilbert_basis_validate::hilbert_basis_validate(ast_manager& m):
|
||||
m(m) {
|
||||
}
|
||||
|
||||
void hilbert_basis_validate::validate_solution(hilbert_basis& hb, vector<rational> const& v, bool is_initial) {
|
||||
unsigned sz = hb.get_num_ineqs();
|
||||
rational bound;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
bool is_eq;
|
||||
vector<rational> w;
|
||||
hb.get_ge(i, w, bound, is_eq);
|
||||
rational sum(0);
|
||||
for (unsigned j = 0; j < v.size(); ++j) {
|
||||
sum += w[j]*v[j];
|
||||
}
|
||||
if (bound > sum ||
|
||||
(is_eq && bound != sum)) {
|
||||
// validation failed.
|
||||
std::cout << "validation failed for inequality\n";
|
||||
for (unsigned j = 0; j < v.size(); ++j) {
|
||||
std::cout << v[j] << " ";
|
||||
}
|
||||
std::cout << "\n";
|
||||
for (unsigned j = 0; j < w.size(); ++j) {
|
||||
std::cout << w[j] << " ";
|
||||
}
|
||||
std::cout << (is_eq?" = ":" >= ") << bound << "\n";
|
||||
std::cout << "is initial: " << (is_initial?"true":"false") << "\n";
|
||||
std::cout << "sum: " << sum << "\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
|
||||
arith_util a(m);
|
||||
unsigned sz = hb.get_basis_size();
|
||||
vector<rational> v;
|
||||
bool is_initial;
|
||||
|
||||
// check that claimed solution really satisfies inequalities:
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
hb.get_basis_solution(i, v, is_initial);
|
||||
validate_solution(hb, v, is_initial);
|
||||
}
|
||||
|
||||
// check that solutions satisfying inequalities are in solution.
|
||||
// build a formula that says solutions to linear inequalities
|
||||
// coincide with linear combinations of basis.
|
||||
vector<expr_ref_vector> offsets, increments;
|
||||
expr_ref_vector xs(m), vars(m);
|
||||
expr_ref var(m);
|
||||
svector<symbol> names;
|
||||
sort_ref_vector sorts(m);
|
||||
|
||||
#define mk_mul(_r,_x) (_r.is_one()?((expr*)_x):((expr*)a.mk_mul(a.mk_numeral(_r,true),_x)))
|
||||
|
||||
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
hb.get_basis_solution(i, v, is_initial);
|
||||
|
||||
for (unsigned j = 0; xs.size() < v.size(); ++j) {
|
||||
xs.push_back(m.mk_fresh_const("x", a.mk_int()));
|
||||
}
|
||||
|
||||
if (is_initial) {
|
||||
expr_ref_vector tmp(m);
|
||||
for (unsigned j = 0; j < v.size(); ++j) {
|
||||
tmp.push_back(a.mk_numeral(v[j], true));
|
||||
}
|
||||
offsets.push_back(tmp);
|
||||
}
|
||||
else {
|
||||
var = m.mk_var(vars.size(), a.mk_int());
|
||||
expr_ref_vector tmp(m);
|
||||
for (unsigned j = 0; j < v.size(); ++j) {
|
||||
tmp.push_back(mk_mul(v[j], var));
|
||||
}
|
||||
std::stringstream name;
|
||||
name << "u" << i;
|
||||
increments.push_back(tmp);
|
||||
vars.push_back(var);
|
||||
names.push_back(symbol(name.str().c_str()));
|
||||
sorts.push_back(a.mk_int());
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref_vector bounds(m);
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
bounds.push_back(a.mk_ge(vars[i].get(), a.mk_numeral(rational(0), true)));
|
||||
}
|
||||
expr_ref_vector fmls(m);
|
||||
expr_ref fml(m), fml1(m), fml2(m);
|
||||
for (unsigned i = 0; i < offsets.size(); ++i) {
|
||||
expr_ref_vector eqs(m);
|
||||
eqs.append(bounds);
|
||||
for (unsigned j = 0; j < xs.size(); ++j) {
|
||||
expr_ref_vector sum(m);
|
||||
sum.push_back(offsets[i][j].get());
|
||||
for (unsigned k = 0; k < increments.size(); ++k) {
|
||||
sum.push_back(increments[k][j].get());
|
||||
}
|
||||
eqs.push_back(m.mk_eq(xs[j].get(), a.mk_add(sum.size(), sum.c_ptr())));
|
||||
}
|
||||
fml = m.mk_and(eqs.size(), eqs.c_ptr());
|
||||
if (!names.empty()) {
|
||||
fml = m.mk_exists(names.size(), sorts.c_ptr(), names.c_ptr(), fml);
|
||||
}
|
||||
fmls.push_back(fml);
|
||||
}
|
||||
fml1 = m.mk_or(fmls.size(), fmls.c_ptr());
|
||||
fmls.reset();
|
||||
|
||||
sz = hb.get_num_ineqs();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
bool is_eq;
|
||||
vector<rational> w;
|
||||
rational bound;
|
||||
hb.get_ge(i, w, bound, is_eq);
|
||||
expr_ref_vector sum(m);
|
||||
for (unsigned j = 0; j < w.size(); ++j) {
|
||||
if (!w[j].is_zero()) {
|
||||
sum.push_back(mk_mul(w[j], xs[j].get()));
|
||||
}
|
||||
}
|
||||
expr_ref lhs(m), rhs(m);
|
||||
lhs = a.mk_add(sum.size(), sum.c_ptr());
|
||||
rhs = a.mk_numeral(bound, true);
|
||||
if (is_eq) {
|
||||
fmls.push_back(a.mk_eq(lhs, rhs));
|
||||
}
|
||||
else {
|
||||
fmls.push_back(a.mk_ge(lhs, rhs));
|
||||
}
|
||||
}
|
||||
fml2 = m.mk_and(fmls.size(), fmls.c_ptr());
|
||||
fml = m.mk_eq(fml1, fml2);
|
||||
|
||||
bounds.reset();
|
||||
for (unsigned i = 0; i < xs.size(); ++i) {
|
||||
if (!hb.get_is_int(i)) {
|
||||
bounds.push_back(a.mk_ge(xs[i].get(), a.mk_numeral(rational(0), true)));
|
||||
}
|
||||
}
|
||||
if (!bounds.empty()) {
|
||||
fml = m.mk_implies(m.mk_and(bounds.size(), bounds.c_ptr()), fml);
|
||||
}
|
||||
return fml;
|
||||
|
||||
}
|
||||
|
||||
#include<signal.h>
|
||||
#include<time.h>
|
||||
|
||||
hilbert_basis* g_hb = 0;
|
||||
static double g_start_time;
|
||||
|
|
@ -236,6 +402,7 @@ static void tst6() {
|
|||
// Sigma_4 table 1, Ajili, Contejean
|
||||
static void tst7() {
|
||||
hilbert_basis hb;
|
||||
hb.add_eq(vec( 1, 1, 1, 0), R(5));
|
||||
hb.add_le(vec( 2, 1, 0, 1), R(6));
|
||||
hb.add_le(vec( 1, 2, 1, 1), R(7));
|
||||
hb.add_le(vec( 1, 3,-1, 2), R(8));
|
||||
|
|
@ -268,7 +435,7 @@ static void tst9() {
|
|||
static void tst10() {
|
||||
hilbert_basis hb;
|
||||
hb.add_le(vec( 1,-1,-1,-3), R(2));
|
||||
hb.add_le(vec(-2, 3, 3, 5), R(3));
|
||||
hb.add_le(vec(-2, 3, 3,-5), R(3));
|
||||
saturate_basis(hb);
|
||||
}
|
||||
|
||||
|
|
@ -279,15 +446,8 @@ static void tst11() {
|
|||
saturate_basis(hb);
|
||||
}
|
||||
|
||||
static void tst12() {
|
||||
hilbert_basis hb;
|
||||
hb.add_le(vec(1, 0), R(1));
|
||||
hb.add_le(vec(0, 1), R(1));
|
||||
saturate_basis(hb);
|
||||
}
|
||||
|
||||
// Sigma_9 table 1, Ajili, Contejean
|
||||
static void tst13() {
|
||||
static void tst12() {
|
||||
hilbert_basis hb;
|
||||
hb.add_eq(vec( 1,-2,-4,4), R(0));
|
||||
hb.add_le(vec(100,45,-78,-67), R(0));
|
||||
|
|
@ -295,17 +455,25 @@ static void tst13() {
|
|||
}
|
||||
|
||||
// Sigma_10 table 1, Ajili, Contejean
|
||||
static void tst14() {
|
||||
static void tst13() {
|
||||
hilbert_basis hb;
|
||||
hb.add_le(vec( 23, -56, -34, 12, 11), R(0));
|
||||
saturate_basis(hb);
|
||||
}
|
||||
|
||||
// Sigma_11 table 1, Ajili, Contejean
|
||||
static void tst14() {
|
||||
hilbert_basis hb;
|
||||
hb.add_eq(vec(1, 0, -4, 8), R(2));
|
||||
hb.add_le(vec(12,19,-11,7), R(-7));
|
||||
saturate_basis(hb);
|
||||
}
|
||||
|
||||
static void tst15() {
|
||||
// hilbert_basis hb;
|
||||
// hb.add_le(vec( 23, -56, -34, 12, 11), R(0));
|
||||
// saturate_basis(hb);
|
||||
hilbert_basis hb;
|
||||
hb.add_le(vec(1, 0), R(1));
|
||||
hb.add_le(vec(0, 1), R(1));
|
||||
saturate_basis(hb);
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -336,5 +504,6 @@ void tst_hilbert_basis() {
|
|||
}
|
||||
else {
|
||||
gorrila_test(0, 10, 7, 20, 11);
|
||||
tst4();
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue