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