1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 distribute_forall.cpp
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2010-04-02.
15
16 Revision History:
17
18 Christoph Wintersteiger 2010-04-06: Added implementation.
19
20 --*/
21 #include "ast/rewriter/var_subst.h"
22 #include "ast/ast_ll_pp.h"
23 #include "ast/ast_util.h"
24 #include "ast/rewriter/distribute_forall.h"
25 #include "ast/rewriter/bool_rewriter.h"
26
distribute_forall(ast_manager & m)27 distribute_forall::distribute_forall(ast_manager & m) :
28 m_manager(m),
29 m_cache(m) {
30 }
31
visit(expr * n,bool & visited)32 void distribute_forall::visit(expr * n, bool & visited) {
33 if (!is_cached(n)) {
34 m_todo.push_back(n);
35 visited = false;
36 }
37 }
38
visit_children(expr * n)39 bool distribute_forall::visit_children(expr * n) {
40 bool visited = true;
41 unsigned j;
42 switch(n->get_kind()) {
43 case AST_VAR:
44 break;
45 case AST_APP:
46 j = to_app(n)->get_num_args();
47 while (j > 0) {
48 --j;
49 visit(to_app(n)->get_arg(j), visited);
50 }
51 break;
52 case AST_QUANTIFIER:
53 visit(to_quantifier(n)->get_expr(), visited);
54 break;
55 default:
56 UNREACHABLE();
57 }
58 return visited;
59 }
60
reduce1(expr * n)61 void distribute_forall::reduce1(expr * n) {
62 switch (n->get_kind()) {
63 case AST_VAR:
64 cache_result(n, n);
65 break;
66 case AST_APP:
67 reduce1_app(to_app(n));
68 break;
69 case AST_QUANTIFIER:
70 reduce1_quantifier(to_quantifier(n));
71 break;
72 default: UNREACHABLE();
73 }
74 }
75
reduce1_app(app * a)76 void distribute_forall::reduce1_app(app * a) {
77 SASSERT(a);
78 unsigned num_args = a->get_num_args();
79 unsigned j = num_args;
80 bool reduced = false;
81 m_new_args.reserve(num_args);
82 app * na = a;
83
84 while(j > 0) {
85 --j;
86 SASSERT(is_cached(a->get_arg(j)));
87 expr * c = get_cached(a->get_arg(j));
88 SASSERT(c!=0);
89 if (c != a->get_arg(j))
90 reduced = true;
91 m_new_args[j] = c;
92 }
93
94 if (reduced) {
95 na = m_manager.mk_app(a->get_decl(), num_args, m_new_args.data());
96 }
97
98 cache_result(a, na);
99 }
100
reduce1_quantifier(quantifier * q)101 void distribute_forall::reduce1_quantifier(quantifier * q) {
102 // This transformation is applied after skolemization/quantifier elimination. So, all quantifiers are universal.
103 SASSERT(q->get_kind() == forall_k);
104
105 // This transformation is applied after basic pre-processing steps.
106 // So, we can assume that
107 // 1) All (and f1 ... fn) are already encoded as (not (or (not f1 ... fn)))
108 // 2) All or-formulas are flat (or f1 (or f2 f3)) is encoded as (or f1 f2 f3)
109
110 expr * e = get_cached(q->get_expr());
111 if (m_manager.is_not(e) && m_manager.is_or(to_app(e)->get_arg(0))) {
112 bool_rewriter br(m_manager);
113
114 // found target for simplification
115 // (forall X (not (or F1 ... Fn)))
116 // -->
117 // (and (forall X (not F1))
118 // ...
119 // (forall X (not Fn)))
120 app * or_e = to_app(to_app(e)->get_arg(0));
121 unsigned num_args = or_e->get_num_args();
122 expr_ref_buffer new_args(m_manager);
123 for (unsigned i = 0; i < num_args; i++) {
124 expr * arg = or_e->get_arg(i);
125 expr_ref not_arg(m_manager);
126 br.mk_not(arg, not_arg);
127 quantifier_ref tmp_q(m_manager);
128 tmp_q = m_manager.update_quantifier(q, not_arg);
129 new_args.push_back(elim_unused_vars(m_manager, tmp_q, params_ref()));
130 }
131 expr_ref result(m_manager);
132 // m_bsimp.mk_and actually constructs a (not (or ...)) formula,
133 // it will also apply basic simplifications.
134 br.mk_and(new_args.size(), new_args.data(), result);
135 cache_result(q, result);
136 }
137 else {
138 cache_result(q, m_manager.update_quantifier(q, e));
139 }
140 }
141
operator ()(expr * f,expr_ref & result)142 void distribute_forall::operator()(expr * f, expr_ref & result) {
143 m_todo.reset();
144 flush_cache();
145
146 m_todo.push_back(f);
147
148 while (!m_todo.empty()) {
149 expr * e = m_todo.back();
150 if (visit_children(e)) {
151 m_todo.pop_back();
152 reduce1(e);
153 }
154 }
155
156 result = get_cached(f);
157 SASSERT(result!=0);
158 TRACE("distribute_forall", tout << mk_ll_pp(f, m_manager) << "======>\n"
159 << mk_ll_pp(result, m_manager););
160 }
161
get_cached(expr * n) const162 expr * distribute_forall::get_cached(expr * n) const {
163 return const_cast<distribute_forall*>(this)->m_cache.find(n);
164 }
165
cache_result(expr * n,expr * r)166 void distribute_forall::cache_result(expr * n, expr * r) {
167 SASSERT(r != 0);
168 m_cache.insert(n, r);
169 }
170