Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/lazy_proof.cpp	Lines:	96	99	97.0 %
Date:	2021-09-07	Branches:	173	356	48.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * 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.h"

#include "proof/proof_ensure_closed.h"
#include "proof/proof_node.h"
#include "proof/proof_node_manager.h"

using namespace cvc5::kind;

namespace cvc5 {

LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
                         ProofGenerator* dpg,
                         context::Context* c,
                         const std::string& name)
    : CDProof(pnm, c, name), d_gens(c ? c : &d_context), d_defaultGen(dpg)
{
}

LazyCDProof::~LazyCDProof() {}

std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
{
  Trace("lazy-cdproof") << "LazyCDProof::mkLazyProof " << fact << std::endl;
  // make the proof, which should always be non-null, since we construct an
  // assumption in the worst case.
  std::shared_ptr<ProofNode> opf = CDProof::getProofFor(fact);
  Assert(opf != nullptr);
  if (!hasGenerators())
  {
    Trace("lazy-cdproof") << "...no generators, finished" << std::endl;
    // optimization: no generators, we are done
    return opf;
  }
  // otherwise, we traverse the proof opf and fill in the ASSUME leafs that
  // have generators
  std::unordered_set<ProofNode*> visited;
  std::unordered_set<ProofNode*>::iterator it;
  std::vector<ProofNode*> visit;
  ProofNode* cur;
  visit.push_back(opf.get());
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);

    if (it == visited.end())
    {
      visited.insert(cur);
      Node cfact = cur->getResult();
      if (getProof(cfact).get() != cur)
      {
        // We don't own this proof, skip it. This is to ensure that this method
        // is idempotent, since it may be the case that a previous call to
        // getProofFor connected a proof from a proof generator as a child of
        // a ProofNode in the range of the map in CDProof. Thus, this ensures
        // we don't touch such proofs.
        Trace("lazy-cdproof") << "...skip unowned proof" << std::endl;
      }
      else if (cur->getRule() == PfRule::ASSUME)
      {
        bool isSym = false;
        ProofGenerator* pg = getGeneratorFor(cfact, isSym);
        if (pg != nullptr)
        {
          Trace("lazy-cdproof")
              << "LazyCDProof: Call generator " << pg->identify()
              << " for assumption " << cfact << std::endl;
          Node cfactGen = isSym ? CDProof::getSymmFact(cfact) : cfact;
          Assert(!cfactGen.isNull());
          // Do not use the addProofTo interface, instead use the update node
          // interface, since this ensures that we don't take ownership for
          // the current proof. Instead, it is only linked, and ignored on
          // future calls to getProofFor due to the check above.
          std::shared_ptr<ProofNode> pgc = pg->getProofFor(cfactGen);
          // If the proof was null, then the update is not performed. This is
          // not considered an error, since this behavior is equivalent to
          // if pg had provided the proof (ASSUME cfactGen). Ensuring the
          // proper behavior wrt closed proofs should be done outside this
          // method.
          if (pgc != nullptr)
          {
            Trace("lazy-cdproof-gen")
                << "LazyCDProof: stored proof: " << *pgc.get() << std::endl;

            if (isSym)
            {
              if (pgc->getRule() == PfRule::SYMM)
              {
                d_manager->updateNode(cur, pgc->getChildren()[0].get());
              }
              else
              {
                d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {});
              }
            }
            else
            {
              d_manager->updateNode(cur, pgc.get());
            }
            Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for "
                                  << cfactGen << std::endl;
          }
        }
        else
        {
          Trace("lazy-cdproof") << "LazyCDProof: " << identify()
                                << " : No generator for " << cfact << std::endl;
        }
        // Notice that we do not traverse the proofs that have been generated
        // lazily by the proof generators here.  In other words, we assume that
        // the proofs from provided proof generators are final and need
        // no further modification by this class.
      }
      else
      {
        const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
        for (const std::shared_ptr<ProofNode>& cp : cc)
        {
          visit.push_back(cp.get());
        }
      }
    }
  } while (!visit.empty());
  // we have now updated the ASSUME leafs of opf, return it
  Trace("lazy-cdproof") << "...finished" << std::endl;
  Assert(opf->getResult() == fact);
  return opf;
}

