Major restructuring of the code.

8 files changed, 24 insertions, 25 deletions

diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index 02fcc21b..9916b582 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __MFS_H__
-#define __MFS_H__
+#ifndef ABC__opt__mfs__mfs_h
+#define ABC__opt__mfs__mfs_h
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/mfs/mfsGia.c b/src/opt/mfs/mfsGia.c
index af6cc159..07c258ab 100644
--- a/src/opt/mfs/mfsGia.c
+++ b/src/opt/mfs/mfsGia.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
  
 #include "mfsInt.h"
-#include "giaAig.h"
+#include "aig/gia/giaAig.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 650a154a..fe154093 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -18,23 +18,22 @@
 
 ***********************************************************************/
  
-#ifndef __MFS_INT_H__
-#define __MFS_INT_H__
+#ifndef ABC__opt__mfs__mfsInt_h
+#define ABC__opt__mfs__mfsInt_h
 
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
 #include "mfs.h"
-#include "aig.h"
-#include "cnf.h"
-#include "satSolver.h"
-#include "satStore.h"
-#include "bdc.h"
-#include "gia.h"
+#include "src/aig/aig/aig.h"
+#include "src/sat/cnf/cnf.h"
+#include "src/sat/bsat/satSolver.h"
+#include "src/sat/bsat/satStore.h"
+#include "src/bool/bdc/bdc.h"
+#include "src/aig/gia/gia.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 0934513b..d18613c7 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "mfsInt.h"
-#include "kit.h"
+#include "src/bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index df331b43..caa82e68 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -52,7 +52,7 @@ Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars )
     p->vProjVarsCnf = Vec_IntAlloc( 100 );
     p->vProjVarsSat = Vec_IntAlloc( 100 );
     p->vDivLits  = Vec_IntAlloc( 100 );
-    p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX);
+    p->nDivWords = Abc_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX);
     p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords );
     p->pMan      = Int_ManAlloc();
     p->vMem      = Vec_IntAlloc( 0 );
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 40cb6198..45f75674 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -142,8 +142,8 @@ p->timeGia += clock() - clk;
         pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
         if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
         {
-            assert( Aig_InfoHasBit(pData, p->nCexes) );
-            Aig_InfoXorBit( pData, p->nCexes );
+            assert( Abc_InfoHasBit(pData, p->nCexes) );
+            Abc_InfoXorBit( pData, p->nCexes );
         }
     }
     p->nCexes++;
@@ -242,13 +242,13 @@ p->timeInt += clock() - clk;
             for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
             {
                 pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
-                printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
+                printf( "%d", Abc_InfoHasBit(pData, p->nCexes-1) );
             }
             printf( "\n" );
         }
 
         // find the next divisor to try
-        nWords = Aig_BitWordNum(p->nCexes);
+        nWords = Abc_BitWordNum(p->nCexes);
         assert( nWords <= p->nDivWords );
         for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
         {
@@ -387,13 +387,13 @@ p->timeInt += clock() - clk;
             for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
             {
                 pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
-                printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
+                printf( "%d", Abc_InfoHasBit(pData, p->nCexes-1) );
             }
             printf( "\n" );
         }
 
         // find the next divisor to try
-        nWords = Aig_BitWordNum(p->nCexes);
+        nWords = Abc_BitWordNum(p->nCexes);
         assert( nWords <= p->nDivWords );
         fBreak = 0;
         for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index 37ee2b39..e5e9de1a 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -72,8 +72,8 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
             Lits[b] = lit_neg( Lits[b] );
         }
     }
-    assert( !Aig_InfoHasBit(p->uCare, Mint) );
-    Aig_InfoSetBit( p->uCare, Mint );
+    assert( !Abc_InfoHasBit(p->uCare, Mint) );
+    Abc_InfoSetBit( p->uCare, Mint );
     // add the blocking clause
     RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVarsSat) );
     if ( RetValue == 0 )
@@ -106,7 +106,7 @@ int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
 
     // prepare the truth table of care set
     p->nFanins = Vec_IntSize( p->vProjVarsSat );
-    p->nWords = Aig_TruthWordNum( p->nFanins );
+    p->nWords = Abc_TruthWordNum( p->nFanins );
     memset( p->uCare, 0, sizeof(unsigned) * p->nWords );
 
     // iterate through the SAT assignments
diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c
index a5c7b987..922af3a8 100644
--- a/src/opt/mfs/mfsStrash.c
+++ b/src/opt/mfs/mfsStrash.c
@@ -367,7 +367,7 @@ Aig_Man_t * Abc_NtkAigForConstraints( Mfs_Man_t * p, Abc_Obj_t * pNode )
 
 ABC_NAMESPACE_IMPL_END
 
-#include "fra.h"
+#include "src/proof/fra/fra.h"
 
 ABC_NAMESPACE_IMPL_START