CVC3  2.4.1
Public Member Functions | List of all members
SAT::DPLLT::TheoryAPI Class Reference

#include <dpllt.h>

Inheritance diagram for SAT::DPLLT::TheoryAPI:
CVC3::SearchSatTheoryAPI

Public Member Functions

 TheoryAPI ()
virtual ~TheoryAPI ()
virtual void push ()=0
 Set a checkpoint for backtracking.
virtual void pop ()=0
 Restore most recent checkpoint.
virtual void assertLit (Lit l)=0
 Notify theory when a literal is set to true.
virtual ConsistentResult checkConsistent (CNF_Formula &cnf, bool fullEffort)=0
 Check consistency of the current assignment.
virtual bool outOfResources ()=0
 Check if the work budget has been exceeded.
virtual Lit getImplication ()=0
 Get a literal that is implied by the current assignment.
virtual void getExplanation (Lit l, CNF_Formula &c)=0
 Get an explanation for a literal that was implied.
virtual bool getNewClauses (CNF_Formula &cnf)=0
 Get new clauses from the theory.

Detailed Description

Definition at line 28 of file dpllt.h.

Constructor & Destructor Documentation

SAT::DPLLT::TheoryAPI::TheoryAPI ( )
inline

Definition at line 30 of file dpllt.h.

virtual SAT::DPLLT::TheoryAPI::~TheoryAPI ( )
inlinevirtual

Definition at line 31 of file dpllt.h.

Member Function Documentation

virtual void SAT::DPLLT::TheoryAPI::push ( )
pure virtual
virtual void SAT::DPLLT::TheoryAPI::pop ( )
pure virtual
virtual void SAT::DPLLT::TheoryAPI::assertLit ( Lit  l)
pure virtual
virtual ConsistentResult SAT::DPLLT::TheoryAPI::checkConsistent ( CNF_Formula cnf,
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).

Parameters
cnfshould 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.
fullEfforttrue for a full check, false for a fast check

Implemented in CVC3::SearchSatTheoryAPI.

Referenced by SATAssignmentHook(), SATDecisionHook(), and MiniSat::Solver::search().

virtual bool SAT::DPLLT::TheoryAPI::outOfResources ( )
pure 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.

Implemented in CVC3::SearchSatTheoryAPI.

Referenced by SATDecisionHook(), and MiniSat::Solver::search().

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 CVC3::SearchSatTheoryAPI.

Referenced by MiniSat::Solver::push(), SATDeductionHook(), and MiniSat::Solver::search().

virtual void SAT::DPLLT::TheoryAPI::getExplanation ( Lit  l,
CNF_Formula 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 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
lthe literal
cshould be empty initially.

Implemented in CVC3::SearchSatTheoryAPI.

Referenced by MiniSat::Solver::push(), SATDeductionHook(), and MiniSat::Solver::search().

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.

Parameters
cnfshould be empty initially.

Implemented in CVC3::SearchSatTheoryAPI.

Referenced by MiniSat::Solver::push(), SATDecisionHook(), SATDeductionHook(), and MiniSat::Solver::search().


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