CVC3
2.4.1
|
#include <records_proof_rules.h>
Definition at line 28 of file records_proof_rules.h.
virtual CVC3::RecordsProofRules::~RecordsProofRules | ( | ) | [inline, virtual] |
< Destructor
Definition at line 31 of file records_proof_rules.h.
virtual Theorem CVC3::RecordsProofRules::rewriteLitSelect | ( | const Expr & | e | ) | [pure virtual] |
==> (REC_LITERAL (f1 v1) ... (fi vi) ...).fi = vi
Implemented in CVC3::RecordsTheoremProducer.
Referenced by CVC3::TheoryRecords::rewrite().
virtual Theorem CVC3::RecordsProofRules::rewriteUpdateSelect | ( | const Expr & | e | ) | [pure virtual] |
==> (REC_SELECT (REC_UPDATE e fi vi) fi) = vi
Implemented in CVC3::RecordsTheoremProducer.
Referenced by CVC3::TheoryRecords::rewrite().
virtual Theorem CVC3::RecordsProofRules::rewriteLitUpdate | ( | const Expr & | e | ) | [pure virtual] |
==> (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().
virtual Theorem CVC3::RecordsProofRules::expandEq | ( | const Theorem & | eqThrm | ) | [pure virtual] |
From T|- e = e' return T|- AND (e.i = e'.i) for all i.
Implemented in CVC3::RecordsTheoremProducer.
Referenced by CVC3::TheoryRecords::assertFact().
virtual Theorem CVC3::RecordsProofRules::expandNeq | ( | const Theorem & | neqThrm | ) | [pure virtual] |
From T|- NOT e=e' return T|- NOT AND (e.i = e'.i) for all i.
Implemented in CVC3::RecordsTheoremProducer.
virtual Theorem CVC3::RecordsProofRules::expandRecord | ( | const Expr & | e | ) | [pure virtual] |
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().
virtual Theorem CVC3::RecordsProofRules::expandTuple | ( | const Expr & | e | ) | [pure virtual] |
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().