CVC3::CoreSatAPI_implBase Class Reference

Inherits CVC3::TheoryCore::CoreSatAPI.

Collaboration diagram for CVC3::CoreSatAPI_implBase:

Public Member Functions
	CoreSatAPI_implBase (SearchImplBase *se)
virtual	~CoreSatAPI_implBase ()
virtual void	addLemma (const Theorem &thm, int priority, bool atBottomScope)
	Add a new lemma derived by theory core.
virtual Theorem	addAssumption (const Expr &assump)
	Add an assumption to the set of assumptions in the current context.
virtual void	addSplitter (const Expr &e, int priority)
	Suggest a splitter to the Sat engine.
virtual 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
SearchImplBase *	d_se

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 ( )

inlinevirtual

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  )

inlinevirtual

Add a new lemma derived by theory core.

Implements CVC3::TheoryCore::CoreSatAPI.

Definition at line 45 of file search_impl_base.cpp.

virtual Theorem CVC3::CoreSatAPI_implBase::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 47 of file search_impl_base.cpp.

virtual void CVC3::CoreSatAPI_implBase::addSplitter ( const Expr &  e, int  priority  )

inlinevirtual

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.

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::VALID.

Member Data Documentation

SearchImplBase* CVC3::CoreSatAPI_implBase::d_se

private

Definition at line 41 of file search_impl_base.cpp.

---

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

• search_impl_base.cpp