Version abc60115

26 files changed, 3597 insertions, 1298 deletions

diff --git a/abc.dsp b/abc.dsp
index fadbc83c..e322aca8 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -1045,6 +1045,70 @@ SOURCE=.\src\sat\csat\csat_apis.c
 SOURCE=.\src\sat\csat\csat_apis.h
 # End Source File
 # End Group
+# Begin Group "aig"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aig.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigBalance.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigNode.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigOper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigReplace.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\aigUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\fraigClass.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\fraigCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\fraigProve.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\aig\fraigSim.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "opt"
 
diff --git a/abc.opt b/abc.opt
index b6e9637f..a7f59668 100644
--- a/abc.opt
+++ b/abc.opt
diff --git a/abc.plg b/abc.plg
index 17867ca9..4871060b 100644
--- a/abc.plg
+++ b/abc.plg
@@ -6,13 +6,13 @@
 --------------------Configuration: abc - Win32 Debug--------------------
 </h3>
 <h3>Command Lines</h3>
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14F9.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FE.tmp" with contents
 [
 /nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c 
-"C:\_projects\abc\src\opt\xyz\xyzCore.c"
+"C:\_projects\abc\src\sat\aig\aigReplace.c"
 ]
-Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14F9.tmp" 
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FA.tmp" with contents
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FE.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FF.tmp" with contents
 [
 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:yes /pdb:"Debug/abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept 
 .\Debug\abcAig.obj
@@ -187,6 +187,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\msatClause.obj
 .\Debug\msatClauseVec.obj
 .\Debug\msatMem.obj
+.\Debug\msatOrderJ.obj
 .\Debug\msatQueue.obj
 .\Debug\msatRead.obj
 .\Debug\msatSolverApi.obj
@@ -208,6 +209,13 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\fraigUtil.obj
 .\Debug\fraigVec.obj
 .\Debug\csat_apis.obj
+.\Debug\aigBalance.obj
+.\Debug\aigFanout.obj
+.\Debug\aigMan.obj
+.\Debug\aigMem.obj
+.\Debug\aigNode.obj
+.\Debug\aigOper.obj
+.\Debug\aigUtil.obj
 .\Debug\fxu.obj
 .\Debug\fxuCreate.obj
 .\Debug\fxuHeapD.obj
@@ -338,14 +346,20 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\mvcPrint.obj
 .\Debug\mvcSort.obj
 .\Debug\mvcUtils.obj
-.\Debug\msatOrderJ.obj
+.\Debug\aigTable.obj
+.\Debug\aigCheck.obj
+.\Debug\aigReplace.obj
+.\Debug\fraigCore.obj
+.\Debug\fraigProve.obj
+.\Debug\fraigSim.obj
+.\Debug\fraigClass.obj
 ]
-Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FA.tmp"
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FF.tmp"
 <h3>Output Window</h3>
 Compiling...
-xyzCore.c
+aigReplace.c
 Linking...
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp" with contents
 [
 /nologo /o"Debug/abc.bsc" 
 .\Debug\abcAig.sbr
@@ -520,6 +534,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with cont
 .\Debug\msatClause.sbr
 .\Debug\msatClauseVec.sbr
 .\Debug\msatMem.sbr
+.\Debug\msatOrderJ.sbr
 .\Debug\msatQueue.sbr
 .\Debug\msatRead.sbr
 .\Debug\msatSolverApi.sbr
@@ -541,6 +556,13 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with cont
 .\Debug\fraigUtil.sbr
 .\Debug\fraigVec.sbr
 .\Debug\csat_apis.sbr
+.\Debug\aigBalance.sbr
+.\Debug\aigFanout.sbr
+.\Debug\aigMan.sbr
+.\Debug\aigMem.sbr
+.\Debug\aigNode.sbr
+.\Debug\aigOper.sbr
+.\Debug\aigUtil.sbr
 .\Debug\fxu.sbr
 .\Debug\fxuCreate.sbr
 .\Debug\fxuHeapD.sbr
@@ -671,8 +693,14 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with cont
 .\Debug\mvcPrint.sbr
 .\Debug\mvcSort.sbr
 .\Debug\mvcUtils.sbr
-.\Debug\msatOrderJ.sbr]
-Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp"
+.\Debug\aigTable.sbr
+.\Debug\aigCheck.sbr
+.\Debug\aigReplace.sbr
+.\Debug\fraigCore.sbr
+.\Debug\fraigProve.sbr
+.\Debug\fraigSim.sbr
+.\Debug\fraigClass.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp"
 Creating browse info file...
 <h3>Output Window</h3>
 
diff --git a/abclib.dsp b/abclib.dsp
index 999b7aab..b2c0fb7a 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -457,6 +457,10 @@ SOURCE=.\src\base\io\ioWriteList.c
 
 SOURCE=.\src\base\io\ioWritePla.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteVerilog.c
+# End Source File
 # End Group
 # Begin Group "main"
 
diff --git a/abclib.opt b/abclib.opt
index ac49ca90..a13d7236 100644
--- a/abclib.opt
+++ b/abclib.opt
diff --git a/abclib.plg b/abclib.plg
index de81adb8..67c7c8bb 100644
--- a/abclib.plg
+++ b/abclib.plg
@@ -3,1308 +3,670 @@
 <pre>
 <h1>Build Log</h1>
 <h3>
---------------------Configuration: abclib - Win32 Release--------------------
+--------------------Configuration: abclib - Win32 Debug--------------------
 </h3>
 <h3>Command Lines</h3>
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP82.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F0.tmp" with contents
 [
-/nologo /ML /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"abclib\ReleaseLib/" /Fp"abclib\ReleaseLib/abclib.pch" /YX /Fo"abclib\ReleaseLib/" /Fd"abclib\ReleaseLib/" /FD /c 
-"C:\_projects\abc\src\base\abc\abcAig.c"
-"C:\_projects\abc\src\base\abc\abcCheck.c"
-"C:\_projects\abc\src\base\abc\abcDfs.c"
-"C:\_projects\abc\src\base\abc\abcFanio.c"
-"C:\_projects\abc\src\base\abc\abcFunc.c"
-"C:\_projects\abc\src\base\abc\abcLatch.c"
-"C:\_projects\abc\src\base\abc\abcMinBase.c"
-"C:\_projects\abc\src\base\abc\abcNames.c"
-"C:\_projects\abc\src\base\abc\abcNetlist.c"
-"C:\_projects\abc\src\base\abc\abcNtk.c"
-"C:\_projects\abc\src\base\abc\abcObj.c"
-"C:\_projects\abc\src\base\abc\abcRefs.c"
-"C:\_projects\abc\src\base\abc\abcShow.c"
-"C:\_projects\abc\src\base\abc\abcSop.c"
-"C:\_projects\abc\src\base\abc\abcUtil.c"
+/nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"abclib\DebugLib/" /Fp"abclib\DebugLib/abclib.pch" /YX /Fo"abclib\DebugLib/" /Fd"abclib\DebugLib/" /FD /GZ /c 
 "C:\_projects\abc\src\base\abci\abc.c"
-"C:\_projects\abc\src\base\abci\abcAttach.c"
-"C:\_projects\abc\src\base\abci\abcBalance.c"
-"C:\_projects\abc\src\base\abci\abcCollapse.c"
-"C:\_projects\abc\src\base\abci\abcCut.c"
-"C:\_projects\abc\src\base\abci\abcDsd.c"
-"C:\_projects\abc\src\base\abci\abcFpga.c"
-"C:\_projects\abc\src\base\abci\abcFraig.c"
-"C:\_projects\abc\src\base\abci\abcFxu.c"
-"C:\_projects\abc\src\base\abci\abcMap.c"
-"C:\_projects\abc\src\base\abci\abcMiter.c"
-"C:\_projects\abc\src\base\abci\abcNtbdd.c"
-"C:\_projects\abc\src\base\abci\abcPga.c"
-"C:\_projects\abc\src\base\abci\abcPrint.c"
-"C:\_projects\abc\src\base\abci\abcReconv.c"
-"C:\_projects\abc\src\base\abci\abcRefactor.c"
-"C:\_projects\abc\src\base\abci\abcRenode.c"
-"C:\_projects\abc\src\base\abci\abcRewrite.c"
-"C:\_projects\abc\src\base\abci\abcSat.c"
-"C:\_projects\abc\src\base\abci\abcStrash.c"
-"C:\_projects\abc\src\base\abci\abcSweep.c"
-"C:\_projects\abc\src\base\abci\abcSymm.c"
-"C:\_projects\abc\src\base\abci\abcTiming.c"
-"C:\_projects\abc\src\base\abci\abcUnreach.c"
-"C:\_projects\abc\src\base\abci\abcVanEijk.c"
-"C:\_projects\abc\src\base\abci\abcVanImp.c"
-"C:\_projects\abc\src\base\abci\abcVerify.c"
-"C:\_projects\abc\src\base\seq\seqAigCore.c"
-"C:\_projects\abc\src\base\seq\seqAigIter.c"
-"C:\_projects\abc\src\base\seq\seqCreate.c"
-"C:\_projects\abc\src\base\seq\seqFpgaCore.c"
-"C:\_projects\abc\src\base\seq\seqFpgaIter.c"
-"C:\_projects\abc\src\base\seq\seqLatch.c"
-"C:\_projects\abc\src\base\seq\seqMan.c"
-"C:\_projects\abc\src\base\seq\seqMapCore.c"
-"C:\_projects\abc\src\base\seq\seqMapIter.c"
-"C:\_projects\abc\src\base\seq\seqRetCore.c"
-"C:\_projects\abc\src\base\seq\seqRetIter.c"
-"C:\_projects\abc\src\base\seq\seqShare.c"
-"C:\_projects\abc\src\base\seq\seqUtil.c"
-"C:\_projects\abc\src\base\cmd\cmd.c"
-"C:\_projects\abc\src\base\cmd\cmdAlias.c"
-"C:\_projects\abc\src\base\cmd\cmdApi.c"
-"C:\_projects\abc\src\base\cmd\cmdFlag.c"
-"C:\_projects\abc\src\base\cmd\cmdHist.c"
-"C:\_projects\abc\src\base\cmd\cmdUtils.c"
-"C:\_projects\abc\src\base\io\io.c"
-"C:\_projects\abc\src\base\io\ioRead.c"
-"C:\_projects\abc\src\base\io\ioReadBaf.c"
-"C:\_projects\abc\src\base\io\ioReadBench.c"
-"C:\_projects\abc\src\base\io\ioReadBlif.c"
-"C:\_projects\abc\src\base\io\ioReadEdif.c"
-"C:\_projects\abc\src\base\io\ioReadEqn.c"
-"C:\_projects\abc\src\base\io\ioReadPla.c"
-"C:\_projects\abc\src\base\io\ioReadVerilog.c"
-"C:\_projects\abc\src\base\io\ioUtil.c"
-"C:\_projects\abc\src\base\io\ioWriteBaf.c"
-"C:\_projects\abc\src\base\io\ioWriteBench.c"
-"C:\_projects\abc\src\base\io\ioWriteBlif.c"
-"C:\_projects\abc\src\base\io\ioWriteCnf.c"
-"C:\_projects\abc\src\base\io\ioWriteDot.c"
-"C:\_projects\abc\src\base\io\ioWriteEqn.c"
-"C:\_projects\abc\src\base\io\ioWriteGml.c"
-"C:\_projects\abc\src\base\io\ioWriteList.c"
-"C:\_projects\abc\src\base\io\ioWritePla.c"
-"C:\_projects\abc\src\base\main\libSupport.c"
-"C:\_projects\abc\src\base\main\main.c"
-"C:\_projects\abc\src\base\main\mainFrame.c"
-"C:\_projects\abc\src\base\main\mainInit.c"
-"C:\_projects\abc\src\base\main\mainUtils.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddAbs.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddApply.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddFind.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddInv.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddIte.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddNeg.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAddWalsh.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAndAbs.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAnneal.c"
-"C:\_projects\abc\src\bdd\cudd\cuddApa.c"
-"C:\_projects\abc\src\bdd\cudd\cuddAPI.c"
-"C:\_projects\abc\src\bdd\cudd\cuddApprox.c"
-"C:\_projects\abc\src\bdd\cudd\cuddBddAbs.c"
-"C:\_projects\abc\src\bdd\cudd\cuddBddCorr.c"
-"C:\_projects\abc\src\bdd\cudd\cuddBddIte.c"
-"C:\_projects\abc\src\bdd\cudd\cuddBridge.c"
-"C:\_projects\abc\src\bdd\cudd\cuddCache.c"
-"C:\_projects\abc\src\bdd\cudd\cuddCheck.c"
-"C:\_projects\abc\src\bdd\cudd\cuddClip.c"
-"C:\_projects\abc\src\bdd\cudd\cuddCof.c"
-"C:\_projects\abc\src\bdd\cudd\cuddCompose.c"
-"C:\_projects\abc\src\bdd\cudd\cuddDecomp.c"
-"C:\_projects\abc\src\bdd\cudd\cuddEssent.c"
-"C:\_projects\abc\src\bdd\cudd\cuddExact.c"
-"C:\_projects\abc\src\bdd\cudd\cuddExport.c"
-"C:\_projects\abc\src\bdd\cudd\cuddGenCof.c"
-"C:\_projects\abc\src\bdd\cudd\cuddGenetic.c"
-"C:\_projects\abc\src\bdd\cudd\cuddGroup.c"
-"C:\_projects\abc\src\bdd\cudd\cuddHarwell.c"
-"C:\_projects\abc\src\bdd\cudd\cuddInit.c"
-"C:\_projects\abc\src\bdd\cudd\cuddInteract.c"
-"C:\_projects\abc\src\bdd\cudd\cuddLCache.c"
-"C:\_projects\abc\src\bdd\cudd\cuddLevelQ.c"
-"C:\_projects\abc\src\bdd\cudd\cuddLinear.c"
-"C:\_projects\abc\src\bdd\cudd\cuddLiteral.c"
-"C:\_projects\abc\src\bdd\cudd\cuddMatMult.c"
-"C:\_projects\abc\src\bdd\cudd\cuddPriority.c"
-"C:\_projects\abc\src\bdd\cudd\cuddRead.c"
-"C:\_projects\abc\src\bdd\cudd\cuddRef.c"
-"C:\_projects\abc\src\bdd\cudd\cuddReorder.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSat.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSign.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSolve.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSplit.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSubsetHB.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSubsetSP.c"
-"C:\_projects\abc\src\bdd\cudd\cuddSymmetry.c"
-"C:\_projects\abc\src\bdd\cudd\cuddTable.c"
-"C:\_projects\abc\src\bdd\cudd\cuddUtil.c"
-"C:\_projects\abc\src\bdd\cudd\cuddWindow.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddCount.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddFuncs.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddGroup.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddIsop.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddLin.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddMisc.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddPort.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddReord.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddSetop.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddSymm.c"
-"C:\_projects\abc\src\bdd\cudd\cuddZddUtil.c"
-"C:\_projects\abc\src\bdd\epd\epd.c"
-"C:\_projects\abc\src\bdd\mtr\mtrBasic.c"
-"C:\_projects\abc\src\bdd\mtr\mtrGroup.c"
-"C:\_projects\abc\src\bdd\parse\parseCore.c"
-"C:\_projects\abc\src\bdd\parse\parseStack.c"
-"C:\_projects\abc\src\bdd\dsd\dsdApi.c"
-"C:\_projects\abc\src\bdd\dsd\dsdCheck.c"
-"C:\_projects\abc\src\bdd\dsd\dsdLocal.c"
-"C:\_projects\abc\src\bdd\dsd\dsdMan.c"
-"C:\_projects\abc\src\bdd\dsd\dsdProc.c"
-"C:\_projects\abc\src\bdd\dsd\dsdTree.c"
-"C:\_projects\abc\src\bdd\reo\reoApi.c"
-"C:\_projects\abc\src\bdd\reo\reoCore.c"
-"C:\_projects\abc\src\bdd\reo\reoProfile.c"
-"C:\_projects\abc\src\bdd\reo\reoSift.c"
-"C:\_projects\abc\src\bdd\reo\reoSwap.c"
-"C:\_projects\abc\src\bdd\reo\reoTest.c"
-"C:\_projects\abc\src\bdd\reo\reoTransfer.c"
-"C:\_projects\abc\src\bdd\reo\reoUnits.c"
-"C:\_projects\abc\src\sat\asat\added.c"
-"C:\_projects\abc\src\sat\asat\solver.c"
-"C:\_projects\abc\src\sat\msat\msatActivity.c"
-"C:\_projects\abc\src\sat\msat\msatClause.c"
-"C:\_projects\abc\src\sat\msat\msatClauseVec.c"
-"C:\_projects\abc\src\sat\msat\msatMem.c"
-"C:\_projects\abc\src\sat\msat\msatOrderJ.c"
-"C:\_projects\abc\src\sat\msat\msatQueue.c"
-"C:\_projects\abc\src\sat\msat\msatRead.c"
-"C:\_projects\abc\src\sat\msat\msatSolverApi.c"
-"C:\_projects\abc\src\sat\msat\msatSolverCore.c"
-"C:\_projects\abc\src\sat\msat\msatSolverIo.c"
-"C:\_projects\abc\src\sat\msat\msatSolverSearch.c"
-"C:\_projects\abc\src\sat\msat\msatSort.c"
-"C:\_projects\abc\src\sat\msat\msatVec.c"
-"C:\_projects\abc\src\sat\fraig\fraigApi.c"
-"C:\_projects\abc\src\sat\fraig\fraigCanon.c"
-"C:\_projects\abc\src\sat\fraig\fraigFanout.c"
-"C:\_projects\abc\src\sat\fraig\fraigFeed.c"
-"C:\_projects\abc\src\sat\fraig\fraigMan.c"
-"C:\_projects\abc\src\sat\fraig\fraigMem.c"
-"C:\_projects\abc\src\sat\fraig\fraigNode.c"
-"C:\_projects\abc\src\sat\fraig\fraigPrime.c"
-"C:\_projects\abc\src\sat\fraig\fraigSat.c"
-"C:\_projects\abc\src\sat\fraig\fraigTable.c"
-"C:\_projects\abc\src\sat\fraig\fraigUtil.c"
-"C:\_projects\abc\src\sat\fraig\fraigVec.c"
-"C:\_projects\abc\src\sat\csat\csat_apis.c"
-"C:\_projects\abc\src\opt\fxu\fxu.c"
-"C:\_projects\abc\src\opt\fxu\fxuCreate.c"
-"C:\_projects\abc\src\opt\fxu\fxuHeapD.c"
-"C:\_projects\abc\src\opt\fxu\fxuHeapS.c"
-"C:\_projects\abc\src\opt\fxu\fxuList.c"
-"C:\_projects\abc\src\opt\fxu\fxuMatrix.c"
-"C:\_projects\abc\src\opt\fxu\fxuPair.c"
-"C:\_projects\abc\src\opt\fxu\fxuPrint.c"
-"C:\_projects\abc\src\opt\fxu\fxuReduce.c"
-"C:\_projects\abc\src\opt\fxu\fxuSelect.c"
-"C:\_projects\abc\src\opt\fxu\fxuSingle.c"
-"C:\_projects\abc\src\opt\fxu\fxuUpdate.c"
-"C:\_projects\abc\src\opt\rwr\rwrDec.c"
-"C:\_projects\abc\src\opt\rwr\rwrEva.c"
-"C:\_projects\abc\src\opt\rwr\rwrExp.c"
-"C:\_projects\abc\src\opt\rwr\rwrLib.c"
-"C:\_projects\abc\src\opt\rwr\rwrMan.c"
-"C:\_projects\abc\src\opt\rwr\rwrPrint.c"
-"C:\_projects\abc\src\opt\rwr\rwrUtil.c"
-"C:\_projects\abc\src\opt\cut\cutApi.c"
-"C:\_projects\abc\src\opt\cut\cutCut.c"
-"C:\_projects\abc\src\opt\cut\cutMan.c"
-"C:\_projects\abc\src\opt\cut\cutMerge.c"
-"C:\_projects\abc\src\opt\cut\cutNode.c"
-"C:\_projects\abc\src\opt\cut\cutOracle.c"
-"C:\_projects\abc\src\opt\cut\cutSeq.c"
-"C:\_projects\abc\src\opt\cut\cutTruth.c"
-"C:\_projects\abc\src\opt\dec\decAbc.c"
-"C:\_projects\abc\src\opt\dec\decFactor.c"
-"C:\_projects\abc\src\opt\dec\decMan.c"
-"C:\_projects\abc\src\opt\dec\decPrint.c"
-"C:\_projects\abc\src\opt\dec\decUtil.c"
-"C:\_projects\abc\src\opt\sim\simMan.c"
-"C:\_projects\abc\src\opt\sim\simSat.c"
-"C:\_projects\abc\src\opt\sim\simSeq.c"
-"C:\_projects\abc\src\opt\sim\simSupp.c"
-"C:\_projects\abc\src\opt\sim\simSwitch.c"
-"C:\_projects\abc\src\opt\sim\simSym.c"
-"C:\_projects\abc\src\opt\sim\simSymSat.c"
-"C:\_projects\abc\src\opt\sim\simSymSim.c"
-"C:\_projects\abc\src\opt\sim\simSymStr.c"
-"C:\_projects\abc\src\opt\sim\simUtils.c"
-"C:\_projects\abc\src\map\fpga\fpga.c"
-"C:\_projects\abc\src\map\fpga\fpgaCore.c"
-"C:\_projects\abc\src\map\fpga\fpgaCreate.c"
-"C:\_projects\abc\src\map\fpga\fpgaCut.c"
-"C:\_projects\abc\src\map\fpga\fpgaCutUtils.c"
-"C:\_projects\abc\src\map\fpga\fpgaFanout.c"
-"C:\_projects\abc\src\map\fpga\fpgaLib.c"
-"C:\_projects\abc\src\map\fpga\fpgaMatch.c"
-"C:\_projects\abc\src\map\fpga\fpgaSwitch.c"
-"C:\_projects\abc\src\map\fpga\fpgaTime.c"
-"C:\_projects\abc\src\map\fpga\fpgaTruth.c"
-"C:\_projects\abc\src\map\fpga\fpgaUtils.c"
-"C:\_projects\abc\src\map\fpga\fpgaVec.c"
-"C:\_projects\abc\src\map\mapper\mapper.c"
-"C:\_projects\abc\src\map\mapper\mapperCanon.c"
-"C:\_projects\abc\src\map\mapper\mapperCore.c"
-"C:\_projects\abc\src\map\mapper\mapperCreate.c"
-"C:\_projects\abc\src\map\mapper\mapperCut.c"
-"C:\_projects\abc\src\map\mapper\mapperCutUtils.c"
-"C:\_projects\abc\src\map\mapper\mapperFanout.c"
-"C:\_projects\abc\src\map\mapper\mapperLib.c"
-"C:\_projects\abc\src\map\mapper\mapperMatch.c"
-"C:\_projects\abc\src\map\mapper\mapperRefs.c"
-"C:\_projects\abc\src\map\mapper\mapperSuper.c"
-"C:\_projects\abc\src\map\mapper\mapperSwitch.c"
-"C:\_projects\abc\src\map\mapper\mapperTable.c"
-"C:\_projects\abc\src\map\mapper\mapperTime.c"
-"C:\_projects\abc\src\map\mapper\mapperTree.c"
-"C:\_projects\abc\src\map\mapper\mapperTruth.c"
-"C:\_projects\abc\src\map\mapper\mapperUtils.c"
-"C:\_projects\abc\src\map\mapper\mapperVec.c"
-"C:\_projects\abc\src\map\mio\mio.c"
-"C:\_projects\abc\src\map\mio\mioApi.c"
-"C:\_projects\abc\src\map\mio\mioFunc.c"
-"C:\_projects\abc\src\map\mio\mioRead.c"
-"C:\_projects\abc\src\map\mio\mioUtils.c"
-"C:\_projects\abc\src\map\super\super.c"
-"C:\_projects\abc\src\map\super\superAnd.c"
-"C:\_projects\abc\src\map\super\superGate.c"
-"C:\_projects\abc\src\map\super\superWrite.c"
-"C:\_projects\abc\src\map\pga\pgaCore.c"
-"C:\_projects\abc\src\map\pga\pgaMan.c"
-"C:\_projects\abc\src\map\pga\pgaMatch.c"
-"C:\_projects\abc\src\map\pga\pgaUtil.c"
-"C:\_projects\abc\src\misc\extra\extraBddKmap.c"
-"C:\_projects\abc\src\misc\extra\extraBddMisc.c"
-"C:\_projects\abc\src\misc\extra\extraBddSymm.c"
-"C:\_projects\abc\src\misc\extra\extraUtilBitMatrix.c"
-"C:\_projects\abc\src\misc\extra\extraUtilCanon.c"
-"C:\_projects\abc\src\misc\extra\extraUtilFile.c"
-"C:\_projects\abc\src\misc\extra\extraUtilMemory.c"
-"C:\_projects\abc\src\misc\extra\extraUtilMisc.c"
-"C:\_projects\abc\src\misc\extra\extraUtilProgress.c"
-"C:\_projects\abc\src\misc\extra\extraUtilReader.c"
-"C:\_projects\abc\src\misc\st\st.c"
-"C:\_projects\abc\src\misc\st\stmm.c"
-"C:\_projects\abc\src\misc\util\cpu_stats.c"
-"C:\_projects\abc\src\misc\util\cpu_time.c"
-"C:\_projects\abc\src\misc\util\datalimit.c"
-"C:\_projects\abc\src\misc\util\getopt.c"
-"C:\_projects\abc\src\misc\util\pathsearch.c"
-"C:\_projects\abc\src\misc\util\safe_mem.c"
-"C:\_projects\abc\src\misc\util\strsav.c"
-"C:\_projects\abc\src\misc\util\texpand.c"
-"C:\_projects\abc\src\misc\mvc\mvc.c"
-"C:\_projects\abc\src\misc\mvc\mvcApi.c"
-"C:\_projects\abc\src\misc\mvc\mvcCompare.c"
-"C:\_projects\abc\src\misc\mvc\mvcContain.c"
-"C:\_projects\abc\src\misc\mvc\mvcCover.c"
-"C:\_projects\abc\src\misc\mvc\mvcCube.c"
-"C:\_projects\abc\src\misc\mvc\mvcDivide.c"
-"C:\_projects\abc\src\misc\mvc\mvcDivisor.c"
-"C:\_projects\abc\src\misc\mvc\mvcList.c"
-"C:\_projects\abc\src\misc\mvc\mvcLits.c"
-"C:\_projects\abc\src\misc\mvc\mvcMan.c"
-"C:\_projects\abc\src\misc\mvc\mvcOpAlg.c"
-"C:\_projects\abc\src\misc\mvc\mvcOpBool.c"
-"C:\_projects\abc\src\misc\mvc\mvcPrint.c"
-"C:\_projects\abc\src\misc\mvc\mvcSort.c"
-"C:\_projects\abc\src\misc\mvc\mvcUtils.c"
+"C:\_projects\abc\src\base\io\ioWriteVerilog.c"
 ]
-Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP82.tmp" 
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP83.tmp" with contents
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F0.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F1.tmp" with contents
 [
-/nologo /out:"abclib\abclib_release.lib" 
-.\abclib\ReleaseLib\abcAig.obj
-.\abclib\ReleaseLib\abcCheck.obj
-.\abclib\ReleaseLib\abcDfs.obj
-.\abclib\ReleaseLib\abcFanio.obj
-.\abclib\ReleaseLib\abcFunc.obj
-.\abclib\ReleaseLib\abcLatch.obj
-.\abclib\ReleaseLib\abcMinBase.obj
-.\abclib\ReleaseLib\abcNames.obj
-.\abclib\ReleaseLib\abcNetlist.obj
-.\abclib\ReleaseLib\abcNtk.obj
-.\abclib\ReleaseLib\abcObj.obj
-.\abclib\ReleaseLib\abcRefs.obj
-.\abclib\ReleaseLib\abcShow.obj
-.\abclib\ReleaseLib\abcSop.obj
-.\abclib\ReleaseLib\abcUtil.obj
-.\abclib\ReleaseLib\abc.obj
-.\abclib\ReleaseLib\abcAttach.obj
-.\abclib\ReleaseLib\abcBalance.obj
-.\abclib\ReleaseLib\abcCollapse.obj
-.\abclib\ReleaseLib\abcCut.obj
-.\abclib\ReleaseLib\abcDsd.obj
-.\abclib\ReleaseLib\abcFpga.obj
-.\abclib\ReleaseLib\abcFraig.obj
-.\abclib\ReleaseLib\abcFxu.obj
-.\abclib\ReleaseLib\abcMap.obj
-.\abclib\ReleaseLib\abcMiter.obj
-.\abclib\ReleaseLib\abcNtbdd.obj
-.\abclib\ReleaseLib\abcPga.obj
-.\abclib\ReleaseLib\abcPrint.obj
-.\abclib\ReleaseLib\abcReconv.obj
-.\abclib\ReleaseLib\abcRefactor.obj
-.\abclib\ReleaseLib\abcRenode.obj
-.\abclib\ReleaseLib\abcRewrite.obj
-.\abclib\ReleaseLib\abcSat.obj
-.\abclib\ReleaseLib\abcStrash.obj
-.\abclib\ReleaseLib\abcSweep.obj
-.\abclib\ReleaseLib\abcSymm.obj
-.\abclib\ReleaseLib\abcTiming.obj
-.\abclib\ReleaseLib\abcUnreach.obj
-.\abclib\ReleaseLib\abcVanEijk.obj
-.\abclib\ReleaseLib\abcVanImp.obj
-.\abclib\ReleaseLib\abcVerify.obj
-.\abclib\ReleaseLib\seqAigCore.obj
-.\abclib\ReleaseLib\seqAigIter.obj
-.\abclib\ReleaseLib\seqCreate.obj
-.\abclib\ReleaseLib\seqFpgaCore.obj
-.\abclib\ReleaseLib\seqFpgaIter.obj
-.\abclib\ReleaseLib\seqLatch.obj
-.\abclib\ReleaseLib\seqMan.obj
-.\abclib\ReleaseLib\seqMapCore.obj
-.\abclib\ReleaseLib\seqMapIter.obj
-.\abclib\ReleaseLib\seqRetCore.obj
-.\abclib\ReleaseLib\seqRetIter.obj
-.\abclib\ReleaseLib\seqShare.obj
-.\abclib\ReleaseLib\seqUtil.obj
-.\abclib\ReleaseLib\cmd.obj
-.\abclib\ReleaseLib\cmdAlias.obj
-.\abclib\ReleaseLib\cmdApi.obj
-.\abclib\ReleaseLib\cmdFlag.obj
-.\abclib\ReleaseLib\cmdHist.obj
-.\abclib\ReleaseLib\cmdUtils.obj
-.\abclib\ReleaseLib\io.obj
-.\abclib\ReleaseLib\ioRead.obj
-.\abclib\ReleaseLib\ioReadBaf.obj
-.\abclib\ReleaseLib\ioReadBench.obj
-.\abclib\ReleaseLib\ioReadBlif.obj
-.\abclib\ReleaseLib\ioReadEdif.obj
-.\abclib\ReleaseLib\ioReadEqn.obj
-.\abclib\ReleaseLib\ioReadPla.obj
-.\abclib\ReleaseLib\ioReadVerilog.obj
-.\abclib\ReleaseLib\ioUtil.obj
-.\abclib\ReleaseLib\ioWriteBaf.obj
-.\abclib\ReleaseLib\ioWriteBench.obj
-.\abclib\ReleaseLib\ioWriteBlif.obj
-.\abclib\ReleaseLib\ioWriteCnf.obj
-.\abclib\ReleaseLib\ioWriteDot.obj
-.\abclib\ReleaseLib\ioWriteEqn.obj
-.\abclib\ReleaseLib\ioWriteGml.obj
-.\abclib\ReleaseLib\ioWriteList.obj
-.\abclib\ReleaseLib\ioWritePla.obj
-.\abclib\ReleaseLib\libSupport.obj
-.\abclib\ReleaseLib\main.obj
-.\abclib\ReleaseLib\mainFrame.obj
-.\abclib\ReleaseLib\mainInit.obj
-.\abclib\ReleaseLib\mainUtils.obj
-.\abclib\ReleaseLib\cuddAddAbs.obj
-.\abclib\ReleaseLib\cuddAddApply.obj
-.\abclib\ReleaseLib\cuddAddFind.obj
-.\abclib\ReleaseLib\cuddAddInv.obj
-.\abclib\ReleaseLib\cuddAddIte.obj
-.\abclib\ReleaseLib\cuddAddNeg.obj
-.\abclib\ReleaseLib\cuddAddWalsh.obj
-.\abclib\ReleaseLib\cuddAndAbs.obj
-.\abclib\ReleaseLib\cuddAnneal.obj
-.\abclib\ReleaseLib\cuddApa.obj
-.\abclib\ReleaseLib\cuddAPI.obj
-.\abclib\ReleaseLib\cuddApprox.obj
-.\abclib\ReleaseLib\cuddBddAbs.obj
-.\abclib\ReleaseLib\cuddBddCorr.obj
-.\abclib\ReleaseLib\cuddBddIte.obj
-.\abclib\ReleaseLib\cuddBridge.obj
-.\abclib\ReleaseLib\cuddCache.obj
-.\abclib\ReleaseLib\cuddCheck.obj
-.\abclib\ReleaseLib\cuddClip.obj
-.\abclib\ReleaseLib\cuddCof.obj
-.\abclib\ReleaseLib\cuddCompose.obj
-.\abclib\ReleaseLib\cuddDecomp.obj
-.\abclib\ReleaseLib\cuddEssent.obj
-.\abclib\ReleaseLib\cuddExact.obj
-.\abclib\ReleaseLib\cuddExport.obj
-.\abclib\ReleaseLib\cuddGenCof.obj
-.\abclib\ReleaseLib\cuddGenetic.obj
-.\abclib\ReleaseLib\cuddGroup.obj
-.\abclib\ReleaseLib\cuddHarwell.obj
-.\abclib\ReleaseLib\cuddInit.obj
-.\abclib\ReleaseLib\cuddInteract.obj
-.\abclib\ReleaseLib\cuddLCache.obj
-.\abclib\ReleaseLib\cuddLevelQ.obj
-.\abclib\ReleaseLib\cuddLinear.obj
-.\abclib\ReleaseLib\cuddLiteral.obj
-.\abclib\ReleaseLib\cuddMatMult.obj
-.\abclib\ReleaseLib\cuddPriority.obj
-.\abclib\ReleaseLib\cuddRead.obj
-.\abclib\ReleaseLib\cuddRef.obj
-.\abclib\ReleaseLib\cuddReorder.obj
-.\abclib\ReleaseLib\cuddSat.obj
-.\abclib\ReleaseLib\cuddSign.obj
-.\abclib\ReleaseLib\cuddSolve.obj
-.\abclib\ReleaseLib\cuddSplit.obj
-.\abclib\ReleaseLib\cuddSubsetHB.obj
-.\abclib\ReleaseLib\cuddSubsetSP.obj
-.\abclib\ReleaseLib\cuddSymmetry.obj
-.\abclib\ReleaseLib\cuddTable.obj
-.\abclib\ReleaseLib\cuddUtil.obj
-.\abclib\ReleaseLib\cuddWindow.obj
-.\abclib\ReleaseLib\cuddZddCount.obj
-.\abclib\ReleaseLib\cuddZddFuncs.obj
-.\abclib\ReleaseLib\cuddZddGroup.obj
-.\abclib\ReleaseLib\cuddZddIsop.obj
-.\abclib\ReleaseLib\cuddZddLin.obj
-.\abclib\ReleaseLib\cuddZddMisc.obj
-.\abclib\ReleaseLib\cuddZddPort.obj
-.\abclib\ReleaseLib\cuddZddReord.obj
-.\abclib\ReleaseLib\cuddZddSetop.obj
-.\abclib\ReleaseLib\cuddZddSymm.obj
-.\abclib\ReleaseLib\cuddZddUtil.obj
-.\abclib\ReleaseLib\epd.obj
-.\abclib\ReleaseLib\mtrBasic.obj
-.\abclib\ReleaseLib\mtrGroup.obj
-.\abclib\ReleaseLib\parseCore.obj
-.\abclib\ReleaseLib\parseStack.obj
-.\abclib\ReleaseLib\dsdApi.obj
-.\abclib\ReleaseLib\dsdCheck.obj
-.\abclib\ReleaseLib\dsdLocal.obj
-.\abclib\ReleaseLib\dsdMan.obj
-.\abclib\ReleaseLib\dsdProc.obj
-.\abclib\ReleaseLib\dsdTree.obj
-.\abclib\ReleaseLib\reoApi.obj
-.\abclib\ReleaseLib\reoCore.obj
-.\abclib\ReleaseLib\reoProfile.obj
-.\abclib\ReleaseLib\reoSift.obj
-.\abclib\ReleaseLib\reoSwap.obj
-.\abclib\ReleaseLib\reoTest.obj
-.\abclib\ReleaseLib\reoTransfer.obj
-.\abclib\ReleaseLib\reoUnits.obj
-.\abclib\ReleaseLib\added.obj
-.\abclib\ReleaseLib\solver.obj
-.\abclib\ReleaseLib\msatActivity.obj
-.\abclib\ReleaseLib\msatClause.obj
-.\abclib\ReleaseLib\msatClauseVec.obj
-.\abclib\ReleaseLib\msatMem.obj
-.\abclib\ReleaseLib\msatOrderJ.obj
-.\abclib\ReleaseLib\msatQueue.obj
-.\abclib\ReleaseLib\msatRead.obj
-.\abclib\ReleaseLib\msatSolverApi.obj
-.\abclib\ReleaseLib\msatSolverCore.obj
-.\abclib\ReleaseLib\msatSolverIo.obj
-.\abclib\ReleaseLib\msatSolverSearch.obj
-.\abclib\ReleaseLib\msatSort.obj
-.\abclib\ReleaseLib\msatVec.obj
-.\abclib\ReleaseLib\fraigApi.obj
-.\abclib\ReleaseLib\fraigCanon.obj
-.\abclib\ReleaseLib\fraigFanout.obj
-.\abclib\ReleaseLib\fraigFeed.obj
-.\abclib\ReleaseLib\fraigMan.obj
-.\abclib\ReleaseLib\fraigMem.obj
-.\abclib\ReleaseLib\fraigNode.obj
-.\abclib\ReleaseLib\fraigPrime.obj
-.\abclib\ReleaseLib\fraigSat.obj
-.\abclib\ReleaseLib\fraigTable.obj
-.\abclib\ReleaseLib\fraigUtil.obj
-.\abclib\ReleaseLib\fraigVec.obj
-.\abclib\ReleaseLib\csat_apis.obj
-.\abclib\ReleaseLib\fxu.obj
-.\abclib\ReleaseLib\fxuCreate.obj
-.\abclib\ReleaseLib\fxuHeapD.obj
-.\abclib\ReleaseLib\fxuHeapS.obj
-.\abclib\ReleaseLib\fxuList.obj
-.\abclib\ReleaseLib\fxuMatrix.obj
-.\abclib\ReleaseLib\fxuPair.obj
-.\abclib\ReleaseLib\fxuPrint.obj
-.\abclib\ReleaseLib\fxuReduce.obj
-.\abclib\ReleaseLib\fxuSelect.obj
-.\abclib\ReleaseLib\fxuSingle.obj
-.\abclib\ReleaseLib\fxuUpdate.obj
-.\abclib\ReleaseLib\rwrDec.obj
-.\abclib\ReleaseLib\rwrEva.obj
-.\abclib\ReleaseLib\rwrExp.obj
-.\abclib\ReleaseLib\rwrLib.obj
-.\abclib\ReleaseLib\rwrMan.obj
-.\abclib\ReleaseLib\rwrPrint.obj
-.\abclib\ReleaseLib\rwrUtil.obj
-.\abclib\ReleaseLib\cutApi.obj
-.\abclib\ReleaseLib\cutCut.obj
-.\abclib\ReleaseLib\cutMan.obj
-.\abclib\ReleaseLib\cutMerge.obj
-.\abclib\ReleaseLib\cutNode.obj
-.\abclib\ReleaseLib\cutOracle.obj
-.\abclib\ReleaseLib\cutSeq.obj
-.\abclib\ReleaseLib\cutTruth.obj
-.\abclib\ReleaseLib\decAbc.obj
-.\abclib\ReleaseLib\decFactor.obj
-.\abclib\ReleaseLib\decMan.obj
-.\abclib\ReleaseLib\decPrint.obj
-.\abclib\ReleaseLib\decUtil.obj
-.\abclib\ReleaseLib\simMan.obj
-.\abclib\ReleaseLib\simSat.obj
-.\abclib\ReleaseLib\simSeq.obj
-.\abclib\ReleaseLib\simSupp.obj
-.\abclib\ReleaseLib\simSwitch.obj
-.\abclib\ReleaseLib\simSym.obj
-.\abclib\ReleaseLib\simSymSat.obj
-.\abclib\ReleaseLib\simSymSim.obj
-.\abclib\ReleaseLib\simSymStr.obj
-.\abclib\ReleaseLib\simUtils.obj
-.\abclib\ReleaseLib\fpga.obj
-.\abclib\ReleaseLib\fpgaCore.obj
-.\abclib\ReleaseLib\fpgaCreate.obj
-.\abclib\ReleaseLib\fpgaCut.obj
-.\abclib\ReleaseLib\fpgaCutUtils.obj
-.\abclib\ReleaseLib\fpgaFanout.obj
-.\abclib\ReleaseLib\fpgaLib.obj
-.\abclib\ReleaseLib\fpgaMatch.obj
-.\abclib\ReleaseLib\fpgaSwitch.obj
-.\abclib\ReleaseLib\fpgaTime.obj
-.\abclib\ReleaseLib\fpgaTruth.obj
-.\abclib\ReleaseLib\fpgaUtils.obj
-.\abclib\ReleaseLib\fpgaVec.obj
-.\abclib\ReleaseLib\mapper.obj
-.\abclib\ReleaseLib\mapperCanon.obj
-.\abclib\ReleaseLib\mapperCore.obj
-.\abclib\ReleaseLib\mapperCreate.obj
-.\abclib\ReleaseLib\mapperCut.obj
-.\abclib\ReleaseLib\mapperCutUtils.obj
-.\abclib\ReleaseLib\mapperFanout.obj
-.\abclib\ReleaseLib\mapperLib.obj
-.\abclib\ReleaseLib\mapperMatch.obj
-.\abclib\ReleaseLib\mapperRefs.obj
-.\abclib\ReleaseLib\mapperSuper.obj
-.\abclib\ReleaseLib\mapperSwitch.obj
-.\abclib\ReleaseLib\mapperTable.obj
-.\abclib\ReleaseLib\mapperTime.obj
-.\abclib\ReleaseLib\mapperTree.obj
-.\abclib\ReleaseLib\mapperTruth.obj
-.\abclib\ReleaseLib\mapperUtils.obj
-.\abclib\ReleaseLib\mapperVec.obj
-.\abclib\ReleaseLib\mio.obj
-.\abclib\ReleaseLib\mioApi.obj
-.\abclib\ReleaseLib\mioFunc.obj
-.\abclib\ReleaseLib\mioRead.obj
-.\abclib\ReleaseLib\mioUtils.obj
-.\abclib\ReleaseLib\super.obj
-.\abclib\ReleaseLib\superAnd.obj
-.\abclib\ReleaseLib\superGate.obj
-.\abclib\ReleaseLib\superWrite.obj
-.\abclib\ReleaseLib\pgaCore.obj
-.\abclib\ReleaseLib\pgaMan.obj
-.\abclib\ReleaseLib\pgaMatch.obj
-.\abclib\ReleaseLib\pgaUtil.obj
-.\abclib\ReleaseLib\extraBddKmap.obj
-.\abclib\ReleaseLib\extraBddMisc.obj
-.\abclib\ReleaseLib\extraBddSymm.obj
-.\abclib\ReleaseLib\extraUtilBitMatrix.obj
-.\abclib\ReleaseLib\extraUtilCanon.obj
-.\abclib\ReleaseLib\extraUtilFile.obj
-.\abclib\ReleaseLib\extraUtilMemory.obj
-.\abclib\ReleaseLib\extraUtilMisc.obj
-.\abclib\ReleaseLib\extraUtilProgress.obj
-.\abclib\ReleaseLib\extraUtilReader.obj
-.\abclib\ReleaseLib\st.obj
-.\abclib\ReleaseLib\stmm.obj
-.\abclib\ReleaseLib\cpu_stats.obj
-.\abclib\ReleaseLib\cpu_time.obj
-.\abclib\ReleaseLib\datalimit.obj
-.\abclib\ReleaseLib\getopt.obj
-.\abclib\ReleaseLib\pathsearch.obj
-.\abclib\ReleaseLib\safe_mem.obj
-.\abclib\ReleaseLib\strsav.obj
-.\abclib\ReleaseLib\texpand.obj
-.\abclib\ReleaseLib\mvc.obj
-.\abclib\ReleaseLib\mvcApi.obj
-.\abclib\ReleaseLib\mvcCompare.obj
-.\abclib\ReleaseLib\mvcContain.obj
-.\abclib\ReleaseLib\mvcCover.obj
-.\abclib\ReleaseLib\mvcCube.obj
-.\abclib\ReleaseLib\mvcDivide.obj
-.\abclib\ReleaseLib\mvcDivisor.obj
-.\abclib\ReleaseLib\mvcList.obj
-.\abclib\ReleaseLib\mvcLits.obj
-.\abclib\ReleaseLib\mvcMan.obj
-.\abclib\ReleaseLib\mvcOpAlg.obj
-.\abclib\ReleaseLib\mvcOpBool.obj
-.\abclib\ReleaseLib\mvcPrint.obj
-.\abclib\ReleaseLib\mvcSort.obj
-.\abclib\ReleaseLib\mvcUtils.obj
+/nologo /out:"abclib\abclib_debug.lib" 
+.\abclib\DebugLib\abcAig.obj
+.\abclib\DebugLib\abcCheck.obj
+.\abclib\DebugLib\abcDfs.obj
+.\abclib\DebugLib\abcFanio.obj
+.\abclib\DebugLib\abcFunc.obj
+.\abclib\DebugLib\abcLatch.obj
+.\abclib\DebugLib\abcMinBase.obj
+.\abclib\DebugLib\abcNames.obj
+.\abclib\DebugLib\abcNetlist.obj
+.\abclib\DebugLib\abcNtk.obj
+.\abclib\DebugLib\abcObj.obj
+.\abclib\DebugLib\abcRefs.obj
+.\abclib\DebugLib\abcShow.obj
+.\abclib\DebugLib\abcSop.obj
+.\abclib\DebugLib\abcUtil.obj
+.\abclib\DebugLib\abc.obj
+.\abclib\DebugLib\abcAttach.obj
+.\abclib\DebugLib\abcBalance.obj
+.\abclib\DebugLib\abcCollapse.obj
+.\abclib\DebugLib\abcCut.obj
+.\abclib\DebugLib\abcDsd.obj
+.\abclib\DebugLib\abcFpga.obj
+.\abclib\DebugLib\abcFraig.obj
+.\abclib\DebugLib\abcFxu.obj
+.\abclib\DebugLib\abcMap.obj
+.\abclib\DebugLib\abcMiter.obj
+.\abclib\DebugLib\abcNtbdd.obj
+.\abclib\DebugLib\abcPga.obj
+.\abclib\DebugLib\abcPrint.obj
+.\abclib\DebugLib\abcReconv.obj
+.\abclib\DebugLib\abcRefactor.obj
+.\abclib\DebugLib\abcRenode.obj
+.\abclib\DebugLib\abcRewrite.obj
+.\abclib\DebugLib\abcSat.obj
+.\abclib\DebugLib\abcStrash.obj
+.\abclib\DebugLib\abcSweep.obj
+.\abclib\DebugLib\abcSymm.obj
+.\abclib\DebugLib\abcTiming.obj
+.\abclib\DebugLib\abcUnreach.obj
+.\abclib\DebugLib\abcVanEijk.obj
+.\abclib\DebugLib\abcVanImp.obj
+.\abclib\DebugLib\abcVerify.obj
+.\abclib\DebugLib\seqAigCore.obj
+.\abclib\DebugLib\seqAigIter.obj
+.\abclib\DebugLib\seqCreate.obj
+.\abclib\DebugLib\seqFpgaCore.obj
+.\abclib\DebugLib\seqFpgaIter.obj
+.\abclib\DebugLib\seqLatch.obj
+.\abclib\DebugLib\seqMan.obj
+.\abclib\DebugLib\seqMapCore.obj
+.\abclib\DebugLib\seqMapIter.obj
+.\abclib\DebugLib\seqRetCore.obj
+.\abclib\DebugLib\seqRetIter.obj
+.\abclib\DebugLib\seqShare.obj
+.\abclib\DebugLib\seqUtil.obj
+.\abclib\DebugLib\cmd.obj
+.\abclib\DebugLib\cmdAlias.obj
+.\abclib\DebugLib\cmdApi.obj
+.\abclib\DebugLib\cmdFlag.obj
+.\abclib\DebugLib\cmdHist.obj
+.\abclib\DebugLib\cmdUtils.obj
+.\abclib\DebugLib\io.obj
+.\abclib\DebugLib\ioRead.obj
+.\abclib\DebugLib\ioReadBaf.obj
+.\abclib\DebugLib\ioReadBench.obj
+.\abclib\DebugLib\ioReadBlif.obj
+.\abclib\DebugLib\ioReadEdif.obj
+.\abclib\DebugLib\ioReadEqn.obj
+.\abclib\DebugLib\ioReadPla.obj
+.\abclib\DebugLib\ioReadVerilog.obj
+.\abclib\DebugLib\ioUtil.obj
+.\abclib\DebugLib\ioWriteBaf.obj
+.\abclib\DebugLib\ioWriteBench.obj
+.\abclib\DebugLib\ioWriteBlif.obj
+.\abclib\DebugLib\ioWriteCnf.obj
+.\abclib\DebugLib\ioWriteDot.obj
+.\abclib\DebugLib\ioWriteEqn.obj
+.\abclib\DebugLib\ioWriteGml.obj
+.\abclib\DebugLib\ioWriteList.obj
+.\abclib\DebugLib\ioWritePla.obj
+.\abclib\DebugLib\libSupport.obj
+.\abclib\DebugLib\main.obj
+.\abclib\DebugLib\mainFrame.obj
+.\abclib\DebugLib\mainInit.obj
+.\abclib\DebugLib\mainUtils.obj
+.\abclib\DebugLib\cuddAddAbs.obj
+.\abclib\DebugLib\cuddAddApply.obj
+.\abclib\DebugLib\cuddAddFind.obj
+.\abclib\DebugLib\cuddAddInv.obj
+.\abclib\DebugLib\cuddAddIte.obj
+.\abclib\DebugLib\cuddAddNeg.obj
+.\abclib\DebugLib\cuddAddWalsh.obj
+.\abclib\DebugLib\cuddAndAbs.obj
+.\abclib\DebugLib\cuddAnneal.obj
+.\abclib\DebugLib\cuddApa.obj
+.\abclib\DebugLib\cuddAPI.obj
+.\abclib\DebugLib\cuddApprox.obj
+.\abclib\DebugLib\cuddBddAbs.obj
+.\abclib\DebugLib\cuddBddCorr.obj
+.\abclib\DebugLib\cuddBddIte.obj
+.\abclib\DebugLib\cuddBridge.obj
+.\abclib\DebugLib\cuddCache.obj
+.\abclib\DebugLib\cuddCheck.obj
+.\abclib\DebugLib\cuddClip.obj
+.\abclib\DebugLib\cuddCof.obj
+.\abclib\DebugLib\cuddCompose.obj
+.\abclib\DebugLib\cuddDecomp.obj
+.\abclib\DebugLib\cuddEssent.obj
+.\abclib\DebugLib\cuddExact.obj
+.\abclib\DebugLib\cuddExport.obj
+.\abclib\DebugLib\cuddGenCof.obj
+.\abclib\DebugLib\cuddGenetic.obj
+.\abclib\DebugLib\cuddGroup.obj
+.\abclib\DebugLib\cuddHarwell.obj
+.\abclib\DebugLib\cuddInit.obj
+.\abclib\DebugLib\cuddInteract.obj
+.\abclib\DebugLib\cuddLCache.obj
+.\abclib\DebugLib\cuddLevelQ.obj
+.\abclib\DebugLib\cuddLinear.obj
+.\abclib\DebugLib\cuddLiteral.obj
+.\abclib\DebugLib\cuddMatMult.obj
+.\abclib\DebugLib\cuddPriority.obj
+.\abclib\DebugLib\cuddRead.obj
+.\abclib\DebugLib\cuddRef.obj
+.\abclib\DebugLib\cuddReorder.obj
+.\abclib\DebugLib\cuddSat.obj
+.\abclib\DebugLib\cuddSign.obj
+.\abclib\DebugLib\cuddSolve.obj
+.\abclib\DebugLib\cuddSplit.obj
+.\abclib\DebugLib\cuddSubsetHB.obj
+.\abclib\DebugLib\cuddSubsetSP.obj
+.\abclib\DebugLib\cuddSymmetry.obj
+.\abclib\DebugLib\cuddTable.obj
+.\abclib\DebugLib\cuddUtil.obj
+.\abclib\DebugLib\cuddWindow.obj
+.\abclib\DebugLib\cuddZddCount.obj
+.\abclib\DebugLib\cuddZddFuncs.obj
+.\abclib\DebugLib\cuddZddGroup.obj
+.\abclib\DebugLib\cuddZddIsop.obj
+.\abclib\DebugLib\cuddZddLin.obj
+.\abclib\DebugLib\cuddZddMisc.obj
+.\abclib\DebugLib\cuddZddPort.obj
+.\abclib\DebugLib\cuddZddReord.obj
+.\abclib\DebugLib\cuddZddSetop.obj
+.\abclib\DebugLib\cuddZddSymm.obj
+.\abclib\DebugLib\cuddZddUtil.obj
+.\abclib\DebugLib\epd.obj
+.\abclib\DebugLib\mtrBasic.obj
+.\abclib\DebugLib\mtrGroup.obj
+.\abclib\DebugLib\parseCore.obj
+.\abclib\DebugLib\parseStack.obj
+.\abclib\DebugLib\dsdApi.obj
+.\abclib\DebugLib\dsdCheck.obj
+.\abclib\DebugLib\dsdLocal.obj
+.\abclib\DebugLib\dsdMan.obj
+.\abclib\DebugLib\dsdProc.obj
+.\abclib\DebugLib\dsdTree.obj
+.\abclib\DebugLib\reoApi.obj
+.\abclib\DebugLib\reoCore.obj
+.\abclib\DebugLib\reoProfile.obj
+.\abclib\DebugLib\reoSift.obj
+.\abclib\DebugLib\reoSwap.obj
+.\abclib\DebugLib\reoTest.obj
+.\abclib\DebugLib\reoTransfer.obj
+.\abclib\DebugLib\reoUnits.obj
+.\abclib\DebugLib\added.obj
+.\abclib\DebugLib\solver.obj
+.\abclib\DebugLib\msatActivity.obj
+.\abclib\DebugLib\msatClause.obj
+.\abclib\DebugLib\msatClauseVec.obj
+.\abclib\DebugLib\msatMem.obj
+.\abclib\DebugLib\msatOrderJ.obj
+.\abclib\DebugLib\msatQueue.obj
+.\abclib\DebugLib\msatRead.obj
+.\abclib\DebugLib\msatSolverApi.obj
+.\abclib\DebugLib\msatSolverCore.obj
+.\abclib\DebugLib\msatSolverIo.obj
+.\abclib\DebugLib\msatSolverSearch.obj
+.\abclib\DebugLib\msatSort.obj
+.\abclib\DebugLib\msatVec.obj
+.\abclib\DebugLib\fraigApi.obj
+.\abclib\DebugLib\fraigCanon.obj
+.\abclib\DebugLib\fraigFanout.obj
+.\abclib\DebugLib\fraigFeed.obj
+.\abclib\DebugLib\fraigMan.obj
+.\abclib\DebugLib\fraigMem.obj
+.\abclib\DebugLib\fraigNode.obj
+.\abclib\DebugLib\fraigPrime.obj
+.\abclib\DebugLib\fraigSat.obj
+.\abclib\DebugLib\fraigTable.obj
+.\abclib\DebugLib\fraigUtil.obj
+.\abclib\DebugLib\fraigVec.obj
+.\abclib\DebugLib\csat_apis.obj
+.\abclib\DebugLib\fxu.obj
+.\abclib\DebugLib\fxuCreate.obj
+.\abclib\DebugLib\fxuHeapD.obj
+.\abclib\DebugLib\fxuHeapS.obj
+.\abclib\DebugLib\fxuList.obj
+.\abclib\DebugLib\fxuMatrix.obj
+.\abclib\DebugLib\fxuPair.obj
+.\abclib\DebugLib\fxuPrint.obj
+.\abclib\DebugLib\fxuReduce.obj
+.\abclib\DebugLib\fxuSelect.obj
+.\abclib\DebugLib\fxuSingle.obj
+.\abclib\DebugLib\fxuUpdate.obj
+.\abclib\DebugLib\rwrDec.obj
+.\abclib\DebugLib\rwrEva.obj
+.\abclib\DebugLib\rwrExp.obj
+.\abclib\DebugLib\rwrLib.obj
+.\abclib\DebugLib\rwrMan.obj
+.\abclib\DebugLib\rwrPrint.obj
+.\abclib\DebugLib\rwrUtil.obj
+.\abclib\DebugLib\cutApi.obj
+.\abclib\DebugLib\cutCut.obj
+.\abclib\DebugLib\cutMan.obj
+.\abclib\DebugLib\cutMerge.obj
+.\abclib\DebugLib\cutNode.obj
+.\abclib\DebugLib\cutOracle.obj
+.\abclib\DebugLib\cutSeq.obj
+.\abclib\DebugLib\cutTruth.obj
+.\abclib\DebugLib\decAbc.obj
+.\abclib\DebugLib\decFactor.obj
+.\abclib\DebugLib\decMan.obj
+.\abclib\DebugLib\decPrint.obj
+.\abclib\DebugLib\decUtil.obj
+.\abclib\DebugLib\simMan.obj
+.\abclib\DebugLib\simSat.obj
+.\abclib\DebugLib\simSeq.obj
+.\abclib\DebugLib\simSupp.obj
+.\abclib\DebugLib\simSwitch.obj
+.\abclib\DebugLib\simSym.obj
+.\abclib\DebugLib\simSymSat.obj
+.\abclib\DebugLib\simSymSim.obj
+.\abclib\DebugLib\simSymStr.obj
+.\abclib\DebugLib\simUtils.obj
+.\abclib\DebugLib\fpga.obj
+.\abclib\DebugLib\fpgaCore.obj
+.\abclib\DebugLib\fpgaCreate.obj
+.\abclib\DebugLib\fpgaCut.obj
+.\abclib\DebugLib\fpgaCutUtils.obj
+.\abclib\DebugLib\fpgaFanout.obj
+.\abclib\DebugLib\fpgaLib.obj
+.\abclib\DebugLib\fpgaMatch.obj
+.\abclib\DebugLib\fpgaSwitch.obj
+.\abclib\DebugLib\fpgaTime.obj
+.\abclib\DebugLib\fpgaTruth.obj
+.\abclib\DebugLib\fpgaUtils.obj
+.\abclib\DebugLib\fpgaVec.obj
+.\abclib\DebugLib\mapper.obj
+.\abclib\DebugLib\mapperCanon.obj
+.\abclib\DebugLib\mapperCore.obj
+.\abclib\DebugLib\mapperCreate.obj
+.\abclib\DebugLib\mapperCut.obj
+.\abclib\DebugLib\mapperCutUtils.obj
+.\abclib\DebugLib\mapperFanout.obj
+.\abclib\DebugLib\mapperLib.obj
+.\abclib\DebugLib\mapperMatch.obj
+.\abclib\DebugLib\mapperRefs.obj
+.\abclib\DebugLib\mapperSuper.obj
+.\abclib\DebugLib\mapperSwitch.obj
+.\abclib\DebugLib\mapperTable.obj
+.\abclib\DebugLib\mapperTime.obj
+.\abclib\DebugLib\mapperTree.obj
+.\abclib\DebugLib\mapperTruth.obj
+.\abclib\DebugLib\mapperUtils.obj
+.\abclib\DebugLib\mapperVec.obj
+.\abclib\DebugLib\mio.obj
+.\abclib\DebugLib\mioApi.obj
+.\abclib\DebugLib\mioFunc.obj
+.\abclib\DebugLib\mioRead.obj
+.\abclib\DebugLib\mioUtils.obj
+.\abclib\DebugLib\super.obj
+.\abclib\DebugLib\superAnd.obj
+.\abclib\DebugLib\superGate.obj
+.\abclib\DebugLib\superWrite.obj
+.\abclib\DebugLib\pgaCore.obj
+.\abclib\DebugLib\pgaMan.obj
+.\abclib\DebugLib\pgaMatch.obj
+.\abclib\DebugLib\pgaUtil.obj
+.\abclib\DebugLib\extraBddKmap.obj
+.\abclib\DebugLib\extraBddMisc.obj
+.\abclib\DebugLib\extraBddSymm.obj
+.\abclib\DebugLib\extraUtilBitMatrix.obj
+.\abclib\DebugLib\extraUtilCanon.obj
+.\abclib\DebugLib\extraUtilFile.obj
+.\abclib\DebugLib\extraUtilMemory.obj
+.\abclib\DebugLib\extraUtilMisc.obj
+.\abclib\DebugLib\extraUtilProgress.obj
+.\abclib\DebugLib\extraUtilReader.obj
+.\abclib\DebugLib\st.obj
+.\abclib\DebugLib\stmm.obj
+.\abclib\DebugLib\cpu_stats.obj
+.\abclib\DebugLib\cpu_time.obj
+.\abclib\DebugLib\datalimit.obj
+.\abclib\DebugLib\getopt.obj
+.\abclib\DebugLib\pathsearch.obj
+.\abclib\DebugLib\safe_mem.obj
+.\abclib\DebugLib\strsav.obj
+.\abclib\DebugLib\texpand.obj
+.\abclib\DebugLib\mvc.obj
+.\abclib\DebugLib\mvcApi.obj
+.\abclib\DebugLib\mvcCompare.obj
+.\abclib\DebugLib\mvcContain.obj
+.\abclib\DebugLib\mvcCover.obj
+.\abclib\DebugLib\mvcCube.obj
+.\abclib\DebugLib\mvcDivide.obj
+.\abclib\DebugLib\mvcDivisor.obj
+.\abclib\DebugLib\mvcList.obj
+.\abclib\DebugLib\mvcLits.obj
+.\abclib\DebugLib\mvcMan.obj
+.\abclib\DebugLib\mvcOpAlg.obj
+.\abclib\DebugLib\mvcOpBool.obj
+.\abclib\DebugLib\mvcPrint.obj
+.\abclib\DebugLib\mvcSort.obj
+.\abclib\DebugLib\mvcUtils.obj
+.\abclib\DebugLib\ioWriteVerilog.obj
 ]
