CVC3

uf_theorem_producer.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file uf_theorem_producer.h
00004  *\brief TRUSTED implementation of uninterpreted function/predicate proof rules
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Tue Aug 31 23:14:54 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: UFTheoremProducer
00020  * 
00021  */
00022 /*****************************************************************************/
00023 #ifndef _cvc3__theory_uf__uf_theorem_producer_h_
00024 #define _cvc3__theory_uf__uf_theorem_producer_h_
00025 
00026 #include "uf_proof_rules.h"
00027 #include "theorem_producer.h"
00028 
00029 namespace CVC3 {
00030 
00031   class TheoryUF;
00032 
00033 class UFTheoremProducer: public UFProofRules, public TheoremProducer {
00034     TheoryUF* d_theoryUF;
00035   private:
00036   public:
00037     //! Constructor
00038     UFTheoremProducer(TheoremManager* tm, TheoryUF* theoryUF) :
00039       TheoremProducer(tm), d_theoryUF(theoryUF) { }
00040 
00041     Theorem relToClosure(const Theorem& rel);
00042     Theorem relTrans(const Theorem& t1, const Theorem& t2);
00043     Theorem applyLambda(const Expr& e);
00044     Theorem rewriteOpDef(const Expr& e);
00045     
00046   }; // end of class UFTheoremProducer
00047 } // end of namespace CVC3
00048 
00049 #endif
00050