CVC3::RecordsTheoremProducer Class Reference

#include <records_theorem_producer.h>

Inheritance diagram for CVC3::RecordsTheoremProducer:

[legend]Collaboration diagram for CVC3::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 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

1.5.2