From 8b0fe4b3f91b0d4294545fddf258eb8ea388c22d Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 6 Mar 2011 23:15:48 +0000 Subject: [PATCH] Add simplification of the top-most propositional part of the problem using AIGs. This is currently disabled by default. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1191 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/RunTimes.cpp | 2 +- src/AST/RunTimes.h | 3 +- src/STPManager/STP.cpp | 18 +- src/simplifier/AIGSimplifyPropositionalCore.h | 201 ++++++++++++++++++ 4 files changed, 221 insertions(+), 3 deletions(-) create mode 100644 src/simplifier/AIGSimplifyPropositionalCore.h diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp index 5d7abc4..5e9bc0f 100644 --- a/src/AST/RunTimes.cpp +++ b/src/AST/RunTimes.cpp @@ -16,7 +16,7 @@ #include "../sat/utils/System.h" // BE VERY CAREFUL> Update the Category Names to match. -std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Remove Unconstrained", "Pure Literals" , "ITE Contexts"}; +std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Remove Unconstrained", "Pure Literals" , "ITE Contexts", "AIG core simplification"}; namespace BEEV { diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h index cde2269..f167829 100644 --- a/src/AST/RunTimes.h +++ b/src/AST/RunTimes.h @@ -35,7 +35,8 @@ public: ApplyingSubstitutions, RemoveUnconstrained, PureLiterals, - UseITEContext + UseITEContext, + AIGSimplifyCore }; static std::string CategoryNames[]; diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 13e074a..9244582 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -19,6 +19,7 @@ #include "../simplifier/FindPureLiterals.h" #include "../simplifier/EstablishIntervals.h" #include "../simplifier/UseITEContext.h" +#include "../simplifier/AIGSimplifyPropositionalCore.h" #include namespace BEEV { @@ -178,9 +179,10 @@ namespace BEEV { { EstablishIntervals intervals(*bm); simplified_solved_InputToSAT = intervals.topLevel_unsignedIntervals(simplified_solved_InputToSAT ); + bm->ASTNodeStats("After Establishing Intervals: ", + simplified_solved_InputToSAT); } - // Find pure literals. if (bm->UserFlags.isSet("pure-literals","1")) { @@ -190,6 +192,8 @@ namespace BEEV { { simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT); simp->haveAppliedSubstitutionMap(); + bm->ASTNodeStats("After Pure Literals: ", + simplified_solved_InputToSAT); } } @@ -198,8 +202,20 @@ namespace BEEV { { UseITEContext iteC(bm); simplified_solved_InputToSAT = iteC.topLevel(simplified_solved_InputToSAT); + bm->ASTNodeStats("After ITE Context: ", + simplified_solved_InputToSAT); + } + if (bm->UserFlags.isSet("aig-core-simplify","0")) + { + AIGSimplifyPropositionalCore aigRR(bm); + simplified_solved_InputToSAT = aigRR.topLevel(simplified_solved_InputToSAT); + bm->ASTNodeStats("After AIG Core: ", + simplified_solved_InputToSAT); + } + + bm->ASTNodeStats("Before SimplifyWrites_Inplace begins: ", simplified_solved_InputToSAT); diff --git a/src/simplifier/AIGSimplifyPropositionalCore.h b/src/simplifier/AIGSimplifyPropositionalCore.h new file mode 100644 index 0000000..2fead48 --- /dev/null +++ b/src/simplifier/AIGSimplifyPropositionalCore.h @@ -0,0 +1,201 @@ +/* + * This takes the topmost propositional part of the input, simplifies it with DAG aware rewritting, + * then converts it back to ASTNodes. + * + * + * This has two problems: 1) It doesn't consider that the propositional variables that are introduced, + * might actually represent many thousands of AIG nodes, so it doesn't do the "DAG aware" part correctly. + * 2) The startup of the DAR takes about 150M instructions, which is agggeeesss for small problems. + */ + +#ifndef AIGSIMPLIFYPROPOSITIONALCORE_H_ +#define AIGSIMPLIFYPROPOSITIONALCORE_H_ + +#include "../AST/AST.h" +#include "../STPManager/STPManager.h" +#include "simplifier.h" +#include "../extlib-abc/aig.h" +#include "../extlib-abc/dar.h" +#include "../to-sat/AIG/BBNodeManagerAIG.h" +#include "../to-sat/BitBlaster.h" + + +namespace BEEV +{ +class AIGSimplifyPropositionalCore { + + ASTNodeMap varToNodeMap; + STPMgr * bm; + NodeFactory* nf; + +public: + AIGSimplifyPropositionalCore(STPMgr *_bm) + { + bm = _bm; + nf = new SimplifyingNodeFactory(*bm->hashingNodeFactory,*bm); + } + + virtual ~AIGSimplifyPropositionalCore() + { + delete nf; + } +private: + + // Convert theory nodes to fresh variables. + ASTNode theoryToFresh(const ASTNode& n, ASTNodeMap& fromTo ) + { + if (n.isConstant()) + return n; + + const Kind k = n.GetKind(); + if (k == SYMBOL) + return n; + + ASTNodeMap::const_iterator it; + if ((it = fromTo.find(n)) != fromTo.end()) + return it->second; + + assert(n.GetValueWidth() ==0); + assert(n.GetIndexWidth() ==0); + + if (k == BVGT || k == BVGE || k == EQ || k == BVSGE || k == BVSGT || k == PARAMBOOL) // plus the rest. + { + ASTNode fresh = bm->CreateFreshVariable(n.GetIndexWidth(), n.GetValueWidth(),"theoryToFresh"); + varToNodeMap.insert(make_pair(fresh,n)); + fromTo.insert(make_pair(n,fresh)); + return fresh; + } + + const ASTVec& children = n.GetChildren(); + ASTVec new_children; + new_children.reserve(children.size()); + + for (ASTVec::const_iterator it = children.begin(); it != children.end(); it++) + new_children.push_back(theoryToFresh(*it,fromTo)); + + ASTNode result; + + if (children != new_children) + result = nf->CreateNode(k,new_children); + else + result = n; + + fromTo.insert(make_pair(n,result)); + return result; + } + + typedef map cacheType; + + // Convert the AIG back to an ASTNode. + ASTNode convert (BBNodeManagerAIG& mgr, Aig_Obj_t * obj, cacheType& cache) + { + cacheType::const_iterator it; + if ((it = cache.find(obj))!= cache.end()) + return it->second; + + if (Aig_IsComplement(obj)) + return nf->CreateNode(NOT, convert(mgr,Aig_Regular(obj),cache)); + else if (Aig_ObjIsAnd(obj)) + { + ASTNode result = nf->CreateNode(AND,convert(mgr,Aig_ObjChild0(obj),cache),convert(mgr,Aig_ObjChild1(obj),cache)); + cache.insert(make_pair(obj,result)); + return result; + } + else if (obj == Aig_ManConst1(mgr.aigMgr)) + return bm->ASTTrue; + else if (obj == Aig_ManConst0(mgr.aigMgr)) + return bm->ASTFalse; + else if (Aig_ObjIsPo(obj)) + return convert(mgr,Aig_ObjChild0(obj),cache); + else + FatalError("Unknown type"); + } +public: + + ASTNode topLevel(const ASTNode& top) + { + if (top.isConstant()) + return top; + + bm->GetRunTimes()->start(RunTimes::AIGSimplifyCore); + + ASTNodeMap fromTo; + + // Replace theory nodes with new variables. + ASTNode replaced = theoryToFresh(top,fromTo); + + Simplifier simplifier(bm); + BBNodeManagerAIG mgr; + BitBlaster bb(&mgr,NULL, &simplifier, bm->defaultNodeFactory,&bm->UserFlags); + BBNodeAIG blasted = bb.BBForm(replaced); + + Aig_ObjCreatePo(mgr.aigMgr, blasted.n); + Aig_ManCleanup( mgr.aigMgr); // remove nodes not connected to the PO. + Aig_ManCheck( mgr.aigMgr); // check that AIG looks ok. + + assert(Aig_ManPoNum(mgr.aigMgr) == 1); + + int initial_nodeCount = mgr.aigMgr->nObjs[AIG_OBJ_AND]; + //cerr << "Nodes before AIG rewrite:" << initial_nodeCount << endl; + + Dar_LibStart(); // About 150M instructions. Very expensive. + Aig_Man_t * pTemp; + Dar_RwrPar_t Pars, *pPars = &Pars; + Dar_ManDefaultRwrParams(pPars); + + // Assertion errors occur with this enabled. + pPars->fUseZeros = 1; + + const int iterations = 3; + + int lastNodeCount = initial_nodeCount; + for (int i = 0; i < iterations; i++) { + mgr.aigMgr = Aig_ManDup(pTemp = mgr.aigMgr, 0); + Aig_ManStop(pTemp); + Dar_ManRewrite(mgr.aigMgr, pPars); + + mgr.aigMgr = Aig_ManDup(pTemp = mgr.aigMgr, 0); + Aig_ManStop(pTemp); + + //cerr << "After rewrite [" << i << "] nodes:" + // << mgr.aigMgr->nObjs[AIG_OBJ_AND] << endl; + + if (lastNodeCount == mgr.aigMgr->nObjs[AIG_OBJ_AND]) + break; + lastNodeCount = mgr.aigMgr->nObjs[AIG_OBJ_AND]; + } + + + cacheType ptrToOrig; + // This needs to be done after bitblasting because the PI nodes will be altered. + + for (BBNodeManagerAIG::SymbolToBBNode::iterator it = mgr.symbolToBBNode.begin(); it!= mgr.symbolToBBNode.end();it++) + { + ASTNode fresh = it->first; // the fresh variable. + assert(fresh.GetKind() == SYMBOL); + + ASTNode result; + if (varToNodeMap.find(fresh)== varToNodeMap.end()) + result = it->first; // It's not a fresh variable. i.e. it's a propositional var. in the original formula. + else + result = varToNodeMap.find(fresh)->second; // what it replaced. + assert((it->second).size() == 1); // should be a propositional variable. + const int index = (it->second)[0].symbol_index; // This is the index of the pi. + Aig_Obj_t * pi = Aig_ManPi(mgr.aigMgr,index); + ptrToOrig.insert(make_pair(pi,result)); + } + + Aig_Obj_t * pObj = (Aig_Obj_t*)Vec_PtrEntry(mgr.aigMgr->vPos, 0); + + ASTNode result = convert(mgr, pObj,ptrToOrig); + + Dar_LibStop(); + + bm->GetRunTimes()->stop(RunTimes::AIGSimplifyCore); + return result; + //return simplifier.SimplifyFormula(result,false,NULL); + } + +}; +}; +#endif /* AIGSIMPLIFYPROPOSITIONALCORE_H_ */ -- 2.47.3