add testing stubs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/test/CMakeLists.txt

@@ -3,7 +3,7 @@ add_subdirectory(lp)
 ################################################################################
 # z3-test executable
 ################################################################################
-set(z3_test_deps api fuzzing simplex)
+set(z3_test_deps api fuzzing simplex polysat)
 z3_expand_dependencies(z3_test_expanded_deps ${z3_test_deps})
 set (z3_test_extra_object_files "")
 foreach (component ${z3_test_expanded_deps})

src/test/main.cpp

@@ -263,4 +263,5 @@ int main(int argc, char ** argv) {
     //TST_ARGV(hs);
     TST(finder);
     TST(polysat);
+    TST_ARGV(polysat_argv);
 }

src/test/polysat.cpp

@@ -1,15 +1,107 @@
 #include "math/polysat/polysat.h"
+#include "ast/ast.h"
 
 namespace polysat {
     // test resolve, factoring routines
     // auxiliary 
-    static void test1() {
+
+    
+    /**
+     * This one is unsat because a*a*(a*a - 1)
+     * is 0 for all values of a.
+     */
+    static void test_eq1() {
+        trail_stack stack;
+        solver s(stack);
+        auto a = s.var(s.add_var(2));
+        auto p = a*a*(a*a - 1) + 1;
+        s.add_eq(p);
+        std::cout << s.check_sat() << "\n";
+    }
+
+    /**
+     * has solution a = 3
+     */
+    static void test_eq2() {
+        trail_stack stack;
+        solver s(stack);
+        auto a = s.var(s.add_var(2));
+        auto p = a*(a-1) + 2;
+        s.add_eq(p);
+        std::cout << s.check_sat() << "\n";
+    }
+
+    /**
+     * Check unsat of:
+     * u = v*q + r
+     * r < u
+     * v*q > u
+     */
+    static void test_ineq1() {
+        trail_stack stack;
+        solver s(stack);
+        auto u = s.var(s.add_var(5));
+        auto v = s.var(s.add_var(5));
+        auto q = s.var(s.add_var(5));
+        auto r = s.var(s.add_var(5));
+        s.add_eq(u - (v*q) - r, 0);
+        s.add_ult(r, u, 0);
+        s.add_ult(u, v*q, 0);
+        std::cout << s.check_sat() << "\n";        
+    }
+
+    /**
+     * Check unsat of:
+     * n*q1 = a - b
+     * n*q2 + r2 = c*a - c*b
+     * n > r2 > 0
+     */
+    static void test_ineq2() {
+        trail_stack stack;
+        solver s(stack);
+        auto n = s.var(s.add_var(5));
+        auto q1 = s.var(s.add_var(5));
+        auto a = s.var(s.add_var(5));
+        auto b = s.var(s.add_var(5));
+        auto c = s.var(s.add_var(5));
+        auto q2 = s.var(s.add_var(5));
+        auto r2 = s.var(s.add_var(5));
+        s.add_eq(n*q1 - a + b);
+        s.add_eq(n*q2 + r2 - c*a + c*b);
+        s.add_ult(r2, n);
+        s.add_diseq(n);
+        std::cout << s.check_sat() << "\n";
+    }
+
+    // convert assertions into internal solver state
+    // support small grammar of formulas.
+    void internalize(solver& s, expr_ref_vector& fmls) {
 
     }
 }
 
-// also add test that loads from a file and runs the polysat engine.
 
 void tst_polysat() {
-    polysat::test1();
+    polysat::test_eq1();
+    polysat::test_eq2();
+    polysat::test_ineq1();
+    polysat::test_ineq2();
+}
+
+// TBD also add test that loads from a file and runs the polysat engine.
+// sketch follows below:
+
+void tst_polysat_argv(char** argv, int argc, int& i) {
+    // set up SMT2 parser to extract assertions
+    // assume they are simple bit-vector equations (and inequations)
+    // convert to solver state.
+    // std::ifstream is(argv[0]);
+    // cmd_context ctx(false, &m);
+    // ctx.set_ignore_check(true);
+    // VERIFY(parse_smt2_commands(ctx, is));
+    // auto fmls = ctx.assertions();
+    // trail_stack stack;
+    // solver s(stack);
+    // polysat::internalize(s, fmls);
+    // std::cout << s.check() << "\n";
 }