fix 0-1 translation bug reported by Klaus Becker

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

src/tactic/arith/lia2card_tactic.cpp

@@ -15,6 +15,24 @@ Author:
 
 Notes:
 
+--*/
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    lia2card_tactic.cpp
+
+Abstract:
+
+    Convert 0-1 integer variables cardinality constraints to built-in cardinality operator.
+
+Author:
+ 
+    Nikolaj Bjorner (nbjorner) 2013-11-5
+
+Notes:
+
 --*/
 #include"tactical.h"
 #include"cooperate.h"
@@ -24,6 +42,7 @@ Notes:
 #include"arith_decl_plugin.h"
 #include"rewriter_def.h"
 #include"ast_util.h"
+#include"ast_pp_util.h"
 
 class lia2card_tactic : public tactic {
     struct lia_rewriter_cfg : public default_rewriter_cfg {
@@ -34,9 +53,17 @@ class lia2card_tactic : public tactic {
         vector<rational> coeffs;
         rational         coeff;
 
+        bool is_pb(expr* x, expr* y, expr_ref_vector& args, vector<rational>& coeffs, rational& coeff) {
+            args.reset();
+            coeffs.reset();
+            coeff.reset();
+            return 
+                t.get_pb_sum(x, rational::one(), args, coeffs, coeff) &&
+                t.get_pb_sum(y, -rational::one(), args, coeffs, coeff);
+        }
+
         bool is_le(expr* x, expr* y, expr_ref& result) {
-            if (t.get_pb_sum(x, rational::one(), args, coeffs, coeff) &&
+            if (is_pb(x, y, args, coeffs, coeff)) {
-                t.get_pb_sum(y, -rational::one(), args, coeffs, coeff)) {
                 result = t.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff);
                 return true;
             }
@@ -46,31 +73,41 @@ class lia2card_tactic : public tactic {
         }
 
         br_status mk_app_core(func_decl* f, unsigned sz, expr*const* es, expr_ref& result) {
-            args.reset();
-            coeffs.reset();
-            coeff.reset();
             if (is_decl_of(f, a.get_family_id(), OP_LE) && is_le(es[0], es[1], result)) {
-                return BR_DONE;
             }
-            if (is_decl_of(f, a.get_family_id(), OP_GE) && is_le(es[1], es[0], result)) {
+            else if (is_decl_of(f, a.get_family_id(), OP_GE) && is_le(es[1], es[0], result)) {
-                return BR_DONE;
             }
-            if (is_decl_of(f, a.get_family_id(), OP_LT) && is_le(es[1], es[0], result)) {
+            else if (is_decl_of(f, a.get_family_id(), OP_LT) && is_le(es[1], es[0], result)) {
                 result = m.mk_not(result);
-                return BR_DONE;
             }
-            if (is_decl_of(f, a.get_family_id(), OP_GT) && is_le(es[0], es[1], result)) {
+            else if (is_decl_of(f, a.get_family_id(), OP_GT) && is_le(es[0], es[1], result)) {
                 result = m.mk_not(result);
-                return BR_DONE;
             }
-            if (m.is_eq(f) && 
+            else if (m.is_eq(f) && is_pb(es[0], es[1], args, coeffs, coeff)) {
-                t.get_pb_sum(es[0], rational::one(), args, coeffs, coeff) &&
-                t.get_pb_sum(es[1], -rational::one(), args, coeffs, coeff)) {
                 result = t.mk_eq(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff); 
-                return BR_DONE;
             }    
+            else {
                 return BR_FAILED;
             }
+            TRACE("pbsum", tout << expr_ref(m.mk_app(f, sz, es), m) << " ==>\n" <<  result << "\n";);
+
+#if 0
+            expr_ref vc(m);
+            vc = m.mk_not(m.mk_eq(m.mk_app(f, sz, es), result));
+            ast_pp_util pp(m);
+            pp.collect(vc);
+            std::cout 
+                << "(push)\n"
+                << "(echo \"" << result << "\")\n"
+                ;
+            pp.display_decls(std::cout);
+            std::cout
+                << "(assert " << vc << ")\n"
+                << "(check-sat)\n"
+                << "(pop)\n";
+#endif
+            return BR_DONE;
+        }
 
         bool rewrite_patterns() const { return false; }
         bool flat_assoc(func_decl * f) const { return false; }
@@ -192,10 +229,18 @@ public:
         if (sz == 1 && weights[0].is_one() && w.is_zero()) {
             return m.mk_not(args[0]);
         }
+        if (w.is_neg()) {
+            DEBUG_CODE(for (unsigned i = 0; i < sz; ++i) SASSERT(weights[i].is_nonneg()); );
+            return m.mk_false();
+        }
         return m_pb.mk_le(sz, weights, args, w);
     }
 
     expr* mk_eq(unsigned sz, rational const* weights, expr* const* args, rational const& w) {
+        if (w.is_neg()) {
+            DEBUG_CODE(for (unsigned i = 0; i < sz; ++i) SASSERT(weights[i].is_nonneg()); );
+            return m.mk_false();
+        }
         if (m_compile_equality) {
             return m_pb.mk_eq(sz, weights, args, w);
         }
@@ -214,6 +259,10 @@ public:
         if (sz == 1 && weights[0].is_one() && w.is_zero()) {
             return m.mk_not(args[0]);
         }
+        if (w.is_neg()) {
+            DEBUG_CODE(for (unsigned i = 0; i < sz; ++i) SASSERT(weights[i].is_nonneg()); );
+            return m.mk_true();
+        }
         return m_pb.mk_ge(sz, weights, args, w);
     }
     
@@ -248,12 +297,6 @@ public:
         else if (a.is_to_real(x, y)) {
             ok = get_sum(y, mul, conds, args, coeffs, coeff);
         }
-        else if (m.is_ite(x, y, z, u) && is_numeral(z, r) && is_numeral(u, q)) {
-            insert_arg(r*mul, add_conds(conds, y), args, coeffs, coeff);
-            // q*(1-y) = -q*y + q
-            coeff += q*mul;
-            insert_arg(-q*mul, add_conds(conds, y), args, coeffs, coeff);
-        }
         else if (m.is_ite(x, y, z, u)) {
             conds.push_back(y);
             ok = get_sum(z, mul, conds, args, coeffs, coeff);
@@ -263,10 +306,10 @@ public:
             conds.pop_back();            
         }
         else if (is_01var(x)) {
-            insert_arg(mul, add_conds(conds, mk_01(x)), args, coeffs, coeff);
+            insert_arg(mul, conds, mk_01(x), args, coeffs, coeff);
         }
         else if (is_numeral(x, r)) {
-            insert_arg(mul*r, add_conds(conds, m.mk_true()), args, coeffs, coeff);
+            insert_arg(mul*r, conds, m.mk_true(), args, coeffs, coeff);
         }
         else {
             TRACE("pb", tout << "Can't handle " << mk_pp(x, m) << "\n";);
@@ -275,10 +318,15 @@ public:
         return ok;
     }
 
-    expr_ref add_conds(expr_ref_vector const& es, expr* e) {
+    expr_ref add_conds(expr_ref_vector& es, expr* e) {
-        if (es.empty()) return expr_ref(e, m);
+        expr_ref result(m);
-        expr_ref result = expr_ref(m.mk_and(es.size(), es.c_ptr()), m);
+        if (!m.is_true(e)) {
-        result = m.mk_and(e, result);
+            es.push_back(e);
+        }
+        result = mk_and(m, es.size(), es.c_ptr());
+        if (!m.is_true(e)) {
+            es.pop_back();
+        }
         return result;
     }
 
@@ -293,19 +341,23 @@ public:
         return a.is_numeral(e, r);
     }
     
-    void insert_arg(rational const& p, expr* x, 
+    void insert_arg(
+        rational const& p, 
+        expr_ref_vector& conds,
+        expr* x, 
         expr_ref_vector& args, vector<rational>& coeffs, rational& coeff) {
-        if (m.is_true(x)) {
+        expr_ref cond = add_conds(conds, x);
+        if (m.is_true(cond)) {
             coeff += p;
         }
         else if (p.is_neg()) {
-            // p*x = -p*(1-x) + p
+            // -p*x = p*(1-x) - p
-            args.push_back(m.mk_not(x));
+            args.push_back(m.mk_not(cond));
             coeffs.push_back(-p);
             coeff += p;
         }
         else if (p.is_pos()) {
-            args.push_back(x);
+            args.push_back(cond);
             coeffs.push_back(p);
         }
     }