Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/lazy_proof_chain.cpp	Lines:	145	174	83.3 %
Date:	2021-11-07	Branches:	227	582	39.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Haniel Barbosa, Andrew Reynolds, Gereon Kremer
 *
 * 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 lazy proof utility.
 */

#include "proof/lazy_proof_chain.h"

#include "options/proof_options.h"
#include "proof/proof.h"
#include "proof/proof_ensure_closed.h"
#include "proof/proof_node.h"
#include "proof/proof_node_algorithm.h"
#include "proof/proof_node_manager.h"

namespace cvc5 {

LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
                                   bool cyclic,
                                   context::Context* c,
                                   ProofGenerator* defGen,
                                   bool defRec,
                                   const std::string& name)
    : d_manager(pnm),
      d_cyclic(cyclic),
      d_defRec(defRec),
      d_context(),
      d_gens(c ? c : &d_context),
      d_defGen(defGen),
      d_name(name)
{
}

LazyCDProofChain::~LazyCDProofChain() {}

const std::map<Node, std::shared_ptr<ProofNode>> LazyCDProofChain::getLinks()
    const
{
  std::map<Node, std::shared_ptr<ProofNode>> links;
  for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
  {
    Assert(link.second);
    std::shared_ptr<ProofNode> pfn = link.second->getProofFor(link.first);
    Assert(pfn);
    links[link.first] = pfn;
  }
  return links;
}

