Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat

src/math/polysat/polysat.cpp

@@ -129,6 +129,14 @@ namespace polysat {
         // save for later
     }
 
+    void solver::add_ult(pdd const& p, pdd const& q, unsigned dep) {
+        // save for later
+    }
+
+    void solver::add_slt(pdd const& p, pdd const& q, unsigned dep) {
+        // save for later
+    }
+
     void solver::assign(unsigned var, unsigned index, bool value, unsigned dep) {
         m_viable[var] &= value ? m_bdd.mk_var(index) : m_bdd.mk_nvar(index);
         m_trail.push(vector_value_trail<u_dependency*, false>(m_vdeps, var));

src/math/polysat/polysat.h

@@ -182,6 +182,7 @@ namespace polysat {
          * by pushing an undo action on the trail stack.
          */
         solver(trail_stack& s);
+
         ~solver();
 
         /**
@@ -206,10 +207,13 @@ namespace polysat {
          * Each constraint is tracked by a dependency.
          * assign sets the 'index'th bit of var.
          */
-        void add_eq(pdd const& p, unsigned dep);
-        void add_diseq(pdd const& p, unsigned dep);
-        void add_ule(pdd const& p, pdd const& q, unsigned dep);
-        void add_sle(pdd const& p, pdd const& q, unsigned dep);
+        void add_eq(pdd const& p, unsigned dep = 0);
+        void add_diseq(pdd const& p, unsigned dep = 0);
+        void add_ule(pdd const& p, pdd const& q, unsigned dep = 0);
+        void add_ult(pdd const& p, pdd const& q, unsigned dep = 0);
+        void add_sle(pdd const& p, pdd const& q, unsigned dep = 0);
+        void add_slt(pdd const& p, pdd const& q, unsigned dep = 0);
+        
         void assign(unsigned var, unsigned index, bool value, unsigned dep);        
 
         /**

src/smt/theory_seq.cpp

@@ -2731,7 +2731,7 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
 }
 
 void theory_seq::add_axiom(literal_vector & lits) {
-    TRACE("seq", ctx.display_literals_verbose(tout << "assert:", lits) << "\n";);
+    TRACE("seq", ctx.display_literals_smt2(tout << "assert:", lits) << "\n";);
     for (literal lit : lits)
         ctx.mark_as_relevant(lit);
 

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";
 }