dpllt_basic.cpp File Reference

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

#include "dpllt_basic.h"
#include "cnf.h"
#include "sat_api.h"
#include "exception.h"

Include dependency graph for dpllt_basic.cpp:

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

---

License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution.

---

Definition in file dpllt_basic.cpp.

---

Function Documentation

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

Definition at line 35 of file dpllt_basic.cpp.

References SAT::DPLLT::theoryAPI().

Referenced by SAT::DPLLTBasic::createManager().

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

Definition at line 50 of file dpllt_basic.cpp.

References SAT::DPLLTBasic::addNewClauses(), SAT::DPLLTBasic::cvc2SAT(), DebugAssert, SAT::DPLLT::decider(), SatSolver::Lit::id, IF_DEBUG, SAT::Lit::isNull(), and SAT::DPLLT::theoryAPI().

Referenced by SAT::DPLLTBasic::createManager().

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

Definition at line 98 of file dpllt_basic.cpp.

References SAT::DPLLTBasic::addNewClauses(), SatSolver::GetVarIndex(), SatSolver::Var::id, SAT::DPLLTBasic::satSolver(), SAT::DPLLT::theoryAPI(), and TRACE.

Referenced by SAT::DPLLTBasic::createManager().

static void SATDeductionHook

(

void *

cookie

)

[static]

Definition at line 117 of file dpllt_basic.cpp.

References SAT::DPLLTBasic::addNewClauses(), SAT::Lit::isNull(), SAT::CNF_Formula_Impl::reset(), and SAT::DPLLT::theoryAPI().

Referenced by SAT::DPLLTBasic::createManager().

---