Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/proof_node_manager.cpp	Lines:	182	220	82.7 %
Date:	2021-11-07	Branches:	292	894	32.7 %


/******************************************************************************
 * 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 "proof/proof_node_manager.h"

#include <sstream>

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

using namespace cvc5::kind;

namespace cvc5 {

ProofNodeManager::ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc)
    : d_rewriter(rr), d_checker(pc)
{
  d_true = NodeManager::currentNM()->mkConst(true);
  // we always allocate a proof checker, regardless of the proof checking mode
  Assert(d_checker != nullptr);
}

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";
  bool didCheck = false;
  Node res = checkInternal(id, children, args, expected, didCheck);
  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;
  pn->d_provenChecked = didCheck;
  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::mkSymm(
    std::shared_ptr<ProofNode> child, Node expected)
{
  if (child->getRule() == PfRule::SYMM)
  {
    Assert(expected.isNull()
           || child->getChildren()[0]->getResult() == expected);
    return child->getChildren()[0];
  }
  return mkNode(PfRule::SYMM, {child}, {}, expected);
}

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 = d_rewriter->rewrite(acc);
          if (accr != acc)
          {
            acr[accr] = acc;
          }
        }
      }
      Node ar = d_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)
        {
          if (pfaa->getRule() == PfRule::SYMM)
          {
            updateNode(pfs.get(), pfaa->getChildren()[0].get());
          }
          else
          {
            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())
      {
        Trace("pnm") << "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 == pnr)
  {
    // same node, no update necessary
    return true;
  }
  if (pn->getResult() != pnr->getResult())
  {
    return false;
  }
  // copy whether we did the check
  pn->d_provenChecked = pnr->d_provenChecked;
  // can shortcut re-check of rule
  return updateNodeInternal(
      pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false);
}

void ProofNodeManager::ensureChecked(ProofNode* pn)
{
  if (pn->d_provenChecked)
  {
    // already checked
    return;
  }
  // directly call the proof checker
  Node res = d_checker->check(pn, pn->getResult());
  pn->d_provenChecked = true;
  // should have the correct result
  Assert(res == pn->d_proven);
}

Node ProofNodeManager::checkInternal(
    PfRule id,
    const std::vector<std::shared_ptr<ProofNode>>& children,
    const std::vector<Node>& args,
    Node expected,
    bool& didCheck)
{
  // if the user supplied an expected result, then we trust it if we are in
  // a proof checking mode that does not eagerly check rule applications
  if (!expected.isNull())
  {
    if (options::proofCheck() == options::ProofCheckMode::LAZY
        || options::proofCheck() == options::ProofCheckMode::NONE)
    {
      return expected;
    }
  }
  // check with the checker, which takes expected as argument
  Node res = d_checker->check(id, children, args, expected);
  didCheck = true;
  Assert(!res.isNull())
      << "ProofNodeManager::checkInternal: failed to check proof";
  return res;
}

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

std::shared_ptr<ProofNode> ProofNodeManager::clone(
    std::shared_ptr<ProofNode> pn) const
{
  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());
        // if we encounter nullptr here, then this child is currently being
        // traversed at a higher level, hence this corresponds to a cyclic
        // proof.
        if (it->second == nullptr)
        {
          Unreachable() << "Cyclic proof encountered when cloning a proof node";
        }
        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;
      cloned->d_provenChecked = cur->d_provenChecked;
    }
  }
  Assert(visited.find(orig) != visited.end());
  return visited[orig];
}

ProofNode* ProofNodeManager::cancelDoubleSymm(ProofNode* pn)
{
  while (pn->getRule() == PfRule::SYMM)
  {
    std::shared_ptr<ProofNode> pnc = pn->getChildren()[0];
    if (pnc->getRule() == PfRule::SYMM)
    {
      pn = pnc->getChildren()[0].get();
    }
    else
    {
      break;
    }
  }
  return pn;
}

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::proofCheck() == options::ProofCheckMode::EAGER)
  {
    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
    bool didCheck = false;
    Node res = checkInternal(id, children, args, pn->d_proven, didCheck);
    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);
    pn->d_provenChecked = didCheck;
  }

  // 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 "proof/proof_node_manager.h"
17
18		#include <sstream>
19
20		#include "options/proof_options.h"
21		#include "proof/proof.h"
22		#include "proof/proof_checker.h"
23		#include "proof/proof_node.h"
24		#include "proof/proof_node_algorithm.h"
25		#include "theory/rewriter.h"
26
27		using namespace cvc5::kind;
28
29		namespace cvc5 {
30
31	7989	ProofNodeManager::ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc)
32	7989	: d_rewriter(rr), d_checker(pc)
33		{
34	7989	d_true = NodeManager::currentNM()->mkConst(true);
35		// we always allocate a proof checker, regardless of the proof checking mode
36	7989	Assert(d_checker != nullptr);
37	7989	}
38
39	18966527	std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
40		PfRule id,
41		const std::vector<std::shared_ptr<ProofNode>>& children,
42		const std::vector<Node>& args,
43		Node expected)
44		{
45	37933054	Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId()
46	18966527	<< "} " << expected << "\n";
47	18966527	bool didCheck = false;
48	37933054	Node res = checkInternal(id, children, args, expected, didCheck);
49	18966527	if (res.isNull())
50		{
51		// if it was invalid, then we return the null node
52		return nullptr;
53		}
54		// otherwise construct the proof node and set its proven field
55		std::shared_ptr<ProofNode> pn =
56	37933054	std::make_shared<ProofNode>(id, children, args);
57	18966527	pn->d_proven = res;
58	18966527	pn->d_provenChecked = didCheck;
59	18966527	return pn;
60		}
61
62	9986899	std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact)
63		{
64	9986899	Assert(!fact.isNull());
65	9986899	Assert(fact.getType().isBoolean());
66	9986899	return mkNode(PfRule::ASSUME, {}, {fact}, fact);
67		}
68
69	330037	std::shared_ptr<ProofNode> ProofNodeManager::mkSymm(
70		std::shared_ptr<ProofNode> child, Node expected)
71		{
72	330037	if (child->getRule() == PfRule::SYMM)
73		{
74	222	Assert(expected.isNull()
75		\|\| child->getChildren()[0]->getResult() == expected);
76	222	return child->getChildren()[0];
77		}
78	329815	return mkNode(PfRule::SYMM, {child}, {}, expected);
79		}
80
81	277	std::shared_ptr<ProofNode> ProofNodeManager::mkTrans(
82		const std::vector<std::shared_ptr<ProofNode>>& children, Node expected)
83		{
84	277	Assert(!children.empty());
85	277	if (children.size() == 1)
86		{
87		Assert(expected.isNull() \|\| children[0]->getResult() == expected);
88		return children[0];
89		}
90	277	return mkNode(PfRule::TRANS, children, {}, expected);
91		}
92
93	194106	std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
94		std::shared_ptr<ProofNode> pf,
95		std::vector<Node>& assumps,
96		bool ensureClosed,
97		bool doMinimize,
98		Node expected)
99		{
100	194106	if (!ensureClosed)
101		{
102	58499	return mkNode(PfRule::SCOPE, {pf}, assumps, expected);
103		}
104	135607	Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl;
105		// we first ensure the assumptions are flattened
106	271214	std::unordered_set<Node> ac{assumps.begin(), assumps.end()};
107		// map from the rewritten form of assumptions to the original. This is only
108		// computed in the rare case when we need rewriting to match the
109		// assumptions. An example of this is for Boolean constant equalities in
110		// scoped proofs from the proof equality engine.
111	271214	std::unordered_map<Node, Node> acr;
112		// whether we have compute the map above
113	135607	bool computedAcr = false;
114
115		// The free assumptions of the proof
116	271214	std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
117	135607	expr::getFreeAssumptionsMap(pf, famap);
118	271214	std::unordered_set<Node> acu;
119	569969	for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
120	135607	fa : famap)
121		{
122	1139938	Node a = fa.first;
123	1016764	if (ac.find(a) != ac.end())
124		{
125		// already covered by an assumption
126	446795	acu.insert(a);
127	446795	continue;
128		}
129		// trivial assumption
130	123174	if (a == d_true)
131		{
132		Trace("pnm-scope") << "- justify trivial True assumption\n";
133		for (std::shared_ptr<ProofNode> pfs : fa.second)
134		{
135		Assert(pfs->getResult() == a);
136		updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a});
137		}
138		Trace("pnm-scope") << "...finished" << std::endl;
139		acu.insert(a);
140		continue;
141		}
142	123174	Trace("pnm-scope") << "- try matching free assumption " << a << "\n";
143		// otherwise it may be due to symmetry?
144	246348	Node aeqSym = CDProof::getSymmFact(a);
145	123174	Trace("pnm-scope") << " - try sym " << aeqSym << "\n";
146	246348	Node aMatch;
147	123174	if (!aeqSym.isNull() && ac.count(aeqSym))
148		{
149	244516	Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a
150	244516	<< " for " << fa.second.size() << " proof nodes"
151	122258	<< std::endl;
152	122258	aMatch = aeqSym;
153		}
154		else
155		{
156		// Otherwise, may be derivable by rewriting. Note this is used in
157		// ensuring that proofs from the proof equality engine that involve
158		// equality with Boolean constants are closed.
159	916	if (!computedAcr)
160		{
161	329	computedAcr = true;
162	5412	for (const Node& acc : ac)
163		{
164	10166	Node accr = d_rewriter->rewrite(acc);
165	5083	if (accr != acc)
166		{
167	1912	acr[accr] = acc;
168		}
169		}
170		}
171	1832	Node ar = d_rewriter->rewrite(a);
172	916	std::unordered_map<Node, Node>::iterator itr = acr.find(ar);
173	916	if (itr != acr.end())
174		{
175	916	aMatch = itr->second;
176		}
177		}
178
179		// if we found a match either by symmetry or rewriting, then we connect
180		// the assumption here.
181	123174	if (!aMatch.isNull())
182		{
183	246348	std::shared_ptr<ProofNode> pfaa = mkAssume(aMatch);
184		// must correct the orientation on this leaf
185	246348	std::vector<std::shared_ptr<ProofNode>> children;
186	123174	children.push_back(pfaa);
187	246348	for (std::shared_ptr<ProofNode> pfs : fa.second)
188		{
189	123174	Assert(pfs->getResult() == a);
190		// use SYMM if possible
191	123174	if (aMatch == aeqSym)
192		{
193	122258	if (pfaa->getRule() == PfRule::SYMM)
194		{
195		updateNode(pfs.get(), pfaa->getChildren()[0].get());
196		}
197		else
198		{
199	122258	updateNode(pfs.get(), PfRule::SYMM, children, {});
200		}
201		}
202		else
203		{
204	916	updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, {a});
205		}
206		}
207	123174	Trace("pnm-scope") << "...finished" << std::endl;
208	123174	acu.insert(aMatch);
209	123174	continue;
210		}
211		// If we did not find a match, it is an error, since all free assumptions
212		// should be arguments to SCOPE.
213		std::stringstream ss;
214
215		bool dumpProofTraceOn = Trace.isOn("dump-proof-error");
216		if (dumpProofTraceOn)
217		{
218		ss << "The proof : " << *pf << std::endl;
219		}
220		ss << std::endl << "Free assumption: " << a << std::endl;
221		for (const Node& aprint : ac)
222		{
223		ss << "- assumption: " << aprint << std::endl;
224		}
225		if (!dumpProofTraceOn)
226		{
227		ss << "Use -t dump-proof-error for details on proof" << std::endl;
228		}
229		Unreachable() << "Generated a proof that is not closed by the scope: "
230		<< ss.str() << std::endl;
231		}
232	135607	if (acu.size() < ac.size())
233		{
234		// All assumptions should match a free assumption; if one does not, then
235		// the explanation could have been smaller.
236	48166	for (const Node& a : ac)
237		{
238	43649	if (acu.find(a) == acu.end())
239		{
240	57890	Trace("pnm") << "ProofNodeManager::mkScope: assumption " << a
241	28945	<< " does not match a free assumption in proof"
242	28945	<< std::endl;
243		}
244		}
245		}
246	135607	if (doMinimize && acu.size() < ac.size())
247		{
248	3473	assumps.clear();
249	3473	assumps.insert(assumps.end(), acu.begin(), acu.end());
250		}
251	132134	else if (ac.size() < assumps.size())
252		{
253		// remove duplicates to avoid redundant literals in clauses
254	677	assumps.clear();
255	677	assumps.insert(assumps.end(), ac.begin(), ac.end());
256		}
257	271214	Node minExpected;
258	135607	NodeManager* nm = NodeManager::currentNM();
259	271214	Node exp;
260	135607	if (assumps.empty())
261		{
262		// SCOPE with no arguments is a no-op, just return original
263	2778	return pf;
264		}
265	265658	Node conc = pf->getResult();
266	132829	exp = assumps.size() == 1 ? assumps[0] : nm->mkNode(AND, assumps);
267	132829	if (conc.isConst() && !conc.getConst<bool>())
268		{
269	49336	minExpected = exp.notNode();
270		}
271		else
272		{
273	83493	minExpected = nm->mkNode(IMPLIES, exp, conc);
274		}
275	132829	return mkNode(PfRule::SCOPE, {pf}, assumps, minExpected);
276		}
277
278	193065	bool ProofNodeManager::updateNode(
279		ProofNode* pn,
280		PfRule id,
281		const std::vector<std::shared_ptr<ProofNode>>& children,
282		const std::vector<Node>& args)
283		{
284	193065	return updateNodeInternal(pn, id, children, args, true);
285		}
286
287	2183558	bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr)
288		{
289	2183558	Assert(pn != nullptr);
290	2183558	Assert(pnr != nullptr);
291	2183558	if (pn == pnr)
292		{
293		// same node, no update necessary
294	2187	return true;
295		}
296	2181371	if (pn->getResult() != pnr->getResult())
297		{
298		return false;
299		}
300		// copy whether we did the check
301	2181371	pn->d_provenChecked = pnr->d_provenChecked;
302		// can shortcut re-check of rule
303	2181371	return updateNodeInternal(
304	2181371	pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false);
305		}
306
307	2491412	void ProofNodeManager::ensureChecked(ProofNode* pn)
308		{
309	2491412	if (pn->d_provenChecked)
310		{
311		// already checked
312	113975	return;
313		}
314		// directly call the proof checker
315	4754874	Node res = d_checker->check(pn, pn->getResult());
316	2377437	pn->d_provenChecked = true;
317		// should have the correct result
318	2377437	Assert(res == pn->d_proven);
319		}
320
321	19159592	Node ProofNodeManager::checkInternal(
322		PfRule id,
323		const std::vector<std::shared_ptr<ProofNode>>& children,
324		const std::vector<Node>& args,
325		Node expected,
326		bool& didCheck)
327		{
328		// if the user supplied an expected result, then we trust it if we are in
329		// a proof checking mode that does not eagerly check rule applications
330	19159592	if (!expected.isNull())
331		{
332	36054088	if (options::proofCheck() == options::ProofCheckMode::LAZY
333	18027044	\|\| options::proofCheck() == options::ProofCheckMode::NONE)
334		{
335	18024232	return expected;
336		}
337		}
338		// check with the checker, which takes expected as argument
339	2270720	Node res = d_checker->check(id, children, args, expected);
340	1135360	didCheck = true;
341	1135360	Assert(!res.isNull())
342		<< "ProofNodeManager::checkInternal: failed to check proof";
343	1135360	return res;
344		}
345
346	10918215	ProofChecker* ProofNodeManager::getChecker() const { return d_checker; }
347
348	61531	std::shared_ptr<ProofNode> ProofNodeManager::clone(
349		std::shared_ptr<ProofNode> pn) const
350		{
351	61531	const ProofNode* orig = pn.get();
352	123062	std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>> visited;
353	61531	std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>>::iterator it;
354	123062	std::vector<const ProofNode*> visit;
355	123062	std::shared_ptr<ProofNode> cloned;
356	61531	visit.push_back(orig);
357		const ProofNode* cur;
358	3967285	while (!visit.empty())
359		{
360	1952877	cur = visit.back();
361	1952877	it = visited.find(cur);
362	1952877	if (it == visited.end())
363		{
364	909630	visited[cur] = nullptr;
365		const std::vector<std::shared_ptr<ProofNode>>& children =
366	909630	cur->getChildren();
367	1891346	for (const std::shared_ptr<ProofNode>& cp : children)
368		{
369	981716	visit.push_back(cp.get());
370		}
371	909630	continue;
372		}
373	1043247	visit.pop_back();
374	1043247	if (it->second.get() == nullptr)
375		{
376	1819260	std::vector<std::shared_ptr<ProofNode>> cchildren;
377		const std::vector<std::shared_ptr<ProofNode>>& children =
378	909630	cur->getChildren();
379	1891346	for (const std::shared_ptr<ProofNode>& cp : children)
380		{
381	981716	it = visited.find(cp.get());
382	981716	Assert(it != visited.end());
383		// if we encounter nullptr here, then this child is currently being
384		// traversed at a higher level, hence this corresponds to a cyclic
385		// proof.
386	981716	if (it->second == nullptr)
387		{
388		Unreachable() << "Cyclic proof encountered when cloning a proof node";
389		}
390	981716	cchildren.push_back(it->second);
391		}
392	1819260	cloned = std::make_shared<ProofNode>(
393	1819260	cur->getRule(), cchildren, cur->getArguments());
394	909630	visited[cur] = cloned;
395		// we trust the above cloning does not change what is proven
396	909630	cloned->d_proven = cur->d_proven;
397	909630	cloned->d_provenChecked = cur->d_provenChecked;
398		}
399		}
400	61531	Assert(visited.find(orig) != visited.end());
401	123062	return visited[orig];
402		}
403
404	270255	ProofNode* ProofNodeManager::cancelDoubleSymm(ProofNode* pn)
405		{
406	271376	while (pn->getRule() == PfRule::SYMM)
407		{
408	270255	std::shared_ptr<ProofNode> pnc = pn->getChildren()[0];
409	269134	if (pnc->getRule() == PfRule::SYMM)
410		{
411	1121	pn = pnc->getChildren()[0].get();
412		}
413		else
414		{
415	268013	break;
416		}
417		}
418	269134	return pn;
419		}
420
421	2374436	bool ProofNodeManager::updateNodeInternal(
422		ProofNode* pn,
423		PfRule id,
424		const std::vector<std::shared_ptr<ProofNode>>& children,
425		const std::vector<Node>& args,
426		bool needsCheck)
427		{
428	2374436	Assert(pn != nullptr);
429		// ---------------- check for cyclic
430	2374436	if (options::proofCheck() == options::ProofCheckMode::EAGER)
431		{
432	1024	std::unordered_set<const ProofNode*> visited;
433	720	for (const std::shared_ptr<ProofNode>& cpc : children)
434		{
435	208	if (expr::containsSubproof(cpc.get(), pn, visited))
436		{
437		std::stringstream ss;
438		ss << "ProofNodeManager::updateNode: attempting to make cyclic proof! "
439		<< id << " " << pn->getResult() << ", children = " << std::endl;
440		for (const std::shared_ptr<ProofNode>& cp : children)
441		{
442		ss << " " << cp->getRule() << " " << cp->getResult() << std::endl;
443		}
444		ss << "Full children:" << std::endl;
445		for (const std::shared_ptr<ProofNode>& cp : children)
446		{
447		ss << " - ";
448		cp->printDebug(ss);
449		ss << std::endl;
450		}
451		Unreachable() << ss.str();
452		}
453		}
454		}
455		// ---------------- end check for cyclic
456
457		// should have already computed what is proven
458	2374436	Assert(!pn->d_proven.isNull())
459		<< "ProofNodeManager::updateProofNode: invalid proof provided";
460	2374436	if (needsCheck)
461		{
462		// We expect to prove the same thing as before
463	193065	bool didCheck = false;
464	386130	Node res = checkInternal(id, children, args, pn->d_proven, didCheck);
465	193065	if (res.isNull())
466		{
467		// if it was invalid, then we do not update
468		return false;
469		}
470		// proven field should already be the same as the result
471	193065	Assert(res == pn->d_proven);
472	193065	pn->d_provenChecked = didCheck;
473		}
474
475		// we update its value
476	2374436	pn->setValue(id, children, args);
477	2374436	return true;
478		}
479
480	31137	} // namespace cvc5