CVC3
2.4.1
|
#include <records_theorem_producer.h>
Public Member Functions | |
RecordsTheoremProducer (TheoremManager *tm, TheoryRecords *t) | |
Theorem | rewriteLitSelect (const Expr &e) |
==> (SELECT (LITERAL v1 ... vi ...) fi) = vi More... | |
Theorem | rewriteUpdateSelect (const Expr &e) |
==> (RECORD_SELECT (RECORD_UPDATE r fi vi) fj) = vi More... | |
Theorem | rewriteLitUpdate (const Expr &e) |
==> (RECORD_UPDATE (RECORD (f1 v1) ... (fi vi) ...) fi v') =(RECORD (f1 v1) ... (fi v') ...) and same for tuples. More... | |
Theorem | expandEq (const Theorem &eqThrm) |
From T|- e = e' return T|- AND (e.i = e'.i) for all i. More... | |
Theorem | expandNeq (const Theorem &neqThrm) |
From T|- NOT e=e' return T|- NOT AND (e.i = e'.i) for all i. More... | |
Theorem | expandRecord (const Expr &e) |
Expand a record into a literal: |- e = (# f1:=e.f1, ..., fn:=e.fn #) More... | |
Theorem | expandTuple (const Expr &e) |
Expand a tuple into a literal: |- e = (e.0, ..., e.n-1) More... | |
bool | isRecordType (const Expr &e) |
Test whether expr is a record type. More... | |
bool | isRecordType (const Type &t) |
Test whether Type is a record type. More... | |
bool | isRecordAccess (const Expr &e) |
Test whether expr is a record select/update subclass. More... | |
Expr | recordExpr (const std::vector< std::string > &fields, const std::vector< Expr > &kids) |
Create a record literal. More... | |
Expr | recordExpr (const std::vector< Expr > &fields, const std::vector< Expr > &kids) |
Create a record literal. More... | |
Type | recordType (const std::vector< std::string > &fields, const std::vector< Type > &types) |
Create a record type. More... | |
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) More... | |
Expr | recordSelect (const Expr &r, const std::string &field) |
Create a record field select expression. More... | |
Expr | recordUpdate (const Expr &r, const std::string &field, const Expr &val) |
Create a record field update expression. More... | |
const std::vector< Expr > & | getFields (const Expr &r) |
Get the list of fields from a record literal. More... | |
const std::string & | getField (const Expr &e, int i) |
Get the i-th field name from the record literal or type. More... | |
int | getFieldIndex (const Expr &e, const std::string &field) |
Get the field index in the record literal or type. More... | |
const std::string & | getField (const Expr &e) |
Get the field name from the record select and update expressions. More... | |
Expr | tupleExpr (const std::vector< Expr > &kids) |
Create a tuple literal. More... | |
Type | tupleType (const std::vector< Type > &types) |
Create a tuple type. More... | |
Type | tupleType (const std::vector< Expr > &types) |
Create a tuple type (types of components are given as Exprs) More... | |
Expr | tupleSelect (const Expr &tup, int i) |
Create a tuple index selector expression. More... | |
Expr | tupleUpdate (const Expr &tup, int i, const Expr &val) |
Create a tuple index update expression. More... | |
int | getIndex (const Expr &e) |
Get the index from the tuple select and update expressions. More... | |
bool | isTupleAccess (const Expr &e) |
Test whether expr is a tuple select/update subclass. More... | |
![]() | |
virtual | ~RecordsProofRules () |
< Destructor More... | |
![]() | |
TheoremProducer (TheoremManager *tm) | |
virtual | ~TheoremProducer () |
bool | withProof () |
Testing whether to generate proofs. More... | |
bool | withAssumptions () |
Testing whether to generate assumptions. More... | |
Proof | newLabel (const Expr &e) |
Create a new proof label (bound variable) for an assumption (formula) More... | |
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) More... | |
Proof | newPf (const Proof &label, const Proof &pf) |
Creating LAMBDA-abstraction (LAMBDA label proof). More... | |
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) More... | |
Proof | newPf (const std::vector< Proof > &labels, const Proof &pf) |
Private Attributes | |
TheoryRecords * | d_theoryRecords |
Additional Inherited Members | |
![]() | |
Theorem | newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf) |
Create a new theorem. See also newRWTheorem() and newReflTheorem() More... | |
Theorem | newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) |
Create a rewrite theorem: lhs = rhs. More... | |
Theorem | newReflTheorem (const Expr &e) |
Create a reflexivity theorem. More... | |
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) |
![]() | |
TheoremManager * | d_tm |
ExprManager * | d_em |
const bool * | d_checkProofs |
Op | d_pfOp |
Expr | d_hole |
Definition at line 29 of file records_theorem_producer.h.
|
inline |
Definition at line 35 of file records_theorem_producer.h.
==> (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.
==> (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.
==> (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.
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.
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.
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().
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.
|
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().
|
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().
|
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().
|
inline |
Create a record literal.
Definition at line 56 of file records_theorem_producer.h.
References d_theoryRecords, and CVC3::TheoryRecords::recordExpr().
|
inline |
Create a record literal.
Definition at line 60 of file records_theorem_producer.h.
References d_theoryRecords, and CVC3::TheoryRecords::recordExpr().
|
inline |
Create a record type.
Definition at line 64 of file records_theorem_producer.h.
References d_theoryRecords, and CVC3::TheoryRecords::recordType().
|
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().
|
inline |
Create a record field select expression.
Definition at line 72 of file records_theorem_producer.h.
References d_theoryRecords, and CVC3::TheoryRecords::recordSelect().
|
inline |
Create a record field update expression.
Definition at line 75 of file records_theorem_producer.h.
References d_theoryRecords, and CVC3::TheoryRecords::recordUpdate().
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().
|
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().
|
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().
|
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().
Create a tuple literal.
Definition at line 92 of file records_theorem_producer.h.
References d_theoryRecords, and CVC3::TheoryRecords::tupleExpr().
Create a tuple type.
Definition at line 95 of file records_theorem_producer.h.
References d_theoryRecords, and CVC3::TheoryRecords::tupleType().
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().
Create a tuple index selector expression.
Definition at line 101 of file records_theorem_producer.h.
References d_theoryRecords, and CVC3::TheoryRecords::tupleSelect().
Create a tuple index update expression.
Definition at line 104 of file records_theorem_producer.h.
References d_theoryRecords, and CVC3::TheoryRecords::tupleUpdate().
|
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().
|
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().
|
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().