CVC3
Public Member Functions | Private Attributes | List of all members
CVC3::SearchSatTheoryAPI Class Reference

Inherits SAT::DPLLT::TheoryAPI.

Collaboration diagram for CVC3::SearchSatTheoryAPI:
Collaboration graph

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.
 
- Public Member Functions inherited from SAT::DPLLT::TheoryAPI
 TheoryAPI ()
 
virtual ~TheoryAPI ()
 

Private Attributes

ContextManagerd_cm
 
SearchSatd_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 ( )
inlinevirtual

Set a checkpoint for backtracking.

Implements SAT::DPLLT::TheoryAPI.

Definition at line 79 of file search_sat.cpp.

void CVC3::SearchSatTheoryAPI::pop ( )
inlinevirtual

Restore most recent checkpoint.

Implements SAT::DPLLT::TheoryAPI.

Definition at line 80 of file search_sat.cpp.

void CVC3::SearchSatTheoryAPI::assertLit ( Lit  l)
inlinevirtual

Notify theory when a literal is set to true.

Implements SAT::DPLLT::TheoryAPI.

Definition at line 81 of file search_sat.cpp.

SAT::DPLLT::ConsistentResult CVC3::SearchSatTheoryAPI::checkConsistent ( CNF_Formula cnf,
bool  fullEffort 
)
inlinevirtual

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

Implements SAT::DPLLT::TheoryAPI.

Definition at line 82 of file search_sat.cpp.

bool CVC3::SearchSatTheoryAPI::outOfResources ( )
inlinevirtual

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

Lit CVC3::SearchSatTheoryAPI::getImplication ( )
inlinevirtual

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

void CVC3::SearchSatTheoryAPI::getExplanation ( Lit  l,
CNF_Formula c 
)
inlinevirtual

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.

Implements SAT::DPLLT::TheoryAPI.

Definition at line 86 of file search_sat.cpp.

bool CVC3::SearchSatTheoryAPI::getNewClauses ( CNF_Formula cnf)
inlinevirtual

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.

Implements SAT::DPLLT::TheoryAPI.

Definition at line 87 of file search_sat.cpp.

Member Data Documentation

ContextManager* CVC3::SearchSatTheoryAPI::d_cm
private

Definition at line 73 of file search_sat.cpp.

SearchSat* CVC3::SearchSatTheoryAPI::d_ss
private

Definition at line 74 of file search_sat.cpp.


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