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 (CNF_Formula &cnf, bool fullEffort)
Check consistency of the current assignment.
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, CNF_Formula &cnf)
Get an explanation for a literal that was implied.
bool getNewClauses (CNF_Formula &cnf)
Get new clauses from the theory.

Private Attributes

ContextManager * d_cm
SearchSat * d_ss

Detailed Description

Definition at line 72 of file search_sat.cpp.

Constructor & Destructor Documentation

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

Definition at line 76 of file search_sat.cpp.

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

Definition at line 78 of file search_sat.cpp.

Member Function Documentation

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

Set a checkpoint for backtracking.

Implements SAT::DPLLT::DPLLT::TheoryAPI.

Definition at line 79 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::DPLLT::TheoryAPI.

Definition at line 80 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::DPLLT::TheoryAPI.

Definition at line 81 of file search_sat.cpp.

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

SAT::DPLLT::ConsistentResult CVC3::SearchSatTheoryAPI::checkConsistent	(	CNF_Formula &	cnf,
		bool	fullEffort
	)			`[inline, virtual]`

Check consistency of the current assignment.

The result is either INCONSISTENT, MAYBE_CONSISTENT, or CONSISTENT Most of the time, fullEffort should be false, and the result will most likely be either INCONSISTENT or MAYBE_CONSISTENT. To force a full check, set fullEffort to true. When fullEffort is set to true, the only way the result can be MAYBE_CONSISTENT is if there are new clauses to get (via getNewClauses).

Parameters:

	cnf	should be empty initially. If INCONSISTENT is returned, then cnf will contain one or more clauses ruling out the current assignment when it returns. Otherwise, cnf is unchanged.
	fullEffort	true for a full check, false for a fast check

Implements SAT::DPLLT::DPLLT::TheoryAPI.

Definition at line 82 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::DPLLT::TheoryAPI.

Definition at line 84 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::DPLLT::TheoryAPI.

Definition at line 85 of file search_sat.cpp.

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

void CVC3::SearchSatTheoryAPI::getExplanation	(	Lit	l,
		CNF_Formula &	c
	)			`[inline, virtual]`

Get an explanation for a literal that was implied.

Given a literal l that is true in the current assignment as a result of an earlier call to getImplication(), this method returns a set of clauses which justifies the propagation of that literal. The clauses will contain the literal l as well as other literals that are in the current assignment. The clauses are such that they would have propagated l via unit propagation at the time getImplication() was called.

Parameters:

	l	the literal
	c	should be empty initially.

Implements SAT::DPLLT::DPLLT::TheoryAPI.

Definition at line 86 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::DPLLT::TheoryAPI.

Definition at line 87 of file search_sat.cpp.

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

Member Data Documentation

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

Definition at line 73 of file search_sat.cpp.

Referenced by pop(), and push().

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

Definition at line 74 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