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 void learnedClauses(const Theorem& thm,
00053                                 std::vector<Theorem>&,
00054                                 bool newLemma) = 0;
00055 
00056     //! |- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))
00057     virtual Theorem ifLiftRule(const Expr& e, int itePos) = 0;
00058     virtual Theorem CNFAddUnit(const Theorem& thm) = 0 ;
00059     virtual Theorem CNFConvert(const Expr& e, const Theorem& thm) = 0 ;
00060     virtual Theorem CNFtranslate(const Expr& before, 
00061          const Expr& after, 
00062          std::string reason, 
00063          int pos) = 0;
00064 
00065     virtual Theorem CNFITEtranslate(const Expr& before, 
00066             const std::vector<Expr>& after,
00067             const std::vector<Theorem>& thms,
00068             int pos) = 0;
00069 
00070     /*! @} */ // end of CNF_Rules
00071   }; // end of class CNF_Rules
00072 
00073 } // end of namespace CVC3
00074 
00075 #endif

Generated on Wed Nov 18 16:13:29 2009 for CVC3 by  doxygen 1.5.2