Removing internal ABC and linking to recent upstream.

Problems are:
* I've hardcorded the file locations on my machine.
* It's failing on the divZero.cvc test

CMakeLists.txt

@@ -51,6 +51,12 @@ if(NOT CMAKE_BUILD_TYPE)
 endif()
 message(STATUS "Doing a ${CMAKE_BUILD_TYPE} build")
 
+# Location to find the header files we need.
+include_directories(/home/ec2-user/abc/src/)
+# ABC builds a C application that prints this out. This is what it is on my machine...
+add_definitions(-DLIN64 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -DSIZEOF_INT=4)
+
+
 # -----------------------------------------------------------------------------
 # Option to enable/disable assertions
 # -----------------------------------------------------------------------------

include/stp/Simplifier/AIGSimplifyPropositionalCore.h

@@ -44,7 +44,7 @@ THE SOFTWARE.
 #include "stp/STPManager/STPManager.h"
 
 // FIXME: External libraries
-#include "extlib-abc/aig.h"
+#include "aig/aig/aig.h"
 #include "stp/ToSat/AIG/BBNodeManagerAIG.h"
 
 namespace stp

include/stp/ToSat/AIG/BBNodeAIG.h

@@ -26,7 +26,7 @@ THE SOFTWARE.
 #ifndef BBNODEAIG_H_
 #define BBNODEAIG_H_
 
-#include "extlib-abc/aig.h"
+#include "aig/aig/aig.h"
 #include <iostream>
 
 namespace stp

include/stp/ToSat/AIG/BBNodeManagerAIG.h

@@ -31,9 +31,9 @@ THE SOFTWARE.
 
 // cnf_short omits some stuff that doesn't compile in g++ that we don't need
 // anyway.
-#include "extlib-abc/aig.h"
-#include "extlib-abc/cnf_short.h"
-#include "extlib-abc/dar.h"
+#include "aig/aig/aig.h"
+#include "sat/cnf/cnf.h"
+#include "opt/dar/dar.h"
 #include "stp/ToSat/ToSATBase.h"
 
 typedef Cnf_Dat_t_ CNFData;
@@ -145,8 +145,8 @@ class BBNodeManagerAIG
     if (!it->second[i].IsNull())
       return it->second[i];
 
-    it->second[i] = BBNodeAIG(Aig_ObjCreatePi(aigMgr));
-    it->second[i].symbol_index = aigMgr->vPis->nSize - 1;
+    it->second[i] = BBNodeAIG(Aig_ObjCreateCi(aigMgr));
+    it->second[i].symbol_index = aigMgr->vCis->nSize - 1;
     return it->second[i];
   }
 

include/stp/ToSat/AIG/ToCNFAIG.h

@@ -25,9 +25,9 @@ THE SOFTWARE.
 #ifndef TOCNFAIG_H_
 #define TOCNFAIG_H_
 
-#include "extlib-abc/aig.h"
-#include "extlib-abc/cnf_short.h"
-#include "extlib-abc/dar.h"
+#include "aig/aig/aig.h"
+#include "sat/cnf/cnf.h"
+#include "opt/dar/dar.h"
 #include "stp/ToSat/ToSATBase.h"
 #include "stp/ToSat/AIG/BBNodeManagerAIG.h"
 

lib/CMakeLists.txt

@@ -25,7 +25,6 @@ add_subdirectory(Simplifier)
 add_subdirectory(Printer)
 add_subdirectory(Parser)
 add_subdirectory(Interface)
-add_subdirectory(extlib-abc)
 add_subdirectory(extlib-constbv)
 add_subdirectory(STPManager)
 add_subdirectory(ToSat)
