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().
