Public Member Functions | Private Member Functions | Private Attributes

CVC3::CommonTheoremProducer Class Reference

#include <common_theorem_producer.h>

Inheritance diagram for CVC3::CommonTheoremProducer:
CVC3::CommonProofRules CVC3::TheoremProducer

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


Detailed Description

Definition at line 40 of file common_theorem_producer.h.


Constructor & Destructor Documentation

CommonTheoremProducer::CommonTheoremProducer ( TheoremManager tm  ) 

Definition at line 40 of file common_theorem_producer.cpp.

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

Definition at line 60 of file common_theorem_producer.h.


Member Function Documentation

void CommonTheoremProducer::findITE ( const Expr e,
Expr condition,
Expr thenpart,
Expr elsepart 
) [private]
Theorem CommonTheoremProducer::assumpRule ( const Expr a,
int  scope = -1 
)
Theorem CommonTheoremProducer::reflexivityRule ( const Expr a  ) 
Theorem CommonTheoremProducer::andIntro ( const Theorem e1,
const Theorem e2 
)

e1, e2 ==> AND(e1, e2)

Definition at line 733 of file common_theorem_producer.cpp.

Theorem CommonTheoremProducer::andIntro ( const std::vector< Theorem > &  es  ) 
Expr CommonTheoremProducer::skolemize ( const Expr e  ) 
Theorem CommonTheoremProducer::trueTheorem (  ) 
Theorem CommonTheoremProducer::rewriteAnd ( const Theorem e  ) 

Definition at line 1286 of file common_theorem_producer.cpp.

References CVC3::Theorem::getExpr(), iffMP(), and rewriteAnd().

Theorem CommonTheoremProducer::rewriteOr ( const Theorem e  ) 

Definition at line 1292 of file common_theorem_producer.cpp.

References CVC3::Theorem::getExpr(), iffMP(), and rewriteOr().

std::vector<Theorem>& CVC3::CommonTheoremProducer::getSkolemAxioms (  )  [inline]

Definition at line 126 of file common_theorem_producer.h.

References d_skolem_axioms.

void CVC3::CommonTheoremProducer::clearSkolemAxioms (  )  [inline]

Definition at line 127 of file common_theorem_producer.h.

References d_skolem_axioms.


Member Data Documentation

Mapping of e to "|- e = v" for fresh Skolem vars v.

Definition at line 53 of file common_theorem_producer.h.

Referenced by varIntroSkolem().


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