CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_core
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
40
class
CoreTheoremProducer
:
public
CoreProofRules
,
public
TheoremProducer
{
41
private
:
42
//! pointer to theory core
43
TheoryCore
*
d_core
;
44
45
public
:
46
CoreTheoremProducer
(
TheoremManager
* tm,
TheoryCore
* core)
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);
60
Theorem
orDistributivityRule
(
const
Expr
& e);
61
Theorem
andDistributivityRule
(
const
Expr
& e);
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
Generated on Tue May 14 2013 09:02:05 for CVC3 by
1.8.3.1