CVC3  2.4.1
Public Member Functions | Private Attributes | List of all members
CVC3::RecordsTheoremProducer Class Reference

#include <records_theorem_producer.h>

Inheritance diagram for CVC3::RecordsTheoremProducer:
CVC3::RecordsProofRules CVC3::TheoremProducer

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

TheoryRecordsd_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
TheoremManagerd_tm
ExprManagerd_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
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

TheoryRecords* CVC3::RecordsTheoremProducer::d_theoryRecords
private

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