Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/eager_proof_generator.cpp	Lines:	59	63	93.7 %
Date:	2021-09-17	Branches:	81	196	41.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Alex Ozdemir
 *
 * 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 the abstract proof generator class.
 */

#include "proof/eager_proof_generator.h"

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

namespace cvc5 {

EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm,
                                         context::Context* c,
                                         std::string name)
    : d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c)
{
}

void EagerProofGenerator::setProofFor(Node f, std::shared_ptr<ProofNode> pf)
{
  // pf should prove f
  Assert(pf->getResult() == f)
      << "EagerProofGenerator::setProofFor: unexpected result" << std::endl
      << "Expected: " << f << std::endl
      << "Actual: " << pf->getResult() << std::endl;
  d_proofs[f] = pf;
}
void EagerProofGenerator::setProofForConflict(Node conf,
                                              std::shared_ptr<ProofNode> pf)
{
  // Normalize based on key
  Node ckey = TrustNode::getConflictProven(conf);
  setProofFor(ckey, pf);
}

void EagerProofGenerator::setProofForLemma(Node lem,
                                           std::shared_ptr<ProofNode> pf)
{
  // Normalize based on key
  Node lkey = TrustNode::getLemmaProven(lem);
  setProofFor(lkey, pf);
}

void EagerProofGenerator::setProofForPropExp(TNode lit,
                                             Node exp,
                                             std::shared_ptr<ProofNode> pf)
{
  // Normalize based on key
  Node pekey = TrustNode::getPropExpProven(lit, exp);
  setProofFor(pekey, pf);
}

std::shared_ptr<ProofNode> EagerProofGenerator::getProofFor(Node f)
{
  NodeProofNodeMap::iterator it = d_proofs.find(f);
  if (it == d_proofs.end())
  {
    return nullptr;
  }
  return (*it).second;
}

bool EagerProofGenerator::hasProofFor(Node f)
{
  return d_proofs.find(f) != d_proofs.end();
}

TrustNode EagerProofGenerator::mkTrustNode(Node n,
                                           std::shared_ptr<ProofNode> pf,
                                           bool isConflict)
{
  if (pf == nullptr)
  {
    return TrustNode::null();
  }
  if (isConflict)
  {
    // this shouldnt modify the key
    setProofForConflict(n, pf);
    // we can now return the trust node
    return TrustNode::mkTrustConflict(n, this);
  }
  // this shouldnt modify the key
  setProofForLemma(n, pf);
  // we can now return the trust node
  return TrustNode::mkTrustLemma(n, this);
}

TrustNode EagerProofGenerator::mkTrustNode(Node conc,
                                           PfRule id,
                                           const std::vector<Node>& exp,
                                           const std::vector<Node>& args,
                                           bool isConflict)
{
  // if no children, its easy
  if (exp.empty())
  {
    std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, conc);
    return mkTrustNode(conc, pf, isConflict);
  }
  // otherwise, we use CDProof + SCOPE
  CDProof cdp(d_pnm);
  cdp.addStep(conc, id, exp, args);
  std::shared_ptr<ProofNode> pf = cdp.getProofFor(conc);
  // We use mkNode instead of mkScope, since there is no reason to check
  // whether the free assumptions of pf are in exp, since they are by the
  // construction above.
  std::shared_ptr<ProofNode> pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp);
  return mkTrustNode(pfs->getResult(), pfs, isConflict);
}

TrustNode EagerProofGenerator::mkTrustedRewrite(Node a,
                                                Node b,
                                                std::shared_ptr<ProofNode> pf)
{
  if (pf == nullptr)
  {
    return TrustNode::null();
  }
  Node eq = a.eqNode(b);
  setProofFor(eq, pf);
  return TrustNode::mkTrustRewrite(a, b, this);
}

TrustNode EagerProofGenerator::mkTrustedPropagation(
    Node n, Node exp, std::shared_ptr<ProofNode> pf)
{
  if (pf == nullptr)
  {
    return TrustNode::null();
  }
  setProofForPropExp(n, exp, pf);
  return TrustNode::mkTrustPropExp(n, exp, this);
}

TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f)
{
  // make the lemma
  Node lem = f.orNode(f.notNode());
  return mkTrustNode(lem, PfRule::SPLIT, {}, {f}, false);
}

