Public Member Functions

CVC3::UFProofRules Class Reference

#include <uf_proof_rules.h>

Inherited by CVC3::UFTheoremProducer.

List of all members.

Public Member Functions

Detailed Description

Definition at line 32 of file uf_proof_rules.h.

Constructor & Destructor Documentation

virtual CVC3::UFProofRules::~UFProofRules ( ) [inline, virtual]

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: