Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/proof_node_manager.cpp	Lines:	146	189	77.2 %
Date:	2021-05-24	Branches:	238	810	29.4 %


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

#include "expr/proof_node_manager.h"

#include <sstream>

#include "expr/proof.h"
#include "expr/proof_checker.h"
#include "expr/proof_node.h"
#include "expr/proof_node_algorithm.h"
#include "options/proof_options.h"
#include "theory/rewriter.h"

using namespace cvc5::kind;

namespace cvc5 {

ProofNodeManager::ProofNodeManager(ProofChecker* pc)
    : d_checker(pc)
{
  d_true = NodeManager::currentNM()->mkConst(true);
}

std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
    PfRule id,
    const std::vector<std::shared_ptr<ProofNode>>& children,
    const std::vector<Node>& args,
    Node expected)
{
  Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId()
               << "} " << expected << "\n";
  Node res = checkInternal(id, children, args, expected);
  if (res.isNull())
  {
    // if it was invalid, then we return the null node
    return nullptr;
  }
  // otherwise construct the proof node and set its proven field
  std::shared_ptr<ProofNode> pn =
      std::make_shared<ProofNode>(id, children, args);
  pn->d_proven = res;
  return pn;
}

std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact)
{
  Assert(!fact.isNull());
  Assert(fact.getType().isBoolean());
  return mkNode(PfRule::ASSUME, {}, {fact}, fact);
}

std::shared_ptr<ProofNode> ProofNodeManager::mkTrans(
    const std::vector<std::shared_ptr<ProofNode>>& children, Node expected)
{
  Assert(!children.empty());
  if (children.size() == 1)
  {
    Assert(expected.isNull() || children[0]->getResult() == expected);
    return children[0];
  }
  return mkNode(PfRule::TRANS, children, {}, expected);
}

