cnf_rules.h

Go to the documentation of this file.
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

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