diff --git a/src/aig/gia/giaNewBdd.h b/src/aig/gia/giaNewBdd.h index 6d75f4d99..23e92c2d9 100644 --- a/src/aig/gia/giaNewBdd.h +++ b/src/aig/gia/giaNewBdd.h @@ -780,10 +780,34 @@ namespace NewBdd { for(size_t i = 0; i < vLits.size(); i++) IncRef(vLits[i]); } + void RemoveRefIfUnused() { + if(!nGbc && nReo == BvarMax()) + vRefs.clear(); + } + void TurnOnReo(int nReo_ = 0, std::vector const *vLits = NULL) { + if(nReo_) + nReo = nReo_; + else + nReo = nObjs << 1; + if((lit)nReo > (lit)BvarMax()) + nReo = BvarMax(); + if(vRefs.empty()) { + if(vLits) + SetRef(*vLits); + else + vRefs.resize(nObjsAlloc); + } + } void TurnOffReo() { nReo = BvarMax(); - if(!nGbc) - vRefs.clear(); + } + var GetNumVars() const { + return nVars; + } + void GetOrdering(std::vector &Var2Level_) { + Var2Level_.resize(nVars); + for(var v = 0; v < nVars; v++) + Var2Level_[v] = Var2Level[v]; } bvar CountNodes() { bvar count = 1; diff --git a/src/aig/gia/giaNewTt.h b/src/aig/gia/giaNewTt.h index 494b8636b..52badb5e1 100644 --- a/src/aig/gia/giaNewTt.h +++ b/src/aig/gia/giaNewTt.h @@ -48,6 +48,7 @@ namespace NewTt { bool fCountOnes; int nGbc; int nReo; // dummy + std::vector *pVar2Level; // dummy Param() { nObjsAllocLog = 15; nObjsMaxLog = 20; @@ -261,10 +262,14 @@ namespace NewTt { for(size_t i = 0; i < vLits.size(); i++) IncRef(vLits[i]); } - void TurnOffReo() { + void RemoveRefIfUnused() { if(!nGbc) vRefs.clear(); } + void TurnOffReo() {} + int GetNumVars() const { + return nVars; + } void PrintNode(lit x) const { bvar a = Lit2Bvar(x); word c = LitIsCompl(x)? one(): 0;