CVC3  2.4.1
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
Data structure of expressions in CVC3.
Definition: expr.h:133
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
Type recordType(const std::vector< std::string > &fields, const std::vector< Type > &types)
Create a record type.
bool isTuple(const Expr &e)
Test if expr is a tuple literal.
Expr tupleSelect(const Expr &tup, int i)
Create a tuple index selector expression.
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.
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
MS C++ specific settings.
Definition: type.h:42
void checkType(const Expr &e)
check record or tuple type
Base class for theories.
Definition: theory.h:64
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
RecordsProofRules * d_rules
const Expr & getExpr() const
Definition: type.h:52
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Expr recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &kids)
Create a record literal.
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
void computeType(const Expr &e)
computes the type of a record or a tuple
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Definition: expr.h:1196
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
Theorem rewrite(const Expr &e)
rewrites an expression e to one of several allowed forms
void assertFact(const Theorem &e)
assert a fact to the theory of records
This theory handles records.
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
bool isApply() const
Definition: expr.h:1014
Type tupleType(const std::vector< Type > &types)
Create a tuple type.
bool isRecord(const Expr &e)
Test whether expr is a record literal.
RecordsProofRules * createProofRules()
creates a reference to the proof rules
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Theorem rewriteAux(const Expr &e)
Auxiliary rewrites: Processing of AND and OR of equations. Returns e=e'.
Generic API for Theories plus methods commonly used by theories.
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.
ExprStream & print(ExprStream &os, const Expr &e)
pretty printing
bool isRecordType(const Type &t)
Test whether expr is a record type.
int getFieldIndex(const Expr &e, const std::string &field)
Get the field index in the record literal or type.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
bool isTupleType(const Expr &e)
Test if expr represents a tuple type.
Expr tupleUpdate(const Expr &tup, int i, const Expr &val)
Create a tuple index update expression.
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
void checkSat(bool fullEffort)
empty implementation to fit theory interface
const std::vector< Expr > & getFields(const Expr &r)
Get the list of fields from a record literal.
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 recordSelect(const Expr &r, const std::string &field)
Create a record field select expression.
bool isTupleType(const Type &tp)
Test if 'tp' is a tuple type.
TheoryRecords(TheoryCore *core)
Constructor.
Expr tupleExpr(const std::vector< Expr > &kids)
Create a tuple literal.