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