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     //    unsigned d_insts; //by yeting, this is to store the number of instantiations. debug only
00042   public:
00043     Proof(const Expr &e) : d_proof(e) { } // Constructor
00044     Proof(const Proof& p) : d_proof(p.d_proof) { } // Copy constructor
00045     Proof() : d_proof() { } // Null proof constructor
00046     Expr getExpr() const { return d_proof; } // Extract the expr handle
00047     bool isNull() const { return d_proof.isNull(); }
00048     // Printing
00049     friend std::ostream& operator<<(std::ostream& os, const Proof& pf);
00050     std::string toString() const {
00051       std::ostringstream ss;
00052       ss<<(*this);
00053       return ss.str();
00054     }
00055   }; // End of class Proof
00056 
00057   inline std::ostream& operator<<(std::ostream& os, const Proof& pf) {
00058     return os << "Proof(" << pf.getExpr() << ")";
00059   }
00060 
00061   inline bool operator==(const Proof& pf1, const Proof& pf2) {
00062     return pf1.getExpr() == pf2.getExpr();
00063   }
00064 
00065 } // end of namespace CVC3
00066 #endif

Generated on Wed Nov 18 16:13:30 2009 for CVC3 by  doxygen 1.5.2