Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/proof_generator.h	Lines:	1	1	100.0 %
Date:	2021-09-30	Branches:	0	0	0.0 %


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

#include "cvc5_private.h"

#ifndef CVC5__PROOF__PROOF_GENERATOR_H
#define CVC5__PROOF__PROOF_GENERATOR_H

#include "expr/node.h"

namespace cvc5 {

class CDProof;
class ProofNode;

/** An overwrite policy for CDProof */
enum class CDPOverwrite : uint32_t
{
  // always overwrite an existing step.
  ALWAYS,
  // overwrite ASSUME with non-ASSUME steps.
  ASSUME_ONLY,
  // never overwrite an existing step.
  NEVER,
};
/** Writes a overwrite policy name to a stream. */
std::ostream& operator<<(std::ostream& out, CDPOverwrite opol);

/**
 * An abstract proof generator class.
 *
 * A proof generator is intended to be used as a utility e.g. in theory
 * solvers for constructing and storing proofs internally. A theory may have
 * multiple instances of ProofGenerator objects, e.g. if it has more than one
 * way of justifying lemmas or conflicts.
 *
 * A proof generator has two main interfaces for generating proofs:
 * (1) getProofFor, and (2) addProofTo. The latter is optional.
 *
 * The addProofTo method can be used as an optimization for avoiding
 * the construction of the ProofNode for a given fact.
 *
 * If no implementation of addProofTo is provided, then addProofTo(f, pf)
 * calls getProofFor(f) and links the topmost ProofNode of the returned proof
 * into pf. Note this top-most ProofNode can be avoided in the addProofTo
 * method.
 */
class ProofGenerator
{
 public:
  ProofGenerator();
  virtual ~ProofGenerator();
  /** Get the proof for formula f
   *
   * This forces the proof generator to construct a proof for formula f and
   * return it. If this is an "eager" proof generator, this function is expected
   * to be implemented as a map lookup. If this is a "lazy" proof generator,
   * this function is expected to invoke a proof producing procedure of the
   * generator.
   *
   * It should be the case that hasProofFor(f) is true.
   *
   * @param f The fact to get the proof for.
   * @return The proof for f.
   */
  virtual std::shared_ptr<ProofNode> getProofFor(Node f);
  /**
   * Add the proof for formula f to proof pf. The proof of f is overwritten in
   * pf based on the policy opolicy.
   *
   * @param f The fact to get the proof for.
   * @param pf The CDProof object to add the proof to.
   * @param opolicy The overwrite policy for adding to pf.
   * @param doCopy Whether to do a deep copy of the proof steps into pf.
   * @return True if this call was sucessful.
   */
  virtual bool addProofTo(Node f,
                          CDProof* pf,
                          CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY,
                          bool doCopy = false);
  /**
   * Can we give the proof for formula f? This is used for debugging. This
   * returns false if the generator cannot provide a proof of formula f.
   *
   * Also notice that this function does not require the proof for f to be
   * constructed at the time of this call. Thus, if this is a "lazy" proof
   * generator, it is expected that this call is implemented as a map lookup
   * into the bookkeeping maintained by the generator only.
   *
   * Notice the default return value is true. In other words, a proof generator
   * may choose to override this function to verify the construction, although
   * we do not insist this is the case.
   */
  virtual bool hasProofFor(Node f) { return true; }
  /** Identify this generator (for debugging, etc..) */
  virtual std::string identify() const = 0;
};

}  // namespace cvc5

#endif /* CVC5__PROOF__PROOF_GENERATOR_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Gereon Kremer
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		* The abstract proof generator class.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__PROOF__PROOF_GENERATOR_H
19		#define CVC5__PROOF__PROOF_GENERATOR_H
20
21		#include "expr/node.h"
22
23		namespace cvc5 {
24
25		class CDProof;
26		class ProofNode;
27
28		/** An overwrite policy for CDProof */
29		enum class CDPOverwrite : uint32_t
30		{
31		// always overwrite an existing step.
32		ALWAYS,
33		// overwrite ASSUME with non-ASSUME steps.
34		ASSUME_ONLY,
35		// never overwrite an existing step.
36		NEVER,
37		};
38		/** Writes a overwrite policy name to a stream. */
39		std::ostream& operator<<(std::ostream& out, CDPOverwrite opol);
40
41		/**
42		* An abstract proof generator class.
43		*
44		* A proof generator is intended to be used as a utility e.g. in theory
45		* solvers for constructing and storing proofs internally. A theory may have
46		* multiple instances of ProofGenerator objects, e.g. if it has more than one
47		* way of justifying lemmas or conflicts.
48		*
49		* A proof generator has two main interfaces for generating proofs:
50		* (1) getProofFor, and (2) addProofTo. The latter is optional.
51		*
52		* The addProofTo method can be used as an optimization for avoiding
53		* the construction of the ProofNode for a given fact.
54		*
55		* If no implementation of addProofTo is provided, then addProofTo(f, pf)
56		* calls getProofFor(f) and links the topmost ProofNode of the returned proof
57		* into pf. Note this top-most ProofNode can be avoided in the addProofTo
58		* method.
59		*/
60		class ProofGenerator
61		{
62		public:
63		ProofGenerator();
64		virtual ~ProofGenerator();
65		/** Get the proof for formula f
66		*
67		* This forces the proof generator to construct a proof for formula f and
68		* return it. If this is an "eager" proof generator, this function is expected
69		* to be implemented as a map lookup. If this is a "lazy" proof generator,
70		* this function is expected to invoke a proof producing procedure of the
71		* generator.
72		*
73		* It should be the case that hasProofFor(f) is true.
74		*
75		* @param f The fact to get the proof for.
76		* @return The proof for f.
77		*/
78		virtual std::shared_ptr<ProofNode> getProofFor(Node f);
79		/**
80		* Add the proof for formula f to proof pf. The proof of f is overwritten in
81		* pf based on the policy opolicy.
82		*
83		* @param f The fact to get the proof for.
84		* @param pf The CDProof object to add the proof to.
85		* @param opolicy The overwrite policy for adding to pf.
86		* @param doCopy Whether to do a deep copy of the proof steps into pf.
87		* @return True if this call was sucessful.
88		*/
89		virtual bool addProofTo(Node f,
90		CDProof* pf,
91		CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY,
92		bool doCopy = false);
93		/**
94		* Can we give the proof for formula f? This is used for debugging. This
95		* returns false if the generator cannot provide a proof of formula f.
96		*
97		* Also notice that this function does not require the proof for f to be
98		* constructed at the time of this call. Thus, if this is a "lazy" proof
99		* generator, it is expected that this call is implemented as a map lookup
100		* into the bookkeeping maintained by the generator only.
101		*
102		* Notice the default return value is true. In other words, a proof generator
103		* may choose to override this function to verify the construction, although
104		* we do not insist this is the case.
105		*/
106	27234	virtual bool hasProofFor(Node f) { return true; }
107		/** Identify this generator (for debugging, etc..) */
108		virtual std::string identify() const = 0;
109		};
110
111		} // namespace cvc5
112
113		#endif /* CVC5__PROOF__PROOF_GENERATOR_H */