CVCL::SearchSatCoreSatAPI Class Reference

Inheritance diagram for CVCL::SearchSatCoreSatAPI:

[legend]Collaboration diagram for CVCL::SearchSatCoreSatAPI:

[legend]List of all members.

Public Member Functions

• SearchSatCoreSatAPI (SearchSat *ss)
• ~SearchSatCoreSatAPI ()
• void addLemma (const Theorem &thm)

  Add a new lemma derived by theory core.
  

• int getBottomScope ()

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

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

Private Attributes

• SearchSat * d_ss

---

Detailed Description

Definition at line 30 of file search_sat.cpp.

---

Constructor & Destructor Documentation

CVCL::SearchSatCoreSatAPI::SearchSatCoreSatAPI (  SearchSat *  ss  )  [inline]

Definition at line 33 of file search_sat.cpp.

CVCL::SearchSatCoreSatAPI::~SearchSatCoreSatAPI (   )  [inline]

Definition at line 34 of file search_sat.cpp.

---

Member Function Documentation

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

Add a new lemma derived by theory core. Implements CVCL::TheoryCore::CoreSatAPI. Definition at line 35 of file search_sat.cpp. References CVCL::SearchSat::addLemma(), and d_ss.

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

Get the bottom-most scope where conflict clauses are still valid. Implements CVCL::TheoryCore::CoreSatAPI. Definition at line 36 of file search_sat.cpp. References d_ss, and CVCL::SearchSat::getBottomScope().

Theorem CVCL::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 Implements CVCL::TheoryCore::CoreSatAPI. Definition at line 37 of file search_sat.cpp. References d_ss, and CVCL::SearchSat::newUserAssumption().

void CVCL::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. Implements CVCL::TheoryCore::CoreSatAPI. Definition at line 39 of file search_sat.cpp. References CVCL::SearchSat::addSplitter(), and d_ss.

---

Member Data Documentation

SearchSat* CVCL::SearchSatCoreSatAPI::d_ss [private]

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

---

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

• search_sat.cpp

---