CVC3::SearchSatTheoryAPI Class Reference

Inheritance diagram for CVC3::SearchSatTheoryAPI:

[legend]Collaboration diagram for CVC3::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.
  

• SAT::DPLLT::ConsistentResult checkConsistent (Clause &c, bool fullEffort)
• bool outOfResources ()

  Check if the work budget has been exceeded.
  

• 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 71 of file search_sat.cpp.

---

Constructor & Destructor Documentation

CVC3::SearchSatTheoryAPI::SearchSatTheoryAPI

(

SearchSat *

ss

)

[inline]

Definition at line 75 of file search_sat.cpp.

CVC3::SearchSatTheoryAPI::~SearchSatTheoryAPI

(

)

[inline]

Definition at line 77 of file search_sat.cpp.

---

Member Function Documentation

void CVC3::SearchSatTheoryAPI::push

(

)

[inline, virtual]

Set a checkpoint for backtracking.

Implements SAT::DPLLT::TheoryAPI.

Definition at line 78 of file search_sat.cpp.

References d_cm, and CVC3::ContextManager::push().

void CVC3::SearchSatTheoryAPI::pop

(

)

[inline, virtual]

Restore most recent checkpoint.

Implements SAT::DPLLT::TheoryAPI.

Definition at line 79 of file search_sat.cpp.

References d_cm, and CVC3::ContextManager::pop().

void CVC3::SearchSatTheoryAPI::assertLit

(

Lit

l

)

[inline, virtual]

Notify theory when a literal is set to true.

Implements SAT::DPLLT::TheoryAPI.

Definition at line 80 of file search_sat.cpp.

References CVC3::SearchSat::assertLit(), and d_ss.

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

Definition at line 81 of file search_sat.cpp.

References CVC3::SearchSat::checkConsistent(), and d_ss.

bool CVC3::SearchSatTheoryAPI::outOfResources

(

)

[inline, virtual]

Check if the work budget has been exceeded.

If true, it means that the engine should quit and return ABORT. Otherwise, it should proceed normally. This should be checked regularly.

Implements SAT::DPLLT::TheoryAPI.

Definition at line 83 of file search_sat.cpp.

References d_ss, CVC3::TheoryCore::outOfResources(), and CVC3::SearchEngine::theoryCore().

Lit CVC3::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 84 of file search_sat.cpp.

References d_ss, and CVC3::SearchSat::getImplication().

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

Definition at line 85 of file search_sat.cpp.

References d_ss, and CVC3::SearchSat::getExplanation().

bool CVC3::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 86 of file search_sat.cpp.

References d_ss, and CVC3::SearchSat::getNewClauses().

---

Member Data Documentation

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

Definition at line 72 of file search_sat.cpp.

Referenced by pop(), and push().

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

Definition at line 73 of file search_sat.cpp.

Referenced by assertLit(), checkConsistent(), getExplanation(), getImplication(), getNewClauses(), and outOfResources().

---

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

• search_sat.cpp

---