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