std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
    std::shared_ptr<ProofNode> pf,
    std::vector<Node>& assumps,
    bool ensureClosed,
    bool doMinimize,
    Node expected)
{
  if (!ensureClosed)
  {
    return mkNode(PfRule::SCOPE, {pf}, assumps, expected);
  }
  Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl;
  // we first ensure the assumptions are flattened
  std::unordered_set<Node> ac{assumps.begin(), assumps.end()};
  // map from the rewritten form of assumptions to the original. This is only
  // computed in the rare case when we need rewriting to match the
  // assumptions. An example of this is for Boolean constant equalities in
  // scoped proofs from the proof equality engine.
  std::unordered_map<Node, Node> acr;
  // whether we have compute the map above
  bool computedAcr = false;

  // The free assumptions of the proof
  std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
  expr::getFreeAssumptionsMap(pf, famap);
  std::unordered_set<Node> acu;
  for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
           fa : famap)
  {
    Node a = fa.first;
    if (ac.find(a) != ac.end())
    {
      // already covered by an assumption
      acu.insert(a);
      continue;
    }
    // trivial assumption
    if (a == d_true)
    {
      Trace("pnm-scope") << "- justify trivial True assumption\n";
      for (std::shared_ptr<ProofNode> pfs : fa.second)
      {
        Assert(pfs->getResult() == a);
        updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a});
      }
      Trace("pnm-scope") << "...finished" << std::endl;
      acu.insert(a);
      continue;
    }
    Trace("pnm-scope") << "- try matching free assumption " << a << "\n";
    // otherwise it may be due to symmetry?
    Node aeqSym = CDProof::getSymmFact(a);
    Trace("pnm-scope") << "  - try sym " << aeqSym << "\n";
    Node aMatch;
    if (!aeqSym.isNull() && ac.count(aeqSym))
    {
      Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a
                         << " for " << fa.second.size() << " proof nodes"
                         << std::endl;
      aMatch = aeqSym;
    }
    else
    {
      // Otherwise, may be derivable by rewriting. Note this is used in
      // ensuring that proofs from the proof equality engine that involve
      // equality with Boolean constants are closed.
      if (!computedAcr)
      {
        computedAcr = true;
        for (const Node& acc : ac)
        {
          Node accr = theory::Rewriter::rewrite(acc);
          if (accr != acc)
          {
            acr[accr] = acc;
          }
        }
      }
      Node ar = theory::Rewriter::rewrite(a);
      std::unordered_map<Node, Node>::iterator itr = acr.find(ar);
      if (itr != acr.end())
      {
        aMatch = itr->second;
      }
    }

    // if we found a match either by symmetry or rewriting, then we connect
    // the assumption here.
    if (!aMatch.isNull())
    {
      std::shared_ptr<ProofNode> pfaa = mkAssume(aMatch);
      // must correct the orientation on this leaf
      std::vector<std::shared_ptr<ProofNode>> children;
      children.push_back(pfaa);
      for (std::shared_ptr<ProofNode> pfs : fa.second)
      {
        Assert(pfs->getResult() == a);
        // use SYMM if possible
        if (aMatch == aeqSym)
        {
          updateNode(pfs.get(), PfRule::SYMM, children, {});
        }
        else
        {
          updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, {a});
        }
      }
      Trace("pnm-scope") << "...finished" << std::endl;
      acu.insert(aMatch);
      continue;
    }
    // If we did not find a match, it is an error, since all free assumptions
    // should be arguments to SCOPE.
    std::stringstream ss;

    bool dumpProofTraceOn = Trace.isOn("dump-proof-error");
    if (dumpProofTraceOn)
    {
      ss << "The proof : " << *pf << std::endl;
    }
    ss << std::endl << "Free assumption: " << a << std::endl;
    for (const Node& aprint : ac)
    {
      ss << "- assumption: " << aprint << std::endl;
    }
    if (!dumpProofTraceOn)
    {
      ss << "Use -t dump-proof-error for details on proof" << std::endl;
    }
    Unreachable() << "Generated a proof that is not closed by the scope: "
                  << ss.str() << std::endl;
  }
  if (acu.size() < ac.size())
  {
    // All assumptions should match a free assumption; if one does not, then
    // the explanation could have been smaller.
    for (const Node& a : ac)
    {
      if (acu.find(a) == acu.end())
      {
        Notice() << "ProofNodeManager::mkScope: assumption " << a
                 << " does not match a free assumption in proof" << std::endl;
      }
    }
  }
  if (doMinimize && acu.size() < ac.size())
  {
    assumps.clear();
    assumps.insert(assumps.end(), acu.begin(), acu.end());
  }
  else if (ac.size() < assumps.size())
  {
    // remove duplicates to avoid redundant literals in clauses
    assumps.clear();
    assumps.insert(assumps.end(), ac.begin(), ac.end());
  }
  Node minExpected;
  NodeManager* nm = NodeManager::currentNM();
  Node exp;
  if (assumps.empty())
  {
    // SCOPE with no arguments is a no-op, just return original
    return pf;
  }
  Node conc = pf->getResult();
  exp = assumps.size() == 1 ? assumps[0] : nm->mkNode(AND, assumps);
  if (conc.isConst() && !conc.getConst<bool>())
  {
    minExpected = exp.notNode();
  }
  else
  {
    minExpected = nm->mkNode(IMPLIES, exp, conc);
  }
  return mkNode(PfRule::SCOPE, {pf}, assumps, minExpected);
}

bool ProofNodeManager::updateNode(
    ProofNode* pn,
    PfRule id,
    const std::vector<std::shared_ptr<ProofNode>>& children,
    const std::vector<Node>& args)
{
  return updateNodeInternal(pn, id, children, args, true);
}

bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr)
{
  Assert(pn != nullptr);
  Assert(pnr != nullptr);
  if (pn->getResult() != pnr->getResult())
  {
    return false;
  }
  // can shortcut re-check of rule
  return updateNodeInternal(
      pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false);
}

Node ProofNodeManager::checkInternal(
    PfRule id,
    const std::vector<std::shared_ptr<ProofNode>>& children,
    const std::vector<Node>& args,
    Node expected)
{
  Node res;
  if (d_checker)
  {
    // check with the checker, which takes expected as argument
    res = d_checker->check(id, children, args, expected);
    Assert(!res.isNull())
        << "ProofNodeManager::checkInternal: failed to check proof";
  }
  else
  {
    // otherwise we trust the expected value, if it exists
    Assert(!expected.isNull()) << "ProofNodeManager::checkInternal: no checker "
                                  "or expected value provided";
    res = expected;
  }
  return res;
}

ProofChecker* ProofNodeManager::getChecker() const { return d_checker; }

