Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Hans-Joerg Schurr
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Implementation of lambda lifting.
14 : : */
15 : :
16 : : #include "theory/uf/lambda_lift.h"
17 : :
18 : : #include "expr/node_algorithm.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "options/uf_options.h"
21 : : #include "smt/env.h"
22 : : #include "theory/uf/function_const.h"
23 : : #include "expr/sort_type_size.h"
24 : :
25 : : using namespace cvc5::internal::kind;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : : namespace uf {
30 : :
31 : 49856 : LambdaLift::LambdaLift(Env& env)
32 : : : EnvObj(env),
33 : 99712 : d_lifted(userContext()),
34 : 99712 : d_lambdaMap(userContext()),
35 : 99712 : d_epg(env.isTheoryProofProducing()
36 : 20798 : ? new EagerProofGenerator(env, userContext(), "LambdaLift::epg")
37 : 70654 : : nullptr)
38 : : {
39 : 49856 : }
40 : :
41 : 1002 : TrustNode LambdaLift::lift(Node node)
42 : : {
43 [ + + ]: 1002 : if (d_lifted.find(node) != d_lifted.end())
44 : : {
45 : 749 : return TrustNode::null();
46 : : }
47 : 253 : d_lifted.insert(node);
48 : 506 : Node assertion = getAssertionFor(node);
49 [ - + ]: 253 : if (assertion.isNull())
50 : : {
51 : 0 : return TrustNode::null();
52 : : }
53 : : // if no proofs, return lemma with no generator
54 [ + + ]: 253 : if (d_epg == nullptr)
55 : : {
56 : 98 : return TrustNode::mkTrustLemma(assertion);
57 : : }
58 : : return d_epg->mkTrustNode(
59 : 310 : assertion, ProofRule::MACRO_SR_PRED_INTRO, {}, {assertion});
60 : : }
61 : :
62 : 7412 : bool LambdaLift::needsLift(const Node& lam)
63 : : {
64 [ - + ][ - + ]: 7412 : Assert(lam.getKind() == Kind::LAMBDA);
[ - - ]
65 : 7412 : std::map<Node, bool>::iterator it = d_needsLift.find(lam);
66 [ + + ]: 7412 : if (it != d_needsLift.end())
67 : : {
68 : 6944 : return it->second;
69 : : }
70 : : // Model construction considers types in order of their type size
71 : : // (SortTypeSize::getTypeSize). If the lambda has a free variable, that
72 : : // comes later in the model construction, it may need to be lifted eagerly.
73 : : // As an example, say f : Int -> Int, g : Int x Int -> Int
74 : : // The following lambdas require eager lifting:
75 : : // - (lambda ((x Int)) (g x x))
76 : : // - (lambda ((x Int) (y Int)) (f (g x y)))
77 : : // The following lambads do not require eager lifting:
78 : : // - (lambda ((x Int)) (+ x 1)), since it has no free symbols.
79 : : // - (lambda ((x Int) (y Int)) (f x)), since its free symbol f has a type
80 : : // Int -> Int which is processed before the type of the lambda, i.e.
81 : : // Int x Int -> Int.
82 : : // Note that we only eagerly lift lambdas that furthermore impact model
83 : : // construction, which is only the case if the lambda occurs as an argument
84 : : // to a APPLY_UF or is equated to another function symbol.
85 : 468 : bool shouldLift = false;
86 : 936 : std::unordered_set<Node> syms;
87 : 468 : expr::getSymbols(lam[1], syms);
88 : 468 : SortTypeSize sts;
89 : 468 : size_t lsize = sts.getTypeSize(lam.getType());
90 [ + - ]: 468 : Trace("uf-lazy-ll") << "Lift " << lam << "?" << std::endl;
91 [ + + ]: 719 : for (const Node& v : syms)
92 : : {
93 : 500 : TypeNode tn = v.getType();
94 [ + + ]: 500 : if (!tn.isFirstClass())
95 : : {
96 : : // don't need to worry about constructor/selector/testers/etc.
97 : 147 : continue;
98 : : }
99 : 353 : size_t vsize = sts.getTypeSize(tn);
100 [ + + ]: 353 : if (vsize >= lsize)
101 : : {
102 : 249 : shouldLift = true;
103 [ + - ]: 249 : Trace("uf-lazy-ll") << "...yes due to " << v << std::endl;
104 : 249 : break;
105 : : }
106 : : }
107 : 468 : d_needsLift[lam] = shouldLift;
108 : 468 : return shouldLift;
109 : : }
110 : :
111 : 13637 : bool LambdaLift::isLifted(const Node& node) const
112 : : {
113 : 13637 : return d_lifted.find(node)!=d_lifted.end();
114 : : }
115 : :
116 : 512 : TrustNode LambdaLift::ppRewrite(Node node, std::vector<SkolemLemma>& lems)
117 : : {
118 : 1024 : Node lam = FunctionConst::toLambda(node);
119 : 1536 : TNode skolem = getSkolemFor(lam);
120 [ - + ]: 512 : if (skolem.isNull())
121 : : {
122 : 0 : return TrustNode::null();
123 : : }
124 : 512 : d_lambdaMap[skolem] = lam;
125 : 512 : bool shouldLift = true;
126 [ + + ]: 512 : if (options().uf.ufHoLazyLambdaLift)
127 : : {
128 : : // We never lift eagerly. Lambdas that may induce inconsistencies based
129 : : // on the symbols in their bodies are lifted lazily if/when they become
130 : : // equal to ordinary function symbols. This is handled in the ho extension.
131 : 496 : shouldLift = false;
132 : : }
133 [ + + ]: 512 : if (shouldLift)
134 : : {
135 : 32 : TrustNode trn = lift(lam);
136 [ + - ]: 16 : if (!trn.isNull())
137 : : {
138 : 16 : lems.push_back(SkolemLemma(trn, skolem));
139 : : }
140 : : }
141 : : // if no proofs, return lemma with no generator
142 [ + + ]: 512 : if (d_epg == nullptr)
143 : : {
144 : 292 : return TrustNode::mkTrustRewrite(node, skolem);
145 : : }
146 : 220 : Node eq = node.eqNode(skolem);
147 : : return d_epg->mkTrustedRewrite(
148 : 440 : node, skolem, ProofRule::MACRO_SR_PRED_INTRO, {eq});
149 : : }
150 : :
151 : 3728850 : Node LambdaLift::getLambdaFor(TNode skolem) const
152 : : {
153 : 3728850 : NodeNodeMap::const_iterator it = d_lambdaMap.find(skolem);
154 [ + + ]: 3728850 : if (it == d_lambdaMap.end())
155 : : {
156 : 3711220 : return Node::null();
157 : : }
158 : 17630 : return it->second;
159 : : }
160 : :
161 : 3669160 : bool LambdaLift::isLambdaFunction(TNode n) const
162 : : {
163 : 3669160 : return !getLambdaFor(n).isNull();
164 : : }
165 : :
166 : 253 : Node LambdaLift::getAssertionFor(TNode node)
167 : : {
168 : 759 : TNode skolem = getSkolemFor(node);
169 [ - + ]: 253 : if (skolem.isNull())
170 : : {
171 : 0 : return Node::null();
172 : : }
173 : 506 : Node assertion;
174 : 506 : Node lambda = FunctionConst::toLambda(node);
175 [ + - ]: 253 : if (!lambda.isNull())
176 : : {
177 : 253 : NodeManager* nm = NodeManager::currentNM();
178 : : // The new assertion
179 : 506 : std::vector<Node> children;
180 : : // bound variable list
181 : 253 : children.push_back(lambda[0]);
182 : : // body
183 : 506 : std::vector<Node> skolem_app_c;
184 : 253 : skolem_app_c.push_back(skolem);
185 : 253 : skolem_app_c.insert(skolem_app_c.end(), lambda[0].begin(), lambda[0].end());
186 : 506 : Node skolem_app = nm->mkNode(Kind::APPLY_UF, skolem_app_c);
187 : 253 : skolem_app_c[0] = lambda;
188 : 253 : Node rhs = nm->mkNode(Kind::APPLY_UF, skolem_app_c);
189 : : // For the sake of proofs, we use
190 : : // (= (k t1 ... tn) ((lambda (x1 ... xn) s) t1 ... tn)) here. This is instead of
191 : : // (= (k t1 ... tn) s); the former is more accurate since
192 : : // beta reduction uses capture-avoiding substitution, which implies that
193 : : // ((lambda (y1 ... yn) s) t1 ... tn) is alpha-equivalent but not
194 : : // necessarily syntactical equal to s.
195 : 253 : children.push_back(skolem_app.eqNode(rhs));
196 : : // axiom defining skolem
197 : 253 : assertion = nm->mkNode(Kind::FORALL, children);
198 : :
199 : : // Lambda lifting is trivial to justify, hence we don't set a proof
200 : : // generator here. In particular, replacing the skolem introduced
201 : : // here with its original lambda ensures the new assertion rewrites
202 : : // to true.
203 : : // For example, if (lambda y. t[y]) has skolem k, then this lemma is:
204 : : // forall x. k(x)=t[x]
205 : : // whose witness form rewrites
206 : : // forall x. (lambda y. t[y])(x)=t[x] --> forall x. t[x]=t[x] --> true
207 : : }
208 : 253 : return assertion;
209 : : }
210 : :
211 : 765 : Node LambdaLift::getSkolemFor(TNode node)
212 : : {
213 : 765 : Node skolem;
214 : 765 : Kind k = node.getKind();
215 [ + - ]: 765 : if (k == Kind::LAMBDA)
216 : : {
217 : : // if a lambda, return the purification variable for the node. We ignore
218 : : // lambdas with free variables, which can occur beneath quantifiers
219 : : // during preprocessing.
220 [ + - ]: 765 : if (!expr::hasFreeVar(node))
221 : : {
222 [ + - ]: 1530 : Trace("rtf-proof-debug")
223 : 765 : << "RemoveTermFormulas::run: make LAMBDA skolem" << std::endl;
224 : : // Make the skolem to represent the lambda
225 : 765 : NodeManager* nm = NodeManager::currentNM();
226 : 765 : SkolemManager* sm = nm->getSkolemManager();
227 : 765 : skolem = sm->mkPurifySkolem(node);
228 : : }
229 : : }
230 : 765 : return skolem;
231 : : }
232 : :
233 : 0 : TrustNode LambdaLift::betaReduce(TNode node) const
234 : : {
235 : 0 : Kind k = node.getKind();
236 [ - - ]: 0 : if (k == Kind::APPLY_UF)
237 : : {
238 : 0 : Node op = node.getOperator();
239 : 0 : Node opl = getLambdaFor(op);
240 [ - - ]: 0 : if (!opl.isNull())
241 : : {
242 : 0 : std::vector<Node> args(node.begin(), node.end());
243 : 0 : Node app = betaReduce(opl, args);
244 [ - - ]: 0 : Trace("uf-lazy-ll") << "Beta reduce: " << node << " -> " << app
245 : 0 : << std::endl;
246 [ - - ]: 0 : if (d_epg == nullptr)
247 : : {
248 : 0 : return TrustNode::mkTrustRewrite(node, app);
249 : : }
250 : : return d_epg->mkTrustedRewrite(
251 : 0 : node, app, ProofRule::MACRO_SR_PRED_INTRO, {node.eqNode(app)});
252 : : }
253 : : }
254 : : // otherwise, unchanged
255 : 0 : return TrustNode::null();
256 : : }
257 : :
258 : 548 : Node LambdaLift::betaReduce(TNode lam, const std::vector<Node>& args) const
259 : : {
260 [ - + ][ - + ]: 548 : Assert(lam.getKind() == Kind::LAMBDA);
[ - - ]
261 : 548 : NodeManager* nm = NodeManager::currentNM();
262 : 1096 : std::vector<Node> betaRed;
263 : 548 : betaRed.push_back(lam);
264 : 548 : betaRed.insert(betaRed.end(), args.begin(), args.end());
265 : 548 : Node app = nm->mkNode(Kind::APPLY_UF, betaRed);
266 : 548 : app = rewrite(app);
267 : 1096 : return app;
268 : : }
269 : :
270 : : } // namespace uf
271 : : } // namespace theory
272 : : } // namespace cvc5::internal
|
