1 /*********************                                                        */
2 /*! \file proof.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Morgan Deters, Tim King, Guy Katz
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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 [[ Add one-line brief description here ]]
13  **
14  ** [[ Add lengthier description here ]]
15  ** \todo document this file
16  **/
17 
18 #include "cvc4_public.h"
19 
20 #ifndef __CVC4__PROOF_H
21 #define __CVC4__PROOF_H
22 
23 #include <iosfwd>
24 #include <unordered_map>
25 
26 namespace CVC4 {
27 
28 class Expr;
29 class ProofLetCount;
30 struct ExprHashFunction;
31 
32 typedef std::unordered_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap;
33 
34 class CVC4_PUBLIC Proof
35 {
36  public:
~Proof()37   virtual ~Proof() {}
38   virtual void toStream(std::ostream& out) const = 0;
39   virtual void toStream(std::ostream& out, const ProofLetMap& map) const = 0;
40 };/* class Proof */
41 
42 }/* CVC4 namespace */
43 
44 #endif /* __CVC4__PROOF_H */
45