spacer: lemma generalizer for small numbers

Attempts to reduce denominators in coefficients of farkas lemmas

src/muz/spacer/CMakeLists.txt

@@ -21,6 +21,7 @@ z3_add_component(spacer
   spacer_qe_project.cpp
   spacer_sem_matcher.cpp
   spacer_quant_generalizer.cpp
+  spacer_arith_generalizers.cpp
   spacer_callback.cpp
   spacer_json.cpp
   spacer_iuc_proof.cpp

src/muz/spacer/spacer_arith_generalizers.cpp

@@ -0,0 +1,164 @@
+/*++
+  Copyright (c) 2019 Microsoft Corporation and Arie Gurfinkel
+
+  Module Name:
+
+  spacer_arith_generalizers.cpp
+
+  Abstract:
+
+  Arithmetic-related generalizers
+
+  Author:
+
+  Arie Gurfinkel
+
+  Revision History:
+
+  --*/
+
+#include "ast/rewriter/rewriter.h"
+#include "ast/rewriter/rewriter_def.h"
+#include "muz/spacer/spacer_generalizers.h"
+
+namespace spacer {
+
+namespace {
+/* Rewrite all denominators to be no larger than a given limit */
+struct limit_denominator_rewriter_cfg : public default_rewriter_cfg {
+    ast_manager &m;
+    arith_util m_arith;
+    rational m_limit;
+
+    limit_denominator_rewriter_cfg(ast_manager &manager, rational limit)
+        : m(manager), m_arith(m), m_limit(limit) {}
+
+    bool is_numeral(func_decl *f, rational &val, bool &is_int) {
+        if (f->get_family_id() == m_arith.get_family_id() &&
+            f->get_decl_kind() == OP_NUM) {
+            val = f->get_parameter(0).get_rational();
+            is_int = f->get_parameter(1).get_int() != 0;
+            return true;
+        }
+        return false;
+    }
+
+    bool limit_denominator(rational &num) {
+        rational n, d;
+        n = numerator(num);
+        d = denominator(num);
+        if (d < m_limit) return false;
+
+        /*
+          Iteratively computes approximation using continuous fraction
+          decomposition
+
+          p(-1) = 0, p(0) = 1
+          p(j) = t(j)*p(j-1) + p(j-2)
+
+          q(-1) = 1, q(0) = 0
+          q(j) = t(j)*q(j-1) + q(j-2)
+
+          cf[t1; t2, ..., tr] =  p(r) / q(r) for r >= 1
+          reference: https://www.math.u-bordeaux.fr/~pjaming/M1/exposes/MA2.pdf
+        */
+
+        rational p0(0), p1(1);
+        rational q0(1), q1(0);
+
+        while (d != rational(0)) {
+            rational tj(0), rem(0);
+            rational p2(0), q2(0);
+            tj = div(n, d);
+
+            q2 = tj * q1 + q0;
+            p2 = tj * p1 + p0;
+            if (q2 >= m_limit) {
+                num = p2/q2;
+                return true;
+            }
+            rem = n - tj * d;
+            p0 = p1;
+            p1 = p2;
+            q0 = q1;
+            q1 = q2;
+            n = d;
+            d = rem;
+        }
+        return false;
+    }
+
+    br_status reduce_app(func_decl *f, unsigned num, expr *const *args,
+                         expr_ref &result, proof_ref &result_pr) {
+        bool is_int;
+        rational val;
+
+        if (is_numeral(f, val, is_int) && !is_int) {
+            if (limit_denominator(val)) {
+                result = m_arith.mk_numeral(val, false);
+                return BR_DONE;
+            }
+        }
+        return BR_FAILED;
+    }
+};
+} // namespace
+limit_num_generalizer::limit_num_generalizer(context &ctx,
+                                                   unsigned failure_limit)
+    : lemma_generalizer(ctx), m_failure_limit(failure_limit) {}
+
+bool limit_num_generalizer::limit_denominators(expr_ref_vector &lits,
+                                                  rational &limit) {
+    ast_manager &m = m_ctx.get_ast_manager();
+    limit_denominator_rewriter_cfg rw_cfg(m, limit);
+    rewriter_tpl<limit_denominator_rewriter_cfg> rw(m, false, rw_cfg);
+
+    expr_ref lit(m);
+    bool dirty = false;
+    for (unsigned i = 0, sz = lits.size(); i < sz; ++i) {
+        rw(lits.get(i), lit);
+        dirty |= (lits.get(i) != lit.get());
+        lits[i] = lit;
+    }
+    return dirty;
+}
+
+void limit_num_generalizer::operator()(lemma_ref &lemma) {
+    if (lemma->get_cube().empty()) return;
+
+    m_st.count++;
+    scoped_watch _w_(m_st.watch);
+
+    unsigned uses_level;
+    pred_transformer &pt = lemma->get_pob()->pt();
+    ast_manager &m = pt.get_ast_manager();
+
+    expr_ref_vector cube(m);
+
+    unsigned weakness = lemma->weakness();
+    rational limit(100);
+    for (unsigned num_failures = 0; num_failures < m_failure_limit;
+         ++num_failures) {
+        cube.reset();
+        cube.append(lemma->get_cube());
+        // try to limit denominators
+        if (!limit_denominators(cube, limit)) return;
+        // check that the result is inductive
+        if (pt.check_inductive(lemma->level(), cube, uses_level, weakness)) {
+            lemma->update_cube(lemma->get_pob(), cube);
+            lemma->set_level(uses_level);
+            // done
+            return;
+        }
+        ++m_st.num_failures;
+        // increase limit
+        limit = limit * 10;
+    }
+}
+
+void limit_num_generalizer::collect_statistics(statistics &st) const {
+    st.update("time.spacer.solve.reach.gen.lim_num", m_st.watch.get_seconds());
+    st.update("limitted num gen", m_st.count);
+    st.update("limitted num gen failures", m_st.num_failures);
+}
+} // namespace spacer

src/muz/spacer/spacer_context.cpp

@@ -2323,6 +2323,7 @@ void context::updt_params() {
     m_children_order = static_cast<spacer_children_order>(m_params.spacer_order_children());
     m_simplify_pob = m_params.spacer_simplify_pob();
     m_use_euf_gen = m_params.spacer_use_euf_gen();
+    m_use_lim_num_gen = m_params.spacer_use_lim_num_gen();
     m_use_ctp = m_params.spacer_ctp();
     m_use_inc_clause = m_params.spacer_use_inc_clause();
     m_blast_term_ite_inflation = m_params.spacer_blast_term_ite_inflation();
@@ -2654,6 +2655,11 @@ void context::init_lemma_generalizers()
 {
     reset_lemma_generalizers();
 
+    if (m_use_lim_num_gen) {
+        // first, to get small numbers before any other smt calls
+        m_lemma_generalizers.push_back(alloc(limit_num_generalizer, *this, 5));
+    }
+
     if (m_q3_qgen) {
         m_lemma_generalizers.push_back(alloc(lemma_bool_inductive_generalizer,
                                              *this, 0, true));

src/muz/spacer/spacer_context.h

@@ -954,6 +954,7 @@ class context {
     bool                 m_use_restarts;
     bool                 m_simplify_pob;
     bool                 m_use_euf_gen;
+    bool                 m_use_lim_num_gen;
     bool                 m_use_ctp;
     bool                 m_use_inc_clause;
     bool                 m_use_ind_gen;
@@ -1055,6 +1056,7 @@ public:
     bool weak_abs() const {return m_weak_abs;}
     bool use_qlemmas() const {return m_use_qlemmas;}
     bool use_euf_gen() const {return m_use_euf_gen;}
+    bool use_lim_num_gen() const {return m_use_lim_num_gen;}
     bool simplify_pob() const {return m_simplify_pob;}
     bool use_ctp() const {return m_use_ctp;}
     bool use_inc_clause() const {return m_use_inc_clause;}

src/muz/spacer/spacer_generalizers.h

@@ -20,16 +20,16 @@ Revision History:
 #ifndef _SPACER_GENERALIZERS_H_
 #define _SPACER_GENERALIZERS_H_
 
-#include "muz/spacer/spacer_context.h"
 #include "ast/arith_decl_plugin.h"
+#include "muz/spacer/spacer_context.h"
 
 namespace spacer {
 
 // can be used to check whether produced core is really implied by
 // frame and therefore valid TODO: or negation?
 class lemma_sanity_checker : public lemma_generalizer {
-public:
-    lemma_sanity_checker(context& ctx) : lemma_generalizer(ctx) {}
+  public:
+    lemma_sanity_checker(context &ctx) : lemma_generalizer(ctx) {}
     ~lemma_sanity_checker() override {}
     void operator()(lemma_ref &lemma) override;
 };
@@ -43,24 +43,28 @@ class lemma_bool_inductive_generalizer : public lemma_generalizer {
         unsigned count;
         unsigned num_failures;
         stopwatch watch;
-        stats() {reset();}
-        void reset() {count = 0; num_failures = 0; watch.reset();}
+        stats() { reset(); }
+        void reset() {
+            count = 0;
+            num_failures = 0;
+            watch.reset();
+        }
     };
 
     unsigned m_failure_limit;
     bool m_array_only;
     stats m_st;
 
-public:
-    lemma_bool_inductive_generalizer(context& ctx, unsigned failure_limit,
-                                     bool array_only = false) :
-        lemma_generalizer(ctx), m_failure_limit(failure_limit),
-        m_array_only(array_only) {}
+  public:
+    lemma_bool_inductive_generalizer(context &ctx, unsigned failure_limit,
+                                     bool array_only = false)
+        : lemma_generalizer(ctx), m_failure_limit(failure_limit),
+          m_array_only(array_only) {}
     ~lemma_bool_inductive_generalizer() override {}
     void operator()(lemma_ref &lemma) override;
 
-    void collect_statistics(statistics& st) const override;
-    void reset_statistics() override {m_st.reset();}
+    void collect_statistics(statistics &st) const override;
+    void reset_statistics() override { m_st.reset(); }
 };
 
 class unsat_core_generalizer : public lemma_generalizer {
@@ -69,31 +73,36 @@ class unsat_core_generalizer : public lemma_generalizer {
         unsigned num_failures;
         stopwatch watch;
         stats() { reset(); }
-        void reset() {count = 0; num_failures = 0; watch.reset();}
+        void reset() {
+            count = 0;
+            num_failures = 0;
+            watch.reset();
+        }
     };
 
     stats m_st;
-public:
+
+  public:
     unsat_core_generalizer(context &ctx) : lemma_generalizer(ctx) {}
     ~unsat_core_generalizer() override {}
     void operator()(lemma_ref &lemma) override;
 
     void collect_statistics(statistics &st) const override;
-    void reset_statistics() override {m_st.reset();}
+    void reset_statistics() override { m_st.reset(); }
 };
 
 class lemma_array_eq_generalizer : public lemma_generalizer {
-private:
+  private:
     bool is_array_eq(ast_manager &m, expr *e);
-public:
+
+  public:
     lemma_array_eq_generalizer(context &ctx) : lemma_generalizer(ctx) {}
     ~lemma_array_eq_generalizer() override {}
     void operator()(lemma_ref &lemma) override;
-
 };
 
 class lemma_eq_generalizer : public lemma_generalizer {
-public:
+  public:
     lemma_eq_generalizer(context &ctx) : lemma_generalizer(ctx) {}
     ~lemma_eq_generalizer() override {}
     void operator()(lemma_ref &lemma) override;
@@ -104,8 +113,12 @@ class lemma_quantifier_generalizer : public lemma_generalizer {
         unsigned count;
         unsigned num_failures;
         stopwatch watch;
-        stats() {reset();}
-        void reset() {count = 0; num_failures = 0; watch.reset();}
+        stats() { reset(); }
+        void reset() {
+            count = 0;
+            num_failures = 0;
+            watch.reset();
+        }
     };
 
     ast_manager &m;
@@ -115,29 +128,60 @@ class lemma_quantifier_generalizer : public lemma_generalizer {
 
     bool m_normalize_cube;
     int m_offset;
-public:
+
+  public:
     lemma_quantifier_generalizer(context &ctx, bool normalize_cube = true);
     ~lemma_quantifier_generalizer() override {}
     void operator()(lemma_ref &lemma) override;
 
-    void collect_statistics(statistics& st) const override;
-    void reset_statistics() override {m_st.reset();}
-private:
+    void collect_statistics(statistics &st) const override;
+    void reset_statistics() override { m_st.reset(); }
+
+  private:
     bool generalize(lemma_ref &lemma, app *term);
 
     void find_candidates(expr *e, app_ref_vector &candidate);
     bool is_ub(var *var, expr *e);
     bool is_lb(var *var, expr *e);
-    void mk_abs_cube (lemma_ref &lemma, app *term, var *var,
-                      expr_ref_vector &gnd_cube,
-                      expr_ref_vector &abs_cube,
-                      expr *&lb, expr *&ub, unsigned &stride);
+    void mk_abs_cube(lemma_ref &lemma, app *term, var *var,
+                     expr_ref_vector &gnd_cube, expr_ref_vector &abs_cube,
+                     expr *&lb, expr *&ub, unsigned &stride);
 
     bool match_sk_idx(expr *e, app_ref_vector const &zks, expr *&idx, app *&sk);
-    void cleanup(expr_ref_vector& cube, app_ref_vector const &zks, expr_ref &bind);
+    void cleanup(expr_ref_vector &cube, app_ref_vector const &zks,
+                 expr_ref &bind);
 
     bool find_stride(expr_ref_vector &c, expr_ref &pattern, unsigned &stride);
 };
-}
+
+class limit_num_generalizer : public lemma_generalizer {
+
+    struct stats {
+        unsigned count;
+        unsigned num_failures;
+        stopwatch watch;
+        stats() { reset(); }
+        void reset() {
+            count = 0;
+            num_failures = 0;
+            watch.reset();
+        }
+    };
+
+    unsigned m_failure_limit;
+    stats m_st;
+
+    bool limit_denominators(expr_ref_vector &lits, rational &limit);
+
+  public:
+    limit_num_generalizer(context &ctx, unsigned failure_limit);
+    ~limit_num_generalizer() override {}
+
+    void operator()(lemma_ref &lemma) override;
+
+    void collect_statistics(statistics &st) const override;
+    void reset_statistics() override { m_st.reset(); }
+};
+} // namespace spacer
 
 #endif