CVC3::CoreSatAPI_implBase Class Reference

Inheritance diagram for CVC3::CoreSatAPI_implBase:

[legend]Collaboration diagram for CVC3::CoreSatAPI_implBase:

[legend]List of all members.

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.
  

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

(

)

[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:

• search_impl_base.cpp

---