#include <records_theorem_producer.h>

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

Collaboration diagram for CVC3::RecordsTheoremProducer:

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.

Public Member Functions inherited from CVC3::RecordsProofRules
virtual	~RecordsProofRules ()
	< Destructor

Public Member Functions inherited from CVC3::TheoremProducer
	TheoremProducer (TheoremManager *tm)

virtual	~TheoremProducer ()

bool	withProof ()
	Testing whether to generate proofs.

bool	withAssumptions ()
	Testing whether to generate assumptions.

Proof	newLabel (const Expr &e)
	Create a new proof label (bound variable) for an assumption (formula)

Proof	newPf (const std::string &name)

Proof	newPf (const std::string &name, const Expr &e)

Proof	newPf (const std::string &name, const Proof &pf)

Proof	newPf (const std::string &name, const Expr &e1, const Expr &e2)

Proof	newPf (const std::string &name, const Expr &e, const Proof &pf)

Proof	newPf (const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3)

Proof	newPf (const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf)

Proof	newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end)

Proof	newPf (const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end)

Proof	newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs)

Proof	newPf (const std::string &name, const std::vector< Expr > &args)

Proof	newPf (const std::string &name, const Expr &e, const std::vector< Expr > &args)

Proof	newPf (const std::string &name, const Expr &e, const std::vector< Proof > &pfs)

Proof	newPf (const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs)

Proof	newPf (const std::string &name, const std::vector< Proof > &pfs)

Proof	newPf (const std::string &name, const std::vector< Expr > &args, const Proof &pf)

Proof	newPf (const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs)

Proof	newPf (const Proof &label, const Expr &frm, const Proof &pf)
	Creating LAMBDA-abstraction (LAMBDA label formula proof)

Proof	newPf (const Proof &label, const Proof &pf)
	Creating LAMBDA-abstraction (LAMBDA label proof).

Proof	newPf (const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf)
	Similarly, multi-argument lambda-abstractions: (LAMBDA (u1,...,un): (f1,...,fn). pf)

Proof	newPf (const std::vector< Proof > &labels, const Proof &pf)

Private Attributes
TheoryRecords *	d_theoryRecords

Additional Inherited Members
Protected Member Functions inherited from CVC3::TheoremProducer
Theorem	newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf)
	Create a new theorem. See also newRWTheorem() and newReflTheorem()

Theorem	newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
	Create a rewrite theorem: lhs = rhs.

Theorem	newReflTheorem (const Expr &e)
	Create a reflexivity theorem.

Theorem	newAssumption (const Expr &thm, const Proof &pf, int scope=-1)

Theorem3	newTheorem3 (const Expr &thm, const Assumptions &assump, const Proof &pf)

Theorem3	newRWTheorem3 (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)

void	soundError (const std::string &file, int line, const std::string &cond, const std::string &msg)

Protected Attributes inherited from CVC3::TheoremProducer
TheoremManager *	d_tm

ExprManager *	d_em

const bool *	d_checkProofs

Op	d_pfOp

Expr	d_hole

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::Type::getExpr(), CVC3::Theorem::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:

Public Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation