1 /*****************************************************************************/ 2 /*! 3 * \file cnf_rules.h 4 * \brief Abstract proof rules for CNF conversion 5 * 6 * Author: Clark Barrett 7 * 8 * Created: Thu Jan 5 05:24:45 2006 9 * 10 * <hr> 11 * 12 * License to use, copy, modify, sell and/or distribute this software 13 * and its documentation for any purpose is hereby granted without 14 * royalty, subject to the terms and conditions defined in the \ref 15 * LICENSE file provided with this distribution. 16 * 17 * <hr> 18 * 19 */ 20 /*****************************************************************************/ 21 22 #ifndef _cvc3__sat__cnf_rules_h_ 23 #define _cvc3__sat__cnf_rules_h_ 24 25 namespace CVC3 { 26 27 class Theorem; 28 29 /*! \defgroup CNF_Rules Proof Rules for the Search Engines 30 * \ingroup CNF 31 */ 32 //! API to the CNF proof rules 33 /*! \ingroup CNF_Rules */ 34 class CNF_Rules { 35 /*! \addtogroup CNF_Rules 36 * @{ 37 */ 38 public: 39 //! Destructor ~CNF_Rules()40 virtual ~CNF_Rules() { } 41 42 // A_1,...,A_n |- B ==> |- (OR !A_1 ... !A_n B) 43 /*! @brief Learned clause rule: 44 \f[\frac{A_1,\ldots,A_n\vdash B} 45 {\vdash\neg A_1\vee\cdots\vee \neg A_n\vee B}\f] 46 * 47 * \param thm is the theorem 48 * \f$ A_1,\ldots,A_n\vdash B\f$ 49 * Each \f$A_i\f$ and \f$B\f$ should be literals 50 * \f$B\f$ can also be \f$\mathrm{FALSE}\f$ 51 */ 52 virtual void learnedClauses(const Theorem& thm, 53 std::vector<Theorem>&, 54 bool newLemma) = 0; 55 56 //! |- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _)) 57 virtual Theorem ifLiftRule(const Expr& e, int itePos) = 0; 58 virtual Theorem CNFAddUnit(const Theorem& thm) = 0 ; 59 virtual Theorem CNFConvert(const Expr& e, const Theorem& thm) = 0 ; 60 virtual Theorem CNFtranslate(const Expr& before, 61 const Expr& after, 62 std::string reason, 63 int pos, 64 const std::vector<Theorem>& thms) = 0; 65 66 virtual Theorem CNFITEtranslate(const Expr& before, 67 const std::vector<Expr>& after, 68 const std::vector<Theorem>& thms, 69 int pos) = 0; 70 71 /*! @} */ // end of CNF_Rules 72 }; // end of class CNF_Rules 73 74 } // end of namespace CVC3 75 76 #endif 77