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.

Private Attributes

Definition at line 46 of file search_sat.cpp.

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.

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

Add a new lemma derived by theory core.

Definition at line 51 of file search_sat.cpp.

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

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

Assumptions have the form e |- e

Definition at line 53 of file search_sat.cpp.

void CVC3::SearchSatCoreSatAPI::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.

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.

Definition at line 62 of file search_sat.cpp.

References CVC3::VALID.