Initial stride towards external libabc integration

Does not yet compile
stp · Mar 22, 2015 · 1e8ebd4 · 1e8ebd4
1 parent 79ddd02
commit 1e8ebd4
Show file tree

Hide file tree

Showing 75 changed files with 423 additions and 41,202 deletions.
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -258,6 +258,9 @@ else()
   include_directories(${Boost_INCLUDE_DIRS})
 endif()
 
+find_package(ABC)
+include_directories(${ABC_INCLUDE_DIRS})
+
 
 # -----------------------------------------------------------------------------
 # Find CryptoMiniSat4

diff --git a/include/stp/Simplifier/AIGSimplifyPropositionalCore.h b/include/stp/Simplifier/AIGSimplifyPropositionalCore.h
@@ -43,9 +43,7 @@ THE SOFTWARE.
 #include "stp/AST/AST.h"
 #include "stp/STPManager/STPManager.h"
 #include "stp/Simplifier/simplifier.h"
-// FIXME: External libraries
-#include "extlib-abc/aig.h"
-#include "extlib-abc/dar.h"
+
 #include "stp/ToSat/AIG/BBNodeManagerAIG.h"
 #include "stp/ToSat/BitBlaster.h"
 
@@ -117,124 +115,10 @@ class AIGSimplifyPropositionalCore // not copyable
   typedef std::map<Aig_Obj_t*, ASTNode> 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");
-    }
-  }
+  ASTNode convert(BBNodeManagerAIG& mgr, Aig_Obj_t* obj, cacheType& cache);
 
 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<BBNodeAIG, BBNodeManagerAIG> bb(
-        &mgr, &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);
-  }
+  ASTNode topLevel(const ASTNode& top);
 };
 }
 #endif /* AIGSIMPLIFYPROPOSITIONALCORE_H_ */
diff --git a/include/stp/ToSat/AIG/BBNodeAIG.h b/include/stp/ToSat/AIG/BBNodeAIG.h
@@ -26,9 +26,10 @@ THE SOFTWARE.
 #ifndef BBNODEAIG_H_
 #define BBNODEAIG_H_
 
-#include "extlib-abc/aig.h"
 #include <iostream>
 
+typedef struct Aig_Obj_t_            Aig_Obj_t;
+
 namespace stp
 {
 using std::cerr;
@@ -41,38 +42,7 @@ using std::endl;
 class BBNodeAIG
 {
   // This is only useful for printing small instances for debuging.
-  void print(Aig_Obj_t* node) const
-  {
-    Aig_Obj_t* c0 = node->pFanin0, *c1 = node->pFanin1;
-    bool c0Not = Aig_IsComplement(c0), c1Not = Aig_IsComplement(c1);
-    if (c0Not)
-      c0 = Aig_Not(c0);
-    if (c1Not)
-      c1 = Aig_Not(c1);
-
-    cerr << node->Id;
-    cerr << "[" << node->Type << "]";
-    cerr << ": (";
-    if (c0 != 0)
-    {
-      if (c0Not)
-        cerr << "-";
-      cerr << c0->Id;
-      cerr << ",";
-    }
-    if (c1 != 0)
-    {
-      if (c1Not)
-        cerr << "-";
-
-      cerr << c1->Id;
-    }
-    cerr << ")" << endl;
-    if (c0 != 0)
-      print(c0);
-    if (c1 != 0)
-      print(c1);
-  }
+  void print(Aig_Obj_t* node) const;
 
 public:
   intptr_t GetNodeNum() const { return (intptr_t)n; }
@@ -87,19 +57,7 @@ class BBNodeAIG
 
   BBNodeAIG() { n = NULL; }
 
-  BBNodeAIG(Aig_Obj_t* _n)
-  {
-    n = _n;
-    assert(n != NULL);
-    if (Aig_IsComplement(n))
-    {
-      assert(Aig_Not(n)->Type != 0); // don't want nodes of type UNKNOWN>
-    }
-    else
-    {
-      assert(n->Type != 0);
-    }
-  }
+  BBNodeAIG(Aig_Obj_t* _n);
 
   bool IsNull() const { return n == NULL; }