From 0879c6f0529ea2156497caf3c8fc710efe2b39c0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 12 Feb 2013 18:13:02 -0800
Subject: [PATCH] updating tests

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/test/hilbert_basis.cpp | 45 ++++++++++++++++++++++++++++++++++++++
 src/test/matcher.cpp       |  4 ++--
 src/test/var_subst.cpp     |  2 +-
 3 files changed, 48 insertions(+), 3 deletions(-)

diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp
index 267ad9ae5..5edc4cf99 100644
--- a/src/test/hilbert_basis.cpp
+++ b/src/test/hilbert_basis.cpp
@@ -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();
diff --git a/src/test/matcher.cpp b/src/test/matcher.cpp
index cfbab2d3c..05d971e24 100644
--- a/src/test/matcher.cpp
+++ b/src/test/matcher.cpp
@@ -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};
diff --git a/src/test/var_subst.cpp b/src/test/var_subst.cpp
index 3e75d1527..e82c09218 100644
--- a/src/test/var_subst.cpp
+++ b/src/test/var_subst.cpp
@@ -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());