CVC3
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_quant
quant_proof_rules.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file quant_proof_rules.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_proof_rules_h_
21
#define _cvc3__quant_proof_rules_h_
22
23
#include <vector>
24
25
namespace
CVC3 {
26
27
class
Expr;
28
class
Theorem;
29
30
class
QuantProofRules
{
31
public
:
32
//! Destructor
33
virtual
~QuantProofRules
() { }
34
35
virtual
Theorem
addNewConst
(
const
Expr
& e) =0;
36
37
virtual
Theorem
newRWThm
(
const
Expr
& e,
const
Expr
& newE) = 0 ;
38
39
virtual
Theorem
normalizeQuant
(
const
Expr
& e) =0;
40
41
//! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
42
virtual
Theorem
rewriteNotExists
(
const
Expr
& e) = 0;
43
44
//! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
45
virtual
Theorem
rewriteNotForall
(
const
Expr
& e) = 0;
46
47
//! Instantiate a universally quantified formula
48
/*! From T|-FORALL(var): e generate T|-e' where e' is obtained
49
* from e by instantiating bound variables with terms in
50
* vector<Expr>& terms. The vector of terms should be the same
51
* size as the vector of bound variables in e. Also elements in
52
* each position i need to have matching types.
53
* \param t1 is the quantifier (a Theorem)
54
* \param terms are the terms to instantiate.
55
* \param quantLevel is the quantification level for the theorem.
56
*/
57
virtual
Theorem
universalInst
(
const
Theorem
& t1,
const
std::vector<Expr>& terms,
int
quantLevel,
Expr
gterm ) = 0 ;
58
59
virtual
Theorem
universalInst
(
const
Theorem
& t1,
60
const
std::vector<Expr>& terms,
int
quantLevel) = 0;
61
62
virtual
Theorem
universalInst
(
const
Theorem
& t1,
63
const
std::vector<Expr>& terms) = 0;
64
65
66
virtual
Theorem
partialUniversalInst
(
const
Theorem
& t1,
67
const
std::vector<Expr>& terms,
68
int
quantLevel) = 0;
69
70
/*! @brief From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e
71
* where vars' is obtained from vars by removing all bound variables
72
* not used in e. If vars' is empty the produced theorem is just T|-e
73
*/
74
virtual
Theorem
boundVarElim
(
const
Theorem
& t1) = 0;
75
76
virtual
Theorem
packVar
(
const
Theorem
& t1) = 0;
77
78
virtual
Theorem
pullVarOut
(
const
Theorem
& t1) = 0;
79
80
virtual
Theorem
adjustVarUniv
(
const
Theorem
& t1,
81
const
std::vector<Expr>& newBvs) = 0;
82
83
};
84
}
85
#endif
Generated on Thu May 16 2013 13:25:14 for CVC3 by
1.8.2