CVCL::TheoryRecords Class Reference
[Theories]

This theory handles records. More...

#include <theory_records.h>

Inheritance diagram for CVCL::TheoryRecords:

[legend]Collaboration diagram for CVCL::TheoryRecords:

[legend]List of all members.

Public Member Functions

• TheoryRecords (TheoryCore *core)

  Constructor.
  

• ~TheoryRecords ()
• RecordsProofRules * createProofRules ()

  creates a reference to the proof rules
  

• void assertFact (const Theorem &e)

  assert a fact to the theory of records
  

• void checkSat (bool fullEffort)

  empty implementation to fit theory interface
  

• Theorem rewrite (const Expr &e)

  rewrites an expression e to one of several allowed forms
  

• void checkType (const Expr &e)

  check record or tuple type
  

• void computeType (const Expr &e)

  computes the type of a record or a tuple
  

• Type computeBaseType (const Type &t)

  Compute the base type of the top-level operator of an arbitrary type.
  

• Expr computeTypePred (const Type &t, const Expr &e)

  Theory specific computation of the subtyping predicate for type t applied to the expression e.
  

• void computeModelTerm (const Expr &e, std::vector< Expr > &v)

  Add variables from 'e' to 'v' for constructing a concrete model.
  

• void computeModel (const Expr &e, std::vector< Expr > &v)

  Compute the value of a compound variable from the more primitive ones.
  

• Expr computeTCC (const Expr &e)

  Compute and cache the TCC of e.
  

• virtual Expr parseExprOp (const Expr &e)

  Theory-specific parsing implemented by the DP.
  

• void setup (const Expr &e)

  Set up the term e for call-backs when e or its children change.
  

• void update (const Theorem &e, const Expr &d)

  Notify a theory of a new equality.
  

• ExprStream & print (ExprStream &os, const Expr &e)

  pretty printing
  

• bool isRecord (const Expr &e)

  Test whether expr is a record literal.
  

• bool isRecordType (const Expr &e)

  Test whether expr is a record type.
  

• bool isRecordType (const Type &t)

  Test whether expr is a record type.
  

• bool isRecordAccess (const Expr &e)

  Test whether expr is a record select/update subclass.
  

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

• Type recordType (const std::vector< std::string > &fields, const std::vector< Type > &types)

  Create a record type.
  

• 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).
  

• Type recordType (const std::vector< Expr > &fields, const std::vector< Expr > &types)

  Create a record type (fields and types are given as a vector of Expr).
  

• Expr recordSelect (const Expr &r, const std::string &field)

  Create a record field select expression.
  

• Expr recordUpdate (const Expr &r, const std::string &field, const Expr &val)

  Create a record field update expression.
  

• const std::vector< Expr > & getFields (const Expr &r)

  Get the list of fields from a record literal.
  

• const std::string & getField (const Expr &e, int i)

  Get the i-th field name from the record literal or type.
  

• int getFieldIndex (const Expr &e, const std::string &field)

  Get the field index in the record literal or type.
  

• const std::string & getField (const Expr &e)

  Get the field name from the record select and update expressions.
  

• Expr tupleExpr (const std::vector< Expr > &kids)

  Create a tuple literal.
  

• Type tupleType (const std::vector< Type > &types)

  Create a tuple 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.
  

• Expr tupleUpdate (const Expr &tup, int i, const Expr &val)

  Create a tuple index update expression.
  

• int getIndex (const Expr &e)

  Get the index from the tuple select and update expressions.
  

• bool isTupleAccess (const Expr &e)

  Test whether expr is a tuple select/update subclass.
  

• bool isTuple (const Expr &e)

  Test if expr is a tuple literal.
  

• bool isTupleType (const Expr &e)

  Test if expr represents a tuple type.
  

• bool isTupleType (const Type &tp)

  Test if 'tp' is a tuple type.
  

Private Member Functions

