SAT::DPLLT::TheoryAPI Class Reference

#include <dpllt.h>

Inheritance diagram for SAT::DPLLT::TheoryAPI:

Inheritance graph
List of all members.

Public Member Functions

Detailed Description

Definition at line 25 of file dpllt.h.

Constructor & Destructor Documentation

SAT::DPLLT::TheoryAPI::TheoryAPI  )  [inline]

Definition at line 27 of file dpllt.h.

virtual SAT::DPLLT::TheoryAPI::~TheoryAPI  )  [inline, virtual]

Definition at line 28 of file dpllt.h.

Member Function Documentation

virtual void SAT::DPLLT::TheoryAPI::push  )  [pure virtual]

Set a checkpoint for backtracking.

Implemented in CVCL::SearchSatTheoryAPI.

virtual void SAT::DPLLT::TheoryAPI::pop  )  [pure virtual]

Restore most recent checkpoint.

Implemented in CVCL::SearchSatTheoryAPI.

virtual void SAT::DPLLT::TheoryAPI::assertLit Lit  l  )  [pure virtual]

Notify theory when a literal is set to true.

Implemented in CVCL::SearchSatTheoryAPI.

virtual ConsistentResult SAT::DPLLT::TheoryAPI::checkConsistent Clause c,
bool  fullEffort
[pure 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).

c should be empty initially. If INCONSISTENT is returned, then c will contain a conflict clause when it returns. Otherwise, c is unchanged.

virtual Lit SAT::DPLLT::TheoryAPI::getImplication  )  [pure 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.

Implemented in CVCL::SearchSatTheoryAPI.

virtual void SAT::DPLLT::TheoryAPI::getExplanation Lit  l,
Clause c
[pure 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 clause which justifies the propagation of that literal. The clause will contain the literal l as well as other literals that are in the current assignment. The clause is such that it would have caused a unit propagation at the time getImplication() was called.

c should be empty initially.

virtual bool SAT::DPLLT::TheoryAPI::getNewClauses CNF_Formula cnf  )  [pure 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.

cnf should be empty initially.

Implemented in CVCL::SearchSatTheoryAPI.

The documentation for this class was generated from the following file:
Generated on Thu Apr 13 16:57:46 2006 for CVC Lite by  doxygen 1.4.4