CVC3
theory_records.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_records.h
4  *
5  * Author: Daniel Wichs
6  *
7  * Created: 7/22/03
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__include__theory_records_h_
21 #define _cvc3__include__theory_records_h_
22 
23 #include "theory.h"
24 
25 namespace CVC3 {
26 
27  class RecordsProofRules;
28 
29  typedef enum {
30  RECORD = 2500,
38  } RecordKinds;
39 
40 /*****************************************************************************/
41 /*!
42  *\class TheoryRecords
43  *\ingroup Theories
44  *\brief This theory handles records.
45  *
46  * Author: Daniel Wichs
47  *
48  * Created: 7/22/03
49  */
50 /*****************************************************************************/
51 class TheoryRecords :public Theory {
53  //! Auxiliary rewrites: Processing of AND and OR of equations. Returns e=e'.
54  Theorem rewriteAux(const Expr& e);
55  //! Takes Thm(e), returns Thm(e'), where e rewrites to e' by rewriteAux.
56  Theorem rewriteAux(const Theorem& thm);
57 
58 public:
59  TheoryRecords(TheoryCore* core); //!< Constructor
60  ~TheoryRecords(); //!< Destructor
61  //! creates a reference to the proof rules
63 
64  // Theory interface
65 
66  //! assert a fact to the theory of records
67  void assertFact(const Theorem& e);
68  //! empty implementation to fit theory interface
69  void checkSat(bool fullEffort) {}
70  //! rewrites an expression e to one of several allowed forms
71  Theorem rewrite(const Expr& e);
72  //! check record or tuple type
73  void checkType(const Expr& e);
75  bool enumerate, bool computeSize);
76  //! computes the type of a record or a tuple
77  void computeType(const Expr& e);
78  Type computeBaseType(const Type& t);
79 
80  Expr computeTypePred(const Type& t, const Expr& e);
81  void computeModelTerm(const Expr& e, std::vector<Expr>& v);
82  void computeModel(const Expr& e, std::vector<Expr>& vars);
83 
84  Expr computeTCC(const Expr& e);
85  virtual Expr parseExprOp(const Expr& e);
86  void setup(const Expr& e);
87  void update(const Theorem& e, const Expr& d);
88  //! pretty printing
89  ExprStream& print(ExprStream& os, const Expr& e);
90  //! Test whether expr is a record literal
91  bool isRecord(const Expr& e) {
92  return e.isApply() && e.getOpKind() == RECORD;
93  }
94  //! Test whether expr is a record type
95  bool isRecordType(const Expr& e) {
96  return e.isApply() && e.getOpKind() == RECORD_TYPE;
97  }
98  //! Test whether expr is a record type
99  bool isRecordType(const Type& t) {
100  return isRecordType(t.getExpr());
101  }
102  //! Test whether expr is a record select/update subclass
103  bool isRecordAccess(const Expr& e)
104  { return e.isApply() &&
105  (e.getOpKind() == RECORD_SELECT || e.getOpKind() == RECORD_UPDATE); }
106  //! Create a record literal
107  Expr recordExpr(const std::vector<std::string>& fields,
108  const std::vector<Expr>& kids);
109  //! Create a record literal
110  Expr recordExpr(const std::vector<Expr>& fields,
111  const std::vector<Expr>& kids);
112  //! Create a record type
113  Type recordType(const std::vector<std::string>& fields,
114  const std::vector<Type>& types);
115  //! Create a record type (field types are given as a vector of Expr)
116  Type recordType(const std::vector<std::string>& fields,
117  const std::vector<Expr>& types);
118  //! Create a record type (fields and types are given as a vector of Expr)
119  Type recordType(const std::vector<Expr>& fields,
120  const std::vector<Expr>& types);
121  //! Create a record field select expression
122  Expr recordSelect(const Expr& r, const std::string& field);
123  //! Create a record field update expression
124  Expr recordUpdate(const Expr& r, const std::string& field, const Expr& val);
125  //! Get the list of fields from a record literal
126  const std::vector<Expr>& getFields(const Expr& r);
127  //! Get the i-th field name from the record literal or type
128  const std::string& getField(const Expr& e, int i);
129  //! Get the field index in the record literal or type
130  /*! The field must be present in the record; otherwise it's an error. */
131  int getFieldIndex(const Expr& e, const std::string& field);
132  //! Get the field name from the record select and update expressions
133  const std::string& getField(const Expr& e);
134  //! Create a tuple literal
135  Expr tupleExpr(const std::vector<Expr>& kids);
136  //! Create a tuple type
137  Type tupleType(const std::vector<Type>& types);
138  //! Create a tuple type (types of components are given as Exprs)
139  Type tupleType(const std::vector<Expr>& types);
140  //! Create a tuple index selector expression
141  Expr tupleSelect(const Expr& tup, int i);
142  //! Create a tuple index update expression
143  Expr tupleUpdate(const Expr& tup, int i, const Expr& val);
144  //! Get the index from the tuple select and update expressions
145  int getIndex(const Expr& e);
146  //! Test whether expr is a tuple select/update subclass
147  bool isTupleAccess(const Expr& e)
148  { return e.isApply() &&
149  (e.getOpKind() == TUPLE_SELECT || e.getOpKind() == TUPLE_UPDATE); }
150  //! Test if expr is a tuple literal
151  bool isTuple(const Expr& e) { return e.isApply() && e.getOpKind() == TUPLE; }
152  //! Test if expr represents a tuple type
153  bool isTupleType(const Expr& e)
154  { return e.isApply() && e.getOpKind() == TUPLE_TYPE; }
155  //! Test if 'tp' is a tuple type
156  bool isTupleType(const Type& tp) { return isTupleType(tp.getExpr()); }
157 }; // end of class TheoryRecords
158 
159 }
160 
161 #endif