CVC3::RecordsTheoremProducer Class Reference

#include <records_theorem_producer.h>

Inheritance diagram for CVC3::RecordsTheoremProducer:

Inheritance graph
[legend]
Collaboration diagram for CVC3::RecordsTheoremProducer:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Attributes


Detailed Description

Definition at line 29 of file records_theorem_producer.h.


Constructor & Destructor Documentation

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

Definition at line 35 of file records_theorem_producer.h.


Member Function Documentation

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

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

Implements CVC3::RecordsProofRules.

Definition at line 40 of file records_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), getField(), getFieldIndex(), getIndex(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::RECORD, CVC3::RECORD_SELECT, CVC3::Expr::toString(), CVC3::TUPLE, CVC3::TUPLE_SELECT, and CVC3::TheoremProducer::withProof().

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

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

Implements CVC3::RecordsProofRules.

Definition at line 81 of file records_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), getField(), getIndex(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::RECORD_SELECT, CVC3::RECORD_UPDATE, recordSelect(), CVC3::Expr::toString(), CVC3::TUPLE_SELECT, CVC3::TUPLE_UPDATE, tupleSelect(), and CVC3::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 CVC3::RecordsProofRules.

Definition at line 120 of file records_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), getField(), getFieldIndex(), getFields(), getIndex(), CVC3::Expr::getKids(), CVC3::Expr::getOpKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::RECORD, CVC3::RECORD_UPDATE, recordExpr(), CVC3::Expr::toString(), CVC3::TUPLE, CVC3::TUPLE_UPDATE, tupleExpr(), and CVC3::TheoremProducer::withProof().

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

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

Implements CVC3::RecordsProofRules.

Definition at line 205 of file records_theorem_producer.cpp.

References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Type::getExpr(), CVC3::Theorem::getExpr(), getField(), getFields(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::RECORD_TYPE, recordSelect(), CVC3::Expr::toString(), CVC3::TUPLE_TYPE, tupleSelect(), and CVC3::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 CVC3::RecordsProofRules.

Definition at line 158 of file records_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::EQ, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Type::getExpr(), CVC3::Theorem::getExpr(), getField(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::Theorem::getProof(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::NOT, CVC3::orExpr(), CVC3::RECORD_TYPE, recordSelect(), CVC3::Expr::toString(), CVC3::TUPLE_TYPE, tupleSelect(), and CVC3::TheoremProducer::withProof().

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

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

Implements CVC3::RecordsProofRules.

Definition at line 252 of file records_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, d_theoryRecords, CVC3::Assumptions::emptyAssump(), CVC3::Theory::getBaseType(), getFields(), CVC3::Expr::getString(), isRecordType(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), recordExpr(), recordSelect(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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

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

Implements CVC3::RecordsProofRules.

Definition at line 269 of file records_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, d_theoryRecords, CVC3::Assumptions::emptyAssump(), CVC3::Theory::getBaseType(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::TUPLE_TYPE, tupleExpr(), tupleSelect(), and CVC3::TheoremProducer::withProof().

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

Test whether expr is a record type.

Definition at line 47 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::isRecordType().

Referenced by expandRecord().

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

Test whether Type is a record type.

Definition at line 50 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::isRecordType().

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

Test whether expr is a record select/update subclass.

Definition at line 53 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::isRecordAccess().

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

Create a record literal.

Definition at line 56 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::recordExpr().

Referenced by expandRecord(), and rewriteLitUpdate().

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

Create a record literal.

Definition at line 60 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::recordExpr().

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

Create a record type.

Definition at line 64 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::recordType().

Type CVC3::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 68 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::recordType().

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

Create a record field select expression.

Definition at line 72 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::recordSelect().

Referenced by expandEq(), expandNeq(), expandRecord(), and rewriteUpdateSelect().

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

Create a record field update expression.

Definition at line 75 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::recordUpdate().

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

Get the list of fields from a record literal.

Definition at line 79 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::getFields().

Referenced by expandEq(), expandRecord(), and rewriteLitUpdate().

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

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

Definition at line 82 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::getField().

Referenced by expandEq(), expandNeq(), rewriteLitSelect(), rewriteLitUpdate(), and rewriteUpdateSelect().

int CVC3::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 86 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::getFieldIndex().

Referenced by rewriteLitSelect(), and rewriteLitUpdate().

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

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

Definition at line 89 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::getField().

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

Create a tuple literal.

Definition at line 92 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::tupleExpr().

Referenced by expandTuple(), and rewriteLitUpdate().

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

Create a tuple type.

Definition at line 95 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::tupleType().

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

Create a tuple type (types of components are given as Exprs).

Definition at line 98 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::tupleType().

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

Create a tuple index selector expression.

Definition at line 101 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::tupleSelect().

Referenced by expandEq(), expandNeq(), expandTuple(), and rewriteUpdateSelect().

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

Create a tuple index update expression.

Definition at line 104 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::tupleUpdate().

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

Get the index from the tuple select and update expressions.

Definition at line 107 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::getIndex().

Referenced by rewriteLitSelect(), rewriteLitUpdate(), and rewriteUpdateSelect().

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

Test whether expr is a tuple select/update subclass.

Definition at line 110 of file records_theorem_producer.h.

References d_theoryRecords, and CVC3::TheoryRecords::isTupleAccess().


Member Data Documentation

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

Definition at line 31 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:
Generated on Wed Nov 18 16:18:34 2009 for CVC3 by  doxygen 1.5.2