Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/proof.cpp	Lines:	176	218	80.7 %
Date:	2021-09-07	Branches:	395	924	42.7 %


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

#include "proof/proof.h"

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

using namespace cvc5::kind;

namespace cvc5 {

CDProof::CDProof(ProofNodeManager* pnm,
                 context::Context* c,
                 const std::string& name,
                 bool autoSymm)
    : d_manager(pnm),
      d_context(),
      d_nodes(c ? c : &d_context),
      d_name(name),
      d_autoSymm(autoSymm)
{
}

CDProof::~CDProof() {}

std::shared_ptr<ProofNode> CDProof::getProofFor(Node fact)
{
  std::shared_ptr<ProofNode> pf = getProofSymm(fact);
  if (pf != nullptr)
  {
    return pf;
  }
  // add as assumption
  std::vector<Node> pargs = {fact};
  std::vector<std::shared_ptr<ProofNode>> passume;
  std::shared_ptr<ProofNode> pfa =
      d_manager->mkNode(PfRule::ASSUME, passume, pargs, fact);
  d_nodes.insert(fact, pfa);
  return pfa;
}

std::shared_ptr<ProofNode> CDProof::getProof(Node fact) const
{
  NodeProofNodeMap::iterator it = d_nodes.find(fact);
  if (it != d_nodes.end())
  {
    return (*it).second;
  }
  return nullptr;
}

std::shared_ptr<ProofNode> CDProof::getProofSymm(Node fact)
{
  Trace("cdproof") << "CDProof::getProofSymm: " << fact << std::endl;
  std::shared_ptr<ProofNode> pf = getProof(fact);
  if (pf != nullptr && !isAssumption(pf.get()))
  {
    Trace("cdproof") << "...existing non-assume " << pf->getRule() << std::endl;
    return pf;
  }
  else if (!d_autoSymm)
  {
    Trace("cdproof") << "...not auto considering symmetry" << std::endl;
    return pf;
  }
  Node symFact = getSymmFact(fact);
  if (symFact.isNull())
  {
    Trace("cdproof") << "...no possible symm" << std::endl;
    // no symmetry possible, return original proof (possibly assumption)
    return pf;
  }
  // See if a proof exists for the opposite direction, if so, add the step.
  // Notice that SYMM is also disallowed.
  std::shared_ptr<ProofNode> pfs = getProof(symFact);
  if (pfs != nullptr)
  {
    // The symmetric fact exists, and the current one either does not, or is
    // an assumption. We make a new proof that applies SYMM to pfs.
    std::vector<std::shared_ptr<ProofNode>> pschild;
    pschild.push_back(pfs);
    std::vector<Node> args;
    if (pf == nullptr)
    {
      Trace("cdproof") << "...fresh make symm" << std::endl;
      std::shared_ptr<ProofNode> psym = d_manager->mkSymm(pfs, fact);
      Assert(psym != nullptr);
      d_nodes.insert(fact, psym);
      return psym;
    }
    else if (!isAssumption(pfs.get()))
    {
      // if its not an assumption, make the connection
      Trace("cdproof") << "...update symm" << std::endl;
      // update pf
      bool sret = d_manager->updateNode(pf.get(), PfRule::SYMM, pschild, args);
      AlwaysAssert(sret);
    }
  }
  else
  {
    Trace("cdproof") << "...no symm, return "
                     << (pf == nullptr ? "null" : "non-null") << std::endl;
  }
  // return original proof (possibly assumption)
  return pf;
}

bool CDProof::addStep(Node expected,
                      PfRule id,
                      const std::vector<Node>& children,
                      const std::vector<Node>& args,
                      bool ensureChildren,
                      CDPOverwrite opolicy)
{
  Trace("cdproof") << "CDProof::addStep: " << identify() << " : " << id << " "
                   << expected << ", ensureChildren = " << ensureChildren
                   << ", overwrite policy = " << opolicy << std::endl;
  Trace("cdproof-debug") << "CDProof::addStep: " << identify()
                         << " : children: " << children << "\n";
  Trace("cdproof-debug") << "CDProof::addStep: " << identify()
                         << " : args: " << args << "\n";
  // We must always provide expected to this method
  Assert(!expected.isNull());

  std::shared_ptr<ProofNode> pprev = getProofSymm(expected);
  if (pprev != nullptr)
  {
    if (!shouldOverwrite(pprev.get(), id, opolicy))
    {
      // we should not overwrite the current step
      Trace("cdproof") << "...success, no overwrite" << std::endl;
      return true;
    }
    Trace("cdproof") << "existing proof " << pprev->getRule()
                     << ", overwrite..." << std::endl;
    // we will overwrite the existing proof node by updating its contents below
  }
  // collect the child proofs, for each premise
  std::vector<std::shared_ptr<ProofNode>> pchildren;
  for (const Node& c : children)
  {
    Trace("cdproof") << "- get child " << c << std::endl;
    std::shared_ptr<ProofNode> pc = getProofSymm(c);
    if (pc == nullptr)
    {
      if (ensureChildren)
      {
        // failed to get a proof for a child, fail
        Trace("cdproof") << "...fail, no child" << std::endl;
        return false;
      }
      Trace("cdproof") << "--- add assume" << std::endl;
      // otherwise, we initialize it as an assumption
      std::vector<Node> pcargs = {c};
      std::vector<std::shared_ptr<ProofNode>> pcassume;
      pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c);
      // assumptions never fail to check
      Assert(pc != nullptr);
      d_nodes.insert(c, pc);
    }
    pchildren.push_back(pc);
  }

