Public Member Functions | Private Member Functions | Private Attributes

CVC3::SearchEngineTheoremProducer Class Reference

#include <search_theorem_producer.h>

Inheritance diagram for CVC3::SearchEngineTheoremProducer:
CVC3::SearchEngineRules CVC3::TheoremProducer

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


Detailed Description

Definition at line 32 of file search_theorem_producer.h.


Constructor & Destructor Documentation

SearchEngineTheoremProducer::SearchEngineTheoremProducer ( TheoremManager tm  ) 

Definition at line 46 of file search_theorem_producer.cpp.

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

Definition at line 47 of file search_theorem_producer.h.


Member Function Documentation

void SearchEngineTheoremProducer::verifyConflict ( const Theorem thm,
TheoremMap m 
) [private]

Definition at line 171 of file search_theorem_producer.cpp.

References CHECK_SOUND, and CVC3::Theorem::getAssumptionsRef().

Referenced by conflictClause().

void SearchEngineTheoremProducer::checkSoundNoSkolems ( const Expr e,
ExprMap< bool > &  visited,
const ExprMap< bool > &  skolems 
) [private]
void SearchEngineTheoremProducer::checkSoundNoSkolems ( const Theorem t,
ExprMap< bool > &  visited,
const ExprMap< bool > &  skolems 
) [private]
Theorem SearchEngineTheoremProducer::eliminateSkolemAxioms ( const Theorem tFalse,
const std::vector< Theorem > &  delta 
) [virtual]

Eliminate skolem axioms: Gamma, Delta |- false => Gamma|- false where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)} and gamma does not contain any of the skolem constants c.

Definition at line 433 of file search_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, checkSoundNoSkolems(), CVC3::Theorem::clearAllFlags(), CVC3::TheoremProducer::d_em, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isFalse(), CVC3::ExprManager::newLeafExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

void SearchEngineTheoremProducer::propAndrLRT ( const Theorem andr_th,
const Theorem a_th,
Theorem l_th,
Theorem r_th 
) [virtual]
Theorem SearchEngineTheoremProducer::andCNFRule ( const Theorem thm  ) 

Definition at line 1139 of file search_theorem_producer.cpp.

References CVC3::AND, and opCNFRule().

Theorem SearchEngineTheoremProducer::orCNFRule ( const Theorem thm  ) 

Definition at line 1144 of file search_theorem_producer.cpp.

References opCNFRule(), and CVC3::OR.

Theorem SearchEngineTheoremProducer::impCNFRule ( const Theorem thm  ) 

Definition at line 1149 of file search_theorem_producer.cpp.

References CVC3::IMPLIES, and opCNFRule().

Theorem SearchEngineTheoremProducer::iffCNFRule ( const Theorem thm  ) 

Definition at line 1154 of file search_theorem_producer.cpp.

References CVC3::IFF, and opCNFRule().

Theorem SearchEngineTheoremProducer::iteCNFRule ( const Theorem thm  ) 

Definition at line 1159 of file search_theorem_producer.cpp.

References CVC3::ITE, and opCNFRule().

Expr SearchEngineTheoremProducer::convertToCNF ( const Expr v,
const Expr phi 
) [private]
Expr SearchEngineTheoremProducer::findInLocalCache ( const Expr i,
ExprMap< Expr > &  localCache,
std::vector< Expr > &  boundVars 
) [private]

checks if phi has v in local cache of opCNFRule, if so reuse v.

similarly for ( ! ... ! (phi))

Definition at line 1362 of file search_theorem_producer.cpp.

References CVC3::TheoremProducer::d_em, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getType(), IF_DEBUG, CVC3::Expr::iffExpr(), CVC3::Expr::isNot(), CVC3::ExprManager::newBoundVarExpr(), CVC3::Expr::toString(), and CVC3::TRACE.

Referenced by opCNFRule().


Member Data Documentation


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