#include <records_theorem_producer.h>

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

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::Expr::getOpKind(), CVC3::RECORD, CVC3::RECORD_SELECT, CVC3::Expr::toString(), CVC3::TUPLE, and CVC3::TUPLE_SELECT.

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::Expr::getOpKind(), CVC3::RECORD_SELECT, CVC3::RECORD_UPDATE, CVC3::Expr::toString(), CVC3::TUPLE_SELECT, and CVC3::TUPLE_UPDATE.

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]

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::Theorem::getExpr(), CVC3::Type::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::Theorem::isRewrite(), CVC3::RECORD_TYPE, CVC3::Expr::toString(), and CVC3::TUPLE_TYPE.

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, EQ, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Type::getExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::Theorem::getProof(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), NOT, CVC3::orExpr(), CVC3::RECORD_TYPE, CVC3::Expr::toString(), and CVC3::TUPLE_TYPE.

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

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

Definition at line 31 of file records_theorem_producer.h.

Referenced by 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:

CVC3::RecordsTheoremProducer Class Reference

Public Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation