CVC3

# 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 {
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,
00064          const std::vector<Theorem>& thms) = 0;
00065
00066     virtual Theorem CNFITEtranslate(const Expr& before,
00067             const std::vector<Expr>& after,
00068             const std::vector<Theorem>& thms,
00069             int pos) = 0;
00070
00071     /*! @} */ // end of CNF_Rules
00072   }; // end of class CNF_Rules
00073
00074 } // end of namespace CVC3
00075
00076 #endif