CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_records
records_theorem_producer.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file records_theorem_producer.h
4
*
5
* Author: Daniel Wichs
6
*
7
* Created: Jul 22 22:59:07 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__records_theorem_producer_h_
21
#define _cvc3__records_theorem_producer_h_
22
23
#include "
records_proof_rules.h
"
24
#include "
theorem_producer.h
"
25
#include "
theory_records.h
"
26
27
namespace
CVC3 {
28
29
class
RecordsTheoremProducer
:
public
RecordsProofRules
,
30
public
TheoremProducer
{
31
TheoryRecords
*
d_theoryRecords
;
32
33
public
:
34
// Constructor
35
RecordsTheoremProducer
(
TheoremManager
* tm,
TheoryRecords
* t):
36
TheoremProducer
(tm),
d_theoryRecords
(t) { }
37
Theorem
rewriteLitSelect
(
const
Expr
&e);
38
Theorem
rewriteUpdateSelect
(
const
Expr
& e);
39
Theorem
rewriteLitUpdate
(
const
Expr
& e);
40
Theorem
expandEq
(
const
Theorem
& eqThrm);
41
Theorem
expandNeq
(
const
Theorem
& neqThrm);
42
Theorem
expandRecord
(
const
Expr
& e);
43
Theorem
expandTuple
(
const
Expr
& e);
44
45
// Expr creation functions
46
//! Test whether expr is a record type
47
bool
isRecordType
(
const
Expr
& e)
48
{
return
d_theoryRecords
->
isRecordType
(e); }
49
//! Test whether Type is a record type
50
bool
isRecordType
(
const
Type
& t)
51
{
return
d_theoryRecords
->
isRecordType
(t); }
52
//! Test whether expr is a record select/update subclass
53
bool
isRecordAccess
(
const
Expr
& e)
54
{
return
d_theoryRecords
->
isRecordAccess
(e); }
55
//! Create a record literal
56
Expr
recordExpr
(
const
std::vector<std::string>& fields,
57
const
std::vector<Expr>& kids)
58
{
return
d_theoryRecords
->
recordExpr
(fields, kids); }
59
//! Create a record literal
60
Expr
recordExpr
(
const
std::vector<Expr>& fields,
61
const
std::vector<Expr>& kids)
62
{
return
d_theoryRecords
->
recordExpr
(fields, kids); }
63
//! Create a record type
64
Type
recordType
(
const
std::vector<std::string>& fields,
65
const
std::vector<Type>& types)
66
{
return
d_theoryRecords
->
recordType
(fields, types); }
67
//! Create a record type (field types are given as a vector of Expr)
68
Type
recordType
(
const
std::vector<std::string>& fields,
69
const
std::vector<Expr>& types)
70
{
return
d_theoryRecords
->
recordType
(fields, types); }
71
//! Create a record field select expression
72
Expr
recordSelect
(
const
Expr
& r,
const
std::string& field)
73
{
return
d_theoryRecords
->
recordSelect
(r, field); }
74
//! Create a record field update expression
75
Expr
recordUpdate
(
const
Expr
& r,
const
std::string& field,
76
const
Expr
& val)
77
{
return
d_theoryRecords
->
recordUpdate
(r, field, val); }
78
//! Get the list of fields from a record literal
79
const
std::vector<Expr>&
getFields
(
const
Expr
& r)
80
{
return
d_theoryRecords
->
getFields
(r); }
81
//! Get the i-th field name from the record literal or type
82
const
std::string&
getField
(
const
Expr
& e,
int
i)
83
{
return
d_theoryRecords
->
getField
(e, i); }
84
//! Get the field index in the record literal or type
85
/*! The field must be present in the record; otherwise it's an error. */
86
int
getFieldIndex
(
const
Expr
& e,
const
std::string& field)
87
{
return
d_theoryRecords
->
getFieldIndex
(e, field); }
88
//! Get the field name from the record select and update expressions
89
const
std::string&
getField
(
const
Expr
& e)
90
{
return
d_theoryRecords
->
getField
(e); }
91
//! Create a tuple literal
92
Expr
tupleExpr
(
const
std::vector<Expr>& kids)
93
{
return
d_theoryRecords
->
tupleExpr
(kids); }
94
//! Create a tuple type
95
Type
tupleType
(
const
std::vector<Type>& types)
96
{
return
d_theoryRecords
->
tupleType
(types); }
97
//! Create a tuple type (types of components are given as Exprs)
98
Type
tupleType
(
const
std::vector<Expr>& types)
99
{
return
d_theoryRecords
->
tupleType
(types); }
100
//! Create a tuple index selector expression
101
Expr
tupleSelect
(
const
Expr
& tup,
int
i)
102
{
return
d_theoryRecords
->
tupleSelect
(tup, i); }
103
//! Create a tuple index update expression
104
Expr
tupleUpdate
(
const
Expr
& tup,
int
i,
const
Expr
& val)
105
{
return
d_theoryRecords
->
tupleUpdate
(tup, i, val); }
106
//! Get the index from the tuple select and update expressions
107
int
getIndex
(
const
Expr
& e)
108
{
return
d_theoryRecords
->
getIndex
(e); }
109
//! Test whether expr is a tuple select/update subclass
110
bool
isTupleAccess
(
const
Expr
& e)
111
{
return
d_theoryRecords
->
isTupleAccess
(e); }
112
};
113
114
}
115
116
#endif
Generated on Tue May 14 2013 09:02:07 for CVC3 by
1.8.3.1