1 /*++
2 Copyright (c) 2019 Microsoft Corporation and Arie Gurfinkel
3
4 Module Name:
5
6 spacer_arith_generalizers.cpp
7
8 Abstract:
9
10 Arithmetic-related generalizers
11
12 Author:
13
14 Arie Gurfinkel
15
16 Revision History:
17
18 --*/
19
20 #include "ast/rewriter/rewriter.h"
21 #include "ast/rewriter/rewriter_def.h"
22 #include "muz/spacer/spacer_generalizers.h"
23 #include "smt/smt_solver.h"
24
25 namespace spacer {
26
27 namespace {
28 /* Rewrite all denominators to be no larger than a given limit */
29 struct limit_denominator_rewriter_cfg : public default_rewriter_cfg {
30 ast_manager &m;
31 arith_util m_arith;
32 rational m_limit;
33
limit_denominator_rewriter_cfgspacer::__anone5ab778d0111::limit_denominator_rewriter_cfg34 limit_denominator_rewriter_cfg(ast_manager &manager, rational limit)
35 : m(manager), m_arith(m), m_limit(limit) {}
36
is_numeralspacer::__anone5ab778d0111::limit_denominator_rewriter_cfg37 bool is_numeral(func_decl *f, rational &val, bool &is_int) {
38 if (f->get_family_id() == m_arith.get_family_id() &&
39 f->get_decl_kind() == OP_NUM) {
40 val = f->get_parameter(0).get_rational();
41 is_int = f->get_parameter(1).get_int() != 0;
42 return true;
43 }
44 return false;
45 }
46
limit_denominatorspacer::__anone5ab778d0111::limit_denominator_rewriter_cfg47 bool limit_denominator(rational &num) {
48 return rational::limit_denominator(num, m_limit);
49 }
50
reduce_appspacer::__anone5ab778d0111::limit_denominator_rewriter_cfg51 br_status reduce_app(func_decl *f, unsigned num, expr *const *args,
52 expr_ref &result, proof_ref &result_pr) {
53 bool is_int;
54 rational val;
55
56 if (is_numeral(f, val, is_int) && !is_int) {
57 if (limit_denominator(val)) {
58 result = m_arith.mk_numeral(val, false);
59 return BR_DONE;
60 }
61 }
62 return BR_FAILED;
63 }
64 };
65 } // namespace
limit_num_generalizer(context & ctx,unsigned failure_limit)66 limit_num_generalizer::limit_num_generalizer(context &ctx,
67 unsigned failure_limit)
68 : lemma_generalizer(ctx), m_failure_limit(failure_limit) {}
69
limit_denominators(expr_ref_vector & lits,rational & limit)70 bool limit_num_generalizer::limit_denominators(expr_ref_vector &lits,
71 rational &limit) {
72 ast_manager &m = m_ctx.get_ast_manager();
73 limit_denominator_rewriter_cfg rw_cfg(m, limit);
74 rewriter_tpl<limit_denominator_rewriter_cfg> rw(m, false, rw_cfg);
75
76 expr_ref lit(m);
77 bool dirty = false;
78 for (unsigned i = 0, sz = lits.size(); i < sz; ++i) {
79 rw(lits.get(i), lit);
80 dirty |= (lits.get(i) != lit.get());
81 lits[i] = lit;
82 }
83 return dirty;
84 }
85
operator ()(lemma_ref & lemma)86 void limit_num_generalizer::operator()(lemma_ref &lemma) {
87 if (lemma->get_cube().empty()) return;
88
89 m_st.count++;
90 scoped_watch _w_(m_st.watch);
91
92 unsigned uses_level;
93 pred_transformer &pt = lemma->get_pob()->pt();
94 ast_manager &m = pt.get_ast_manager();
95
96 expr_ref_vector cube(m);
97
98 // create a solver to check whether updated cube is in a generalization
99 ref<solver> sol = mk_smt_solver(m, params_ref::get_empty(), symbol::null);
100 SASSERT(lemma->has_pob());
101 sol->assert_expr(lemma->get_pob()->post());
102 unsigned weakness = lemma->weakness();
103 rational limit(100);
104 for (unsigned num_failures = 0; num_failures < m_failure_limit;
105 ++num_failures) {
106 cube.reset();
107 cube.append(lemma->get_cube());
108 // try to limit denominators
109 if (!limit_denominators(cube, limit)) return;
110
111 bool failed = false;
112 // check that pob->post() ==> cube
113 for (auto *lit : cube) {
114 solver::scoped_push _p_(*sol);
115 expr_ref nlit(m);
116 nlit = m.mk_not(lit);
117 sol->assert_expr(nlit);
118 lbool res = sol->check_sat(0, nullptr);
119 if (res == l_false) {
120 // good
121 } else {
122 failed = true;
123 TRACE("spacer.limnum", tout << "Failed to generalize: "
124 << lemma->get_cube()
125 << "\ninto\n"
126 << cube << "\n";);
127 break;
128 }
129 }
130
131 // check that !cube & F & Tr ==> !cube'
132 if (!failed && pt.check_inductive(lemma->level(), cube, uses_level, weakness)) {
133 TRACE("spacer",
134 tout << "Reduced fractions from:\n"
135 << lemma->get_cube() << "\n\nto\n"
136 << cube << "\n";);
137 lemma->update_cube(lemma->get_pob(), cube);
138 lemma->set_level(uses_level);
139 // done
140 return;
141 }
142 ++m_st.num_failures;
143 // increase limit
144 limit = limit * 10;
145 }
146 }
147
collect_statistics(statistics & st) const148 void limit_num_generalizer::collect_statistics(statistics &st) const {
149 st.update("time.spacer.solve.reach.gen.lim_num", m_st.watch.get_seconds());
150 st.update("limitted num gen", m_st.count);
151 st.update("limitted num gen failures", m_st.num_failures);
152 }
153 } // namespace spacer
154