diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/Makefile | 4 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 2 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 33 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 5 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 3 |
5 files changed, 24 insertions, 23 deletions
diff --git a/src/prop/bvminisat/Makefile b/src/prop/bvminisat/Makefile new file mode 100644 index 000000000..71888016d --- /dev/null +++ b/src/prop/bvminisat/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/prop/bvminisat + +include $(topdir)/Makefile.subdir diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 978ac8d7b..68969c78b 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -32,7 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "theory/interrupted.h" using namespace BVMinisat; -namespace CVC4 { +namespace BVMinisat { #define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] " diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 9f2138e9d..89cd731e9 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -108,11 +108,10 @@ void TseitinCnfStream::ensureLiteral(TNode n) { Debug("cnf") << "ensureLiteral(" << n << ")" << endl; if(hasLiteral(n)) { SatLiteral lit = getLiteral(n); - LiteralToNodeMap::iterator i = d_literalToNodeMap.find(lit); - if(i == d_literalToNodeMap.end()) { + if(!d_literalToNodeMap.contains(lit)){ // Store backward-mappings - d_literalToNodeMap[lit] = n; - d_literalToNodeMap[~lit] = n.notNode(); + d_literalToNodeMap.insert(lit, n); + d_literalToNodeMap.insert(~lit, n.notNode()); } return; } @@ -140,8 +139,9 @@ void TseitinCnfStream::ensureLiteral(TNode n) { lit = toCNF(n, false); // Store backward-mappings - d_literalToNodeMap[lit] = n; - d_literalToNodeMap[~lit] = n.notNode(); + // These may already exist + d_literalToNodeMap.insert_safe(lit, n); + d_literalToNodeMap.insert_safe(~lit, n.notNode()); } else { // We have a theory atom or variable. lit = convertAtom(n); @@ -168,8 +168,8 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { } else { lit = SatLiteral(d_satSolver->newVar(theoryLiteral)); } - d_nodeToLiteralMap[node] = lit; - d_nodeToLiteralMap[node.notNode()] = ~lit; + d_nodeToLiteralMap.insert(node, lit); + d_nodeToLiteralMap.insert(node.notNode(), ~lit); } else { lit = getLiteral(node); } @@ -178,8 +178,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { if ( theoryLiteral || d_fullLitToNodeMap || ( CVC4_USE_REPLAY && options::replayLog() != NULL ) || (Dump.isOn("clauses")) ) { - d_literalToNodeMap[lit] = node; - d_literalToNodeMap[~lit] = node.notNode(); + + d_literalToNodeMap.insert_safe(lit, node); + d_literalToNodeMap.insert_safe(~lit, node.notNode()); } // If a theory literal, we pre-register it @@ -197,11 +198,8 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { TNode CnfStream::getNode(const SatLiteral& literal) { Debug("cnf") << "getNode(" << literal << ")" << endl; - LiteralToNodeMap::iterator find = d_literalToNodeMap.find(literal); - Assert(find != d_literalToNodeMap.end()); - Assert(d_nodeToLiteralMap.find((*find).second) != d_nodeToLiteralMap.end()); - Debug("cnf") << "getNode(" << literal << ") => " << (*find).second << endl; - return (*find).second; + Debug("cnf") << "getNode(" << literal << ") => " << d_literalToNodeMap[literal] << endl; + return d_literalToNodeMap[literal]; } void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const { @@ -229,10 +227,9 @@ SatLiteral CnfStream::convertAtom(TNode node) { } SatLiteral CnfStream::getLiteral(TNode node) { - NodeToLiteralMap::iterator find = d_nodeToLiteralMap.find(node); Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node"); - Assert(find != d_nodeToLiteralMap.end(), "Literal not in the CNF Cache: %s\n", node.toString().c_str()); - SatLiteral literal = (*find).second; + Assert(d_nodeToLiteralMap.contains(node), "Literal not in the CNF Cache: %s\n", node.toString().c_str()); + SatLiteral literal = d_nodeToLiteralMap[node]; Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; return literal; } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 6ab639712..042cccd56 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -29,6 +29,7 @@ #include "prop/theory_proxy.h" #include "prop/registrar.h" #include "context/cdlist.h" +#include "context/cdinsert_hashmap.h" #include <ext/hash_map> @@ -47,10 +48,10 @@ class CnfStream { public: /** Cache of what nodes have been registered to a literal. */ - typedef context::CDHashMap<SatLiteral, TNode, SatLiteralHashFunction> LiteralToNodeMap; + typedef context::CDInsertHashMap<SatLiteral, TNode, SatLiteralHashFunction> LiteralToNodeMap; /** Cache of what literals have been registered to a node. */ - typedef context::CDHashMap<Node, SatLiteral, NodeHashFunction> NodeToLiteralMap; + typedef context::CDInsertHashMap<Node, SatLiteral, NodeHashFunction> NodeToLiteralMap; protected: diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index e5d876b48..b4807b021 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -130,8 +130,6 @@ public: };/* class DPLLSatSolverInterface */ -}/* CVC4::prop namespace */ - inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { out << lit.toString(); return out; @@ -167,6 +165,7 @@ inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) { return out; } +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* __CVC4__PROP__SAT_MODULE_H */ |