  // the user may have provided SYMM of an assumption
  if (id == PfRule::SYMM)
  {
    Assert(pchildren.size() == 1);
    if (isAssumption(pchildren[0].get()))
    {
      // the step we are constructing is a (symmetric fact of an) assumption, so
      // there is no use adding it to the proof.
      return true;
    }
  }

  bool ret = true;
  // create or update it
  std::shared_ptr<ProofNode> pthis;
  if (pprev == nullptr)
  {
    Trace("cdproof") << "  new node " << expected << "..." << std::endl;
    pthis = d_manager->mkNode(id, pchildren, args, expected);
    if (pthis == nullptr)
    {
      // failed to construct the node, perhaps due to a proof checking failure
      Trace("cdproof") << "...fail, proof checking" << std::endl;
      return false;
    }
    d_nodes.insert(expected, pthis);
  }
  else
  {
    Trace("cdproof") << "  update node " << expected << "..." << std::endl;
    // update its value
    pthis = pprev;
    // We return the value of updateNode here. This means this method may return
    // false if this call failed, regardless of whether we already have a proof
    // step for expected.
    ret = d_manager->updateNode(pthis.get(), id, pchildren, args);
  }
  if (ret)
  {
    // the result of the proof node should be expected
    Assert(pthis->getResult() == expected);

    // notify new proof
    notifyNewProof(expected);
  }

  Trace("cdproof") << "...return " << ret << std::endl;
  return ret;
}

void CDProof::notifyNewProof(Node expected)
{
  if (!d_autoSymm)
  {
    return;
  }
  // ensure SYMM proof is also linked to an existing proof, if it is an
  // assumption.
  Node symExpected = getSymmFact(expected);
  if (!symExpected.isNull())
  {
    Trace("cdproof") << "  check connect symmetry " << symExpected << std::endl;
    // if it exists, we may need to update it
    std::shared_ptr<ProofNode> pfs = getProof(symExpected);
    if (pfs != nullptr)
    {
      Trace("cdproof") << "  connect via getProofSymm method..." << std::endl;
      // call the get function with symmetry, which will do the update
      std::shared_ptr<ProofNode> pfss = getProofSymm(symExpected);
    }
    else
    {
      Trace("cdproof") << "  no connect" << std::endl;
    }
  }
}

bool CDProof::addStep(Node expected,
                      const ProofStep& step,
                      bool ensureChildren,
                      CDPOverwrite opolicy)
{
  return addStep(expected,
                 step.d_rule,
                 step.d_children,
                 step.d_args,
                 ensureChildren,
                 opolicy);
}

bool CDProof::addSteps(const ProofStepBuffer& psb,
                       bool ensureChildren,
                       CDPOverwrite opolicy)
{
  const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
  for (const std::pair<Node, ProofStep>& ps : steps)
  {
    if (!addStep(ps.first, ps.second, ensureChildren, opolicy))
    {
      return false;
    }
  }
  return true;
}

