CVC3
|
#include <uf_proof_rules.h>
Inherited by CVC3::UFTheoremProducer.
Public Member Functions | |
virtual | ~UFProofRules () |
virtual Theorem | relToClosure (const Theorem &rel)=0 |
virtual Theorem | relTrans (const Theorem &t1, const Theorem &t2)=0 |
virtual Theorem | applyLambda (const Expr &e)=0 |
Beta reduction: |- (lambda x. f(x))(arg) = f(arg) | |
virtual Theorem | rewriteOpDef (const Expr &e)=0 |
Replace LETDECL in the operator with the definition. | |
Definition at line 32 of file uf_proof_rules.h.
|
inlinevirtual |
Definition at line 35 of file uf_proof_rules.h.
Implemented in CVC3::UFTheoremProducer.
Referenced by CVC3::TheoryUF::assertFact(), and CVC3::TheoryUF::update().
|
pure virtual |
Implemented in CVC3::UFTheoremProducer.
Referenced by CVC3::TheoryUF::assertFact().
Beta reduction: |- (lambda x. f(x))(arg) = f(arg)
Implemented in CVC3::UFTheoremProducer.
Referenced by CVC3::TheoryUF::checkSat(), and CVC3::TheoryUF::rewrite().
Replace LETDECL in the operator with the definition.
Implemented in CVC3::UFTheoremProducer.