add option to bypass compression of unbound tails, issue #738

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

contrib/cmake/src/ast/rewriter/CMakeLists.txt

@@ -4,6 +4,7 @@ z3_add_component(rewriter
     array_rewriter.cpp
     ast_counter.cpp
     bool_rewriter.cpp
+    bv_bounds.cpp
     bv_rewriter.cpp
     datatype_rewriter.cpp
     der.cpp

contrib/cmake/src/tactic/bv/CMakeLists.txt

@@ -5,6 +5,7 @@ z3_add_component(bv_tactics
     bv1_blaster_tactic.cpp
     bvarray2uf_rewriter.cpp
     bvarray2uf_tactic.cpp
+    bv_bound_chk_tactic.cpp
     bv_bounds_tactic.cpp
     bv_size_reduction_tactic.cpp
     dt2bv_tactic.cpp

src/muz/base/dl_context.cpp

@@ -303,6 +303,7 @@ namespace datalog {
     bool context::karr() const { return m_params->xform_karr(); }
     bool context::scale() const { return m_params->xform_scale(); }
     bool context::magic() const { return m_params->xform_magic(); }
+    bool context::compress_unbound() const { return m_params->xform_compress_unbound(); }
     bool context::quantify_arrays() const { return m_params->xform_quantify_arrays(); }
     bool context::instantiate_quantifiers() const { return m_params->xform_instantiate_quantifiers(); }
 

src/muz/base/dl_context.h

@@ -272,6 +272,7 @@ namespace datalog {
         bool karr() const;
         bool scale() const;
         bool magic() const;
+        bool compress_unbound() const;
         bool quantify_arrays() const;
         bool instantiate_quantifiers() const;
         bool xform_bit_blast() const;        

src/muz/base/fixedpoint_params.pyg

@@ -131,6 +131,7 @@ def_module_params('fixedpoint',
                           ('xform.inline_eager', BOOL, True, "try eager inlining of rules"),
                           ('xform.inline_linear_branch', BOOL, False, 
                            "try linear inlining method with potential expansion"),
+                          ('xform.compress_unbound', BOOL, True, "compress tails with unbound variables"),
                           ('xform.fix_unbound_vars', BOOL, False, "fix unbound variables in tail"),
                           ('xform.unfold_rules', UINT, 0, 
                            "unfold rules statically using iterative squarring"),

src/muz/transforms/dl_mk_unbound_compressor.cpp

@@ -344,6 +344,11 @@ namespace datalog {
 
     rule_set * mk_unbound_compressor::operator()(rule_set const & source) {
         // TODO mc
+
+        if (!m_context.compress_unbound()) {
+            return 0;
+        }
+
         m_modified = false;
 
         SASSERT(m_rules.empty());