std::string EagerProofGenerator::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, Alex Ozdemir
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 the abstract proof generator class.
14		*/
15
16		#include "proof/eager_proof_generator.h"
17
18		#include "proof/proof.h"
19		#include "proof/proof_node.h"
20		#include "proof/proof_node_manager.h"
21
22		namespace cvc5 {
23
24	87744	EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm,
25		context::Context* c,
26	87744	std::string name)
27	87744	: d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c)
28		{
29	87744	}
30
31	379052	void EagerProofGenerator::setProofFor(Node f, std::shared_ptr<ProofNode> pf)
32		{
33		// pf should prove f
34	758104	Assert(pf->getResult() == f)
35		<< "EagerProofGenerator::setProofFor: unexpected result" << std::endl
36	379052	<< "Expected: " << f << std::endl
37	379052	<< "Actual: " << pf->getResult() << std::endl;
38	379052	d_proofs[f] = pf;
39	379052	}
40	16444	void EagerProofGenerator::setProofForConflict(Node conf,
41		std::shared_ptr<ProofNode> pf)
42		{
43		// Normalize based on key
44	32888	Node ckey = TrustNode::getConflictProven(conf);
45	16444	setProofFor(ckey, pf);
46	16444	}
47
48	255508	void EagerProofGenerator::setProofForLemma(Node lem,
49		std::shared_ptr<ProofNode> pf)
50		{
51		// Normalize based on key
52	511016	Node lkey = TrustNode::getLemmaProven(lem);
53	255508	setProofFor(lkey, pf);
54	255508	}
55
56	58596	void EagerProofGenerator::setProofForPropExp(TNode lit,
57		Node exp,
58		std::shared_ptr<ProofNode> pf)
59		{
60		// Normalize based on key
61	117192	Node pekey = TrustNode::getPropExpProven(lit, exp);
62	58596	setProofFor(pekey, pf);
63	58596	}
64
65	139569	std::shared_ptr<ProofNode> EagerProofGenerator::getProofFor(Node f)
66		{
67	139569	NodeProofNodeMap::iterator it = d_proofs.find(f);
68	139569	if (it == d_proofs.end())
69		{
70	2690	return nullptr;
71		}
72	136879	return (*it).second;
73		}
74
75	889962	bool EagerProofGenerator::hasProofFor(Node f)
76		{
77	889962	return d_proofs.find(f) != d_proofs.end();
78		}
79
80	263928	TrustNode EagerProofGenerator::mkTrustNode(Node n,
81		std::shared_ptr<ProofNode> pf,
82		bool isConflict)
83		{
84	263928	if (pf == nullptr)
85		{
86		return TrustNode::null();
87		}
88	263928	if (isConflict)
89		{
90		// this shouldnt modify the key
91	13404	setProofForConflict(n, pf);
92		// we can now return the trust node
93	13404	return TrustNode::mkTrustConflict(n, this);
94		}
95		// this shouldnt modify the key
96	250524	setProofForLemma(n, pf);
97		// we can now return the trust node
98	250524	return TrustNode::mkTrustLemma(n, this);
99		}
100
101	14449	TrustNode EagerProofGenerator::mkTrustNode(Node conc,
102		PfRule id,
103		const std::vector<Node>& exp,
104		const std::vector<Node>& args,
105		bool isConflict)
106		{
107		// if no children, its easy
108	14449	if (exp.empty())
109		{
110	28208	std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, conc);
111	14104	return mkTrustNode(conc, pf, isConflict);
112		}
113		// otherwise, we use CDProof + SCOPE
114	690	CDProof cdp(d_pnm);
115	345	cdp.addStep(conc, id, exp, args);
116	690	std::shared_ptr<ProofNode> pf = cdp.getProofFor(conc);
117		// We use mkNode instead of mkScope, since there is no reason to check
118		// whether the free assumptions of pf are in exp, since they are by the
119		// construction above.
120	690	std::shared_ptr<ProofNode> pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp);
121	345	return mkTrustNode(pfs->getResult(), pfs, isConflict);
122		}
123
124	2647	TrustNode EagerProofGenerator::mkTrustedRewrite(Node a,
125		Node b,
126		std::shared_ptr<ProofNode> pf)
127		{
128	2647	if (pf == nullptr)
129		{
130		return TrustNode::null();
131		}
132	5294	Node eq = a.eqNode(b);
133	2647	setProofFor(eq, pf);
134	2647	return TrustNode::mkTrustRewrite(a, b, this);
135		}
136
137	3040	TrustNode EagerProofGenerator::mkTrustedPropagation(
138		Node n, Node exp, std::shared_ptr<ProofNode> pf)
139		{
140	3040	if (pf == nullptr)
141		{
142		return TrustNode::null();
143		}
144	3040	setProofForPropExp(n, exp, pf);
145	3040	return TrustNode::mkTrustPropExp(n, exp, this);
146		}
147
148	10030	TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f)
149		{
150		// make the lemma
151	20060	Node lem = f.orNode(f.notNode());
152	20060	return mkTrustNode(lem, PfRule::SPLIT, {}, {f}, false);
153		}
154
155	284818	std::string EagerProofGenerator::identify() const { return d_name; }
156
157	29577	} // namespace cvc5