CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_quant
quant_theorem_producer.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file quant_theorem_producer.h
4
*
5
* Author: Daniel Wichs
6
*
7
* Created: Jul 07 22:22:38 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
#ifndef _cvc3__quant_theorem_producer_h_
21
#define _cvc3__quant_theorem_producer_h_
22
23
#include "
quant_proof_rules.h
"
24
#include "
theorem_producer.h
"
25
#include "
theory_quant.h
"
26
27
namespace
CVC3 {
28
29
class
QuantTheoremProducer
:
public
QuantProofRules
,
public
TheoremProducer
{
30
TheoryQuant
*
d_theoryQuant
;
31
std::map<Expr,int>
d_typeFound
;
32
private
:
33
34
//! find all bound variables in e and maps them to true in boundVars
35
void
recFindBoundVars
(
const
Expr
& e,
36
ExprMap<bool>
& boundVars,
ExprMap<bool>
&visited);
37
public
:
38
//! Constructor
39
QuantTheoremProducer
(
TheoremManager
* tm,
TheoryQuant
* theoryQuant):
40
TheoremProducer
(tm),
d_theoryQuant
(theoryQuant) {
d_typeFound
.clear(); }
41
42
virtual
Theorem
addNewConst
(
const
Expr
& e) ;
43
virtual
Theorem
newRWThm
(
const
Expr
& e,
const
Expr
& newE) ;
44
virtual
Theorem
normalizeQuant
(
const
Expr
& e) ;
45
46
//! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
47
virtual
Theorem
rewriteNotExists
(
const
Expr
& e);
48
//! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
49
virtual
Theorem
rewriteNotForall
(
const
Expr
& e);
50
//! Instantiate a universally quantified formula
51
/*! From T|-FORALL(var): e generate T|-e' where e' is obtained
52
* from e by instantiating bound variables with terms in
53
* vector<Expr>& terms. The vector of terms should be the same
54
* size as the vector of bound variables in e. Also elements in
55
* each position i need to have matching types.
56
* \param t1 is the quantifier (a Theorem)
57
* \param terms are the terms to instantiate.
58
* \param quantLevel the quantification level for the theorem.
59
60
*/
61
62
virtual
Theorem
universalInst
(
const
Theorem
& t1,
63
const
std::vector<Expr>& terms,
int
quantLevel ,
64
Expr
gterm);
65
66
virtual
Theorem
universalInst
(
const
Theorem
& t1,
67
const
std::vector<Expr>& terms,
int
quantLevel);
68
69
virtual
Theorem
universalInst
(
const
Theorem
& t1,
70
const
std::vector<Expr>& terms);
71
72
73
virtual
Theorem
partialUniversalInst
(
const
Theorem
& t1,
74
const
std::vector<Expr>& terms,
75
int
quantLevel) ;
76
77
78
/*! @brief From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e
79
* where vars' is obtained from vars by removing all bound variables
80
* not used in e. If vars' is empty the produced theorem is just T|-e
81
*/
82
virtual
Theorem
boundVarElim
(
const
Theorem
& t1);
83
84
virtual
Theorem
adjustVarUniv
(
const
Theorem
& t1,
85
const
std::vector<Expr>& newBvs);
86
87
virtual
Theorem
packVar
(
const
Theorem
& t1);
88
89
virtual
Theorem
pullVarOut
(
const
Theorem
& t1);
90
91
92
};
93
94
}
95
96
#endif
Generated on Mon Aug 6 2012 09:40:06 for CVC3 by
1.8.1.1