From 0d3fed9a6ad844c0b65130b2013e7372dd16d92f Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 9 Sep 2019 19:55:21 +0200 Subject: [PATCH] spacer: lemma generalizer for small numbers Attempts to reduce denominators in coefficients of farkas lemmas --- src/muz/base/fp_params.pyg | 1 + src/muz/spacer/CMakeLists.txt | 1 + src/muz/spacer/spacer_arith_generalizers.cpp | 164 +++++++++++++++++++ src/muz/spacer/spacer_context.cpp | 6 + src/muz/spacer/spacer_context.h | 2 + src/muz/spacer/spacer_generalizers.h | 106 ++++++++---- 6 files changed, 249 insertions(+), 31 deletions(-) create mode 100644 src/muz/spacer/spacer_arith_generalizers.cpp diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index 111a274de..afa4b5218 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -179,5 +179,6 @@ def_module_params('fp', ('spacer.gpdr', BOOL, False, 'Use GPDR solving strategy for non-linear CHC'), ('spacer.gpdr.bfs', BOOL, True, 'Use BFS exploration strategy for expanding model search'), ('spacer.use_bg_invs', BOOL, False, 'Enable external background invariants'), + ('spacer.use_lim_num_gen', BOOL, False, 'Enable limit numbers generalizer to get smaller numbers'), )) diff --git a/src/muz/spacer/CMakeLists.txt b/src/muz/spacer/CMakeLists.txt index 43fffd9fb..d703c5db4 100644 --- a/src/muz/spacer/CMakeLists.txt +++ b/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 diff --git a/src/muz/spacer/spacer_arith_generalizers.cpp b/src/muz/spacer/spacer_arith_generalizers.cpp new file mode 100644 index 000000000..5eef2a6d8 --- /dev/null +++ b/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 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 diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 492182dbe..b4a06f361 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -2323,6 +2323,7 @@ void context::updt_params() { m_children_order = static_cast(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)); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index f73af2fe3..125017c24 100644 --- a/src/muz/spacer/spacer_context.h +++ b/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;} diff --git a/src/muz/spacer/spacer_generalizers.h b/src/muz/spacer/spacer_generalizers.h index e83cc1bc9..82567b49d 100644 --- a/src/muz/spacer/spacer_generalizers.h +++ b/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