--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of lambda lifting.
+ */
+
+#include "theory/uf/lambda_lift.h"
+
+#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
+#include "options/uf_options.h"
+#include "smt/env.h"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+namespace theory {
+namespace uf {
+
+LambdaLift::LambdaLift(Env& env)
+ : EnvObj(env),
+ d_lifted(userContext()),
+ d_lambdaMap(userContext()),
+ d_epg(env.isTheoryProofProducing() ? new EagerProofGenerator(
+ env.getProofNodeManager(), userContext(), "LambdaLift::epg")
+ : nullptr)
+{
+}
+
+TrustNode LambdaLift::lift(Node node)
+{
+ if (d_lifted.find(node) != d_lifted.end())
+ {
+ return TrustNode::null();
+ }
+ d_lifted.insert(node);
+ Node assertion = getAssertionFor(node);
+ if (assertion.isNull())
+ {
+ return TrustNode::null();
+ }
+ // if no proofs, return lemma with no generator
+ if (d_epg == nullptr)
+ {
+ return TrustNode::mkTrustLemma(assertion);
+ }
+ return d_epg->mkTrustNode(
+ assertion, PfRule::MACRO_SR_PRED_INTRO, {}, {assertion});
+}
+
+TrustNode LambdaLift::ppRewrite(Node node, std::vector<SkolemLemma>& lems)
+{
+ TNode skolem = getSkolemFor(node);
+ if (skolem.isNull())
+ {
+ return TrustNode::null();
+ }
+ d_lambdaMap[skolem] = node;
+ if (!options().uf.ufHoLazyLambdaLift)
+ {
+ TrustNode trn = lift(node);
+ lems.push_back(SkolemLemma(trn, skolem));
+ }
+ // if no proofs, return lemma with no generator
+ if (d_epg == nullptr)
+ {
+ return TrustNode::mkTrustRewrite(node, skolem);
+ }
+ Node eq = node.eqNode(skolem);
+ return d_epg->mkTrustedRewrite(
+ node, skolem, PfRule::MACRO_SR_PRED_INTRO, {eq});
+}
+
+Node LambdaLift::getLambdaFor(TNode skolem) const
+{
+ NodeNodeMap::const_iterator it = d_lambdaMap.find(skolem);
+ if (it == d_lambdaMap.end())
+ {
+ return Node::null();
+ }
+ return it->second;
+}
+
+Node LambdaLift::getAssertionFor(TNode node)
+{
+ TNode skolem = getSkolemFor(node);
+ if (skolem.isNull())
+ {
+ return Node::null();
+ }
+ Kind k = node.getKind();
+ Node assertion;
+ if (k == LAMBDA)
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ // The new assertion
+ std::vector<Node> children;
+ // bound variable list
+ children.push_back(node[0]);
+ // body
+ std::vector<Node> skolem_app_c;
+ skolem_app_c.push_back(skolem);
+ skolem_app_c.insert(skolem_app_c.end(), node[0].begin(), node[0].end());
+ Node skolem_app = nm->mkNode(APPLY_UF, skolem_app_c);
+ children.push_back(skolem_app.eqNode(node[1]));
+ // axiom defining skolem
+ assertion = nm->mkNode(FORALL, children);
+
+ // Lambda lifting is trivial to justify, hence we don't set a proof
+ // generator here. In particular, replacing the skolem introduced
+ // here with its original lambda ensures the new assertion rewrites
+ // to true.
+ // For example, if (lambda y. t[y]) has skolem k, then this lemma is:
+ // forall x. k(x)=t[x]
+ // whose witness form rewrites
+ // forall x. (lambda y. t[y])(x)=t[x] --> forall x. t[x]=t[x] --> true
+ }
+ return assertion;
+}
+
+Node LambdaLift::getSkolemFor(TNode node)
+{
+ Node skolem;
+ Kind k = node.getKind();
+ if (k == LAMBDA)
+ {
+ // if a lambda, return the purification variable for the node. We ignore
+ // lambdas with free variables, which can occur beneath quantifiers
+ // during preprocessing.
+ if (!expr::hasFreeVar(node))
+ {
+ Trace("rtf-proof-debug")
+ << "RemoveTermFormulas::run: make LAMBDA skolem" << std::endl;
+ // Make the skolem to represent the lambda
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ skolem = sm->mkPurifySkolem(
+ node,
+ "lambdaF",
+ "a function introduced due to term-level lambda removal");
+ }
+ }
+ return skolem;
+}
+
+TrustNode LambdaLift::betaReduce(TNode node) const
+{
+ Kind k = node.getKind();
+ if (k == APPLY_UF)
+ {
+ Node op = node.getOperator();
+ Node opl = getLambdaFor(op);
+ if (!opl.isNull())
+ {
+ std::vector<Node> args(node.begin(), node.end());
+ Node app = betaReduce(opl, args);
+ Trace("uf-lazy-ll") << "Beta reduce: " << node << " -> " << app
+ << std::endl;
+ if (d_epg == nullptr)
+ {
+ return TrustNode::mkTrustRewrite(node, app);
+ }
+ return d_epg->mkTrustedRewrite(
+ node, app, PfRule::MACRO_SR_PRED_INTRO, {node.eqNode(app)});
+ }
+ }
+ // otherwise, unchanged
+ return TrustNode::null();
+}
+
+Node LambdaLift::betaReduce(TNode lam, const std::vector<Node>& args) const
+{
+ Assert(lam.getKind() == LAMBDA);
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<Node> betaRed;
+ betaRed.push_back(lam);
+ betaRed.insert(betaRed.end(), args.begin(), args.end());
+ Node app = nm->mkNode(APPLY_UF, betaRed);
+ app = rewrite(app);
+ return app;
+}
+
+} // namespace uf
+} // namespace theory
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Lambda lifting
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__UF__LAMBDA_LIFT_H
+#define CVC5__THEORY__UF__LAMBDA_LIFT_H
+
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "expr/node.h"
+#include "proof/eager_proof_generator.h"
+#include "proof/trust_node.h"
+#include "smt/env_obj.h"
+#include "theory/skolem_lemma.h"
+
+namespace cvc5 {
+namespace theory {
+namespace uf {
+
+/**
+ * Module for doing various operations on lambdas, including lambda lifting.
+ *
+ * In the following, we say a "lambda function" is a skolem variable that
+ * was introduced as a purification skolem for a lambda term.
+ */
+class LambdaLift : protected EnvObj
+{
+ typedef context::CDHashSet<Node> NodeSet;
+ typedef context::CDHashMap<Node, Node> NodeNodeMap;
+
+ public:
+ LambdaLift(Env& env);
+
+ /**
+ * process, return the trust node corresponding to the lemma for the lambda
+ * lifting of (lambda) term node, or null if it is not a lambda or if
+ * the lambda lifting lemma has already been generated in this context.
+ */
+ TrustNode lift(Node node);
+
+ /**
+ * This method has the same contract as Theory::ppRewrite.
+ * Preprocess, return the trust node corresponding to the rewrite. A null
+ * trust node indicates no rewrite.
+ */
+ TrustNode ppRewrite(Node node, std::vector<SkolemLemma>& lems);
+
+ /** Get the lambda term for skolem, if skolem is a lambda function. */
+ Node getLambdaFor(TNode skolem) const;
+
+ /**
+ * Beta-reduce node. If node is APPLY_UF and its operator is a lambda
+ * function known by this class, then this method returns the beta
+ * reduced version of node. We only beta-reduce the top-most application
+ * in node.
+ *
+ * This method returns the trust node corresponding to the rewrite of node to
+ * the return value. It returns the null trust node if no beta reduction is
+ * possible for node.
+ */
+ TrustNode betaReduce(TNode node) const;
+ /** Beta-reduce the given lambda on the given arguments. */
+ Node betaReduce(TNode lam, const std::vector<Node>& args) const;
+
+ private:
+ /**
+ * Get assertion for node, which is the axiom defining
+ */
+ static Node getAssertionFor(TNode node);
+ /** Get skolem for lambda term node, returns its purification skolem */
+ static Node getSkolemFor(TNode node);
+ /** The nodes we have already returned trust nodes for */
+ NodeSet d_lifted;
+ /** Mapping skolems to their lambda */
+ NodeNodeMap d_lambdaMap;
+ /** An eager proof generator */
+ std::unique_ptr<EagerProofGenerator> d_epg;
+};
+
+} // namespace uf
+} // namespace theory
+} // namespace cvc5
+
+#endif /* CVC5__THEORY__UF__LAMBDA_LIFT_H */
projects / cvc5.git / commitdiff