1 /*
2 Copyright (c) 2017 Arie Gurfinkel
3
4 Legacy implementations of frames. To be removed.
5 */
6 #include <sstream>
7 #include <iomanip>
8
9 #include "muz/spacer/spacer_context.h"
10 #include "muz/base/dl_util.h"
11 #include "ast/rewriter/rewriter.h"
12 #include "ast/rewriter/rewriter_def.h"
13 #include "ast/rewriter/var_subst.h"
14 #include "util/util.h"
15 #include "muz/spacer/spacer_prop_solver.h"
16 #include "muz/spacer/spacer_context.h"
17 #include "muz/spacer/spacer_generalizers.h"
18 #include "ast/for_each_expr.h"
19 #include "muz/base/dl_rule_set.h"
20 #include "smt/tactic/unit_subsumption_tactic.h"
21 #include "model/model_smt2_pp.h"
22 #include "muz/transforms/dl_mk_rule_inliner.h"
23 #include "ast/ast_smt2_pp.h"
24 #include "ast/ast_ll_pp.h"
25 #include "ast/ast_util.h"
26 #include "ast/proofs/proof_checker.h"
27 #include "smt/smt_value_sort.h"
28 #include "ast/proofs/proof_utils.h"
29 #include "ast/scoped_proof.h"
30 #include "muz/spacer/spacer_qe_project.h"
31 #include "tactic/core/blast_term_ite_tactic.h"
32
33 #include "util/timeit.h"
34 #include "util/luby.h"
35 #include "ast/rewriter/expr_safe_replace.h"
36 #include "ast/expr_abstract.h"
37 #include "ast/rewriter/factor_equivs.h"
38
39
40 namespace spacer {
41 // ------------------
42 // legacy_frames
simplify_formulas(tactic & tac,expr_ref_vector & v)43 void pred_transformer::legacy_frames::simplify_formulas(tactic& tac,
44 expr_ref_vector& v)
45 {
46 ast_manager &m = m_pt.get_ast_manager();
47 goal_ref g(alloc(goal, m, false, false, false));
48 for (unsigned j = 0; j < v.size(); ++j) { g->assert_expr(v[j].get()); }
49 goal_ref_buffer result;
50 tac(g, result);
51 SASSERT(result.size() == 1);
52 goal* r = result[0];
53 v.reset();
54 for (unsigned j = 0; j < r->size(); ++j) { v.push_back(r->form(j)); }
55 }
56
simplify_formulas()57 void pred_transformer::legacy_frames::simplify_formulas()
58 {
59 ast_manager &m = m_pt.get_ast_manager();
60 tactic_ref us = mk_unit_subsumption_tactic(m);
61 simplify_formulas(*us, m_invariants);
62 for (unsigned i = 0; i < m_levels.size(); ++i) {
63 simplify_formulas(*us, m_levels[i]);
64 }
65 }
66
get_frame_geq_lemmas(unsigned lvl,expr_ref_vector & out)67 void pred_transformer::legacy_frames::get_frame_geq_lemmas(unsigned lvl,
68 expr_ref_vector &out)
69 {
70 get_frame_lemmas(infty_level(), out);
71 for (unsigned i = lvl, sz = m_levels.size(); i < sz; ++i)
72 { get_frame_lemmas(i, out); }
73 }
74
propagate_to_next_level(unsigned src_level)75 bool pred_transformer::legacy_frames::propagate_to_next_level(unsigned src_level)
76 {
77
78 ast_manager &m = m_pt.get_ast_manager();
79 (void) m;
80 if (m_levels.size() <= src_level) { return true; }
81 if (m_levels [src_level].empty()) { return true; }
82
83 unsigned tgt_level = next_level(src_level);
84 m_pt.ensure_level(next_level(tgt_level));
85
86 TRACE("spacer",
87 tout << "propagating " << src_level << " to " << tgt_level;
88 tout << " for relation " << m_pt.head()->get_name() << "\n";);
89
90 for (unsigned i = 0; i < m_levels[src_level].size();) {
91 expr_ref_vector &src = m_levels[src_level];
92 expr * curr = src[i].get();
93 unsigned stored_lvl;
94 VERIFY(m_prop2level.find(curr, stored_lvl));
95 SASSERT(stored_lvl >= src_level);
96 unsigned solver_level;
97 if (stored_lvl > src_level) {
98 TRACE("spacer", tout << "at level: " << stored_lvl << " " << mk_pp(curr, m) << "\n";);
99 src[i] = src.back();
100 src.pop_back();
101 } else if (m_pt.is_invariant(tgt_level, curr, solver_level)) {
102 // -- might invalidate src reference
103 add_lemma(curr, solver_level);
104 TRACE("spacer", tout << "is invariant: " << pp_level(solver_level) << " " << mk_pp(curr, m) << "\n";);
105 // shadow higher-level src
106 expr_ref_vector &src = m_levels[src_level];
107 src[i] = src.back();
108 src.pop_back();
109 ++m_pt.m_stats.m_num_propagations;
110 } else {
111 TRACE("spacer", tout << "not propagated: " << mk_pp(curr, m) << "\n";);
112 ++i;
113 }
114 }
115
116 CTRACE("spacer", m_levels[src_level].empty(),
117 tout << "Fully propagated level "
118 << src_level << " of " << m_pt.head()->get_name() << "\n";);
119
120 return m_levels[src_level].empty();
121 }
122
add_lemma(expr * lemma,unsigned lvl)123 bool pred_transformer::legacy_frames::add_lemma(expr * lemma, unsigned lvl)
124 {
125 if (is_infty_level(lvl)) {
126 if (!m_invariants.contains(lemma)) {
127 m_invariants.push_back(lemma);
128 m_prop2level.insert(lemma, lvl);
129 //m_pt.add_lemma_core (lemma, lvl);
130 return true;
131 }
132 return false;
133 }
134
135 unsigned old_level;
136 if (!m_prop2level.find(lemma, old_level) || old_level < lvl) {
137 m_levels[lvl].push_back(lemma);
138 m_prop2level.insert(lemma, lvl);
139 //m_pt.add_lemma_core (lemma, lvl);
140 return true;
141 }
142 return false;
143 }
144
propagate_to_infinity(unsigned level)145 void pred_transformer::legacy_frames::propagate_to_infinity(unsigned level)
146 {
147 TRACE("spacer", tout << "propagating to oo from lvl " << level
148 << " of " << m_pt.m_head->get_name() << "\n";);
149
150 if (m_levels.empty()) { return; }
151
152 for (unsigned i = m_levels.size(); i > level; --i) {
153 expr_ref_vector &lemmas = m_levels [i - 1];
154 for (unsigned j = 0; j < lemmas.size(); ++j)
155 { add_lemma(lemmas.get(j), infty_level()); }
156 lemmas.reset();
157 }
158 }
159
inherit_frames(legacy_frames & other)160 void pred_transformer::legacy_frames::inherit_frames(legacy_frames& other)
161 {
162
163 SASSERT(m_pt.m_head == other.m_pt.m_head);
164 obj_map<expr, unsigned>::iterator it = other.m_prop2level.begin();
165 obj_map<expr, unsigned>::iterator end = other.m_prop2level.end();
166 for (; it != end; ++it) { add_lemma(it->m_key, it->m_value); }
167 }
168 }
169