CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
theory_array.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file theory_array.h
4
*
5
* Author: Clark Barrett
6
*
7
* Created: Wed Feb 26 18:32:06 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
21
#ifndef _cvc3__include__theory_array_h_
22
#define _cvc3__include__theory_array_h_
23
24
#include "
theory_core.h
"
25
26
namespace
CVC3 {
27
28
class
ArrayProofRules;
29
30
typedef
enum
{
31
ARRAY
= 2000,
32
READ
,
33
WRITE
,
34
// Array literal [ [type] e ]; creates a constant array holding 'e'
35
// in all elements: (CONST_ARRAY type e)
36
ARRAY_LITERAL
37
}
ArrayKinds
;
38
39
/*****************************************************************************/
40
/*!
41
*\class TheoryArray
42
*\ingroup Theories
43
*\brief This theory handles arrays.
44
*
45
* Author: Clark Barrett
46
*
47
* Created: Thu Feb 27 00:38:20 2003
48
*/
49
/*****************************************************************************/
50
class
TheoryArray
:
public
Theory
{
51
ArrayProofRules
*
d_rules
;
52
53
//! Backtracking list of array reads, for building concrete models.
54
CDList<Expr>
d_reads
;
55
//! Set of renaming theorems \f$\exists x. t = x\f$ indexed by t
56
ExprMap<Theorem>
d_renameThms
;
57
//! Flag to include array reads to the concrete model
58
const
bool
&
d_applicationsInModel
;
59
//! Flag to lift ite's over reads
60
const
bool
&
d_liftReadIte
;
61
62
//! Backtracking database of subterms of shared terms
63
CDMap<Expr,Expr>
d_sharedSubterms
;
64
//! Backtracking database of subterms of shared terms
65
CDList<Expr>
d_sharedSubtermsList
;
66
//! Used in checkSat
67
CDO<unsigned>
d_index
;
68
69
CDO<size_t>
d_sharedIdx1
,
d_sharedIdx2
;
70
71
//! Flag for use in checkSat
72
int
d_inCheckSat
;
73
74
//! Derived rule
75
// w(...,i,v1,...,) => w(......,i,v1')
76
// Returns Null Theorem if index does not appear
77
Theorem
pullIndex
(
const
Expr
& e,
const
Expr
& index);
78
79
public
:
80
TheoryArray
(
TheoryCore
* core);
81
~TheoryArray
();
82
83
// Trusted method that creates the proof rules class (used in constructor).
84
// Implemented in array_theorem_producer.cpp
85
ArrayProofRules
*
createProofRules
();
86
87
// Theory interface
88
void
addSharedTerm
(
const
Expr
& e);
89
void
assertFact
(
const
Theorem
& e);
90
void
checkSat
(
bool
fullEffort);
91
Theorem
rewrite
(
const
Expr
& e);
92
void
setup
(
const
Expr
& e);
93
void
update
(
const
Theorem
& e,
const
Expr
& d);
94
Theorem
solve
(
const
Theorem
& e);
95
void
checkType
(
const
Expr
& e);
96
Cardinality
finiteTypeInfo
(
Expr
& e,
Unsigned
& n,
97
bool
enumerate,
bool
computeSize);
98
void
computeType
(
const
Expr
& e);
99
Type
computeBaseType
(
const
Type
& t);
100
void
computeModelTerm
(
const
Expr
& e, std::vector<Expr>& v);
101
void
computeModel
(
const
Expr
& e, std::vector<Expr>& vars);
102
Expr
computeTCC
(
const
Expr
& e);
103
virtual
Expr
parseExprOp
(
const
Expr
& e);
104
ExprStream
&
print
(
ExprStream
& os,
const
Expr
& e);
105
Expr
getBaseArray
(
const
Expr
& e)
const
;
106
};
107
108
// Array testers
109
inline
bool
isArray
(
const
Type
& t) {
return
t.
getExpr
().
getKind
() ==
ARRAY
; }
110
inline
bool
isRead
(
const
Expr
& e) {
return
e.
getKind
() ==
READ
; }
111
inline
bool
isWrite
(
const
Expr
& e) {
return
e.
getKind
() ==
WRITE
; }
112
inline
bool
isArrayLiteral
(
const
Expr
& e)
113
{
return
(e.
isClosure
() && e.
getKind
() ==
ARRAY_LITERAL
); }
114
115
// Array constructors
116
inline
Type
arrayType
(
const
Type
& type1,
const
Type
& type2)
117
{
return
Type
(
Expr
(
ARRAY
, type1.
getExpr
(), type2.
getExpr
())); }
118
119
// Expr read(const Expr& arr, const Expr& index);
120
// Expr write(const Expr& arr, const Expr& index, const Expr& value);
121
Expr
arrayLiteral
(
const
Expr& ind,
const
Expr& body);
122
}
// end of namespace CVC3
123
124
#endif
Generated on Tue May 14 2013 14:44:53 for CVC3 by
1.8.3.1