• Theorem rewriteAux (const Expr &e)

  Auxiliary rewrites: Processing of AND and OR of equations. Returns e=e'.
  

• Theorem rewriteAux (const Theorem &thm)

  Takes Thm(e), returns Thm(e'), where e rewrites to e' by rewriteAux.
  

Private Attributes

• RecordsProofRules * d_rules

---

Detailed Description

This theory handles records.

Author: Daniel Wichs

Created: 7/22/03

Definition at line 59 of file theory_records.h.

---

Constructor & Destructor Documentation

TheoryRecords::TheoryRecords (  TheoryCore *  core  )

Constructor. Definition at line 103 of file theory_records.cpp. References createProofRules(), d_rules, CVCL::Theory::getEM(), CVCL::ExprManager::newKind(), CVCL::RECORD, CVCL::RECORD_SELECT, CVCL::RECORD_TYPE, CVCL::RECORD_UPDATE, CVCL::Theory::registerTheory(), CVCL::TUPLE, CVCL::TUPLE_SELECT, CVCL::TUPLE_TYPE, and CVCL::TUPLE_UPDATE.

TheoryRecords::~TheoryRecords (   )

Destructor Definition at line 132 of file theory_records.cpp. References d_rules.

---

Member Function Documentation

Theorem TheoryRecords::rewriteAux (  const Expr &  e  )  [private]

Auxiliary rewrites: Processing of AND and OR of equations. Returns e=e'. When a record/tuple (dis)equality is expanded into the (dis)equalities of fields, we have to perform rewrites on the resulting record terms before the simplifier kicks in. Otherwise, if we have r1.f = r2.f, but r1=r2 was asserted before, for some complex record expressions r1 and r2, then the simplifier will substitute r2 for r1, and we get r2.f=r2.f at the end, which is not a useful fact to have. However, r1.f and/or r2.f may rewrite to something interesting, and the equality may yield new important facts. Definition at line 52 of file theory_records.cpp. References CVCL::AND, CVCL::Expr::arity(), CVCL::EQ, CVCL::Expr::getFind(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::Expr::hasFind(), CVCL::IFF, CVCL::NOT, CVCL::OR, CVCL::Theory::reflexivityRule(), rewrite(), CVCL::Theory::substitutivityRule(), and CVCL::Theory::transitivityRule(). Referenced by assertFact(), and rewriteAux().

Theorem TheoryRecords::rewriteAux (  const Theorem &  thm  )  [private]

Takes Thm(e), returns Thm(e'), where e rewrites to e' by rewriteAux. Definition at line 98 of file theory_records.cpp. References CVCL::Theorem::getExpr(), CVCL::Theory::iffMP(), and rewriteAux().

RecordsProofRules * TheoryRecords::createProofRules (   )

creates a reference to the proof rules Definition at line 40 of file records_theorem_producer.cpp. References CVCL::Theory::theoryCore(). Referenced by TheoryRecords().

void TheoryRecords::assertFact (  const Theorem &  e  )  [virtual]

assert a fact to the theory of records Implements CVCL::Theory. Definition at line 136 of file theory_records.cpp. References d_rules, CVCL::Theory::enqueueFact(), CVCL::EQ, CVCL::RecordsProofRules::expandEq(), CVCL::Theory::getBaseType(), CVCL::Type::getExpr(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Expr::getOpKind(), CVCL::IFF, CVCL::NOT, CVCL::RECORD_TYPE, rewriteAux(), CVCL::Expr::toString(), CVCL::Theorem::toString(), CVCL::TRACE, and CVCL::TUPLE_TYPE.

void CVCL::TheoryRecords::checkSat (  bool  fullEffort  )  [inline, virtual]

empty implementation to fit theory interface Implements CVCL::Theory. Definition at line 77 of file theory_records.h.

Theorem TheoryRecords::rewrite (  const Expr &  e  )  [virtual]

rewrites an expression e to one of several allowed forms Reimplemented from CVCL::Theory. Definition at line 168 of file theory_records.cpp. References CVCL::Expr::arity(), d_rules, CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::RECORD, CVCL::RECORD_SELECT, CVCL::RECORD_UPDATE, CVCL::Theory::reflexivityRule(), CVCL::Theory::rewriteCC(), CVCL::RecordsProofRules::rewriteLitSelect(), CVCL::RecordsProofRules::rewriteLitUpdate(), CVCL::RecordsProofRules::rewriteUpdateSelect(), CVCL::Expr::toString(), CVCL::TRACE, CVCL::Theory::transitivityRule(), CVCL::TUPLE, CVCL::TUPLE_SELECT, and CVCL::TUPLE_UPDATE. Referenced by computeModelTerm(), rewriteAux(), setup(), and update().

void TheoryRecords::checkType (  const Expr &  e  )  [virtual]

check record or tuple type Reimplemented from CVCL::Theory. Definition at line 351 of file theory_records.cpp. References CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Theory::getEM(), CVCL::Expr::getOpKind(), CVCL::Type::isFunction(), CVCL::RECORD_TYPE, and CVCL::TUPLE_TYPE.

void TheoryRecords::computeType (  const Expr &  e  )  [virtual]

computes the type of a record or a tuple Reimplemented from CVCL::Theory. Definition at line 381 of file theory_records.cpp. References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Theory::getBaseType(), CVCL::Theory::getEM(), CVCL::Type::getExpr(), getField(), getFieldIndex(), getFields(), getIndex(), CVCL::Expr::getOpKind(), CVCL::Expr::getType(), CVCL::RECORD, CVCL::RECORD_SELECT, CVCL::RECORD_TYPE, CVCL::RECORD_UPDATE, recordType(), CVCL::Expr::setType(), CVCL::Expr::toString(), CVCL::TUPLE, CVCL::TUPLE_SELECT, CVCL::TUPLE_TYPE, and CVCL::TUPLE_UPDATE.

Type TheoryRecords::computeBaseType (  const Type &  t  )  [virtual]

Compute the base type of the top-level operator of an arbitrary type. Reimplemented from CVCL::Theory. Definition at line 477 of file theory_records.cpp. References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Theory::getBaseType(), CVCL::Type::getExpr(), CVCL::Expr::getOp(), CVCL::Expr::getOpKind(), CVCL::RECORD_TYPE, CVCL::Type::toString(), and CVCL::TUPLE_TYPE.

Expr TheoryRecords::computeTypePred (  const Type &  t, const Expr &  e )  [virtual]

Theory specific computation of the subtyping predicate for type t applied to the expression e. By default returns true. Each theory needs to compute subtype predicates for the types associated with it. So, for example, the theory of records will take a record type [# f1: T1, f2: T2 #] and an expression e and will return the subtyping predicate for e, namely: computeTypePred(T1, e.f1) AND computeTypePred(T2, e.f2) Reimplemented from CVCL::Theory. Definition at line 319 of file theory_records.cpp. References CVCL::andExpr(), CVCL::Expr::arity(), CVCL::Type::getExpr(), getFields(), CVCL::Expr::getOpKind(), CVCL::Theory::getTypePred(), CVCL::RECORD_TYPE, recordSelect(), CVCL::TRACE, CVCL::TUPLE_TYPE, and tupleSelect().

void TheoryRecords::computeModelTerm (  const Expr &  e, std::vector< Expr > &  v )  [virtual]

Add variables from 'e' to 'v' for constructing a concrete model. If e is already of primitive type, do NOT add it to v. Reimplemented from CVCL::Theory. Definition at line 268 of file theory_records.cpp. References CVCL::Expr::arity(), CVCL::Type::getExpr(), getFields(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::RECORD_TYPE, recordSelect(), rewrite(), CVCL::TUPLE_TYPE, and tupleSelect().

void TheoryRecords::computeModel (  const Expr &  e, std::vector< Expr > &  v )  [virtual]

Compute the value of a compound variable from the more primitive ones. The more primitive variables for e are already assigned concrete values, and are available through getModelValue(). The new value for e must be assigned using assignValue() method. Parameters: e  is the compound type expression to assign a value; vars  are the variables actually assigned. Normally, 'e' is the only element of vars. However, e.g. in the case of uninterpreted functions, assigning 'f' means assigning all relevant applications of 'f' to constant values (f(0), f(5), etc.). Such applications might not be known before the model is constructed (they may be of the form f(x), f(y+z), etc., where x,y,z are still unassigned). Populating 'vars' is an opportunity for a DP to change the set of top-level "variables" to assign, if needed. In particular, it may drop 'e' from the model entirely, if it is already a concrete value by itself. Reimplemented from CVCL::Theory. Definition at line 288 of file theory_records.cpp. References CVCL::Expr::arity(), CVCL::Theory::assignValue(), d_rules, CVCL::RecordsProofRules::expandRecord(), CVCL::RecordsProofRules::expandTuple(), CVCL::Theory::getBaseType(), CVCL::Type::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theory::getModelValue(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::RECORD_TYPE, CVCL::Theory::substitutivityRule(), CVCL::Expr::toString(), CVCL::Theory::transitivityRule(), and CVCL::TUPLE_TYPE.

Expr TheoryRecords::computeTCC (  const Expr &  e  )  [virtual]

Compute and cache the TCC of e. Parameters: e  is an expression (term or formula). This function computes the TCC of e which is true iff the expression is defined. This function computes the TCC or predicate of the top-level operator of e, and recurses into children using getTCC(), if necessary. The default implementation is to compute TCCs recursively for all children, and return their conjunction. Reimplemented from CVCL::Theory. Definition at line 235 of file theory_records.cpp. References CVCL::Expr::andExpr(), CVCL::Theory::computeTCC(), getField(), getFieldIndex(), getIndex(), CVCL::Theorem::getRHS(), CVCL::Theory::getTypePred(), CVCL::RECORD, CVCL::RECORD_SELECT, CVCL::RECORD_UPDATE, CVCL::Theory::rewriteAnd(), CVCL::TRACE, CVCL::TUPLE, CVCL::TUPLE_SELECT, and CVCL::TUPLE_UPDATE.

Expr TheoryRecords::parseExprOp (  const Expr &  e  )  [virtual]

Theory-specific parsing implemented by the DP. Reimplemented from CVCL::Theory. Definition at line 872 of file theory_records.cpp. References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Expr::getEM(), CVCL::Type::getExpr(), CVCL::ExprManager::getKind(), CVCL::Expr::getKind(), CVCL::Expr::getRational(), CVCL::Expr::getString(), CVCL::ID, CVCL::Rational::isInteger(), CVCL::Expr::isRational(), CVCL::Theory::parseExpr(), CVCL::RAW_LIST, CVCL::RECORD, CVCL::RECORD_SELECT, CVCL::RECORD_TYPE, CVCL::RECORD_UPDATE, recordExpr(), recordSelect(), recordType(), recordUpdate(), CVCL::Expr::toString(), CVCL::TRACE, CVCL::TUPLE, CVCL::TUPLE_SELECT, CVCL::TUPLE_TYPE, CVCL::TUPLE_UPDATE, tupleExpr(), tupleSelect(), tupleType(), and tupleUpdate().

void TheoryRecords::setup (  const Expr &  e  )  [virtual]

Set up the term e for call-backs when e or its children change. setup is called once for each expression associated with the theory. It is typically used to setup theory-specific data for an expression and to add call-back information for use with update. See also: update Reimplemented from CVCL::Theory. Definition at line 501 of file theory_records.cpp. References CVCL::Expr::arity(), CVCL::Expr::begin(), d_rules, CVCL::Expr::end(), CVCL::Theory::enqueueFact(), CVCL::RecordsProofRules::expandRecord(), CVCL::RecordsProofRules::expandTuple(), CVCL::Theory::find(), CVCL::Theory::getBaseType(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::hasFind(), CVCL::int2string(), CVCL::Theorem::isNull(), isRecordType(), CVCL::Expr::isTerm(), isTupleType(), CVCL::RECORD, rewrite(), CVCL::Expr::setFind(), CVCL::Theory::setupCC(), CVCL::Theory::substitutivityRule(), CVCL::Theory::symmetryRule(), CVCL::TRACE, CVCL::Theory::transitivityRule(), and CVCL::TUPLE.

void TheoryRecords::update (  const Theorem &  e, const Expr &  d )  [virtual]

Notify a theory of a new equality. update is a call-back used by the notify mechanism of the core theory. It works as follows. When an equation t1 = t2 makes it into the core framework, the two find equivalence classes for t1 and t2 are merged. The result is that t2 is the new equivalence class representative and t1 is no longer an equivalence class representative. When this happens, the notify list of t1 is traversed. Notify list entries consist of a theory and an expression d. For each entry (i,d), i->update(e, d) is called, where e is the theorem corresponding to the equality t1=t2. To add the entry (i,d) to a term t1's notify list, a call must be made to t1.addNotify(i,d). This is typically done in setup. See also: setup Reimplemented from CVCL::Theory. Definition at line 554 of file theory_records.cpp. References CVCL::Theory::enqueueEquality(), CVCL::Theory::find(), CVCL::Expr::getOpKind(), CVCL::Theorem::getRHS(), CVCL::Expr::hasFind(), CVCL::Theory::inconsistent(), CVCL::RECORD, rewrite(), CVCL::Theory::transitivityRule(), CVCL::TUPLE, CVCL::Theory::updateCC(), and CVCL::Theory::updateHelper().

ExprStream & TheoryRecords::print (  ExprStream &  os, const Expr &  e )  [virtual]

pretty printing Reimplemented from CVCL::Theory. Definition at line 577 of file theory_records.cpp. References CVCL::Expr::arity(), CVCL::Theory::d_theoryUsed, getField(), getFields(), getIndex(), CVCL::Expr::getOpKind(), isRecord(), isRecordAccess(), isRecordType(), isTupleAccess(), CVCL::ExprStream::lang(), CVCL::LISP_LANG, CVCL::pop(), CVCL::PRESENTATION_LANG, CVCL::Expr::printAST(), CVCL::push(), CVCL::RECORD, CVCL::RECORD_SELECT, CVCL::RECORD_TYPE, CVCL::RECORD_UPDATE, CVCL::SMTLIB_LANG, CVCL::space(), CVCL::TUPLE, CVCL::TUPLE_SELECT, CVCL::TUPLE_TYPE, and CVCL::TUPLE_UPDATE.

bool CVCL::TheoryRecords::isRecord (  const Expr &  e  )  [inline]

Test whether expr is a record literal. Definition at line 97 of file theory_records.h. References CVCL::Expr::getOpKind(), CVCL::Expr::isApply(), and CVCL::RECORD. Referenced by print().

bool CVCL::TheoryRecords::isRecordType (  const Expr &  e  )  [inline]

Test whether expr is a record type. Definition at line 101 of file theory_records.h. References CVCL::Expr::getOpKind(), CVCL::Expr::isApply(), and CVCL::RECORD_TYPE. Referenced by isRecordType(), CVCL::RecordsTheoremProducer::isRecordType(), print(), and setup().

bool CVCL::TheoryRecords::isRecordType (  const Type &  t  )  [inline]

Test whether expr is a record type. Definition at line 105 of file theory_records.h. References CVCL::Type::getExpr(), and isRecordType().

bool CVCL::TheoryRecords::isRecordAccess (  const Expr &  e  )  [inline]

Test whether expr is a record select/update subclass. Definition at line 109 of file theory_records.h. References CVCL::Expr::getOpKind(), CVCL::Expr::isApply(), CVCL::RECORD_SELECT, and CVCL::RECORD_UPDATE. Referenced by CVCL::RecordsTheoremProducer::isRecordAccess(), and print().

Expr TheoryRecords::recordExpr (  const std::vector< std::string > &  fields, const std::vector< Expr > &  kids )

Create a record literal. Definition at line 953 of file theory_records.cpp. References CVCL::Expr::begin(), and CVCL::Theory::getEM(). Referenced by parseExprOp(), and CVCL::RecordsTheoremProducer::recordExpr().

Expr TheoryRecords::recordExpr (  const std::vector< Expr > &  fields, const std::vector< Expr > &  kids )

Create a record literal. Definition at line 962 of file theory_records.cpp. References CVCL::RECORD.

Type TheoryRecords::recordType (  const std::vector< std::string > &  fields, const std::vector< Type > &  types )

Create a record type. Definition at line 969 of file theory_records.cpp. Referenced by computeType(), parseExprOp(), recordType(), and CVCL::RecordsTheoremProducer::recordType().

Type TheoryRecords::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). Definition at line 980 of file theory_records.cpp. References CVCL::Theory::getEM(), and recordType().

Type TheoryRecords::recordType (  const std::vector< Expr > &  fields, const std::vector< Expr > &  types )

Create a record type (fields and types are given as a vector of Expr). Definition at line 989 of file theory_records.cpp. References CVCL::RECORD_TYPE.

Expr TheoryRecords::recordSelect (  const Expr &  r, const std::string &  field )

Create a record field select expression. Definition at line 996 of file theory_records.cpp. References CVCL::Theory::getEM(), and CVCL::RECORD_SELECT. Referenced by computeModelTerm(), computeTypePred(), parseExprOp(), and CVCL::RecordsTheoremProducer::recordSelect().

Expr TheoryRecords::recordUpdate (  const Expr &  r, const std::string &  field, const Expr &  val )

Create a record field update expression. Definition at line 1002 of file theory_records.cpp. References CVCL::Theory::getEM(), and CVCL::RECORD_UPDATE. Referenced by parseExprOp(), and CVCL::RecordsTheoremProducer::recordUpdate().

const vector< Expr > & TheoryRecords::getFields (  const Expr &  r  )

Get the list of fields from a record literal. Definition at line 1009 of file theory_records.cpp. References CVCL::AST_LANG, CVCL::Expr::getKids(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::isApply(), CVCL::RECORD, CVCL::RECORD_TYPE, and CVCL::Expr::toString(). Referenced by computeModelTerm(), computeType(), computeTypePred(), CVCL::RecordsTheoremProducer::getFields(), and print().

const string & TheoryRecords::getField (  const Expr &  e, int  i )

Get the i-th field name from the record literal or type. Definition at line 1019 of file theory_records.cpp. References CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getString(), CVCL::Expr::isApply(), CVCL::RECORD, CVCL::RECORD_TYPE, and CVCL::Expr::toString(). Referenced by computeTCC(), computeType(), CVCL::RecordsTheoremProducer::getField(), and print().

int CVCL::TheoryRecords::getFieldIndex (  const Expr &  e, const std::string &  field )

Get the field index in the record literal or type. The field must be present in the record; otherwise it's an error. Referenced by computeTCC(), computeType(), and CVCL::RecordsTheoremProducer::getFieldIndex().

const std::string & TheoryRecords::getField (  const Expr &  e  )

Get the field name from the record select and update expressions. Definition at line 1041 of file theory_records.cpp. References CVCL::Expr::getName(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::isApply(), CVCL::RECORD_SELECT, and CVCL::RECORD_UPDATE.

Expr TheoryRecords::tupleExpr (  const std::vector< Expr > &  kids  )

Create a tuple literal. Definition at line 1050 of file theory_records.cpp. References CVCL::Theory::getEM(), and CVCL::TUPLE. Referenced by parseExprOp(), and CVCL::RecordsTheoremProducer::tupleExpr().

Type TheoryRecords::tupleType (  const std::vector< Type > &  types  )

Create a tuple type. Definition at line 1056 of file theory_records.cpp. References CVCL::Theory::getEM(), and CVCL::TUPLE_TYPE. Referenced by parseExprOp(), CVCL::VCL::tupleType(), and CVCL::RecordsTheoremProducer::tupleType().

Type TheoryRecords::tupleType (  const std::vector< Expr > &  types  )

Create a tuple type (types of components are given as Exprs). Definition at line 1066 of file theory_records.cpp. References CVCL::Theory::getEM(), and CVCL::TUPLE_TYPE.

Expr TheoryRecords::tupleSelect (  const Expr &  tup, int  i )

Create a tuple index selector expression. Definition at line 1072 of file theory_records.cpp. References CVCL::Theory::getEM(), and CVCL::TUPLE_SELECT. Referenced by computeModelTerm(), computeTypePred(), parseExprOp(), CVCL::RecordsTheoremProducer::tupleSelect(), and CVCL::VCL::tupleSelectExpr().

Expr TheoryRecords::tupleUpdate (  const Expr &  tup, int  i, const Expr &  val )

Create a tuple index update expression. Definition at line 1078 of file theory_records.cpp. References CVCL::Theory::getEM(), and CVCL::TUPLE_UPDATE. Referenced by parseExprOp(), CVCL::RecordsTheoremProducer::tupleUpdate(), and CVCL::VCL::tupleUpdateExpr().

int TheoryRecords::getIndex (  const Expr &  e  )

Get the index from the tuple select and update expressions. Definition at line 1084 of file theory_records.cpp. References CVCL::Rational::getInt(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getRational(), CVCL::Expr::isApply(), CVCL::TUPLE_SELECT, and CVCL::TUPLE_UPDATE. Referenced by computeTCC(), computeType(), CVCL::RecordsTheoremProducer::getIndex(), and print().

bool CVCL::TheoryRecords::isTupleAccess (  const Expr &  e  )  [inline]

Test whether expr is a tuple select/update subclass. Definition at line 153 of file theory_records.h. References CVCL::Expr::getOpKind(), CVCL::Expr::isApply(), CVCL::TUPLE_SELECT, and CVCL::TUPLE_UPDATE. Referenced by CVCL::RecordsTheoremProducer::isTupleAccess(), and print().

bool CVCL::TheoryRecords::isTuple (  const Expr &  e  )  [inline]

Test if expr is a tuple literal. Definition at line 157 of file theory_records.h. References CVCL::Expr::getOpKind(), CVCL::Expr::isApply(), and CVCL::TUPLE.

bool CVCL::TheoryRecords::isTupleType (  const Expr &  e  )  [inline]

Test if expr represents a tuple type. Definition at line 159 of file theory_records.h. References CVCL::Expr::getOpKind(), CVCL::Expr::isApply(), and CVCL::TUPLE_TYPE. Referenced by isTupleType(), and setup().

bool CVCL::TheoryRecords::isTupleType (  const Type &  tp  )  [inline]

Test if 'tp' is a tuple type. Definition at line 162 of file theory_records.h. References CVCL::Type::getExpr(), and isTupleType().

---

Member Data Documentation

RecordsProofRules* CVCL::TheoryRecords::d_rules [private]

Definition at line 60 of file theory_records.h. Referenced by assertFact(), computeModel(), rewrite(), setup(), TheoryRecords(), and ~TheoryRecords().

---

The documentation for this class was generated from the following files:

• theory_records.h
• records_theorem_producer.cpp
• theory_records.cpp

---