@@ -47,7 +46,6 @@ set(stp_lib_targets
     sat
     simplifier
     constantbv
-    abc
     cinterface
     cppinterface
     parser
@@ -123,6 +121,12 @@ if (USE_CRYPTOMINISAT)
     endif()
 endif()
 
+#Where I install the abc library to on my machine..
+set(libstp_link_libs ${libstp_link_libs} /home/ec2-user/abc/libabc.a)
+set(libstp_link_libs ${libstp_link_libs} dl)
+set(libstp_link_libs ${libstp_link_libs} readline)
+
+
 target_link_libraries(libstp ${libstp_link_libs})
 
 # Set the public header so it will be installed

lib/Interface/c_interface.cpp

@@ -29,7 +29,7 @@ THE SOFTWARE.
 #include "stp/Printer/printers.h"
 #include "stp/cpp_interface.h"
 // FIXME: External library
-#include "extlib-abc/cnf_short.h"
+#include "sat/cnf/cnf.h"
 
 #ifdef _MSC_VER
 #include <compdep.h>
@@ -1818,7 +1818,7 @@ void vc_Destroy(VC vc)
     b->persist.clear();
   }
 
-  Cnf_ClearMemory();
+  Cnf_ManFree();
   vc_clearDecls(vc);
 
   delete ((stp::STP*)vc);

lib/Simplifier/AIGSimplifyPropositionalCore.cpp

@@ -40,7 +40,7 @@ THE SOFTWARE.
 
 // FIXME: External libraries
 #include "stp/Simplifier/AIGSimplifyPropositionalCore.h"
-#include "extlib-abc/dar.h"
+#include "opt/dar/dar.h"
 #include "stp/Simplifier/Simplifier.h"
 #include "stp/ToSat/BitBlaster.h"
 
@@ -129,7 +129,7 @@ using std::make_pair;
       return bm->ASTTrue;
     else if (obj == Aig_ManConst0(mgr.aigMgr))
       return bm->ASTFalse;
-    else if (Aig_ObjIsPo(obj))
+    else if (Aig_ObjIsCo(obj))
       return convert(mgr, Aig_ObjChild0(obj), cache);
     else
     {
@@ -158,11 +158,11 @@ using std::make_pair;
         &mgr, &simplifier, bm->defaultNodeFactory, &bm->UserFlags);
     BBNodeAIG blasted = bb.BBForm(replaced);
 
-    Aig_ObjCreatePo(mgr.aigMgr, blasted.n);
+    Aig_ObjCreateCo(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);
+    assert(Aig_ManCoNum(mgr.aigMgr) == 1);
 
     int initial_nodeCount = mgr.aigMgr->nObjs[AIG_OBJ_AND];
     // cerr << "Nodes before AIG rewrite:" << initial_nodeCount << endl;
@@ -180,11 +180,11 @@ using std::make_pair;
     int lastNodeCount = initial_nodeCount;
     for (int i = 0; i < iterations; i++)
     {
-      mgr.aigMgr = Aig_ManDup(pTemp = mgr.aigMgr, 0);
+      mgr.aigMgr = Aig_ManDupDfs(pTemp = mgr.aigMgr);
       Aig_ManStop(pTemp);
       Dar_ManRewrite(mgr.aigMgr, pPars);
 
-      mgr.aigMgr = Aig_ManDup(pTemp = mgr.aigMgr, 0);
+      mgr.aigMgr = Aig_ManDupDfs(pTemp = mgr.aigMgr);
       Aig_ManStop(pTemp);
 
       // cerr << "After rewrite [" << i << "]  nodes:"
@@ -215,11 +215,11 @@ using std::make_pair;
       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);
+      Aig_Obj_t* pi = Aig_ManCi(mgr.aigMgr, index);
       ptrToOrig.insert(make_pair(pi, result));
     }
 
-    Aig_Obj_t* pObj = (Aig_Obj_t*)Vec_PtrEntry(mgr.aigMgr->vPos, 0);
+    Aig_Obj_t* pObj = (Aig_Obj_t*)Vec_PtrEntry(mgr.aigMgr->vCos, 0);
 
     ASTNode result = convert(mgr, pObj, ptrToOrig);
 

lib/ToSat/AIG/ToCNFAIG.cpp

