CVC3  2.4.1
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 
30  public TheoremProducer {
32 
33  public:
34  // Constructor
36  TheoremProducer(tm), d_theoryRecords(t) { }
37  Theorem rewriteLitSelect(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
Data structure of expressions in CVC3.
Definition: expr.h:133
const std::string & getField(const Expr &e, int i)
Get the i-th field name from the record literal or type.
Type recordType(const std::vector< std::string > &fields, const std::vector< Type > &types)
Create a record type.
Type tupleType(const std::vector< Expr > &types)
Create a tuple type (types of components are given as Exprs)
Expr tupleSelect(const Expr &tup, int i)
Create a tuple index selector expression.
Theorem expandRecord(const Expr &e)
Expand a record into a literal: |- e = (# f1:=e.f1, ..., fn:=e.fn #)
int getFieldIndex(const Expr &e, const std::string &field)
Get the field index in the record literal or type.
Expr tupleUpdate(const Expr &tup, int i, const Expr &val)
Create a tuple index update expression.
const std::string & getField(const Expr &e)
Get the field name from the record select and update expressions.
Expr tupleSelect(const Expr &tup, int i)
Create a tuple index selector expression.
Expr recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &kids)
Create a record literal.
bool isRecordAccess(const Expr &e)
Test whether expr is a record select/update subclass.
bool isRecordType(const Expr &e)
Test whether expr is a record type.
MS C++ specific settings.
Definition: type.h:42
bool isRecordType(const Expr &e)
Test whether expr is a record type.
Theorem rewriteUpdateSelect(const Expr &e)
==> (RECORD_SELECT (RECORD_UPDATE r fi vi) fj) = vi
Type recordType(const std::vector< std::string > &fields, const std::vector< Expr > &types)
Create a record type (field types are given as a vector of Expr)
Theorem expandNeq(const Theorem &neqThrm)
From T|- NOT e=e' return T|- NOT AND (e.i = e'.i) for all i.
Type tupleType(const std::vector< Type > &types)
Create a tuple type.
Expr recordSelect(const Expr &r, const std::string &field)
Create a record field select expression.
Expr recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &kids)
Create a record literal.
Expr recordExpr(const std::vector< Expr > &fields, const std::vector< Expr > &kids)
Create a record literal.
int getIndex(const Expr &e)
Get the index from the tuple select and update expressions.
Theorem rewriteLitSelect(const Expr &e)
==> (SELECT (LITERAL v1 ... vi ...) fi) = vi
RecordsTheoremProducer(TheoremManager *tm, TheoryRecords *t)
Theorem expandTuple(const Expr &e)
Expand a tuple into a literal: |- e = (e.0, ..., e.n-1)
This theory handles records.
Theorem rewriteLitUpdate(const Expr &e)
==> (RECORD_UPDATE (RECORD (f1 v1) ... (fi vi) ...) fi v') =(RECORD (f1 v1) ... (fi v') ...
Type tupleType(const std::vector< Type > &types)
Create a tuple type.
Theorem expandEq(const Theorem &eqThrm)
From T|- e = e' return T|- AND (e.i = e'.i) for all i.
const std::vector< Expr > & getFields(const Expr &r)
Get the list of fields from a record literal.
Expr recordUpdate(const Expr &r, const std::string &field, const Expr &val)
Create a record field update expression.
bool isTupleAccess(const Expr &e)
Test whether expr is a tuple select/update subclass.
Type recordType(const std::vector< std::string > &fields, const std::vector< Type > &types)
Create a record type.
bool isRecordType(const Type &t)
Test whether Type is a record type.
int getFieldIndex(const Expr &e, const std::string &field)
Get the field index in the record literal or type.
Expr recordUpdate(const Expr &r, const std::string &field, const Expr &val)
Create a record field update expression.
Expr tupleUpdate(const Expr &tup, int i, const Expr &val)
Create a tuple index update expression.
Definition: expr.cpp:35
const std::vector< Expr > & getFields(const Expr &r)
Get the list of fields from a record literal.
bool isRecordAccess(const Expr &e)
Test whether expr is a record select/update subclass.
int getIndex(const Expr &e)
Get the index from the tuple select and update expressions.
const std::string & getField(const Expr &e, int i)
Get the i-th field name from the record literal or type.
Expr tupleExpr(const std::vector< Expr > &kids)
Create a tuple literal.
Expr recordSelect(const Expr &r, const std::string &field)
Create a record field select expression.
bool isTupleAccess(const Expr &e)
Test whether expr is a tuple select/update subclass.
Expr tupleExpr(const std::vector< Expr > &kids)
Create a tuple literal.