void LazyCDProof::addLazyStep(Node expected,
                              ProofGenerator* pg,
                              PfRule idNull,
                              bool isClosed,
                              const char* ctx,
                              bool forceOverwrite)
{
  if (pg == nullptr)
  {
    // null generator, should have given a proof rule
    if (idNull == PfRule::ASSUME)
    {
      Unreachable() << "LazyCDProof::addLazyStep: " << identify()
                    << ": failed to provide proof generator for " << expected;
      return;
    }
    Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
                          << " set (trusted) step " << idNull << "\n";
    addStep(expected, idNull, {}, {expected});
    return;
  }
  Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
                        << " set to generator " << pg->identify() << "\n";
  if (!forceOverwrite)
  {
    NodeProofGeneratorMap::const_iterator it = d_gens.find(expected);
    if (it != d_gens.end())
    {
      // don't overwrite something that is already there
      return;
    }
  }
  // just store now
  d_gens.insert(expected, pg);
  // debug checking
  if (isClosed)
  {
    Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl;
    pfgEnsureClosed(expected, pg, "lazy-cdproof-debug", ctx);
  }
}

ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, bool& isSym)
{
  isSym = false;
  NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
  if (it != d_gens.end())
  {
    return (*it).second;
  }
  Node factSym = CDProof::getSymmFact(fact);
  // could be symmetry
  if (factSym.isNull())
  {
    // can't be symmetry, return the default generator
    return d_defaultGen;
  }
  it = d_gens.find(factSym);
  if (it != d_gens.end())
  {
    isSym = true;
    return (*it).second;
  }
  // return the default generator
  return d_defaultGen;
}

bool LazyCDProof::hasGenerators() const
{
  return !d_gens.empty() || d_defaultGen != nullptr;
}

bool LazyCDProof::hasGenerator(Node fact) const
{
  if (d_defaultGen != nullptr)
  {
    return true;
  }
  NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
  if (it != d_gens.end())
  {
    return true;
  }
  // maybe there is a symmetric fact?
  Node factSym = CDProof::getSymmFact(fact);
  if (!factSym.isNull())
  {
    it = d_gens.find(factSym);
  }
  return it != d_gens.end();
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Aina Niemetz
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.h"
17
18		#include "proof/proof_ensure_closed.h"
19		#include "proof/proof_node.h"
20		#include "proof/proof_node_manager.h"
21
22		using namespace cvc5::kind;
23
24		namespace cvc5 {
25
26	278745	LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
27		ProofGenerator* dpg,
28		context::Context* c,
29	278745	const std::string& name)
30	278745	: CDProof(pnm, c, name), d_gens(c ? c : &d_context), d_defaultGen(dpg)
31		{
32	278745	}
33
34	335322	LazyCDProof::~LazyCDProof() {}
35
36	1616163	std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
37		{
38	1616163	Trace("lazy-cdproof") << "LazyCDProof::mkLazyProof " << fact << std::endl;
39		// make the proof, which should always be non-null, since we construct an
40		// assumption in the worst case.
41	1616163	std::shared_ptr<ProofNode> opf = CDProof::getProofFor(fact);
42	1616163	Assert(opf != nullptr);
43	1616163	if (!hasGenerators())
44		{
45	663033	Trace("lazy-cdproof") << "...no generators, finished" << std::endl;
46		// optimization: no generators, we are done
47	663033	return opf;
48		}
49		// otherwise, we traverse the proof opf and fill in the ASSUME leafs that
50		// have generators
51	1906260	std::unordered_set<ProofNode*> visited;
52	953130	std::unordered_set<ProofNode*>::iterator it;
53	1906260	std::vector<ProofNode*> visit;
54		ProofNode* cur;
55	953130	visit.push_back(opf.get());
56	57651643	do
57		{
58	58604773	cur = visit.back();
59	58604773	visit.pop_back();
60	58604773	it = visited.find(cur);
61
62	58604773	if (it == visited.end())
63		{
64	12529028	visited.insert(cur);
65	25058056	Node cfact = cur->getResult();
66	12529028	if (getProof(cfact).get() != cur)
67		{
68		// We don't own this proof, skip it. This is to ensure that this method
69		// is idempotent, since it may be the case that a previous call to
70		// getProofFor connected a proof from a proof generator as a child of
71		// a ProofNode in the range of the map in CDProof. Thus, this ensures
72		// we don't touch such proofs.
73	892534	Trace("lazy-cdproof") << "...skip unowned proof" << std::endl;
74		}
75	11636494	else if (cur->getRule() == PfRule::ASSUME)
76		{
77	1018967	bool isSym = false;
78	1018967	ProofGenerator* pg = getGeneratorFor(cfact, isSym);
79	1018967	if (pg != nullptr)
80		{
81	1787990	Trace("lazy-cdproof")
82	1787990	<< "LazyCDProof: Call generator " << pg->identify()
83	893995	<< " for assumption " << cfact << std::endl;
84	1787990	Node cfactGen = isSym ? CDProof::getSymmFact(cfact) : cfact;
85	893995	Assert(!cfactGen.isNull());
86		// Do not use the addProofTo interface, instead use the update node
87		// interface, since this ensures that we don't take ownership for
88		// the current proof. Instead, it is only linked, and ignored on
89		// future calls to getProofFor due to the check above.
90	1787990	std::shared_ptr<ProofNode> pgc = pg->getProofFor(cfactGen);
91		// If the proof was null, then the update is not performed. This is
92		// not considered an error, since this behavior is equivalent to
93		// if pg had provided the proof (ASSUME cfactGen). Ensuring the
94		// proper behavior wrt closed proofs should be done outside this
95		// method.
96	893995	if (pgc != nullptr)
97		{
98	1787990	Trace("lazy-cdproof-gen")
99	893995	<< "LazyCDProof: stored proof: " << *pgc.get() << std::endl;
100
101	893995	if (isSym)
102		{
103	4872	if (pgc->getRule() == PfRule::SYMM)
104		{
105	2	d_manager->updateNode(cur, pgc->getChildren()[0].get());
106		}
107		else
108		{
109	4870	d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {});
110		}
111		}
112		else
113		{
114	889123	d_manager->updateNode(cur, pgc.get());
115		}
116	1787990	Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for "
117	893995	<< cfactGen << std::endl;
118		}
119		}
120		else
121		{
122	249944	Trace("lazy-cdproof") << "LazyCDProof: " << identify()
123	124972	<< " : No generator for " << cfact << std::endl;
124		}
125		// Notice that we do not traverse the proofs that have been generated
126		// lazily by the proof generators here. In other words, we assume that
127		// the proofs from provided proof generators are final and need
128		// no further modification by this class.
129		}
130		else
131		{
132	10617527	const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
133	68269170	for (const std::shared_ptr<ProofNode>& cp : cc)
134		{
135	57651643	visit.push_back(cp.get());
136		}
137		}
138		}
139	58604773	} while (!visit.empty());
140		// we have now updated the ASSUME leafs of opf, return it
141	953130	Trace("lazy-cdproof") << "...finished" << std::endl;
142	953130	Assert(opf->getResult() == fact);
143	953130	return opf;
144		}
145
146	1634835	void LazyCDProof::addLazyStep(Node expected,
147		ProofGenerator* pg,
148		PfRule idNull,
149		bool isClosed,
150		const char* ctx,
151		bool forceOverwrite)
152		{
153	1634835	if (pg == nullptr)
154		{
155		// null generator, should have given a proof rule
156	30621	if (idNull == PfRule::ASSUME)
157		{
158		Unreachable() << "LazyCDProof::addLazyStep: " << identify()
159		<< ": failed to provide proof generator for " << expected;
160		return;
161		}
162	61242	Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
163	30621	<< " set (trusted) step " << idNull << "\n";
164	30621	addStep(expected, idNull, {}, {expected});
165	30621	return;
166		}
167	3208428	Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
168	1604214	<< " set to generator " << pg->identify() << "\n";
169	1604214	if (!forceOverwrite)
170		{
171	1604214	NodeProofGeneratorMap::const_iterator it = d_gens.find(expected);
172	1604214	if (it != d_gens.end())
173		{
174		// don't overwrite something that is already there
175	668505	return;
176		}
177		}
178		// just store now
179	935709	d_gens.insert(expected, pg);
180		// debug checking
181	935709	if (isClosed)
182		{
183	171982	Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl;
184	171982	pfgEnsureClosed(expected, pg, "lazy-cdproof-debug", ctx);
185		}
186		}
187
188	1018967	ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, bool& isSym)
189		{
190	1018967	isSym = false;
191	1018967	NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
192	1018967	if (it != d_gens.end())
193		{
194	144717	return (*it).second;
195		}
196	1748500	Node factSym = CDProof::getSymmFact(fact);
197		// could be symmetry
198	874250	if (factSym.isNull())
199		{
200		// can't be symmetry, return the default generator
201	257367	return d_defaultGen;
202		}
203	616883	it = d_gens.find(factSym);
204	616883	if (it != d_gens.end())
205		{
206	4872	isSym = true;
207	4872	return (*it).second;
208		}
209		// return the default generator
210	612011	return d_defaultGen;
211		}
212
213	1616163	bool LazyCDProof::hasGenerators() const
214		{
215	1616163	return !d_gens.empty() \|\| d_defaultGen != nullptr;
216		}
217
218	155419	bool LazyCDProof::hasGenerator(Node fact) const
219		{
220	155419	if (d_defaultGen != nullptr)
221		{
222		return true;
223		}
224	155419	NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
225	155419	if (it != d_gens.end())
226		{
227	1535	return true;
228		}
229		// maybe there is a symmetric fact?
230	307768	Node factSym = CDProof::getSymmFact(fact);
231	153884	if (!factSym.isNull())
232		{
233	13414	it = d_gens.find(factSym);
234		}
235	153884	return it != d_gens.end();
236		}
237
238	29502	} // namespace cvc5