CVC3
Public Member Functions | Private Attributes

CVC3::RecordsTheoremProducer Class Reference

#include <records_theorem_producer.h>

Inherits CVC3::RecordsProofRules, and CVC3::TheoremProducer.

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]
Theorem RecordsTheoremProducer::rewriteUpdateSelect ( const Expr e) [virtual]
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::Expr::getKids(), CVC3::Expr::getOpKind(), CVC3::RECORD, CVC3::RECORD_UPDATE, CVC3::Expr::toString(), CVC3::TUPLE, and CVC3::TUPLE_UPDATE.

Theorem RecordsTheoremProducer::expandEq ( const Theorem eqThrm) [virtual]
Theorem RecordsTheoremProducer::expandNeq ( const Theorem neqThrm) [virtual]
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, CVC3::Expr::getString(), and CVC3::Expr::toString().

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, CVC3::Expr::toString(), and CVC3::TUPLE_TYPE.

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

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

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

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

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

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

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

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

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

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


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