CVC3

uf_proof_rules.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file uf_proof_rules.h
00004  *\brief Abstract interface for uninterpreted function/predicate proof rules
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Tue Aug 31 23:12:01 2004
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  * CLASS: UFProofRules
00020  * 
00021  */
00022 /*****************************************************************************/
00023 
00024 #ifndef _cvc3__theory_uf__uf_proof_rules_h_
00025 #define _cvc3__theory_uf__uf_proof_rules_h_
00026 
00027 namespace CVC3 {
00028 
00029   class Expr;
00030   class Theorem;
00031 
00032   class UFProofRules {
00033   public:
00034     // Destructor
00035     virtual ~UFProofRules() { }
00036 
00037     ////////////////////////////////////////////////////////////////////
00038     // Proof rules
00039     ////////////////////////////////////////////////////////////////////
00040 
00041     virtual Theorem relToClosure(const Theorem& rel) = 0;
00042     virtual Theorem relTrans(const Theorem& t1, const Theorem& t2) = 0;
00043 
00044     //! Beta reduction: |- (lambda x. f(x))(arg) = f(arg)
00045     virtual Theorem applyLambda(const Expr& e) = 0;
00046     //! Replace LETDECL in the operator with the definition
00047     virtual Theorem rewriteOpDef(const Expr& e) = 0;
00048 
00049   }; // end of class UFProofRules
00050 
00051 } // end of namespace CVC3
00052 
00053 #endif