std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
{
  Trace("lazy-cdproofchain")
      << "LazyCDProofChain::getProofFor of gen " << d_name << "\n";
  Trace("lazy-cdproofchain")
      << "LazyCDProofChain::getProofFor: " << fact << "\n";
  // which facts have had proofs retrieved for. This is maintained to avoid
  // cycles. It also saves the proof node of the fact
  std::unordered_map<Node, std::shared_ptr<ProofNode>> toConnect;
  // leaves of proof node links in the chain, i.e. assumptions, yet to be
  // expanded
  std::unordered_map<Node, std::vector<std::shared_ptr<ProofNode>>>
      assumptionsToExpand;
  // invariant of the loop below, the first iteration notwithstanding:
  //   visit = domain(assumptionsToExpand) \ domain(toConnect)
  std::vector<Node> visit{fact};
  std::unordered_map<Node, bool> visited;
  Node cur;
  do
  {
    cur = visit.back();
    visit.pop_back();
    auto itVisited = visited.find(cur);
    // pre-traversal
    if (itVisited == visited.end())
    {
      Trace("lazy-cdproofchain")
          << "LazyCDProofChain::getProofFor: check " << cur << "\n";
      Assert(toConnect.find(cur) == toConnect.end());
      bool rec = true;
      ProofGenerator* pg = getGeneratorForInternal(cur, rec);
      if (!pg)
      {
        Trace("lazy-cdproofchain")
            << "LazyCDProofChain::getProofFor: nothing to do\n";
        // nothing to do for this fact, it'll be a leaf in the final proof
        // node, don't post-traverse.
        visited[cur] = true;
        continue;
      }
      Trace("lazy-cdproofchain")
          << "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
          << " for chain link " << cur << "\n";
      std::shared_ptr<ProofNode> curPfn = pg->getProofFor(cur);
      if (curPfn == nullptr)
      {
        Trace("lazy-cdproofchain")
            << "LazyCDProofChain::getProofFor: No proof found, skip\n";
        visited[cur] = true;
        continue;
      }
      // map node whose proof node must be expanded to the respective poof node
      toConnect[cur] = curPfn;
      // We may not want to recursively connect this proof or, if it's
      // assumption, there is nothing to connect, so we skip. Note that in the
      // special case in which curPfn is an assumption and cur is actually the
      // initial fact that getProofFor is called on, the cycle detection below
      // would prevent this method from generating the assumption proof for it,
      // which would be wrong.
      if (!rec || curPfn->getRule() == PfRule::ASSUME)
      {
        visited[cur] = true;
        continue;
      }
      Trace("lazy-cdproofchain-debug")
          << "LazyCDProofChain::getProofFor: stored proof: " << *curPfn.get()
          << "\n";
      // retrieve free assumptions and their respective proof nodes
      std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
      expr::getFreeAssumptionsMap(curPfn, famap);
      if (Trace.isOn("lazy-cdproofchain"))
      {
        unsigned alreadyToVisit = 0;
        Trace("lazy-cdproofchain")
            << "LazyCDProofChain::getProofFor: " << famap.size()
            << " free assumptions:\n";
        for (auto fap : famap)
        {
          Trace("lazy-cdproofchain")
              << "LazyCDProofChain::getProofFor:  - " << fap.first << "\n";
          alreadyToVisit +=
              std::find(visit.begin(), visit.end(), fap.first) != visit.end()
                  ? 1
                  : 0;
        }
        Trace("lazy-cdproofchain")
            << "LazyCDProofChain::getProofFor: " << alreadyToVisit
            << " already to visit\n";
      }
      // If we are controlling cycle, check whether any of the assumptions of
      // cur would provoke a cycle. In such a case we treat cur as an
      // assumption, removing it from toConnect, and do not proceed to expand
      // any of its assumptions.
      if (d_cyclic)
      {
        Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: marking "
                                   << cur << " for cycle check\n";
        bool isCyclic = false;
        // enqueue free assumptions to process
        for (const auto& fap : famap)
        {
          // A cycle is characterized by cur having an assumption being
          // *currently* expanded that is seen again, i.e. in toConnect and not
          // yet post-visited
          auto itToConnect = toConnect.find(fap.first);
          if (itToConnect != toConnect.end() && !visited[fap.first])
          {
            // Since we have a cycle with an assumption, cur will be an
            // assumption in the final proof node produced by this
            // method.
            Trace("lazy-cdproofchain")
                << "LazyCDProofChain::getProofFor: cyclic assumption "
                << fap.first << "\n";
            isCyclic = true;
            break;
          }
        }
        if (isCyclic)
        {
          visited[cur] = true;
          Trace("lazy-cdproofchain")
              << "LazyCDProofChain::getProofFor: Removing " << cur
              << " from toConnect\n";
          auto itToConnect = toConnect.find(cur);
          toConnect.erase(itToConnect);
          continue;
        }
        visit.push_back(cur);
        visited[cur] = false;
      }
      else
      {
        visited[cur] = true;
      }
      // enqueue free assumptions to process
      for (const auto& fap : famap)
      {
        Trace("lazy-cdproofchain")
            << "LazyCDProofChain::getProofFor: marking " << fap.first
            << " for revisit and for expansion\n";
        // We always add assumptions to visit so that their last seen occurrence
        // is expanded (rather than the first seen occurrence, if we were not
        // adding assumptions, say, in assumptionsToExpand). This is so because
        // in the case where we are checking cycles this is necessary (and
        // harmless when we are not). For example the cycle
        //
        //                 a2
        //                ...
        //               ----
        //                a1
        //               ...
        //             --------
        //   a0   a1    a2
        //       ...
        //  ---------------
        //       n
        //
        // in which a2 has a1 as an assumption, which has a2 an assumption,
        // would not be captured if we did not revisit a1, which is an
        // assumption of n and this already occur in assumptionsToExpand when
        // it shows up again as an assumption of a2.
        visit.push_back(fap.first);
        // add assumption proof nodes to be updated
        assumptionsToExpand[fap.first].insert(
            assumptionsToExpand[fap.first].end(),
            fap.second.begin(),
            fap.second.end());
      }
      if (d_cyclic)
      {
        Trace("lazy-cdproofchain") << push;
        Trace("lazy-cdproofchain-debug") << push;
      }
    }
    else if (!itVisited->second)
    {
      visited[cur] = true;
      Trace("lazy-cdproofchain") << pop;
      Trace("lazy-cdproofchain-debug") << pop;
      Trace("lazy-cdproofchain")
          << "LazyCDProofChain::getProofFor: post-visited " << cur << "\n";
    }
    else
    {
      Trace("lazy-cdproofchain")
          << "LazyCDProofChain::getProofFor: already fully processed " << cur
          << "\n";
    }
  } while (!visit.empty());
  // expand all assumptions marked to be connected
  for (const std::pair<const Node, std::shared_ptr<ProofNode>>& npfn :
       toConnect)
  {
    auto it = assumptionsToExpand.find(npfn.first);
    if (it == assumptionsToExpand.end())
    {
      Assert(npfn.first == fact);
      continue;
    }
    Assert(npfn.second);
    Trace("lazy-cdproofchain")
        << "LazyCDProofChain::getProofFor: expand assumption " << npfn.first
        << "\n";
    Trace("lazy-cdproofchain-debug")
        << "LazyCDProofChain::getProofFor: ...expand to " << *npfn.second.get()
        << "\n";
    // update each assumption proof node
    for (std::shared_ptr<ProofNode> pfn : it->second)
    {
      d_manager->updateNode(pfn.get(), npfn.second.get());
    }
  }
  Trace("lazy-cdproofchain") << "===========\n";
  // final proof of fact
  auto it = toConnect.find(fact);
  if (it == toConnect.end())
  {
    return nullptr;
  }
  return it->second;
}

