From badb32f9aeda4f95e512e2bdfee27c87d037a122 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 3 Feb 2018 16:33:14 -0800
Subject: [PATCH] neatify rewriting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/pb_decl_plugin.cpp           | 12 ++++++++++++
 src/ast/rewriter/pb_rewriter.cpp     | 13 ++++++++++---
 src/tactic/arith/lia2card_tactic.cpp |  4 ++--
 3 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp
index 298733a94..d36c4ba89 100644
--- a/src/ast/pb_decl_plugin.cpp
+++ b/src/ast/pb_decl_plugin.cpp
@@ -129,9 +129,15 @@ app * pb_util::mk_le(unsigned num_args, rational const * coeffs, expr * const *
     normalize(num_args, coeffs, k);
     m_params.reset();
     m_params.push_back(parameter(floor(m_k)));
+    bool all_ones = true;
     for (unsigned i = 0; i < num_args; ++i) {
+        all_ones &= m_coeffs[i].is_one();
         m_params.push_back(parameter(m_coeffs[i]));
     }
+    if (all_ones && k.is_unsigned()) {
+        m_params[0] = parameter(floor(m_k).get_unsigned());
+        return m.mk_app(m_fid, OP_AT_MOST_K, 1, m_params.c_ptr(), num_args, args, m.mk_bool_sort());
+    }
     return m.mk_app(m_fid, OP_PB_LE, m_params.size(), m_params.c_ptr(), num_args, args, m.mk_bool_sort());
 }
 
@@ -139,9 +145,15 @@ app * pb_util::mk_ge(unsigned num_args, rational const * coeffs, expr * const *
     normalize(num_args, coeffs, k);
     m_params.reset();
     m_params.push_back(parameter(ceil(m_k)));
+    bool all_ones = true;
     for (unsigned i = 0; i < num_args; ++i) {
+        all_ones &= m_coeffs[i].is_one();
         m_params.push_back(parameter(m_coeffs[i]));
     }
+    if (all_ones && k.is_unsigned()) {
+        m_params[0] = parameter(ceil(m_k).get_unsigned());
+        return m.mk_app(m_fid, OP_AT_LEAST_K, 1, m_params.c_ptr(), num_args, args, m.mk_bool_sort());
+    }
     return m.mk_app(m_fid, OP_PB_GE, m_params.size(), m_params.c_ptr(), num_args, args, m.mk_bool_sort());
 }
 
diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp
index 33527ea2c..004f0d592 100644
--- a/src/ast/rewriter/pb_rewriter.cpp
+++ b/src/ast/rewriter/pb_rewriter.cpp
@@ -115,14 +115,15 @@ expr_ref pb_rewriter::translate_pb2lia(obj_map<expr,expr*>& vars, expr* fml) {
         else {
             tmp = a.mk_add(es.size(), es.c_ptr());
         }
+        rational k = util.get_k(fml);
         if (util.is_le(fml)) {
-            result = a.mk_le(tmp, a.mk_numeral(util.get_k(fml), false));
+            result = a.mk_le(tmp, a.mk_numeral(k, false));
         }
         else if (util.is_ge(fml)) {
-            result = a.mk_ge(tmp, a.mk_numeral(util.get_k(fml), false));
+            result = a.mk_ge(tmp, a.mk_numeral(k, false));
         }
         else {
-            result = m().mk_eq(tmp, a.mk_numeral(util.get_k(fml), false));
+            result = m().mk_eq(tmp, a.mk_numeral(k, false));
         }
     }
     else {
@@ -265,6 +266,12 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
             if (sz == 0) {
                 result = k.is_zero()?m.mk_true():m.mk_false();
             }
+            else if (k.is_zero()) {
+                result = mk_not(m, mk_or(m, sz, m_args.c_ptr()));
+            }
+            else if (k.is_one() && all_unit && m_args.size() == 1) {
+                result = m_args.back();
+            }
             else {
                 result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k);
             }
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index 09facedbe..dd9c5ff6b 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -158,7 +158,7 @@ public:
         m_rw(*this),
         m_pb(m),
         m_todo(alloc(ptr_vector<expr>)),
-        m_compile_equality(false) {
+        m_compile_equality(true) {
         m_max_ub = 100;
     }
 
@@ -168,7 +168,7 @@ public:
                 
     void updt_params(params_ref const & p) {
         m_params = p;
-        m_compile_equality = p.get_bool("compile_equality", false);
+        m_compile_equality = p.get_bool("compile_equality", true);
     }
     
     expr_ref mk_bounded(expr_ref_vector& axioms, app* x, unsigned lo, unsigned hi) {