CVC3
|
#include <records_proof_rules.h>
Inherited by CVC3::RecordsTheoremProducer.
Public Member Functions | |
virtual | ~RecordsProofRules () |
< Destructor | |
virtual Theorem | rewriteLitSelect (const Expr &e)=0 |
==> (REC_LITERAL (f1 v1) ... (fi vi) ...).fi = vi | |
virtual Theorem | rewriteUpdateSelect (const Expr &e)=0 |
==> (REC_SELECT (REC_UPDATE e fi vi) fi) = vi | |
virtual Theorem | rewriteLitUpdate (const Expr &e)=0 |
==> (REC_UPDATE (REC_LITERAL (f1 v1) ... (fi vi) ...) fi v') =(REC_LITERAL (f1 v1) ... (fi v') ...) | |
virtual Theorem | expandEq (const Theorem &eqThrm)=0 |
From T|- e = e' return T|- AND (e.i = e'.i) for all i. | |
virtual Theorem | expandNeq (const Theorem &neqThrm)=0 |
From T|- NOT e=e' return T|- NOT AND (e.i = e'.i) for all i. | |
virtual Theorem | expandRecord (const Expr &e)=0 |
Expand a record into a literal: |- e = (# f1:=e.f1, ..., fn:=e.fn #) | |
virtual Theorem | expandTuple (const Expr &e)=0 |
Expand a tuple into a literal: |- e = (e.0, ..., e.n-1) | |
Definition at line 28 of file records_proof_rules.h.
|
inlinevirtual |
< Destructor
Definition at line 31 of file records_proof_rules.h.
==> (REC_LITERAL (f1 v1) ... (fi vi) ...).fi = vi
Implemented in CVC3::RecordsTheoremProducer.
Referenced by CVC3::TheoryRecords::rewrite().
==> (REC_SELECT (REC_UPDATE e fi vi) fi) = vi
Implemented in CVC3::RecordsTheoremProducer.
Referenced by CVC3::TheoryRecords::rewrite().
==> (REC_UPDATE (REC_LITERAL (f1 v1) ... (fi vi) ...) fi v') =(REC_LITERAL (f1 v1) ... (fi v') ...)
Implemented in CVC3::RecordsTheoremProducer.
Referenced by CVC3::TheoryRecords::rewrite().
From T|- e = e' return T|- AND (e.i = e'.i) for all i.
Implemented in CVC3::RecordsTheoremProducer.
Referenced by CVC3::TheoryRecords::assertFact().
From T|- NOT e=e' return T|- NOT AND (e.i = e'.i) for all i.
Implemented in CVC3::RecordsTheoremProducer.
Expand a record into a literal: |- e = (# f1:=e.f1, ..., fn:=e.fn #)
Implemented in CVC3::RecordsTheoremProducer.
Referenced by CVC3::TheoryRecords::computeModel(), and CVC3::TheoryRecords::setup().
Expand a tuple into a literal: |- e = (e.0, ..., e.n-1)
Implemented in CVC3::RecordsTheoremProducer.
Referenced by CVC3::TheoryRecords::computeModel(), and CVC3::TheoryRecords::setup().