CVCL::CoreSatAPI_implBase Class Reference

Inheritance diagram for CVCL::CoreSatAPI_implBase:

[legend]Collaboration diagram for CVCL::CoreSatAPI_implBase:

[legend]List of all members.

Public Member Functions

• CoreSatAPI_implBase (SearchImplBase *se)
• virtual ~CoreSatAPI_implBase ()
• virtual void addLemma (const Theorem &thm)

  Add a new lemma derived by theory core.
  

• virtual int getBottomScope ()

  Get the bottom-most scope where conflict clauses are still valid.
  

• 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.
  

Private Attributes

• SearchImplBase * d_se

---

Detailed Description

Definition at line 47 of file search_impl_base.cpp.

---

Constructor & Destructor Documentation

CVCL::CoreSatAPI_implBase::CoreSatAPI_implBase (  SearchImplBase *  se  )  [inline]

Definition at line 50 of file search_impl_base.cpp.

virtual CVCL::CoreSatAPI_implBase::~CoreSatAPI_implBase (   )  [inline, virtual]

Definition at line 51 of file search_impl_base.cpp.

---

Member Function Documentation

virtual void CVCL::CoreSatAPI_implBase::addLemma (  const Theorem &  thm  )  [inline, virtual]

Add a new lemma derived by theory core. Implements CVCL::TheoryCore::CoreSatAPI. Definition at line 52 of file search_impl_base.cpp. References CVCL::SearchImplBase::addFact(), and d_se.

virtual int CVCL::CoreSatAPI_implBase::getBottomScope (   )  [inline, virtual]

Get the bottom-most scope where conflict clauses are still valid. Implements CVCL::TheoryCore::CoreSatAPI. Definition at line 53 of file search_impl_base.cpp. References d_se, and CVCL::SearchImplBase::getBottomScope().

virtual Theorem CVCL::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 CVCL::TheoryCore::CoreSatAPI. Definition at line 54 of file search_impl_base.cpp. References d_se, and CVCL::SearchImplBase::newIntAssumption().

virtual void CVCL::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 CVCL::TheoryCore::CoreSatAPI. Definition at line 56 of file search_impl_base.cpp. References CVCL::SearchImplBase::addSplitter(), and d_se.

---

Member Data Documentation

SearchImplBase* CVCL::CoreSatAPI_implBase::d_se [private]

Definition at line 48 of file search_impl_base.cpp. Referenced by addAssumption(), addLemma(), addSplitter(), and getBottomScope().

---

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

• search_impl_base.cpp

---