CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_core
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
34
class
CoreProofRules
{
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
Generated on Tue May 14 2013 15:43:25 for CVC3 by
1.8.3.1