GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_generator.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

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