CVC3
core_proof_rules.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file core_proof_rules.h
4  *\brief Proof rules used by theory_core
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Wed Jan 11 15:48:35 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__core_proof_rules_h_
23 #define _cvc3__core_proof_rules_h_
24 
25 #include <vector>
26 
27 namespace CVC3 {
28 
29  class Theorem;
30  class Theorem3;
31  class Expr;
32  class Op;
33 
35  public:
36  //! Destructor
37  virtual ~CoreProofRules() { }
38 
39  //! e: T ==> |- typePred_T(e) [deriving the type predicate of e]
40  virtual Theorem typePred(const Expr& e) = 0;
41 
42  ////////////////////////////////////////////////////////////////////////
43  // Core rewrite rules
44  ////////////////////////////////////////////////////////////////////////
45 
46  //! Replace LETDECL with its definition
47  /*! Used only in TheoryCore */
48  virtual Theorem rewriteLetDecl(const Expr& e) = 0;
49  //! ==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)
50  virtual Theorem rewriteNotAnd(const Expr& e) = 0;
51  //! ==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)
52  virtual Theorem rewriteNotOr(const Expr& e) = 0;
53  //! ==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2)
54  virtual Theorem rewriteNotIff(const Expr& e) = 0;
55  //! ==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)
56  virtual Theorem rewriteNotIte(const Expr& e) = 0;
57  //! a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)
58  virtual Theorem rewriteIteThen(const Expr& e, const Theorem& thenThm) = 0;
59  //! !a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)
60  virtual Theorem rewriteIteElse(const Expr& e, const Theorem& elseThm) = 0;
61  //! ==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2)
62  virtual Theorem rewriteIteBool(const Expr& c,
63  const Expr& e1, const Expr& e2) = 0;
64 
65  //! |= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)
66  virtual Theorem orDistributivityRule(const Expr& e) = 0;
67  //! |= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)
68  virtual Theorem andDistributivityRule(const Expr& e) = 0;
69 
70 
71  //! ==> IMPLIES(e1,e2) IFF OR(!e1, e2)
72  virtual Theorem rewriteImplies(const Expr& e) = 0;
73 
74  //! ==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])
75  virtual Theorem rewriteDistinct(const Expr& e) = 0;
76 
77  //! ==> NOT(e) == ITE(e, FALSE, TRUE)
78  virtual Theorem NotToIte(const Expr& not_e) = 0;
79  //! ==> Or(e) == ITE(e[1], TRUE, e[0])
80  virtual Theorem OrToIte(const Expr& e) = 0;
81  //! ==> And(e) == ITE(e[1], e[0], FALSE)
82  virtual Theorem AndToIte(const Expr& e) = 0;
83  //! ==> IFF(a,b) == ITE(a, b, !b)
84  virtual Theorem IffToIte(const Expr& e) = 0;
85  //! ==> IMPLIES(a,b) == ITE(a, b, TRUE)
86  virtual Theorem ImpToIte(const Expr& e) = 0;
87 
88  //! ==> ITE(e, FALSE, TRUE) IFF NOT(e)
89  virtual Theorem rewriteIteToNot(const Expr& e) = 0;
90  //! ==> ITE(a, TRUE, b) IFF OR(a, b)
91  virtual Theorem rewriteIteToOr(const Expr& e) = 0;
92  //! ==> ITE(a, b, FALSE) IFF AND(a, b)
93  virtual Theorem rewriteIteToAnd(const Expr& e) = 0;
94  //! ==> ITE(a, b, !b) IFF IFF(a, b)
95  virtual Theorem rewriteIteToIff(const Expr& e) = 0;
96  //! ==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
97  virtual Theorem rewriteIteToImp(const Expr& e) = 0;
98  //! ==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
99  virtual Theorem rewriteIteCond(const Expr& e) = 0;
100 
101  //! |- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))
102  virtual Theorem ifLiftUnaryRule(const Expr& e) = 0;
103  //! ((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff'
104  virtual Theorem iffOrDistrib(const Expr& iff) = 0;
105  //! ((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff'
106  virtual Theorem iffAndDistrib(const Expr& iff) = 0;
107 
108  // Advanced Boolean transformations
109 
110  //! (a & b) <=> a & b[a/true]; takes the index of a
111  /*! and rewrites all the other conjuncts. */
112  virtual Theorem rewriteAndSubterms(const Expr& e, int idx) = 0;
113  //! (a | b) <=> a | b[a/false]; takes the index of a
114  /*! and rewrites all the other disjuncts. */
115  virtual Theorem rewriteOrSubterms(const Expr& e, int idx) = 0;
116 
117  //! Temporary cheat for building theorems
118  virtual Theorem dummyTheorem(const Expr& e) = 0;
119 
120  }; // end of class CoreProofRules
121 
122 } // end of namespace CVC3
123 
124 #endif