std::shared_ptr<ProofNode> ProofNodeManager::clone(
    std::shared_ptr<ProofNode> pn)
{
  const ProofNode* orig = pn.get();
  std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>> visited;
  std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>>::iterator it;
  std::vector<const ProofNode*> visit;
  std::shared_ptr<ProofNode> cloned;
  visit.push_back(orig);
  const ProofNode* cur;
  while (!visit.empty())
  {
    cur = visit.back();
    it = visited.find(cur);
    if (it == visited.end())
    {
      visited[cur] = nullptr;
      const std::vector<std::shared_ptr<ProofNode>>& children =
          cur->getChildren();
      for (const std::shared_ptr<ProofNode>& cp : children)
      {
        visit.push_back(cp.get());
      }
      continue;
    }
    visit.pop_back();
    if (it->second.get() == nullptr)
    {
      std::vector<std::shared_ptr<ProofNode>> cchildren;
      const std::vector<std::shared_ptr<ProofNode>>& children =
          cur->getChildren();
      for (const std::shared_ptr<ProofNode>& cp : children)
      {
        it = visited.find(cp.get());
        Assert(it != visited.end());
        Assert(it->second != nullptr);
        cchildren.push_back(it->second);
      }
      cloned = std::make_shared<ProofNode>(
          cur->getRule(), cchildren, cur->getArguments());
      visited[cur] = cloned;
      // we trust the above cloning does not change what is proven
      cloned->d_proven = cur->d_proven;
    }
  }
  Assert(visited.find(orig) != visited.end());
  return visited[orig];
}

