dpllt_minisat.cpp File Reference

Implementation of dpllt module using MiniSat. More...

#include "dpllt_minisat.h"
#include "minisat_solver.h"
#include "sat_proof.h"
#include "theorem_producer.h"
#include "exception.h"

Go to the source code of this file.

Defines

• #define _CVC3_TRUSTED_

Functions

• CVC3::Proof generateSatProof (SAT::SatProofNode *node, CNF_Manager *cnfManager, TheoremProducer *thmProducer)
• void printSatProof (SAT::SatProofNode *node)

---

Detailed Description

Implementation of dpllt module using MiniSat.

Author: Alexander Fuchs

Created: Fri Sep 08 11:04:00 2006

---

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_minisat.cpp.

---

Define Documentation

#define _CVC3_TRUSTED_

Definition at line 21 of file dpllt_minisat.cpp.

---

Function Documentation

CVC3::Proof generateSatProof	(	SAT::SatProofNode *	node,
		CNF_Manager *	cnfManager,
		TheoremProducer *	thmProducer
	)

Definition at line 258 of file dpllt_minisat.cpp.

References SAT::CNF_Manager::concreteLit(), DebugAssert, std::endl(), SAT::SatProofNode::getLeaf(), SAT::SatProofNode::getLeftParent(), SAT::SatProofNode::getLit(), SAT::SatProofNode::getNodeProof(), CVC3::Theorem::getProof(), SAT::SatProofNode::getRightParent(), SAT::SatProofNode::hasNodeProof(), SAT::SatProofNode::isLeaf(), CVC3::Theorem::isNull(), CVC3::TheoremProducer::newPf(), and SAT::SatProofNode::setNodeProof().

Referenced by SAT::DPLLTMiniSat::getSatProof().

void printSatProof

(

SAT::SatProofNode *

node

)

Definition at line 330 of file dpllt_minisat.cpp.

References std::endl(), SAT::SatProofNode::getLeaf(), SAT::SatProofNode::getLeftParent(), SAT::SatProofNode::getRightParent(), SAT::SatProofNode::isLeaf(), and CVC3::Theorem::isNull().