From 3089ce189b1130227d7787dd30e55b89b33fbbfc Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 15 Aug 2010 04:57:31 +0000 Subject: [PATCH] Refactor. Remove unncessary code. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@985 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/AIG/BBNodeManagerAIG.h | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/to-sat/AIG/BBNodeManagerAIG.h b/src/to-sat/AIG/BBNodeManagerAIG.h index 25c323a..db12056 100644 --- a/src/to-sat/AIG/BBNodeManagerAIG.h +++ b/src/to-sat/AIG/BBNodeManagerAIG.h @@ -141,7 +141,6 @@ public: toCNF(BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar) { assert(cnfData == NULL); - assert(nodeToVar.size() ==0); Aig_ObjCreatePo(aigMgr, top.n); Aig_ManCleanup( aigMgr); // remove nodes not connected to the PO. @@ -157,23 +156,23 @@ public: assert(nodeToVar.size() ==0); + // Each symbol maps to a vector of CNF variables. for (it = symbolToBBNode.begin(); it != symbolToBBNode.end(); it++) { const ASTNode& n = it->first; const vector &b = it->second; - if (nodeToVar.find(n) == nodeToVar.end()) - { - const int width = (n.GetType() == BOOLEAN_TYPE) ? 1: n.GetValueWidth(); - vector v(width, ~((unsigned) 0)); - nodeToVar.insert(make_pair(n, v)); - } + assert (nodeToVar.find(n) == nodeToVar.end()); + + const int width = (n.GetType() == BOOLEAN_TYPE) ? 1: n.GetValueWidth(); + vector v(width, ~((unsigned) 0)); - vector& v = nodeToVar[n]; for (unsigned i = 0; i < b.size(); i++) { if (!b[i].IsNull()) - v[i] = cnfData->pVarNums[b[i].n->Id]; + v[i] = cnfData->pVarNums[b[i].n->Id]; } + + nodeToVar.insert(make_pair(n, v)); } assert(cnfData != NULL); } -- 2.47.3