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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 nonASSUME 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 topmost 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 
411169 
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 */ 