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