void LazyCDProofChain::addLazyStep(Node expected, ProofGenerator* pg)
{
  Assert(pg != nullptr);
  Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
                             << " set to generator " << pg->identify() << "\n";
  // note this will replace the generator for expected, if any
  d_gens.insert(expected, pg);
}

void LazyCDProofChain::addLazyStep(Node expected,
                                   ProofGenerator* pg,
                                   const std::vector<Node>& assumptions,
                                   const char* ctx)
{
  Assert(pg != nullptr);
  Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
                             << " set to generator " << pg->identify() << "\n";
  // note this will rewrite the generator for expected, if any
  d_gens.insert(expected, pg);
  // check if chain is closed if eager checking is on
  if (options::proofCheck() == options::ProofCheckMode::EAGER)
  {
    Trace("lazy-cdproofchain")
        << "LazyCDProofChain::addLazyStep: Checking closed proof...\n";
    std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected);
    std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()};
    // add all current links in the chain
    for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
    {
      allowedLeaves.push_back(link.first);
    }
    if (Trace.isOn("lazy-cdproofchain"))
    {
      Trace("lazy-cdproofchain") << "Checking relative to leaves...\n";
      for (const Node& n : allowedLeaves)
      {
        Trace("lazy-cdproofchain") << "  - " << n << "\n";
      }
      Trace("lazy-cdproofchain") << "\n";
    }
    pfnEnsureClosedWrt(pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx);
  }
}

bool LazyCDProofChain::hasGenerator(Node fact) const
{
  return d_gens.find(fact) != d_gens.end();
}

ProofGenerator* LazyCDProofChain::getGeneratorFor(Node fact)
{
  bool rec = true;
  return getGeneratorForInternal(fact, rec);
}

ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec)
{
  auto it = d_gens.find(fact);
  if (it != d_gens.end())
  {
    return (*it).second;
  }
  // otherwise, if no explicit generators, we use the default one
  if (d_defGen != nullptr)
  {
    rec = d_defRec;
    return d_defGen;
  }
  return nullptr;
}

