20 #ifndef _cvc3__include__theory_records_h_
21 #define _cvc3__include__theory_records_h_
27 class RecordsProofRules;
75 bool enumerate,
bool computeSize);
108 const std::vector<Expr>& kids);
111 const std::vector<Expr>& kids);
114 const std::vector<Type>& types);
117 const std::vector<Expr>& types);
120 const std::vector<Expr>& types);
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
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.
void checkType(const Expr &e)
check record or tuple type
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
RecordsProofRules * d_rules
const Expr & getExpr() const
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)
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
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.
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.
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.