testing qe_arith

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

src/qe/qe_arith.cpp

@@ -67,7 +67,7 @@ namespace qe {
                 ts.push_back(a.mk_numeral(mul*mul1, m.get_sort(t)));
             }
             else if ((*m_var)(t)) {
-                IF_VERBOSE(1, verbose_stream() << mk_pp(t, m) << "\n";);
+                IF_VERBOSE(1, verbose_stream() << "can't project:" << mk_pp(t, m) << "\n";);
                 throw cant_project();
             }
             else if (mul.is_one()) {
@@ -111,6 +111,7 @@ namespace qe {
                 is_strict = false;
             }            
             else {
+                IF_VERBOSE(1, verbose_stream() << "can't project:" << mk_pp(lit, m) << "\n";);
                 throw cant_project();
             }
             if (ts.empty()) {
@@ -125,6 +126,9 @@ namespace qe {
         void project(model& model, expr_ref_vector& lits) {
             unsigned num_pos = 0;
             unsigned num_neg = 0;
+            m_ineq_terms.reset();
+            m_ineq_coeffs.reset();
+            m_ineq_strict.reset();
             expr_ref_vector new_lits(m);
             for (unsigned i = 0; i < lits.size(); ++i) {
                 rational c(0);
@@ -134,12 +138,16 @@ namespace qe {
                     m_ineq_coeffs.push_back(c);
                     m_ineq_terms.push_back(t);
                     m_ineq_strict.push_back(is_strict);
-                    if (c.is_pos()) {
+                    if (c.is_zero()) {
+                        m_rw(lits[i].get(), t);
+                        new_lits.push_back(t);
+                    }
+                    else if (c.is_pos()) {
                         ++num_pos;
                     }
                     else {
                         ++num_neg;
-                    }
+                    }                    
                 }
                 else {
                     new_lits.push_back(lits[i].get());
@@ -208,14 +216,15 @@ namespace qe {
             expr_ref as = mk_mul(abs(ac), s);
             expr_ref ts = mk_add(bt, as);
             expr*    z  = a.mk_numeral(rational(0), m.get_sort(t));
-            expr_ref result(m);
+            expr_ref result1(m), result2(m);
             if (m_ineq_strict[i] || m_ineq_strict[j]) {
-                result = a.mk_lt(ts, z);
+                result1 = a.mk_lt(ts, z);
             }
             else {
-                result = a.mk_le(ts, z);
+                result1 = a.mk_le(ts, z);
             }
-            return result;
+            m_rw(result1, result2);
+            return result2;
         }
 
         // ax + t <= 0
@@ -232,12 +241,15 @@ namespace qe {
             expr* s = m_ineq_terms[j].get();
             expr_ref bt = mk_mul(abs(bc), t);
             expr_ref as = mk_mul(abs(ac), s);
+            expr_ref result1(m), result2(m);
             if (m_ineq_strict[j] && !m_ineq_strict[i]) {
-                return expr_ref(a.mk_lt(bt, as), m);
+                result1 = a.mk_lt(bt, as);
             }
             else {
-                return expr_ref(a.mk_le(bt, as), m);
+                result1 = a.mk_le(bt, as);
             }
+            m_rw(result1, result2);
+            return result2;
         }
 
 
@@ -257,20 +269,23 @@ namespace qe {
             app_ref_vector new_vars(m);
             expr_ref_vector result(lits);
             for (unsigned i = 0; i < vars.size(); ++i) {
-                m_var = alloc(contains_app, m, vars[i].get());
+                app* v = vars[i].get();
+                m_var = alloc(contains_app, m, v);
                 try {
                     project(model, result);
+                    TRACE("qe", tout << "projected: " << mk_pp(v, m) << " ";
+                          for (unsigned i = 0; i < result.size(); ++i) {
+                              tout << mk_pp(result[i].get(), m) << "\n";
+                          });
                 }
                 catch (cant_project) {
-                    new_vars.push_back(vars[i].get());
+                    IF_VERBOSE(1, verbose_stream() << "can't project:" << mk_pp(v, m) << "\n";);
+                    new_vars.push_back(v);
                 }
             }
             vars.reset();
             vars.append(new_vars);
-            expr_ref res1(m);
+            return qe::mk_and(result);
-            expr_ref tmp = qe::mk_and(result);
-            m_rw(tmp, res1);
-            return res1;
         }  
     };
 
@@ -280,4 +295,12 @@ namespace qe {
         return ap(model, vars, lits);
     }
 
+    expr_ref arith_project(model& model, app_ref_vector& vars, expr* fml) {
+        ast_manager& m = vars.get_manager();
+        arith_project_util ap(m);
+        expr_ref_vector lits(m);
+        qe::flatten_and(fml, lits);
+        return ap(model, vars, lits);
+    }
+
 }

src/qe/qe_arith.h

@@ -11,6 +11,8 @@ namespace qe {
        return vector of variables that could not be projected.
      */
     expr_ref arith_project(model& model, app_ref_vector& vars, expr_ref_vector const& lits);
+
+    expr_ref arith_project(model& model, app_ref_vector& vars, expr* fml);
 };
 
 #endif

src/test/qe_arith.cpp

@@ -1,4 +1,5 @@
 #include "qe_arith.h"
+#include "qe.h"
 #include "th_rewriter.h"
 #include "smt2parser.h"
 #include "arith_decl_plugin.h"
@@ -7,7 +8,7 @@
 #include "ast_pp.h"
 #include "qe_util.h"
 #include "smt_context.h"
-
+#include "expr_abstract.h"
 
 static expr_ref parse_fml(ast_manager& m, char const* str) {
     expr_ref result(m);
@@ -36,6 +37,15 @@ static char const* example3 = "(and (<= z x) (<= x 3.0) (< (* 3.0 x) y) (<= z y)
 static char const* example4 = "(and (<= z x) (<= x 3.0) (not (>= (* 3.0 x) y)) (<= z y))";
 static char const* example5 = "(and (<= y x) (<= z x) (<= x u) (<= x v) (<= x t))";
 
+static char const* example6 = "(and (<= 0 (+ x z))\
+     (>= y x) \
+     (<= y x)\
+     (<= (- u y) 0.0)\
+     (>= x (+ v z))\
+     (>= x 0.0)\
+     (<= x 1.0))";
+
+
 static void test(char const *ex) {
     smt_params params;
     params.m_model = true;
@@ -58,9 +68,65 @@ static void test(char const *ex) {
     
     std::cout << mk_pp(fml, m) << "\n";
     std::cout << mk_pp(pr, m) << "\n";
+    
+}
+
+static void test2(char const *ex) {
+    smt_params params;
+    params.m_model = true;
+    ast_manager m;
+    reg_decl_plugins(m);
+    arith_util a(m);
+    expr_ref fml = parse_fml(m, ex);
+    app_ref_vector vars(m);
+    expr_ref_vector lits(m);
+    vars.push_back(m.mk_const(symbol("x"), a.mk_real()));
+    vars.push_back(m.mk_const(symbol("y"), a.mk_real()));
+    vars.push_back(m.mk_const(symbol("z"), a.mk_real()));
+    qe::flatten_and(fml, lits);
+
+    smt::context ctx(m, params);
+    ctx.push();
+    ctx.assert_expr(fml);
+    lbool result = ctx.check();
+    SASSERT(result == l_true);
+    ref<model> md;
+    ctx.get_model(md);  
+    ctx.pop(1);
+    
+    std::cout << mk_pp(fml, m) << "\n";
+
+    expr_ref pr2(m), fml2(m);
+    expr_ref_vector bound(m);
+    ptr_vector<sort> sorts;
+    svector<symbol> names;
+    for (unsigned i = 0; i < vars.size(); ++i) {
+        bound.push_back(vars[i].get());
+        names.push_back(vars[i]->get_decl()->get_name());
+        sorts.push_back(m.get_sort(vars[i].get()));
+    }
+    expr_abstract(m, 0, 3, bound.c_ptr(), fml, fml2);
+    fml2 = m.mk_exists(3, sorts.c_ptr(), names.c_ptr(), fml2);
+    qe::expr_quant_elim qe(m, params);
+    expr_ref pr1 = qe::arith_project(*md, vars, lits);
+    qe(m.mk_true(), fml2, pr2);
+    std::cout << mk_pp(pr1, m) << "\n";
+    std::cout << mk_pp(pr2, m) << "\n";
+
+    expr_ref npr2(m);
+    npr2 = m.mk_not(pr2);
+    ctx.push();
+    ctx.assert_expr(pr1);
+    ctx.assert_expr(npr2);
+    VERIFY(l_false == ctx.check());
+    ctx.pop(1);
+    
+    
 }
 
 void tst_qe_arith() {
+    test2(example6);
+    return;
     test(example1);
     test(example2);
     test(example3);