CVCL::RecordsTheoremProducer Class Reference

#include <records_theorem_producer.h>

Inheritance diagram for CVCL::RecordsTheoremProducer:

[legend]Collaboration diagram for CVCL::RecordsTheoremProducer:

[legend]List of all members.

Public Member Functions

• RecordsTheoremProducer (TheoremManager *tm, TheoryRecords *t)
• Theorem rewriteLitSelect (const Expr &e)

  ==> (SELECT (LITERAL v1 ... vi ...) fi) = vi
  

• Theorem rewriteUpdateSelect (const Expr &e)

  ==> (RECORD_SELECT (RECORD_UPDATE r fi vi) fj) = vi
  

• Theorem rewriteLitUpdate (const Expr &e)

  ==> (RECORD_UPDATE (RECORD (f1 v1) ... (fi vi) ...) fi v') =(RECORD (f1 v1) ... (fi v') ...) and same for tuples.
  

• Theorem expandEq (const Theorem &eqThrm)

  From T|- e = e' return T|- AND (e.i = e'.i) for all i.
  

• Theorem expandNeq (const Theorem &neqThrm)

  From T|- NOT e=e' return T|- NOT AND (e.i = e'.i) for all i.
  

• Theorem expandRecord (const Expr &e)

  Expand a record into a literal: |- e = (# f1:=e.f1, ..., fn:=e.fn #).
  

• Theorem expandTuple (const Expr &e)

  Expand a tuple into a literal: |- e = (e.0, ..., e.n-1).
  

• bool isRecordType (const Expr &e)

  Test whether expr is a record type.
  

• bool isRecordType (const Type &t)

  Test whether Type 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).
  

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

Private Attributes

• TheoryRecords * d_theoryRecords

---

Detailed Description

Definition at line 37 of file records_theorem_producer.h.

---

Constructor & Destructor Documentation

CVCL::RecordsTheoremProducer::RecordsTheoremProducer (  TheoremManager *  tm, TheoryRecords *  t )  [inline]

Definition at line 43 of file records_theorem_producer.h.

---

Member Function Documentation

Theorem RecordsTheoremProducer::rewriteLitSelect (  const Expr &  e  )  [virtual]

==> (SELECT (LITERAL v1 ... vi ...) fi) = vi Implements CVCL::RecordsProofRules. Definition at line 48 of file records_theorem_producer.cpp. References getField(), getFieldIndex(), getIndex(), CVCL::Expr::getOpKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::RECORD, CVCL::RECORD_SELECT, CVCL::Expr::toString(), CVCL::TUPLE, CVCL::TUPLE_SELECT, and CVCL::TheoremProducer::withProof().

Theorem RecordsTheoremProducer::rewriteUpdateSelect (  const Expr &  e  )  [virtual]

==> (RECORD_SELECT (RECORD_UPDATE r fi vi) fj) = vi Implements CVCL::RecordsProofRules. Definition at line 90 of file records_theorem_producer.cpp. References getField(), getIndex(), CVCL::Expr::getOpKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::RECORD_SELECT, CVCL::RECORD_UPDATE, recordSelect(), CVCL::Expr::toString(), CVCL::TUPLE_SELECT, CVCL::TUPLE_UPDATE, tupleSelect(), and CVCL::TheoremProducer::withProof().

Theorem RecordsTheoremProducer::rewriteLitUpdate (  const Expr &  e  )  [virtual]

==> (RECORD_UPDATE (RECORD (f1 v1) ... (fi vi) ...) fi v') =(RECORD (f1 v1) ... (fi v') ...) and same for tuples. Implements CVCL::RecordsProofRules. Definition at line 130 of file records_theorem_producer.cpp. References getField(), getFieldIndex(), getFields(), getIndex(), CVCL::Expr::getKids(), CVCL::Expr::getOpKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::RECORD, CVCL::RECORD_UPDATE, recordExpr(), CVCL::Expr::toString(), CVCL::TUPLE, CVCL::TUPLE_UPDATE, tupleExpr(), and CVCL::TheoremProducer::withProof().