@@ -48,7 +48,7 @@ void addVariables(BBNodeManagerAIG& mgr, Cnf_Dat_t*& cnfData,
       if (!b[i].IsNull())
       {
         Aig_Obj_t* pObj;
-        pObj = (Aig_Obj_t*)Vec_PtrEntry(mgr.aigMgr->vPis, b[i].symbol_index);
+        pObj = (Aig_Obj_t*)Vec_PtrEntry(mgr.aigMgr->vCis, b[i].symbol_index);
         v[i] = cnfData->pVarNums[pObj->Id];
       }
     }
@@ -69,9 +69,13 @@ void ToCNFAIG::dag_aware_aig_rewrite(
     Dar_RwrPar_t Pars, *pPars = &Pars;
     Dar_ManDefaultRwrParams(pPars);
 
-    // Assertion errors occur with this enabled.
+    // TODO check if these help
+    // pPars->fUpdateLevel =0;.
     // pPars->fUseZeros = 1;
 
+    if (uf.stats_flag)
+      pPars->fVerbose=1;
+
     // For mul63bit.smt2 with iterations =3 & nCutsMax = 8
     // CNF generation was taking 139 seconds, solving 10 seconds.
 
@@ -81,11 +85,14 @@ void ToCNFAIG::dag_aware_aig_rewrite(
 
     for (int i = 0; i < iterations; i++)
     {
-      mgr.aigMgr = Aig_ManDup(pTemp = mgr.aigMgr, 0);
+      mgr.aigMgr = Aig_ManDupDfs(pTemp = mgr.aigMgr);
       Aig_ManStop(pTemp);
       Dar_ManRewrite(mgr.aigMgr, pPars);
 
-      mgr.aigMgr = Aig_ManDup(pTemp = mgr.aigMgr, 0);
+      // 1 in a million need cleaning up after dar_manrewrite, seems like an ABC defect.
+      Aig_ManCleanup(mgr.aigMgr);
+
+      mgr.aigMgr = Aig_ManDupDfs(pTemp = mgr.aigMgr);
       Aig_ManStop(pTemp);
 
       if (uf.stats_flag)
@@ -105,14 +112,14 @@ void ToCNFAIG::toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData,
 {
   assert(cnfData == NULL);
 
-  Aig_ObjCreatePo(mgr.aigMgr, top.n);
+  Aig_ObjCreateCo(mgr.aigMgr, top.n);
   if (!needAbsRef)
   {
     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);
+  assert(Aig_ManCoNum(mgr.aigMgr) == 1);
 
   // UseZeroes gives assertion errors.
   // Rewriting is sometimes very slow. Can it be configured to be faster?
@@ -168,7 +175,7 @@ void ToCNFAIG::fill_node_to_var(
       if (!b[i].IsNull())
       {
         Aig_Obj_t* pObj;
-        pObj = (Aig_Obj_t*)Vec_PtrEntry(mgr.aigMgr->vPis, b[i].symbol_index);
+        pObj = (Aig_Obj_t*)Vec_PtrEntry(mgr.aigMgr->vCis, b[i].symbol_index);
         v[i] = cnfData->pVarNums[pObj->Id];
       }
     }

lib/ToSat/AIG/ToSATAIG.cpp

@@ -77,7 +77,7 @@ void ToSATAIG::release_cnf_memory(Cnf_Dat_t* cnfData)
   // If CNF generation is going to be called lots, we'd rather keep it around.
   // because the datatables are expensive to generate.
   if (cnf_calls == 0)
-    Cnf_ClearMemory();
+    Cnf_ManFree();
 
   Cnf_DataFree(cnfData);
   cnf_calls++;
@@ -89,7 +89,7 @@ void ToSATAIG::handle_cnf_options(Cnf_Dat_t* cnfData, bool needAbsRef)
   {
     std::stringstream fileName;
     fileName << "output_" << bm->CNFFileNameCounter++ << ".cnf";
-    Cnf_DataWriteIntoFile(cnfData, (char*)fileName.str().c_str(), 0);
+    Cnf_DataWriteIntoFile(cnfData, (char*)fileName.str().c_str(), 0,0,0);
   }
 
   if (bm->UserFlags.exit_after_CNF)