CVCL::SearchSatTheoryAPI Class Reference

Inheritance diagram for CVCL::SearchSatTheoryAPI:

[legend]Collaboration diagram for CVCL::SearchSatTheoryAPI:

[legend]List of all members.

Public Member Functions

• SearchSatTheoryAPI (SearchSat *ss)
• ~SearchSatTheoryAPI ()
• void push ()

  Set a checkpoint for backtracking.
  

• void pop ()

  Restore most recent checkpoint.
  

• void assertLit (Lit l)

  Notify theory when a literal is set to true.
  

• DPLLT::ConsistentResult checkConsistent (Clause &c, bool fullEffort)
• Lit getImplication ()

  Get a literal that is implied by the current assignment.
  

• void getExplanation (Lit l, Clause &c)
• bool getNewClauses (CNF_Formula &cnf)

  Get new clauses from the theory.
  

Private Attributes

• ContextManager * d_cm
• SearchSat * d_ss

---

Detailed Description

Definition at line 44 of file search_sat.cpp.

---

Constructor & Destructor Documentation

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

Definition at line 48 of file search_sat.cpp.

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

Definition at line 50 of file search_sat.cpp.

---

Member Function Documentation

void CVCL::SearchSatTheoryAPI::push (   )  [inline, virtual]

Set a checkpoint for backtracking. Implements SAT::DPLLT::TheoryAPI. Definition at line 51 of file search_sat.cpp. References d_cm, and CVCL::ContextManager::push().

void CVCL::SearchSatTheoryAPI::pop (   )  [inline, virtual]

Restore most recent checkpoint. Implements SAT::DPLLT::TheoryAPI. Definition at line 52 of file search_sat.cpp. References d_cm, and CVCL::ContextManager::pop().

void CVCL::SearchSatTheoryAPI::assertLit (  Lit  l  )  [inline, virtual]

Notify theory when a literal is set to true. Implements SAT::DPLLT::TheoryAPI. Definition at line 53 of file search_sat.cpp. References CVCL::SearchSat::assertLit(), and d_ss.

DPLLT::ConsistentResult CVCL::SearchSatTheoryAPI::checkConsistent (  Clause &  c, bool  fullEffort )  [inline]

Definition at line 54 of file search_sat.cpp. References CVCL::SearchSat::checkConsistent(), and d_ss.

Lit CVCL::SearchSatTheoryAPI::getImplication (   )  [inline, virtual]

Get a literal that is implied by the current assignment. This is theory propagation. It can be called repeatedly and returns a Null literal when there are no more literals to propagate. It should only be called when the assignment is not known to be inconsistent. Implements SAT::DPLLT::TheoryAPI. Definition at line 56 of file search_sat.cpp. References d_ss, and CVCL::SearchSat::getImplication().

void CVCL::SearchSatTheoryAPI::getExplanation (  Lit  l, Clause &  c )  [inline]

Definition at line 57 of file search_sat.cpp. References d_ss, and CVCL::SearchSat::getExplanation().

bool CVCL::SearchSatTheoryAPI::getNewClauses (  CNF_Formula &  cnf  )  [inline, virtual]

Get new clauses from the theory. This is extended theory learning. Returns false if there are no new clauses to get. Otherwise, returns true and new clauses are added to cnf. Note that the new clauses (if any) are theory lemmas, i.e. clauses that are valid in the theory and not dependent on the current assignment. The clauses may contain new literals as well as literals that are true in the current assignment. Parameters: cnf  should be empty initially. Implements SAT::DPLLT::TheoryAPI. Definition at line 58 of file search_sat.cpp. References d_ss, and CVCL::SearchSat::getNewClauses().

---

Member Data Documentation

ContextManager* CVCL::SearchSatTheoryAPI::d_cm [private]

Definition at line 45 of file search_sat.cpp. Referenced by pop(), and push().

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

Definition at line 46 of file search_sat.cpp. Referenced by assertLit(), checkConsistent(), getExplanation(), getImplication(), and getNewClauses().

---

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

• search_sat.cpp

---