From: trevor_hansen Date: Mon, 16 Aug 2010 01:02:58 +0000 (+0000) Subject: Code for AIG rewriting with ABC. This code is not currently enabled by default. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=88780fd77543c5f7a07423d397a836ba2958da57;p=francis%2Fstp.git Code for AIG rewriting with ABC. This code is not currently enabled by default. I'll enable it when I understand when it's useful. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@987 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h index f365ded..3e5f2a7 100644 --- a/src/STPManager/UserDefinedFlags.h +++ b/src/STPManager/UserDefinedFlags.h @@ -117,6 +117,8 @@ namespace BEEV bool exit_after_CNF; + bool enable_AIG_rewrites_flag; + // Available back-end SAT solvers. enum SATSolvers { @@ -230,6 +232,8 @@ namespace BEEV exit_after_CNF=false; + enable_AIG_rewrites_flag = false; + } //End of constructor for UserDefinedFlags }; //End of struct UserDefinedFlags diff --git a/src/to-sat/AIG/BBNodeAIG.h b/src/to-sat/AIG/BBNodeAIG.h index f9fec0a..eacd91f 100644 --- a/src/to-sat/AIG/BBNodeAIG.h +++ b/src/to-sat/AIG/BBNodeAIG.h @@ -59,6 +59,9 @@ public: // If the pointer is odd. Then it's the NOT of the pointer one less. Aig_Obj_t * n; + // After dag aware rewriting the symbol stays at the same position in the vector of PIs. + // To get it's CNF variable number we get the node at the same position. + int symbol_index; BBNodeAIG() { @@ -100,12 +103,10 @@ public: return n < other.n; } - - void print() const -{ + { print(n); -} + } }; } diff --git a/src/to-sat/AIG/BBNodeManagerAIG.cpp b/src/to-sat/AIG/BBNodeManagerAIG.cpp new file mode 100644 index 0000000..ff1bd68 --- /dev/null +++ b/src/to-sat/AIG/BBNodeManagerAIG.cpp @@ -0,0 +1,84 @@ +#include "BBNodeManagerAIG.h" + +namespace BEEV +{ + + void + BBNodeManagerAIG::toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar, const UserDefinedFlags& uf) + { + assert(cnfData == NULL); + + Aig_ObjCreatePo(aigMgr, top.n); + Aig_ManCleanup(aigMgr); // remove nodes not connected to the PO. + Aig_ManCheck(aigMgr); // check that AIG looks ok. + + assert(Aig_ManPoNum(aigMgr) == 1); + + // UseZeroes gives assertion errors. + // Rewriting is sometimes very slow. Can it be configured to be faster? + // What about refactoring??? + + if (uf.enable_AIG_rewrites_flag) + { + int nodeCount = aigMgr->nObjs[AIG_OBJ_AND]; + if (uf.stats_flag) + cerr << "Nodes before AIG rewrite:" << nodeCount <fUpdateLevel =0; + //pPars->fUseZeros = 1; + + for (int i=0; i < 3;i++) + { + aigMgr = Aig_ManDup( pTemp = aigMgr, 0 ); + Aig_ManStop( pTemp ); + Dar_ManRewrite( aigMgr, pPars ); + + aigMgr = Aig_ManDup( pTemp = aigMgr, 0 ); + Aig_ManStop( pTemp ); + + if (uf.stats_flag) + cerr << "After rewrite [" << i << "] nodes:" << aigMgr->nObjs[AIG_OBJ_AND] << endl; + + if (nodeCount == aigMgr->nObjs[AIG_OBJ_AND]) + break; + } + } + cnfData = Cnf_Derive(aigMgr, 0); + + BBNodeManagerAIG::SymbolToBBNode::const_iterator it; + + 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; + assert (nodeToVar.find(n) == nodeToVar.end()); + + const int width = (n.GetType() == BOOLEAN_TYPE) ? 1: n.GetValueWidth(); + + // INT_MAX for parts of symbols that didn't get encoded. + vector v(width, ~((unsigned) 0)); + + for (unsigned i = 0; i < b.size(); i++) + { + if (!b[i].IsNull()) + { + Aig_Obj_t * pObj; + pObj = (Aig_Obj_t*)Vec_PtrEntry( aigMgr->vPis, b[i].symbol_index ); + v[i] = cnfData->pVarNums[pObj->Id]; + } + } + + nodeToVar.insert(make_pair(n, v)); + } + assert(cnfData != NULL); + } +} + + diff --git a/src/to-sat/AIG/BBNodeManagerAIG.h b/src/to-sat/AIG/BBNodeManagerAIG.h index db12056..451199b 100644 --- a/src/to-sat/AIG/BBNodeManagerAIG.h +++ b/src/to-sat/AIG/BBNodeManagerAIG.h @@ -107,75 +107,7 @@ public: return BBNodeAIG(Aig_ManConst0(aigMgr)); } - void toCNF_experimental(BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar) - { - //cerr << "SAFDASDF"; - - // copied from darScript.c: Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig ) - /* - Dar_LibStart(); - Aig_Man_t * pTemp1, *pTemp2; - Dar_RwrPar_t Pars, * pPars = &Pars; - Dar_ManDefaultRwrParams( pPars ); - Dar_ManRewrite( aigMgr, pPars ); - Aig_ManCheck(aigMgr); // check that AIG looks ok. - Dar_LibStop(); - */ - - //assert(Aig_ManPoNum(aigMgr) == 1); - - //Aig_NtkReassignIds( aigMgr ); - // fix the levels - //Aig_ManUpdateLevel( aigMgr, Aig_ManPo(aigMgr,0)); - //Aig_ManVerifyLevel( aigMgr ); - - - // assert(Aig_ManPoNum(aigMgr) == 1); - - //Dar_RwrPar_t pPars; - //Dar_ManDefaultRwrParams( &pPars ); - //Dar_ManRewrite( aigMgr, &pPars ); - } - - void - toCNF(BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar) - { - assert(cnfData == NULL); - - Aig_ObjCreatePo(aigMgr, top.n); - Aig_ManCleanup( aigMgr); // remove nodes not connected to the PO. - Aig_ManCheck(aigMgr); // check that AIG looks ok. - - assert(Aig_ManPoNum(aigMgr) == 1); - - // Cnf_Derive gives errors sometimes. - //cnfData = Cnf_DeriveSimple(aigMgr, 0); - cnfData = Cnf_Derive(aigMgr, 0); - - BBNodeManagerAIG::SymbolToBBNode::const_iterator it; - - 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; - assert (nodeToVar.find(n) == nodeToVar.end()); - - const int width = (n.GetType() == BOOLEAN_TYPE) ? 1: n.GetValueWidth(); - vector v(width, ~((unsigned) 0)); - - for (unsigned i = 0; i < b.size(); i++) - { - if (!b[i].IsNull()) - v[i] = cnfData->pVarNums[b[i].n->Id]; - } - - nodeToVar.insert(make_pair(n, v)); - } - assert(cnfData != NULL); - } + void toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar, const UserDefinedFlags& uf); // The same symbol always needs to return the same AIG node, // if it doesn't you will get the wrong answer. @@ -201,7 +133,7 @@ public: return it->second[i]; it->second[i] = BBNodeAIG(Aig_ObjCreatePi(aigMgr)); - + it->second[i].symbol_index = aigMgr->vPis->nSize-1; return it->second[i]; } diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp index d79fe27..6ea8b0b 100644 --- a/src/to-sat/AIG/ToSATAIG.cpp +++ b/src/to-sat/AIG/ToSATAIG.cpp @@ -24,7 +24,7 @@ namespace BEEV Cnf_Dat_t* cnfData = NULL; bm->GetRunTimes()->start(RunTimes::CNFConversion); - mgr.toCNF(BBFormula, cnfData, nodeToSATVar); + mgr.toCNF(BBFormula, cnfData, nodeToSATVar,bm->UserFlags); bm->GetRunTimes()->stop(RunTimes::CNFConversion); // Free the memory in the AIGs.