-Creating command line "link.exe -lib @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP83.tmp"
+Creating command line "link.exe -lib @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F1.tmp"
 <h3>Output Window</h3>
 Compiling...
-abcAig.c
-abcCheck.c
-abcDfs.c
-abcFanio.c
-abcFunc.c
-abcLatch.c
-abcMinBase.c
-abcNames.c
-abcNetlist.c
-abcNtk.c
-abcObj.c
-abcRefs.c
-abcShow.c
-abcSop.c
-abcUtil.c
 abc.c
-abcAttach.c
-abcBalance.c
-abcCollapse.c
-abcCut.c
-abcDsd.c
-abcFpga.c
-abcFraig.c
-abcFxu.c
-abcMap.c
-abcMiter.c
-abcNtbdd.c
-abcPga.c
-abcPrint.c
-abcReconv.c
-abcRefactor.c
-abcRenode.c
-abcRewrite.c
-abcSat.c
-abcStrash.c
-abcSweep.c
-abcSymm.c
-abcTiming.c
-abcUnreach.c
-abcVanEijk.c
-abcVanImp.c
-abcVerify.c
-seqAigCore.c
-seqAigIter.c
-seqCreate.c
-seqFpgaCore.c
-seqFpgaIter.c
-seqLatch.c
-seqMan.c
-seqMapCore.c
-seqMapIter.c
-seqRetCore.c
-seqRetIter.c
-seqShare.c
-seqUtil.c
-cmd.c
-cmdAlias.c
-cmdApi.c
-cmdFlag.c
-cmdHist.c
-cmdUtils.c
-io.c
-ioRead.c
-ioReadBaf.c
-ioReadBench.c
-ioReadBlif.c
-ioReadEdif.c
-ioReadEqn.c
-ioReadPla.c
-ioReadVerilog.c
-ioUtil.c
-ioWriteBaf.c
-ioWriteBench.c
-ioWriteBlif.c
-ioWriteCnf.c
-ioWriteDot.c
-ioWriteEqn.c
-ioWriteGml.c
-ioWriteList.c
-ioWritePla.c
-libSupport.c
-main.c
-mainFrame.c
-mainInit.c
-mainUtils.c
-cuddAddAbs.c
-cuddAddApply.c
-cuddAddFind.c
-cuddAddInv.c
-cuddAddIte.c
-cuddAddNeg.c
-cuddAddWalsh.c
-cuddAndAbs.c
-cuddAnneal.c
-cuddApa.c
-C:\_projects\abc\src\bdd\cudd\cuddApa.c(181) : warning C4244: 'return' : conversion from 'unsigned long ' to 'unsigned short ', possible loss of data
-C:\_projects\abc\src\bdd\cudd\cuddApa.c(213) : warning C4244: 'return' : conversion from 'unsigned long ' to 'unsigned short ', possible loss of data
-C:\_projects\abc\src\bdd\cudd\cuddApa.c(530) : warning C4244: '=' : conversion from 'unsigned short ' to 'unsigned char ', possible loss of data
-C:\_projects\abc\src\bdd\cudd\cuddApa.c(588) : warning C4244: '=' : conversion from 'unsigned short ' to 'unsigned char ', possible loss of data
-cuddAPI.c
-cuddApprox.c
-cuddBddAbs.c
-cuddBddCorr.c
-cuddBddIte.c
-cuddBridge.c
-cuddCache.c
-C:\_projects\abc\src\bdd\cudd\cuddCache.c(902) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
-cuddCheck.c
-cuddClip.c
-cuddCof.c
-cuddCompose.c
-cuddDecomp.c
-cuddEssent.c
-cuddExact.c
-cuddExport.c
-cuddGenCof.c
-cuddGenetic.c
-cuddGroup.c
-C:\_projects\abc\src\bdd\cudd\cuddGroup.c(2062) : warning C4018: '<=' : signed/unsigned mismatch
-cuddHarwell.c
-cuddInit.c
-cuddInteract.c
-cuddLCache.c
-C:\_projects\abc\src\bdd\cudd\cuddLCache.c(1387) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
-cuddLevelQ.c
-cuddLinear.c
-cuddLiteral.c
-cuddMatMult.c
-cuddPriority.c
-cuddRead.c
-cuddRef.c
-cuddReorder.c
-C:\_projects\abc\src\bdd\cudd\cuddReorder.c(395) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
-cuddSat.c
-C:\_projects\abc\src\bdd\cudd\cuddReorder.c(2016) : warning C4700: local variable 'minLevel' used without having been initialized
-C:\_projects\abc\src\bdd\cudd\cuddReorder.c(2020) : warning C4700: local variable 'maxLevel' used without having been initialized
-cuddSign.c
-cuddSolve.c
-cuddSplit.c
-cuddSubsetHB.c
-cuddSubsetSP.c
-cuddSymmetry.c
-cuddTable.c
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(1822) : warning C4018: '<' : signed/unsigned mismatch
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(1927) : warning C4018: '<' : signed/unsigned mismatch
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(2235) : warning C4018: '<' : signed/unsigned mismatch
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(2303) : warning C4018: '<' : signed/unsigned mismatch
-C:\_projects\abc\src\bdd\cudd\cuddTable.c(2358) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
-cuddUtil.c
-cuddWindow.c
-cuddZddCount.c
-cuddZddFuncs.c
-cuddZddGroup.c
-cuddZddIsop.c
-cuddZddLin.c
-cuddZddMisc.c
-cuddZddPort.c
-cuddZddReord.c
-cuddZddSetop.c
-cuddZddSymm.c
-cuddZddUtil.c
-epd.c
-mtrBasic.c
-mtrGroup.c
-parseCore.c
-parseStack.c
-dsdApi.c
-dsdCheck.c
-dsdLocal.c
-dsdMan.c
-dsdProc.c
-dsdTree.c
-reoApi.c
-reoCore.c
-reoProfile.c
-reoSift.c
-reoSwap.c
-reoTest.c
-reoTransfer.c
-reoUnits.c
-added.c
-solver.c
-msatActivity.c
-msatClause.c
-msatClauseVec.c
-msatMem.c
-msatOrderJ.c
-msatQueue.c
-msatRead.c
-msatSolverApi.c
-msatSolverCore.c
-msatSolverIo.c
-msatSolverSearch.c
-msatSort.c
-msatVec.c
-fraigApi.c
-fraigCanon.c
-fraigFanout.c
-fraigFeed.c
-fraigMan.c
-fraigMem.c
-fraigNode.c
-fraigPrime.c
-fraigSat.c
-fraigTable.c
-fraigUtil.c
-fraigVec.c
-csat_apis.c
-fxu.c
-fxuCreate.c
-fxuHeapD.c
-fxuHeapS.c
-fxuList.c
-fxuMatrix.c
-fxuPair.c
-fxuPrint.c
-fxuReduce.c
-fxuSelect.c
-fxuSingle.c
-fxuUpdate.c
-rwrDec.c
-rwrEva.c
-rwrExp.c
-rwrLib.c
-rwrMan.c
-rwrPrint.c
-rwrUtil.c
-cutApi.c
-cutCut.c
-cutMan.c
-cutMerge.c
-cutNode.c
-cutOracle.c
-cutSeq.c
-cutTruth.c
-decAbc.c
-decFactor.c
-decMan.c
-decPrint.c
-decUtil.c
-simMan.c
-simSat.c
-simSeq.c
-simSupp.c
-simSwitch.c
-simSym.c
-simSymSat.c
-simSymSim.c
-simSymStr.c
-simUtils.c
-fpga.c
-fpgaCore.c
-fpgaCreate.c
-fpgaCut.c
-fpgaCutUtils.c
-fpgaFanout.c
-fpgaLib.c
-fpgaMatch.c
-fpgaSwitch.c
-fpgaTime.c
-fpgaTruth.c
-fpgaUtils.c
-fpgaVec.c
-mapper.c
-mapperCanon.c
-mapperCore.c
-mapperCreate.c
-mapperCut.c
-mapperCutUtils.c
-mapperFanout.c
-mapperLib.c
-mapperMatch.c
-mapperRefs.c
-mapperSuper.c
-mapperSwitch.c
-mapperTable.c
-mapperTime.c
-mapperTree.c
-mapperTruth.c
-mapperUtils.c
-mapperVec.c
-mio.c
-mioApi.c
-mioFunc.c
-mioRead.c
-mioUtils.c
-super.c
-superAnd.c
-superGate.c
-superWrite.c
-pgaCore.c
-pgaMan.c
-pgaMatch.c
-pgaUtil.c
-extraBddKmap.c
-extraBddMisc.c
-extraBddSymm.c
-extraUtilBitMatrix.c
-extraUtilCanon.c
-extraUtilFile.c
-extraUtilMemory.c
-extraUtilMisc.c
-extraUtilProgress.c
-extraUtilReader.c
-st.c
-stmm.c
-cpu_stats.c
-cpu_time.c
-datalimit.c
-getopt.c
-pathsearch.c
-safe_mem.c
-strsav.c
-texpand.c
-mvc.c
-mvcApi.c
-mvcCompare.c
-mvcContain.c
-mvcCover.c
-mvcCube.c
-mvcDivide.c
-mvcDivisor.c
-mvcList.c
-mvcLits.c
-mvcMan.c
-mvcOpAlg.c
-mvcOpBool.c
-mvcPrint.c
-mvcSort.c
-mvcUtils.c
+c:\_projects\abc\src\base\abci\abc.c(2890) : warning C4013: 'Abc_NtkMiterSat2' undefined; assuming extern returning int
+ioWriteVerilog.c
 Creating library...
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F2.tmp" with contents
 [
-/nologo /o"abclib\ReleaseLib/abclib.bsc" 
-.\abclib\ReleaseLib\abcAig.sbr
-.\abclib\ReleaseLib\abcCheck.sbr
-.\abclib\ReleaseLib\abcDfs.sbr
-.\abclib\ReleaseLib\abcFanio.sbr
-.\abclib\ReleaseLib\abcFunc.sbr
-.\abclib\ReleaseLib\abcLatch.sbr
-.\abclib\ReleaseLib\abcMinBase.sbr
-.\abclib\ReleaseLib\abcNames.sbr
-.\abclib\ReleaseLib\abcNetlist.sbr
-.\abclib\ReleaseLib\abcNtk.sbr
-.\abclib\ReleaseLib\abcObj.sbr
-.\abclib\ReleaseLib\abcRefs.sbr
-.\abclib\ReleaseLib\abcShow.sbr
-.\abclib\ReleaseLib\abcSop.sbr
-.\abclib\ReleaseLib\abcUtil.sbr
-.\abclib\ReleaseLib\abc.sbr
-.\abclib\ReleaseLib\abcAttach.sbr
-.\abclib\ReleaseLib\abcBalance.sbr
-.\abclib\ReleaseLib\abcCollapse.sbr
-.\abclib\ReleaseLib\abcCut.sbr
-.\abclib\ReleaseLib\abcDsd.sbr
-.\abclib\ReleaseLib\abcFpga.sbr
-.\abclib\ReleaseLib\abcFraig.sbr
-.\abclib\ReleaseLib\abcFxu.sbr
-.\abclib\ReleaseLib\abcMap.sbr
-.\abclib\ReleaseLib\abcMiter.sbr
-.\abclib\ReleaseLib\abcNtbdd.sbr
-.\abclib\ReleaseLib\abcPga.sbr
-.\abclib\ReleaseLib\abcPrint.sbr
-.\abclib\ReleaseLib\abcReconv.sbr
-.\abclib\ReleaseLib\abcRefactor.sbr
-.\abclib\ReleaseLib\abcRenode.sbr
-.\abclib\ReleaseLib\abcRewrite.sbr
-.\abclib\ReleaseLib\abcSat.sbr
-.\abclib\ReleaseLib\abcStrash.sbr
-.\abclib\ReleaseLib\abcSweep.sbr
-.\abclib\ReleaseLib\abcSymm.sbr
-.\abclib\ReleaseLib\abcTiming.sbr
-.\abclib\ReleaseLib\abcUnreach.sbr
-.\abclib\ReleaseLib\abcVanEijk.sbr
-.\abclib\ReleaseLib\abcVanImp.sbr
-.\abclib\ReleaseLib\abcVerify.sbr
-.\abclib\ReleaseLib\seqAigCore.sbr
-.\abclib\ReleaseLib\seqAigIter.sbr
-.\abclib\ReleaseLib\seqCreate.sbr
-.\abclib\ReleaseLib\seqFpgaCore.sbr
-.\abclib\ReleaseLib\seqFpgaIter.sbr
-.\abclib\ReleaseLib\seqLatch.sbr
-.\abclib\ReleaseLib\seqMan.sbr
-.\abclib\ReleaseLib\seqMapCore.sbr
-.\abclib\ReleaseLib\seqMapIter.sbr
-.\abclib\ReleaseLib\seqRetCore.sbr
-.\abclib\ReleaseLib\seqRetIter.sbr
-.\abclib\ReleaseLib\seqShare.sbr
-.\abclib\ReleaseLib\seqUtil.sbr
-.\abclib\ReleaseLib\cmd.sbr
-.\abclib\ReleaseLib\cmdAlias.sbr
-.\abclib\ReleaseLib\cmdApi.sbr
-.\abclib\ReleaseLib\cmdFlag.sbr
-.\abclib\ReleaseLib\cmdHist.sbr
-.\abclib\ReleaseLib\cmdUtils.sbr
-.\abclib\ReleaseLib\io.sbr
-.\abclib\ReleaseLib\ioRead.sbr
-.\abclib\ReleaseLib\ioReadBaf.sbr
-.\abclib\ReleaseLib\ioReadBench.sbr
-.\abclib\ReleaseLib\ioReadBlif.sbr
-.\abclib\ReleaseLib\ioReadEdif.sbr
-.\abclib\ReleaseLib\ioReadEqn.sbr
-.\abclib\ReleaseLib\ioReadPla.sbr
-.\abclib\ReleaseLib\ioReadVerilog.sbr
-.\abclib\ReleaseLib\ioUtil.sbr
-.\abclib\ReleaseLib\ioWriteBaf.sbr
-.\abclib\ReleaseLib\ioWriteBench.sbr
-.\abclib\ReleaseLib\ioWriteBlif.sbr
-.\abclib\ReleaseLib\ioWriteCnf.sbr
-.\abclib\ReleaseLib\ioWriteDot.sbr
-.\abclib\ReleaseLib\ioWriteEqn.sbr
-.\abclib\ReleaseLib\ioWriteGml.sbr
-.\abclib\ReleaseLib\ioWriteList.sbr
-.\abclib\ReleaseLib\ioWritePla.sbr
-.\abclib\ReleaseLib\libSupport.sbr
-.\abclib\ReleaseLib\main.sbr
-.\abclib\ReleaseLib\mainFrame.sbr
-.\abclib\ReleaseLib\mainInit.sbr
-.\abclib\ReleaseLib\mainUtils.sbr
-.\abclib\ReleaseLib\cuddAddAbs.sbr
-.\abclib\ReleaseLib\cuddAddApply.sbr
-.\abclib\ReleaseLib\cuddAddFind.sbr
-.\abclib\ReleaseLib\cuddAddInv.sbr
-.\abclib\ReleaseLib\cuddAddIte.sbr
-.\abclib\ReleaseLib\cuddAddNeg.sbr
-.\abclib\ReleaseLib\cuddAddWalsh.sbr
-.\abclib\ReleaseLib\cuddAndAbs.sbr
-.\abclib\ReleaseLib\cuddAnneal.sbr
-.\abclib\ReleaseLib\cuddApa.sbr
-.\abclib\ReleaseLib\cuddAPI.sbr
-.\abclib\ReleaseLib\cuddApprox.sbr
-.\abclib\ReleaseLib\cuddBddAbs.sbr
-.\abclib\ReleaseLib\cuddBddCorr.sbr
-.\abclib\ReleaseLib\cuddBddIte.sbr
-.\abclib\ReleaseLib\cuddBridge.sbr
-.\abclib\ReleaseLib\cuddCache.sbr
-.\abclib\ReleaseLib\cuddCheck.sbr
-.\abclib\ReleaseLib\cuddClip.sbr
-.\abclib\ReleaseLib\cuddCof.sbr
-.\abclib\ReleaseLib\cuddCompose.sbr
-.\abclib\ReleaseLib\cuddDecomp.sbr
-.\abclib\ReleaseLib\cuddEssent.sbr
-.\abclib\ReleaseLib\cuddExact.sbr
-.\abclib\ReleaseLib\cuddExport.sbr
-.\abclib\ReleaseLib\cuddGenCof.sbr
-.\abclib\ReleaseLib\cuddGenetic.sbr
-.\abclib\ReleaseLib\cuddGroup.sbr
-.\abclib\ReleaseLib\cuddHarwell.sbr
-.\abclib\ReleaseLib\cuddInit.sbr
-.\abclib\ReleaseLib\cuddInteract.sbr
-.\abclib\ReleaseLib\cuddLCache.sbr
-.\abclib\ReleaseLib\cuddLevelQ.sbr
-.\abclib\ReleaseLib\cuddLinear.sbr
-.\abclib\ReleaseLib\cuddLiteral.sbr
-.\abclib\ReleaseLib\cuddMatMult.sbr
-.\abclib\ReleaseLib\cuddPriority.sbr
-.\abclib\ReleaseLib\cuddRead.sbr
-.\abclib\ReleaseLib\cuddRef.sbr
-.\abclib\ReleaseLib\cuddReorder.sbr
-.\abclib\ReleaseLib\cuddSat.sbr
-.\abclib\ReleaseLib\cuddSign.sbr
-.\abclib\ReleaseLib\cuddSolve.sbr
-.\abclib\ReleaseLib\cuddSplit.sbr
-.\abclib\ReleaseLib\cuddSubsetHB.sbr
-.\abclib\ReleaseLib\cuddSubsetSP.sbr
-.\abclib\ReleaseLib\cuddSymmetry.sbr
-.\abclib\ReleaseLib\cuddTable.sbr
-.\abclib\ReleaseLib\cuddUtil.sbr
-.\abclib\ReleaseLib\cuddWindow.sbr
-.\abclib\ReleaseLib\cuddZddCount.sbr
-.\abclib\ReleaseLib\cuddZddFuncs.sbr
-.\abclib\ReleaseLib\cuddZddGroup.sbr
-.\abclib\ReleaseLib\cuddZddIsop.sbr
-.\abclib\ReleaseLib\cuddZddLin.sbr
-.\abclib\ReleaseLib\cuddZddMisc.sbr
-.\abclib\ReleaseLib\cuddZddPort.sbr
-.\abclib\ReleaseLib\cuddZddReord.sbr
-.\abclib\ReleaseLib\cuddZddSetop.sbr
-.\abclib\ReleaseLib\cuddZddSymm.sbr
-.\abclib\ReleaseLib\cuddZddUtil.sbr
-.\abclib\ReleaseLib\epd.sbr
-.\abclib\ReleaseLib\mtrBasic.sbr
-.\abclib\ReleaseLib\mtrGroup.sbr
-.\abclib\ReleaseLib\parseCore.sbr
-.\abclib\ReleaseLib\parseStack.sbr
-.\abclib\ReleaseLib\dsdApi.sbr
-.\abclib\ReleaseLib\dsdCheck.sbr
-.\abclib\ReleaseLib\dsdLocal.sbr
-.\abclib\ReleaseLib\dsdMan.sbr
-.\abclib\ReleaseLib\dsdProc.sbr
-.\abclib\ReleaseLib\dsdTree.sbr
-.\abclib\ReleaseLib\reoApi.sbr
-.\abclib\ReleaseLib\reoCore.sbr
-.\abclib\ReleaseLib\reoProfile.sbr
-.\abclib\ReleaseLib\reoSift.sbr
-.\abclib\ReleaseLib\reoSwap.sbr
-.\abclib\ReleaseLib\reoTest.sbr
-.\abclib\ReleaseLib\reoTransfer.sbr
-.\abclib\ReleaseLib\reoUnits.sbr
-.\abclib\ReleaseLib\added.sbr
-.\abclib\ReleaseLib\solver.sbr
-.\abclib\ReleaseLib\msatActivity.sbr
-.\abclib\ReleaseLib\msatClause.sbr
-.\abclib\ReleaseLib\msatClauseVec.sbr
-.\abclib\ReleaseLib\msatMem.sbr
-.\abclib\ReleaseLib\msatOrderJ.sbr
-.\abclib\ReleaseLib\msatQueue.sbr
-.\abclib\ReleaseLib\msatRead.sbr
-.\abclib\ReleaseLib\msatSolverApi.sbr
-.\abclib\ReleaseLib\msatSolverCore.sbr
-.\abclib\ReleaseLib\msatSolverIo.sbr
-.\abclib\ReleaseLib\msatSolverSearch.sbr
-.\abclib\ReleaseLib\msatSort.sbr
-.\abclib\ReleaseLib\msatVec.sbr
-.\abclib\ReleaseLib\fraigApi.sbr
-.\abclib\ReleaseLib\fraigCanon.sbr
-.\abclib\ReleaseLib\fraigFanout.sbr
-.\abclib\ReleaseLib\fraigFeed.sbr
-.\abclib\ReleaseLib\fraigMan.sbr
-.\abclib\ReleaseLib\fraigMem.sbr
-.\abclib\ReleaseLib\fraigNode.sbr
-.\abclib\ReleaseLib\fraigPrime.sbr
-.\abclib\ReleaseLib\fraigSat.sbr
-.\abclib\ReleaseLib\fraigTable.sbr
-.\abclib\ReleaseLib\fraigUtil.sbr
-.\abclib\ReleaseLib\fraigVec.sbr
-.\abclib\ReleaseLib\csat_apis.sbr
-.\abclib\ReleaseLib\fxu.sbr
-.\abclib\ReleaseLib\fxuCreate.sbr
-.\abclib\ReleaseLib\fxuHeapD.sbr
-.\abclib\ReleaseLib\fxuHeapS.sbr
-.\abclib\ReleaseLib\fxuList.sbr
-.\abclib\ReleaseLib\fxuMatrix.sbr
-.\abclib\ReleaseLib\fxuPair.sbr
-.\abclib\ReleaseLib\fxuPrint.sbr
-.\abclib\ReleaseLib\fxuReduce.sbr
-.\abclib\ReleaseLib\fxuSelect.sbr
-.\abclib\ReleaseLib\fxuSingle.sbr
-.\abclib\ReleaseLib\fxuUpdate.sbr
-.\abclib\ReleaseLib\rwrDec.sbr
-.\abclib\ReleaseLib\rwrEva.sbr
-.\abclib\ReleaseLib\rwrExp.sbr
-.\abclib\ReleaseLib\rwrLib.sbr
-.\abclib\ReleaseLib\rwrMan.sbr
-.\abclib\ReleaseLib\rwrPrint.sbr
-.\abclib\ReleaseLib\rwrUtil.sbr
-.\abclib\ReleaseLib\cutApi.sbr
-.\abclib\ReleaseLib\cutCut.sbr
-.\abclib\ReleaseLib\cutMan.sbr
-.\abclib\ReleaseLib\cutMerge.sbr
-.\abclib\ReleaseLib\cutNode.sbr
-.\abclib\ReleaseLib\cutOracle.sbr
-.\abclib\ReleaseLib\cutSeq.sbr
-.\abclib\ReleaseLib\cutTruth.sbr
-.\abclib\ReleaseLib\decAbc.sbr
-.\abclib\ReleaseLib\decFactor.sbr
-.\abclib\ReleaseLib\decMan.sbr
-.\abclib\ReleaseLib\decPrint.sbr
-.\abclib\ReleaseLib\decUtil.sbr
-.\abclib\ReleaseLib\simMan.sbr
-.\abclib\ReleaseLib\simSat.sbr
-.\abclib\ReleaseLib\simSeq.sbr
-.\abclib\ReleaseLib\simSupp.sbr
-.\abclib\ReleaseLib\simSwitch.sbr
-.\abclib\ReleaseLib\simSym.sbr
-.\abclib\ReleaseLib\simSymSat.sbr
-.\abclib\ReleaseLib\simSymSim.sbr
-.\abclib\ReleaseLib\simSymStr.sbr
-.\abclib\ReleaseLib\simUtils.sbr
-.\abclib\ReleaseLib\fpga.sbr
-.\abclib\ReleaseLib\fpgaCore.sbr
-.\abclib\ReleaseLib\fpgaCreate.sbr
-.\abclib\ReleaseLib\fpgaCut.sbr
-.\abclib\ReleaseLib\fpgaCutUtils.sbr
-.\abclib\ReleaseLib\fpgaFanout.sbr
-.\abclib\ReleaseLib\fpgaLib.sbr
-.\abclib\ReleaseLib\fpgaMatch.sbr
-.\abclib\ReleaseLib\fpgaSwitch.sbr
-.\abclib\ReleaseLib\fpgaTime.sbr
-.\abclib\ReleaseLib\fpgaTruth.sbr
-.\abclib\ReleaseLib\fpgaUtils.sbr
-.\abclib\ReleaseLib\fpgaVec.sbr
-.\abclib\ReleaseLib\mapper.sbr
-.\abclib\ReleaseLib\mapperCanon.sbr
-.\abclib\ReleaseLib\mapperCore.sbr
-.\abclib\ReleaseLib\mapperCreate.sbr
-.\abclib\ReleaseLib\mapperCut.sbr
-.\abclib\ReleaseLib\mapperCutUtils.sbr
-.\abclib\ReleaseLib\mapperFanout.sbr
-.\abclib\ReleaseLib\mapperLib.sbr
-.\abclib\ReleaseLib\mapperMatch.sbr
-.\abclib\ReleaseLib\mapperRefs.sbr
-.\abclib\ReleaseLib\mapperSuper.sbr
-.\abclib\ReleaseLib\mapperSwitch.sbr
-.\abclib\ReleaseLib\mapperTable.sbr
-.\abclib\ReleaseLib\mapperTime.sbr
-.\abclib\ReleaseLib\mapperTree.sbr
-.\abclib\ReleaseLib\mapperTruth.sbr
-.\abclib\ReleaseLib\mapperUtils.sbr
-.\abclib\ReleaseLib\mapperVec.sbr
-.\abclib\ReleaseLib\mio.sbr
-.\abclib\ReleaseLib\mioApi.sbr
-.\abclib\ReleaseLib\mioFunc.sbr
-.\abclib\ReleaseLib\mioRead.sbr
-.\abclib\ReleaseLib\mioUtils.sbr
-.\abclib\ReleaseLib\super.sbr
-.\abclib\ReleaseLib\superAnd.sbr
-.\abclib\ReleaseLib\superGate.sbr
-.\abclib\ReleaseLib\superWrite.sbr
-.\abclib\ReleaseLib\pgaCore.sbr
-.\abclib\ReleaseLib\pgaMan.sbr
-.\abclib\ReleaseLib\pgaMatch.sbr
-.\abclib\ReleaseLib\pgaUtil.sbr
-.\abclib\ReleaseLib\extraBddKmap.sbr
-.\abclib\ReleaseLib\extraBddMisc.sbr
-.\abclib\ReleaseLib\extraBddSymm.sbr
-.\abclib\ReleaseLib\extraUtilBitMatrix.sbr
-.\abclib\ReleaseLib\extraUtilCanon.sbr
-.\abclib\ReleaseLib\extraUtilFile.sbr
-.\abclib\ReleaseLib\extraUtilMemory.sbr
-.\abclib\ReleaseLib\extraUtilMisc.sbr
-.\abclib\ReleaseLib\extraUtilProgress.sbr
-.\abclib\ReleaseLib\extraUtilReader.sbr
-.\abclib\ReleaseLib\st.sbr
-.\abclib\ReleaseLib\stmm.sbr
-.\abclib\ReleaseLib\cpu_stats.sbr
-.\abclib\ReleaseLib\cpu_time.sbr
-.\abclib\ReleaseLib\datalimit.sbr
-.\abclib\ReleaseLib\getopt.sbr
-.\abclib\ReleaseLib\pathsearch.sbr
-.\abclib\ReleaseLib\safe_mem.sbr
-.\abclib\ReleaseLib\strsav.sbr
-.\abclib\ReleaseLib\texpand.sbr
-.\abclib\ReleaseLib\mvc.sbr
-.\abclib\ReleaseLib\mvcApi.sbr
-.\abclib\ReleaseLib\mvcCompare.sbr
-.\abclib\ReleaseLib\mvcContain.sbr
-.\abclib\ReleaseLib\mvcCover.sbr
-.\abclib\ReleaseLib\mvcCube.sbr
-.\abclib\ReleaseLib\mvcDivide.sbr
-.\abclib\ReleaseLib\mvcDivisor.sbr
-.\abclib\ReleaseLib\mvcList.sbr
-.\abclib\ReleaseLib\mvcLits.sbr
-.\abclib\ReleaseLib\mvcMan.sbr
-.\abclib\ReleaseLib\mvcOpAlg.sbr
-.\abclib\ReleaseLib\mvcOpBool.sbr
-.\abclib\ReleaseLib\mvcPrint.sbr
-.\abclib\ReleaseLib\mvcSort.sbr
-.\abclib\ReleaseLib\mvcUtils.sbr]
-Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84.tmp"
+/nologo /o"abclib\DebugLib/abclib.bsc" 
+.\abclib\DebugLib\abcAig.sbr
+.\abclib\DebugLib\abcCheck.sbr
+.\abclib\DebugLib\abcDfs.sbr
+.\abclib\DebugLib\abcFanio.sbr
+.\abclib\DebugLib\abcFunc.sbr
+.\abclib\DebugLib\abcLatch.sbr
+.\abclib\DebugLib\abcMinBase.sbr
+.\abclib\DebugLib\abcNames.sbr
+.\abclib\DebugLib\abcNetlist.sbr
+.\abclib\DebugLib\abcNtk.sbr
+.\abclib\DebugLib\abcObj.sbr
+.\abclib\DebugLib\abcRefs.sbr
+.\abclib\DebugLib\abcShow.sbr
+.\abclib\DebugLib\abcSop.sbr
+.\abclib\DebugLib\abcUtil.sbr
+.\abclib\DebugLib\abc.sbr
+.\abclib\DebugLib\abcAttach.sbr
+.\abclib\DebugLib\abcBalance.sbr
+.\abclib\DebugLib\abcCollapse.sbr
+.\abclib\DebugLib\abcCut.sbr
+.\abclib\DebugLib\abcDsd.sbr
+.\abclib\DebugLib\abcFpga.sbr
+.\abclib\DebugLib\abcFraig.sbr
+.\abclib\DebugLib\abcFxu.sbr
+.\abclib\DebugLib\abcMap.sbr
+.\abclib\DebugLib\abcMiter.sbr
+.\abclib\DebugLib\abcNtbdd.sbr
+.\abclib\DebugLib\abcPga.sbr
+.\abclib\DebugLib\abcPrint.sbr
+.\abclib\DebugLib\abcReconv.sbr
+.\abclib\DebugLib\abcRefactor.sbr
+.\abclib\DebugLib\abcRenode.sbr
+.\abclib\DebugLib\abcRewrite.sbr
+.\abclib\DebugLib\abcSat.sbr
+.\abclib\DebugLib\abcStrash.sbr
+.\abclib\DebugLib\abcSweep.sbr
+.\abclib\DebugLib\abcSymm.sbr
+.\abclib\DebugLib\abcTiming.sbr
+.\abclib\DebugLib\abcUnreach.sbr
+.\abclib\DebugLib\abcVanEijk.sbr
+.\abclib\DebugLib\abcVanImp.sbr
+.\abclib\DebugLib\abcVerify.sbr
+.\abclib\DebugLib\seqAigCore.sbr
+.\abclib\DebugLib\seqAigIter.sbr
+.\abclib\DebugLib\seqCreate.sbr
+.\abclib\DebugLib\seqFpgaCore.sbr
+.\abclib\DebugLib\seqFpgaIter.sbr
+.\abclib\DebugLib\seqLatch.sbr
+.\abclib\DebugLib\seqMan.sbr
+.\abclib\DebugLib\seqMapCore.sbr
+.\abclib\DebugLib\seqMapIter.sbr
+.\abclib\DebugLib\seqRetCore.sbr
+.\abclib\DebugLib\seqRetIter.sbr
+.\abclib\DebugLib\seqShare.sbr
+.\abclib\DebugLib\seqUtil.sbr
+.\abclib\DebugLib\cmd.sbr
+.\abclib\DebugLib\cmdAlias.sbr
+.\abclib\DebugLib\cmdApi.sbr
+.\abclib\DebugLib\cmdFlag.sbr
+.\abclib\DebugLib\cmdHist.sbr
+.\abclib\DebugLib\cmdUtils.sbr
+.\abclib\DebugLib\io.sbr
+.\abclib\DebugLib\ioRead.sbr
+.\abclib\DebugLib\ioReadBaf.sbr
+.\abclib\DebugLib\ioReadBench.sbr
+.\abclib\DebugLib\ioReadBlif.sbr
+.\abclib\DebugLib\ioReadEdif.sbr
+.\abclib\DebugLib\ioReadEqn.sbr
+.\abclib\DebugLib\ioReadPla.sbr
+.\abclib\DebugLib\ioReadVerilog.sbr
+.\abclib\DebugLib\ioUtil.sbr
+.\abclib\DebugLib\ioWriteBaf.sbr
+.\abclib\DebugLib\ioWriteBench.sbr
+.\abclib\DebugLib\ioWriteBlif.sbr
+.\abclib\DebugLib\ioWriteCnf.sbr
+.\abclib\DebugLib\ioWriteDot.sbr
+.\abclib\DebugLib\ioWriteEqn.sbr
+.\abclib\DebugLib\ioWriteGml.sbr
+.\abclib\DebugLib\ioWriteList.sbr
+.\abclib\DebugLib\ioWritePla.sbr
+.\abclib\DebugLib\libSupport.sbr
+.\abclib\DebugLib\main.sbr
+.\abclib\DebugLib\mainFrame.sbr
+.\abclib\DebugLib\mainInit.sbr
+.\abclib\DebugLib\mainUtils.sbr
+.\abclib\DebugLib\cuddAddAbs.sbr
+.\abclib\DebugLib\cuddAddApply.sbr
+.\abclib\DebugLib\cuddAddFind.sbr
+.\abclib\DebugLib\cuddAddInv.sbr
+.\abclib\DebugLib\cuddAddIte.sbr
+.\abclib\DebugLib\cuddAddNeg.sbr
+.\abclib\DebugLib\cuddAddWalsh.sbr
+.\abclib\DebugLib\cuddAndAbs.sbr
+.\abclib\DebugLib\cuddAnneal.sbr
+.\abclib\DebugLib\cuddApa.sbr
+.\abclib\DebugLib\cuddAPI.sbr
+.\abclib\DebugLib\cuddApprox.sbr
+.\abclib\DebugLib\cuddBddAbs.sbr
+.\abclib\DebugLib\cuddBddCorr.sbr
+.\abclib\DebugLib\cuddBddIte.sbr
+.\abclib\DebugLib\cuddBridge.sbr
+.\abclib\DebugLib\cuddCache.sbr
+.\abclib\DebugLib\cuddCheck.sbr
+.\abclib\DebugLib\cuddClip.sbr
+.\abclib\DebugLib\cuddCof.sbr
+.\abclib\DebugLib\cuddCompose.sbr
+.\abclib\DebugLib\cuddDecomp.sbr
+.\abclib\DebugLib\cuddEssent.sbr
+.\abclib\DebugLib\cuddExact.sbr
+.\abclib\DebugLib\cuddExport.sbr
+.\abclib\DebugLib\cuddGenCof.sbr
+.\abclib\DebugLib\cuddGenetic.sbr
+.\abclib\DebugLib\cuddGroup.sbr
+.\abclib\DebugLib\cuddHarwell.sbr
+.\abclib\DebugLib\cuddInit.sbr
+.\abclib\DebugLib\cuddInteract.sbr
+.\abclib\DebugLib\cuddLCache.sbr
+.\abclib\DebugLib\cuddLevelQ.sbr
+.\abclib\DebugLib\cuddLinear.sbr
+.\abclib\DebugLib\cuddLiteral.sbr
+.\abclib\DebugLib\cuddMatMult.sbr
+.\abclib\DebugLib\cuddPriority.sbr
+.\abclib\DebugLib\cuddRead.sbr
+.\abclib\DebugLib\cuddRef.sbr
+.\abclib\DebugLib\cuddReorder.sbr
+.\abclib\DebugLib\cuddSat.sbr
+.\abclib\DebugLib\cuddSign.sbr
+.\abclib\DebugLib\cuddSolve.sbr
+.\abclib\DebugLib\cuddSplit.sbr
+.\abclib\DebugLib\cuddSubsetHB.sbr
+.\abclib\DebugLib\cuddSubsetSP.sbr
+.\abclib\DebugLib\cuddSymmetry.sbr
+.\abclib\DebugLib\cuddTable.sbr
+.\abclib\DebugLib\cuddUtil.sbr
+.\abclib\DebugLib\cuddWindow.sbr
+.\abclib\DebugLib\cuddZddCount.sbr
+.\abclib\DebugLib\cuddZddFuncs.sbr
+.\abclib\DebugLib\cuddZddGroup.sbr
+.\abclib\DebugLib\cuddZddIsop.sbr
+.\abclib\DebugLib\cuddZddLin.sbr
+.\abclib\DebugLib\cuddZddMisc.sbr
+.\abclib\DebugLib\cuddZddPort.sbr
+.\abclib\DebugLib\cuddZddReord.sbr
+.\abclib\DebugLib\cuddZddSetop.sbr
+.\abclib\DebugLib\cuddZddSymm.sbr
+.\abclib\DebugLib\cuddZddUtil.sbr
+.\abclib\DebugLib\epd.sbr
+.\abclib\DebugLib\mtrBasic.sbr
+.\abclib\DebugLib\mtrGroup.sbr
+.\abclib\DebugLib\parseCore.sbr
+.\abclib\DebugLib\parseStack.sbr
+.\abclib\DebugLib\dsdApi.sbr
+.\abclib\DebugLib\dsdCheck.sbr
+.\abclib\DebugLib\dsdLocal.sbr
+.\abclib\DebugLib\dsdMan.sbr
+.\abclib\DebugLib\dsdProc.sbr
+.\abclib\DebugLib\dsdTree.sbr
+.\abclib\DebugLib\reoApi.sbr
+.\abclib\DebugLib\reoCore.sbr
+.\abclib\DebugLib\reoProfile.sbr
+.\abclib\DebugLib\reoSift.sbr
+.\abclib\DebugLib\reoSwap.sbr
+.\abclib\DebugLib\reoTest.sbr
+.\abclib\DebugLib\reoTransfer.sbr
+.\abclib\DebugLib\reoUnits.sbr
+.\abclib\DebugLib\added.sbr
+.\abclib\DebugLib\solver.sbr
+.\abclib\DebugLib\msatActivity.sbr
+.\abclib\DebugLib\msatClause.sbr
+.\abclib\DebugLib\msatClauseVec.sbr
+.\abclib\DebugLib\msatMem.sbr
+.\abclib\DebugLib\msatOrderJ.sbr
+.\abclib\DebugLib\msatQueue.sbr
+.\abclib\DebugLib\msatRead.sbr
+.\abclib\DebugLib\msatSolverApi.sbr
+.\abclib\DebugLib\msatSolverCore.sbr
+.\abclib\DebugLib\msatSolverIo.sbr
+.\abclib\DebugLib\msatSolverSearch.sbr
+.\abclib\DebugLib\msatSort.sbr
+.\abclib\DebugLib\msatVec.sbr
+.\abclib\DebugLib\fraigApi.sbr
+.\abclib\DebugLib\fraigCanon.sbr
+.\abclib\DebugLib\fraigFanout.sbr
+.\abclib\DebugLib\fraigFeed.sbr
+.\abclib\DebugLib\fraigMan.sbr
+.\abclib\DebugLib\fraigMem.sbr
+.\abclib\DebugLib\fraigNode.sbr
+.\abclib\DebugLib\fraigPrime.sbr
+.\abclib\DebugLib\fraigSat.sbr
+.\abclib\DebugLib\fraigTable.sbr
+.\abclib\DebugLib\fraigUtil.sbr
+.\abclib\DebugLib\fraigVec.sbr
+.\abclib\DebugLib\csat_apis.sbr
+.\abclib\DebugLib\fxu.sbr
+.\abclib\DebugLib\fxuCreate.sbr
+.\abclib\DebugLib\fxuHeapD.sbr
+.\abclib\DebugLib\fxuHeapS.sbr
+.\abclib\DebugLib\fxuList.sbr
+.\abclib\DebugLib\fxuMatrix.sbr
+.\abclib\DebugLib\fxuPair.sbr
+.\abclib\DebugLib\fxuPrint.sbr
+.\abclib\DebugLib\fxuReduce.sbr
+.\abclib\DebugLib\fxuSelect.sbr
+.\abclib\DebugLib\fxuSingle.sbr
+.\abclib\DebugLib\fxuUpdate.sbr
+.\abclib\DebugLib\rwrDec.sbr
+.\abclib\DebugLib\rwrEva.sbr
+.\abclib\DebugLib\rwrExp.sbr
+.\abclib\DebugLib\rwrLib.sbr
+.\abclib\DebugLib\rwrMan.sbr
+.\abclib\DebugLib\rwrPrint.sbr
+.\abclib\DebugLib\rwrUtil.sbr
+.\abclib\DebugLib\cutApi.sbr
+.\abclib\DebugLib\cutCut.sbr
+.\abclib\DebugLib\cutMan.sbr
+.\abclib\DebugLib\cutMerge.sbr
+.\abclib\DebugLib\cutNode.sbr
+.\abclib\DebugLib\cutOracle.sbr
+.\abclib\DebugLib\cutSeq.sbr
+.\abclib\DebugLib\cutTruth.sbr
+.\abclib\DebugLib\decAbc.sbr
+.\abclib\DebugLib\decFactor.sbr
+.\abclib\DebugLib\decMan.sbr
+.\abclib\DebugLib\decPrint.sbr
+.\abclib\DebugLib\decUtil.sbr
+.\abclib\DebugLib\simMan.sbr
+.\abclib\DebugLib\simSat.sbr
+.\abclib\DebugLib\simSeq.sbr
+.\abclib\DebugLib\simSupp.sbr
+.\abclib\DebugLib\simSwitch.sbr
+.\abclib\DebugLib\simSym.sbr
+.\abclib\DebugLib\simSymSat.sbr
+.\abclib\DebugLib\simSymSim.sbr
+.\abclib\DebugLib\simSymStr.sbr
+.\abclib\DebugLib\simUtils.sbr
+.\abclib\DebugLib\fpga.sbr
+.\abclib\DebugLib\fpgaCore.sbr
+.\abclib\DebugLib\fpgaCreate.sbr
+.\abclib\DebugLib\fpgaCut.sbr
+.\abclib\DebugLib\fpgaCutUtils.sbr
+.\abclib\DebugLib\fpgaFanout.sbr
+.\abclib\DebugLib\fpgaLib.sbr
+.\abclib\DebugLib\fpgaMatch.sbr
+.\abclib\DebugLib\fpgaSwitch.sbr
+.\abclib\DebugLib\fpgaTime.sbr
+.\abclib\DebugLib\fpgaTruth.sbr
+.\abclib\DebugLib\fpgaUtils.sbr
+.\abclib\DebugLib\fpgaVec.sbr
+.\abclib\DebugLib\mapper.sbr
+.\abclib\DebugLib\mapperCanon.sbr
+.\abclib\DebugLib\mapperCore.sbr
+.\abclib\DebugLib\mapperCreate.sbr
+.\abclib\DebugLib\mapperCut.sbr
+.\abclib\DebugLib\mapperCutUtils.sbr
+.\abclib\DebugLib\mapperFanout.sbr
+.\abclib\DebugLib\mapperLib.sbr
+.\abclib\DebugLib\mapperMatch.sbr
+.\abclib\DebugLib\mapperRefs.sbr
+.\abclib\DebugLib\mapperSuper.sbr
+.\abclib\DebugLib\mapperSwitch.sbr
+.\abclib\DebugLib\mapperTable.sbr
+.\abclib\DebugLib\mapperTime.sbr
+.\abclib\DebugLib\mapperTree.sbr
+.\abclib\DebugLib\mapperTruth.sbr
+.\abclib\DebugLib\mapperUtils.sbr
+.\abclib\DebugLib\mapperVec.sbr
+.\abclib\DebugLib\mio.sbr
+.\abclib\DebugLib\mioApi.sbr
+.\abclib\DebugLib\mioFunc.sbr
+.\abclib\DebugLib\mioRead.sbr
+.\abclib\DebugLib\mioUtils.sbr
+.\abclib\DebugLib\super.sbr
+.\abclib\DebugLib\superAnd.sbr
+.\abclib\DebugLib\superGate.sbr
+.\abclib\DebugLib\superWrite.sbr
+.\abclib\DebugLib\pgaCore.sbr
+.\abclib\DebugLib\pgaMan.sbr
+.\abclib\DebugLib\pgaMatch.sbr
+.\abclib\DebugLib\pgaUtil.sbr
+.\abclib\DebugLib\extraBddKmap.sbr
+.\abclib\DebugLib\extraBddMisc.sbr
+.\abclib\DebugLib\extraBddSymm.sbr
+.\abclib\DebugLib\extraUtilBitMatrix.sbr
+.\abclib\DebugLib\extraUtilCanon.sbr
+.\abclib\DebugLib\extraUtilFile.sbr
+.\abclib\DebugLib\extraUtilMemory.sbr
+.\abclib\DebugLib\extraUtilMisc.sbr
+.\abclib\DebugLib\extraUtilProgress.sbr
+.\abclib\DebugLib\extraUtilReader.sbr
+.\abclib\DebugLib\st.sbr
+.\abclib\DebugLib\stmm.sbr
+.\abclib\DebugLib\cpu_stats.sbr
+.\abclib\DebugLib\cpu_time.sbr
+.\abclib\DebugLib\datalimit.sbr
+.\abclib\DebugLib\getopt.sbr
+.\abclib\DebugLib\pathsearch.sbr
+.\abclib\DebugLib\safe_mem.sbr
+.\abclib\DebugLib\strsav.sbr
+.\abclib\DebugLib\texpand.sbr
+.\abclib\DebugLib\mvc.sbr
+.\abclib\DebugLib\mvcApi.sbr
+.\abclib\DebugLib\mvcCompare.sbr
+.\abclib\DebugLib\mvcContain.sbr
+.\abclib\DebugLib\mvcCover.sbr
+.\abclib\DebugLib\mvcCube.sbr
+.\abclib\DebugLib\mvcDivide.sbr
+.\abclib\DebugLib\mvcDivisor.sbr
+.\abclib\DebugLib\mvcList.sbr
+.\abclib\DebugLib\mvcLits.sbr
+.\abclib\DebugLib\mvcMan.sbr
+.\abclib\DebugLib\mvcOpAlg.sbr
+.\abclib\DebugLib\mvcOpBool.sbr
+.\abclib\DebugLib\mvcPrint.sbr
+.\abclib\DebugLib\mvcSort.sbr
+.\abclib\DebugLib\mvcUtils.sbr
+.\abclib\DebugLib\ioWriteVerilog.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP15F2.tmp"
 Creating browse info file...
 <h3>Output Window</h3>
 
 
 
 <h3>Results</h3>
