Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Utility for quantifiers macro definitions.
14 : : */
15 : :
16 : : #include "theory/quantifiers/quantifiers_macros.h"
17 : :
18 : : #include "expr/node_algorithm.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "options/quantifiers_options.h"
21 : : #include "theory/arith/arith_msum.h"
22 : : #include "theory/quantifiers/ematching/pattern_term_selector.h"
23 : : #include "theory/quantifiers/quantifiers_registry.h"
24 : : #include "theory/quantifiers/term_database.h"
25 : : #include "theory/quantifiers/term_util.h"
26 : : #include "theory/rewriter.h"
27 : :
28 : : using namespace cvc5::internal::kind;
29 : :
30 : : namespace cvc5::internal {
31 : : namespace theory {
32 : : namespace quantifiers {
33 : :
34 : 40 : QuantifiersMacros::QuantifiersMacros(Env& env, QuantifiersRegistry& qr)
35 : 40 : : EnvObj(env), d_qreg(qr)
36 : : {
37 : 40 : }
38 : :
39 : 71 : Node QuantifiersMacros::solve(Node lit, bool reqGround)
40 : : {
41 [ + - ]: 71 : Trace("macros-debug") << "QuantifiersMacros::solve " << lit << std::endl;
42 [ + + ]: 71 : if (lit.getKind() != Kind::FORALL)
43 : : {
44 : 6 : return Node::null();
45 : : }
46 : 65 : Node body = lit[1];
47 : 65 : bool pol = body.getKind() != Kind::NOT;
48 [ + + ]: 65 : Node n = pol ? body : body[0];
49 : 65 : NodeManager* nm = nodeManager();
50 [ + + ]: 65 : if (n.getKind() == Kind::APPLY_UF)
51 : : {
52 : : // predicate case
53 [ + - ]: 21 : if (isBoundVarApplyUf(n))
54 : : {
55 : 21 : Node op = n.getOperator();
56 : 21 : Node n_def = nm->mkConst(pol);
57 : 42 : Node fdef = solveEq(n, n_def);
58 [ - + ][ - + ]: 21 : Assert(!fdef.isNull());
[ - - ]
59 : 21 : return returnMacro(fdef, lit);
60 : 21 : }
61 : : }
62 [ + - ][ + + ]: 44 : else if (pol && n.getKind() == Kind::EQUAL)
[ + + ]
63 : : {
64 : : // literal case
65 [ + - ]: 35 : Trace("macros-debug") << "Check macro literal : " << n << std::endl;
66 : 35 : std::map<Node, bool> visited;
67 : 35 : std::vector<Node> candidates;
68 [ + + ]: 105 : for (const Node& nc : n)
69 : : {
70 : 70 : getMacroCandidates(nc, candidates, visited);
71 : 70 : }
72 [ + + ]: 35 : for (const Node& m : candidates)
73 : : {
74 : 17 : Node op = m.getOperator();
75 [ + - ]: 17 : Trace("macros-debug") << "Check macro candidate : " << m << std::endl;
76 : : // get definition and condition
77 : 34 : Node n_def = solveInEquality(m, n); // definition for the macro
78 [ - + ]: 17 : if (n_def.isNull())
79 : : {
80 : 0 : continue;
81 : : }
82 [ + - ]: 34 : Trace("macros-debug")
83 : 17 : << m << " is possible macro in " << lit << std::endl;
84 [ + - ]: 34 : Trace("macros-debug")
85 : 17 : << " corresponding definition is : " << n_def << std::endl;
86 : 17 : visited.clear();
87 : : // cannot contain a defined operator
88 [ + - ]: 17 : if (!containsBadOp(n_def, op, reqGround))
89 : : {
90 [ + - ]: 34 : Trace("macros-debug")
91 : 17 : << "...does not contain bad (recursive) operator." << std::endl;
92 : : // must be ground UF term if mode is GROUND_UF
93 : 51 : if (options().quantifiers.macrosQuantMode
94 : : != options::MacrosQuantMode::GROUND_UF
95 : 17 : || preservesTriggerVariables(lit, n_def))
96 : : {
97 [ + - ]: 34 : Trace("macros-debug")
98 : 17 : << "...respects ground-uf constraint." << std::endl;
99 : 34 : Node fdef = solveEq(m, n_def);
100 [ + - ]: 17 : if (!fdef.isNull())
101 : : {
102 : 17 : return returnMacro(fdef, lit);
103 : : }
104 [ - + ]: 17 : }
105 : : }
106 [ - - ][ + - ]: 34 : }
[ - + ]
107 [ + + ][ + + ]: 52 : }
108 : 27 : return Node::null();
109 : 65 : }
110 : :
111 : 17 : bool QuantifiersMacros::containsBadOp(Node n, Node op, bool reqGround)
112 : : {
113 : 17 : std::unordered_set<TNode> visited;
114 : 17 : std::unordered_set<TNode>::iterator it;
115 : 17 : std::vector<TNode> visit;
116 : 17 : TNode cur;
117 : 17 : visit.push_back(n);
118 : : do
119 : : {
120 : 31 : cur = visit.back();
121 : 31 : visit.pop_back();
122 : 31 : it = visited.find(cur);
123 [ + - ]: 31 : if (it == visited.end())
124 : : {
125 : 31 : visited.insert(cur);
126 [ - + ][ - - ]: 31 : if (cur.isClosure() && reqGround)
[ - + ]
127 : : {
128 : 0 : return true;
129 : : }
130 [ - + ]: 31 : else if (cur == op)
131 : : {
132 : 0 : return true;
133 : : }
134 [ + + ][ - + ]: 31 : else if (cur.hasOperator() && cur.getOperator() == op)
[ + + ][ - + ]
[ - - ]
135 : : {
136 : 0 : return true;
137 : : }
138 : 31 : visit.insert(visit.end(), cur.begin(), cur.end());
139 : : }
140 [ + + ]: 31 : } while (!visit.empty());
141 : 17 : return false;
142 : 17 : }
143 : :
144 : 15 : bool QuantifiersMacros::preservesTriggerVariables(Node q, Node n)
145 : : {
146 : 15 : Assert(q.getKind() == Kind::FORALL)
147 : 0 : << "Expected quantified formula, got " << q;
148 : 30 : Node icn = d_qreg.substituteBoundVariablesToInstConstants(n, q);
149 [ + - ]: 15 : Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
150 : 15 : std::vector<Node> var;
151 : 15 : quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var);
152 [ + - ]: 15 : Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
153 : 15 : std::vector<Node> trigger_var;
154 : 30 : inst::PatternTermSelector::getTriggerVariables(
155 : 15 : d_env.getOptions(), icn, q, trigger_var);
156 [ + - ]: 15 : Trace("macros-debug2") << "Done." << std::endl;
157 : : // only if all variables are also trigger variables
158 : 30 : return trigger_var.size() >= var.size();
159 : 15 : }
160 : :
161 : 60 : bool QuantifiersMacros::isBoundVarApplyUf(Node n)
162 : : {
163 [ - + ][ - + ]: 60 : Assert(n.getKind() == Kind::APPLY_UF);
[ - - ]
164 : 60 : TypeNode tno = n.getOperator().getType();
165 : 60 : std::map<Node, bool> vars;
166 : : // allow if a vector of unique variables of the same type as UF arguments
167 [ + + ]: 284 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
168 : : {
169 [ + + ]: 244 : if (n[i].getKind() != Kind::BOUND_VARIABLE)
170 : : {
171 : 13 : return false;
172 : : }
173 [ - + ]: 231 : if (n[i].getType() != tno[i])
174 : : {
175 : 0 : return false;
176 : : }
177 [ + + ]: 231 : if (vars.find(n[i]) == vars.end())
178 : : {
179 : 224 : vars[n[i]] = true;
180 : : }
181 : : else
182 : : {
183 : 7 : return false;
184 : : }
185 : : }
186 : 40 : return true;
187 : 60 : }
188 : :
189 : 76 : void QuantifiersMacros::getMacroCandidates(Node n,
190 : : std::vector<Node>& candidates,
191 : : std::map<Node, bool>& visited)
192 : : {
193 [ + - ]: 76 : if (visited.find(n) == visited.end())
194 : : {
195 : 76 : visited[n] = true;
196 [ + + ]: 76 : if (n.getKind() == Kind::APPLY_UF)
197 : : {
198 [ + + ]: 39 : if (isBoundVarApplyUf(n))
199 : : {
200 : 19 : candidates.push_back(n);
201 : : }
202 : : }
203 [ + + ]: 37 : else if (n.getKind() == Kind::ADD)
204 : : {
205 [ + + ]: 6 : for (size_t i = 0; i < n.getNumChildren(); i++)
206 : : {
207 : 4 : getMacroCandidates(n[i], candidates, visited);
208 : : }
209 : : }
210 [ + + ]: 35 : else if (n.getKind() == Kind::MULT)
211 : : {
212 : : // if the LHS is a constant
213 [ + - ][ + - ]: 2 : if (n.getNumChildren() == 2 && n[0].isConst())
[ + - ][ + - ]
[ - - ]
214 : : {
215 : 2 : getMacroCandidates(n[1], candidates, visited);
216 : : }
217 : : }
218 [ - + ]: 33 : else if (n.getKind() == Kind::NOT)
219 : : {
220 : 0 : getMacroCandidates(n[0], candidates, visited);
221 : : }
222 : : }
223 : 76 : }
224 : :
225 : 17 : Node QuantifiersMacros::solveInEquality(Node n, Node lit)
226 : : {
227 [ + - ]: 17 : if (lit.getKind() == Kind::EQUAL)
228 : : {
229 : : // return the opposite side of the equality if defined that way
230 [ + + ]: 25 : for (int i = 0; i < 2; i++)
231 : : {
232 [ + + ]: 21 : if (lit[i] == n)
233 : : {
234 [ + - ]: 30 : return lit[i == 0 ? 1 : 0];
235 : : }
236 : 8 : else if (lit[i].getKind() == Kind::NOT && lit[i][0] == n)
237 : : {
238 [ - - ]: 0 : return lit[i == 0 ? 1 : 0].negate();
239 : : }
240 : : }
241 : 4 : std::map<Node, Node> msum;
242 [ + - ]: 4 : if (ArithMSum::getMonomialSumLit(lit, msum))
243 : : {
244 : 4 : Node veq_c;
245 : 4 : Node val;
246 : 4 : int res = ArithMSum::isolate(n, msum, veq_c, val, Kind::EQUAL);
247 [ + - ][ + - ]: 4 : if (res != 0 && veq_c.isNull())
[ + - ]
248 : : {
249 : 4 : return val;
250 : : }
251 [ - + ][ - + ]: 8 : }
252 [ - + ]: 4 : }
253 [ - - ]: 0 : Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl;
254 : 0 : return Node::null();
255 : : }
256 : :
257 : 38 : Node QuantifiersMacros::solveEq(Node n, Node ndef)
258 : : {
259 [ - + ][ - + ]: 38 : Assert(n.getKind() == Kind::APPLY_UF);
[ - - ]
260 : 38 : NodeManager* nm = nodeManager();
261 [ + - ]: 38 : Trace("macros-debug") << "Add macro eq for " << n << std::endl;
262 [ + - ]: 38 : Trace("macros-debug") << " def: " << ndef << std::endl;
263 : 38 : std::vector<Node> vars;
264 : 38 : std::vector<Node> fvars;
265 [ + + ]: 211 : for (const Node& nc : n)
266 : : {
267 : 173 : vars.push_back(nc);
268 : 173 : Node v = NodeManager::mkBoundVar(nc.getType());
269 : 173 : fvars.push_back(v);
270 : 173 : }
271 : : Node fdef =
272 : 38 : ndef.substitute(vars.begin(), vars.end(), fvars.begin(), fvars.end());
273 : : fdef =
274 : 38 : nm->mkNode(Kind::LAMBDA, nm->mkNode(Kind::BOUND_VAR_LIST, fvars), fdef);
275 : : // If the definition has a free variable, it is malformed. This can happen
276 : : // if the right hand side of a macro definition contains a variable not
277 : : // contained in the left hand side
278 [ - + ]: 38 : if (expr::hasFreeVar(fdef))
279 : : {
280 : 0 : return Node::null();
281 : : }
282 : 38 : TNode op = n.getOperator();
283 : 38 : TNode fdeft = fdef;
284 [ - + ][ - + ]: 38 : Assert(op.getType() == fdef.getType());
[ - - ]
285 : 38 : return op.eqNode(fdef);
286 : 38 : }
287 : :
288 : 38 : Node QuantifiersMacros::returnMacro(Node fdef, Node lit) const
289 : : {
290 [ + - ]: 76 : Trace("macros") << "* Inferred macro " << fdef << " from " << lit
291 : 38 : << std::endl;
292 : 38 : return fdef;
293 : : }
294 : :
295 : : } // namespace quantifiers
296 : : } // namespace theory
297 : : } // namespace cvc5::internal
|
