20 #ifndef _cvc3__records_theorem_producer_h_
21 #define _cvc3__records_theorem_producer_h_
57 const std::vector<Expr>& kids)
61 const std::vector<Expr>& kids)
65 const std::vector<Type>& types)
69 const std::vector<Expr>& types)
Data structure of expressions in CVC3.
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.
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.
TheoryRecords * d_theoryRecords
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.
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.