-abclib_release.lib - 0 error(s), 15 warning(s)
+abclib_debug.lib - 0 error(s), 1 warning(s)
 </pre>
 </body>
 </html>
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index e0a27f9a..cbdf87c7 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -211,7 +211,7 @@ struct Abc_Ntk_t_
 // transforming floats into ints and back
 static inline int         Abc_Float2Int( float Val )                 { return *((int *)&Val);               }
 static inline float       Abc_Int2Float( int Num )                   { return *((float *)&Num);             }
-static inline int         Abc_BitWordNum( int nBits )                { return nBits/32 + ((nBits%32) > 0);  }
+static inline int         Abc_BitWordNum( int nBits )                { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0);  }
 
 // checking the network type
 static inline bool        Abc_NtkIsNetlist( Abc_Ntk_t * pNtk )       { return pNtk->ntkType == ABC_NTK_NETLIST; }
@@ -487,6 +487,8 @@ extern int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
 /*=== abcMiter.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 extern Abc_Ntk_t *        Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
+extern Abc_Ntk_t *        Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist );
+extern Abc_Ntk_t *        Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter );
 extern void               Abc_NtkMiterReport( Abc_Ntk_t * pMiter );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 70cd2e6c..259187bf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3745,7 +3745,9 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // run the command
-    pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose );
+//    pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose );
+    pNtkRes = NULL;
+
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -3811,7 +3813,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    Abc_NtkTestEsop( pNtk );
+//    Abc_NtkTestEsop( pNtk );
 //    Abc_NtkTestSop( pNtk );
 //    printf( "This command is currently not used.\n" );
 
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index b5338127..44130a20 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -350,6 +350,94 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Derives the miter of two cofactors of one output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
+{
+    Abc_Ntk_t * pNtkMiter;
+    Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( 1 == Abc_NtkCoNum(pNtk) );
+    assert( In < Abc_NtkCiNum(pNtk) );
+
+    // start the new network
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkMiter->pName = util_strsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) );
+
+    // get the root output
+    pRoot = Abc_NtkCo( pNtk, 0 );
+
+    // perform strashing
+    Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 );
+    // set the first cofactor
+    Abc_NtkCi(pNtk, In)->pCopy = Abc_ObjNot( Abc_NtkConst1(pNtkMiter) );
+    // add the first cofactor
+    Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
+    // save the output
+    pOutput1 = Abc_ObjFanin0(pRoot)->pCopy;
+
+    // set the second cofactor
+    Abc_NtkCi(pNtk, In)->pCopy = Abc_NtkConst1( pNtkMiter );
+    // add the second cofactor
+    Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
+    // save the output
+    pOutput2 = Abc_ObjFanin0(pRoot)->pCopy;
+
+    // create the miter of the two outputs
+    if ( fExist ) 
+        pMiter = Abc_AigOr( pNtkMiter->pManFunc, pOutput1, pOutput2 );
+    else
+        pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 );
+    Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
+
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkMiter ) )
+    {
+        printf( "Abc_NtkMiter: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkMiter );
+        return NULL;
+    }
+    return pNtkMiter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the miter of two cofactors of one output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkTemp;
+    Abc_Obj_t * pObj;
+    int i;
+
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
+        pNtk = Abc_NtkMiterQuantify( pNtkTemp = pNtk, i, 1 );
+        Abc_NtkDelete( pNtkTemp );
+    }
+
+    return pNtk;
+}
+
 
 
 
diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
new file mode 100644
index 00000000..009a17bb
--- /dev/null
+++ b/src/sat/aig/aig.h
@@ -0,0 +1,308 @@
+/**CFile****************************************************************
+
+  FileName    [aig.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __AIG_H__
+#define __AIG_H__
+
+/*
+    AIG is an And-Inv Graph with structural hashing.
+    It is always structurally hashed. It means that at any time:
+    - for each AND gate, there are no other AND gates with the same children
+    - the constants are propagated
+    - there is no single-input nodes (inverters/buffers)
+    Additionally the following invariants are satisfied:
+    - there are no dangling nodes (the nodes without fanout)
+    - the level of each AND gate reflects the levels of this fanins
+    - the AND nodes are in the topological order
+    - the constant 1 node has always number 0 in the object list
+    The operations that are performed on AIGs:
+    - building new nodes (Aig_And)
+    - performing elementary Boolean operations (Aig_Or, Aig_Xor, etc)
+    - replacing one node by another (Abc_AigReplace)
+    - propagating constants (Abc_AigReplace)
+    - deleting dangling nodes (Abc_AigDelete)
+    When AIG is duplicated, the new graph is structurally hashed too.
+    If this repeated hashing leads to fewer nodes, it means the original
+    AIG was not strictly hashed (one of the conditions above is violated).
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+//typedef int                   bool;
+#ifndef bool
+#define bool int
+#endif
+
+typedef struct Aig_Param_t_     Aig_Param_t;
+typedef struct Aig_Man_t_       Aig_Man_t;
+typedef struct Aig_Node_t_      Aig_Node_t;
+typedef struct Aig_Edge_t_      Aig_Edge_t;
+typedef struct Aig_MemFixed_t_  Aig_MemFixed_t;
+typedef struct Aig_SimInfo_t_   Aig_SimInfo_t;
+typedef struct Aig_Table_t_     Aig_Table_t;
+
+// network types
+typedef enum { 
+    AIG_NONE = 0,  // 0: unknown
+    AIG_PI,        // 1: primary input
+    AIG_PO,        // 2: primary output
+    AIG_AND        // 3: internal node
+} Aig_NodeType_t;
+
+// the AIG parameters
+struct Aig_Param_t_
+{
+    int              nPatsRand;     // the number of random patterns
+    int              nBTLimit;      // backtrack limit at the intermediate nodes
+    int              nSeconds;      // the runtime limit at the final miter
+};
+
+// the AIG edge 
+struct Aig_Edge_t_ 
+{
+    unsigned         iNode   : 31;  // the node
+    unsigned         fComp   :  1;  // the complemented attribute
+};
+
+// the AIG node
+struct Aig_Node_t_  // 8 words
+{
+    // various numbers associated with the node
+    int              Id;            // the unique number (SAT var number) of this node 
+    int              nRefs;         // the reference counter
+    unsigned         Type    :  2;  // the node type
+    unsigned         fPhase  :  1;  // the phase of this node
+    unsigned         fMarkA  :  1;  // the mask
+    unsigned         fMarkB  :  1;  // the mask
+    unsigned         fMarkC  :  1;  // the mask
+    unsigned         TravId  : 26;  // the traversal ID
+    unsigned         Level   : 16;  // the direct level of the node
+    unsigned         LevelR  : 16;  // the reverse level of the node
+    Aig_Edge_t       Fans[2];       // the fanins
+    int              NextH;         // next node in the hash table          
+    int              Data;          // miscelleneous data
+    Aig_Man_t *      pMan;          // the parent manager
+};
+
+// the AIG manager
+struct Aig_Man_t_
+{
+    // the AIG parameters
+    Aig_Param_t      Param;         // the full set of AIG parameters
+    Aig_Param_t *    pParam;        // the pointer to the above set
+    // the nodes
+    Aig_Node_t *     pConst1;       // the constant 1 node (ID=0)
+    Vec_Ptr_t *      vNodes;        // all nodes by ID
+    Vec_Ptr_t *      vPis;          // all PIs
+    Vec_Ptr_t *      vPos;          // all POs
+    Aig_Table_t *    pTable;        // structural hash table
+    int              nLevelMax;     // the maximum level
+    // fanout representation
+    Vec_Ptr_t *      vFanPivots;    // fanout pivots
+    Vec_Ptr_t *      vFanFans0;     // the next fanout of the first fanin
+    Vec_Ptr_t *      vFanFans1;     // the next fanout of the second fanin 
+    // the memory managers
+    Aig_MemFixed_t * mmNodes;       // the memory manager for nodes
+    int              nTravIds;      // the traversal ID
+    // simulation info
+    Aig_SimInfo_t *  pInfo;         // random and systematic sim info for PIs
+    Aig_SimInfo_t *  pInfoTemp;     // temporary sim info for all nodes
+    // simulation patterns
+    int              nPiWords;      // the number of words in the PI info
+    int              nPatsMax;      // the max number of patterns 
+    Vec_Ptr_t *      vPats;         // simulation patterns to try
+    // equivalence classes
+    Vec_Vec_t *      vClasses;      // the non-trival equivalence classes of nodes
+    // temporary data
+    Vec_Ptr_t *      vFanouts;      // temporary storage for fanouts of a node
+    Vec_Ptr_t *      vToReplace;    // the nodes to replace
+};
+
+// the AIG simulation info
+struct Aig_SimInfo_t_  
+{
+    int              Type;          // the type (0 = PI, 1 = all)
+    int              nNodes;        // the number of nodes for which allocated
+    int              nWords;        // the number of words for each node
+    int              nPatsMax;      // the maximum number of patterns
+    int              nPatsCur;      // the current number of patterns
+    unsigned *       pData;         // the simulation data
+};
+
+// iterators over nodes, PIs, POs, ANDs
+#define Aig_ManForEachNode( pMan, pNode, i )                                                  \
+    for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ )
+#define Aig_ManForEachPi( pMan, pNode, i )                                                    \
+    for ( i = 0; (i < Aig_ManPiNum(pMan)) && (((pNode) = Aig_ManPi(pMan, i)), 1); i++ )
+#define Aig_ManForEachPo( pMan, pNode, i )                                                    \
+    for ( i = 0; (i < Aig_ManPoNum(pMan)) && (((pNode) = Aig_ManPo(pMan, i)), 1); i++ )
+#define Aig_ManForEachAnd( pNtk, pNode, i )                                                   \
+    for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ )   \
+        if ( Aig_NodeIsAnd(pNode) ) {} else
+
+// maximum/minimum operators
+#define AIG_MIN(a,b)  (((a) < (b))? (a) : (b))
+#define AIG_MAX(a,b)  (((a) > (b))? (a) : (b))
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int          Aig_BitWordNum( int nBits )            { return nBits/32 + ((nBits%32) > 0);    }
+
+static inline Aig_Node_t * Aig_ManNode( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vNodes, i);  }
+static inline Aig_Node_t * Aig_ManPi( Aig_Man_t * pMan, int i )   { return Vec_PtrEntry(pMan->vPis, i);    }
+static inline Aig_Node_t * Aig_ManPo( Aig_Man_t * pMan, int i )   { return Vec_PtrEntry(pMan->vPos, i);    }
+
+static inline int          Aig_ManNodeNum( Aig_Man_t * pMan )     { return Vec_PtrSize(pMan->vNodes);      }
+static inline int          Aig_ManPiNum( Aig_Man_t * pMan )       { return Vec_PtrSize(pMan->vPis);        }
+static inline int          Aig_ManPoNum( Aig_Man_t * pMan )       { return Vec_PtrSize(pMan->vPos);        }
+static inline int          Aig_ManAndNum( Aig_Man_t * pMan )      { return Aig_ManNodeNum(pMan)-Aig_ManPiNum(pMan)-Aig_ManPoNum(pMan)-1;  }
+
+static inline Aig_Node_t * Aig_Regular( Aig_Node_t * p )          { return (Aig_Node_t *)((unsigned)(p) & ~01);  }
+static inline Aig_Node_t * Aig_Not( Aig_Node_t * p )              { return (Aig_Node_t *)((unsigned)(p) ^  01);  }
+static inline Aig_Node_t * Aig_NotCond( Aig_Node_t * p, int c )   { return (Aig_Node_t *)((unsigned)(p) ^ (c));  }
+static inline bool         Aig_IsComplement( Aig_Node_t * p )     { return (bool)(((unsigned)p) & 01);           }
+
+static inline bool         Aig_NodeIsConst( Aig_Node_t * pNode )  { return Aig_Regular(pNode)->Id == 0;          }
+static inline bool         Aig_NodeIsPi( Aig_Node_t * pNode )     { return Aig_Regular(pNode)->Type == AIG_PI;   }
+static inline bool         Aig_NodeIsPo( Aig_Node_t * pNode )     { return Aig_Regular(pNode)->Type == AIG_PO;   }
+static inline bool         Aig_NodeIsAnd( Aig_Node_t * pNode )    { return Aig_Regular(pNode)->Type == AIG_AND;  }
+
+static inline int          Aig_NodeId( Aig_Node_t * pNode )       { assert( !Aig_IsComplement(pNode) ); return pNode->Id;                      }
+static inline int          Aig_NodeRefs( Aig_Node_t * pNode )     { assert( !Aig_IsComplement(pNode) ); return pNode->nRefs;                   }
+static inline bool         Aig_NodePhase( Aig_Node_t * pNode )    { assert( !Aig_IsComplement(pNode) ); return pNode->fPhase;                  }
+static inline int          Aig_NodeLevel( Aig_Node_t * pNode )    { assert( !Aig_IsComplement(pNode) ); return pNode->Level;                   }
+static inline int          Aig_NodeLevelR( Aig_Node_t * pNode )   { assert( !Aig_IsComplement(pNode) ); return pNode->LevelR;                  }
+static inline int          Aig_NodeData( Aig_Node_t * pNode )     { assert( !Aig_IsComplement(pNode) ); return pNode->Data;                    }
+static inline Aig_Man_t *  Aig_NodeMan( Aig_Node_t * pNode )      { assert( !Aig_IsComplement(pNode) ); return pNode->pMan;                    }
+static inline int          Aig_NodeFaninId0( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[0].iNode;           }
+static inline int          Aig_NodeFaninId1( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[1].iNode;           }
+static inline bool         Aig_NodeFaninC0( Aig_Node_t * pNode )  { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[0].fComp;           }
+static inline bool         Aig_NodeFaninC1( Aig_Node_t * pNode )  { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[1].fComp;           }
+static inline Aig_Node_t * Aig_NodeFanin0( Aig_Node_t * pNode )   { return Aig_ManNode( Aig_NodeMan(pNode), Aig_NodeFaninId0(pNode) );   }
+static inline Aig_Node_t * Aig_NodeFanin1( Aig_Node_t * pNode )   { return Aig_ManNode( Aig_NodeMan(pNode), Aig_NodeFaninId1(pNode) );   }
+static inline Aig_Node_t * Aig_NodeChild0( Aig_Node_t * pNode )   { return Aig_NotCond( Aig_NodeFanin0(pNode), Aig_NodeFaninC0(pNode) ); }
+static inline Aig_Node_t * Aig_NodeChild1( Aig_Node_t * pNode )   { return Aig_NotCond( Aig_NodeFanin1(pNode), Aig_NodeFaninC1(pNode) ); }
+static inline Aig_Node_t * Aig_NodeNextH( Aig_Node_t * pNode )    { return pNode->NextH? Aig_ManNode(pNode->pMan, pNode->NextH) : NULL;  }
+static inline int          Aig_NodeWhatFanin( Aig_Node_t * pNode, Aig_Node_t * pFanin )    { if ( Aig_NodeFaninId0(pNode) == pFanin->Id ) return 0; if ( Aig_NodeFaninId1(pNode) == pFanin->Id ) return 1; assert(0); return -1; }
+static inline int          Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); }
+
+static inline unsigned *   Aig_SimInfoForNode( Aig_SimInfo_t * p, Aig_Node_t * pNode )  { assert(  p->Type ); return p->pData + p->nWords * pNode->Id; }
+static inline unsigned *   Aig_SimInfoForPi( Aig_SimInfo_t * p, int Num )               { assert( !p->Type ); return p->pData + p->nWords * Num;       }
+
+static inline void         Aig_NodeSetTravId( Aig_Node_t * pNode, int TravId ) { pNode->TravId = TravId;                                    }
+static inline void         Aig_NodeSetTravIdCurrent( Aig_Node_t * pNode )      { pNode->TravId = pNode->pMan->nTravIds;                     }
+static inline void         Aig_NodeSetTravIdPrevious( Aig_Node_t * pNode )     { pNode->TravId = pNode->pMan->nTravIds - 1;                 }
+static inline bool         Aig_NodeIsTravIdCurrent( Aig_Node_t * pNode )       { return (bool)((int)pNode->TravId == pNode->pMan->nTravIds);     }
+static inline bool         Aig_NodeIsTravIdPrevious( Aig_Node_t * pNode )      { return (bool)((int)pNode->TravId == pNode->pMan->nTravIds - 1); }
+
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== aigCheck.c ==========================================================*/
+extern bool                Aig_ManCheck( Aig_Man_t * pMan );
+extern bool                Aig_NodeIsAcyclic( Aig_Node_t * pNode, Aig_Node_t * pRoot );
+/*=== aigFanout.c ==========================================================*/
+extern void                Aig_ManCreateFanouts( Aig_Man_t * p );
+extern void                Aig_NodeAddFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanout );
+extern void                Aig_NodeRemoveFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanoutToRemove );
+extern int                 Aig_NodeGetFanoutNum( Aig_Node_t * pNode );
+extern Vec_Ptr_t *         Aig_NodeGetFanouts( Aig_Node_t * pNode );
+extern int                 Aig_NodeGetLevelRNew( Aig_Node_t * pNode );
+extern int                 Aig_ManSetLevelR( Aig_Man_t * pMan );
+extern int                 Aig_ManGetLevelMax( Aig_Man_t * pMan );
+extern int                 Aig_NodeUpdateLevel_int( Aig_Node_t * pNode );
+extern int                 Aig_NodeUpdateLevelR_int( Aig_Node_t * pNode );
+/*=== aigMem.c =============================================================*/
+extern Aig_MemFixed_t *    Aig_MemFixedStart( int nEntrySize );
+extern void                Aig_MemFixedStop( Aig_MemFixed_t * p, int fVerbose );
+extern char *              Aig_MemFixedEntryFetch( Aig_MemFixed_t * p );
+extern void                Aig_MemFixedEntryRecycle( Aig_MemFixed_t * p, char * pEntry );
+extern void                Aig_MemFixedRestart( Aig_MemFixed_t * p );
+extern int                 Aig_MemFixedReadMemUsage( Aig_MemFixed_t * p );
+/*=== aigMan.c =============================================================*/
+extern void                Aig_ManSetDefaultParams( Aig_Param_t * pParam );
+extern Aig_Man_t *         Aig_ManStart( Aig_Param_t * pParam );
+extern int                 Aig_ManCleanup( Aig_Man_t * pMan );
+extern void                Aig_ManStop( Aig_Man_t * p );
+/*=== aigNode.c =============================================================*/
+extern Aig_Node_t *        Aig_NodeCreateConst( Aig_Man_t * p );
+extern Aig_Node_t *        Aig_NodeCreatePi( Aig_Man_t * p );
+extern Aig_Node_t *        Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin );
+extern Aig_Node_t *        Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 );
+extern void                Aig_NodeConnectAnd( Aig_Node_t * pFanin0, Aig_Node_t * pFanin1, Aig_Node_t * pNode );
+extern void                Aig_NodeDisconnectAnd( Aig_Node_t * pNode );
+extern void                Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot );
+extern void                Aig_NodePrint( Aig_Node_t * pNode );
+extern char *              Aig_NodeName( Aig_Node_t * pNode );
+/*=== aigOper.c ==========================================================*/
+extern Aig_Node_t *        Aig_And( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
+extern Aig_Node_t *        Aig_Or( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
+extern Aig_Node_t *        Aig_Xor( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
+extern Aig_Node_t *        Aig_Mux( Aig_Man_t * pMan, Aig_Node_t * pC, Aig_Node_t * p1, Aig_Node_t * p0 );
+extern Aig_Node_t *        Aig_Miter( Aig_Man_t * pMan, Vec_Ptr_t * vPairs );
+/*=== aigReplace.c ==========================================================*/
+extern void                Aig_ManReplaceNode( Aig_Man_t * pMan, Aig_Node_t * pOld, Aig_Node_t * pNew, int fUpdateLevel );
+/*=== aigTable.c ==========================================================*/
+extern Aig_Table_t *       Aig_TableCreate( int nSize );
+extern void                Aig_TableFree( Aig_Table_t * p );
+extern int                 Aig_TableNumNodes( Aig_Table_t * p );
+extern Aig_Node_t *        Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
+extern Aig_Node_t *        Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1, Aig_Node_t * pAnd );
+extern void                Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis );
+extern void                Aig_TableResize( Aig_Man_t * pMan );
+extern void                Aig_TableRehash( Aig_Man_t * pMan );
+/*=== aigUtil.c ==========================================================*/
+extern void                Aig_ManIncrementTravId( Aig_Man_t * pMan );
+extern void                Aig_PrintNode( Aig_Node_t * pNode );
+
+
+/*=== fraigClasses.c ==========================================================*/
+extern Vec_Vec_t *         Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfoAll );
+/*=== fraigSim.c ==========================================================*/
+extern Aig_SimInfo_t *     Aig_SimInfoAlloc( int nNodes, int nWords, int Type );
+extern void                Aig_SimInfoClean( Aig_SimInfo_t * p );
+extern void                Aig_SimInfoRandom( Aig_SimInfo_t * p );
+extern void                Aig_SimInfoResize( Aig_SimInfo_t * p );
+extern void                Aig_SimInfoFree( Aig_SimInfo_t * p );
+extern Aig_SimInfo_t *     Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/sat/aig/aigBalance.c b/src/sat/aig/aigBalance.c
new file mode 100644
index 00000000..1dd8ab01
--- /dev/null
+++ b/src/sat/aig/aigBalance.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [aigBalance.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigBalance.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigCheck.c b/src/sat/aig/aigCheck.c
new file mode 100644
index 00000000..a9facef3
--- /dev/null
+++ b/src/sat/aig/aigCheck.c
@@ -0,0 +1,146 @@
+/**CFile****************************************************************
+
+  FileName    [aigCheck.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Makes sure that every node in the table is in the network and vice versa.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Aig_ManCheck( Aig_Man_t * pMan )
+{
+    Aig_Node_t * pObj, * pAnd;
+    int i;
+    Aig_ManForEachNode( pMan, pObj, i )
+    {
+        if ( pObj == pMan->pConst1 || Aig_NodeIsPi(pObj) )
+        {
+            if ( pObj->Fans[0].iNode || pObj->Fans[1].iNode || pObj->Level )
+            {
+                printf( "Aig_ManCheck: The AIG has non-standard constant or PI node \"%d\".\n", pObj->Id );
+                return 0;
+            }
+            continue;
+        }
+        if ( Aig_NodeIsPo(pObj) )
+        {
+            if ( pObj->Fans[1].iNode )
+            {
+                printf( "Aig_ManCheck: The AIG has non-standard PO node \"%d\".\n", pObj->Id );
+                return 0;
+            }
+            continue;
+        }
+        // consider the AND node
+        if ( !pObj->Fans[0].iNode || !pObj->Fans[1].iNode )
+        {
+            printf( "Aig_ManCheck: The AIG has node \"%d\" with a constant fanin.\n", pObj->Id );
+            return 0;
+        }
+        if ( pObj->Fans[0].iNode > pObj->Fans[1].iNode )
+        {
+            printf( "Aig_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
+            return 0;
+        }
+        if ( pObj->Level != 1 + AIG_MAX(Aig_NodeFanin0(pObj)->Level, Aig_NodeFanin1(pObj)->Level) )
+            printf( "Aig_ManCheck: Node \"%d\" has level that does not agree with the fanin levels.\n", pObj->Id );
+        pAnd = Aig_TableLookupNode( pMan, Aig_NodeChild0(pObj), Aig_NodeChild1(pObj) );
+        if ( pAnd != pObj )
+            printf( "Aig_ManCheck: Node \"%d\" is not in the structural hashing table.\n", pObj->Id );
+    }
+    // count the number of nodes in the table
+    if ( Aig_TableNumNodes(pMan->pTable) != Aig_ManAndNum(pMan) )
+    {
+        printf( "Aig_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the node has a combination loop of depth 1 or 2.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Aig_NodeIsAcyclic( Aig_Node_t * pNode, Aig_Node_t * pRoot )
+{
+    Aig_Node_t * pFanin0, * pFanin1;
+    Aig_Node_t * pChild00, * pChild01;
+    Aig_Node_t * pChild10, * pChild11;
+    if ( !Aig_NodeIsAnd(pNode) )
+        return 1;
+    pFanin0 = Aig_NodeFanin0(pNode);
+    pFanin1 = Aig_NodeFanin1(pNode);
+    if ( pRoot == pFanin0 || pRoot == pFanin1 )
+        return 0;
+    if ( Aig_NodeIsPi(pFanin0) )
+    {
+        pChild00 = NULL;
+        pChild01 = NULL;
+    }
+    else
+    {
+        pChild00 = Aig_NodeFanin0(pFanin0);
+        pChild01 = Aig_NodeFanin1(pFanin0);
+        if ( pRoot == pChild00 || pRoot == pChild01 )
+            return 0;
+    }
+    if ( Aig_NodeIsPi(pFanin1) )
+    {
+        pChild10 = NULL;
+        pChild11 = NULL;
+    }
+    else
+    {
+        pChild10 = Aig_NodeFanin0(pFanin1);
+        pChild11 = Aig_NodeFanin1(pFanin1);
+        if ( pRoot == pChild10 || pRoot == pChild11 )
+            return 0;
+    }
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigFanout.c b/src/sat/aig/aigFanout.c
new file mode 100644
index 00000000..aed38426
--- /dev/null
+++ b/src/sat/aig/aigFanout.c
@@ -0,0 +1,423 @@
+/**CFile****************************************************************
+
+  FileName    [aigFanout.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigFanout.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Node_t *  Aig_NodeFanPivot( Aig_Node_t * pNode )                { return Vec_PtrEntry(pNode->pMan->vFanPivots, pNode->Id); }
+static inline Aig_Node_t *  Aig_NodeFanFan0( Aig_Node_t * pNode )                 { return Vec_PtrEntry(pNode->pMan->vFanFans0, pNode->Id);  }
+static inline Aig_Node_t *  Aig_NodeFanFan1( Aig_Node_t * pNode )                 { return Vec_PtrEntry(pNode->pMan->vFanFans1, pNode->Id);  }
+static inline Aig_Node_t ** Aig_NodeFanPivotPlace( Aig_Node_t * pNode )           { return ((Aig_Node_t **)pNode->pMan->vFanPivots->pArray) + pNode->Id; }
+static inline Aig_Node_t ** Aig_NodeFanFan0Place( Aig_Node_t * pNode )            { return ((Aig_Node_t **)pNode->pMan->vFanFans0->pArray) + pNode->Id;  }
+static inline Aig_Node_t ** Aig_NodeFanFan1Place( Aig_Node_t * pNode )            { return ((Aig_Node_t **)pNode->pMan->vFanFans1->pArray) + pNode->Id;  }
+static inline void Aig_NodeSetFanPivot( Aig_Node_t * pNode, Aig_Node_t * pNode2 ) { Vec_PtrWriteEntry(pNode->pMan->vFanPivots, pNode->Id, pNode2); }
+static inline void Aig_NodeSetFanFan0( Aig_Node_t * pNode, Aig_Node_t * pNode2 )  { Vec_PtrWriteEntry(pNode->pMan->vFanFans0, pNode->Id, pNode2);  }
+static inline void Aig_NodeSetFanFan1( Aig_Node_t * pNode, Aig_Node_t * pNode2 )  { Vec_PtrWriteEntry(pNode->pMan->vFanFans1, pNode->Id, pNode2);  }
+static inline Aig_Node_t * Aig_NodeNextFanout( Aig_Node_t * pNode, Aig_Node_t * pFanout )       { if ( pFanout == NULL ) return NULL; return Aig_NodeFaninId0(pFanout) == pNode->Id? Aig_NodeFanFan0(pFanout) : Aig_NodeFanFan1(pFanout); }
+static inline Aig_Node_t ** Aig_NodeNextFanoutPlace( Aig_Node_t * pNode, Aig_Node_t * pFanout ) { return Aig_NodeFaninId0(pFanout) == pNode->Id? Aig_NodeFanFan0Place(pFanout) : Aig_NodeFanFan1Place(pFanout); }
+
+// iterator through the fanouts of the node
+#define Aig_NodeForEachFanout( pNode, pFanout )                           \
+    for ( pFanout = Aig_NodeFanPivot(pNode); pFanout;                     \
+          pFanout = Aig_NodeNextFanout(pNode, pFanout) )
+// safe iterator through the fanouts of the node
+#define Aig_NodeForEachFanoutSafe( pNode, pFanout, pFanout2 )             \
+    for ( pFanout  = Aig_NodeFanPivot(pNode),                             \
+          pFanout2 = Aig_NodeNextFanout(pNode, pFanout);              \
+          pFanout;                                                        \
+          pFanout  = pFanout2,                                            \
+          pFanout2 = Aig_NodeNextFanout(pNode, pFanout) )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the fanouts for all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCreateFanouts( Aig_Man_t * p )
+{
+    Aig_Node_t * pNode;
+    int i;
+    assert( p->vFanPivots == NULL );
+    p->vFanPivots = Vec_PtrStart( Aig_ManNodeNum(p) );
+    p->vFanFans0  = Vec_PtrStart( Aig_ManNodeNum(p) );
+    p->vFanFans1  = Vec_PtrStart( Aig_ManNodeNum(p) );
+    Aig_ManForEachNode( p, pNode, i )
+    {
+        if ( Aig_NodeIsPi(pNode) || i == 0 )
+            continue;
+        Aig_NodeAddFaninFanout( Aig_NodeFanin0(pNode), pNode );
+        if ( Aig_NodeIsPo(pNode) )
+            continue;
+        Aig_NodeAddFaninFanout( Aig_NodeFanin1(pNode), pNode );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the fanouts for all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Aig_ManResizeFanouts( Aig_Man_t * p, int nSizeNew )
+{
+    assert( p->vFanPivots );
+    if ( Vec_PtrSize(p->vFanPivots) < nSizeNew )
+    {
+        Vec_PtrFillExtra( p->vFanPivots, nSizeNew + 1000, NULL );
+        Vec_PtrFillExtra( p->vFanFans0,  nSizeNew + 1000, NULL );
+        Vec_PtrFillExtra( p->vFanFans1,  nSizeNew + 1000, NULL );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add the fanout to the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeAddFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanout )
+{
+    Aig_Node_t * pPivot;
+
+    // check that they are not complemented
+    assert( !Aig_IsComplement(pFanin) );
+    assert( !Aig_IsComplement(pFanout) );
+    // check that pFanins is a fanin of pFanout
+    assert( Aig_NodeFaninId0(pFanout) == pFanin->Id || Aig_NodeFaninId1(pFanout) == pFanin->Id );
+
+    // resize the fanout manager
+    Aig_ManResizeFanouts( pFanin->pMan, 1 + AIG_MAX(pFanin->Id, pFanout->Id) );
+
+    // consider the case of the first fanout
+    pPivot = Aig_NodeFanPivot(pFanin);
+    if ( pPivot == NULL )
+    {
+        Aig_NodeSetFanPivot( pFanin, pFanout );
+        return;
+    }
+
+    // consider the case of more than one fanouts
+    if ( Aig_NodeFaninId0(pPivot) == pFanin->Id )
+    {
+        if ( Aig_NodeFaninId0(pFanout) == pFanin->Id )
+        {
+            Aig_NodeSetFanFan0( pFanout, Aig_NodeFanFan0(pPivot) );
+            Aig_NodeSetFanFan0( pPivot, pFanout );
+        }
+        else // if ( Aig_NodeFaninId1(pFanout) == pFanin->Id )
+        {
+            Aig_NodeSetFanFan1( pFanout, Aig_NodeFanFan0(pPivot) );
+            Aig_NodeSetFanFan0( pPivot, pFanout );
+        }
+    }
+    else // if ( Aig_NodeFaninId1(pPivot) == pFanin->Id )
+    {
+        assert( Aig_NodeFaninId1(pPivot) == pFanin->Id );
+        if ( Aig_NodeFaninId0(pFanout) == pFanin->Id )
+        {
+            Aig_NodeSetFanFan0( pFanout, Aig_NodeFanFan1(pPivot) );
+            Aig_NodeSetFanFan1( pPivot, pFanout );
+        }
+        else // if ( Aig_NodeFaninId1(pFanout) == pFanin->Id )
+        {
+            Aig_NodeSetFanFan1( pFanout, Aig_NodeFanFan1(pPivot) );
+            Aig_NodeSetFanFan1( pPivot, pFanout );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add the fanout to the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeRemoveFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanoutToRemove )
+{
+    Aig_Node_t * pFanout, * pFanout2, ** ppFanList;
+    // start the linked list of fanouts
+    ppFanList = Aig_NodeFanPivotPlace(pFanin); 
+    // go through the fanouts
+    Aig_NodeForEachFanoutSafe( pFanin, pFanout, pFanout2 )
+    {
+        // skip the fanout-to-remove
+        if ( pFanout == pFanoutToRemove )
+            continue;
+        // add useful fanouts to the list
+        *ppFanList = pFanout;
+        ppFanList = Aig_NodeNextFanoutPlace( pFanin, pFanout );
+    }
+    *ppFanList = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of fanouts of a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeGetFanoutNum( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanout;
+    int Counter = 0;
+    Aig_NodeForEachFanout( pNode, pFanout )
+        Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_NodeGetFanouts( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanout;
+    Vec_PtrClear( pNode->pMan->vFanouts );
+    Aig_NodeForEachFanout( pNode, pFanout )
+        Vec_PtrPush( pNode->pMan->vFanouts, pFanout );
+    return pNode->pMan->vFanouts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the node has at least one complemented fanout.]
+
+  Description [A fanout is complemented if the fanout's fanin edge pointing
+  to the given node is complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Aig_NodeHasComplFanoutEdge( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanout;
+    int iFanin;
+    Aig_NodeForEachFanout( pNode, pFanout )
+    {
+        iFanin = Aig_NodeWhatFanin( pFanout, pNode );
+        assert( iFanin >= 0 );
+        if ( iFanin && Aig_NodeFaninC1(pFanout) || !iFanin && Aig_NodeFaninC0(pFanout) )
+            return 1;
+    }
+    return 0;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes and assigns the reverse level of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Aig_NodeSetLevelR_rec( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanout;
+    int LevelR = 0;
+    if ( Aig_NodeIsPo(pNode) )
+        return pNode->LevelR = 0;
+    Aig_NodeForEachFanout( pNode, pFanout )
+        if ( LevelR < Aig_NodeSetLevelR_rec(pFanout) )
+            LevelR = pFanout->LevelR;
+    return pNode->LevelR = 1 + LevelR;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the reverse level of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManSetLevelR( Aig_Man_t * pMan )
+{
+    Aig_Node_t * pNode;
+    int i, LevelR = 0;
+    Aig_ManForEachPi( pMan, pNode, i )
+        if ( LevelR < Aig_NodeSetLevelR_rec(pNode) )
+            LevelR = pNode->LevelR;
+    return LevelR;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the global number of logic levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManGetLevelMax( Aig_Man_t * pMan )
+{
+    Aig_Node_t * pNode;
+    int i, LevelsMax = 0;
+    Aig_ManForEachPo( pMan, pNode, i )
+        if ( LevelsMax < (int)pNode->Level )
+            LevelsMax = (int)pNode->Level;
+    return LevelsMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes but does not assign the reverse level of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeGetLevelRNew( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanout;
+    unsigned LevelR = 0;
+    Aig_NodeForEachFanout( pNode, pFanout )
+        LevelR = AIG_MAX( LevelR, pFanout->LevelR );
+    return LevelR + !Aig_NodeIsPi(pNode);
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the direct level of one node.]
+
+  Description [Returns 1 if direct level of at least one CO was changed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeUpdateLevel_int( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanout;
+    unsigned LevelNew, fStatus = 0;
+    Aig_NodeForEachFanout( pNode, pFanout )
+    {
+        LevelNew = Aig_NodeGetLevelNew( pFanout );
+        if ( pFanout->Level == LevelNew )
+            continue;
+        // the level has changed
+        pFanout->Level = LevelNew;
+        if ( Aig_NodeIsPo(pNode) )
+            fStatus = 1;
+        else
+            fStatus |= Aig_NodeUpdateLevel_int( pFanout );
+    }
+    return fStatus;    
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the reverse level of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeUpdateLevelR_int( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanin;
+    unsigned LevelNew;
+    assert( !Aig_NodeIsPo(pNode) );
+    pFanin = Aig_NodeFanin0(pNode);
+    LevelNew = Aig_NodeGetLevelRNew(pFanin);
+    if ( pFanin->LevelR != LevelNew )
+    {
+        pFanin->LevelR = LevelNew;
+        if ( Aig_NodeIsAnd(pFanin) )
+            Aig_NodeUpdateLevelR_int( pFanin );
+    }
+    pFanin = Aig_NodeFanin1(pNode);
+    LevelNew = Aig_NodeGetLevelRNew(pFanin);
+    if ( pFanin->LevelR != LevelNew )
+    {
+        pFanin->LevelR = LevelNew;
+        if ( Aig_NodeIsAnd(pFanin) )
+            Aig_NodeUpdateLevelR_int( pFanin );
+    }
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigMan.c b/src/sat/aig/aigMan.c
new file mode 100644
index 00000000..2058f6b0
--- /dev/null
+++ b/src/sat/aig/aigMan.c
@@ -0,0 +1,142 @@
+/**CFile****************************************************************
+
+  FileName    [aigMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManSetDefaultParams( Aig_Param_t * pParam )
+{
+    memset( pParam, 0, sizeof(Aig_Param_t) );
+    pParam->nPatsRand = 1024;  // the number of random patterns
+    pParam->nBTLimit  =   99;  // backtrack limit at the intermediate nodes
+    pParam->nSeconds  =    1;  // the timeout for the final miter in seconds
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam )
+{
+    Aig_Man_t * p;
+    // set the random seed for simulation
+    srand( 0xDEADCAFE );
+    // start the manager
+    p = ALLOC( Aig_Man_t, 1 );
+    memset( p, 0, sizeof(Aig_Man_t) );
+    p->pParam = &p->Param;
+    p->nTravIds = 1;
+    // set the defaults
+    *p->pParam = *pParam;
+    // start memory managers
+    p->mmNodes    = Aig_MemFixedStart( sizeof(Aig_Node_t) );
+    // allocate node arrays
+    p->vPis       = Vec_PtrAlloc( 1000 );    // the array of primary inputs
+    p->vPos       = Vec_PtrAlloc( 1000 );    // the array of primary outputs
+    p->vNodes     = Vec_PtrAlloc( 1000 );    // the array of internal nodes
+    // start the table
+    p->pTable     = Aig_TableCreate( 1000 );
+    // create the constant node
+    p->pConst1    = Aig_NodeCreateConst( p );
+    // initialize other variables
+    p->vFanouts   = Vec_PtrAlloc( 10 ); 
+    p->vToReplace = Vec_PtrAlloc( 10 ); 
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCleanup( Aig_Man_t * pMan )
+{
+    Aig_Node_t * pAnd;
+    int i, nNodesOld;
+    nNodesOld = Aig_ManAndNum(pMan);
+    Aig_ManForEachAnd( pMan, pAnd, i )
+        if ( pAnd->nRefs == 0 )
+            Aig_NodeDeleteAnd_rec( pMan, pAnd );
+    return nNodesOld - Aig_ManAndNum(pMan);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManStop( Aig_Man_t * p )
+{
+    if ( p->vFanPivots ) Vec_PtrFree( p->vFanPivots );
+    if ( p->vFanFans0 )  Vec_PtrFree( p->vFanFans0 );
+    if ( p->vFanFans1 )  Vec_PtrFree( p->vFanFans1 );
+    if ( p->vClasses  )  Vec_VecFree( p->vClasses );
+    Aig_MemFixedStop( p->mmNodes, 0 );
+    Vec_PtrFree( p->vNodes );
+    Vec_PtrFree( p->vPis );
+    Vec_PtrFree( p->vPos );
+    Vec_PtrFree( p->vFanouts );
+    Vec_PtrFree( p->vToReplace );
+    Aig_TableFree( p->pTable );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigMem.c b/src/sat/aig/aigMem.c
new file mode 100644
index 00000000..280cf98b
--- /dev/null
+++ b/src/sat/aig/aigMem.c
@@ -0,0 +1,246 @@
+/**CFile****************************************************************
+
+  FileName    [aigMem.c]
+
+  PackageName [ABC: Logic synthesis and verification system.]
+
+  Synopsis    [Fixed-size-entry memory manager for the AIG package.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 2.0. Started - October 1, 2004]
+
+  Revision    [$Id: aigMem.c,v 1.4 2005/07/08 01:01:31 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Aig_MemFixed_t_
+{
+    // information about individual entries
+    int           nEntrySize;    // the size of one entry
+    int           nEntriesAlloc; // the total number of entries allocated
+    int           nEntriesUsed;  // the number of entries in use
+    int           nEntriesMax;   // the max number of entries in use
+    char *        pEntriesFree;  // the linked list of free entries
+
+    // this is where the memory is stored
+    int           nChunkSize;    // the size of one chunk
+    int           nChunksAlloc;  // the maximum number of memory chunks 
+    int           nChunks;       // the current number of memory chunks 
+    char **       pChunks;       // the allocated memory
+
+    // statistics
+    int           nMemoryUsed;   // memory used in the allocated entries
+    int           nMemoryAlloc;  // memory allocated
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the internal memory manager.]
+
+  Description [Can only work with entry size at least 4 byte long.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_MemFixed_t * Aig_MemFixedStart( int nEntrySize )
+{
+    Aig_MemFixed_t * p;
+
+    p = ALLOC( Aig_MemFixed_t, 1 );
+    memset( p, 0, sizeof(Aig_MemFixed_t) );
+
+    p->nEntrySize    = nEntrySize;
+    p->nEntriesAlloc = 0;
+    p->nEntriesUsed  = 0;
+    p->pEntriesFree  = NULL;
+
+    if ( nEntrySize * (1 << 10) < (1<<16) )
+        p->nChunkSize = (1 << 10);
+    else
+        p->nChunkSize = (1<<16) / nEntrySize;
+    if ( p->nChunkSize < 8 )
+        p->nChunkSize = 8;
+
+    p->nChunksAlloc  = 64;
+    p->nChunks       = 0;
+    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+
+    p->nMemoryUsed   = 0;
+    p->nMemoryAlloc  = 0;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the internal memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_MemFixedStop( Aig_MemFixed_t * p, int fVerbose )
+{
+    int i;
+    if ( p == NULL )
+        return;
+    if ( fVerbose )
+    {
+        printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
+            p->nEntrySize, p->nChunkSize, p->nChunks );
+        printf( "   Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
+            p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
+    }
+    for ( i = 0; i < p->nChunks; i++ )
+        free( p->pChunks[i] );
+    free( p->pChunks );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts one entry from the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Aig_MemFixedEntryFetch( Aig_MemFixed_t * p )
+{
+    char * pTemp;
+    int i;
+
+    // check if there are still free entries
+    if ( p->nEntriesUsed == p->nEntriesAlloc )
+    { // need to allocate more entries
+        assert( p->pEntriesFree == NULL );
+        if ( p->nChunks == p->nChunksAlloc )
+        {
+            p->nChunksAlloc *= 2;
+            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+        }
+        p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
+        p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
+        // transform these entries into a linked list
+        pTemp = p->pEntriesFree;
+        for ( i = 1; i < p->nChunkSize; i++ )
+        {
+            *((char **)pTemp) = pTemp + p->nEntrySize;
+            pTemp += p->nEntrySize;
+        }
+        // set the last link
+        *((char **)pTemp) = NULL;
+        // add the chunk to the chunk storage
+        p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
+        // add to the number of entries allocated
+        p->nEntriesAlloc += p->nChunkSize;
+    }
+    // incrememt the counter of used entries
+    p->nEntriesUsed++;
+    if ( p->nEntriesMax < p->nEntriesUsed )
+        p->nEntriesMax = p->nEntriesUsed;
+    // return the first entry in the free entry list
+    pTemp = p->pEntriesFree;
+    p->pEntriesFree = *((char **)pTemp);
+    return pTemp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns one entry into the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_MemFixedEntryRecycle( Aig_MemFixed_t * p, char * pEntry )
+{
+    // decrement the counter of used entries
+    p->nEntriesUsed--;
+    // add the entry to the linked list of free entries
+    *((char **)pEntry) = p->pEntriesFree;
+    p->pEntriesFree = pEntry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees all associated memory and resets the manager.]
+
+  Description [Relocates all the memory except the first chunk.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_MemFixedRestart( Aig_MemFixed_t * p )
+{
+    int i;
+    char * pTemp;
+
+    // delocate all chunks except the first one
+    for ( i = 1; i < p->nChunks; i++ )
+        free( p->pChunks[i] );
+    p->nChunks = 1;
+    // transform these entries into a linked list
+    pTemp = p->pChunks[0];
+    for ( i = 1; i < p->nChunkSize; i++ )
+    {
+        *((char **)pTemp) = pTemp + p->nEntrySize;
+        pTemp += p->nEntrySize;
+    }
+    // set the last link
+    *((char **)pTemp) = NULL;
+    // set the free entry list
+    p->pEntriesFree  = p->pChunks[0];
+    // set the correct statistics
+    p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
+    p->nMemoryUsed   = 0;
+    p->nEntriesAlloc = p->nChunkSize;
+    p->nEntriesUsed  = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reports the memory usage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_MemFixedReadMemUsage( Aig_MemFixed_t * p )
+{
+    return p->nMemoryAlloc;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigNode.c b/src/sat/aig/aigNode.c
new file mode 100644
index 00000000..afccd985
--- /dev/null
+++ b/src/sat/aig/aigNode.c
@@ -0,0 +1,292 @@
+/**CFile****************************************************************
+
+  FileName    [aigNode.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigNode.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Node_t * Aig_NodeCreate( Aig_Man_t * p )
+{
+    Aig_Node_t * pNode;
+    // create the node
+    pNode = (Aig_Node_t *)Aig_MemFixedEntryFetch( p->mmNodes );
+    memset( pNode, 0, sizeof(Aig_Node_t) );
+    // assign the number and add to the array of nodes
+    pNode->Id = p->vNodes->nSize;
+    Vec_PtrPush( p->vNodes, pNode );
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the constant 1 node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p )
+{
+    Aig_Node_t * pNode;
+    pNode = Aig_NodeCreate( p );
+    pNode->fPhase = 1; // sim value for 000... pattern
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a primary input node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p )
+{
+    Aig_Node_t * pNode;
+    pNode = Aig_NodeCreate( p );
+    Vec_PtrPush( p->vPis, pNode );
+    pNode->fPhase  =  0;  // sim value for 000... pattern
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a primary output node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin )
+{
+    Aig_Node_t * pNode;
+    pNode = Aig_NodeCreate( p );
+    Vec_PtrPush( p->vPos, pNode );
+    // connect to the fanin
+    pNode->Fans[0].fComp = Aig_IsComplement(pFanin);
+    pNode->Fans[0].iNode = Aig_Regular(pFanin)->Id;
+    pNode->fPhase = pNode->Fans[0].fComp ^ Aig_Regular(pFanin)->fPhase;  // sim value for 000... pattern
+    pNode->Level = Aig_Regular(pFanin)->Level;
+    Aig_Regular(pFanin)->nRefs++;
+    if ( pNode->pMan->vFanPivots )  Aig_NodeAddFaninFanout( pFanin, pNode );
+    // update global level if needed
+    if ( p->nLevelMax < (int)pNode->Level )
+        p->nLevelMax = pNode->Level;
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 )
+{
+    Aig_Node_t * pNode;
+    pNode = Aig_NodeCreate( p );
+    Aig_NodeConnectAnd( pFanin0, pFanin1, pNode );
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connects the nodes to the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeConnectAnd( Aig_Node_t * pFanin0, Aig_Node_t * pFanin1, Aig_Node_t * pNode )
+{
+    assert( !Aig_IsComplement(pNode) );
+    assert( Aig_NodeIsAnd(pNode) );
+    // add the fanins
+    pNode->Fans[0].fComp = Aig_IsComplement(pFanin0);
+    pNode->Fans[0].iNode = Aig_Regular(pFanin0)->Id;
+    pNode->Fans[1].fComp = Aig_IsComplement(pFanin1);
+    pNode->Fans[1].iNode = Aig_Regular(pFanin1)->Id;
+    // compute the phase (sim value for 000... pattern)
+    pNode->fPhase = (pNode->Fans[0].fComp ^ Aig_Regular(pFanin0)->fPhase) & 
+                    (pNode->Fans[1].fComp ^ Aig_Regular(pFanin1)->fPhase);
+    pNode->Level = Aig_NodeGetLevelNew(pNode);
+    // reference the fanins
+    Aig_Regular(pFanin0)->nRefs++;
+    Aig_Regular(pFanin1)->nRefs++;
+    // add the fanouts
+    if ( pNode->pMan->vFanPivots )  Aig_NodeAddFaninFanout( pFanin0, pNode );
+    if ( pNode->pMan->vFanPivots )  Aig_NodeAddFaninFanout( pFanin1, pNode );
+    // add the node to the structural hash table
+    Aig_TableInsertNode( pNode->pMan, pFanin0, pFanin1, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connects the nodes to the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeDisconnectAnd( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pFanin0, * pFanin1;
+    assert( !Aig_IsComplement(pNode) );
+    assert( Aig_NodeIsAnd(pNode) );
+    // get the fanins
+    pFanin0 = Aig_NodeFanin0(pNode);
+    pFanin1 = Aig_NodeFanin1(pNode);
+    // dereference the fanins
+    pFanin0->nRefs--;
+    pFanin0->nRefs--;
+    // remove the fanouts
+    if ( pNode->pMan->vFanPivots )  Aig_NodeRemoveFaninFanout( pFanin0, pNode );
+    if ( pNode->pMan->vFanPivots )  Aig_NodeRemoveFaninFanout( pFanin1, pNode );
+    // remove the node from the structural hash table
+    Aig_TableDeleteNode( pNode->pMan, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs internal deletion step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot )
+{
+    Aig_Node_t * pNode0, * pNode1;
+    // make sure the node is regular and dangling
+    assert( !Aig_IsComplement(pRoot) );
+    assert( pRoot->nRefs == 0 );
+    assert( Aig_NodeIsAnd(pRoot) );
+    // save the children
+    pNode0 = Aig_NodeFanin0(pRoot);
+    pNode1 = Aig_NodeFanin1(pRoot);
+    // disconnect the node
+    Aig_NodeDisconnectAnd( pRoot );
+    // recycle the node
+    Vec_PtrWriteEntry( pMan->vNodes, pRoot->Id, NULL );
+    Aig_MemFixedEntryRecycle( pMan->mmNodes, (char *)pRoot );
+    // call recursively
+    if ( Aig_NodeIsAnd(pNode0) && pNode0->nRefs == 0 )
+        Aig_NodeDeleteAnd_rec( pMan, pNode0 );
+    if ( Aig_NodeIsAnd(pNode1) && pNode1->nRefs == 0 )
+        Aig_NodeDeleteAnd_rec( pMan, pNode1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the AIG node for debugging purposes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodePrint( Aig_Node_t * pNode )
+{
+    Aig_Node_t * pNodeR = Aig_Regular(pNode);
+    if ( Aig_NodeIsPi(pNode) )
+    {
+        printf( "PI %4s%s.\n", Aig_NodeName(pNode), Aig_IsComplement(pNode)? "\'" : "" );
+        return;
+    }
+    if ( Aig_NodeIsConst(pNode) )
+    {
+        printf( "Constant 1 %s.\n", Aig_IsComplement(pNode)? "(complemented)" : ""  );
+        return;
+    }
+    // print the node's function
+    printf( "%7s%s", Aig_NodeName(pNodeR),                 Aig_IsComplement(pNode)? "\'" : "" );
+    printf( " = " );
+    printf( "%7s%s", Aig_NodeName(Aig_NodeFanin0(pNodeR)), Aig_NodeFaninC0(pNodeR)? "\'" : "" );
+    printf( " * " );
+    printf( "%7s%s", Aig_NodeName(Aig_NodeFanin1(pNodeR)), Aig_NodeFaninC1(pNodeR)? "\'" : "" );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the name of the node.]
+
+  Description [The name should be used before this procedure is called again.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Aig_NodeName( Aig_Node_t * pNode )
+{
+    static char Buffer[100];
+    sprintf( Buffer, "%d", Aig_Regular(pNode)->Id );
+    return Buffer;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigOper.c b/src/sat/aig/aigOper.c
new file mode 100644
index 00000000..a10cc7ff
--- /dev/null
+++ b/src/sat/aig/aigOper.c
@@ -0,0 +1,175 @@
+/**CFile****************************************************************
+
+  FileName    [aigOper.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigOper.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description [The argument nodes can be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_And( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 )
+{
+    Aig_Node_t * pAnd;
+    // check for trivial cases
+    if ( p0 == p1 )
+        return p0;
+    if ( p0 == Aig_Not(p1) )
+        return Aig_Not(pMan->pConst1);
+    if ( Aig_Regular(p0) == pMan->pConst1 )
+    {
+        if ( p0 == pMan->pConst1 )
+            return p1;
+        return Aig_Not(pMan->pConst1);
+    }
+    if ( Aig_Regular(p1) == pMan->pConst1 )
+    {
+        if ( p1 == pMan->pConst1 )
+            return p0;
+        return Aig_Not(pMan->pConst1);
+    }
+    // order the arguments
+    if ( Aig_Regular(p0)->Id > Aig_Regular(p1)->Id )
+    {
+        if ( pAnd = Aig_TableLookupNode( pMan, p1, p0 ) )
+            return pAnd;
+        return Aig_NodeCreateAnd( pMan, p1, p0 );
+    }
+    else
+    {
+        if ( pAnd = Aig_TableLookupNode( pMan, p0, p1 ) )
+            return pAnd;
+        return Aig_NodeCreateAnd( pMan, p0, p1 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements Boolean OR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_Or( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 )
+{
+    return Aig_Not( Aig_And( pMan, Aig_Not(p0), Aig_Not(p1) ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements Boolean XOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_Xor( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 )
+{
+    return Aig_Or( pMan, Aig_And(pMan, p0, Aig_Not(p1)), 
+                         Aig_And(pMan, p1, Aig_Not(p0)) );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_Mux( Aig_Man_t * pMan, Aig_Node_t * pC, Aig_Node_t * p1, Aig_Node_t * p0 )
+{
+    return Aig_Or( pMan, Aig_And(pMan, pC, p1), Aig_And(pMan, Aig_Not(pC), p0) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_Miter_rec( Aig_Man_t * pMan, Aig_Node_t ** ppObjs, int nObjs )
+{
+    Aig_Node_t * pObj1, * pObj2;
+    if ( nObjs == 1 )
+        return ppObjs[0];
+    pObj1 = Aig_Miter_rec( pMan, ppObjs,           nObjs/2         );
+    pObj2 = Aig_Miter_rec( pMan, ppObjs + nObjs/2, nObjs - nObjs/2 );
+    return Aig_Or( pMan, pObj1, pObj2 );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Implements the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_Miter( Aig_Man_t * pMan, Vec_Ptr_t * vPairs )
+{
+    int i;
+    if ( vPairs->nSize == 0 )
+        return Aig_Not( pMan->pConst1 );
+    assert( vPairs->nSize % 2 == 0 );
+    // go through the cubes of the node's SOP
+    for ( i = 0; i < vPairs->nSize; i += 2 )
+        vPairs->pArray[i/2] = Aig_Xor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] );
+    vPairs->nSize = vPairs->nSize/2;
+    return Aig_Miter_rec( pMan, (Aig_Node_t **)vPairs->pArray, vPairs->nSize );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigReplace.c b/src/sat/aig/aigReplace.c
new file mode 100644
index 00000000..d928fdf8
--- /dev/null
+++ b/src/sat/aig/aigReplace.c
@@ -0,0 +1,133 @@
+/**CFile****************************************************************
+
+  FileName    [aigUpdate.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigUpdate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs internal replacement step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Abc_AigReplace_int( Aig_Man_t * pMan, int fUpdateLevel )
+{
+    Vec_Ptr_t * vFanouts;
+    Aig_Node_t * pOld, * pNew, * pFanin0, * pFanin1, * pFanout, * pTemp, * pFanoutNew;
+    int k, iFanin;
+    // get the pair of nodes to replace
+    assert( Vec_PtrSize(pMan->vToReplace) > 0 );
+    pNew = Vec_PtrPop( pMan->vToReplace );
+    pOld = Vec_PtrPop( pMan->vToReplace );
+    // make sure the old node is internal, regular, and has fanouts
+    // (the new node can be PI or internal, is complemented, and can have fanouts)
+    assert( !Aig_IsComplement(pOld) );
+    assert( pOld->nRefs > 0 );
+    assert( Aig_NodeIsAnd(pOld) );
+    assert( Aig_NodeIsPo(pNew) );
+    // look at the fanouts of old node
+    vFanouts = Aig_NodeGetFanouts( pOld );
+    Vec_PtrForEachEntry( vFanouts, pFanout, k )
+    {
+        if ( Aig_NodeIsPo(pFanout) )
+        {
+            // patch the first fanin of the PO
+            pFanout->Fans[0].iNode  = Aig_Regular(pNew)->Id;
+            pFanout->Fans[0].fComp ^= Aig_IsComplement(pNew);
+            continue;
+        }
+        // find the old node as a fanin of this fanout
+        iFanin = Aig_NodeWhatFanin( pFanout, pOld );
+        assert( iFanin == 0 || iFanin == 1 );
+        // get the new fanin
+        pFanin0 = Aig_NotCond( pNew, pFanout->Fans[iFanin].fComp );
+        assert( Aig_Regular(pFanin0) != pFanout );
+        // get another fanin
+        pFanin1 = iFanin? Aig_NodeChild0(pFanout) : Aig_NodeChild1(pFanout);
+        assert( Aig_Regular(pFanin1) != pFanout );
+        assert( Aig_Regular(pFanin0) != Aig_Regular(pFanin1) );             
+        // order them
+        if ( Aig_Regular(pFanin0)->Id > Aig_Regular(pFanin1)->Id ) 
+            pTemp = pFanin0, pFanin0 = pFanin1, pFanin1 = pTemp;
+        // check if the node with these fanins exists
+        if ( pFanoutNew = Aig_TableLookupNode( pMan, pFanin0, pFanin1 ) )
+        { // such node exists (it may be a constant)
+            // schedule replacement of the old fanout by the new fanout
+            Vec_PtrPush( pMan->vToReplace, pFanout );
+            Vec_PtrPush( pMan->vToReplace, pFanoutNew );
+            continue;
+        }
+        // such node does not exist - modify the old fanout node 
+        // (this way the change will not propagate all the way to the COs)
+        Aig_NodeDisconnectAnd( pFanout );
+        Aig_NodeConnectAnd( pFanin0, pFanin1, pFanout );
+        // recreate the old fanout with new fanins and add it to the table
+        assert( Aig_NodeIsAcyclic(pFanout, pFanout) );
+        // update the level if requested
+        if ( fUpdateLevel )
+        {
+            if ( Aig_NodeUpdateLevel_int(pFanout) )
+                pMan->nLevelMax = Aig_ManGetLevelMax( pMan );
+            //Aig_NodeGetLevelRNew( pFanout );
+            Aig_NodeUpdateLevelR_int( pFanout );
+        }
+    }
+    // if the node has no fanouts left, remove its MFFC
+    if ( pOld->nRefs == 0 )
+        Aig_NodeDeleteAnd_rec( pMan, pOld );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces one AIG node by the other.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManReplaceNode( Aig_Man_t * pMan, Aig_Node_t * pOld, Aig_Node_t * pNew, int fUpdateLevel )
+{
+    assert( Vec_PtrSize(pMan->vToReplace) == 0 );
+    Vec_PtrPush( pMan->vToReplace, pOld );
+    Vec_PtrPush( pMan->vToReplace, pNew );
+    while ( Vec_PtrSize(pMan->vToReplace) )
+        Abc_AigReplace_int( pMan, fUpdateLevel );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigTable.c b/src/sat/aig/aigTable.c
new file mode 100644
index 00000000..cfc94f6b
--- /dev/null
+++ b/src/sat/aig/aigTable.c
@@ -0,0 +1,335 @@
+/**CFile****************************************************************
+
+  FileName    [aigTable.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the hash table 
+struct Aig_Table_t_
+{
+    Aig_Node_t **    pBins;         // the table bins
+    int              nBins;         // the size of the table
+    int              nEntries;      // the total number of entries in the table
+};
+
+// iterators through the entries in the linked lists of nodes
+#define Aig_TableBinForEachEntry( pBin, pEnt )                 \
+    for ( pEnt = pBin;                                         \
+          pEnt;                                                \
+          pEnt = pEnt->NextH? Aig_ManNode(pEnt->pMan, pEnt->NextH) : NULL )
+#define Aig_TableBinForEachEntrySafe( pBin, pEnt, pEnt2 )      \
+    for ( pEnt = pBin,                                         \
+          pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL;            \
+          pEnt;                                                \
+          pEnt = pEnt2,                                        \
+          pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL )
+
+// hash key for the structural hash table
+static inline unsigned Abc_HashKey2( Aig_Node_t * p0, Aig_Node_t * p1, int TableSize ) { return ((unsigned)(p0) + (unsigned)(p1) * 12582917) % TableSize; }
+//static inline unsigned Abc_HashKey2( Aig_Node_t * p0, Aig_Node_t * p1, int TableSize ) { return ((unsigned)((a)->Id + (b)->Id) * ((a)->Id + (b)->Id + 1) / 2) % TableSize; }
+
+static unsigned int Cudd_PrimeAig( unsigned int  p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Table_t * Aig_TableCreate( int nSize )
+{
+    Aig_Table_t * p;
+    // allocate the table
+    p = ALLOC( Aig_Table_t, 1 );
+    memset( p, 0, sizeof(Aig_Table_t) );
+    // allocate and clean the bins
+    p->nBins = Cudd_PrimeAig(nSize);
+    p->pBins = ALLOC( Aig_Node_t *, p->nBins );
+    memset( p->pBins, 0, sizeof(Aig_Node_t *) * p->nBins );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the supergate hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TableFree( Aig_Table_t * p )
+{
+    FREE( p->pBins );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of nodes in the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_TableNumNodes( Aig_Table_t * p )
+{
+    return p->nEntries;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description [The argument nodes can be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 )
+{
+    Aig_Node_t * pAnd;
+    unsigned Key;
+    assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id );
+    assert( p0->pMan == p1->pMan );
+    // get the hash key for these two nodes
+    Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
+    // find the matching node in the table
+    Aig_TableBinForEachEntry( pMan->pTable->pBins[Key], pAnd )
+        if ( p0 == Aig_NodeChild0(pAnd) && p1 == Aig_NodeChild1(pAnd) )
+             return pAnd;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description [The argument nodes can be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1, Aig_Node_t * pAnd )
+{
+    unsigned Key;
+    assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id );
+    // check if it is a good time for table resizing
+    if ( pMan->pTable->nEntries > 2 * pMan->pTable->nBins )
+        Aig_TableResize( pMan );
+    // add the node to the corresponding linked list in the table
+    Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
+    pAnd->NextH = pMan->pTable->pBins[Key]->Id;
+    pMan->pTable->pBins[Key]->NextH = pAnd->Id;
+    pMan->pTable->nEntries++;
+    return pAnd;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes an AIG node from the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis )
+{
+    Aig_Node_t * pAnd, * pPlace = NULL;
+    unsigned Key;
+    assert( !Aig_IsComplement(pThis) );
+    assert( Aig_NodeIsAnd(pThis) );
+    assert( pMan == pThis->pMan );
+    // get the hash key for these two nodes
+    Key = Abc_HashKey2( Aig_NodeChild0(pThis), Aig_NodeChild1(pThis), pMan->pTable->nBins );
+    // find the matching node in the table
+    Aig_TableBinForEachEntry( pMan->pTable->pBins[Key], pAnd )
+    {
+        if ( pThis != pAnd )
+        {
+            pPlace = pAnd;
+            continue;
+        }
+        if ( pPlace == NULL )
+            pMan->pTable->pBins[Key] = Aig_NodeNextH(pThis);
+        else
+            pPlace->NextH = pThis->Id;
+        break;
+    }
+    assert( pThis == pAnd );
+    pMan->pTable->nEntries--;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the hash table of AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TableResize( Aig_Man_t * pMan )
+{
+    Aig_Node_t ** pBinsNew;
+    Aig_Node_t * pEnt, * pEnt2;
+    int nBinsNew, Counter, i, clk;
+    unsigned Key;
+
+clk = clock();
+    // get the new table size
+    nBinsNew = Cudd_PrimeCopy( 3 * pMan->pTable->nBins ); 
+    // allocate a new array
+    pBinsNew = ALLOC( Aig_Node_t *, nBinsNew );
+    memset( pBinsNew, 0, sizeof(Aig_Node_t *) * nBinsNew );
+    // rehash the entries from the old table
+    Counter = 0;
+    for ( i = 0; i < pMan->pTable->nBins; i++ )
+        Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 )
+        {
+            Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), nBinsNew );
+            pEnt->NextH = pBinsNew[Key]->Id;
+            pBinsNew[Key]->NextH = pEnt->Id;
+            Counter++;
+        }
+    assert( Counter == pMan->pTable->nEntries );
+//    printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew );
+//    PRT( "Time", clock() - clk );
+    // replace the table and the parameters
+    free( pMan->pTable->pBins );
+    pMan->pTable->pBins = pBinsNew;
+    pMan->pTable->nBins = nBinsNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the hash table of AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TableRehash( Aig_Man_t * pMan )
+{
+    Aig_Node_t ** pBinsNew;
+    Aig_Node_t * pEnt, * pEnt2;
+    unsigned Key;
+    int Counter, Temp, i;
+    // allocate a new array
+    pBinsNew = ALLOC( Aig_Node_t *, pMan->pTable->nBins );
+    memset( pBinsNew, 0, sizeof(Aig_Node_t *) * pMan->pTable->nBins );
+    // rehash the entries from the old table
+    Counter = 0;
+    for ( i = 0; i < pMan->pTable->nBins; i++ )
+        Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 )
+        {
+            // swap the fanins if needed
+            if ( pEnt->Fans[0].iNode > pEnt->Fans[1].iNode )
+            {
+                Temp = pEnt->Fans[0].iNode;
+                pEnt->Fans[0].iNode = pEnt->Fans[1].iNode;
+                pEnt->Fans[1].iNode = Temp;
+                Temp = pEnt->Fans[0].fComp;
+                pEnt->Fans[0].fComp = pEnt->Fans[1].fComp;
+                pEnt->Fans[1].fComp = Temp;
+           }
+            // rehash the node
+            Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), pMan->pTable->nBins );
+            pEnt->NextH = pBinsNew[Key]->Id;
+            pBinsNew[Key]->NextH = pEnt->Id;
+            Counter++;
+        }
+    assert( Counter == pMan->pTable->nEntries );
+    // replace the table and the parameters
+    free( pMan->pTable->pBins );
+    pMan->pTable->pBins = pBinsNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the smallest prime larger than the number.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned int Cudd_PrimeAig( unsigned int p )
+{
+    int i,pn;
+
+    p--;
+    do {
+        p++;
+        if (p&1) {
+        pn = 1;
+        i = 3;
+        while ((unsigned) (i * i) <= p) {
+        if (p % i == 0) {
+            pn = 0;
+            break;
+        }
+        i += 2;
+        }
+    } else {
+        pn = 0;
+    }
+    } while (!pn);
+    return(p);
+
+} /* end of Cudd_Prime */
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/aigUtil.c b/src/sat/aig/aigUtil.c
new file mode 100644
index 00000000..a1c9ca44
--- /dev/null
+++ b/src/sat/aig/aigUtil.c
@@ -0,0 +1,60 @@
+/**CFile****************************************************************
+
+  FileName    [aigUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Increments the current traversal ID of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManIncrementTravId( Aig_Man_t * pMan )
+{
+    Aig_Node_t * pObj;
+    int i;
+    if ( pMan->nTravIds == (1<<24)-1 )
+    {
+        pMan->nTravIds = 0;
+        Aig_ManForEachNode( pMan, pObj, i )
+            pObj->TravId = 0;
+    }
+    pMan->nTravIds++;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigClass.c b/src/sat/aig/fraigClass.c
new file mode 100644
index 00000000..b3040e2a
--- /dev/null
+++ b/src/sat/aig/fraigClass.c
@@ -0,0 +1,108 @@
+/**CFile****************************************************************
+
+  FileName    [aigFraig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "stmm.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static unsigned Aig_ManHashKey( unsigned * pData, int nWords );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the equivalence classes of patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
+{
+    Vec_Vec_t * vClasses;     // equivalence classes
+    stmm_table * tSim2Node;  // temporary hash table hashing key into the class number
+    Aig_Node_t * pNode;       
+    unsigned uKey;
+    int i, * pSpot, ClassNum;
+    assert( pInfo->Type == 1 );
+    // fill in the hash table
+    tSim2Node = stmm_init_table( stmm_numcmp, stmm_numhash );
+    vClasses = Vec_VecAlloc( 100 );
+    Aig_ManForEachNode( p, pNode, i )
+    {
+        if ( Aig_NodeIsPo(pNode) )
+            continue;
+        uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords );
+        if ( !stmm_find_or_add( tSim2Node, (char *)uKey, (char ***)&pSpot ) ) // does not exist
+            *pSpot = (pNode->Id << 1) | 1; // save the node, and do nothing
+        else if ( (*pSpot) & 1 ) // this is a node
+        {
+            // create the class
+            ClassNum = Vec_VecSize( vClasses );
+            Vec_VecPush( vClasses, ClassNum, (void *)((*pSpot) >> 1) );
+            Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id );
+            // save the class
+            *pSpot = (ClassNum << 1); 
+        }
+        else // this is a class
+        {
+            ClassNum = (*pSpot) >> 1;
+            Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id );
+        }
+    }
+    stmm_free_table( tSim2Node );
+    return vClasses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the hash key of the simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Aig_ManHashKey( unsigned * pData, int nWords )
+{
+    static int Primes[10] = { 1009, 2207, 3779, 4001, 4877, 5381, 6427, 6829, 7213, 7919 };
+    unsigned uKey;
+    int i;
+    uKey = 0;
+    for ( i = 0; i < nWords; i++ )
+        uKey ^= pData[i] * Primes[i%10];
+    return uKey;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c
new file mode 100644
index 00000000..6187538b
--- /dev/null
+++ b/src/sat/aig/fraigCore.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [aigFraig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigProve.c b/src/sat/aig/fraigProve.c
new file mode 100644
index 00000000..b5cce582
--- /dev/null
+++ b/src/sat/aig/fraigProve.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [aigProve.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigSim.c b/src/sat/aig/fraigSim.c
new file mode 100644
index 00000000..1d547621
--- /dev/null
+++ b/src/sat/aig/fraigSim.c
@@ -0,0 +1,238 @@
+/**CFile****************************************************************
+
+  FileName    [aigSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: aigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates all nodes using random simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManSimulateRandomFirst( Aig_Man_t * p )
+{
+    Aig_SimInfo_t * pInfoPi, * pInfoAll;
+    assert( p->pInfo && p->pInfoTemp );
+    // create random PI info
+    pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 );
+    Aig_SimInfoRandom( pInfoPi );
+    // simulate it though the circuit
+    pInfoAll = Aig_ManSimulateInfo( p, pInfoPi );
+    // detect classes
+    p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
+    Aig_SimInfoFree( pInfoAll );
+    // save simulation info
+    p->pInfo = pInfoPi;
+    p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates all nodes using the given simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
+{
+    Aig_SimInfo_t * pInfoAll;
+    Aig_Node_t * pNode;
+    unsigned * pDataPi, * pData0, * pData1, * pDataAnd;
+    int i, k, fComp0, fComp1;
+
+    assert( !pInfoPi->Type ); // PI siminfo
+    // allocate sim info for all nodes
+    pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 );
+    // set the constant sim info
+    pData1 = Aig_SimInfoForNode( pInfoAll, p->pConst1 );
+    for ( k = 0; k < pInfoPi->nWords; k++ )
+        pData1[k] = ~((unsigned)0);
+    // copy the PI siminfo
+    Vec_PtrForEachEntry( p->vPis, pNode, i )
+    {
+        pDataPi  = Aig_SimInfoForPi( pInfoPi, i );
+        pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode );
+        for ( k = 0; k < pInfoPi->nWords; k++ )
+            pDataAnd[k] = pDataPi[k];
+    }
+    // simulate the nodes
+    Vec_PtrForEachEntry( p->vNodes, pNode, i )
+    {
+        if ( !Aig_NodeIsAnd(pNode) )
+            continue;
+        pData0   = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) );
+        pData1   = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin1(pNode) );
+        pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode                 );
+        fComp0 = Aig_NodeFaninC0(pNode);
+        fComp1 = Aig_NodeFaninC1(pNode);
+        if ( fComp0 && fComp1 )
+            for ( k = 0; k < pInfoPi->nWords; k++ )
+                pDataAnd[k] = ~pData0[k] & ~pData1[k];
+        else if ( fComp0  )
+            for ( k = 0; k < pInfoPi->nWords; k++ )
+                pDataAnd[k] = ~pData0[k] &  pData1[k];
+        else if ( fComp1 )
+            for ( k = 0; k < pInfoPi->nWords; k++ )
+                pDataAnd[k] =  pData0[k] & ~pData1[k];
+        else 
+            for ( k = 0; k < pInfoPi->nWords; k++ )
+                pDataAnd[k] =  pData0[k] &  pData1[k];
+    }
+    return pInfoAll;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type )
+{
+    Aig_SimInfo_t * p;
+    p = ALLOC( Aig_SimInfo_t, 1 );
+    memset( p, 0, sizeof(Aig_SimInfo_t) );
+    p->Type     = Type;
+    p->nNodes   = nNodes;
+    p->nWords   = nWords;
+    p->nPatsMax = nWords * sizeof(unsigned) * 8;
+    p->pData    = ALLOC( unsigned, nNodes * nWords );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SimInfoClean( Aig_SimInfo_t * p )
+{
+    int i, Size = p->nNodes * p->nWords;
+    p->nPatsCur = 0;
+    for ( i = 0; i < Size; i++ )
+        p->pData[i] = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SimInfoRandom( Aig_SimInfo_t * p )
+{
+    int i, Size = p->nNodes * p->nWords;
+    unsigned * pData;
+    for ( i = 0; i < Size; i++ )
+        p->pData[i] = ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()));
+    // make sure the first bit of all nodes is 0
+    for ( i = 0; i < p->nNodes; i++ )
+    {
+        pData = p->pData + p->nWords * i;
+        *pData <<= 1;
+    }
+    p->nPatsCur = p->nPatsMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SimInfoResize( Aig_SimInfo_t * p )
+{
+    unsigned * pData;
+    int i, k;
+    assert( p->nPatsCur == p->nPatsMax );
+    pData = ALLOC( unsigned, 2 * p->nNodes * p->nWords );
+    for ( i = 0; i < p->nNodes; i++ )
+    {
+        for ( k = 0; k < p->nWords; k++ )
+            pData[2 * p->nWords * i + k] = p->pData[p->nWords * i + k];
+        for ( k = 0; k < p->nWords; k++ )
+            pData[2 * p->nWords * i + k + p->nWords] = 0;
+    }
+    p->nPatsMax *= 2;
+    p->nWords   *= 2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SimInfoFree( Aig_SimInfo_t * p )
+{
+    free( p->pData );
+    free( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 74503a2b..eb1c5374 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -291,6 +291,8 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
     // check that there is no dangling nodes
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
+        if ( i == 0 ) 
+            continue;
         if ( Abc_ObjFanoutNum(pObj) == 0 )
         {
             printf( "CSAT_Check_Integrity: The network has dangling nodes.\n" );
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index 13f6b50b..a9e09f61 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -233,7 +233,7 @@ clk = clock();
     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
 p->timeSat += clock() - clk;
 
-Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
+//Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
 
     if ( RetValue1 == MSAT_FALSE )
     {