CVC3  2.4.1
Public Member Functions | List of all members
CVC3::UFProofRules Class Reference

#include <uf_proof_rules.h>

Inheritance diagram for CVC3::UFProofRules:
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.

Detailed Description

Definition at line 32 of file uf_proof_rules.h.

Constructor & Destructor Documentation

virtual CVC3::UFProofRules::~UFProofRules ( )
inlinevirtual

Definition at line 35 of file uf_proof_rules.h.

Member Function Documentation

virtual Theorem CVC3::UFProofRules::relToClosure ( const Theorem rel)
pure virtual
virtual Theorem CVC3::UFProofRules::relTrans ( const Theorem t1,
const Theorem t2 
)
pure virtual

Implemented in CVC3::UFTheoremProducer.

Referenced by CVC3::TheoryUF::assertFact().

virtual Theorem CVC3::UFProofRules::applyLambda ( const Expr e)
pure virtual

Beta reduction: |- (lambda x. f(x))(arg) = f(arg)

Implemented in CVC3::UFTheoremProducer.

Referenced by CVC3::TheoryUF::checkSat(), and CVC3::TheoryUF::rewrite().

virtual Theorem CVC3::UFProofRules::rewriteOpDef ( const Expr e)
pure virtual

Replace LETDECL in the operator with the definition.

Implemented in CVC3::UFTheoremProducer.


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