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