Theorem RecordsTheoremProducer::expandEq (  const Theorem &  eqThrm  )  [virtual]

From T|- e = e' return T|- AND (e.i = e'.i) for all i. Implements CVCL::RecordsProofRules. Definition at line 219 of file records_theorem_producer.cpp. References CVCL::andExpr(), CVCL::Expr::arity(), CVCL::Expr::eqExpr(), CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Type::getExpr(), getField(), getFields(), CVCL::Theorem::getLHS(), CVCL::Expr::getOpKind(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Expr::iffExpr(), CVCL::Type::isBool(), CVCL::Theorem::isRewrite(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::RECORD_TYPE, recordSelect(), CVCL::Expr::toString(), CVCL::TUPLE_TYPE, tupleSelect(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem RecordsTheoremProducer::expandNeq (  const Theorem &  neqThrm  )  [virtual]

From T|- NOT e=e' return T|- NOT AND (e.i = e'.i) for all i. Implements CVCL::RecordsProofRules. Definition at line 169 of file records_theorem_producer.cpp. References CVCL::Expr::arity(), CVCL::EQ, CVCL::Expr::eqExpr(), CVCL::Theorem::getAssumptions(), CVCL::Type::getExpr(), CVCL::Theorem::getExpr(), getField(), CVCL::Expr::getKind(), CVCL::Expr::getOpKind(), CVCL::Theorem::getProof(), CVCL::Expr::getType(), CVCL::Expr::iffExpr(), CVCL::Type::isBool(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::NOT, CVCL::orExpr(), CVCL::RECORD_TYPE, recordSelect(), CVCL::Expr::toString(), CVCL::TUPLE_TYPE, tupleSelect(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem RecordsTheoremProducer::expandRecord (  const Expr &  e  )  [virtual]

Expand a record into a literal: |- e = (# f1:=e.f1, ..., fn:=e.fn #). Implements CVCL::RecordsProofRules. Definition at line 269 of file records_theorem_producer.cpp. References d_theoryRecords, CVCL::Theory::getBaseType(), CVCL::Type::getExpr(), getFields(), CVCL::Expr::getString(), isRecordType(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), recordExpr(), recordSelect(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem RecordsTheoremProducer::expandTuple (  const Expr &  e  )  [virtual]

Expand a tuple into a literal: |- e = (e.0, ..., e.n-1). Implements CVCL::RecordsProofRules. Definition at line 287 of file records_theorem_producer.cpp. References CVCL::Type::arity(), d_theoryRecords, CVCL::Theory::getBaseType(), CVCL::Type::getExpr(), CVCL::Expr::getOpKind(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), CVCL::TUPLE_TYPE, tupleExpr(), tupleSelect(), and CVCL::TheoremProducer::withProof().

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

Test whether expr is a record type. Definition at line 55 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::isRecordType(). Referenced by expandRecord().

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

Test whether Type is a record type. Definition at line 58 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::isRecordType().

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

Test whether expr is a record select/update subclass. Definition at line 61 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::isRecordAccess().

Expr CVCL::RecordsTheoremProducer::recordExpr (  const std::vector< std::string > &  fields, const std::vector< Expr > &  kids )  [inline]

Create a record literal. Definition at line 64 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::recordExpr(). Referenced by expandRecord(), and rewriteLitUpdate().

Expr CVCL::RecordsTheoremProducer::recordExpr (  const std::vector< Expr > &  fields, const std::vector< Expr > &  kids )  [inline]

Create a record literal. Definition at line 68 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::recordExpr().

Type CVCL::RecordsTheoremProducer::recordType (  const std::vector< std::string > &  fields, const std::vector< Type > &  types )  [inline]

Create a record type. Definition at line 72 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::recordType().

Type CVCL::RecordsTheoremProducer::recordType (  const std::vector< std::string > &  fields, const std::vector< Expr > &  types )  [inline]

Create a record type (field types are given as a vector of Expr). Definition at line 76 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::recordType().

Expr CVCL::RecordsTheoremProducer::recordSelect (  const Expr &  r, const std::string &  field )  [inline]

Create a record field select expression. Definition at line 80 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::recordSelect(). Referenced by expandEq(), expandNeq(), expandRecord(), and rewriteUpdateSelect().

Expr CVCL::RecordsTheoremProducer::recordUpdate (  const Expr &  r, const std::string &  field, const Expr &  val )  [inline]

Create a record field update expression. Definition at line 83 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::recordUpdate().

const std::vector<Expr>& CVCL::RecordsTheoremProducer::getFields (  const Expr &  r  )  [inline]

Get the list of fields from a record literal. Definition at line 87 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::getFields(). Referenced by expandEq(), expandRecord(), and rewriteLitUpdate().

const std::string& CVCL::RecordsTheoremProducer::getField (  const Expr &  e, int  i )  [inline]

Get the i-th field name from the record literal or type. Definition at line 90 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::getField(). Referenced by expandEq(), expandNeq(), rewriteLitSelect(), rewriteLitUpdate(), and rewriteUpdateSelect().

int CVCL::RecordsTheoremProducer::getFieldIndex (  const Expr &  e, const std::string &  field )  [inline]

Get the field index in the record literal or type. The field must be present in the record; otherwise it's an error. Definition at line 94 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::getFieldIndex(). Referenced by rewriteLitSelect(), and rewriteLitUpdate().

const std::string& CVCL::RecordsTheoremProducer::getField (  const Expr &  e  )  [inline]

Get the field name from the record select and update expressions. Definition at line 97 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::getField().

Expr CVCL::RecordsTheoremProducer::tupleExpr (  const std::vector< Expr > &  kids  )  [inline]

Create a tuple literal. Definition at line 100 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::tupleExpr(). Referenced by expandTuple(), and rewriteLitUpdate().

Type CVCL::RecordsTheoremProducer::tupleType (  const std::vector< Type > &  types  )  [inline]

Create a tuple type. Definition at line 103 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::tupleType().

Type CVCL::RecordsTheoremProducer::tupleType (  const std::vector< Expr > &  types  )  [inline]

Create a tuple type (types of components are given as Exprs). Definition at line 106 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::tupleType().

Expr CVCL::RecordsTheoremProducer::tupleSelect (  const Expr &  tup, int  i )  [inline]

Create a tuple index selector expression. Definition at line 109 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::tupleSelect(). Referenced by expandEq(), expandNeq(), expandTuple(), and rewriteUpdateSelect().

Expr CVCL::RecordsTheoremProducer::tupleUpdate (  const Expr &  tup, int  i, const Expr &  val )  [inline]

Create a tuple index update expression. Definition at line 112 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::tupleUpdate().

int CVCL::RecordsTheoremProducer::getIndex (  const Expr &  e  )  [inline]

Get the index from the tuple select and update expressions. Definition at line 115 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::getIndex(). Referenced by rewriteLitSelect(), rewriteLitUpdate(), and rewriteUpdateSelect().

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

Test whether expr is a tuple select/update subclass. Definition at line 118 of file records_theorem_producer.h. References d_theoryRecords, and CVCL::TheoryRecords::isTupleAccess().

---

Member Data Documentation

TheoryRecords* CVCL::RecordsTheoremProducer::d_theoryRecords [private]

Definition at line 39 of file records_theorem_producer.h. Referenced by expandRecord(), expandTuple(), getField(), getFieldIndex(), getFields(), getIndex(), isRecordAccess(), isRecordType(), isTupleAccess(), recordExpr(), recordSelect(), recordType(), recordUpdate(), tupleExpr(), tupleSelect(), tupleType(), and tupleUpdate().

---

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

• records_theorem_producer.h
• records_theorem_producer.cpp

---