bool CDProof::addProof(std::shared_ptr<ProofNode> pn,
                       CDPOverwrite opolicy,
                       bool doCopy)
{
  if (!doCopy)
  {
    // If we aren't doing a deep copy, we either store pn or link its top
    // node into the existing pointer
    Node curFact = pn->getResult();
    std::shared_ptr<ProofNode> cur = getProofSymm(curFact);
    if (cur == nullptr)
    {
      // Assert that the checker of this class agrees with (the externally
      // provided) pn. This ensures that if pn was checked by a different
      // checker than the one of the manager in this class, then it is double
      // checked here, so that this class maintains the invariant that all of
      // its nodes in d_nodes have been checked by the underlying checker.
      Assert(d_manager->getChecker() == nullptr
             || d_manager->getChecker()->check(pn.get(), curFact) == curFact);
      // just store the proof for fact
      d_nodes.insert(curFact, pn);
    }
    else if (shouldOverwrite(cur.get(), pn->getRule(), opolicy))
    {
      // We update cur to have the structure of the top node of pn. Notice that
      // the interface to update this node will ensure that the proof apf is a
      // proof of the assumption. If it does not, then pn was wrong.
      if (!d_manager->updateNode(
              cur.get(), pn->getRule(), pn->getChildren(), pn->getArguments()))
      {
        return false;
      }
    }
    // also need to connect via SYMM if necessary
    notifyNewProof(curFact);
    return true;
  }
  std::unordered_map<ProofNode*, bool> visited;
  std::unordered_map<ProofNode*, bool>::iterator it;
  std::vector<ProofNode*> visit;
  ProofNode* cur;
  Node curFact;
  visit.push_back(pn.get());
  bool retValue = true;
  do
  {
    cur = visit.back();
    curFact = cur->getResult();
    visit.pop_back();
    it = visited.find(cur);
    if (it == visited.end())
    {
      // visit the children
      visited[cur] = false;
      visit.push_back(cur);
      const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
      for (const std::shared_ptr<ProofNode>& c : cs)
      {
        visit.push_back(c.get());
      }
    }
    else if (!it->second)
    {
      // we always call addStep, which may or may not overwrite the
      // current step
      std::vector<Node> pexp;
      const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
      for (const std::shared_ptr<ProofNode>& c : cs)
      {
        Assert(!c->getResult().isNull());
        pexp.push_back(c->getResult());
      }
      // can ensure children at this point
      bool res = addStep(
          curFact, cur->getRule(), pexp, cur->getArguments(), true, opolicy);
      // should always succeed
      Assert(res);
      retValue = retValue && res;
      visited[cur] = true;
    }
  } while (!visit.empty());

  return retValue;
}

bool CDProof::hasStep(Node fact)
{
  std::shared_ptr<ProofNode> pf = getProof(fact);
  if (pf != nullptr && !isAssumption(pf.get()))
  {
    return true;
  }
  else if (!d_autoSymm)
  {
    return false;
  }
  Node symFact = getSymmFact(fact);
  if (symFact.isNull())
  {
    return false;
  }
  pf = getProof(symFact);
  if (pf != nullptr && !isAssumption(pf.get()))
  {
    return true;
  }
  return false;
}

ProofNodeManager* CDProof::getManager() const { return d_manager; }

bool CDProof::shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol)
{
  Assert(pn != nullptr);
  // we overwrite only if opol is CDPOverwrite::ALWAYS, or if
  // opol is CDPOverwrite::ASSUME_ONLY and the previously
  // provided proof pn was an assumption and the currently provided step is not
  return opol == CDPOverwrite::ALWAYS
         || (opol == CDPOverwrite::ASSUME_ONLY && isAssumption(pn)
             && newId != PfRule::ASSUME);
}

bool CDProof::isAssumption(ProofNode* pn)
{
  PfRule rule = pn->getRule();
  if (rule == PfRule::ASSUME)
  {
    return true;
  }
  else if (rule != PfRule::SYMM)
  {
    return false;
  }
  pn = ProofNodeManager::cancelDoubleSymm(pn);
  rule = pn->getRule();
  if (rule == PfRule::ASSUME)
  {
    return true;
  }
  else if (rule != PfRule::SYMM)
  {
    return false;
  }
  const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren();
  Assert(pc.size() == 1);
  return pc[0]->getRule() == PfRule::ASSUME;
}

