CVC3
Public Member Functions | Private Attributes | List of all members
CVC3::SearchSatCoreSatAPI Class Reference

Inherits CVC3::TheoryCore::CoreSatAPI.

Collaboration diagram for CVC3::SearchSatCoreSatAPI:
Collaboration graph

Public Member Functions

 SearchSatCoreSatAPI (SearchSat *ss)
 
 ~SearchSatCoreSatAPI ()
 
void addLemma (const Theorem &thm, int priority, bool atBottomScope)
 Add a new lemma derived by theory core.
 
Theorem addAssumption (const Expr &assump)
 Add an assumption to the set of assumptions in the current context.
 
void addSplitter (const Expr &e, int priority)
 Suggest a splitter to the Sat engine.
 
bool check (const Expr &e)
 Check the validity of e in the current context.
 
- Public Member Functions inherited from CVC3::TheoryCore::CoreSatAPI
 CoreSatAPI ()
 
virtual ~CoreSatAPI ()
 

Private Attributes

SearchSatd_ss
 

Detailed Description

Definition at line 46 of file search_sat.cpp.

Constructor & Destructor Documentation

CVC3::SearchSatCoreSatAPI::SearchSatCoreSatAPI ( SearchSat ss)
inline

Definition at line 49 of file search_sat.cpp.

CVC3::SearchSatCoreSatAPI::~SearchSatCoreSatAPI ( )
inline

Definition at line 50 of file search_sat.cpp.

Member Function Documentation

void CVC3::SearchSatCoreSatAPI::addLemma ( const Theorem thm,
int  priority,
bool  atBottomScope 
)
inlinevirtual

Add a new lemma derived by theory core.

Implements CVC3::TheoryCore::CoreSatAPI.

Definition at line 51 of file search_sat.cpp.

Theorem CVC3::SearchSatCoreSatAPI::addAssumption ( const Expr assump)
inlinevirtual

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 53 of file search_sat.cpp.

void CVC3::SearchSatCoreSatAPI::addSplitter ( const Expr e,
int  priority 
)
inlinevirtual

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.

Implements CVC3::TheoryCore::CoreSatAPI.

Definition at line 55 of file search_sat.cpp.

bool CVC3::SearchSatCoreSatAPI::check ( const Expr e)
virtual

Check the validity of e in the current context.

Implements CVC3::TheoryCore::CoreSatAPI.

Definition at line 62 of file search_sat.cpp.

References CVC3::VALID.

Member Data Documentation

SearchSat* CVC3::SearchSatCoreSatAPI::d_ss
private

Definition at line 47 of file search_sat.cpp.


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