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