CVC3
Public Member Functions

CVC3::TheoryCore::CoreSatAPI Class Reference

Interface class for callbacks to SAT from Core. More...

#include <theory_core.h>

Inherited by CVC3::CoreSatAPI_implBase, and CVC3::SearchSatCoreSatAPI.

List of all members.

Public Member Functions


Detailed Description

Interface class for callbacks to SAT from Core.

Author: Clark Barrett

Created: Mon Dec 5 18:42:15 2005

Definition at line 219 of file theory_core.h.


Constructor & Destructor Documentation

CVC3::TheoryCore::CoreSatAPI::CoreSatAPI ( ) [inline]

Definition at line 221 of file theory_core.h.

virtual CVC3::TheoryCore::CoreSatAPI::~CoreSatAPI ( ) [inline, virtual]

Definition at line 222 of file theory_core.h.


Member Function Documentation

virtual void CVC3::TheoryCore::CoreSatAPI::addLemma ( const Theorem thm,
int  priority = 0,
bool  atBottomScope = false 
) [pure virtual]

Add a new lemma derived by theory core.

Implemented in CVC3::CoreSatAPI_implBase, and CVC3::SearchSatCoreSatAPI.

virtual Theorem CVC3::TheoryCore::CoreSatAPI::addAssumption ( const Expr assump) [pure virtual]

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

Assumptions have the form e |- e

Implemented in CVC3::CoreSatAPI_implBase, and CVC3::SearchSatCoreSatAPI.

Referenced by CVC3::TheoryCore::assignValue().

virtual void CVC3::TheoryCore::CoreSatAPI::addSplitter ( const Expr e,
int  priority 
) [pure virtual]

Suggest a splitter to the Sat engine.

Parameters:
eis a literal.
priorityis 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.

Implemented in CVC3::CoreSatAPI_implBase, and CVC3::SearchSatCoreSatAPI.

virtual bool CVC3::TheoryCore::CoreSatAPI::check ( const Expr e) [pure virtual]

Check the validity of e in the current context.

Implemented in CVC3::CoreSatAPI_implBase, and CVC3::SearchSatCoreSatAPI.


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