mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

updating tests

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-02-12 18:13:02 -08:00
parent 0fc44a43e1
commit 0879c6f052
3 changed files with 48 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
src/test/hilbert_basis.cpp
View file

@ -20,6 +20,17 @@ static vector<rational> vec(int i, int j, int k, int l) {
return nv;
}
static vector<rational> vec(int i, int j, int k, int l, int m) {
vector<rational> nv;
nv.resize(5);
nv[0] = rational(i);
nv[1] = rational(j);
nv[2] = rational(k);
nv[3] = rational(l);
nv[4] = rational(m);
return nv;
}
static vector<rational> vec(int i, int j, int k, int l, int x, int y, int z) {
vector<rational> nv;
nv.resize(7);
@ -164,6 +175,40 @@ static void tst7() {
}
// Sigma_5 table 1, Ajili, Contejean
static void tst8() {
hilbert_sl_basis hb;
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));
hb.add_le(vec( 1,-1,-3), R(-2));
saturate_basis(hb);
}
// Sigma_6 table 1, Ajili, Contejean
static void tst9() {
hilbert_sl_basis hb;
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));
saturate_basis(hb);
}
// Sigma_7 table 1, Ajili, Contejean
static void tst10() {
hilbert_sl_basis hb;
hb.add_le(vec( 1,-1,-1,-3), R(2));
hb.add_le(vec(-2, 3, 3, 5), R(3));
saturate_basis(hb);
}
// Sigma_8 table 1, Ajili, Contejean
static void tst11() {
hilbert_sl_basis hb;
hb.add_le(vec( 7,-2,11, 3, -5), R(5));
saturate_basis(hb);
}
void tst_hilbert_basis() {
std::cout << "hilbert basis test\n";
tst1();

4
src/test/matcher.cpp
View file

@ -52,7 +52,7 @@ void tst_match(ast_manager & m, app * t, app * i) {
s.display(std::cout);
// create some dummy term to test for applying the substitution.
sort_ref S( m.mk_sort(symbol("S")), m);
sort_ref S( m.mk_uninterpreted_sort(symbol("S")), m);
sort * domain[3] = {S, S, S};
func_decl_ref r( m.mk_func_decl(symbol("r"), 3, domain, S), m);
expr_ref x1( m.mk_var(0, S), m);
@ -75,7 +75,7 @@ void tst_match(ast_manager & m, app * t, app * i) {
void tst1() {
ast_manager m;
reg_decl_plugins(m);
sort_ref s( m.mk_sort(symbol("S")), m);
sort_ref s( m.mk_uninterpreted_sort(symbol("S")), m);
func_decl_ref g( m.mk_func_decl(symbol("g"), s, s), m);
func_decl_ref h( m.mk_func_decl(symbol("h"), s, s), m);
sort * domain[2] = {s, s};

2
src/test/var_subst.cpp
View file

@ -62,7 +62,7 @@ void tst_subst(ast_manager& m) {
obj_ref<var, ast_manager> x(m), y(m), z(m), u(m), v(m);
expr_ref e1(m), e2(m), e3(m);
expr_ref t1(m), t2(m), t3(m);
s = m.mk_sort(symbol("S"));
s = m.mk_uninterpreted_sort(symbol("S"));
sort* ss[2] = { s.get(), s.get() };
symbol names[2] = { symbol("y"), symbol("x") };
p = m.mk_func_decl(symbol("p"), 2, ss, m.mk_bool_sort());