Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/eager_proof_generator.cpp	Lines:	59	63	93.7 %
Date:	2021-08-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	85977	EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm,
25		context::Context* c,
26	85977	std::string name)
27	85977	: d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c)
28		{
29	85977	}
30
31	344294	void EagerProofGenerator::setProofFor(Node f, std::shared_ptr<ProofNode> pf)
32		{
33		// pf should prove f
34	688588	Assert(pf->getResult() == f)
35		<< "EagerProofGenerator::setProofFor: unexpected result" << std::endl
36	344294	<< "Expected: " << f << std::endl
37	344294	<< "Actual: " << pf->getResult() << std::endl;
38	344294	d_proofs[f] = pf;
39	344294	}
40	14934	void EagerProofGenerator::setProofForConflict(Node conf,
41		std::shared_ptr<ProofNode> pf)
42		{
43		// Normalize based on key
44	29868	Node ckey = TrustNode::getConflictProven(conf);
45	14934	setProofFor(ckey, pf);
46	14934	}
47
48	225425	void EagerProofGenerator::setProofForLemma(Node lem,
49		std::shared_ptr<ProofNode> pf)
50		{
51		// Normalize based on key
52	450850	Node lkey = TrustNode::getLemmaProven(lem);
53	225425	setProofFor(lkey, pf);
54	225425	}
55
56	54354	void EagerProofGenerator::setProofForPropExp(TNode lit,
57		Node exp,
58		std::shared_ptr<ProofNode> pf)
59		{
60		// Normalize based on key
61	108708	Node pekey = TrustNode::getPropExpProven(lit, exp);
62	54354	setProofFor(pekey, pf);
63	54354	}
64
65	137624	std::shared_ptr<ProofNode> EagerProofGenerator::getProofFor(Node f)
66		{
67	137624	NodeProofNodeMap::iterator it = d_proofs.find(f);
68	137624	if (it == d_proofs.end())
69		{
70	2685	return nullptr;
71		}
72	134939	return (*it).second;
73		}
74
75	804416	bool EagerProofGenerator::hasProofFor(Node f)
76		{
77	804416	return d_proofs.find(f) != d_proofs.end();
78		}
79
80	235311	TrustNode EagerProofGenerator::mkTrustNode(Node n,
81		std::shared_ptr<ProofNode> pf,
82		bool isConflict)
83		{
84	235311	if (pf == nullptr)
85		{
86		return TrustNode::null();
87		}
88	235311	if (isConflict)
89		{
90		// this shouldnt modify the key
91	12010	setProofForConflict(n, pf);
92		// we can now return the trust node
93	12010	return TrustNode::mkTrustConflict(n, this);
94		}
95		// this shouldnt modify the key
96	223301	setProofForLemma(n, pf);
97		// we can now return the trust node
98	223301	return TrustNode::mkTrustLemma(n, this);
99		}
100
101	13586	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	13586	if (exp.empty())
109		{
110	26486	std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, conc);
111	13243	return mkTrustNode(conc, pf, isConflict);
112		}
113		// otherwise, we use CDProof + SCOPE
114	686	CDProof cdp(d_pnm);
115	343	cdp.addStep(conc, id, exp, args);
116	686	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	686	std::shared_ptr<ProofNode> pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp);
121	343	return mkTrustNode(pfs->getResult(), pfs, isConflict);
122		}
123
124	3404	TrustNode EagerProofGenerator::mkTrustedRewrite(Node a,
125		Node b,
126		std::shared_ptr<ProofNode> pf)
127		{
128	3404	if (pf == nullptr)
129		{
130		return TrustNode::null();
131		}
132	6808	Node eq = a.eqNode(b);
133	3404	setProofFor(eq, pf);
134	3404	return TrustNode::mkTrustRewrite(a, b, this);
135		}
136
137	2559	TrustNode EagerProofGenerator::mkTrustedPropagation(
138		Node n, Node exp, std::shared_ptr<ProofNode> pf)
139		{
140	2559	if (pf == nullptr)
141		{
142		return TrustNode::null();
143		}
144	2559	setProofForPropExp(n, exp, pf);
145	2559	return TrustNode::mkTrustPropExp(n, exp, this);
146		}
147
148	10041	TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f)
149		{
150		// make the lemma
151	20082	Node lem = f.orNode(f.notNode());
152	20082	return mkTrustNode(lem, PfRule::SPLIT, {}, {f}, false);
153		}
154
155	263455	std::string EagerProofGenerator::identify() const { return d_name; }
156
157	29337	} // namespace cvc5