proof.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file proof.h
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Dec 10 00:37:49 GMT 2002
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 // CLASS: Proof
00021 //
00022 // AUTHOR: Sergey Berezin, 12/03/2002
00023 //
00024 // Abstract:
00025 //
00026 // Proof is a wrapper around Expr, to prevent accidental mix-up.  Only
00027 // proof rules and adaptors are supposed to use any of its methods.
00028 ///////////////////////////////////////////////////////////////////////////////
00029 #ifndef _cvc3__expr_h_
00030 #include "expr.h"
00031 #endif
00032 
00033 #ifndef _cvc3__proof_h_
00034 #define _cvc3__proof_h_
00035 
00036 namespace CVC3 {
00037 
00038   class Proof {
00039   private:
00040     Expr d_proof;
00041   public:
00042     Proof(const Expr &e) : d_proof(e) { } // Constructor
00043     Proof(const Proof& p) : d_proof(p.d_proof) { } // Copy constructor
00044     Proof() : d_proof() { } // Null proof constructor
00045     Expr getExpr() const { return d_proof; } // Extract the expr handle
00046     bool isNull() const { return d_proof.isNull(); }
00047     // Printing
00048     friend std::ostream& operator<<(std::ostream& os, const Proof& pf);
00049     std::string toString() const {
00050       std::ostringstream ss;
00051       ss<<(*this);
00052       return ss.str();
00053     }
00054   }; // End of class Proof
00055 
00056   inline std::ostream& operator<<(std::ostream& os, const Proof& pf) {
00057     return os << "Proof(" << pf.getExpr() << ")";
00058   }
00059 
00060   inline bool operator==(const Proof& pf1, const Proof& pf2) {
00061     return pf1.getExpr() == pf2.getExpr();
00062   }
00063 
00064 } // end of namespace CVC3
00065 #endif

Generated on Tue Jul 3 14:33:38 2007 for CVC3 by  doxygen 1.5.1