CVC3::CoreSatAPI_implBase Class Reference

Inheritance diagram for CVC3::CoreSatAPI_implBase:

Inheritance graph
[legend]
Collaboration diagram for CVC3::CoreSatAPI_implBase:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Attributes


Detailed Description

Definition at line 40 of file search_impl_base.cpp.


Constructor & Destructor Documentation

CVC3::CoreSatAPI_implBase::CoreSatAPI_implBase ( SearchImplBase se  )  [inline]

Definition at line 43 of file search_impl_base.cpp.

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

Definition at line 44 of file search_impl_base.cpp.


Member Function Documentation

virtual void CVC3::CoreSatAPI_implBase::addLemma ( const Theorem thm,
int  priority,
bool  atBottomScope 
) [inline, virtual]

Add a new lemma derived by theory core.

Implements CVC3::TheoryCore::CoreSatAPI.

Definition at line 45 of file search_impl_base.cpp.

References CVC3::SearchImplBase::addFact(), and d_se.

virtual Theorem CVC3::CoreSatAPI_implBase::addAssumption ( const Expr assump  )  [inline, virtual]

Add an assumption to the set of assumptions in the current context.

Assumptions have the form e |- e

Implements CVC3::TheoryCore::CoreSatAPI.

Definition at line 47 of file search_impl_base.cpp.

References d_se, and CVC3::SearchImplBase::newIntAssumption().

virtual void CVC3::CoreSatAPI_implBase::addSplitter ( const Expr e,
int  priority 
) [inline, virtual]

Suggest a splitter to the Sat engine.

Parameters:
e is a literal.
priority is between -10 and 10. A priority above 0 indicates that the splitter should be favored. A priority below 0 indicates that the splitter should be delayed.

Implements CVC3::TheoryCore::CoreSatAPI.

Definition at line 49 of file search_impl_base.cpp.

References CVC3::SearchImplBase::addSplitter(), and d_se.

bool CVC3::CoreSatAPI_implBase::check ( const Expr e  )  [virtual]

Check the validity of e in the current context.

Implements CVC3::TheoryCore::CoreSatAPI.

Definition at line 54 of file search_impl_base.cpp.

References CVC3::SearchImplBase::checkValid(), d_se, CVC3::TheoryCore::getCM(), CVC3::ContextManager::popto(), CVC3::ContextManager::push(), CVC3::ContextManager::scopeLevel(), CVC3::SearchEngine::theoryCore(), and CVC3::VALID.


Member Data Documentation

SearchImplBase* CVC3::CoreSatAPI_implBase::d_se [private]

Definition at line 41 of file search_impl_base.cpp.

Referenced by addAssumption(), addLemma(), addSplitter(), and check().


The documentation for this class was generated from the following file:
Generated on Wed Nov 18 16:17:51 2009 for CVC3 by  doxygen 1.5.2