cnf_theorem_producer.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file cnf_theorem_producer.h
00004  *\brief Implementation of CNF_Rules API
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Thu Jan  5 05:33:42 2006
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  */
00020 /*****************************************************************************/
00021 
00022 #ifndef _cvc3__sat__cnf_theorem_producer_h_
00023 #define _cvc3__sat__cnf_theorem_producer_h_
00024 
00025 #include "theorem_producer.h"
00026 #include "cnf_rules.h"
00027 
00028 namespace CVC3 {
00029 
00030   class CNF_TheoremProducer
00031     : public CNF_Rules,
00032       public TheoremProducer {
00033 
00034   public:
00035     CNF_TheoremProducer(TheoremManager* tm): TheoremProducer(tm) { }
00036     ~CNF_TheoremProducer() { }
00037 
00038     Theorem learnedClause(const Theorem& thm);
00039     Theorem ifLiftRule(const Expr& e, int itePos);
00040 
00041   }; // end of class CNF_TheoremProducer
00042 } // end of namespace CVC3
00043 #endif

Generated on Tue Jul 3 14:33:35 2007 for CVC3 by  doxygen 1.5.1