CVC3  2.4.1
proof.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file proof.h
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Dec 10 00:37:49 GMT 2002
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 // CLASS: Proof
21 //
22 // AUTHOR: Sergey Berezin, 12/03/2002
23 //
24 // Abstract:
25 //
26 // Proof is a wrapper around Expr, to prevent accidental mix-up. Only
27 // proof rules and adaptors are supposed to use any of its methods.
28 ///////////////////////////////////////////////////////////////////////////////
29 #ifndef _cvc3__expr_h_
30 #include "expr.h"
31 #endif
32 
33 #ifndef _cvc3__proof_h_
34 #define _cvc3__proof_h_
35 
36 namespace CVC3 {
37 
38  class Proof {
39  private:
41  // unsigned d_insts; //by yeting, this is to store the number of instantiations. debug only
42  public:
43  Proof(const Expr &e) : d_proof(e) { } // Constructor
44  Proof(const Proof& p) : d_proof(p.d_proof) { } // Copy constructor
45  Proof() : d_proof() { } // Null proof constructor
46  Expr getExpr() const { return d_proof; } // Extract the expr handle
47  bool isNull() const { return d_proof.isNull(); }
48  // Printing
49  friend std::ostream& operator<<(std::ostream& os, const Proof& pf);
50  std::string toString() const {
51  std::ostringstream ss;
52  ss<<(*this);
53  return ss.str();
54  }
55  }; // End of class Proof
56 
57  inline std::ostream& operator<<(std::ostream& os, const Proof& pf) {
58  return os << "Proof(" << pf.getExpr() << ")";
59  }
60 
61  inline bool operator==(const Proof& pf1, const Proof& pf2) {
62  return pf1.getExpr() == pf2.getExpr();
63  }
64 
65 } // end of namespace CVC3
66 #endif
bool isNull() const
Definition: expr.h:1223
std::string toString() const
Definition: proof.h:50
Data structure of expressions in CVC3.
Definition: expr.h:133
bool isNull() const
Definition: proof.h:47
Expr d_proof
Definition: proof.h:40
ostream & operator<<(ostream &os, const Expr &e)
Definition: expr.cpp:621
friend std::ostream & operator<<(std::ostream &os, const Proof &pf)
Definition: proof.h:57
Proof()
Definition: proof.h:45
bool operator==(const Expr &e1, const Expr &e2)
Definition: expr.h:1600
Expr getExpr() const
Definition: proof.h:46
Proof(const Proof &p)
Definition: proof.h:44
Definition of the API to expression package. See class Expr for details.
Definition: expr.cpp:35
Proof(const Expr &e)
Definition: proof.h:43