Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/eager_proof_generator.cpp	Lines:	59	63	93.7 %
Date:	2021-05-22	Branches:	81	198	40.9 %


/******************************************************************************
 * 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 "theory/eager_proof_generator.h"

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

namespace cvc5 {
namespace theory {

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 theory
}  // 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 "theory/eager_proof_generator.h"
17
18		#include "expr/proof.h"
19		#include "expr/proof_node.h"
20		#include "expr/proof_node_manager.h"
21
22		namespace cvc5 {
23		namespace theory {
24
25	68293	EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm,
26		context::Context* c,
27	68293	std::string name)
28	68293	: d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c)
29		{
30	68293	}
31
32	357361	void EagerProofGenerator::setProofFor(Node f, std::shared_ptr<ProofNode> pf)
33		{
34		// pf should prove f
35	714722	Assert(pf->getResult() == f)
36		<< "EagerProofGenerator::setProofFor: unexpected result" << std::endl
37	357361	<< "Expected: " << f << std::endl
38	357361	<< "Actual: " << pf->getResult() << std::endl;
39	357361	d_proofs[f] = pf;
40	357361	}
41	15542	void EagerProofGenerator::setProofForConflict(Node conf,
42		std::shared_ptr<ProofNode> pf)
43		{
44		// Normalize based on key
45	31084	Node ckey = TrustNode::getConflictProven(conf);
46	15542	setProofFor(ckey, pf);
47	15542	}
48
49	209663	void EagerProofGenerator::setProofForLemma(Node lem,
50		std::shared_ptr<ProofNode> pf)
51		{
52		// Normalize based on key
53	419326	Node lkey = TrustNode::getLemmaProven(lem);
54	209663	setProofFor(lkey, pf);
55	209663	}
56
57	70400	void EagerProofGenerator::setProofForPropExp(TNode lit,
58		Node exp,
59		std::shared_ptr<ProofNode> pf)
60		{
61		// Normalize based on key
62	140800	Node pekey = TrustNode::getPropExpProven(lit, exp);
63	70400	setProofFor(pekey, pf);
64	70400	}
65
66	151470	std::shared_ptr<ProofNode> EagerProofGenerator::getProofFor(Node f)
67		{
68	151470	NodeProofNodeMap::iterator it = d_proofs.find(f);
69	151470	if (it == d_proofs.end())
70		{
71	2369	return nullptr;
72		}
73	149101	return (*it).second;
74		}
75
76	804052	bool EagerProofGenerator::hasProofFor(Node f)
77		{
78	804052	return d_proofs.find(f) != d_proofs.end();
79		}
80
81	220181	TrustNode EagerProofGenerator::mkTrustNode(Node n,
82		std::shared_ptr<ProofNode> pf,
83		bool isConflict)
84		{
85	220181	if (pf == nullptr)
86		{
87		return TrustNode::null();
88		}
89	220181	if (isConflict)
90		{
91		// this shouldnt modify the key
92	11465	setProofForConflict(n, pf);
93		// we can now return the trust node
94	11465	return TrustNode::mkTrustConflict(n, this);
95		}
96		// this shouldnt modify the key
97	208716	setProofForLemma(n, pf);
98		// we can now return the trust node
99	208716	return TrustNode::mkTrustLemma(n, this);
100		}
101
102	12766	TrustNode EagerProofGenerator::mkTrustNode(Node conc,
103		PfRule id,
104		const std::vector<Node>& exp,
105		const std::vector<Node>& args,
106		bool isConflict)
107		{
108		// if no children, its easy
109	12766	if (exp.empty())
110		{
111	24638	std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, conc);
112	12319	return mkTrustNode(conc, pf, isConflict);
113		}
114		// otherwise, we use CDProof + SCOPE
115	894	CDProof cdp(d_pnm);
116	447	cdp.addStep(conc, id, exp, args);
117	894	std::shared_ptr<ProofNode> pf = cdp.getProofFor(conc);
118		// We use mkNode instead of mkScope, since there is no reason to check
119		// whether the free assumptions of pf are in exp, since they are by the
120		// construction above.
121	894	std::shared_ptr<ProofNode> pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp);
122	447	return mkTrustNode(pfs->getResult(), pfs, isConflict);
123		}
124
125	3404	TrustNode EagerProofGenerator::mkTrustedRewrite(
126		Node a, Node b, 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	2099	TrustNode EagerProofGenerator::mkTrustedPropagation(
138		Node n, Node exp, std::shared_ptr<ProofNode> pf)
139		{
140	2099	if (pf == nullptr)
141		{
142		return TrustNode::null();
143		}
144	2099	setProofForPropExp(n, exp, pf);
145	2099	return TrustNode::mkTrustPropExp(n, exp, this);
146		}
147
148	9864	TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f)
149		{
150		// make the lemma
151	19728	Node lem = f.orNode(f.notNode());
152	19728	return mkTrustNode(lem, PfRule::SPLIT, {}, {f}, false);
153		}
154
155	278357	std::string EagerProofGenerator::identify() const { return d_name; }
156
157		} // namespace theory
158	28194	} // namespace cvc5