CVC3::SearchSatTheoryAPI Class Reference

Inheritance diagram for CVC3::SearchSatTheoryAPI:

Inheritance graph
[legend]
Collaboration diagram for CVC3::SearchSatTheoryAPI:

Collaboration graph
[legend]

List of all members.

Public Member Functions

Private Attributes


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

Definition at line 73 of file search_sat.cpp.

Referenced by pop(), and push().


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

Generated on Thu Oct 15 22:25:04 2009 for CVC3 by  doxygen 1.5.8