Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/lazy_proof_chain.cpp	Lines:	115	159	72.3 %
Date:	2021-09-06	Branches:	168	530	31.7 %


/******************************************************************************
 * 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 " << 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;
      if (!rec)
      {
        // we don't want to recursively connect this proof
        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";
      }
      // mark for post-traversal if we are controlling cycles
      if (d_cyclic)
      {
        Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: marking "
                                   << cur << " for cycle check\n";
        visit.push_back(cur);
        visited[cur] = false;
      }
      else
      {
        visited[cur] = true;
      }
      // enqueue free assumptions to process
      for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
               fap : famap)
      {
        // check cycles
        if (d_cyclic)
        {
          // cycles are assumptions being *currently* expanded and 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, this fact will be an
            // assumption in the final proof node produced by this
            // method. Thus we erase it as something to be connected, which
            // will keep it as an assumption.
            Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: "
                                          "removing cyclic assumption "
                                       << fap.first << " from expansion\n";
            continue;
          }
        }
        // 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());
    }
  }
  // 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	14203	LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
28		bool cyclic,
29		context::Context* c,
30		ProofGenerator* defGen,
31		bool defRec,
32	14203	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	14203	d_name(name)
40		{
41	14203	}
42
43	21775	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	40417	std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
60		{
61	80834	Trace("lazy-cdproofchain")
62	40417	<< "LazyCDProofChain::getProofFor " << fact << "\n";
63		// which facts have had proofs retrieved for. This is maintained to avoid
64		// cycles. It also saves the proof node of the fact
65	80834	std::unordered_map<Node, std::shared_ptr<ProofNode>> toConnect;
66		// leaves of proof node links in the chain, i.e. assumptions, yet to be
67		// expanded
68		std::unordered_map<Node, std::vector<std::shared_ptr<ProofNode>>>
69	80834	assumptionsToExpand;
70		// invariant of the loop below, the first iteration notwithstanding:
71		// visit = domain(assumptionsToExpand) \ domain(toConnect)
72	80834	std::vector<Node> visit{fact};
73	80834	std::unordered_map<Node, bool> visited;
74	80834	Node cur;
75	1930277	do
76		{
77	1970694	cur = visit.back();
78	1970694	visit.pop_back();
79	1970694	auto itVisited = visited.find(cur);
80		// pre-traversal
81	1970694	if (itVisited == visited.end())
82		{
83	871558	Trace("lazy-cdproofchain")
84	435779	<< "LazyCDProofChain::getProofFor: check " << cur << "\n";
85	435779	Assert(toConnect.find(cur) == toConnect.end());
86	435779	bool rec = true;
87	435779	ProofGenerator* pg = getGeneratorForInternal(cur, rec);
88	670644	if (!pg)
89		{
90	469730	Trace("lazy-cdproofchain")
91	234865	<< "LazyCDProofChain::getProofFor: nothing to do\n";
92		// nothing to do for this fact, it'll be a leaf in the final proof
93		// node, don't post-traverse.
94	234865	visited[cur] = true;
95	493250	continue;
96		}
97	401828	Trace("lazy-cdproofchain")
98	401828	<< "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
99	200914	<< " for chain link " << cur << "\n";
100	378308	std::shared_ptr<ProofNode> curPfn = pg->getProofFor(cur);
101	203985	if (curPfn == nullptr)
102		{
103	6142	Trace("lazy-cdproofchain")
104	3071	<< "LazyCDProofChain::getProofFor: No proof found, skip\n";
105	3071	visited[cur] = true;
106	3071	continue;
107		}
108		// map node whose proof node must be expanded to the respective poof node
109	197843	toConnect[cur] = curPfn;
110	218292	if (!rec)
111		{
112		// we don't want to recursively connect this proof
113	20449	visited[cur] = true;
114	20449	continue;
115		}
116	354788	Trace("lazy-cdproofchain-debug")
117	177394	<< "LazyCDProofChain::getProofFor: stored proof: " << *curPfn.get()
118	177394	<< "\n";
119		// retrieve free assumptions and their respective proof nodes
120	354788	std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
121	177394	expr::getFreeAssumptionsMap(curPfn, famap);
122	177394	if (Trace.isOn("lazy-cdproofchain"))
123		{
124		unsigned alreadyToVisit = 0;
125		Trace("lazy-cdproofchain")
126		<< "LazyCDProofChain::getProofFor: " << famap.size()
127		<< " free assumptions:\n";
128		for (auto fap : famap)
129		{
130		Trace("lazy-cdproofchain")
131		<< "LazyCDProofChain::getProofFor: - " << fap.first << "\n";
132		alreadyToVisit +=
133		std::find(visit.begin(), visit.end(), fap.first) != visit.end()
134		? 1
135		: 0;
136		}
137		Trace("lazy-cdproofchain")
138		<< "LazyCDProofChain::getProofFor: " << alreadyToVisit
139		<< " already to visit\n";
140		}
141		// mark for post-traversal if we are controlling cycles
142	177394	if (d_cyclic)
143		{
144	354788	Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: marking "
145	177394	<< cur << " for cycle check\n";
146	177394	visit.push_back(cur);
147	177394	visited[cur] = false;
148		}
149		else
150		{
151		visited[cur] = true;
152		}
153		// enqueue free assumptions to process
154	1776598	for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
155	177394	fap : famap)
156		{
157		// check cycles
158	1776598	if (d_cyclic)
159		{
160		// cycles are assumptions being currently expanded and seen again,
161		// i.e. in toConnect and not yet post-visited
162	1776598	auto itToConnect = toConnect.find(fap.first);
163	1800313	if (itToConnect != toConnect.end() && !visited[fap.first])
164		{
165		// Since we have a cycle with an assumption, this fact will be an
166		// assumption in the final proof node produced by this
167		// method. Thus we erase it as something to be connected, which
168		// will keep it as an assumption.
169	47430	Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: "
170	23715	"removing cyclic assumption "
171	23715	<< fap.first << " from expansion\n";
172	23715	continue;
173		}
174		}
175		// We always add assumptions to visit so that their last seen occurrence
176		// is expanded (rather than the first seen occurrence, if we were not
177		// adding assumptions, say, in assumptionsToExpand). This is so because
178		// in the case where we are checking cycles this is necessary (and
179		// harmless when we are not). For example the cycle
180		//
181		// a2
182		// ...
183		// ----
184		// a1
185		// ...
186		// --------
187		// a0 a1 a2
188		// ...
189		// ---------------
190		// n
191		//
192		// in which a2 has a1 as an assumption, which has a2 an assumption,
193		// would not be captured if we did not revisit a1, which is an
194		// assumption of n and this already occur in assumptionsToExpand when
195		// it shows up again as an assumption of a2.
196	1752883	visit.push_back(fap.first);
197		// add assumption proof nodes to be updated
198	3505766	assumptionsToExpand[fap.first].insert(
199	3505766	assumptionsToExpand[fap.first].end(),
200		fap.second.begin(),
201	5258649	fap.second.end());
202		}
203	177394	if (d_cyclic)
204		{
205	177394	Trace("lazy-cdproofchain") << push;
206	177394	Trace("lazy-cdproofchain-debug") << push;
207		}
208		}
209	1534915	else if (!itVisited->second)
210		{
211	177394	visited[cur] = true;
212	177394	Trace("lazy-cdproofchain") << pop;
213	177394	Trace("lazy-cdproofchain-debug") << pop;
214	354788	Trace("lazy-cdproofchain")
215	177394	<< "LazyCDProofChain::getProofFor: post-visited " << cur << "\n";
216		}
217		else
218		{
219	2715042	Trace("lazy-cdproofchain")
220	1357521	<< "LazyCDProofChain::getProofFor: already fully processed " << cur
221	1357521	<< "\n";
222		}
223	1970694	} while (!visit.empty());
224		// expand all assumptions marked to be connected
225	197843	for (const std::pair<const Node, std::shared_ptr<ProofNode>>& npfn :
226	40417	toConnect)
227		{
228	197843	auto it = assumptionsToExpand.find(npfn.first);
229	237396	if (it == assumptionsToExpand.end())
230		{
231	39553	Assert(npfn.first == fact);
232	39553	continue;
233		}
234	158290	Assert(npfn.second);
235	316580	Trace("lazy-cdproofchain")
236	158290	<< "LazyCDProofChain::getProofFor: expand assumption " << npfn.first
237	158290	<< "\n";
238	316580	Trace("lazy-cdproofchain-debug")
239	158290	<< "LazyCDProofChain::getProofFor: ...expand to " << *npfn.second.get()
240	158290	<< "\n";
241		// update each assumption proof node
242	542778	for (std::shared_ptr<ProofNode> pfn : it->second)
243		{
244	384488	d_manager->updateNode(pfn.get(), npfn.second.get());
245		}
246		}
247		// final proof of fact
248	40417	auto it = toConnect.find(fact);
249	40417	if (it == toConnect.end())
250		{
251	864	return nullptr;
252		}
253	39553	return it->second;
254		}
255
256	76432	void LazyCDProofChain::addLazyStep(Node expected, ProofGenerator* pg)
257		{
258	76432	Assert(pg != nullptr);
259	152864	Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
260	76432	<< " set to generator " << pg->identify() << "\n";
261		// note this will replace the generator for expected, if any
262	76432	d_gens.insert(expected, pg);
263	76432	}
264
265		void LazyCDProofChain::addLazyStep(Node expected,
266		ProofGenerator* pg,
267		const std::vector<Node>& assumptions,
268		const char* ctx)
269		{
270		Assert(pg != nullptr);
271		Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
272		<< " set to generator " << pg->identify() << "\n";
273		// note this will rewrite the generator for expected, if any
274		d_gens.insert(expected, pg);
275		// check if chain is closed if eager checking is on
276		if (options::proofCheck() == options::ProofCheckMode::EAGER)
277		{
278		Trace("lazy-cdproofchain")
279		<< "LazyCDProofChain::addLazyStep: Checking closed proof...\n";
280		std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected);
281		std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()};
282		// add all current links in the chain
283		for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
284		{
285		allowedLeaves.push_back(link.first);
286		}
287		if (Trace.isOn("lazy-cdproofchain"))
288		{
289		Trace("lazy-cdproofchain") << "Checking relative to leaves...\n";
290		for (const Node& n : allowedLeaves)
291		{
292		Trace("lazy-cdproofchain") << " - " << n << "\n";
293		}
294		Trace("lazy-cdproofchain") << "\n";
295		}
296		pfnEnsureClosedWrt(pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx);
297		}
298		}
299
300	23838	bool LazyCDProofChain::hasGenerator(Node fact) const
301		{
302	23838	return d_gens.find(fact) != d_gens.end();
303		}
304
305		ProofGenerator* LazyCDProofChain::getGeneratorFor(Node fact)
306		{
307		bool rec = true;
308		return getGeneratorForInternal(fact, rec);
309		}
310
311	435779	ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec)
312		{
313	435779	auto it = d_gens.find(fact);
314	435779	if (it != d_gens.end())
315		{
316	155257	return (*it).second;
317		}
318		// otherwise, if no explicit generators, we use the default one
319	280522	if (d_defGen != nullptr)
320		{
321	45657	rec = d_defRec;
322	45657	return d_defGen;
323		}
324	234865	return nullptr;
325		}
326
327	72703	std::string LazyCDProofChain::identify() const { return d_name; }
328
329	29508	} // namespace cvc5