CVC3  2.4.1
core_theorem_producer.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file core_theorem_producer.h
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Feb 05 03:40:36 GMT 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 // CLASS: CoreTheoremProducer
21 //
22 // AUTHOR: Sergey Berezin, 12/09/2002
23 //
24 // Description: Implementation of the proof rules for ground
25 // equational logic (reflexivity, symmetry, transitivity, and
26 // substitutivity).
27 //
28 ///////////////////////////////////////////////////////////////////////////////
29 
30 #ifndef _cvc3__core_theorem_producer_h_
31 #define _cvc3__core_theorem_producer_h_
32 
33 #include "core_proof_rules.h"
34 #include "theorem_producer.h"
35 
36 namespace CVC3 {
37 
38  class TheoryCore;
39 
41  private:
42  //! pointer to theory core
44 
45  public:
47  : TheoremProducer(tm), d_core(core) { }
48  virtual ~CoreTheoremProducer() { }
49 
50  Theorem typePred(const Expr& e);
51  Theorem rewriteLetDecl(const Expr& e);
52  Theorem rewriteNotAnd(const Expr& e);
53  Theorem rewriteNotOr(const Expr& e);
54  Theorem rewriteNotIff(const Expr& e);
55  Theorem rewriteNotIte(const Expr& e);
56  Theorem rewriteIteThen(const Expr& e, const Theorem& thenThm);
57  Theorem rewriteIteElse(const Expr& e, const Theorem& elseThm);
58  Theorem rewriteIteBool(const Expr& c,
59  const Expr& e1, const Expr& e2);
62  Theorem rewriteImplies(const Expr& e);
63  Theorem rewriteDistinct(const Expr& e);
64  Theorem NotToIte(const Expr& not_e);
65  Theorem OrToIte(const Expr& e);
66  Theorem AndToIte(const Expr& e);
67  Theorem IffToIte(const Expr& e);
68  Theorem ImpToIte(const Expr& e);
69  Theorem rewriteIteToNot(const Expr& e);
70  Theorem rewriteIteToOr(const Expr& e);
71  Theorem rewriteIteToAnd(const Expr& e);
72  Theorem rewriteIteToIff(const Expr& e);
73  Theorem rewriteIteToImp(const Expr& e);
74  Theorem rewriteIteCond(const Expr& e);
75  Theorem ifLiftUnaryRule(const Expr& e);
76  Theorem iffOrDistrib(const Expr& iff);
77  Theorem iffAndDistrib(const Expr& iff);
78  Theorem rewriteAndSubterms(const Expr& e, int idx);
79  Theorem rewriteOrSubterms(const Expr& e, int idx);
80  Theorem dummyTheorem(const Expr& e);
81 
82  }; // end of class CoreTheoremProducer
83 
84 } // end of namespace CVC3
85 
86 #endif
Theorem IffToIte(const Expr &e)
==> IFF(a,b) == ITE(a, b, !b)
Data structure of expressions in CVC3.
Definition: expr.h:133
Theorem rewriteIteToOr(const Expr &e)
==> ITE(a, TRUE, b) IFF OR(a, b)
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
Theorem rewriteNotIte(const Expr &e)
==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)
Theorem iffOrDistrib(const Expr &iff)
((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff'
Theorem OrToIte(const Expr &e)
==> Or(e) == ITE(e[1], TRUE, e[0])
Theorem rewriteIteCond(const Expr &e)
==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
Theorem rewriteIteToAnd(const Expr &e)
==> ITE(a, b, FALSE) IFF AND(a, b)
Theorem rewriteIteElse(const Expr &e, const Theorem &elseThm)
!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)
Theorem ImpToIte(const Expr &e)
==> IMPLIES(a,b) == ITE(a, b, TRUE)
Theorem rewriteNotAnd(const Expr &e)
==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)
Theorem rewriteIteToImp(const Expr &e)
==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
Theorem rewriteIteToNot(const Expr &e)
==> ITE(e, FALSE, TRUE) IFF NOT(e)
Theorem rewriteDistinct(const Expr &e)
==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])
TheoryCore * d_core
pointer to theory core
Theorem rewriteAndSubterms(const Expr &e, int idx)
(a & b) <=> a & b[a/true]; takes the index of a
Theorem dummyTheorem(const Expr &e)
Temporary cheat for building theorems.
Theorem rewriteIteBool(const Expr &c, const Expr &e1, const Expr &e2)
==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2)
Theorem rewriteLetDecl(const Expr &e)
Replace LETDECL with its definition.
Theorem rewriteIteThen(const Expr &e, const Theorem &thenThm)
a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)
Theorem rewriteIteToIff(const Expr &e)
==> ITE(a, b, !b) IFF IFF(a, b)
CoreTheoremProducer(TheoremManager *tm, TheoryCore *core)
Theorem rewriteImplies(const Expr &e)
==> IMPLIES(e1,e2) IFF OR(!e1, e2)
Theorem rewriteOrSubterms(const Expr &e, int idx)
(a | b) <=> a | b[a/false]; takes the index of a
Theorem NotToIte(const Expr &not_e)
==> NOT(e) == ITE(e, FALSE, TRUE)
Theorem iffAndDistrib(const Expr &iff)
((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff'
Theorem andDistributivityRule(const Expr &e)
|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)
Theorem rewriteNotIff(const Expr &e)
==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2)
Theorem orDistributivityRule(const Expr &e)
|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)
Proof rules used by theory_core.
Theorem AndToIte(const Expr &e)
==> And(e) == ITE(e[1], e[0], FALSE)
Theorem rewriteNotOr(const Expr &e)
==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)
Theorem ifLiftUnaryRule(const Expr &e)
|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))
Theorem typePred(const Expr &e)
e: T ==> |- typePred_T(e) [deriving the type predicate of e]