00001 /*****************************************************************************/ 00002 /*! 00003 * \file cnf_rules.h 00004 * \brief Abstract proof rules for CNF conversion 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Thu Jan 5 05:24:45 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_rules_h_ 00023 #define _cvc3__sat__cnf_rules_h_ 00024 00025 namespace CVC3 { 00026 00027 class Theorem; 00028 00029 /*! \defgroup CNF_Rules Proof Rules for the Search Engines 00030 * \ingroup CNF 00031 */ 00032 //! API to the CNF proof rules 00033 /*! \ingroup CNF_Rules */ 00034 class CNF_Rules { 00035 /*! \addtogroup CNF_Rules 00036 * @{ 00037 */ 00038 public: 00039 //! Destructor 00040 virtual ~CNF_Rules() { } 00041 00042 // A_1,...,A_n |- B ==> |- (OR !A_1 ... !A_n B) 00043 /*! @brief Learned clause rule: 00044 \f[\frac{A_1,\ldots,A_n\vdash B} 00045 {\vdash\neg A_1\vee\cdots\vee \neg A_n\vee B}\f] 00046 * 00047 * \param thm is the theorem 00048 * \f$ A_1,\ldots,A_n\vdash B\f$ 00049 * Each \f$A_i\f$ and \f$B\f$ should be literals 00050 * \f$B\f$ can also be \f$\mathrm{FALSE}\f$ 00051 */ 00052 virtual Theorem learnedClause(const Theorem& thm) = 0; 00053 00054 //! |- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _)) 00055 virtual Theorem ifLiftRule(const Expr& e, int itePos) = 0; 00056 00057 /*! @} */ // end of CNF_Rules 00058 }; // end of class CNF_Rules 00059 00060 } // end of namespace CVC3 00061 00062 #endif