29 #ifndef _cvc3__expr_h_
33 #ifndef _cvc3__proof_h_
34 #define _cvc3__proof_h_
51 std::ostringstream ss;
58 return os <<
"Proof(" << pf.
getExpr() <<
")";
std::string toString() const
Data structure of expressions in CVC3.
ostream & operator<<(ostream &os, const Expr &e)
friend std::ostream & operator<<(std::ostream &os, const Proof &pf)
bool operator==(const Expr &e1, const Expr &e2)
Definition of the API to expression package. See class Expr for details.