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