std::string LazyCDProofChain::identify() const { return d_name; }

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Haniel Barbosa, Andrew Reynolds, Gereon Kremer
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 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 lazy proof utility.
14		*/
15
16		#include "proof/lazy_proof_chain.h"
17
18		#include "options/proof_options.h"
19		#include "proof/proof.h"
20		#include "proof/proof_ensure_closed.h"
21		#include "proof/proof_node.h"
22		#include "proof/proof_node_algorithm.h"
23		#include "proof/proof_node_manager.h"
24
25		namespace cvc5 {
26
27	26826	LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
28		bool cyclic,
29		context::Context* c,
30		ProofGenerator* defGen,
31		bool defRec,
32	26826	const std::string& name)
33		: d_manager(pnm),
34		d_cyclic(cyclic),
35		d_defRec(defRec),
36		d_context(),
37		d_gens(c ? c : &d_context),
38		d_defGen(defGen),
39	26826	d_name(name)
40		{
41	26826	}
42
43	42804	LazyCDProofChain::~LazyCDProofChain() {}
44
45		const std::map<Node, std::shared_ptr<ProofNode>> LazyCDProofChain::getLinks()
46		const
47		{
48		std::map<Node, std::shared_ptr<ProofNode>> links;
49		for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
50		{
51		Assert(link.second);
52		std::shared_ptr<ProofNode> pfn = link.second->getProofFor(link.first);
53		Assert(pfn);
54		links[link.first] = pfn;
55		}
56		return links;
57		}
58
59	53765	std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
60		{
61	107530	Trace("lazy-cdproofchain")
62	53765	<< "LazyCDProofChain::getProofFor of gen " << d_name << "\n";
63	107530	Trace("lazy-cdproofchain")
64	53765	<< "LazyCDProofChain::getProofFor: " << fact << "\n";
65		// which facts have had proofs retrieved for. This is maintained to avoid
66		// cycles. It also saves the proof node of the fact
67	107530	std::unordered_map<Node, std::shared_ptr<ProofNode>> toConnect;
68		// leaves of proof node links in the chain, i.e. assumptions, yet to be
69		// expanded
70		std::unordered_map<Node, std::vector<std::shared_ptr<ProofNode>>>
71	107530	assumptionsToExpand;
72		// invariant of the loop below, the first iteration notwithstanding:
73		// visit = domain(assumptionsToExpand) \ domain(toConnect)
74	107530	std::vector<Node> visit{fact};
75	107530	std::unordered_map<Node, bool> visited;
76	107530	Node cur;
77	1733499	do
78		{
79	1787264	cur = visit.back();
80	1787264	visit.pop_back();
81	1787264	auto itVisited = visited.find(cur);
82		// pre-traversal
83	1787264	if (itVisited == visited.end())
84		{
85	896266	Trace("lazy-cdproofchain")
86	448133	<< "LazyCDProofChain::getProofFor: check " << cur << "\n";
87	448133	Assert(toConnect.find(cur) == toConnect.end());
88	448133	bool rec = true;
89	448133	ProofGenerator* pg = getGeneratorForInternal(cur, rec);
90	679602	if (!pg)
91		{
92	462938	Trace("lazy-cdproofchain")
93	231469	<< "LazyCDProofChain::getProofFor: nothing to do\n";
94		// nothing to do for this fact, it'll be a leaf in the final proof
95		// node, don't post-traverse.
96	231469	visited[cur] = true;
97	515636	continue;
98		}
99	433328	Trace("lazy-cdproofchain")
100	433328	<< "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
101	216664	<< " for chain link " << cur << "\n";
102	380630	std::shared_ptr<ProofNode> curPfn = pg->getProofFor(cur);
103	220772	if (curPfn == nullptr)
104		{
105	8216	Trace("lazy-cdproofchain")
106	4108	<< "LazyCDProofChain::getProofFor: No proof found, skip\n";
107	4108	visited[cur] = true;
108	4108	continue;
109		}
110		// map node whose proof node must be expanded to the respective poof node
111	212556	toConnect[cur] = curPfn;
112		// We may not want to recursively connect this proof or, if it's
113		// assumption, there is nothing to connect, so we skip. Note that in the
114		// special case in which curPfn is an assumption and cur is actually the
115		// initial fact that getProofFor is called on, the cycle detection below
116		// would prevent this method from generating the assumption proof for it,
117		// which would be wrong.
118	261136	if (!rec \|\| curPfn->getRule() == PfRule::ASSUME)
119		{
120	48580	visited[cur] = true;
121	48580	continue;
122		}
123	327952	Trace("lazy-cdproofchain-debug")
124	163976	<< "LazyCDProofChain::getProofFor: stored proof: " << *curPfn.get()
125	163976	<< "\n";
126		// retrieve free assumptions and their respective proof nodes
127	327942	std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
128	163976	expr::getFreeAssumptionsMap(curPfn, famap);
129	163976	if (Trace.isOn("lazy-cdproofchain"))
130		{
131		unsigned alreadyToVisit = 0;
132		Trace("lazy-cdproofchain")
133		<< "LazyCDProofChain::getProofFor: " << famap.size()
134		<< " free assumptions:\n";
135		for (auto fap : famap)
136		{
137		Trace("lazy-cdproofchain")
138		<< "LazyCDProofChain::getProofFor: - " << fap.first << "\n";
139		alreadyToVisit +=
140		std::find(visit.begin(), visit.end(), fap.first) != visit.end()
141		? 1
142		: 0;
143		}
144		Trace("lazy-cdproofchain")
145		<< "LazyCDProofChain::getProofFor: " << alreadyToVisit
146		<< " already to visit\n";
147		}
148		// If we are controlling cycle, check whether any of the assumptions of
149		// cur would provoke a cycle. In such a case we treat cur as an
150		// assumption, removing it from toConnect, and do not proceed to expand
151		// any of its assumptions.
152	163976	if (d_cyclic)
153		{
154	327952	Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: marking "
155	163976	<< cur << " for cycle check\n";
156	163976	bool isCyclic = false;
157		// enqueue free assumptions to process
158	1733509	for (const auto& fap : famap)
159		{
160		// A cycle is characterized by cur having an assumption being
161		// currently expanded that is seen again, i.e. in toConnect and not
162		// yet post-visited
163	1569543	auto itToConnect = toConnect.find(fap.first);
164	1569543	if (itToConnect != toConnect.end() && !visited[fap.first])
165		{
166		// Since we have a cycle with an assumption, cur will be an
167		// assumption in the final proof node produced by this
168		// method.
169	20	Trace("lazy-cdproofchain")
170	10	<< "LazyCDProofChain::getProofFor: cyclic assumption "
171	10	<< fap.first << "\n";
172	10	isCyclic = true;
173	10	break;
174		}
175		}
176	163976	if (isCyclic)
177		{
178	10	visited[cur] = true;
179	20	Trace("lazy-cdproofchain")
180	10	<< "LazyCDProofChain::getProofFor: Removing " << cur
181	10	<< " from toConnect\n";
182	10	auto itToConnect = toConnect.find(cur);
183	10	toConnect.erase(itToConnect);
184	10	continue;
185		}
186	163966	visit.push_back(cur);
187	163966	visited[cur] = false;
188		}
189		else
190		{
191		visited[cur] = true;
192		}
193		// enqueue free assumptions to process
194	1733499	for (const auto& fap : famap)
195		{
196	3139066	Trace("lazy-cdproofchain")
197	1569533	<< "LazyCDProofChain::getProofFor: marking " << fap.first
198	1569533	<< " for revisit and for expansion\n";
199		// We always add assumptions to visit so that their last seen occurrence
200		// is expanded (rather than the first seen occurrence, if we were not
201		// adding assumptions, say, in assumptionsToExpand). This is so because
202		// in the case where we are checking cycles this is necessary (and
203		// harmless when we are not). For example the cycle
204		//
205		// a2
206		// ...
207		// ----
208		// a1
209		// ...
210		// --------
211		// a0 a1 a2
212		// ...
213		// ---------------
214		// n
215		//
216		// in which a2 has a1 as an assumption, which has a2 an assumption,
217		// would not be captured if we did not revisit a1, which is an
218		// assumption of n and this already occur in assumptionsToExpand when
219		// it shows up again as an assumption of a2.
220	1569533	visit.push_back(fap.first);
221		// add assumption proof nodes to be updated
222	3139066	assumptionsToExpand[fap.first].insert(
223	3139066	assumptionsToExpand[fap.first].end(),
224		fap.second.begin(),
225	4708599	fap.second.end());
226		}
227	163966	if (d_cyclic)
228		{
229	163966	Trace("lazy-cdproofchain") << push;
230	163966	Trace("lazy-cdproofchain-debug") << push;
231		}
232		}
233	1339131	else if (!itVisited->second)
234		{
235	163966	visited[cur] = true;
236	163966	Trace("lazy-cdproofchain") << pop;
237	163966	Trace("lazy-cdproofchain-debug") << pop;
238	327932	Trace("lazy-cdproofchain")
239	163966	<< "LazyCDProofChain::getProofFor: post-visited " << cur << "\n";
240		}
241		else
242		{
243	2350330	Trace("lazy-cdproofchain")
244	1175165	<< "LazyCDProofChain::getProofFor: already fully processed " << cur
245	1175165	<< "\n";
246		}
247	1787264	} while (!visit.empty());
248		// expand all assumptions marked to be connected
249	212546	for (const std::pair<const Node, std::shared_ptr<ProofNode>>& npfn :
250	53765	toConnect)
251		{
252	212546	auto it = assumptionsToExpand.find(npfn.first);
253	260137	if (it == assumptionsToExpand.end())
254		{
255	47591	Assert(npfn.first == fact);
256	47591	continue;
257		}
258	164955	Assert(npfn.second);
259	329910	Trace("lazy-cdproofchain")
260	164955	<< "LazyCDProofChain::getProofFor: expand assumption " << npfn.first
261	164955	<< "\n";
262	329910	Trace("lazy-cdproofchain-debug")
263	164955	<< "LazyCDProofChain::getProofFor: ...expand to " << *npfn.second.get()
264	164955	<< "\n";
265		// update each assumption proof node
266	534889	for (std::shared_ptr<ProofNode> pfn : it->second)
267		{
268	369934	d_manager->updateNode(pfn.get(), npfn.second.get());
269		}
270		}
271	53765	Trace("lazy-cdproofchain") << "===========\n";
272		// final proof of fact
273	53765	auto it = toConnect.find(fact);
274	53765	if (it == toConnect.end())
275		{
276	6174	return nullptr;
277		}
278	47591	return it->second;
279		}
280
281	83291	void LazyCDProofChain::addLazyStep(Node expected, ProofGenerator* pg)
282		{
283	83291	Assert(pg != nullptr);
284	166582	Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
285	83291	<< " set to generator " << pg->identify() << "\n";
286		// note this will replace the generator for expected, if any
287	83291	d_gens.insert(expected, pg);
288	83291	}
289
290	3	void LazyCDProofChain::addLazyStep(Node expected,
291		ProofGenerator* pg,
292		const std::vector<Node>& assumptions,
293		const char* ctx)
294		{
295	3	Assert(pg != nullptr);
296	6	Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
297	3	<< " set to generator " << pg->identify() << "\n";
298		// note this will rewrite the generator for expected, if any
299	3	d_gens.insert(expected, pg);
300		// check if chain is closed if eager checking is on
301	3	if (options::proofCheck() == options::ProofCheckMode::EAGER)
302		{
303	6	Trace("lazy-cdproofchain")
304	3	<< "LazyCDProofChain::addLazyStep: Checking closed proof...\n";
305	6	std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected);
306	6	std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()};
307		// add all current links in the chain
308	12	for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
309		{
310	9	allowedLeaves.push_back(link.first);
311		}
312	3	if (Trace.isOn("lazy-cdproofchain"))
313		{
314		Trace("lazy-cdproofchain") << "Checking relative to leaves...\n";
315		for (const Node& n : allowedLeaves)
316		{
317		Trace("lazy-cdproofchain") << " - " << n << "\n";
318		}
319		Trace("lazy-cdproofchain") << "\n";
320		}
321	3	pfnEnsureClosedWrt(pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx);
322		}
323	3	}
324
325	21899	bool LazyCDProofChain::hasGenerator(Node fact) const
326		{
327	21899	return d_gens.find(fact) != d_gens.end();
328		}
329
330		ProofGenerator* LazyCDProofChain::getGeneratorFor(Node fact)
331		{
332		bool rec = true;
333		return getGeneratorForInternal(fact, rec);
334		}
335
336	448133	ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec)
337		{
338	448133	auto it = d_gens.find(fact);
339	448133	if (it != d_gens.end())
340		{
341	154131	return (*it).second;
342		}
343		// otherwise, if no explicit generators, we use the default one
344	294002	if (d_defGen != nullptr)
345		{
346	62533	rec = d_defRec;
347	62533	return d_defGen;
348		}
349	231469	return nullptr;
350		}
351
352	85378	std::string LazyCDProofChain::identify() const { return d_name; }
353
354	31137	} // namespace cvc5