bool CDProof::isSame(TNode f, TNode g)
{
  if (f == g)
  {
    return true;
  }
  Kind fk = f.getKind();
  Kind gk = g.getKind();
  if (fk == EQUAL && gk == EQUAL && f[0] == g[1] && f[1] == g[0])
  {
    // symmetric equality
    return true;
  }
  if (fk == NOT && gk == NOT && f[0].getKind() == EQUAL
      && g[0].getKind() == EQUAL && f[0][0] == g[0][1] && f[0][1] == g[0][0])
  {
    // symmetric disequality
    return true;
  }
  return false;
}

Node CDProof::getSymmFact(TNode f)
{
  bool polarity = f.getKind() != NOT;
  TNode fatom = polarity ? f : f[0];
  if (fatom.getKind() != EQUAL || fatom[0] == fatom[1])
  {
    return Node::null();
  }
  Node symFact = fatom[1].eqNode(fatom[0]);
  return polarity ? symFact : symFact.notNode();
}

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

}  // 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 proof.
14		*/
15
16		#include "proof/proof.h"
17
18		#include "proof/proof_checker.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	1479252	CDProof::CDProof(ProofNodeManager* pnm,
27		context::Context* c,
28		const std::string& name,
29	1479252	bool autoSymm)
30		: d_manager(pnm),
31		d_context(),
32		d_nodes(c ? c : &d_context),
33		d_name(name),
34	1479252	d_autoSymm(autoSymm)
35		{
36	1479252	}
37
38	1480495	CDProof::~CDProof() {}
39
40	2576091	std::shared_ptr<ProofNode> CDProof::getProofFor(Node fact)
41		{
42	5152182	std::shared_ptr<ProofNode> pf = getProofSymm(fact);
43	2576091	if (pf != nullptr)
44		{
45	1740870	return pf;
46		}
47		// add as assumption
48	1670442	std::vector<Node> pargs = {fact};
49	1670442	std::vector<std::shared_ptr<ProofNode>> passume;
50		std::shared_ptr<ProofNode> pfa =
51	1670442	d_manager->mkNode(PfRule::ASSUME, passume, pargs, fact);
52	835221	d_nodes.insert(fact, pfa);
53	835221	return pfa;
54		}
55
56	40990977	std::shared_ptr<ProofNode> CDProof::getProof(Node fact) const
57		{
58	40990977	NodeProofNodeMap::iterator it = d_nodes.find(fact);
59	40990977	if (it != d_nodes.end())
60		{
61	22680005	return (*it).second;
62		}
63	18310972	return nullptr;
64		}
65
66	20403285	std::shared_ptr<ProofNode> CDProof::getProofSymm(Node fact)
67		{
68	20403285	Trace("cdproof") << "CDProof::getProofSymm: " << fact << std::endl;
69	40806570	std::shared_ptr<ProofNode> pf = getProof(fact);
70	20403285	if (pf != nullptr && !isAssumption(pf.get()))
71		{
72	8749828	Trace("cdproof") << "...existing non-assume " << pf->getRule() << std::endl;
73	8749828	return pf;
74		}
75	11653457	else if (!d_autoSymm)
76		{
77		Trace("cdproof") << "...not auto considering symmetry" << std::endl;
78		return pf;
79		}
80	23306914	Node symFact = getSymmFact(fact);
81	11653457	if (symFact.isNull())
82		{
83	7232291	Trace("cdproof") << "...no possible symm" << std::endl;
84		// no symmetry possible, return original proof (possibly assumption)
85	7232291	return pf;
86		}
87		// See if a proof exists for the opposite direction, if so, add the step.
88		// Notice that SYMM is also disallowed.
89	8842332	std::shared_ptr<ProofNode> pfs = getProof(symFact);
90	4421166	if (pfs != nullptr)
91		{
92		// The symmetric fact exists, and the current one either does not, or is
93		// an assumption. We make a new proof that applies SYMM to pfs.
94	707355	std::vector<std::shared_ptr<ProofNode>> pschild;
95	539975	pschild.push_back(pfs);
96	707355	std::vector<Node> args;
97	539975	if (pf == nullptr)
98		{
99	372595	Trace("cdproof") << "...fresh make symm" << std::endl;
100	745190	std::shared_ptr<ProofNode> psym = d_manager->mkSymm(pfs, fact);
101	372595	Assert(psym != nullptr);
102	372595	d_nodes.insert(fact, psym);
103	372595	return psym;
104		}
105	167380	else if (!isAssumption(pfs.get()))
106		{
107		// if its not an assumption, make the connection
108	22	Trace("cdproof") << "...update symm" << std::endl;
109		// update pf
110	22	bool sret = d_manager->updateNode(pf.get(), PfRule::SYMM, pschild, args);
111	22	AlwaysAssert(sret);
112		}
113		}
114		else
115		{
116	7762382	Trace("cdproof") << "...no symm, return "
117	3881191	<< (pf == nullptr ? "null" : "non-null") << std::endl;
118		}
119		// return original proof (possibly assumption)
120	4048571	return pf;
121		}
122
123	6100404	bool CDProof::addStep(Node expected,
124		PfRule id,
125		const std::vector<Node>& children,
126		const std::vector<Node>& args,
127		bool ensureChildren,
128		CDPOverwrite opolicy)
129		{
130	12200808	Trace("cdproof") << "CDProof::addStep: " << identify() << " : " << id << " "
131	6100404	<< expected << ", ensureChildren = " << ensureChildren
132	6100404	<< ", overwrite policy = " << opolicy << std::endl;
133	12200808	Trace("cdproof-debug") << "CDProof::addStep: " << identify()
134	6100404	<< " : children: " << children << "\n";
135	12200808	Trace("cdproof-debug") << "CDProof::addStep: " << identify()
136	6100404	<< " : args: " << args << "\n";
137		// We must always provide expected to this method
138	6100404	Assert(!expected.isNull());
139
140	12200808	std::shared_ptr<ProofNode> pprev = getProofSymm(expected);
141	6100404	if (pprev != nullptr)
142		{
143	1860160	if (!shouldOverwrite(pprev.get(), id, opolicy))
144		{
145		// we should not overwrite the current step
146	1810596	Trace("cdproof") << "...success, no overwrite" << std::endl;
147	1810596	return true;
148		}
149	99128	Trace("cdproof") << "existing proof " << pprev->getRule()
150	49564	<< ", overwrite..." << std::endl;
151		// we will overwrite the existing proof node by updating its contents below
152		}
153		// collect the child proofs, for each premise
154	8579616	std::vector<std::shared_ptr<ProofNode>> pchildren;
155	12569060	for (const Node& c : children)
156		{
157	8279252	Trace("cdproof") << "- get child " << c << std::endl;
158	16558504	std::shared_ptr<ProofNode> pc = getProofSymm(c);
159	8279252	if (pc == nullptr)
160		{
161	2295797	if (ensureChildren)
162		{
163		// failed to get a proof for a child, fail
164		Trace("cdproof") << "...fail, no child" << std::endl;
165		return false;
166		}
167	2295797	Trace("cdproof") << "--- add assume" << std::endl;
168		// otherwise, we initialize it as an assumption
169	4591594	std::vector<Node> pcargs = {c};
170	4591594	std::vector<std::shared_ptr<ProofNode>> pcassume;
171	2295797	pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c);
172		// assumptions never fail to check
173	2295797	Assert(pc != nullptr);
174	2295797	d_nodes.insert(c, pc);
175		}
176	8279252	pchildren.push_back(pc);
177		}
178
179		// the user may have provided SYMM of an assumption
180	4289808	if (id == PfRule::SYMM)
181		{
182	54	Assert(pchildren.size() == 1);
183	54	if (isAssumption(pchildren[0].get()))
184		{
185		// the step we are constructing is a (symmetric fact of an) assumption, so
186		// there is no use adding it to the proof.
187	54	return true;
188		}
189		}
190
191	4289754	bool ret = true;
192		// create or update it
193	8579508	std::shared_ptr<ProofNode> pthis;
194	4289754	if (pprev == nullptr)
195		{
196	4240244	Trace("cdproof") << " new node " << expected << "..." << std::endl;
197	4240244	pthis = d_manager->mkNode(id, pchildren, args, expected);
198	4240244	if (pthis == nullptr)
199		{
200		// failed to construct the node, perhaps due to a proof checking failure
201		Trace("cdproof") << "...fail, proof checking" << std::endl;
202		return false;
203		}
204	4240244	d_nodes.insert(expected, pthis);
205		}
206		else
207		{
208	49510	Trace("cdproof") << " update node " << expected << "..." << std::endl;
209		// update its value
210	49510	pthis = pprev;
211		// We return the value of updateNode here. This means this method may return
212		// false if this call failed, regardless of whether we already have a proof
213		// step for expected.
214	49510	ret = d_manager->updateNode(pthis.get(), id, pchildren, args);
215		}
216	4289754	if (ret)
217		{
218		// the result of the proof node should be expected
219	4289754	Assert(pthis->getResult() == expected);
220
221		// notify new proof
222	4289754	notifyNewProof(expected);
223		}
224
225	4289754	Trace("cdproof") << "...return " << ret << std::endl;
226	4289754	return ret;
227		}
228
229	7735922	void CDProof::notifyNewProof(Node expected)
230		{
231	7735922	if (!d_autoSymm)
232		{
233		return;
234		}
235		// ensure SYMM proof is also linked to an existing proof, if it is an
236		// assumption.
237	15471844	Node symExpected = getSymmFact(expected);
238	7735922	if (!symExpected.isNull())
239		{
240	2751567	Trace("cdproof") << " check connect symmetry " << symExpected << std::endl;
241		// if it exists, we may need to update it
242	5503134	std::shared_ptr<ProofNode> pfs = getProof(symExpected);
243	2751567	if (pfs != nullptr)
244		{
245	1370	Trace("cdproof") << " connect via getProofSymm method..." << std::endl;
246		// call the get function with symmetry, which will do the update
247	1370	std::shared_ptr<ProofNode> pfss = getProofSymm(symExpected);
248		}
249		else
250		{
251	2750197	Trace("cdproof") << " no connect" << std::endl;
252		}
253		}
254		}
255
256	2735797	bool CDProof::addStep(Node expected,
257		const ProofStep& step,
258		bool ensureChildren,
259		CDPOverwrite opolicy)
260		{
261	8207391	return addStep(expected,
262	2735797	step.d_rule,
263		step.d_children,
264		step.d_args,
265		ensureChildren,
266	5471594	opolicy);
267		}
268
269	18603	bool CDProof::addSteps(const ProofStepBuffer& psb,
270		bool ensureChildren,
271		CDPOverwrite opolicy)
272		{
273	18603	const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
274	169315	for (const std::pair<Node, ProofStep>& ps : steps)
275		{
276	150712	if (!addStep(ps.first, ps.second, ensureChildren, opolicy))
277		{
278		return false;
279		}
280		}
281	18603	return true;
282		}
283
284	3446168	bool CDProof::addProof(std::shared_ptr<ProofNode> pn,
285		CDPOverwrite opolicy,
286		bool doCopy)
287		{
288	3446168	if (!doCopy)
289		{
290		// If we aren't doing a deep copy, we either store pn or link its top
291		// node into the existing pointer
292	6892336	Node curFact = pn->getResult();
293	6892336	std::shared_ptr<ProofNode> cur = getProofSymm(curFact);
294	3446168	if (cur == nullptr)
295		{
296		// Assert that the checker of this class agrees with (the externally
297		// provided) pn. This ensures that if pn was checked by a different
298		// checker than the one of the manager in this class, then it is double
299		// checked here, so that this class maintains the invariant that all of
300		// its nodes in d_nodes have been checked by the underlying checker.
301	2871924	Assert(d_manager->getChecker() == nullptr
302		\|\| d_manager->getChecker()->check(pn.get(), curFact) == curFact);
303		// just store the proof for fact
304	2871924	d_nodes.insert(curFact, pn);
305		}
306	574244	else if (shouldOverwrite(cur.get(), pn->getRule(), opolicy))
307		{
308		// We update cur to have the structure of the top node of pn. Notice that
309		// the interface to update this node will ensure that the proof apf is a
310		// proof of the assumption. If it does not, then pn was wrong.
311		if (!d_manager->updateNode(
312		cur.get(), pn->getRule(), pn->getChildren(), pn->getArguments()))
313		{
314		return false;
315		}
316		}
317		// also need to connect via SYMM if necessary
318	3446168	notifyNewProof(curFact);
319	3446168	return true;
320		}
321		std::unordered_map<ProofNode*, bool> visited;
322		std::unordered_map<ProofNode*, bool>::iterator it;
323		std::vector<ProofNode*> visit;
324		ProofNode* cur;
325		Node curFact;
326		visit.push_back(pn.get());
327		bool retValue = true;
328		do
329		{
330		cur = visit.back();
331		curFact = cur->getResult();
332		visit.pop_back();
333		it = visited.find(cur);
334		if (it == visited.end())
335		{
336		// visit the children
337		visited[cur] = false;
338		visit.push_back(cur);
339		const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
340		for (const std::shared_ptr<ProofNode>& c : cs)
341		{
342		visit.push_back(c.get());
343		}
344		}
345		else if (!it->second)
346		{
347		// we always call addStep, which may or may not overwrite the
348		// current step
349		std::vector<Node> pexp;
350		const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
351		for (const std::shared_ptr<ProofNode>& c : cs)
352		{
353		Assert(!c->getResult().isNull());
354		pexp.push_back(c->getResult());
355		}
356		// can ensure children at this point
357		bool res = addStep(
358		curFact, cur->getRule(), pexp, cur->getArguments(), true, opolicy);
359		// should always succeed
360		Assert(res);
361		retValue = retValue && res;
362		visited[cur] = true;
363		}
364		} while (!visit.empty());
365
366		return retValue;
367		}
368
369	868907	bool CDProof::hasStep(Node fact)
370		{
371	1737814	std::shared_ptr<ProofNode> pf = getProof(fact);
372	868907	if (pf != nullptr && !isAssumption(pf.get()))
373		{
374	708761	return true;
375		}
376	160146	else if (!d_autoSymm)
377		{
378		return false;
379		}
380	320292	Node symFact = getSymmFact(fact);
381	160146	if (symFact.isNull())
382		{
383	143122	return false;
384		}
385	17024	pf = getProof(symFact);
386	17024	if (pf != nullptr && !isAssumption(pf.get()))
387		{
388		return true;
389		}
390	17024	return false;
391		}
392
393	103367	ProofNodeManager* CDProof::getManager() const { return d_manager; }
394
395	2434404	bool CDProof::shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol)
396		{
397	2434404	Assert(pn != nullptr);
398		// we overwrite only if opol is CDPOverwrite::ALWAYS, or if
399		// opol is CDPOverwrite::ASSUME_ONLY and the previously
400		// provided proof pn was an assumption and the currently provided step is not
401		return opol == CDPOverwrite::ALWAYS
402	2483968	\|\| (opol == CDPOverwrite::ASSUME_ONLY && isAssumption(pn)
403	2791766	&& newId != PfRule::ASSUME);
404		}
405
406	13098103	bool CDProof::isAssumption(ProofNode* pn)
407		{
408	13098103	PfRule rule = pn->getRule();
409	13098103	if (rule == PfRule::ASSUME)
410		{
411	1334373	return true;
412		}
413	11763730	else if (rule != PfRule::SYMM)
414		{
415	11420319	return false;
416		}
417	343411	pn = ProofNodeManager::cancelDoubleSymm(pn);
418	343411	rule = pn->getRule();
419	343411	if (rule == PfRule::ASSUME)
420		{
421	922	return true;
422		}
423	342489	else if (rule != PfRule::SYMM)
424		{
425	163	return false;
426		}
427	342326	const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren();
428	342326	Assert(pc.size() == 1);
429	342326	return pc[0]->getRule() == PfRule::ASSUME;
430		}
431
432	1028691	bool CDProof::isSame(TNode f, TNode g)
433		{
434	1028691	if (f == g)
435		{
436	570333	return true;
437		}
438	458358	Kind fk = f.getKind();
439	458358	Kind gk = g.getKind();
440	458358	if (fk == EQUAL && gk == EQUAL && f[0] == g[1] && f[1] == g[0])
441		{
442		// symmetric equality
443	182017	return true;
444		}
445	331357	if (fk == NOT && gk == NOT && f[0].getKind() == EQUAL
446	298897	&& g[0].getKind() == EQUAL && f[0][0] == g[0][1] && f[0][1] == g[0][0])
447		{
448		// symmetric disequality
449	788	return true;
450		}
451	275553	return false;
452		}
453
454	21215311	Node CDProof::getSymmFact(TNode f)
455		{
456	21215311	bool polarity = f.getKind() != NOT;
457	42430622	TNode fatom = polarity ? f : f[0];
458	21215311	if (fatom.getKind() != EQUAL \|\| fatom[0] == fatom[1])
459		{
460	12863121	return Node::null();
461		}
462	16704380	Node symFact = fatom[1].eqNode(fatom[0]);
463	8352190	return polarity ? symFact : symFact.notNode();
464		}
465
466	20609115	std::string CDProof::identify() const { return d_name; }
467
468	29502	} // namespace cvc5