CVCL::TheoryCore::CoreSatAPI Class Reference

#include <theory_core.h>

Inheritance diagram for CVCL::TheoryCore::CoreSatAPI:

[legend]List of all members.

Public Member Functions

• CoreSatAPI ()
• virtual ~CoreSatAPI ()
• virtual void addLemma (const Theorem &thm)=0

  Add a new lemma derived by theory core.
  

• virtual int getBottomScope ()=0

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

• virtual Theorem addAssumption (const Expr &assump)=0

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

• virtual void addSplitter (const Expr &e, int priority)=0

  Suggest a splitter to the Sat engine.
  

---

Detailed Description

Definition at line 205 of file theory_core.h.

---

Constructor & Destructor Documentation

CVCL::TheoryCore::CoreSatAPI::CoreSatAPI (   )  [inline]

Definition at line 207 of file theory_core.h.

virtual CVCL::TheoryCore::CoreSatAPI::~CoreSatAPI (   )  [inline, virtual]

Definition at line 208 of file theory_core.h.

---

Member Function Documentation

virtual void CVCL::TheoryCore::CoreSatAPI::addLemma (  const Theorem &  thm  )  [pure virtual]

Add a new lemma derived by theory core. Implemented in CVCL::CoreSatAPI_implBase, and CVCL::SearchSatCoreSatAPI. Referenced by TheoryCore::processFactQueue().

virtual int CVCL::TheoryCore::CoreSatAPI::getBottomScope (   )  [pure virtual]

Get the bottom-most scope where conflict clauses are still valid. Implemented in CVCL::CoreSatAPI_implBase, and CVCL::SearchSatCoreSatAPI.

virtual Theorem CVCL::TheoryCore::CoreSatAPI::addAssumption (  const Expr &  assump  )  [pure virtual]

Add an assumption to the set of assumptions in the current context. Assumptions have the form e |- e Implemented in CVCL::CoreSatAPI_implBase, and CVCL::SearchSatCoreSatAPI. Referenced by TheoryCore::assignValue().

virtual void CVCL::TheoryCore::CoreSatAPI::addSplitter (  const Expr &  e, int  priority )  [pure 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. Implemented in CVCL::CoreSatAPI_implBase, and CVCL::SearchSatCoreSatAPI.

---

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

• theory_core.h

---