mirror of
https://github.com/Z3Prover/z3
synced 2025-08-09 20:50:50 +00:00
resource-limit related fixes in src/test
This commit is contained in:
Christoph M. Wintersteiger
parent
e91b1e1da4
commit
c2ab9b72dc
11 changed files with 672 additions and 569 deletions
|
|
@ -12,6 +12,7 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
#include "tactic.h"
|
||||
#include "tactic2solver.h"
|
||||
#include "solver.h"
|
||||
#include "rlimit.h"
|
||||
#include <signal.h>
|
||||
#include <time.h>
|
||||
#include <sstream>
|
||||
|
|
@ -38,7 +39,7 @@ class hilbert_basis_validate {
|
|||
}
|
||||
|
||||
public:
|
||||
|
||||
|
||||
hilbert_basis_validate(ast_manager& m);
|
||||
|
||||
expr_ref mk_validate(hilbert_basis& hb);
|
||||
|
|
@ -46,7 +47,7 @@ public:
|
|||
};
|
||||
|
||||
|
||||
hilbert_basis_validate::hilbert_basis_validate(ast_manager& m):
|
||||
hilbert_basis_validate::hilbert_basis_validate(ast_manager& m):
|
||||
m(m) {
|
||||
}
|
||||
|
||||
|
|
@ -86,7 +87,7 @@ void hilbert_basis_validate::validate_solution(hilbert_basis& hb, vector<rationa
|
|||
}
|
||||
std::cout << "\n";
|
||||
std::cout << "sum: " << sum << "\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
|
||||
|
|
@ -94,7 +95,7 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
|
|||
unsigned sz = hb.get_basis_size();
|
||||
vector<rational> v;
|
||||
|
||||
// check that claimed solution really satisfies inequalities:
|
||||
// check that claimed solution really satisfies inequalities:
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
bool is_initial;
|
||||
hb.get_basis_solution(i, v, is_initial);
|
||||
|
|
@ -111,7 +112,7 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
|
|||
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) {
|
||||
bool is_initial;
|
||||
|
|
@ -169,7 +170,7 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
|
|||
}
|
||||
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;
|
||||
|
|
@ -194,7 +195,7 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
|
|||
}
|
||||
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)) {
|
||||
|
|
@ -221,7 +222,7 @@ static void display_statistics(hilbert_basis& hb) {
|
|||
}
|
||||
|
||||
static void on_ctrl_c(int) {
|
||||
signal (SIGINT, SIG_DFL);
|
||||
signal (SIGINT, SIG_DFL);
|
||||
display_statistics(*g_hb);
|
||||
raise(SIGINT);
|
||||
}
|
||||
|
|
@ -258,17 +259,17 @@ static void saturate_basis(hilbert_basis& hb) {
|
|||
lbool is_sat = hb.saturate();
|
||||
|
||||
switch(is_sat) {
|
||||
case l_true:
|
||||
std::cout << "sat\n";
|
||||
case l_true:
|
||||
std::cout << "sat\n";
|
||||
hb.display(std::cout);
|
||||
//validate_sat(hb);
|
||||
break;
|
||||
case l_false:
|
||||
std::cout << "unsat\n";
|
||||
case l_false:
|
||||
std::cout << "unsat\n";
|
||||
break;
|
||||
case l_undef:
|
||||
std::cout << "undef\n";
|
||||
break;
|
||||
case l_undef:
|
||||
std::cout << "undef\n";
|
||||
break;
|
||||
}
|
||||
display_statistics(hb);
|
||||
}
|
||||
|
|
@ -283,7 +284,8 @@ static void saturate_basis(hilbert_basis& hb) {
|
|||
static void gorrila_test(unsigned seed, unsigned n, unsigned k, unsigned bound, unsigned num_ineqs) {
|
||||
std::cout << "Gorrila test\n";
|
||||
random_gen rand(seed);
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
SASSERT(0 < bound);
|
||||
SASSERT(k <= n);
|
||||
int ibound = static_cast<int>(bound);
|
||||
|
|
@ -303,7 +305,7 @@ static void gorrila_test(unsigned seed, unsigned n, unsigned k, unsigned bound,
|
|||
}
|
||||
a0 = rational(ibound - static_cast<int>(rand(2*bound+1)));
|
||||
hb.add_ge(nv, a0);
|
||||
}
|
||||
}
|
||||
hb.display(std::cout << "Saturate\n");
|
||||
saturate_basis(hb);
|
||||
}
|
||||
|
|
@ -368,7 +370,8 @@ static vector<rational> vec(int i, int j, int k, int l, int x, int y, int z) {
|
|||
// -y + z <= 0
|
||||
|
||||
static void tst1() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_eq(vec(1,1,-2));
|
||||
hb.add_eq(vec(1,0,-1));
|
||||
hb.add_le(vec(0,1,-1));
|
||||
|
|
@ -380,7 +383,8 @@ static void tst1() {
|
|||
// 23x - 12y - 9z <= 0
|
||||
// x - 8y - 8z <= 0
|
||||
void tst2() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
|
||||
hb.add_eq(vec(-23,12,9));
|
||||
hb.add_eq(vec(-1,8,8));
|
||||
|
|
@ -391,7 +395,8 @@ void tst2() {
|
|||
// example 6, Ajili, Contenjean
|
||||
// 3x + 2y - z - 2u <= 0
|
||||
static void tst3() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_le(vec(3,2,-1,-2));
|
||||
saturate_basis(hb);
|
||||
}
|
||||
|
|
@ -400,7 +405,8 @@ static void tst3() {
|
|||
|
||||
// Sigma_1, table 1, Ajili, Contejean
|
||||
static void tst4() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_le(vec( 0,-2, 1, 3, 2,-2, 3), R(3));
|
||||
hb.add_le(vec(-1, 7, 0, 1, 3, 5,-4), R(2));
|
||||
hb.add_le(vec( 0,-1, 1,-1,-1, 0, 0), R(2));
|
||||
|
|
@ -416,7 +422,8 @@ static void tst4() {
|
|||
|
||||
// Sigma_2 table 1, Ajili, Contejean
|
||||
static void tst5() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_le(vec( 1, 2,-1, 1), R(3));
|
||||
hb.add_le(vec( 2, 4, 1, 2), R(12));
|
||||
hb.add_le(vec( 1, 4, 2, 1), R(9));
|
||||
|
|
@ -429,7 +436,8 @@ static void tst5() {
|
|||
|
||||
// Sigma_3 table 1, Ajili, Contejean
|
||||
static void tst6() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_le(vec( 4, 3, 0), R(6));
|
||||
hb.add_le(vec(-3,-4, 0), R(-1));
|
||||
hb.add_le(vec( 4, 0,-3), R(3));
|
||||
|
|
@ -441,7 +449,8 @@ static void tst6() {
|
|||
|
||||
// Sigma_4 table 1, Ajili, Contejean
|
||||
static void tst7() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
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));
|
||||
|
|
@ -454,7 +463,8 @@ static void tst7() {
|
|||
|
||||
// Sigma_5 table 1, Ajili, Contejean
|
||||
static void tst8() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_le(vec( 2, 1, 1), R(2));
|
||||
hb.add_le(vec( 1, 2, 3), R(5));
|
||||
hb.add_le(vec( 2, 2, 3), R(6));
|
||||
|
|
@ -464,7 +474,8 @@ static void tst8() {
|
|||
|
||||
// Sigma_6 table 1, Ajili, Contejean
|
||||
static void tst9() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_le(vec( 1, 2, 3), R(11));
|
||||
hb.add_le(vec( 2, 2, 5), R(13));
|
||||
hb.add_le(vec( 1,-1,-11), R(3));
|
||||
|
|
@ -473,7 +484,8 @@ static void tst9() {
|
|||
|
||||
// Sigma_7 table 1, Ajili, Contejean
|
||||
static void tst10() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_le(vec( 1,-1,-1,-3), R(2));
|
||||
hb.add_le(vec(-2, 3, 3,-5), R(3));
|
||||
saturate_basis(hb);
|
||||
|
|
@ -481,14 +493,16 @@ static void tst10() {
|
|||
|
||||
// Sigma_8 table 1, Ajili, Contejean
|
||||
static void tst11() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_le(vec( 7,-2,11, 3, -5), R(5));
|
||||
saturate_basis(hb);
|
||||
}
|
||||
|
||||
// Sigma_9 table 1, Ajili, Contejean
|
||||
static void tst12() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_eq(vec( 1,-2,-3,4), R(0));
|
||||
hb.add_le(vec(100,45,-78,-67), R(0));
|
||||
saturate_basis(hb);
|
||||
|
|
@ -496,34 +510,39 @@ static void tst12() {
|
|||
|
||||
// Sigma_10 table 1, Ajili, Contejean
|
||||
static void tst13() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
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;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
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;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_le(vec(1, 0), R(1));
|
||||
hb.add_le(vec(0, 1), R(1));
|
||||
saturate_basis(hb);
|
||||
}
|
||||
|
||||
static void tst16() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_le(vec(1, 0), R(100));
|
||||
saturate_basis(hb);
|
||||
}
|
||||
|
||||
static void tst17() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_eq(vec(1, 0), R(0));
|
||||
hb.add_eq(vec(-1, 0), R(0));
|
||||
hb.add_eq(vec(0, 2), R(0));
|
||||
|
|
@ -533,26 +552,29 @@ static void tst17() {
|
|||
}
|
||||
|
||||
static void tst18() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_eq(vec(0, 1), R(0));
|
||||
hb.add_eq(vec(1, -1), R(2));
|
||||
saturate_basis(hb);
|
||||
saturate_basis(hb);
|
||||
}
|
||||
|
||||
static void tst19() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
hb.add_eq(vec(0, 1, 0), R(0));
|
||||
hb.add_eq(vec(1, -1, 0), R(2));
|
||||
saturate_basis(hb);
|
||||
saturate_basis(hb);
|
||||
}
|
||||
|
||||
static void test_A_5_5_3() {
|
||||
hilbert_basis hb;
|
||||
reslimit rl;
|
||||
hilbert_basis hb(rl);
|
||||
for (unsigned i = 0; i < 15; ++i) {
|
||||
vector<rational> v;
|
||||
for (unsigned j = 0; j < 5; ++j) {
|
||||
for (unsigned k = 0; k < 15; ++k) {
|
||||
v.push_back(rational(k == i));
|
||||
v.push_back(rational(k == i));
|
||||
}
|
||||
}
|
||||
hb.add_ge(v, R(0));
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue