dpllt_basic.cpp File Reference

Basic implementation of dpllt module using generic sat solver. More...

Go to the source code of this file.

Functions

• static void SATDLevelHook (void *cookie, int change)
• static SatSolver::Lit SATDecisionHook (void *cookie, bool *done)
• static void SATAssignmentHook (void *cookie, SatSolver::Var var, int value)
• static void SATDeductionHook (void *cookie)

---

Detailed Description

Basic implementation of dpllt module using generic sat solver.

Author: Clark Barrett

Created: Mon Dec 12 19:09:43 2005

Definition in file dpllt_basic.cpp.

---

Function Documentation

static void SATDLevelHook (  void *  cookie, int  change )  [static]

Definition at line 24 of file dpllt_basic.cpp. References SAT::DPLLTBasic::popScopes(), and SAT::DPLLT::theoryAPI(). Referenced by SAT::DPLLTBasic::createManager().

static SatSolver::Lit SATDecisionHook (  void *  cookie, bool *  done )  [static]

Definition at line 37 of file dpllt_basic.cpp. References SAT::DPLLTBasic::addNewClause(), SAT::DPLLTBasic::addNewClauses(), SAT::DPLLTBasic::cvcl2SAT(), SAT::DPLLT::decider(), SAT::DPLLT::INCONSISTENT, SAT::Lit::isNull(), SAT::DPLLT::MAYBE_CONSISTENT, and SAT::DPLLT::theoryAPI(). Referenced by SAT::DPLLTBasic::createManager().

static void SATAssignmentHook (  void *  cookie, SatSolver::Var  var, int  value )  [static]

Definition at line 74 of file dpllt_basic.cpp. References SAT::DPLLTBasic::addNewClause(), SatSolver::GetVarIndex(), SAT::DPLLT::INCONSISTENT, SAT::DPLLTBasic::satSolver(), and SAT::DPLLT::theoryAPI(). Referenced by SAT::DPLLTBasic::createManager().

static void SATDeductionHook (  void *  cookie  )  [static]

Definition at line 91 of file dpllt_basic.cpp. References SAT::DPLLTBasic::addNewClause(), SAT::DPLLTBasic::addNewClauses(), SAT::Lit::isNull(), and SAT::DPLLT::theoryAPI(). Referenced by SAT::DPLLTBasic::createManager().

---