CVC3  2.4.1
search_rules.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file search_rules.h
4  * \brief Abstract proof rules interface to the simple search engine
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Mon Feb 24 14:19:48 2003
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__search__search_rules_h_
23 #define _cvc3__search__search_rules_h_
24 
25 namespace CVC3 {
26 
27  class Theorem;
28  class Expr;
29 
30 /*! \defgroup SE_Rules Proof Rules for the Search Engines
31  * \ingroup SE
32  */
33  //! API to the proof rules for the Search Engines
34  /*! \ingroup SE_Rules */
36  /*! \addtogroup SE_Rules
37  * @{
38  */
39  public:
40  //! Destructor
41  virtual ~SearchEngineRules() { }
42 
43  /*! Eliminate skolem axioms:
44  * Gamma, Delta |- false => Gamma|- false
45  * where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)}
46  * and gamma does not contain any of the skolem constants c.
47  */
48  virtual Theorem eliminateSkolemAxioms(const Theorem& tFalse,
49  const std::vector<Theorem>& delta) = 0;
50 
51  // !A |- FALSE ==> |- A
52  /*! @brief Proof by contradiction:
53  \f[\frac{\Gamma, \neg A \vdash\mathrm{FALSE}}{\Gamma \vdash A}\f]
54  */
55  /*! \f$\neg A\f$ does not have to be present in the assumptions.
56  * \param a is the assumption \e A
57  *
58  * \param pfFalse is the theorem \f$\Gamma, \neg A \vdash\mathrm{FALSE}\f$
59  */
60  virtual Theorem proofByContradiction(const Expr& a,
61  const Theorem& pfFalse) = 0;
62 
63  // A |- FALSE ==> !A
64  /*! @brief Negation introduction:
65  \f[\frac{\Gamma, A \vdash\mathrm{FALSE}}{\Gamma\vdash\neg A}\f]
66  */
67  /*!
68  * \param not_a is the formula \f$\neg A\f$. We pass the negation
69  * \f$\neg A\f$, and not just \e A, for efficiency: building
70  * \f$\neg A\f$ is more expensive (due to uniquifying pointers in
71  * Expr package) than extracting \e A from \f$\neg A\f$.
72  *
73  * \param pfFalse is the theorem \f$\Gamma, A \vdash\mathrm{FALSE}\f$
74  */
75  virtual Theorem negIntro(const Expr& not_a, const Theorem& pfFalse) = 0;
76 
77  // u1:A |- C, u2:!A |- C ==> |- C
78  /*! @brief Case split:
79  \f[\frac{\Gamma_1, A\vdash C \quad \Gamma_2, \neg A\vdash C}
80  {\Gamma_1\cup\Gamma_2\vdash C}\f]
81  */
82  /*!
83  * \param a is the assumption A to split on
84  *
85  * \param a_proves_c is the theorem \f$\Gamma_1, A\vdash C\f$
86  *
87  * \param not_a_proves_c is the theorem \f$\Gamma_2, \neg A\vdash C\f$
88  */
89  virtual Theorem caseSplit(const Expr& a,
90  const Theorem& a_proves_c,
91  const Theorem& not_a_proves_c) = 0;
92 
93  // Gamma, A_1,...,A_n |- FALSE ==> Gamma |- (OR !A_1 ... !A_n)
94  /*! @brief Conflict clause rule:
95  \f[\frac{\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}}
96  {\Gamma\vdash\neg A_1\vee\cdots\vee \neg A_n}\f]
97  */
98  /*!
99  * \param thm is the theorem
100  * \f$\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}\f$
101  *
102  * \param lits is the vector of literals <em>A<sub>i</sub></em>.
103  * They must be present in the set of assumptions of \e thm.
104  *
105  * \param gamma FIXME: document this!!
106  */
107  virtual Theorem conflictClause(const Theorem& thm,
108  const std::vector<Theorem>& lits,
109  const std::vector<Theorem>& gamma) = 0;
110 
111 
112  // "Cut" rule: { G_i |- A_i }; G', { A_i } |- B ==> union(G_i)+G' |- B.
113  /*! @brief Cut rule:
114  \f[\frac{\Gamma_1\vdash A_1\quad\cdots\quad\Gamma_n\vdash A_n
115  \quad \Gamma', A_1,\ldots,A_n\vdash B}
116  {\bigcup_{i=1}^n\Gamma_i\cup\Gamma'\vdash B}\f]
117  */
118  /*!
119  * \param thmsA is a vector of theorems \f$\Gamma_i\vdash A_i\f$
120  *
121  * \param as_prove_b is the theorem
122  * \f$\Gamma', A_1,\ldots,A_n\vdash B\f$
123  * (the name means "A's prove B")
124  */
125  virtual Theorem cutRule(const std::vector<Theorem>& thmsA,
126  const Theorem& as_prove_b) = 0;
127 
128  // { G_j |- !A_j, j in [1..n]-{i} }
129  // G |- (OR A_1 ... A_i ... A_n) ==> G, G_j |- A_i
130  /*! @brief Unit propagation rule:
131  \f[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n]-\{i\}
132  \quad \Gamma\vdash A_1\vee\cdots\vee A_n}
133  {\bigcup_{j\in[1\ldots n]-\{i\}}\Gamma_j\cup\Gamma\vdash A_i}\f]
134  */
135  /*!
136  * \param clause is the proof of the clause \f$ \Gamma\vdash
137  * A_1\vee\cdots\vee A_n\f$
138  *
139  * \param i is the index (0..n-1) of the literal to be unit-propagated
140  *
141  * \param thms is the vector of theorems \f$\Gamma_j\vdash\neg
142  * A_j\f$ for all literals except <em>A<sub>i</sub></em>
143  */
144  virtual Theorem unitProp(const std::vector<Theorem>& thms,
145  const Theorem& clause, unsigned i) = 0;
146 
147  // { G_j |- !A_j, j in [1..n] } , G |- (OR A_1 ... A_n) ==> FALSE
148  /*! @brief "Conflict" rule (all literals in a clause become FALSE)
149  \f[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n]
150  \quad \Gamma\vdash A_1\vee\cdots\vee A_n}
151  {\bigcup_{j\in[1\ldots n]}\Gamma_j\cup\Gamma
152  \vdash\mathrm{FALSE}}\f]
153  */
154  /*!
155  * \param clause is the proof of the clause \f$ \Gamma\vdash
156  * A_1\vee\cdots\vee A_n\f$
157  *
158  * \param thms is the vector of theorems \f$\Gamma_j\vdash\neg
159  * A_j\f$
160  */
161  virtual Theorem conflictRule(const std::vector<Theorem>& thms,
162  const Theorem& clause) = 0;
163 
164 
165  // Unit propagation for AND
166  virtual Theorem propAndrAF(const Theorem& andr_th,
167  bool left,
168  const Theorem& b_th) = 0;
169 
170  virtual Theorem propAndrAT(const Theorem& andr_th,
171  const Theorem& l_th,
172  const Theorem& r_th) = 0;
173 
174 
175  virtual void propAndrLRT(const Theorem& andr_th,
176  const Theorem& a_th,
177  Theorem* l_th,
178  Theorem* r_th) = 0;
179 
180  virtual Theorem propAndrLF(const Theorem& andr_th,
181  const Theorem& a_th,
182  const Theorem& r_th) = 0;
183 
184  virtual Theorem propAndrRF(const Theorem& andr_th,
185  const Theorem& a_th,
186  const Theorem& l_th) = 0;
187 
188  // Conflicts for AND
189  virtual Theorem confAndrAT(const Theorem& andr_th,
190  const Theorem& a_th,
191  bool left,
192  const Theorem& b_th) = 0;
193 
194  virtual Theorem confAndrAF(const Theorem& andr_th,
195  const Theorem& a_th,
196  const Theorem& l_th,
197  const Theorem& r_th) = 0;
198 
199  // Unit propagation for IFF
200  virtual Theorem propIffr(const Theorem& iffr_th,
201  int p,
202  const Theorem& a_th,
203  const Theorem& b_th) = 0;
204 
205  // Conflicts for IFF
206  virtual Theorem confIffr(const Theorem& iffr_th,
207  const Theorem& i_th,
208  const Theorem& l_th,
209  const Theorem& r_th) = 0;
210 
211  // Unit propagation for ITE
212  virtual Theorem propIterIte(const Theorem& iter_th,
213  bool left,
214  const Theorem& if_th,
215  const Theorem& then_th) = 0;
216 
217  virtual void propIterIfThen(const Theorem& iter_th,
218  bool left,
219  const Theorem& ite_th,
220  const Theorem& then_th,
221  Theorem* if_th,
222  Theorem* else_th) = 0;
223 
224  virtual Theorem propIterThen(const Theorem& iter_th,
225  const Theorem& ite_th,
226  const Theorem& if_th) = 0;
227 
228  // Conflict for ITE
229  virtual Theorem confIterThenElse(const Theorem& iter_th,
230  const Theorem& ite_th,
231  const Theorem& then_th,
232  const Theorem& else_th) = 0;
233 
234  virtual Theorem confIterIfThen(const Theorem& iter_th,
235  bool left,
236  const Theorem& ite_th,
237  const Theorem& if_th,
238  const Theorem& then_th) = 0;
239 
240  // CNF Rules
241 
242  //! AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v]
243  virtual Theorem andCNFRule(const Theorem& thm) = 0;
244  //! OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v]
245  virtual Theorem orCNFRule(const Theorem& thm) = 0;
246  //! (x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
247  virtual Theorem impCNFRule(const Theorem& thm) = 0;
248  //! (x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
249  virtual Theorem iffCNFRule(const Theorem& thm) = 0;
250  //! ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v]
251  virtual Theorem iteCNFRule(const Theorem& thm) = 0;
252  //! ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
253  virtual Theorem iteToClauses(const Theorem& ite) = 0;
254  //! e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
255  virtual Theorem iffToClauses(const Theorem& iff) = 0;
256 
257  virtual Theorem satProof(const Expr& queryExpr, const Proof& satProof) = 0;
258 
259  /*! @} */ // end of SE_Rules
260  }; // end of class SearchEngineRules
261 
262 } // end of namespace CVC3
263 
264 #endif
virtual Theorem cutRule(const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)=0
Cut rule: .
virtual Theorem confAndrAT(const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)=0
virtual Theorem andCNFRule(const Theorem &thm)=0
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual Theorem negIntro(const Expr &not_a, const Theorem &pfFalse)=0
Negation introduction: .
virtual Theorem impCNFRule(const Theorem &thm)=0
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
virtual Theorem confIterThenElse(const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)=0
virtual Theorem propAndrAT(const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)=0
virtual Theorem iteCNFRule(const Theorem &thm)=0
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].
virtual ~SearchEngineRules()
Destructor.
Definition: search_rules.h:41
virtual void propIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)=0
virtual Theorem conflictClause(const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)=0
Conflict clause rule: .
virtual Theorem satProof(const Expr &queryExpr, const Proof &satProof)=0
virtual Theorem unitProp(const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)=0
Unit propagation rule: .
virtual Theorem propIterIte(const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)=0
virtual Theorem conflictRule(const std::vector< Theorem > &thms, const Theorem &clause)=0
"Conflict" rule (all literals in a clause become FALSE)
virtual void propAndrLRT(const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)=0
virtual Theorem propAndrRF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)=0
virtual Theorem iffToClauses(const Theorem &iff)=0
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
virtual Theorem orCNFRule(const Theorem &thm)=0
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].
static int left(int i)
Definition: minisat_heap.h:53
virtual Theorem iffCNFRule(const Theorem &thm)=0
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
virtual Theorem confIffr(const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)=0
virtual Theorem iteToClauses(const Theorem &ite)=0
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
virtual Theorem confAndrAF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)=0
virtual Theorem proofByContradiction(const Expr &a, const Theorem &pfFalse)=0
Proof by contradiction: .
virtual Theorem propIffr(const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)=0
API to the proof rules for the Search Engines.
Definition: search_rules.h:35
virtual Theorem confIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)=0
virtual Theorem eliminateSkolemAxioms(const Theorem &tFalse, const std::vector< Theorem > &delta)=0
virtual Theorem propAndrLF(const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)=0
virtual Theorem propAndrAF(const Theorem &andr_th, bool left, const Theorem &b_th)=0
virtual Theorem caseSplit(const Expr &a, const Theorem &a_proves_c, const Theorem &not_a_proves_c)=0
Case split: .
virtual Theorem propIterThen(const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)=0