bool ProofNodeManager::updateNodeInternal(
    ProofNode* pn,
    PfRule id,
    const std::vector<std::shared_ptr<ProofNode>>& children,
    const std::vector<Node>& args,
    bool needsCheck)
{
  Assert(pn != nullptr);
  // ---------------- check for cyclic
  if (options::proofEagerChecking())
  {
    std::unordered_set<const ProofNode*> visited;
    for (const std::shared_ptr<ProofNode>& cpc : children)
    {
      if (expr::containsSubproof(cpc.get(), pn, visited))
      {
        std::stringstream ss;
        ss << "ProofNodeManager::updateNode: attempting to make cyclic proof! "
           << id << " " << pn->getResult() << ", children = " << std::endl;
        for (const std::shared_ptr<ProofNode>& cp : children)
        {
          ss << "  " << cp->getRule() << " " << cp->getResult() << std::endl;
        }
        ss << "Full children:" << std::endl;
        for (const std::shared_ptr<ProofNode>& cp : children)
        {
          ss << "  - ";
          cp->printDebug(ss);
          ss << std::endl;
        }
        Unreachable() << ss.str();
      }
    }
  }
  // ---------------- end check for cyclic

  // should have already computed what is proven
  Assert(!pn->d_proven.isNull())
      << "ProofNodeManager::updateProofNode: invalid proof provided";
  if (needsCheck)
  {
    // We expect to prove the same thing as before
    Node res = checkInternal(id, children, args, pn->d_proven);
    if (res.isNull())
    {
      // if it was invalid, then we do not update
      return false;
    }
    // proven field should already be the same as the result
    Assert(res == pn->d_proven);
  }

  // we update its value
  pn->setValue(id, children, args);
  return true;
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Haniel Barbosa, 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 proof node manager.
14		*/
15
16		#include "expr/proof_node_manager.h"
17
18		#include <sstream>
19
20		#include "expr/proof.h"
21		#include "expr/proof_checker.h"
22		#include "expr/proof_node.h"
23		#include "expr/proof_node_algorithm.h"
24		#include "options/proof_options.h"
25		#include "theory/rewriter.h"
26
27		using namespace cvc5::kind;
28
29		namespace cvc5 {
30
31	3600	ProofNodeManager::ProofNodeManager(ProofChecker* pc)
32	3600	: d_checker(pc)
33		{
34	3600	d_true = NodeManager::currentNM()->mkConst(true);
35	3600	}
36
37	19133680	std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
38		PfRule id,
39		const std::vector<std::shared_ptr<ProofNode>>& children,
40		const std::vector<Node>& args,
41		Node expected)
42		{
43	38267360	Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId()
44	19133680	<< "} " << expected << "\n";
45	38267360	Node res = checkInternal(id, children, args, expected);
46	19133680	if (res.isNull())
47		{
48		// if it was invalid, then we return the null node
49		return nullptr;
50		}
51		// otherwise construct the proof node and set its proven field
52		std::shared_ptr<ProofNode> pn =
53	38267360	std::make_shared<ProofNode>(id, children, args);
54	19133680	pn->d_proven = res;
55	19133680	return pn;
56		}
57
58	9754952	std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact)
59		{
60	9754952	Assert(!fact.isNull());
61	9754952	Assert(fact.getType().isBoolean());
62	9754952	return mkNode(PfRule::ASSUME, {}, {fact}, fact);
63		}
64
65	388	std::shared_ptr<ProofNode> ProofNodeManager::mkTrans(
66		const std::vector<std::shared_ptr<ProofNode>>& children, Node expected)
67		{
68	388	Assert(!children.empty());
69	388	if (children.size() == 1)
70		{
71		Assert(expected.isNull() \|\| children[0]->getResult() == expected);
72		return children[0];
73		}
74	388	return mkNode(PfRule::TRANS, children, {}, expected);
75		}
76
77	181295	std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
78		std::shared_ptr<ProofNode> pf,
79		std::vector<Node>& assumps,
80		bool ensureClosed,
81		bool doMinimize,
82		Node expected)
83		{
84	181295	if (!ensureClosed)
85		{
86	47533	return mkNode(PfRule::SCOPE, {pf}, assumps, expected);
87		}
88	133762	Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl;
89		// we first ensure the assumptions are flattened
90	267524	std::unordered_set<Node> ac{assumps.begin(), assumps.end()};
91		// map from the rewritten form of assumptions to the original. This is only
92		// computed in the rare case when we need rewriting to match the
93		// assumptions. An example of this is for Boolean constant equalities in
94		// scoped proofs from the proof equality engine.
95	267524	std::unordered_map<Node, Node> acr;
96		// whether we have compute the map above
97	133762	bool computedAcr = false;
98
99		// The free assumptions of the proof
100	267524	std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
101	133762	expr::getFreeAssumptionsMap(pf, famap);
102	267524	std::unordered_set<Node> acu;
103	594345	for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
104	133762	fa : famap)
105		{
106	1188690	Node a = fa.first;
107	1037949	if (ac.find(a) != ac.end())
108		{
109		// already covered by an assumption
110	443604	acu.insert(a);
111	443604	continue;
112		}
113		// trivial assumption
114	150741	if (a == d_true)
115		{
116		Trace("pnm-scope") << "- justify trivial True assumption\n";
117		for (std::shared_ptr<ProofNode> pfs : fa.second)
118		{
119		Assert(pfs->getResult() == a);
120		updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a});
121		}
122		Trace("pnm-scope") << "...finished" << std::endl;
123		acu.insert(a);
124		continue;
125		}
126	150741	Trace("pnm-scope") << "- try matching free assumption " << a << "\n";
127		// otherwise it may be due to symmetry?
128	301482	Node aeqSym = CDProof::getSymmFact(a);
129	150741	Trace("pnm-scope") << " - try sym " << aeqSym << "\n";
130	301482	Node aMatch;
131	150741	if (!aeqSym.isNull() && ac.count(aeqSym))
132		{
133	301054	Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a
134	301054	<< " for " << fa.second.size() << " proof nodes"
135	150527	<< std::endl;
136	150527	aMatch = aeqSym;
137		}
138		else
139		{
140		// Otherwise, may be derivable by rewriting. Note this is used in
141		// ensuring that proofs from the proof equality engine that involve
142		// equality with Boolean constants are closed.
143	214	if (!computedAcr)
144		{
145	89	computedAcr = true;
146	1092	for (const Node& acc : ac)
147		{
148	2006	Node accr = theory::Rewriter::rewrite(acc);
149	1003	if (accr != acc)
150		{
151	403	acr[accr] = acc;
152		}
153		}
154		}
155	428	Node ar = theory::Rewriter::rewrite(a);
156	214	std::unordered_map<Node, Node>::iterator itr = acr.find(ar);
157	214	if (itr != acr.end())
158		{
159	214	aMatch = itr->second;
160		}
161		}
162
163		// if we found a match either by symmetry or rewriting, then we connect
164		// the assumption here.
165	150741	if (!aMatch.isNull())
166		{
167	301482	std::shared_ptr<ProofNode> pfaa = mkAssume(aMatch);
168		// must correct the orientation on this leaf
169	301482	std::vector<std::shared_ptr<ProofNode>> children;
170	150741	children.push_back(pfaa);
171	301482	for (std::shared_ptr<ProofNode> pfs : fa.second)
172		{
173	150741	Assert(pfs->getResult() == a);
174		// use SYMM if possible
175	150741	if (aMatch == aeqSym)
176		{
177	150527	updateNode(pfs.get(), PfRule::SYMM, children, {});
178		}
179		else
180		{
181	214	updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, {a});
182		}
183		}
184	150741	Trace("pnm-scope") << "...finished" << std::endl;
185	150741	acu.insert(aMatch);
186	150741	continue;
187		}
188		// If we did not find a match, it is an error, since all free assumptions
189		// should be arguments to SCOPE.
190		std::stringstream ss;
191
192		bool dumpProofTraceOn = Trace.isOn("dump-proof-error");
193		if (dumpProofTraceOn)
194		{
195		ss << "The proof : " << *pf << std::endl;
196		}
197		ss << std::endl << "Free assumption: " << a << std::endl;
198		for (const Node& aprint : ac)
199		{
200		ss << "- assumption: " << aprint << std::endl;
201		}
202		if (!dumpProofTraceOn)
203		{
204		ss << "Use -t dump-proof-error for details on proof" << std::endl;
205		}
206		Unreachable() << "Generated a proof that is not closed by the scope: "
207		<< ss.str() << std::endl;
208		}
209	133762	if (acu.size() < ac.size())
210		{
211		// All assumptions should match a free assumption; if one does not, then
212		// the explanation could have been smaller.
213	22330	for (const Node& a : ac)
214		{
215	17602	if (acu.find(a) == acu.end())
216		{
217	5075	Notice() << "ProofNodeManager::mkScope: assumption " << a
218		<< " does not match a free assumption in proof" << std::endl;
219		}
220		}
221		}
222	133762	if (doMinimize && acu.size() < ac.size())
223		{
224	4706	assumps.clear();
225	4706	assumps.insert(assumps.end(), acu.begin(), acu.end());
226		}
227	129056	else if (ac.size() < assumps.size())
228		{
229		// remove duplicates to avoid redundant literals in clauses
230	38	assumps.clear();
231	38	assumps.insert(assumps.end(), ac.begin(), ac.end());
232		}
233	267524	Node minExpected;
234	133762	NodeManager* nm = NodeManager::currentNM();
235	267524	Node exp;
236	133762	if (assumps.empty())
237		{
238		// SCOPE with no arguments is a no-op, just return original
239	1223	return pf;
240		}
241	265078	Node conc = pf->getResult();
242	132539	exp = assumps.size() == 1 ? assumps[0] : nm->mkNode(AND, assumps);
243	132539	if (conc.isConst() && !conc.getConst<bool>())
244		{
245	38153	minExpected = exp.notNode();
246		}
247		else
248		{
249	94386	minExpected = nm->mkNode(IMPLIES, exp, conc);
250		}
251	132539	return mkNode(PfRule::SCOPE, {pf}, assumps, minExpected);
252		}
253
254	212744	bool ProofNodeManager::updateNode(
255		ProofNode* pn,
256		PfRule id,
257		const std::vector<std::shared_ptr<ProofNode>>& children,
258		const std::vector<Node>& args)
259		{
260	212744	return updateNodeInternal(pn, id, children, args, true);
261		}
262
263	3018511	bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr)
264		{
265	3018511	Assert(pn != nullptr);
266	3018511	Assert(pnr != nullptr);
267	3018511	if (pn->getResult() != pnr->getResult())
268		{
269		return false;
270		}
271		// can shortcut re-check of rule
272	3018511	return updateNodeInternal(
273	3018511	pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false);
274		}
275
276	19346424	Node ProofNodeManager::checkInternal(
277		PfRule id,
278		const std::vector<std::shared_ptr<ProofNode>>& children,
279		const std::vector<Node>& args,
280		Node expected)
281		{
282	19346424	Node res;
283	19346424	if (d_checker)
284		{
285		// check with the checker, which takes expected as argument
286	19346424	res = d_checker->check(id, children, args, expected);
287	19346424	Assert(!res.isNull())
288		<< "ProofNodeManager::checkInternal: failed to check proof";
289		}
290		else
291		{
292		// otherwise we trust the expected value, if it exists
293		Assert(!expected.isNull()) << "ProofNodeManager::checkInternal: no checker "
294		"or expected value provided";
295		res = expected;
296		}
297	19346424	return res;
298		}
299
300	10908963	ProofChecker* ProofNodeManager::getChecker() const { return d_checker; }
301
302	73325	std::shared_ptr<ProofNode> ProofNodeManager::clone(
303		std::shared_ptr<ProofNode> pn)
304		{
305	73325	const ProofNode* orig = pn.get();
306	146650	std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>> visited;
307	73325	std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>>::iterator it;
308	146650	std::vector<const ProofNode*> visit;
309	146650	std::shared_ptr<ProofNode> cloned;
310	73325	visit.push_back(orig);
311		const ProofNode* cur;
312	5012801	while (!visit.empty())
313		{
314	2469738	cur = visit.back();
315	2469738	it = visited.find(cur);
316	2469738	if (it == visited.end())
317		{
318	1138366	visited[cur] = nullptr;
319		const std::vector<std::shared_ptr<ProofNode>>& children =
320	1138366	cur->getChildren();
321	2396413	for (const std::shared_ptr<ProofNode>& cp : children)
322		{
323	1258047	visit.push_back(cp.get());
324		}
325	1138366	continue;
326		}
327	1331372	visit.pop_back();
328	1331372	if (it->second.get() == nullptr)
329		{
330	2276732	std::vector<std::shared_ptr<ProofNode>> cchildren;
331		const std::vector<std::shared_ptr<ProofNode>>& children =
332	1138366	cur->getChildren();
333	2396413	for (const std::shared_ptr<ProofNode>& cp : children)
334		{
335	1258047	it = visited.find(cp.get());
336	1258047	Assert(it != visited.end());
337	1258047	Assert(it->second != nullptr);
338	1258047	cchildren.push_back(it->second);
339		}
340	2276732	cloned = std::make_shared<ProofNode>(
341	2276732	cur->getRule(), cchildren, cur->getArguments());
342	1138366	visited[cur] = cloned;
343		// we trust the above cloning does not change what is proven
344	1138366	cloned->d_proven = cur->d_proven;
345		}
346		}
347	73325	Assert(visited.find(orig) != visited.end());
348	146650	return visited[orig];
349		}
350
351	3231255	bool ProofNodeManager::updateNodeInternal(
352		ProofNode* pn,
353		PfRule id,
354		const std::vector<std::shared_ptr<ProofNode>>& children,
355		const std::vector<Node>& args,
356		bool needsCheck)
357		{
358	3231255	Assert(pn != nullptr);
359		// ---------------- check for cyclic
360	3231255	if (options::proofEagerChecking())
361		{
362		std::unordered_set<const ProofNode*> visited;
363		for (const std::shared_ptr<ProofNode>& cpc : children)
364		{
365		if (expr::containsSubproof(cpc.get(), pn, visited))
366		{
367		std::stringstream ss;
368		ss << "ProofNodeManager::updateNode: attempting to make cyclic proof! "
369		<< id << " " << pn->getResult() << ", children = " << std::endl;
370		for (const std::shared_ptr<ProofNode>& cp : children)
371		{
372		ss << " " << cp->getRule() << " " << cp->getResult() << std::endl;
373		}
374		ss << "Full children:" << std::endl;
375		for (const std::shared_ptr<ProofNode>& cp : children)
376		{
377		ss << " - ";
378		cp->printDebug(ss);
379		ss << std::endl;
380		}
381		Unreachable() << ss.str();
382		}
383		}
384		}
385		// ---------------- end check for cyclic
386
387		// should have already computed what is proven
388	3231255	Assert(!pn->d_proven.isNull())
389		<< "ProofNodeManager::updateProofNode: invalid proof provided";
390	3231255	if (needsCheck)
391		{
392		// We expect to prove the same thing as before
393	425488	Node res = checkInternal(id, children, args, pn->d_proven);
394	212744	if (res.isNull())
395		{
396		// if it was invalid, then we do not update
397		return false;
398		}
399		// proven field should already be the same as the result
400	212744	Assert(res == pn->d_proven);
401		}
402
403		// we update its value
404	3231255	pn->setValue(id, children, args);
405	3231255	return true;
406		}
407
408	28191	} // namespace cvc5