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
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