Version abc50910

Makefile

@@ -13,7 +13,7 @@ MODULES := src/base/abc src/base/abci src/base/abcs src/base/cmd src/base/io src
 	   src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim \
            src/sat/asat src/sat/csat src/sat/msat src/sat/fraig
 
-#default: $(PROG)
+default: $(PROG)
 
 OPTFLAGS  := -DNDEBUG -O3
 #OPTFLAGS  := -g -O
@@ -59,10 +59,6 @@ tags:
 $(PROG): $(OBJ)
 	$(LD) -o $@ $^ $(LIBS)
 
-lib$(PROG).a: $(OBJ)
-	ar rv $@ $?
-	ranlib $@
-
 docs:
 	doxygen doxygen.conf
 

abc.dsp

+# Microsoft Developer Studio Project File - Name="abc" - Package Owner=<4>
+# Microsoft Developer Studio Generated Build File, Format Version 6.00
+# ** DO NOT EDIT **
+
+# TARGTYPE "Win32 (x86) Console Application" 0x0103
+
+CFG=abc - Win32 Debug
+!MESSAGE This is not a valid makefile. To build this project using NMAKE,
+!MESSAGE use the Export Makefile command and run
+!MESSAGE 
+!MESSAGE NMAKE /f "abc.mak".
+!MESSAGE 
+!MESSAGE You can specify a configuration when running NMAKE
+!MESSAGE by defining the macro CFG on the command line. For example:
+!MESSAGE 
+!MESSAGE NMAKE /f "abc.mak" CFG="abc - Win32 Debug"
+!MESSAGE 
+!MESSAGE Possible choices for configuration are:
+!MESSAGE 
+!MESSAGE "abc - Win32 Release" (based on "Win32 (x86) Console Application")
+!MESSAGE "abc - Win32 Debug" (based on "Win32 (x86) Console Application")
+!MESSAGE 
+
+# Begin Project
+# PROP AllowPerConfigDependencies 0
+# PROP Scc_ProjName ""
+# PROP Scc_LocalPath ""
+CPP=cl.exe
+RSC=rc.exe
+
+!IF  "$(CFG)" == "abc - Win32 Release"
+
+# PROP BASE Use_MFC 0
+# PROP BASE Use_Debug_Libraries 0
+# PROP BASE Output_Dir "Release"
+# PROP BASE Intermediate_Dir "Release"
+# PROP BASE Target_Dir ""
+# PROP Use_MFC 0
+# PROP Use_Debug_Libraries 0
+# PROP Output_Dir "Release"
+# PROP Intermediate_Dir "Release"
+# PROP Ignore_Export_Lib 0
+# PROP Target_Dir ""
+# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\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\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c
+# ADD BASE RSC /l 0x409 /d "NDEBUG"
+# ADD RSC /l 0x409 /d "NDEBUG"
+BSC32=bscmake.exe
+# ADD BASE BSC32 /nologo
+# ADD BSC32 /nologo
+LINK32=link.exe
+# ADD BASE LINK32 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 /machine:I386
+# ADD LINK32 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 /machine:I386 /out:"_TEST/abc.exe"
+
+!ELSEIF  "$(CFG)" == "abc - Win32 Debug"
+
+# PROP BASE Use_MFC 0
+# PROP BASE Use_Debug_Libraries 1
+# PROP BASE Output_Dir "Debug"
+# PROP BASE Intermediate_Dir "Debug"
+# PROP BASE Target_Dir ""
+# PROP Use_MFC 0
+# PROP Use_Debug_Libraries 1
+# PROP Output_Dir "Debug"
+# PROP Intermediate_Dir "Debug"
+# PROP Ignore_Export_Lib 0
+# PROP Target_Dir ""
+# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\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\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /GZ /c
+# SUBTRACT CPP /X
+# ADD BASE RSC /l 0x409 /d "_DEBUG"
+# ADD RSC /l 0x409 /d "_DEBUG"
+BSC32=bscmake.exe
+# ADD BASE BSC32 /nologo
+# ADD BSC32 /nologo
+LINK32=link.exe
+# ADD BASE LINK32 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 /debug /machine:I386 /pdbtype:sept
+# ADD LINK32 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 /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept
+
+!ENDIF 
+
+# Begin Target
+
+# Name "abc - Win32 Release"
+# Name "abc - Win32 Debug"
+# Begin Group "Source Files"
+
+# PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
+# Begin Group "base"
+
+# PROP Default_Filter ""
+# Begin Group "abc"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\abc\abc.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcAig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcDfs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcFanio.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcFunc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcLatch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcMinBase.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcNames.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcNetlist.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcNtk.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcObj.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcRefs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcShow.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcSop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcUtil.c
+# End Source File
+# End Group
+# Begin Group "abci"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\abci\abc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcAttach.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcBalance.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcCollapse.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcDsd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcFpga.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcFraig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcFxu.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcMap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcMiter.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcNtbdd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcPga.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcReconv.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcRefactor.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcRenode.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcRewrite.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcStrash.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcSweep.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcSymm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcTiming.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcUnreach.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcVerify.c
+# End Source File
+# End Group
+# Begin Group "abcs"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\abcs\abcRetime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abcs\abcSeq.c
+# End Source File
+# End Group
+# Begin Group "cmd"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmd.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdAlias.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdFlag.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdHist.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdUtils.c
+# End Source File
+# End Group
+# Begin Group "io"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\io\io.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\io.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadBench.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadBlif.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadEdif.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadEqn.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadPla.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadVerilog.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteBench.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteBlif.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteCnf.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteDot.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteEqn.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteGml.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWritePla.c
+# End Source File
+# End Group
+# Begin Group "main"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\main\main.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\main.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\mainFrame.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\mainInit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\mainInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\mainUtils.c
+# End Source File
+# End Group
+# End Group
+# Begin Group "bdd"
+
+# PROP Default_Filter ""
+# Begin Group "cudd"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cudd.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddAbs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddApply.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddFind.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddInv.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddIte.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddNeg.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddWalsh.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAndAbs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAnneal.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddApa.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAPI.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddApprox.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddBddAbs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddBddCorr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddBddIte.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddBridge.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddCache.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddClip.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddCof.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddCompose.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddDecomp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddEssent.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddExact.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddExport.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddGenCof.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddGenetic.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddGroup.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddHarwell.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddInit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddInteract.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddLCache.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddLevelQ.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddLinear.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddLiteral.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddMatMult.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddPriority.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddRef.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddReorder.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSign.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSolve.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSplit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSubsetHB.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSubsetSP.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSymmetry.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddWindow.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddCount.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddFuncs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddGroup.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddIsop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddLin.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddMisc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddPort.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddReord.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddSetop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddSymm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddUtil.c
+# End Source File
+# End Group
+# Begin Group "epd"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\epd\epd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\epd\epd.h
+# End Source File
+# End Group
+# Begin Group "mtr"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\mtr\mtr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\mtr\mtrBasic.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\mtr\mtrGroup.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\mtr\mtrInt.h
+# End Source File
+# End Group
+# Begin Group "parse"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parse.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parseCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parseInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parseStack.c
+# End Source File
+# End Group
+# Begin Group "dsd"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsd.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdLocal.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdProc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdTree.c
+# End Source File
+# End Group
+# Begin Group "reo"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reo.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoProfile.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoSift.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoSwap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoTest.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoTransfer.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoUnits.c
+# End Source File
+# End Group
+# End Group
+# Begin Group "sat"
+
+# PROP Default_Filter ""
+# Begin Group "asat"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\asat\added.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\asat\solver.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\asat\solver.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\asat\solver_vec.h
+# End Source File
+# End Group
+# Begin Group "msat"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msat.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatActivity.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatClause.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatClauseVec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatOrderJ.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatQueue.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSolverApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSolverCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSolverIo.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSolverSearch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSort.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatVec.c
+# End Source File
+# End Group
+# Begin Group "fraig"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraig.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigCanon.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigFeed.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigNode.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigPrime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigVec.c
+# End Source File
+# End Group
+# Begin Group "csat"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\csat\csat_apis.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\csat\csat_apis.h
+# End Source File
+# End Group
+# End Group
+# Begin Group "opt"
+
+# PROP Default_Filter ""
+# Begin Group "fxu"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxu.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxu.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuCreate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuHeapD.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuHeapS.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuList.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuMatrix.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuPair.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuReduce.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuSelect.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuSingle.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuUpdate.c
+# End Source File
+# End Group
+# Begin Group "rwr"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrDec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrEva.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrExp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrUtil.c
+# End Source File
+# End Group
+# Begin Group "cut"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cut.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutMerge.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutNode.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutSeq.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutTruth.c
+# End Source File
+# End Group
+# Begin Group "dec"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\dec\dec.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decAbc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decFactor.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decUtil.c
+# End Source File
+# End Group
+# Begin Group "sim"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\sim\sim.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSupp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSwitch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSym.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSymSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSymSim.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSymStr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simUtils.c
+# End Source File
+# End Group
+# End Group
+# Begin Group "map"
+
+# PROP Default_Filter ""
+# Begin Group "fpga"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpga.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpga.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaCreate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaCutUtils.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaMatch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaSwitch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaTime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaTruth.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaUtils.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaVec.c
+# End Source File
+# End Group
+# Begin Group "mapper"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapper.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCanon.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCreate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCutUtils.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperMatch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperRefs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperSuper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperSwitch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperTime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperTree.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperTruth.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperUtils.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperVec.c
+# End Source File
+# End Group
+# Begin Group "mio"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\mio\mio.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mio.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioFunc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioUtils.c
+# End Source File
+# End Group
+# Begin Group "super"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\super\super.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\super.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\superAnd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\superGate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\superInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\superWrite.c
+# End Source File
+# End Group
+# Begin Group "pga"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\pga\pga.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pga\pgaCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pga\pgaInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pga\pgaMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pga\pgaMatch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pga\pgaUtil.c
+# End Source File
+# End Group
+# End Group
+# Begin Group "misc"
+
+# PROP Default_Filter ""
+# Begin Group "extra"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extra.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraBddMisc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraBddSymm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilBitMatrix.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilCanon.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilFile.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilMemory.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilMisc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilProgress.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilReader.c
+# End Source File
+# End Group
+# Begin Group "st"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\st\st.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\st\st.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\st\stmm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\st\stmm.h
+# End Source File
+# End Group
+# Begin Group "util"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\util\cpu_stats.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\cpu_time.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\datalimit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\getopt.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\leaks.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\pathsearch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\safe_mem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\stdlib_hack.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\strsav.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\texpand.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\util.h
+# End Source File
+# End Group
+# Begin Group "mvc"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvc.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcCompare.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcContain.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcCover.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcCube.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcDivide.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcDivisor.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcList.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcLits.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcOpAlg.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcOpBool.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcSort.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcUtils.c
+# End Source File
+# End Group
+# Begin Group "vec"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vec.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecFan.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecPtr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecStr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecVec.h
+# End Source File
+# End Group
+# End Group
+# End Group
+# Begin Group "Header Files"
+
+# PROP Default_Filter "h;hpp;hxx;hm;inl"
+# End Group
+# Begin Group "Resource Files"
+
+# PROP Default_Filter "ico;cur;bmp;dlg;rc2;rct;bin;rgs;gif;jpg;jpeg;jpe"
+# End Group
+# End Target
+# End Project

abc.dsw

+Microsoft Developer Studio Workspace File, Format Version 6.00
+# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE!
+
+###############################################################################
+
+Project: "abc"=.\abc.dsp - Package Owner=<4>
+
+Package=<5>
+{{{
+}}}
+
+Package=<4>
+{{{
+}}}
+
+###############################################################################
+
+Global:
+
+Package=<5>
+{{{
+}}}
+
+Package=<3>
+{{{
+}}}
+
+###############################################################################
+

abc.plg

+<html>
+<body>
+<pre>
+<h1>Build Log</h1>
+<h3>
+--------------------Configuration: abc - Win32 Debug--------------------
+</h3>
+<h3>Command Lines</h3>
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1748.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\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\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\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\map\pga\pgaMan.c"
+]
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1748.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1749.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
+.\Debug\abcCheck.obj
+.\Debug\abcDfs.obj
+.\Debug\abcFanio.obj
+.\Debug\abcFunc.obj
+.\Debug\abcLatch.obj
+.\Debug\abcMinBase.obj
+.\Debug\abcNames.obj
+.\Debug\abcNetlist.obj
+.\Debug\abcNtk.obj
+.\Debug\abcObj.obj
+.\Debug\abcRefs.obj
+.\Debug\abcShow.obj
+.\Debug\abcSop.obj
+.\Debug\abcUtil.obj
+.\Debug\abc.obj
+.\Debug\abcAttach.obj
+.\Debug\abcBalance.obj
+.\Debug\abcCollapse.obj
+.\Debug\abcCut.obj
+.\Debug\abcDsd.obj
+.\Debug\abcFpga.obj
+.\Debug\abcFraig.obj
+.\Debug\abcFxu.obj
+.\Debug\abcMap.obj
+.\Debug\abcMiter.obj
+.\Debug\abcNtbdd.obj
+.\Debug\abcPrint.obj
+.\Debug\abcReconv.obj
+.\Debug\abcRefactor.obj
+.\Debug\abcRenode.obj
+.\Debug\abcRewrite.obj
+.\Debug\abcSat.obj
+.\Debug\abcStrash.obj
+.\Debug\abcSweep.obj
+.\Debug\abcSymm.obj
+.\Debug\abcTiming.obj
+.\Debug\abcUnreach.obj
+.\Debug\abcVerify.obj
+.\Debug\abcRetime.obj
+.\Debug\abcSeq.obj
+.\Debug\cmd.obj
+.\Debug\cmdAlias.obj
+.\Debug\cmdApi.obj
+.\Debug\cmdFlag.obj
+.\Debug\cmdHist.obj
+.\Debug\cmdUtils.obj
+.\Debug\io.obj
+.\Debug\ioRead.obj
+.\Debug\ioReadBench.obj
+.\Debug\ioReadBlif.obj
+.\Debug\ioReadEdif.obj
+.\Debug\ioReadEqn.obj
+.\Debug\ioReadPla.obj
+.\Debug\ioReadVerilog.obj
+.\Debug\ioUtil.obj
+.\Debug\ioWriteBench.obj
+.\Debug\ioWriteBlif.obj
+.\Debug\ioWriteCnf.obj
+.\Debug\ioWriteDot.obj
+.\Debug\ioWriteEqn.obj
+.\Debug\ioWriteGml.obj
+.\Debug\ioWritePla.obj
+.\Debug\main.obj
+.\Debug\mainFrame.obj
+.\Debug\mainInit.obj
+.\Debug\mainUtils.obj
+.\Debug\cuddAddAbs.obj
+.\Debug\cuddAddApply.obj
+.\Debug\cuddAddFind.obj
+.\Debug\cuddAddInv.obj
+.\Debug\cuddAddIte.obj
+.\Debug\cuddAddNeg.obj
+.\Debug\cuddAddWalsh.obj
+.\Debug\cuddAndAbs.obj
+.\Debug\cuddAnneal.obj
+.\Debug\cuddApa.obj
+.\Debug\cuddAPI.obj
+.\Debug\cuddApprox.obj
+.\Debug\cuddBddAbs.obj
+.\Debug\cuddBddCorr.obj
+.\Debug\cuddBddIte.obj
+.\Debug\cuddBridge.obj
+.\Debug\cuddCache.obj
+.\Debug\cuddCheck.obj
+.\Debug\cuddClip.obj
+.\Debug\cuddCof.obj
+.\Debug\cuddCompose.obj
+.\Debug\cuddDecomp.obj
+.\Debug\cuddEssent.obj
+.\Debug\cuddExact.obj
+.\Debug\cuddExport.obj
+.\Debug\cuddGenCof.obj
+.\Debug\cuddGenetic.obj
+.\Debug\cuddGroup.obj
+.\Debug\cuddHarwell.obj
+.\Debug\cuddInit.obj
+.\Debug\cuddInteract.obj
+.\Debug\cuddLCache.obj
+.\Debug\cuddLevelQ.obj
+.\Debug\cuddLinear.obj
+.\Debug\cuddLiteral.obj
+.\Debug\cuddMatMult.obj
+.\Debug\cuddPriority.obj
+.\Debug\cuddRead.obj
+.\Debug\cuddRef.obj
+.\Debug\cuddReorder.obj
+.\Debug\cuddSat.obj
+.\Debug\cuddSign.obj
+.\Debug\cuddSolve.obj
+.\Debug\cuddSplit.obj
+.\Debug\cuddSubsetHB.obj
+.\Debug\cuddSubsetSP.obj
+.\Debug\cuddSymmetry.obj
+.\Debug\cuddTable.obj
+.\Debug\cuddUtil.obj
+.\Debug\cuddWindow.obj
+.\Debug\cuddZddCount.obj
+.\Debug\cuddZddFuncs.obj
+.\Debug\cuddZddGroup.obj
+.\Debug\cuddZddIsop.obj
+.\Debug\cuddZddLin.obj
+.\Debug\cuddZddMisc.obj
+.\Debug\cuddZddPort.obj
+.\Debug\cuddZddReord.obj
+.\Debug\cuddZddSetop.obj
+.\Debug\cuddZddSymm.obj
+.\Debug\cuddZddUtil.obj
+.\Debug\epd.obj
+.\Debug\mtrBasic.obj
+.\Debug\mtrGroup.obj
+.\Debug\parseCore.obj
+.\Debug\parseStack.obj
+.\Debug\dsdApi.obj
+.\Debug\dsdCheck.obj
+.\Debug\dsdLocal.obj
+.\Debug\dsdMan.obj
+.\Debug\dsdProc.obj
+.\Debug\dsdTree.obj
+.\Debug\reoApi.obj
+.\Debug\reoCore.obj
+.\Debug\reoProfile.obj
+.\Debug\reoSift.obj
+.\Debug\reoSwap.obj
+.\Debug\reoTest.obj
+.\Debug\reoTransfer.obj
+.\Debug\reoUnits.obj
+.\Debug\added.obj
+.\Debug\solver.obj
+.\Debug\msatActivity.obj
+.\Debug\msatClause.obj
+.\Debug\msatClauseVec.obj
+.\Debug\msatMem.obj
+.\Debug\msatOrderJ.obj
+.\Debug\msatQueue.obj
+.\Debug\msatRead.obj
+.\Debug\msatSolverApi.obj
+.\Debug\msatSolverCore.obj
+.\Debug\msatSolverIo.obj
+.\Debug\msatSolverSearch.obj
+.\Debug\msatSort.obj
+.\Debug\msatVec.obj
+.\Debug\fraigApi.obj
+.\Debug\fraigCanon.obj
+.\Debug\fraigFanout.obj
+.\Debug\fraigFeed.obj
+.\Debug\fraigMan.obj
+.\Debug\fraigMem.obj
+.\Debug\fraigNode.obj
+.\Debug\fraigPrime.obj
+.\Debug\fraigSat.obj
+.\Debug\fraigTable.obj
+.\Debug\fraigUtil.obj
+.\Debug\fraigVec.obj
+.\Debug\csat_apis.obj
+.\Debug\fxu.obj
+.\Debug\fxuCreate.obj
+.\Debug\fxuHeapD.obj
+.\Debug\fxuHeapS.obj
+.\Debug\fxuList.obj
+.\Debug\fxuMatrix.obj
+.\Debug\fxuPair.obj
+.\Debug\fxuPrint.obj
+.\Debug\fxuReduce.obj
+.\Debug\fxuSelect.obj
+.\Debug\fxuSingle.obj
+.\Debug\fxuUpdate.obj
+.\Debug\rwrDec.obj
+.\Debug\rwrEva.obj
+.\Debug\rwrExp.obj
+.\Debug\rwrLib.obj
+.\Debug\rwrMan.obj
+.\Debug\rwrPrint.obj
+.\Debug\rwrUtil.obj
+.\Debug\cutApi.obj
+.\Debug\cutCut.obj
+.\Debug\cutMan.obj
+.\Debug\cutMerge.obj
+.\Debug\cutNode.obj
+.\Debug\cutSeq.obj
+.\Debug\cutTruth.obj
+.\Debug\decAbc.obj
+.\Debug\decFactor.obj
+.\Debug\decMan.obj
+.\Debug\decPrint.obj
+.\Debug\decUtil.obj
+.\Debug\simMan.obj
+.\Debug\simSat.obj
+.\Debug\simSupp.obj
+.\Debug\simSwitch.obj
+.\Debug\simSym.obj
+.\Debug\simSymSat.obj
+.\Debug\simSymSim.obj
+.\Debug\simSymStr.obj
+.\Debug\simUtils.obj
+.\Debug\fpga.obj
+.\Debug\fpgaCore.obj
+.\Debug\fpgaCreate.obj
+.\Debug\fpgaCut.obj
+.\Debug\fpgaCutUtils.obj
+.\Debug\fpgaFanout.obj
+.\Debug\fpgaLib.obj
+.\Debug\fpgaMatch.obj
+.\Debug\fpgaSwitch.obj
+.\Debug\fpgaTime.obj
+.\Debug\fpgaTruth.obj
+.\Debug\fpgaUtils.obj
+.\Debug\fpgaVec.obj
+.\Debug\mapper.obj
+.\Debug\mapperCanon.obj
+.\Debug\mapperCore.obj
+.\Debug\mapperCreate.obj
+.\Debug\mapperCut.obj
+.\Debug\mapperCutUtils.obj
+.\Debug\mapperFanout.obj
+.\Debug\mapperLib.obj
+.\Debug\mapperMatch.obj
+.\Debug\mapperRefs.obj
+.\Debug\mapperSuper.obj
+.\Debug\mapperSwitch.obj
+.\Debug\mapperTable.obj
+.\Debug\mapperTime.obj
+.\Debug\mapperTree.obj
+.\Debug\mapperTruth.obj
+.\Debug\mapperUtils.obj
+.\Debug\mapperVec.obj
+.\Debug\mio.obj
+.\Debug\mioApi.obj
+.\Debug\mioFunc.obj
+.\Debug\mioRead.obj
+.\Debug\mioUtils.obj
+.\Debug\super.obj
+.\Debug\superAnd.obj
+.\Debug\superGate.obj
+.\Debug\superWrite.obj
+.\Debug\extraBddMisc.obj
+.\Debug\extraBddSymm.obj
+.\Debug\extraUtilBitMatrix.obj
+.\Debug\extraUtilCanon.obj
+.\Debug\extraUtilFile.obj
+.\Debug\extraUtilMemory.obj
+.\Debug\extraUtilMisc.obj
+.\Debug\extraUtilProgress.obj
+.\Debug\extraUtilReader.obj
+.\Debug\st.obj
+.\Debug\stmm.obj
+.\Debug\cpu_stats.obj
+.\Debug\cpu_time.obj
+.\Debug\datalimit.obj
+.\Debug\getopt.obj
+.\Debug\pathsearch.obj
+.\Debug\safe_mem.obj
+.\Debug\strsav.obj
+.\Debug\texpand.obj
+.\Debug\mvc.obj
+.\Debug\mvcApi.obj
+.\Debug\mvcCompare.obj
+.\Debug\mvcContain.obj
+.\Debug\mvcCover.obj
+.\Debug\mvcCube.obj
+.\Debug\mvcDivide.obj
+.\Debug\mvcDivisor.obj
+.\Debug\mvcList.obj
+.\Debug\mvcLits.obj
+.\Debug\mvcMan.obj
+.\Debug\mvcOpAlg.obj
+.\Debug\mvcOpBool.obj
+.\Debug\mvcPrint.obj
+.\Debug\mvcSort.obj
+.\Debug\mvcUtils.obj
+.\Debug\pgaMan.obj
+.\Debug\pgaUtil.obj
+.\Debug\pgaMatch.obj
+.\Debug\pgaCore.obj
+.\Debug\abcPga.obj
+]
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1749.tmp"
+<h3>Output Window</h3>
+Compiling...
+pgaMan.c
+Linking...
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP174A.tmp" with contents
+[
+/nologo /o"Debug/abc.bsc" 
+.\Debug\abcAig.sbr
+.\Debug\abcCheck.sbr
+.\Debug\abcDfs.sbr
+.\Debug\abcFanio.sbr
+.\Debug\abcFunc.sbr
+.\Debug\abcLatch.sbr
+.\Debug\abcMinBase.sbr
+.\Debug\abcNames.sbr
+.\Debug\abcNetlist.sbr
+.\Debug\abcNtk.sbr
+.\Debug\abcObj.sbr
+.\Debug\abcRefs.sbr
+.\Debug\abcShow.sbr
+.\Debug\abcSop.sbr
+.\Debug\abcUtil.sbr
+.\Debug\abc.sbr
+.\Debug\abcAttach.sbr
+.\Debug\abcBalance.sbr
+.\Debug\abcCollapse.sbr
+.\Debug\abcCut.sbr
+.\Debug\abcDsd.sbr
+.\Debug\abcFpga.sbr
+.\Debug\abcFraig.sbr
+.\Debug\abcFxu.sbr
+.\Debug\abcMap.sbr
+.\Debug\abcMiter.sbr
+.\Debug\abcNtbdd.sbr
+.\Debug\abcPrint.sbr
+.\Debug\abcReconv.sbr
+.\Debug\abcRefactor.sbr
+.\Debug\abcRenode.sbr
+.\Debug\abcRewrite.sbr
+.\Debug\abcSat.sbr
+.\Debug\abcStrash.sbr
+.\Debug\abcSweep.sbr
+.\Debug\abcSymm.sbr
+.\Debug\abcTiming.sbr
+.\Debug\abcUnreach.sbr
+.\Debug\abcVerify.sbr
+.\Debug\abcRetime.sbr
+.\Debug\abcSeq.sbr
+.\Debug\cmd.sbr
+.\Debug\cmdAlias.sbr
+.\Debug\cmdApi.sbr
+.\Debug\cmdFlag.sbr
+.\Debug\cmdHist.sbr
+.\Debug\cmdUtils.sbr
+.\Debug\io.sbr
+.\Debug\ioRead.sbr
+.\Debug\ioReadBench.sbr
+.\Debug\ioReadBlif.sbr
+.\Debug\ioReadEdif.sbr
+.\Debug\ioReadEqn.sbr
+.\Debug\ioReadPla.sbr
+.\Debug\ioReadVerilog.sbr
+.\Debug\ioUtil.sbr
+.\Debug\ioWriteBench.sbr
+.\Debug\ioWriteBlif.sbr
+.\Debug\ioWriteCnf.sbr
+.\Debug\ioWriteDot.sbr
+.\Debug\ioWriteEqn.sbr
+.\Debug\ioWriteGml.sbr
+.\Debug\ioWritePla.sbr
+.\Debug\main.sbr
+.\Debug\mainFrame.sbr
+.\Debug\mainInit.sbr
+.\Debug\mainUtils.sbr
+.\Debug\cuddAddAbs.sbr
+.\Debug\cuddAddApply.sbr
+.\Debug\cuddAddFind.sbr
+.\Debug\cuddAddInv.sbr
+.\Debug\cuddAddIte.sbr
+.\Debug\cuddAddNeg.sbr
+.\Debug\cuddAddWalsh.sbr
+.\Debug\cuddAndAbs.sbr
+.\Debug\cuddAnneal.sbr
+.\Debug\cuddApa.sbr
+.\Debug\cuddAPI.sbr
+.\Debug\cuddApprox.sbr
+.\Debug\cuddBddAbs.sbr
+.\Debug\cuddBddCorr.sbr
+.\Debug\cuddBddIte.sbr
+.\Debug\cuddBridge.sbr
+.\Debug\cuddCache.sbr
+.\Debug\cuddCheck.sbr
+.\Debug\cuddClip.sbr
+.\Debug\cuddCof.sbr
+.\Debug\cuddCompose.sbr
+.\Debug\cuddDecomp.sbr
+.\Debug\cuddEssent.sbr
+.\Debug\cuddExact.sbr
+.\Debug\cuddExport.sbr
+.\Debug\cuddGenCof.sbr
+.\Debug\cuddGenetic.sbr
+.\Debug\cuddGroup.sbr
+.\Debug\cuddHarwell.sbr
+.\Debug\cuddInit.sbr
+.\Debug\cuddInteract.sbr
+.\Debug\cuddLCache.sbr
+.\Debug\cuddLevelQ.sbr
+.\Debug\cuddLinear.sbr
+.\Debug\cuddLiteral.sbr
+.\Debug\cuddMatMult.sbr
+.\Debug\cuddPriority.sbr
+.\Debug\cuddRead.sbr
+.\Debug\cuddRef.sbr
+.\Debug\cuddReorder.sbr
+.\Debug\cuddSat.sbr
+.\Debug\cuddSign.sbr
+.\Debug\cuddSolve.sbr
+.\Debug\cuddSplit.sbr
+.\Debug\cuddSubsetHB.sbr
+.\Debug\cuddSubsetSP.sbr
+.\Debug\cuddSymmetry.sbr
+.\Debug\cuddTable.sbr
+.\Debug\cuddUtil.sbr
+.\Debug\cuddWindow.sbr
+.\Debug\cuddZddCount.sbr
+.\Debug\cuddZddFuncs.sbr
+.\Debug\cuddZddGroup.sbr
+.\Debug\cuddZddIsop.sbr
+.\Debug\cuddZddLin.sbr
+.\Debug\cuddZddMisc.sbr
+.\Debug\cuddZddPort.sbr
+.\Debug\cuddZddReord.sbr
+.\Debug\cuddZddSetop.sbr
+.\Debug\cuddZddSymm.sbr
+.\Debug\cuddZddUtil.sbr
+.\Debug\epd.sbr
+.\Debug\mtrBasic.sbr
+.\Debug\mtrGroup.sbr
+.\Debug\parseCore.sbr
+.\Debug\parseStack.sbr
+.\Debug\dsdApi.sbr
+.\Debug\dsdCheck.sbr
+.\Debug\dsdLocal.sbr
+.\Debug\dsdMan.sbr
+.\Debug\dsdProc.sbr
+.\Debug\dsdTree.sbr
+.\Debug\reoApi.sbr
+.\Debug\reoCore.sbr
+.\Debug\reoProfile.sbr
+.\Debug\reoSift.sbr
+.\Debug\reoSwap.sbr
+.\Debug\reoTest.sbr
+.\Debug\reoTransfer.sbr
+.\Debug\reoUnits.sbr
+.\Debug\added.sbr
+.\Debug\solver.sbr
+.\Debug\msatActivity.sbr
+.\Debug\msatClause.sbr
+.\Debug\msatClauseVec.sbr
+.\Debug\msatMem.sbr
+.\Debug\msatOrderJ.sbr
+.\Debug\msatQueue.sbr
+.\Debug\msatRead.sbr
+.\Debug\msatSolverApi.sbr
+.\Debug\msatSolverCore.sbr
+.\Debug\msatSolverIo.sbr
+.\Debug\msatSolverSearch.sbr
+.\Debug\msatSort.sbr
+.\Debug\msatVec.sbr
+.\Debug\fraigApi.sbr
+.\Debug\fraigCanon.sbr
+.\Debug\fraigFanout.sbr
+.\Debug\fraigFeed.sbr
+.\Debug\fraigMan.sbr
+.\Debug\fraigMem.sbr
+.\Debug\fraigNode.sbr
+.\Debug\fraigPrime.sbr
+.\Debug\fraigSat.sbr
+.\Debug\fraigTable.sbr
+.\Debug\fraigUtil.sbr
+.\Debug\fraigVec.sbr
+.\Debug\csat_apis.sbr
+.\Debug\fxu.sbr
+.\Debug\fxuCreate.sbr
+.\Debug\fxuHeapD.sbr
+.\Debug\fxuHeapS.sbr
+.\Debug\fxuList.sbr
+.\Debug\fxuMatrix.sbr
+.\Debug\fxuPair.sbr
+.\Debug\fxuPrint.sbr
+.\Debug\fxuReduce.sbr
+.\Debug\fxuSelect.sbr
+.\Debug\fxuSingle.sbr
+.\Debug\fxuUpdate.sbr
+.\Debug\rwrDec.sbr
+.\Debug\rwrEva.sbr
+.\Debug\rwrExp.sbr
+.\Debug\rwrLib.sbr
+.\Debug\rwrMan.sbr
+.\Debug\rwrPrint.sbr
+.\Debug\rwrUtil.sbr
+.\Debug\cutApi.sbr
+.\Debug\cutCut.sbr
+.\Debug\cutMan.sbr
+.\Debug\cutMerge.sbr
+.\Debug\cutNode.sbr
+.\Debug\cutSeq.sbr
+.\Debug\cutTruth.sbr
+.\Debug\decAbc.sbr
+.\Debug\decFactor.sbr
+.\Debug\decMan.sbr
+.\Debug\decPrint.sbr
+.\Debug\decUtil.sbr
+.\Debug\simMan.sbr
+.\Debug\simSat.sbr
+.\Debug\simSupp.sbr
+.\Debug\simSwitch.sbr
+.\Debug\simSym.sbr
+.\Debug\simSymSat.sbr
+.\Debug\simSymSim.sbr
+.\Debug\simSymStr.sbr
+.\Debug\simUtils.sbr
+.\Debug\fpga.sbr
+.\Debug\fpgaCore.sbr
+.\Debug\fpgaCreate.sbr
+.\Debug\fpgaCut.sbr
+.\Debug\fpgaCutUtils.sbr
+.\Debug\fpgaFanout.sbr
+.\Debug\fpgaLib.sbr
+.\Debug\fpgaMatch.sbr
+.\Debug\fpgaSwitch.sbr
+.\Debug\fpgaTime.sbr
+.\Debug\fpgaTruth.sbr
+.\Debug\fpgaUtils.sbr
+.\Debug\fpgaVec.sbr
+.\Debug\mapper.sbr
+.\Debug\mapperCanon.sbr
+.\Debug\mapperCore.sbr
+.\Debug\mapperCreate.sbr
+.\Debug\mapperCut.sbr
+.\Debug\mapperCutUtils.sbr
+.\Debug\mapperFanout.sbr
+.\Debug\mapperLib.sbr
+.\Debug\mapperMatch.sbr
+.\Debug\mapperRefs.sbr
+.\Debug\mapperSuper.sbr
+.\Debug\mapperSwitch.sbr
+.\Debug\mapperTable.sbr
+.\Debug\mapperTime.sbr
+.\Debug\mapperTree.sbr
+.\Debug\mapperTruth.sbr
+.\Debug\mapperUtils.sbr
+.\Debug\mapperVec.sbr
+.\Debug\mio.sbr
+.\Debug\mioApi.sbr
+.\Debug\mioFunc.sbr
+.\Debug\mioRead.sbr
+.\Debug\mioUtils.sbr
+.\Debug\super.sbr
+.\Debug\superAnd.sbr
+.\Debug\superGate.sbr
+.\Debug\superWrite.sbr
+.\Debug\extraBddMisc.sbr
+.\Debug\extraBddSymm.sbr
+.\Debug\extraUtilBitMatrix.sbr
+.\Debug\extraUtilCanon.sbr
+.\Debug\extraUtilFile.sbr
+.\Debug\extraUtilMemory.sbr
+.\Debug\extraUtilMisc.sbr
+.\Debug\extraUtilProgress.sbr
+.\Debug\extraUtilReader.sbr
+.\Debug\st.sbr
+.\Debug\stmm.sbr
+.\Debug\cpu_stats.sbr
+.\Debug\cpu_time.sbr
+.\Debug\datalimit.sbr
+.\Debug\getopt.sbr
+.\Debug\pathsearch.sbr
+.\Debug\safe_mem.sbr
+.\Debug\strsav.sbr
+.\Debug\texpand.sbr
+.\Debug\mvc.sbr
+.\Debug\mvcApi.sbr
+.\Debug\mvcCompare.sbr
+.\Debug\mvcContain.sbr
+.\Debug\mvcCover.sbr
+.\Debug\mvcCube.sbr
+.\Debug\mvcDivide.sbr
+.\Debug\mvcDivisor.sbr
+.\Debug\mvcList.sbr
+.\Debug\mvcLits.sbr
+.\Debug\mvcMan.sbr
+.\Debug\mvcOpAlg.sbr
+.\Debug\mvcOpBool.sbr
+.\Debug\mvcPrint.sbr
+.\Debug\mvcSort.sbr
+.\Debug\mvcUtils.sbr
+.\Debug\pgaMan.sbr
+.\Debug\pgaUtil.sbr
+.\Debug\pgaMatch.sbr
+.\Debug\pgaCore.sbr
+.\Debug\abcPga.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP174A.tmp"
+Creating browse info file...
+<h3>Output Window</h3>
+
+
+
+<h3>Results</h3>
+abc.exe - 0 error(s), 0 warning(s)
+</pre>
+</body>
+</html>

abclib.dsp

+# Microsoft Developer Studio Project File - Name="abclib" - Package Owner=<4>
+# Microsoft Developer Studio Generated Build File, Format Version 6.00
+# ** DO NOT EDIT **
+
+# TARGTYPE "Win32 (x86) Static Library" 0x0104
+
+CFG=abclib - Win32 Debug
+!MESSAGE This is not a valid makefile. To build this project using NMAKE,
+!MESSAGE use the Export Makefile command and run
+!MESSAGE 
+!MESSAGE NMAKE /f "abclib.mak".
+!MESSAGE 
+!MESSAGE You can specify a configuration when running NMAKE
+!MESSAGE by defining the macro CFG on the command line. For example:
+!MESSAGE 
+!MESSAGE NMAKE /f "abclib.mak" CFG="abclib - Win32 Debug"
+!MESSAGE 
+!MESSAGE Possible choices for configuration are:
+!MESSAGE 
+!MESSAGE "abclib - Win32 Release" (based on "Win32 (x86) Static Library")
+!MESSAGE "abclib - Win32 Debug" (based on "Win32 (x86) Static Library")
+!MESSAGE 
+
+# Begin Project
+# PROP AllowPerConfigDependencies 0
+# PROP Scc_ProjName ""
+# PROP Scc_LocalPath ""
+CPP=cl.exe
+RSC=rc.exe
+
+!IF  "$(CFG)" == "abclib - Win32 Release"
+
+# PROP BASE Use_MFC 0
+# PROP BASE Use_Debug_Libraries 0
+# PROP BASE Output_Dir "abclib___Win32_Release"
+# PROP BASE Intermediate_Dir "abclib___Win32_Release"
+# PROP BASE Target_Dir ""
+# PROP Use_MFC 0
+# PROP Use_Debug_Libraries 0
+# PROP Output_Dir "abclib\ReleaseLib"
+# PROP Intermediate_Dir "abclib\ReleaseLib"
+# PROP Target_Dir ""
+# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\rwr" /I "src\map\fpga" /I "src\map\mapper" /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\vec" /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c
+# ADD BASE RSC /l 0x409 /d "NDEBUG"
+# ADD RSC /l 0x409 /d "NDEBUG"
+BSC32=bscmake.exe
+# ADD BASE BSC32 /nologo
+# ADD BSC32 /nologo
+LIB32=link.exe -lib
+# ADD BASE LIB32 /nologo
+# ADD LIB32 /nologo /out:"abclib\abclib_release.lib"
+
+!ELSEIF  "$(CFG)" == "abclib - Win32 Debug"
+
+# PROP BASE Use_MFC 0
+# PROP BASE Use_Debug_Libraries 1
+# PROP BASE Output_Dir "abclib___Win32_Debug"
+# PROP BASE Intermediate_Dir "abclib___Win32_Debug"
+# PROP BASE Target_Dir ""
+# PROP Use_MFC 0
+# PROP Use_Debug_Libraries 1
+# PROP Output_Dir "abclib\DebugLib"
+# PROP Intermediate_Dir "abclib\DebugLib"
+# PROP Target_Dir ""
+# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\rwr" /I "src\map\fpga" /I "src\map\mapper" /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\vec" /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /GZ /c
+# ADD BASE RSC /l 0x409 /d "_DEBUG"
+# ADD RSC /l 0x409 /d "_DEBUG"
+BSC32=bscmake.exe
+# ADD BASE BSC32 /nologo
+# ADD BSC32 /nologo
+LIB32=link.exe -lib
+# ADD BASE LIB32 /nologo
+# ADD LIB32 /nologo /out:"abclib\abclib_debug.lib"
+
+!ENDIF 
+
+# Begin Target
+
+# Name "abclib - Win32 Release"
+# Name "abclib - Win32 Debug"
+# Begin Group "Source Files"
+
+# PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
+# Begin Group "base"
+
+# PROP Default_Filter ""
+# Begin Group "abc"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\abc\abc.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcAig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcDfs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcFanio.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcFunc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcLatch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcMinBase.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcNames.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcNetlist.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcNtk.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcObj.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcRefs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcShow.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcSop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcUtil.c
+# End Source File
+# End Group
+# Begin Group "abci"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\abci\abc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcAttach.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcBalance.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcCollapse.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcDsd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcFpga.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcFraig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcFxu.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcMap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcMiter.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcNtbdd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcReconv.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcRefactor.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcRenode.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcRewrite.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcStrash.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcSweep.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcSymm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcTiming.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcUnreach.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcVerify.c
+# End Source File
+# End Group
+# Begin Group "abcs"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\abcs\abcRetime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abcs\abcSeq.c
+# End Source File
+# End Group
+# Begin Group "cmd"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmd.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdAlias.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdFlag.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdHist.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdUtils.c
+# End Source File
+# End Group
+# Begin Group "io"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\io\io.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\io.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadBench.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadBlif.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadEdif.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadEqn.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadPla.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadVerilog.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteBench.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteBlif.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteCnf.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteDot.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteEqn.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteGml.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWritePla.c
+# End Source File
+# End Group
+# Begin Group "main"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\main\main.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\main.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\mainFrame.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\mainInit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\mainInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\mainUtils.c
+# End Source File
+# End Group
+# End Group
+# Begin Group "bdd"
+
+# PROP Default_Filter ""
+# Begin Group "cudd"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cudd.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddAbs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddApply.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddFind.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddInv.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddIte.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddNeg.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddWalsh.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAndAbs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAnneal.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddApa.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAPI.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddApprox.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddBddAbs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddBddCorr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddBddIte.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddBridge.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddCache.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddClip.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddCof.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddCompose.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddDecomp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddEssent.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddExact.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddExport.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddGenCof.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddGenetic.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddGroup.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddHarwell.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddInit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddInteract.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddLCache.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddLevelQ.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddLinear.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddLiteral.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddMatMult.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddPriority.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddRef.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddReorder.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSign.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSolve.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSplit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSubsetHB.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSubsetSP.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSymmetry.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddWindow.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddCount.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddFuncs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddGroup.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddIsop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddLin.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddMisc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddPort.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddReord.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddSetop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddSymm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddUtil.c
+# End Source File
+# End Group
+# Begin Group "epd"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\epd\epd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\epd\epd.h
+# End Source File
+# End Group
+# Begin Group "mtr"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\mtr\mtr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\mtr\mtrBasic.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\mtr\mtrGroup.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\mtr\mtrInt.h
+# End Source File
+# End Group
+# Begin Group "parse"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parse.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parseCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parseInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parseStack.c
+# End Source File
+# End Group
+# Begin Group "dsd"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsd.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdLocal.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdProc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdTree.c
+# End Source File
+# End Group
+# Begin Group "reo"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reo.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoProfile.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoSift.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoSwap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoTest.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoTransfer.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoUnits.c
+# End Source File
+# End Group
+# End Group
+# Begin Group "sat"
+
+# PROP Default_Filter ""
+# Begin Group "asat"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\asat\added.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\asat\solver.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\asat\solver.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\asat\solver_vec.h
+# End Source File
+# End Group
+# Begin Group "msat"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msat.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatActivity.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatClause.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatClauseVec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatOrderJ.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatQueue.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSolverApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSolverCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSolverIo.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSolverSearch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSort.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatVec.c
+# End Source File
+# End Group
+# Begin Group "fraig"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraig.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigCanon.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigFeed.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigNode.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigPrime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigVec.c
+# End Source File
+# End Group
+# Begin Group "csat"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\csat\csat_apis.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\csat\csat_apis.h
+# End Source File
+# End Group
+# End Group
+# Begin Group "opt"
+
+# PROP Default_Filter ""
+# Begin Group "fxu"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxu.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxu.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuCreate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuHeapD.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuHeapS.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuList.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuMatrix.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuPair.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuReduce.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuSelect.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuSingle.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuUpdate.c
+# End Source File
+# End Group
+# Begin Group "rwr"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrDec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrEva.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrExp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrUtil.c
+# End Source File
+# End Group
+# Begin Group "cut"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cut.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutList.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutMerge.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutNode.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutSeq.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutTruth.c
+# End Source File
+# End Group
+# Begin Group "dec"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\dec\dec.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decAbc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decFactor.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decUtil.c
+# End Source File
+# End Group
+# Begin Group "sim"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\sim\sim.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSupp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSwitch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSym.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSymSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSymSim.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSymStr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simUtils.c
+# End Source File
+# End Group
+# End Group
+# Begin Group "map"
+
+# PROP Default_Filter ""
+# Begin Group "fpga"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpga.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpga.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaCreate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaCutUtils.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaMatch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaSwitch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaTime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaTruth.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaUtils.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaVec.c
+# End Source File
+# End Group
+# Begin Group "mapper"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapper.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCanon.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCreate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCutUtils.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperMatch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperRefs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperSuper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperSwitch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperTime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperTree.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperTruth.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperUtils.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperVec.c
+# End Source File
+# End Group
+# Begin Group "mio"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\mio\mio.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mio.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioFunc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioUtils.c
+# End Source File
+# End Group
+# Begin Group "super"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\super\super.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\super.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\superAnd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\superGate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\superInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\superWrite.c
+# End Source File
+# End Group
+# End Group
+# Begin Group "misc"
+
+# PROP Default_Filter ""
+# Begin Group "extra"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extra.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraBddMisc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraBddSymm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilBitMatrix.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilCanon.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilFile.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilMemory.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilMisc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilProgress.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilReader.c
+# End Source File
+# End Group
+# Begin Group "st"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\st\st.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\st\st.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\st\stmm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\st\stmm.h
+# End Source File
+# End Group
+# Begin Group "util"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\util\cpu_stats.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\cpu_time.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\datalimit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\getopt.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\leaks.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\pathsearch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\safe_mem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\stdlib_hack.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\strsav.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\texpand.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\util.h
+# End Source File
+# End Group
+# Begin Group "mvc"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvc.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcCompare.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcContain.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcCover.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcCube.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcDivide.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcDivisor.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcList.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcLits.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcOpAlg.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcOpBool.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcSort.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcUtils.c
+# End Source File
+# End Group
+# Begin Group "vec"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vec.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecFan.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecPtr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecStr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecVec.h
+# End Source File
+# End Group
+# End Group
+# End Group
+# Begin Group "Header Files"
+
+# PROP Default_Filter "h;hpp;hxx;hm;inl"
+# End Group
+# End Target
+# End Project

abclib.dsw

+Microsoft Developer Studio Workspace File, Format Version 6.00
+# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE!
+
+###############################################################################
+
+Project: "abclib"=.\abclib.dsp - Package Owner=<4>
+
+Package=<5>
+{{{
+}}}
+
+Package=<4>
+{{{
+}}}
+
+###############################################################################
+
+Global:
+
+Package=<5>
+{{{
+}}}
+
+Package=<3>
+{{{
+}}}
+
+###############################################################################
+

abclib.plg

+<html>
+<body>
+<pre>
+<h1>Build Log</h1>
+<h3>
+--------------------Configuration: abclib - Win32 Release--------------------
+</h3>
+<h3>Command Lines</h3>
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1014.tmp" with contents
+[
+/nologo /ML /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\rwr" /I "src\map\fpga" /I "src\map\mapper" /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\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\abci\abcRenode.c"
+"C:\_projects\abc\src\base\abci\abcSat.c"
+"C:\_projects\abc\src\base\main\main.c"
+"C:\_projects\abc\src\sat\csat\csat_apis.c"
+]
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1014.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1015.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\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\abcVerify.obj
+.\abclib\ReleaseLib\abcRetime.obj
+.\abclib\ReleaseLib\abcSeq.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\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\ioWriteBench.obj
+.\abclib\ReleaseLib\ioWriteBlif.obj
+.\abclib\ReleaseLib\ioWriteCnf.obj
+.\abclib\ReleaseLib\ioWriteDot.obj
+.\abclib\ReleaseLib\ioWriteEqn.obj
+.\abclib\ReleaseLib\ioWriteGml.obj
+.\abclib\ReleaseLib\ioWritePla.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\cutMan.obj
+.\abclib\ReleaseLib\cutMerge.obj
+.\abclib\ReleaseLib\cutNode.obj
+.\abclib\ReleaseLib\cutSeq.obj
+.\abclib\ReleaseLib\cutTable.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\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\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
+]
+Creating command line "link.exe -lib @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1015.tmp"
+<h3>Output Window</h3>
+Compiling...
+abcRenode.c
+abcSat.c
+main.c
+csat_apis.c
+Creating library...
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1016.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\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\abcVerify.sbr
+.\abclib\ReleaseLib\abcRetime.sbr
+.\abclib\ReleaseLib\abcSeq.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\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\ioWriteBench.sbr
+.\abclib\ReleaseLib\ioWriteBlif.sbr
+.\abclib\ReleaseLib\ioWriteCnf.sbr
+.\abclib\ReleaseLib\ioWriteDot.sbr
+.\abclib\ReleaseLib\ioWriteEqn.sbr
+.\abclib\ReleaseLib\ioWriteGml.sbr
+.\abclib\ReleaseLib\ioWritePla.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\cutMan.sbr
+.\abclib\ReleaseLib\cutMerge.sbr
+.\abclib\ReleaseLib\cutNode.sbr
+.\abclib\ReleaseLib\cutSeq.sbr
+.\abclib\ReleaseLib\cutTable.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\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\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\RSP1016.tmp"
+Creating browse info file...
+<h3>Output Window</h3>
+
+
+
+<h3>Results</h3>
+abclib_release.lib - 0 error(s), 0 warning(s)
+</pre>
+</body>
+</html>

demo.c

-// Demo program for the static library project of ABC
-
-#include <stdio.h>
-#include "src/sat/csat/csat_apis.h"
-
-// procedures to start and stop the ABC framework
-extern void  Abc_Start();
-extern void  Abc_Stop();
-
-// simple test prog
-int main( int argc, char * argv[] )
-{
-    CSAT_Manager_t * mng;
-    CSAT_Target_ResultT * pResult;
-    char * Names[2];
-    int Values[2];
-    int i;
-
-    // start ABC
-    // (calling Abc_Start() for each problem is timeconsuming
-    //  because it allocates some internal data structures used by decomposition packages
-    //  so Abc_Start should be called once before creating many solution managers)
-    Abc_Start();
-
-    // start the solution manager
-    // (the manager can be reused for several targets if the targets
-    //  use the same network and only differ in the asserted values;
-    //  however, only one target can be loaded into the manager at any time)
-    mng = CSAT_InitManager();
-
-    // create a simple circuit
-    // PIs: A, B, C
-    // POs: F = ((AB)C) <+> (A(BC))
-    // Internal nodes:
-    // X = AB   U = XC
-    // Y = BC   W = AY
-    // G = U <+> W
-    // F = G
-
-    // PIs should be added first
-    CSAT_AddGate( mng, CSAT_BPI, "A", 0, NULL, 0 );
-    CSAT_AddGate( mng, CSAT_BPI, "B", 0, NULL, 0 );
-    CSAT_AddGate( mng, CSAT_BPI, "C", 0, NULL, 0 );
-    // internal nodes should be added next
-    Names[0] = "A";
-    Names[1] = "B";
-    CSAT_AddGate( mng, CSAT_BAND, "X", 2, Names, 0 );
-//    CSAT_AddGate( mng, CSAT_BOR, "X", 2, Names, 0 ); // use this line to make the problem SATISFIABLE
-    Names[0] = "X";
-    Names[1] = "C";
-    CSAT_AddGate( mng, CSAT_BAND, "U", 2, Names, 0 );
-    Names[0] = "B";
-    Names[1] = "C";
-    CSAT_AddGate( mng, CSAT_BAND, "Y", 2, Names, 0 );
-    Names[0] = "A";
-    Names[1] = "Y";
-    CSAT_AddGate( mng, CSAT_BAND, "W", 2, Names, 0 );
-    Names[0] = "U";
-    Names[1] = "W";
-    CSAT_AddGate( mng, CSAT_BXOR, "G", 2, Names, 0 );
-    // POs should be added last
-    Names[0] = "G";
-    CSAT_AddGate( mng, CSAT_BPO,  "F", 1, Names, 0 );
-
-    // check integrity of the manager (and finalize ABC network in the manager!)
-    if ( CSAT_Check_Integrity( mng ) )
-        printf( "Integrity is okey.\n" );
-    else
-        printf( "Integrity is NOT okey.\n" );
-
-    // dump the problem into a BENCH file
-    // currently BENCH file can only be written for an AIG
-    // so we will transform the network into AIG before dumping it
-    CSAT_EnableDump( mng, "simple.bench" );
-    CSAT_Dump_Bench_File( mng );
-
-    // set the solving target (only one target at a time!)
-    // the target can be expressed sing PI/PO or internal nodes
-    Names[0] = "F";
-    Values[0] = 1;
-    CSAT_AddTarget( mng, 1, Names, Values );
-
-    // initialize the sover
-    CSAT_SolveInit( mng );
-
-    // set the solving option (0 = brute-force SAT; 1 = resource-aware FRAIG)
-    CSAT_SetSolveOption( mng, 1 );
-
-    // solves the last added target
-    CSAT_Solve( mng );
-
-    // get the result of solving
-    pResult = CSAT_Get_Target_Result( mng, 0 );
-
-    // print the report
-    if ( pResult->status == UNDETERMINED )
-        printf( "The problem is UNDETERMINED.\n" );
-    else if ( pResult->status == UNSATISFIABLE )
-        printf( "The problem is UNSATISFIABLE.\n" );
-    else if ( pResult->status == SATISFIABLE )
-    {
-        printf( "The problem is SATISFIABLE.\n" );
-        printf( "Satisfying assignment is: " );
-        for ( i = 0; i < pResult->no_sig; i++ )
-            printf( "%s=%d ", pResult->names[i], pResult->values[i] );
-        printf( "\n" );
-    }
-
-    // free everything to prevent memory leaks
-    CSAT_TargetResFree( pResult );
-    CSAT_QuitManager( mng );
-    Abc_Stop();
-    return 0;
-}
-

src/base/abc/abc.h

@@ -430,11 +430,13 @@ extern void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
 extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
 extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
+extern bool               Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
 extern Vec_Vec_t *        Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
 extern int                Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis );
 /*=== abcFanio.c ==========================================================*/
 extern void               Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
 extern void               Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );

src/base/abc/abcCheck.c

@@ -101,7 +101,7 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
     }
     if ( Abc_NtkHasMapping(pNtk) )
     {
-        if ( pNtk->pManFunc != Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) )
+        if ( pNtk->pManFunc != Abc_FrameReadLibGen() )
         {
             fprintf( stdout, "NetworkCheck: The library of the mapped network is not the global library.\n" );
             return 0;

src/base/abc/abcDfs.c

@@ -206,6 +206,37 @@ void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
     Vec_PtrPush( vNodes, pNode );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the ordering of nodes is DFS.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    // set the traversal ID
+    Abc_NtkIncrementTravId( pNtk );
+    // mark the CIs
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        Abc_NodeSetTravIdCurrent( pNode );
+    // go through the nodes
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pNode)) )
+            return 0;
+        if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) )
+            return 0;
+        Abc_NodeSetTravIdCurrent( pNode );
+    }
+    return 1;
+}
 
 /**Function*************************************************************
 
@@ -573,6 +604,123 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Analyses choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeSetChoiceLevel_rec( Abc_Obj_t * pNode, int fMaximum )
+{
+    Abc_Obj_t * pTemp;
+    int Level1, Level2, Level, LevelE;
+    // skip the visited node
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return (int)pNode->pCopy;
+    Abc_NodeSetTravIdCurrent( pNode );
+    // compute levels of the children nodes
+    Level1 = Abc_NodeSetChoiceLevel_rec( Abc_ObjFanin0(pNode), fMaximum );
+    Level2 = Abc_NodeSetChoiceLevel_rec( Abc_ObjFanin1(pNode), fMaximum );
+    Level  = 1 + ABC_MAX( Level1, Level2 );
+    if ( pNode->pData )
+    {
+        LevelE = Abc_NodeSetChoiceLevel_rec( pNode->pData, fMaximum );
+        if ( fMaximum )
+            Level = ABC_MAX( Level, LevelE );
+        else
+            Level = ABC_MIN( Level, LevelE );
+        // set the level of all equivalent nodes to be the same minimum
+        for ( pTemp = pNode->pData; pTemp; pTemp = pTemp->pData )
+            pTemp->pCopy = (void *)Level;
+    }
+    pNode->pCopy = (void *)Level;
+    return Level;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resets the levels of the nodes in the choice graph.]
+
+  Description [Makes the level of the choice nodes to be equal to the
+  maximum of the level of the nodes in the equivalence class. This way
+  sorting by level leads to the reverse topological order, which is
+  needed for the required time computation.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_AigSetChoiceLevels( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, LevelMax, LevelCur;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // set the new travid counter
+    Abc_NtkIncrementTravId( pNtk );
+    // set levels of the CI and constant
+    Abc_NtkForEachCi( pNtk, pObj, i )
+    {
+        Abc_NodeSetTravIdCurrent( pObj );
+        pObj->pCopy = NULL;
+    }
+    pObj = Abc_AigConst1( pNtk->pManFunc );
+    Abc_NodeSetTravIdCurrent( pObj );
+    pObj->pCopy = NULL;
+    // set levels of all other nodes
+    LevelMax = 0;
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        LevelCur = Abc_NodeSetChoiceLevel_rec( Abc_ObjFanin0(pObj), 1 );
+        LevelMax = ABC_MAX( LevelMax, LevelCur );
+    }
+    return LevelMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns nodes by level from the smallest to the largest.]
+
+  Description [Correctly handles the case of choice nodes, by first
+  spreading them out across several levels and then collecting.]
+               
+  SideEffects [What happens with dangling nodes???]
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis )
+{
+    Vec_Ptr_t * vNodes, * vLevels;
+    Abc_Obj_t * pNode, ** ppHead;
+    int LevelMax, i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // set the correct levels
+    Abc_NtkCleanCopy( pNtk );
+    LevelMax = Abc_AigSetChoiceLevels( pNtk );
+    // relink nodes by level
+    vLevels = Vec_PtrStart( LevelMax + 1 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        ppHead = ((Abc_Obj_t **)vLevels->pArray) + (int)pNode->pCopy;
+        pNode->pCopy = *ppHead;
+        *ppHead = pNode;
+    }
+    // recollect nodes
+    vNodes = Vec_PtrStart( Abc_NtkNodeNum(pNtk) );
+    Vec_PtrForEachEntryStart( vLevels, pNode, i, !fCollectCis )
+        for ( ; pNode; pNode = pNode->pCopy )
+            Vec_PtrPush( vNodes, pNode );
+    Vec_PtrFree( vLevels );
+    return vNodes;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abc/abcNtk.c

@@ -74,7 +74,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
     else if ( Abc_NtkHasAig(pNtk) )
         pNtk->pManFunc = Abc_AigAlloc( pNtk );
     else if ( Abc_NtkHasMapping(pNtk) )
-        pNtk->pManFunc = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
+        pNtk->pManFunc = Abc_FrameReadLibGen();
     else
         assert( 0 );
     return pNtk;

src/base/abc/abcObj.c

@@ -518,7 +518,7 @@ Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadLogicZero(pNtk->pManFunc), Cudd_Ref( pNode->pData );
     else if ( Abc_NtkHasMapping(pNtk) )
-        pNode->pData = Mio_LibraryReadConst0(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
+        pNode->pData = Mio_LibraryReadConst0(Abc_FrameReadLibGen());
     else
         assert( 0 );
     return pNode;
@@ -546,7 +546,7 @@ Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadOne(pNtk->pManFunc), Cudd_Ref( pNode->pData );
     else if ( Abc_NtkHasMapping(pNtk) )
-        pNode->pData = Mio_LibraryReadConst1(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
+        pNode->pData = Mio_LibraryReadConst1(Abc_FrameReadLibGen());
     else
         assert( 0 );
     return pNode;
@@ -574,7 +574,7 @@ Abc_Obj_t * Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_Not(Cudd_bddIthVar(pNtk->pManFunc,0)), Cudd_Ref( pNode->pData );
     else if ( Abc_NtkHasMapping(pNtk) )
-        pNode->pData = Mio_LibraryReadInv(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
+        pNode->pData = Mio_LibraryReadInv(Abc_FrameReadLibGen());
     else
         assert( 0 );
     return pNode;
@@ -602,7 +602,7 @@ Abc_Obj_t * Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_bddIthVar(pNtk->pManFunc,0), Cudd_Ref( pNode->pData );
     else if ( Abc_NtkHasMapping(pNtk) )
-        pNode->pData = Mio_LibraryReadBuf(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
+        pNode->pData = Mio_LibraryReadBuf(Abc_FrameReadLibGen());
     else
         assert( 0 );
     return pNode;
@@ -781,7 +781,7 @@ bool Abc_NodeIsConst0( Abc_Obj_t * pNode )
     if ( Abc_NtkHasAig(pNtk) )
         return Abc_ObjNot(pNode) == Abc_AigConst1(pNode->pNtk->pManFunc);
     if ( Abc_NtkHasMapping(pNtk) )
-        return pNode->pData == Mio_LibraryReadConst0(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
+        return pNode->pData == Mio_LibraryReadConst0(Abc_FrameReadLibSuper());
     assert( 0 );
     return 0;
 }
@@ -809,7 +809,7 @@ bool Abc_NodeIsConst1( Abc_Obj_t * pNode )
     if ( Abc_NtkHasAig(pNtk) )
         return pNode == Abc_AigConst1(pNode->pNtk->pManFunc);
     if ( Abc_NtkHasMapping(pNtk) )
-        return pNode->pData == Mio_LibraryReadConst1(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
+        return pNode->pData == Mio_LibraryReadConst1(Abc_FrameReadLibSuper());
     assert( 0 );
     return 0;
 }
@@ -838,7 +838,7 @@ bool Abc_NodeIsBuf( Abc_Obj_t * pNode )
     if ( Abc_NtkHasAig(pNtk) )
         return 0;
     if ( Abc_NtkHasMapping(pNtk) )
-        return pNode->pData == Mio_LibraryReadBuf(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
+        return pNode->pData == Mio_LibraryReadBuf(Abc_FrameReadLibSuper());
     assert( 0 );
     return 0;
 }
@@ -867,7 +867,7 @@ bool Abc_NodeIsInv( Abc_Obj_t * pNode )
     if ( Abc_NtkHasAig(pNtk) )
         return 0;
     if ( Abc_NtkHasMapping(pNtk) )
-        return pNode->pData == Mio_LibraryReadInv(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
+        return pNode->pData == Mio_LibraryReadInv(Abc_FrameReadLibSuper());
     assert( 0 );
     return 0;
 }

src/base/abci/abc.c

@@ -22,6 +22,8 @@
 #include "mainInt.h"
 #include "fraig.h"
 #include "fxu.h"
+#include "fpga.h"
+#include "pga.h"
 #include "cut.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -80,6 +82,7 @@ static int Abc_CommandAttach       ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandSuperChoice  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPga          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandSeq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -156,6 +159,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "SC mapping",   "sc",            Abc_CommandSuperChoice,      1 );
 
     Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
+    Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
 
     Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
@@ -2720,14 +2724,13 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     pParams->nVarsMax  = 5;     // the max cut size ("k" of the k-feasible cuts)
     pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
-    pParams->fTruth    = 1;     // compute truth tables
-    pParams->fHash     = 0;     // hash cuts to detect unique
-    pParams->fFilter   = 0;     // filter dominated cuts
+    pParams->fTruth    = 0;     // compute truth tables
+    pParams->fFilter   = 1;     // filter dominated cuts
     pParams->fSeq      = 0;     // compute sequential cuts
     pParams->fDrop     = 0;     // drop cuts on the fly
     pParams->fVerbose  = 0;     // the verbosiness flag
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "KMtrfsdvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "KMtfsdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2756,9 +2759,6 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             pParams->fTruth ^= 1;
             break;
-        case 'r':
-            pParams->fHash ^= 1;
-            break;
         case 'f':
             pParams->fFilter ^= 1;
             break;
@@ -2794,16 +2794,15 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cut [-K num] [-M num] [-trfsdvh]\n" );
+    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfsdvh]\n" );
     fprintf( pErr, "\t         computes k-feasible cuts for the AIG\n" );
-    fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n",    pParams->nVarsMax );
-    fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",     pParams->nKeepMax );
-    fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",          pParams->fTruth? "yes": "no" );
-    fprintf( pErr, "\t-r     : toggle reduction by hashing [default = %s]\n",             pParams->fHash? "yes": "no" );
-    fprintf( pErr, "\t-f     : toggle filtering by dominance [default = %s]\n",           pParams->fFilter? "yes": "no" );
-    fprintf( pErr, "\t-s     : toggle sequential cut computation [default = %s]\n",       pParams->fSeq? "yes": "no" );
-    fprintf( pErr, "\t-d     : toggle dropping when fanouts are done [default = %s]\n",   pParams->fDrop? "yes": "no" );
-    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",     pParams->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n",     pParams->nVarsMax );
+    fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",      pParams->nKeepMax );
+    fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",           pParams->fTruth? "yes": "no" );
+    fprintf( pErr, "\t-f     : toggle filtering of duplicated/dominated [default = %s]\n", pParams->fFilter? "yes": "no" );
+    fprintf( pErr, "\t-s     : toggle sequential cut computation [default = %s]\n",        pParams->fSeq? "yes": "no" );
+    fprintf( pErr, "\t-d     : toggle dropping when fanouts are done [default = %s]\n",    pParams->fDrop? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",      pParams->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -3771,6 +3770,123 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    Pga_Params_t Params, * pParams = &Params;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    memset( pParams, 0, sizeof(Pga_Params_t) );
+    pParams->pNtk       = pNtk;
+    pParams->pLutLib    = Abc_FrameReadLibLut();
+    pParams->fAreaFlow  = 1;
+    pParams->fArea      = 1;
+    pParams->fSwitching = 0;
+    pParams->fDropCuts  = 0;
+    pParams->fVerbose   = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "fapdvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'f':
+            pParams->fAreaFlow ^= 1;
+            break;
+        case 'a':
+            pParams->fArea ^= 1;
+            break;
+        case 'p':
+            pParams->fSwitching ^= 1;
+            break;
+        case 'd':
+            pParams->fDropCuts ^= 1;
+            break;
+        case 'v':
+            pParams->fVerbose ^= 1;
+            break;
+        case 'h':
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        // strash and balance the network
+        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        if ( pNtk == NULL )
+        {
+            fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
+            return 1;
+        }
+        pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0 );
+        Abc_NtkDelete( pNtkRes );
+        if ( pNtk == NULL )
+        {
+            fprintf( pErr, "Balancing before FPGA mapping has failed.\n" );
+            return 1;
+        }
+        fprintf( pOut, "The network was strashed and balanced before FPGA mapping.\n" );
+        // get the new network
+        pNtkRes = Abc_NtkPga( pParams );
+        if ( pNtkRes == NULL )
+        {
+            Abc_NtkDelete( pNtk );
+            fprintf( pErr, "FPGA mapping has failed.\n" );
+            return 1;
+        }
+        Abc_NtkDelete( pNtk );
+    }
+    else
+    {
+        // get the new network
+        pNtkRes = Abc_NtkPga( pParams );
+        if ( pNtkRes == NULL )
+        {
+            fprintf( pErr, "FPGA mapping has failed.\n" );
+            return 1;
+        }
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: pga [-fapdvh]\n" );
+    fprintf( pErr, "\t        performs FPGA mapping of the current network\n" );
+    fprintf( pErr, "\t-f    : toggles area flow recovery [default = %s]\n", pParams->fAreaFlow? "yes": "no" );
+    fprintf( pErr, "\t-a    : toggles area recovery [default = %s]\n", pParams->fArea? "yes": "no" );
+    fprintf( pErr, "\t-p    : optimizes power by minimizing switching activity [default = %s]\n", pParams->fSwitching? "yes": "no" );
+    fprintf( pErr, "\t-d    : toggles dropping cuts to save memory [default = %s]\n", pParams->fDropCuts? "yes": "no" );
+    fprintf( pErr, "\t-v    : toggles verbose output [default = %s]\n", pParams->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h    : prints the command usage\n");
+    return 1;
+}
+
 
 
 /**Function*************************************************************

src/base/abci/abcAttach.c

@@ -66,7 +66,7 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsSopLogic(pNtk) );
 
     // check that the library is available
-    pGenlib = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
+    pGenlib = Abc_FrameReadLibGen();
     if ( pGenlib == NULL )
     {
         printf( "The current library is not available.\n" );

src/base/abci/abcCut.c

@@ -105,7 +105,6 @@ PRT( "Total", clock() - clk );
         if ( Abc_NodeIsTravIdCurrent(pDriver) )
             continue;
         Abc_NodeSetTravIdCurrent(pDriver);
-        Cut_NodeSetComputedAsNew( p, pDriver->Id );
     }
     // compute as long as new cuts appear
 

src/base/abci/abcFraig.c

@@ -556,7 +556,7 @@ void Abc_NtkFraigStoreCheck( Abc_Ntk_t * pFraig )
     int i, k;
     // check that the PO functions are correct
     nPoFinal = Abc_NtkPoNum(pFraig);
-    nStored  = Abc_FrameReadNtkStoreSize(Abc_FrameGetGlobalFrame());
+    nStored  = Abc_FrameReadNtkStoreSize();
     assert( nPoFinal % nStored == 0 );
     nPoOrig  = nPoFinal / nStored;
     for ( i = 0; i < nPoOrig; i++ )

src/base/abci/abcMap.c

@@ -66,18 +66,18 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
     assert( Abc_NtkIsStrash(pNtk) );
 
     // check that the library is available
-    if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == NULL )
+    if ( Abc_FrameReadLibGen() == NULL )
     {
         printf( "The current library is not available.\n" );
         return 0;
     }
 
     // derive the supergate library
-    if ( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) == NULL && Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) )
+    if ( Abc_FrameReadLibSuper() == NULL && Abc_FrameReadLibGen() )
     {
         printf( "A simple supergate library is derived from gate library \"%s\".\n", 
-            Mio_LibraryReadName(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame())) );
-        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
+            Mio_LibraryReadName(Abc_FrameReadLibGen()) );
+        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen() );
     }
 
     // print a warning about choice nodes
@@ -410,7 +410,7 @@ int Abc_NtkUnmap( Abc_Ntk_t * pNtk )
 
     assert( Abc_NtkIsMappedLogic(pNtk) );
     // update the functionality manager
-    assert( pNtk->pManFunc == Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
+    assert( pNtk->pManFunc == Abc_FrameReadLibGen() );
     pNtk->pManFunc = Extra_MmFlexStart();
     pNtk->ntkFunc  = ABC_FUNC_SOP;
     // update the nodes
@@ -446,18 +446,18 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsStrash(pNtk) );
 
     // check that the library is available
-    if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == NULL )
+    if ( Abc_FrameReadLibGen() == NULL )
     {
         printf( "The current library is not available.\n" );
         return 0;
     }
 
     // derive the supergate library
-    if ( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) == NULL && Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) )
+    if ( Abc_FrameReadLibSuper() == NULL && Abc_FrameReadLibGen() )
     {
         printf( "A simple supergate library is derived from gate library \"%s\".\n", 
-            Mio_LibraryReadName(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame())) );
-        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
+            Mio_LibraryReadName(Abc_FrameReadLibGen()) );
+        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen() );
     }
 
     // print a warning about choice nodes

src/base/abci/abcPga.c

+/**CFile****************************************************************
+
+  FileName    [abcPga.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcPga.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fraig.h"
+#include "fpga.h"
+#include "pga.h"
+#include "cut.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t * Abc_NtkFromPga( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodeCuts );
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams )
+{
+    Abc_Ntk_t * pNtkNew, * pNtk = pParams->pNtk;
+    Pga_Man_t * pMan;
+    Vec_Ptr_t * vNodeCuts;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // print a warning about choice nodes
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+        printf( "Performing FPGA mapping with choices.\n" );
+
+    // start the mapping manager
+    pMan = Pga_ManStart( pParams );    
+    if ( pMan == NULL )
+        return NULL;
+
+    // perform mapping
+    vNodeCuts = Pga_DoMapping( pMan );
+
+    // transform the result of mapping into a BDD logic network
+    pNtkNew = Abc_NtkFromPga( pNtk, vNodeCuts );
+    if ( pNtkNew == NULL )
+        return NULL;
+    Pga_ManStop( pMan );
+    Vec_PtrFree( vNodeCuts );
+
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkNew );
+
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkPga: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromPga( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodeCuts )
+{
+    ProgressBar * pProgress;
+    DdManager * dd;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pFanin, * pNodeNew;
+    Cut_Cut_t * pCut;
+    Vec_Ptr_t * vLeaves, * vVisited;
+    int i, k, nDupGates;
+    // create the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
+    dd = pNtkNew->pManFunc;
+    // set the constant node
+    pNode = Abc_AigConst1(pNtk->pManFunc);
+    if ( Abc_ObjFanoutNum(pNode) > 0 )
+        pNode->pCopy = Abc_NodeCreateConst1(pNtkNew);
+    // add new nodes in topologic order
+    vLeaves  = Vec_PtrAlloc( 6 );
+    vVisited = Vec_PtrAlloc( 100 );
+    pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodeCuts) );
+    Vec_PtrForEachEntry( vNodeCuts, pCut, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // create the new node
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );
+        Vec_PtrClear( vLeaves );
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+        {
+            // add the node representing the old fanin in the new network
+            pFanin = Abc_NtkObj( pNtk, pCut->pLeaves[k] );
+            Vec_PtrPush( vLeaves, pFanin );
+            Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
+        }
+        // set the new node at the old node
+        pNode = Abc_NtkObj( pNtk, pCut->uSign );  // pCut->uSign contains the ID of the root node
+        pNode->pCopy = pNodeNew;
+        // create the function of the new node
+        pNodeNew->pData = Abc_NodeConeBdd( dd, dd->vars, pNode, vLeaves, vVisited );   Cudd_Ref( pNodeNew->pData );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vVisited );
+    Vec_PtrFree( vLeaves );
+    // finalize the new network
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    // decouple the PO driver nodes to reduce the number of levels
+    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+//    if ( nDupGates && Fpga_ManReadVerbose(pMan) )
+//        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abci/abcRewrite.c

@@ -32,7 +32,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk, int fDrop );
+static Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk );
 static void        Abc_NodePrintCuts( Abc_Obj_t * pNode );
 
 ////////////////////////////////////////////////////////////////////////
@@ -52,7 +52,6 @@ static void        Abc_NodePrintCuts( Abc_Obj_t * pNode );
 ***********************************************************************/
 int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose )
 {
-    int fDrop = 0;
     ProgressBar * pProgress;
     Cut_Man_t * pManCut;
     Rwr_Man_t * pManRwr;
@@ -72,7 +71,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
         Abc_NtkStartReverseLevels( pNtk );
     // start the cut manager
 clk = clock();
-    pManCut = Abc_NtkStartCutManForRewrite( pNtk, fDrop );
+    pManCut = Abc_NtkStartCutManForRewrite( pNtk );
 Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
     pNtk->pManCut = pManCut;
 
@@ -142,7 +141,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk, int fDrop )
+Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk )
 {
     static Cut_Params_t Params, * pParams = &Params;
     Cut_Man_t * pManCut;
@@ -153,10 +152,9 @@ Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk, int fDrop )
     pParams->nVarsMax  = 4;     // the max cut size ("k" of the k-feasible cuts)
     pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
     pParams->fTruth    = 1;     // compute truth tables
-    pParams->fHash     = 1;     // hash cuts to detect unique
-    pParams->fFilter   = 0;     // filter dominated cuts
+    pParams->fFilter   = 1;     // filter dominated cuts
     pParams->fSeq      = 0;     // compute sequential cuts
-    pParams->fDrop     = fDrop; // drop cuts on the fly
+    pParams->fDrop     = 0;     // drop cuts on the fly
     pParams->fVerbose  = 0;     // the verbosiness flag
     pParams->nIdsMax   = Abc_NtkObjNumMax( pNtk );
     pManCut = Cut_ManStart( pParams );
@@ -182,13 +180,15 @@ Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk, int fDrop )
 ***********************************************************************/
 void Abc_NodePrintCuts( Abc_Obj_t * pNode )
 {
+    Vec_Ptr_t * vCuts;
     Cut_Cut_t * pCut;
-    unsigned uTruth;
+    int k;
+
     printf( "\nNode %s\n", Abc_ObjName(pNode) );
-    for ( pCut = (Cut_Cut_t *)pNode->pCopy; pCut; pCut = pCut->pNext )
+    vCuts = (Vec_Ptr_t *)pNode->pCopy;
+    Vec_PtrForEachEntry( vCuts, pCut, k )
     {
-        uTruth = pCut->uTruth;
-        Extra_PrintBinary( stdout, &uTruth, 16 ); 
+        Extra_PrintBinary( stdout, (unsigned *)&pCut->uSign, 16 ); 
         printf( "   " );
         Cut_CutPrint( pCut );   
         printf( "\n" );

src/base/abci/abcTiming.c

@@ -470,9 +470,9 @@ void Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtkOld )
     int i;
     if ( pNtkOld->pManTime == NULL )
         return;
-    if ( Mio_LibraryReadNand2(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame())) == NULL )
+    if ( Mio_LibraryReadNand2(Abc_FrameReadLibGen()) == NULL )
         return;
-    tAndDelay = Mio_LibraryReadDelayNand2Max(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
+    tAndDelay = Mio_LibraryReadDelayNand2Max(Abc_FrameReadLibGen());
     Abc_NtkForEachPi( pNtkOld, pNodeOld, i )
     {
         pNodeNew = pNodeOld->pCopy;

src/base/abci/module.make

@@ -10,6 +10,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcMap.c \
     src/base/abci/abcMiter.c \
     src/base/abci/abcNtbdd.c \
+    src/base/abci/abcPga.c \
     src/base/abci/abcPrint.c \
     src/base/abci/abcReconv.c \
     src/base/abci/abcRefactor.c \

src/base/io/ioReadBlif.c

@@ -550,7 +550,7 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
     int i, nNames;
 
     // check that the library is available
-    pGenlib = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
+    pGenlib = Abc_FrameReadLibGen();
     if ( pGenlib == NULL )
     {
         p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);

src/base/main/main.c

@@ -21,7 +21,7 @@
 #include "mainInt.h"
 
 // this line should be included in the library project
-#define _LIB
+//#define _LIB
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///

src/map/fpga/fpga.c

@@ -77,7 +77,7 @@ void Fpga_Init( Abc_Frame_t * pAbc )
 ***********************************************************************/
 void Fpga_End()
 {
-    Fpga_LutLibFree( Abc_FrameReadLibLut(Abc_FrameGetGlobalFrame()) );
+    Fpga_LutLibFree( Abc_FrameReadLibLut() );
 }
 
 
@@ -221,7 +221,7 @@ int Fpga_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // set the new network
-    Fpga_LutLibPrint( Abc_FrameReadLibLut(Abc_FrameGetGlobalFrame()) );
+    Fpga_LutLibPrint( Abc_FrameReadLibLut() );
     return 0;
 
 usage:

src/map/fpga/fpga.h

@@ -142,6 +142,11 @@ extern Fpga_Man_t *    Fpga_ManDupFraig( Fraig_Man_t * pManFraig );
 extern Fpga_Man_t *    Fpga_ManBalanceFraig( Fraig_Man_t * pManFraig, int * pInputArrivals );
 /*=== fpgaLib.c =============================================================*/
 extern Fpga_LutLib_t * Fpga_LutLibDup( Fpga_LutLib_t * p );
+extern int             Fpga_LutLibReadVarMax( Fpga_LutLib_t * p );
+extern float *         Fpga_LutLibReadLutAreas( Fpga_LutLib_t * p );
+extern float *         Fpga_LutLibReadLutDelays( Fpga_LutLib_t * p );
+extern float           Fpga_LutLibReadLutArea( Fpga_LutLib_t * p, int Size );
+extern float           Fpga_LutLibReadLutDelay( Fpga_LutLib_t * p, int Size );
 /*=== fpgaTruth.c =============================================================*/
 extern void *          Fpga_TruthsCutBdd( void * dd, Fpga_Cut_t * pCut );
 /*=== fpgaUtil.c =============================================================*/

src/map/fpga/fpgaCreate.c

@@ -164,7 +164,7 @@ Fpga_Man_t * Fpga_ManCreate( int nInputs, int nOutputs, int fVerbose )
     // start the manager
     p = ALLOC( Fpga_Man_t, 1 );
     memset( p, 0, sizeof(Fpga_Man_t) );
-    p->pLutLib   = Abc_FrameReadLibLut(Abc_FrameGetGlobalFrame());
+    p->pLutLib   = Abc_FrameReadLibLut();
     p->nVarsMax  = p->pLutLib->LutMax;
     p->fVerbose  = fVerbose;
     p->fAreaRecovery = 1;

src/map/fpga/fpgaCut.c

@@ -245,7 +245,7 @@ Fpga_Cut_t * Fpga_CutCompute( Fpga_Man_t * p, Fpga_CutTable_t * pTable, Fpga_Nod
     // set at the node
     pNode->pCuts = pCut;
     // remove the dominated cuts
-    Fpga_CutFilter( p, pNode );
+//    Fpga_CutFilter( p, pNode );
     // set the phase correctly
     if ( pNode->pRepr && Fpga_NodeComparePhase(pNode, pNode->pRepr) )
     {

src/map/fpga/fpgaLib.c

@@ -28,6 +28,23 @@
 
 /**Function*************************************************************
 
+  Synopsis    [APIs to access LUT library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int         Fpga_LutLibReadVarMax( Fpga_LutLib_t * p )               { return p->LutMax;     }
+float *     Fpga_LutLibReadLutAreas( Fpga_LutLib_t * p )             { return p->pLutAreas;  }
+float *     Fpga_LutLibReadLutDelays( Fpga_LutLib_t * p )            { return p->pLutDelays; }
+float       Fpga_LutLibReadLutArea( Fpga_LutLib_t * p, int Size )    { assert( Size <= p->LutMax ); return p->pLutAreas[Size];  }
+float       Fpga_LutLibReadLutDelay( Fpga_LutLib_t * p, int Size )   { assert( Size <= p->LutMax ); return p->pLutDelays[Size]; }
+
+/**Function*************************************************************
+
   Synopsis    [Reads the description of LUTs from the LUT library file.]
 
   Description []

src/map/mapper/mapper.c

@@ -61,7 +61,7 @@ void Map_Init( Abc_Frame_t * pAbc )
 void Map_End()
 {
 //    Map_SuperLibFree( s_pSuperLib );
-     Map_SuperLibFree( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) );
+     Map_SuperLibFree( Abc_FrameReadLibSuper() );
 }
 
 

src/map/mapper/mapperCreate.c

@@ -183,7 +183,7 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
     int i;
 
     // derive the supergate library
-    if ( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) == NULL )
+    if ( Abc_FrameReadLibSuper() == NULL )
     {
         printf( "The supergate library is not specified. Use \"read_library\" or \"read_super\".\n" );
         return NULL;
@@ -192,7 +192,7 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
     // start the manager
     p = ALLOC( Map_Man_t, 1 );
     memset( p, 0, sizeof(Map_Man_t) );
-    p->pSuperLib = Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame());
+    p->pSuperLib = Abc_FrameReadLibSuper();
     p->nVarsMax  = p->pSuperLib->nVarsMax;
     p->fVerbose  = fVerbose;
     p->fEpsilon  = (float)0.001;

src/map/mapper/mapperCut.c

@@ -208,7 +208,7 @@ Map_Cut_t * Map_CutCompute( Map_Man_t * p, Map_CutTable_t * pTable, Map_Node_t *
     // set at the node
     pNode->pCuts = pCut;
     // remove the dominated cuts
-//    Map_CutFilter( p, pNode );
+    Map_CutFilter( p, pNode );
     // set the phase correctly
     if ( pNode->pRepr && Map_NodeComparePhase(pNode, pNode->pRepr) )
     {

src/map/mio/mio.c

@@ -108,7 +108,7 @@ void Mio_Init( Abc_Frame_t * pAbc )
 void Mio_End()
 {
 //    Mio_LibraryDelete( s_pLib );
-    Mio_LibraryDelete( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
+    Mio_LibraryDelete( Abc_FrameReadLibGen() );
 }
 
 
@@ -181,7 +181,7 @@ int Mio_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
         return 1;
     }
     // free the current superlib because it depends on the old Mio library
-    if ( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) )
+    if ( Abc_FrameReadLibSuper() )
     {
         extern void Map_SuperLibFree( Map_SuperLib_t * p );
 //        Map_SuperLibFree( s_pSuperLib );
@@ -252,7 +252,7 @@ int Mio_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // set the new network
-    Mio_WriteLibrary( stdout, Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()), 0 );
+    Mio_WriteLibrary( stdout, Abc_FrameReadLibGen(), 0 );
     return 0;
 
 usage:

src/map/pga/module.make

+SRC +=  src/map/pga/pgaCore.c \
+        src/map/pga/pgaMan.c \
+        src/map/pga/pgaMatch.c \
+        src/map/pga/pgaUtil.c 

src/map/pga/pga.h

+/**CFile****************************************************************
+
+  FileName    [pga.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapper.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: pga.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __PGA_H__
+#define __PGA_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Pga_ManStruct_t_      Pga_Man_t;
+typedef struct Pga_ParamsStruct_t_   Pga_Params_t;
+
+struct Pga_ParamsStruct_t_
+{
+    // data for mapping
+    Abc_Ntk_t *        pNtk;          // the network to be mapped
+    Fpga_LutLib_t *    pLutLib;       // the LUT library
+    float *            pSwitching;    // switching activity for each node
+    // mapping parameters
+    int                fDropCuts;     // enables cut dropping
+    int                fAreaFlow;     // enables area flow minimization
+    int                fArea;         // enables area minimization
+    int                fSwitching;    // enables switching activity minimization
+    int                fVerbose;      // enables verbose output
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== pgaApi.c ==========================================================*/
+extern Vec_Ptr_t *   Pga_DoMapping( Pga_Man_t * p );
+/*=== pgaMan.c ==========================================================*/
+extern Pga_Man_t *   Pga_ManStart( Pga_Params_t * pParams );
+extern void          Pga_ManStop( Pga_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+

src/map/pga/pgaCore.c

+/**CFile****************************************************************
+
+  FileName    [pgaCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapper.]
+
+  Synopsis    [External APIs of the FPGA manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: pgaCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pgaInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Pga_MappingInitCis( Pga_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs technology mapping for the given object graph.]
+
+  Description [The object graph is stored in the mapping manager.
+  First, all the AND-nodes, which fanout into the POs, are collected
+  in the DFS fashion. Next, three steps are performed: the k-feasible
+  cuts are computed for each node, the truth tables are computed for
+  each cut, and the delay-optimal matches are assigned for each node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Pga_DoMapping( Pga_Man_t * p )
+{
+    int fShowSwitching = 0;
+    float aAreaTotalCur;
+    int Iter, clk, clkTotal = clock();
+    
+    // assign the arrival times of the PIs
+    Pga_MappingInitCis( p );
+
+    // map the AIG for delay
+clk = clock();
+    Pga_MappingMatches( p, 0 );
+p->timeDelay = clock() - clk;
+
+    // compute area, set references, and collect nodes used in the mapping
+    Iter = 1;
+    aAreaTotalCur = Pga_MappingSetRefsAndArea( p );
+if ( p->pParams->fVerbose )
+{
+printf( "Iteration %dD :  Area = %8.1f  ", Iter++, aAreaTotalCur );
+if ( fShowSwitching )
+printf( "Switch = %8.1f  ", Pga_MappingGetSwitching(p) );
+PRT( "Time", p->timeDelay );
+}
+
+    if ( p->pParams->fAreaFlow )
+    {
+clk = clock();
+        // compute the required times and the fanouts
+        Pga_MappingComputeRequired( p );
+        // remap topologically
+        Pga_MappingMatches( p, 1 );
+p->timeAreaFlow = clock() - clk;
+        // get the resulting area
+        aAreaTotalCur = Pga_MappingSetRefsAndArea( p );
+        // note that here we do not update the reference counter
+        // for some reason, this works better on benchmarks
+if ( p->pParams->fVerbose )
+{
+printf( "Iteration %dF :  Area = %8.1f  ", Iter++, aAreaTotalCur );
+if ( fShowSwitching )
+printf( "Switch = %8.1f  ", Pga_MappingGetSwitching(p) );
+PRT( "Time", p->timeAreaFlow );
+}
+    }
+
+    if ( p->pParams->fArea )
+    {
+clk = clock();
+        // compute the required times and the fanouts
+        Pga_MappingComputeRequired( p );
+        // remap topologically
+        if ( p->pParams->fSwitching )
+            Pga_MappingMatches( p, 3 );
+        else
+            Pga_MappingMatches( p, 2 );
+p->timeArea = clock() - clk;
+        // get the resulting area
+        aAreaTotalCur = Pga_MappingSetRefsAndArea( p );
+if ( p->pParams->fVerbose )
+{
+printf( "Iteration %d%s :  Area = %8.1f  ", Iter++, (p->pParams->fSwitching?"S":"A"), aAreaTotalCur );
+if ( fShowSwitching )
+printf( "Switch = %8.1f  ", Pga_MappingGetSwitching(p) );
+PRT( "Time", p->timeArea );
+}
+    }
+    p->AreaGlobal = aAreaTotalCur;
+
+    if ( p->pParams->fVerbose )
+        Pga_MappingPrintOutputArrivals( p );
+
+    // return the mapping
+    return Pga_MappingResults( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Initializes the CI node arrival times.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pga_MappingInitCis( Pga_Man_t * p )
+{
+    Pga_Node_t * pNode;
+    float * pCiArrs;
+    int i;
+    // get the CI arrival times
+    pCiArrs = Abc_NtkGetCiArrivalFloats( p->pParams->pNtk );
+    // assign the arrival times of the PIs
+    Pga_ManForEachCi( p, pNode, i )
+        pNode->Match.Delay = pCiArrs[i];
+    free( pCiArrs );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/map/pga/pgaInt.h

+/**CFile****************************************************************
+
+  FileName    [pgaInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapper.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: pgaInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __PGA_INT_H__
+#define __PGA_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "abc.h"
+#include "fraig.h"
+#include "fpga.h"
+#include "cut.h"
+#include "pga.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Pga_NodeStruct_t_     Pga_Node_t;
+typedef struct Pga_MatchStruct_t_    Pga_Match_t;
+
+struct Pga_ManStruct_t_
+{
+    // mapping parameters
+    Pga_Params_t *     pParams;       // input data
+    // mapping structures
+    Pga_Node_t *       pMemory;       // the memory for all mapping structures
+    Vec_Ptr_t *        vStructs;      // mapping structures one-to-one with ABC nodes
+    Vec_Ptr_t *        vOrdering;     // mapping nodes ordered by level
+    // k-feasible cuts
+    int                nVarsMax;      // the "k" of k-feasible cuts
+    Cut_Man_t *        pManCut;       // the cut manager
+    // LUT library
+    float *            pLutDelays;    // the delay of the LUTs
+    float *            pLutAreas;     // the areas of the LUTs
+    float              Epsilon;
+    // global parameters
+    float              AreaGlobal;    // the total area of this mapping
+    float              ArrivalGlobal; // the largest delay of any path
+    float              RequiredGlobal;// the global required time (may be different from largest delay)
+    float              RequiredUser;  // the required time given by the user
+    // runtime stats
+    int                timeToMap;     // the time to start the mapper
+    int                timeCuts;      // the time to compute the cuts
+    int                timeDelay;     // the time to compute delay
+    int                timeAreaFlow;  // the time to perform area flow optimization
+    int                timeArea;      // the time to perform area flow optimization
+    int                timeToNet;     // the time to transform back to network
+    int                timeTotal;     // the total time
+    int                time1;         // temporary
+    int                time2;         // temporary
+};
+
+struct Pga_MatchStruct_t_
+{
+    Cut_Cut_t *        pCut;          // the best cut
+    float              Delay;         // the arrival time of this cut
+    float              Area;          // the area of this cut
+};
+
+struct Pga_NodeStruct_t_
+{
+    int                Id;            // ID of the node 
+    int                nRefs;         // the number of references
+    float              EstRefs;       // the estimated reference counter
+    float              Required;      // the required time
+    float              Switching;     // the switching activity
+    Pga_Match_t        Match;         // the best match at the node
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Pga_Node_t * Pga_Node( Pga_Man_t * p, int Id )  { return p->vStructs->pArray[Id]; }
+
+// iterator through the CIs
+#define Pga_ManForEachCi( p, pCi, i )                                    \
+    for ( i = 0; (i < Abc_NtkCiNum(p->pParams->pNtk)) && (((pCi) = Pga_Node(p, Abc_NtkCi(p->pParams->pNtk,i)->Id)), 1); i++ )
+// iterator through the CO derivers
+#define Pga_ManForEachCoDriver( p, pCo, i )                              \
+    for ( i = 0; (i < Abc_NtkCoNum(p->pParams->pNtk)) && (((pCo) = Pga_Node(p, Abc_ObjFaninId0(Abc_NtkCo(p->pParams->pNtk,i)))), 1); i++ )
+// iterators through the CIs and internal nodes
+#define Pga_ManForEachObjDirect( p, pNode, i )                           \
+    Vec_PtrForEachEntry( p->vOrdering, pNode, i )
+#define Pga_ManForEachObjReverse( p, pNode, i )                           \
+    Vec_PtrForEachEntryReverse( p->vOrdering, pNode, i )
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== pgaMatch.c ==========================================================*/
+extern void        Pga_MappingMatches( Pga_Man_t * p, int Mode );
+/*=== pgaUtil.c ==========================================================*/
+extern Vec_Ptr_t * Pga_MappingResults( Pga_Man_t * p );
+extern float       Pga_TimeComputeArrivalMax( Pga_Man_t * p );
+extern void        Pga_MappingComputeRequired( Pga_Man_t * p );
+extern float       Pga_MappingSetRefsAndArea( Pga_Man_t * p );
+extern float       Pga_MappingGetSwitching( Pga_Man_t * p );
+extern void        Pga_MappingPrintOutputArrivals( Pga_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+

src/map/pga/pgaMan.c

+/**CFile****************************************************************
+
+  FileName    [pgaMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapper.]
+
+  Synopsis    [Mapping manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: pgaMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pgaInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Cut_Man_t * Pga_ManStartCutMan( Pga_Params_t * pParamsPga );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Pga_Man_t * Pga_ManStart( Pga_Params_t * pParams )
+{
+    Pga_Man_t * p;
+    Pga_Node_t * pNode;
+    Cut_Man_t * pManCut;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj;
+    int i, Counter;
+    int clk = clock();
+
+    // make sure the network is given
+    pNtk = pParams->pNtk;
+    if ( pNtk == NULL )
+    {
+        printf( "Network is not specified.\n" );
+        return NULL;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        printf( "Mapping can only be applied to an AIG.\n" );
+        return NULL;
+    }
+    // the cut manager if given should be in sinc
+    pManCut = pNtk->pManCut;
+    if ( pManCut && Cut_ManReadVarsMax(pManCut) != Fpga_LutLibReadVarMax(pParams->pLutLib) )
+    {
+        printf( "The precomputed cuts have different size.\n" );
+        return NULL;
+    }
+    // make sure the nodes are in the topological order
+    if ( !Abc_NtkIsDfsOrdered(pNtk) )
+    {
+        printf( "The nodes of the network are not DFS ordered.\n" );
+//        Abc_NtkReassignIds( pNtk );
+        return NULL;
+    }
+    // make sure there are no dangling nodes (unless they are choices)
+
+    // start the mapping manager
+    p = ALLOC( Pga_Man_t, 1 );
+    memset( p, 0, sizeof(Pga_Man_t) );
+    p->pParams    = pParams;
+    p->nVarsMax   = Fpga_LutLibReadVarMax(pParams->pLutLib);
+    p->pManCut    = pManCut? pManCut : Pga_ManStartCutMan(pParams);
+    p->vOrdering  = Abc_AigGetLevelizedOrder(pNtk, 0);  // what happens with dangling nodes???
+    p->pLutAreas  = Fpga_LutLibReadLutAreas(pParams->pLutLib);
+    p->pLutDelays = Fpga_LutLibReadLutDelays(pParams->pLutLib);
+    p->Epsilon    = (float)0.00001;
+
+    // allocate mapping structures
+    p->pMemory  = ALLOC( Pga_Node_t, Abc_NtkObjNum(pNtk) );
+    memset( p->pMemory, 0, sizeof(Pga_Node_t) * Abc_NtkObjNum(pNtk) );
+    p->vStructs = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
+    Counter = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        pNode = p->pMemory + Counter++;
+        pNode->Id          = pObj->Id;
+        pNode->nRefs       = pObj->vFanouts.nSize;
+        pNode->Required    = ABC_INFINITY;
+        pNode->Match.Area  = ABC_INFINITY;
+        // skip secondary nodes
+        if ( Abc_ObjFanoutNum(pObj) == 0 )
+            continue;
+        Vec_PtrWriteEntry( p->vStructs, pObj->Id, pNode );
+    }
+    assert( Counter == Abc_NtkObjNum(pNtk) );
+    // update order to depend on mapping nodes
+    Vec_PtrForEachEntry( p->vOrdering, pObj, i )
+        Vec_PtrWriteEntry( p->vOrdering, i, Pga_Node(p,pObj->Id) );
+p->timeToMap = clock() - clk;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pga_ManStop( Pga_Man_t * p )
+{
+    Cut_ManStop( p->pManCut );
+    Vec_PtrFree( p->vOrdering );
+    Vec_PtrFree( p->vStructs );
+    free( p->pMemory );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the cut manager for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Pga_ManStartCutMan( Pga_Params_t * pParamsPga )
+{
+    static Cut_Params_t Params, * pParams = &Params;
+    Abc_Ntk_t * pNtk = pParamsPga->pNtk;
+    Cut_Man_t * pManCut;
+    Abc_Obj_t * pObj;
+    int i;
+    // start the cut manager
+    memset( pParams, 0, sizeof(Cut_Params_t) );
+    pParams->nVarsMax  = Fpga_LutLibReadVarMax(pParamsPga->pLutLib); // max cut size
+    pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
+    pParams->fTruth    = 0;     // compute truth tables
+    pParams->fFilter   = 1;     // filter dominated cuts
+    pParams->fSeq      = 0;     // compute sequential cuts
+    pParams->fDrop     = pParamsPga->fDropCuts; // drop cuts on the fly
+    pParams->fVerbose  = 0;     // the verbosiness flag
+    pParams->nIdsMax   = Abc_NtkObjNumMax( pNtk );
+    pManCut = Cut_ManStart( pParams );
+    if ( pParams->fDrop )
+        Cut_ManSetFanoutCounts( pManCut, Abc_NtkFanoutCounts(pNtk) );
+    // set cuts for PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+            Cut_NodeSetTriv( pManCut, pObj->Id );
+    return pManCut;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/map/pga/pgaMatch.c

+/**CFile****************************************************************
+
+  FileName    [pgaMatch.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapper.]
+
+  Synopsis    [Mapping procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: pgaMatch.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pgaInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static char * s_Modes[4] = { "Delay", "Flow", "Area", "Switch" };
+
+static int Pga_MappingMatchNode( Pga_Man_t * p, int NodeId, Cut_Cut_t * pList, int Mode );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs mapping for delay, area-flow, area, switching.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pga_MappingMatches( Pga_Man_t * p, int Mode )
+{
+    ProgressBar * pProgress;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj;
+    Cut_Cut_t * pList;
+    int i, clk;
+
+    assert( Mode >= 0 && Mode <= 2 );
+
+    // match LUTs with nodes in the topological order
+    pNtk = p->pParams->pNtk;
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        // skip the CIs
+        if ( Abc_ObjIsCi(pObj) )
+            continue;
+        // when we reached a CO, it is time to deallocate the cuts
+        if ( Abc_ObjIsCo(pObj) )
+        {
+            if ( p->pParams->fDropCuts )
+                Cut_NodeTryDroppingCuts( p->pManCut, Abc_ObjFaninId0(pObj) );
+            continue;
+        }
+        // skip constant node, it has no cuts
+        if ( Abc_NodeIsConst(pObj) )
+            continue;
+        // get the cuts
+clk = clock();
+        pList = Abc_NodeGetCutsRecursive( p->pManCut, pObj );
+p->timeCuts += clock() - clk;
+        // match the node
+        Pga_MappingMatchNode( p, pObj->Id, pList, Mode );
+        Extra_ProgressBarUpdate( pProgress, i, s_Modes[Mode] );
+    }
+    Extra_ProgressBarStop( pProgress );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the match of the cut.]
+
+  Description [Returns 1 if feasible.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline float Pga_CutGetArrival( Pga_Man_t * p, Cut_Cut_t * pCut )
+{
+    float DelayCur, DelayWorst;
+    unsigned i;
+    assert( pCut->nLeaves > 1 );
+    DelayWorst = -ABC_INFINITY;
+    for ( i = 0; i < pCut->nLeaves; i++ )
+    {
+        DelayCur = Pga_Node(p, pCut->pLeaves[i])->Match.Delay;
+        if ( DelayWorst < DelayCur )
+             DelayWorst = DelayCur;
+    }
+    DelayWorst += p->pLutDelays[pCut->nLeaves];
+    return DelayWorst;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the match of the cut.]
+
+  Description [Returns 1 if feasible.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline float Pga_CutGetAreaFlow( Pga_Man_t * p, Cut_Cut_t * pCut )
+{
+    float Flow;
+    Pga_Node_t * pNode;
+    unsigned i;
+    assert( pCut->nLeaves > 1 );
+    Flow = p->pLutAreas[pCut->nLeaves];
+    for ( i = 0; i < pCut->nLeaves; i++ )
+    {
+        pNode = Pga_Node(p, pCut->pLeaves[i]);
+        assert( pNode->EstRefs > 0 );
+        Flow += pNode->Match.Area / pNode->EstRefs;
+    }
+    return Flow;
+}
+
+/**function*************************************************************
+
+  synopsis    [References the cut.]
+
+  description [This procedure is similar to the procedure NodeReclaim.]
+               
+  sideeffects []
+
+  seealso     []
+
+***********************************************************************/
+float Pga_CutRef( Pga_Man_t * p, Pga_Node_t * pNode, Cut_Cut_t * pCut )
+{
+    Pga_Node_t * pFanin;
+    float aArea;
+    unsigned i;
+    // start the area of this cut
+    aArea = p->pLutAreas[pCut->nLeaves];
+    // go through the children
+    for ( i = 0; i < pCut->nLeaves; i++ )
+    {
+        pFanin = Pga_Node(p, pCut->pLeaves[i]);
+        assert( pFanin->nRefs >= 0 );
+        if ( pFanin->nRefs++ > 0 )  
+            continue;
+        if ( pFanin->Match.pCut == NULL ) 
+            continue;
+        aArea += Pga_CutRef( p, pFanin, pFanin->Match.pCut );
+    }
+    return aArea;
+}
+
+/**function*************************************************************
+
+  synopsis    [Dereferences the cut.]
+
+  description [This procedure is similar to the procedure NodeRecusiveDeref.]
+               
+  sideeffects []
+
+  seealso     []
+
+***********************************************************************/
+float Pga_CutDeref( Pga_Man_t * p, Pga_Node_t * pNode, Cut_Cut_t * pCut )
+{
+    Pga_Node_t * pFanin;
+    float aArea;
+    unsigned i;
+    // start the area of this cut
+    aArea = p->pLutAreas[pCut->nLeaves];
+    // go through the children
+    for ( i = 0; i < pCut->nLeaves; i++ )
+    {
+        pFanin = Pga_Node(p, pCut->pLeaves[i]);
+        assert( pFanin->nRefs > 0 );
+        if ( --pFanin->nRefs > 0 )  
+            continue;
+        if ( pFanin->Match.pCut == NULL ) 
+            continue;
+        aArea += Pga_CutDeref( p, pFanin, pFanin->Match.pCut );
+    }
+    return aArea;
+}
+
+/**function*************************************************************
+
+  synopsis    [Computes the exact area associated with the cut.]
+
+  description [Assumes that the cut is deferenced.]
+               
+  sideeffects []
+
+  seealso     []
+
+***********************************************************************/
+static inline float Pga_CutGetAreaDerefed( Pga_Man_t * p, Pga_Node_t * pNode, Cut_Cut_t * pCut )
+{
+    float aResult, aResult2;
+    assert( pCut->nLeaves > 1 );
+    aResult2 = Pga_CutRef( p, pNode, pCut );
+    aResult  = Pga_CutDeref( p, pNode, pCut );
+    assert( aResult == aResult2 );
+    return aResult;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the match of the cut.]
+
+  Description [Returns 1 if feasible.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Pga_MappingMatchCut( Pga_Man_t * p, Pga_Node_t * pNode, Cut_Cut_t * pCut, int Mode, Pga_Match_t * pMatch )
+{
+    // compute the arrival time of the cut and its area flow
+    pMatch->Delay = Pga_CutGetArrival( p, pCut );
+    // drop the cut if it does not meet the required times
+    if ( pMatch->Delay > pNode->Required + p->Epsilon )
+        return 0;
+    // get the second parameter
+    if ( Mode == 0 || Mode == 1 )
+        pMatch->Area = Pga_CutGetAreaFlow( p, pCut );
+    else if ( Mode == 2 )
+        pMatch->Area = Pga_CutGetAreaDerefed( p, pNode, pCut );
+//    else if ( Mode == 3 )
+//        pMatch->Area = Pga_CutGetSwitching( p, pNode, pCut );
+    // if no cut is assigned, use the current one
+    pMatch->pCut = pCut;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares two matches.]
+
+  Description [Returns 1 if the second match is better.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Pga_MappingCompareMatches( Pga_Man_t * p, Pga_Match_t * pMatchBest, Pga_Match_t * pMatchCur, int Mode )
+{
+    if ( pMatchBest->pCut == NULL )
+        return 1;
+    if ( Mode == 0 )
+    {
+        // compare delays
+        if ( pMatchBest->Delay < pMatchCur->Delay - p->Epsilon )
+            return 0;
+        if ( pMatchBest->Delay > pMatchCur->Delay + p->Epsilon )
+            return 1;
+        // compare areas
+        if ( pMatchBest->Area < pMatchCur->Area - p->Epsilon )
+            return 0;
+        if ( pMatchBest->Area > pMatchCur->Area + p->Epsilon )
+            return 1;
+        // if equal, do not update
+        return 0;
+    }
+    else
+    {
+        // compare areas
+        if ( pMatchBest->Area < pMatchCur->Area - p->Epsilon )
+            return 0;
+        if ( pMatchBest->Area > pMatchCur->Area + p->Epsilon )
+            return 1;
+        // compare delays
+        if ( pMatchBest->Delay < pMatchCur->Delay - p->Epsilon )
+            return 0;
+        if ( pMatchBest->Delay > pMatchCur->Delay + p->Epsilon )
+            return 1;
+        // if equal, do not update
+        return 0;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the best matching for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pga_MappingMatchNode( Pga_Man_t * p, int NodeId, Cut_Cut_t * pList, int Mode )
+{
+    Pga_Match_t MatchCur,  * pMatchCur = &MatchCur;
+    Pga_Match_t MatchBest, * pMatchBest = &MatchBest;
+    Pga_Node_t * pNode;
+    Cut_Cut_t * pCut;
+
+    // get the mapping node
+    pNode = Pga_Node( p, NodeId );
+
+    // prepare for mapping
+    if ( Mode == 0 )
+        pNode->EstRefs = (float)pNode->nRefs;
+    else if ( Mode == 1 )
+        pNode->EstRefs = (float)((2.0 * pNode->EstRefs + pNode->nRefs) / 3.0);
+    else if ( Mode == 2 && pNode->nRefs > 0 )
+        Pga_CutDeref( p, pNode, pNode->Match.pCut );
+//    else if ( Mode == 3 && pNode->nRefs > 0 )
+//        Pga_CutDerefSwitch( p, pNode, pNode->Match.pCut );
+
+    // start the best match
+    pMatchBest->pCut = NULL;
+
+    // go through the other cuts
+    assert( pList->pNext );
+    for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
+    {
+        // compute match for this cut
+        if ( !Pga_MappingMatchCut( p, pNode, pCut, Mode, pMatchCur ) )
+            continue;
+        // compare matches
+        if ( !Pga_MappingCompareMatches( p, pMatchBest, pMatchCur, Mode ) )
+            continue;
+        // the best match should be updated
+        *pMatchBest = *pMatchCur;
+    }
+
+    // make sure the match is found
+    if ( pMatchBest->pCut != NULL )
+        pNode->Match = *pMatchBest;
+    else
+    {
+        assert( 0 );
+//        Pga_MappingMatchCut( p, pNode, pCut, Mode, pNode->Match );
+    }
+
+    // reference the best cut
+    if ( Mode == 2 && pNode->nRefs > 0 )
+        Pga_CutRef( p, pNode, pNode->Match.pCut );
+//    else if ( Mode == 3 && pNode->nRefs > 0 )
+//        Pga_CutRefSwitch( p, pNode, pNode->Match.pCut );
+    return 1;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/map/pga/pgaUtil.c

+/**CFile****************************************************************
+
+  FileName    [pgaUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapper.]
+
+  Synopsis    [Verious utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: pgaUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pgaInt.h"
+
+#define PGA_CO_LIST_SIZE  5
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the results of mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Pga_MappingResults( Pga_Man_t * p )
+{
+    Vec_Ptr_t * vResult;
+    Pga_Node_t * pNode;
+    int i;
+    vResult = Vec_PtrAlloc( 1000 );
+    Pga_ManForEachObjDirect( p, pNode, i )
+    {
+        // skip the CIs and nodes not used in the mapping
+        if ( !pNode->Match.pCut || !pNode->nRefs )
+            continue;
+        pNode->Match.pCut->uSign = pNode->Id;
+        Vec_PtrPush( vResult, pNode->Match.pCut );
+    }
+    return vResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the maximum arrival times.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Pga_TimeComputeArrivalMax( Pga_Man_t * p )
+{
+    Pga_Node_t * pNode;
+    float ArrivalMax;
+    int i;
+    ArrivalMax = -ABC_INFINITY;
+    Pga_ManForEachCoDriver( p, pNode, i )
+        ArrivalMax = ABC_MAX( ArrivalMax, pNode->Match.Delay );
+    return ArrivalMax;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes required times of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pga_MappingComputeRequired( Pga_Man_t * p )
+{
+    Pga_Node_t * pNode, * pFanin;
+    Cut_Cut_t * pCutBest;
+    float RequiredNew;
+    int i, k;
+    // clean the required times of all nodes
+    Pga_ManForEachObjDirect( p, pNode, i )
+        pNode->Required = ABC_INFINITY;
+    // get the global required times
+    p->AreaGlobal     = Pga_TimeComputeArrivalMax( p );
+    p->RequiredGlobal = ABC_MAX( p->AreaGlobal, p->RequiredUser );
+    // set the global required times of the CO drivers
+    Pga_ManForEachCoDriver( p, pNode, i )
+        pNode->Required = p->RequiredGlobal;
+    // propagate the required times in the reverse topological order
+    Pga_ManForEachObjReverse( p, pNode, i )
+    {
+        // skip the CIs and nodes not used in the mapping
+        if ( !pNode->Match.pCut || !pNode->nRefs )
+            continue;
+        // get the required time for children
+        pCutBest    = pNode->Match.pCut;
+        RequiredNew = pNode->Required - p->pLutDelays[pCutBest->nLeaves];
+        // update the required time of the children
+        for ( k = 0; k < (int)pCutBest->nLeaves; k++ )
+        {
+            pFanin = Pga_Node( p, pCutBest->pLeaves[k] );
+            pFanin->Required = ABC_MIN( pFanin->Required, RequiredNew );
+        }
+    }
+    // check that the required times does not contradict the arrival times
+    Pga_ManForEachObjDirect( p, pNode, i )
+        assert( !pNode->Match.pCut || pNode->Match.Delay < pNode->Required + p->Epsilon );
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets references and computes area for the current mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Pga_MappingSetRefsAndArea( Pga_Man_t * p )
+{
+    Pga_Node_t * pNode, * pFanin;
+    Cut_Cut_t * pCutBest;
+    float AreaTotal;
+    int i, k;
+    // clean all the references
+    Pga_ManForEachObjDirect( p, pNode, i )
+        pNode->nRefs = 0;
+    // set the references of the CO drivers
+    Pga_ManForEachCoDriver( p, pNode, i )
+        pNode->nRefs++;
+    // go through the nodes in the reverse order
+    AreaTotal = 0.0;
+    Pga_ManForEachObjReverse( p, pNode, i )
+    {
+        // skip the CIs and nodes not used in the mapping
+        if ( !pNode->Match.pCut || !pNode->nRefs )
+            continue;
+        // increate the reference count of the children
+        pCutBest   = pNode->Match.pCut;
+        AreaTotal += p->pLutAreas[pCutBest->nLeaves];
+        // update the required time of the children
+        for ( k = 0; k < (int)pCutBest->nLeaves; k++ )
+        {
+            pFanin = Pga_Node( p, pCutBest->pLeaves[k] );
+            pFanin->nRefs++;
+        }
+    }
+    return AreaTotal;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes switching activity of the mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Pga_MappingGetSwitching( Pga_Man_t * p )
+{
+    float Switching;
+    Pga_Node_t * pNode;
+    int i;
+    Switching = 0;
+    Pga_ManForEachObjDirect( p, pNode, i )
+    {
+        // skip the CIs and nodes not used in the mapping
+        if ( !pNode->Match.pCut || !pNode->nRefs )
+            continue;
+        Switching += pNode->Switching;
+    }
+    return Switching;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares the outputs by their arrival times.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pga_MappingCompareOutputDelay( Pga_Node_t ** ppNode1, Pga_Node_t ** ppNode2 )
+{
+    Pga_Node_t * pNode1 = *ppNode1;
+    Pga_Node_t * pNode2 = *ppNode2;
+    float Arrival1 = pNode1->Match.Delay;
+    float Arrival2 = pNode2->Match.Delay;
+    if ( Arrival1 < Arrival2 )
+        return -1;
+    if ( Arrival1 > Arrival2 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds given number of latest arriving COs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pga_MappingFindLatest( Pga_Man_t * p, int * pNodes, int nNodesMax )
+{
+    Pga_Node_t * pNodeI, * pNodeK;
+    Abc_Obj_t * pObjCo;
+    int nNodes, i, k, v;
+    assert( Abc_NtkCoNum(p->pParams->pNtk) >= nNodesMax );
+    pNodes[0] = 0;
+    nNodes = 1;
+//    for ( i = 1; i < p->nOutputs; i++ )
+    Pga_ManForEachCoDriver( p, pNodeI, i )
+    {
+        for ( k = nNodes - 1; k >= 0; k-- )
+        {
+            pObjCo = Abc_NtkCo( p->pParams->pNtk, pNodes[k] );
+            pNodeK = Pga_Node( p, Abc_ObjFaninId0(pObjCo) );
+            if ( Pga_MappingCompareOutputDelay( &pNodeK, &pNodeI ) >= 0 )
+                break;
+        }
+        if ( k == nNodesMax - 1 )
+            continue;
+        if ( nNodes < nNodesMax )
+            nNodes++;
+        for ( v = nNodes - 1; v > k+1; v-- )
+            pNodes[v] = pNodes[v-1];
+        pNodes[k+1] = i;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints a bunch of latest arriving outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pga_MappingPrintOutputArrivals( Pga_Man_t * p )
+{
+    int pSorted[PGA_CO_LIST_SIZE];
+    Abc_Ntk_t * pNtk = p->pParams->pNtk;
+    Abc_Obj_t * pObjCo;
+    Pga_Node_t * pNode;
+    int Limit, MaxNameSize, i;
+
+    // determine the number of nodes to print
+    Limit = (Abc_NtkCoNum(pNtk) < PGA_CO_LIST_SIZE)? Abc_NtkCoNum(pNtk) : PGA_CO_LIST_SIZE;
+
+    // determine the order
+    Pga_MappingFindLatest( p, pSorted, Limit );
+
+    // determine max size of the node's name
+    MaxNameSize = 0;
+    for ( i = 0; i < Limit; i++ )
+    {
+        pObjCo = Abc_NtkCo( pNtk, pSorted[i] );
+        if ( MaxNameSize < (int)strlen( Abc_ObjName(pObjCo) ) )
+            MaxNameSize = strlen( Abc_ObjName(pObjCo) );
+    }
+
+    // print the latest outputs
+    for ( i = 0; i < Limit; i++ )
+    {
+        // get the i-th latest output
+        pObjCo = Abc_NtkCo( pNtk, pSorted[i] );
+        pNode  = Pga_Node( p, pObjCo->Id );
+        // print out the best arrival time
+        printf( "Output  %-*s : ", MaxNameSize + 3, Abc_ObjName(pObjCo) );
+        printf( "Delay = %8.2f  ", (double)pNode->Match.Delay );
+        if ( Abc_ObjFaninC0(pObjCo) )
+            printf( "NEG" );
+        else
+            printf( "POS" );
+        printf( "\n" );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/misc/extra/extra.h

@@ -63,6 +63,15 @@
 /* Macro declarations                                                        */
 /*---------------------------------------------------------------------------*/
 
+typedef unsigned char      uint8;
+typedef unsigned short     uint16;
+typedef unsigned int       uint32;
+#ifdef WIN32
+typedef unsigned __int64   uint64;
+#else
+typedef unsigned long long uint64;
+#endif
+
 /* constants of the manager */
 #define     b0     Cudd_Not((dd)->one)
 #define     b1              (dd)->one

src/misc/vec/vecPtr.h

@@ -53,6 +53,10 @@ struct Vec_Ptr_t_
     for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
 #define Vec_PtrForEachEntryStart( vVec, pEntry, i, Start )                                   \
     for ( i = Start; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
+#define Vec_PtrForEachEntryStop( vVec, pEntry, i, Stop )                                     \
+    for ( i = 0; (i < Stop) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
+#define Vec_PtrForEachEntryStartStop( vVec, pEntry, i, Start, Stop )                         \
+    for ( i = Start; (i < Stop) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
 #define Vec_PtrForEachEntryReverse( vVec, pEntry, i )                                        \
     for ( i = Vec_PtrSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i-- )
 

src/opt/cut/cut.h

@@ -43,7 +43,6 @@ struct Cut_ParamsStruct_t_
     int  nKeepMax;      // the max number of cuts kept at a node
     int  nIdsMax;       // the max number of IDs of cut objects
     int  fTruth;        // compute truth tables
-    int  fHash;         // hash cuts to detect unique
     int  fFilter;       // filter dominated cuts
     int  fSeq;          // compute sequential cuts
     int  fDrop;         // drop cuts on the fly
@@ -53,28 +52,25 @@ struct Cut_ParamsStruct_t_
 struct Cut_CutStruct_t_
 {
     unsigned           uTruth     : 16;   // truth table for 4-input cuts
-    unsigned           uPhase     :  7;   // the phase when mapping into a canonical form
+    unsigned           uPhase     :  8;   // the phase when mapping into a canonical form
     unsigned           fSimul     :  1;   // the value of cut's output at 000.. pattern
     unsigned           fCompl     :  1;   // the cut is complemented
-    unsigned           fSeq       :  1;   // the cut is sequential
     unsigned           nVarsMax   :  3;   // the max number of vars [4-6]
     unsigned           nLeaves    :  3;   // the number of leaves [4-6]
+    unsigned           uSign;             // the signature
     Cut_Cut_t *        pNext;             // the next cut in the list
-    void *             pData;             // the user data
     int                pLeaves[0];        // the array of leaves
 };
 
-static inline unsigned * Cut_CutReadTruth( Cut_Cut_t * p )     {  if ( p->nVarsMax == 4 )  return (unsigned *)p;  return (unsigned *)(p->pLeaves + p->nVarsMax + p->fSeq); }
+static inline unsigned * Cut_CutReadTruth( Cut_Cut_t * p )     {  if ( p->nVarsMax == 4 )  return (unsigned *)p;  return (unsigned *)(p->pLeaves + p->nVarsMax); }
 static inline unsigned   Cut_CutReadPhase( Cut_Cut_t * p )     {  return p->uPhase;    }
 static inline int        Cut_CutReadLeaveNum( Cut_Cut_t * p )  {  return p->nLeaves;   }
 static inline int *      Cut_CutReadLeaves( Cut_Cut_t * p )    {  return p->pLeaves;   }
-static inline void *     Cut_CutReadData( Cut_Cut_t * p )      {  return p->pData;     }
 
-static inline void       Cut_CutWriteData( Cut_Cut_t * p, void * pData )  { p->pData = pData;  }
 static inline void       Cut_CutWriteTruth( Cut_Cut_t * p, unsigned * puTruth )  { 
     if ( p->nVarsMax == 4 )  { p->uTruth = *puTruth;  return; }
-    p->pLeaves[p->nVarsMax + p->fSeq] = (int)puTruth[0];
-    if ( p->nVarsMax == 6 )  p->pLeaves[p->nVarsMax + p->fSeq + 1] = (int)puTruth[1];
+    p->pLeaves[p->nVarsMax] = (int)puTruth[0];
+    if ( p->nVarsMax == 6 )  p->pLeaves[p->nVarsMax + 1] = (int)puTruth[1];
 }
 
 ////////////////////////////////////////////////////////////////////////
@@ -85,21 +81,23 @@ static inline void       Cut_CutWriteTruth( Cut_Cut_t * p, unsigned * puTruth )
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== cutApi.c ==========================================================*/
+extern Cut_Cut_t *      Cut_NodeReadCuts( Cut_Man_t * p, int Node );
+extern void             Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList );
+extern void             Cut_NodeSetTriv( Cut_Man_t * p, int Node );
+extern void             Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node );
+extern void             Cut_NodeFreeCuts( Cut_Man_t * p, int Node );
+/*=== cutCut.c ==========================================================*/
+extern void             Cut_CutPrint( Cut_Cut_t * pCut );
 /*=== cutMan.c ==========================================================*/
 extern Cut_Man_t *      Cut_ManStart( Cut_Params_t * pParams );
 extern void             Cut_ManStop( Cut_Man_t * p );
 extern void             Cut_ManPrintStats( Cut_Man_t * p );
 extern void             Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts );
+extern int              Cut_ManReadVarsMax( Cut_Man_t * p );
 /*=== cutNode.c ==========================================================*/
-extern void             Cut_NodeSetTriv( Cut_Man_t * p, int Node );
 extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 ); 
 extern Cut_Cut_t *      Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes );
-extern Cut_Cut_t *      Cut_NodeReadCuts( Cut_Man_t * p, int Node ); 
-extern void             Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList );
-extern void             Cut_NodeFreeCuts( Cut_Man_t * p, int Node );
-extern void             Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node );
-extern void             Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node );
-extern void             Cut_CutPrint( Cut_Cut_t * pCut );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/opt/cut/cutApi.c

+/**CFile****************************************************************
+
+  FileName    [cutNode.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [Procedures to compute cuts for a node.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutNode.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the pointer to the linked list of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node )
+{
+    if ( Node >= p->vCuts->nSize )
+        return NULL;
+    return Vec_PtrEntry( p->vCuts, Node );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the pointer to the linked list of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList )
+{
+    Vec_PtrWriteEntry( p->vCuts, Node, pList );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the trivial cut for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeSetTriv( Cut_Man_t * p, int Node )
+{
+    assert( Cut_NodeReadCuts(p, Node) == NULL );
+    Cut_NodeWriteCuts( p, Node, Cut_CutCreateTriv(p, Node) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Consider dropping cuts if they are useless by now.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node )
+{
+    int nFanouts;
+    assert( p->vFanCounts );
+    nFanouts = Vec_IntEntry( p->vFanCounts, Node );
+    assert( nFanouts > 0 );
+    if ( --nFanouts == 0 )
+        Cut_NodeFreeCuts( p, Node );
+    Vec_IntWriteEntry( p->vFanCounts, Node, nFanouts );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the cuts at the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeFreeCuts( Cut_Man_t * p, int Node )
+{
+    Cut_Cut_t * pList, * pCut, * pCut2;
+    pList = Cut_NodeReadCuts( p, Node );
+    if ( pList == NULL )
+        return;
+    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+        Cut_CutRecycle( p, pCut );
+    Cut_NodeWriteCuts( p, Node, NULL );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/cut/cutCut.c

+/**CFile****************************************************************
+
+  FileName    [cutNode.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [Procedures to compute cuts for a node.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutNode.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start the cut computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p )
+{
+    Cut_Cut_t * pCut;
+    // cut allocation
+    pCut = (Cut_Cut_t *)Extra_MmFixedEntryFetch( p->pMmCuts );
+    memset( pCut, 0, sizeof(Cut_Cut_t) );
+    pCut->nVarsMax   = p->pParams->nVarsMax;
+    pCut->fSimul     = p->fSimul;
+    // statistics
+    p->nCutsAlloc++;
+    p->nCutsCur++;
+    if ( p->nCutsPeak < p->nCutsAlloc - p->nCutsDealloc )
+        p->nCutsPeak = p->nCutsAlloc - p->nCutsDealloc;
+    return pCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Start the cut computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
+{
+    Cut_Cut_t * pCut;
+    pCut = Cut_CutAlloc( p );
+    pCut->nLeaves    = 1;
+    pCut->pLeaves[0] = Node;
+    pCut->uSign      = (1 << (Node % 32));
+    if ( p->pParams->fTruth )
+        Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
+    p->nCutsTriv++;
+    return pCut;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Start the cut computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut )
+{
+    p->nCutsDealloc++;
+    p->nCutsCur--;
+    if ( pCut->nLeaves == 1 )
+        p->nCutsTriv--;
+    Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Print the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CutPrint( Cut_Cut_t * pCut )
+{
+    int i;
+    assert( pCut->nLeaves > 0 );
+    printf( "%d : {", pCut->nLeaves );
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        printf( " %d", pCut->pLeaves[i] );
+    printf( " }" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Consider dropping cuts if they are useless by now.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+    printf( "\n" );
+    printf( "%d : %5d %5d %5d %5d %5d\n", 
+        pCut0->nLeaves, 
+        pCut0->nLeaves > 0 ? pCut0->pLeaves[0] : -1, 
+        pCut0->nLeaves > 1 ? pCut0->pLeaves[1] : -1, 
+        pCut0->nLeaves > 2 ? pCut0->pLeaves[2] : -1, 
+        pCut0->nLeaves > 3 ? pCut0->pLeaves[3] : -1, 
+        pCut0->nLeaves > 4 ? pCut0->pLeaves[4] : -1
+        );
+    printf( "%d : %5d %5d %5d %5d %5d\n", 
+        pCut1->nLeaves, 
+        pCut1->nLeaves > 0 ? pCut1->pLeaves[0] : -1, 
+        pCut1->nLeaves > 1 ? pCut1->pLeaves[1] : -1, 
+        pCut1->nLeaves > 2 ? pCut1->pLeaves[2] : -1, 
+        pCut1->nLeaves > 3 ? pCut1->pLeaves[3] : -1, 
+        pCut1->nLeaves > 4 ? pCut1->pLeaves[4] : -1
+        );
+    if ( pCut == NULL )
+        printf( "Cannot merge\n" );
+    else
+        printf( "%d : %5d %5d %5d %5d %5d\n", 
+            pCut->nLeaves, 
+            pCut->nLeaves > 0 ? pCut->pLeaves[0] : -1, 
+            pCut->nLeaves > 1 ? pCut->pLeaves[1] : -1, 
+            pCut->nLeaves > 2 ? pCut->pLeaves[2] : -1, 
+            pCut->nLeaves > 3 ? pCut->pLeaves[3] : -1, 
+            pCut->nLeaves > 4 ? pCut->pLeaves[4] : -1
+            );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/cut/cutInt.h

@@ -48,7 +48,6 @@ struct Cut_ManStruct_t_
     // storage for cuts
     Vec_Ptr_t *        vCuts;            // cuts by ID
     Vec_Ptr_t *        vCutsNew;         // cuts by ID
-    Cut_HashTable_t *  tTable;           // cuts by their leaves (and root)
     // memory management
     Extra_MmFixed_t *  pMmCuts;
     int                EntrySize;
@@ -58,6 +57,7 @@ struct Cut_ManStruct_t_
     int                fCompl0;
     int                fCompl1;
     int                fSimul;
+    int                nNodeCuts;
     // precomputations
     unsigned           uTruthVars[6][2];
     unsigned short **  pPerms43;
@@ -69,7 +69,8 @@ struct Cut_ManStruct_t_
     int                nCutsDealloc;
     int                nCutsPeak;
     int                nCutsTriv;
-    int                nCutsNode;
+    int                nCutsFilter;
+    int                nCutsLimit;
     int                nNodes;
     // runtime
     int                timeMerge;
@@ -79,6 +80,22 @@ struct Cut_ManStruct_t_
     int                timeHash;
 };
 
+// iterator through all the cuts of the list
+#define Cut_ListForEachCut( pList, pCut )                 \
+    for ( pCut = pList;                                   \
+          pCut;                                           \
+          pCut = pCut->pNext )
+#define Cut_ListForEachCutStop( pList, pCut, pStop )      \
+    for ( pCut = pList;                                   \
+          pCut != pStop;                                  \
+          pCut = pCut->pNext )
+#define Cut_ListForEachCutSafe( pList, pCut, pCut2 )      \
+    for ( pCut = pList,                                   \
+          pCut2 = pCut? pCut->pNext: NULL;                \
+          pCut;                                           \
+          pCut = pCut2,                                   \
+          pCut2 = pCut? pCut->pNext: NULL )
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
@@ -87,10 +104,14 @@ struct Cut_ManStruct_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== cutCut.c ==========================================================*/
+extern Cut_Cut_t *         Cut_CutAlloc( Cut_Man_t * p );
+extern Cut_Cut_t *         Cut_CutCreateTriv( Cut_Man_t * p, int Node );
+extern void                Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut );
+extern void                Cut_CutPrint( Cut_Cut_t * pCut );
+extern void                Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
 /*=== cutMerge.c ==========================================================*/
 extern Cut_Cut_t *         Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
-/*=== cutNode.c ==========================================================*/
-extern Cut_Cut_t *         Cut_CutAlloc( Cut_Man_t * p );
 /*=== cutTable.c ==========================================================*/
 extern Cut_HashTable_t *   Cut_TableStart( int Size );
 extern void                Cut_TableStop( Cut_HashTable_t * pTable );

src/opt/cut/cutMan.c

@@ -49,7 +49,7 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
     // set and correct parameters
     p->pParams = pParams;
     if ( p->pParams->fSeq )
-        p->pParams->fHash = 1;
+        p->pParams->fFilter = 1;
     // space for cuts
     p->vCuts = Vec_PtrAlloc( pParams->nIdsMax );
     Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
@@ -58,25 +58,17 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
         p->vCutsNew = Vec_PtrAlloc( pParams->nIdsMax );
         Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
     }
-    // hash tables
-    if ( pParams->fHash )
-        p->tTable = Cut_TableStart( p->pParams->nKeepMax );
     // entry size
     p->EntrySize = sizeof(Cut_Cut_t) + (pParams->nVarsMax + pParams->fSeq) * sizeof(int);
-    if ( pParams->nVarsMax == 5 )
-        p->EntrySize += sizeof(unsigned);
-    else if ( pParams->nVarsMax == 6 )
-        p->EntrySize += 2 * sizeof(unsigned);
+    if ( pParams->fTruth )
+    {
+        if ( pParams->nVarsMax == 5 )
+            p->EntrySize += sizeof(unsigned);
+        else if ( pParams->nVarsMax == 6 )
+            p->EntrySize += 2 * sizeof(unsigned);
+    }
     // memory for cuts
     p->pMmCuts = Extra_MmFixedStart( p->EntrySize );
-    // precomputations
-//    if ( pParams->fTruth && pParams->nVarsMax == 4 )
-//        p->pPerms43 = Extra_TruthPerm43();
-//    else if ( pParams->fTruth )
-//    {
-//        p->pPerms53 = Extra_TruthPerm53();
-//        p->pPerms54 = Extra_TruthPerm54();
-//    }
     p->uTruthVars[0][1] = p->uTruthVars[0][0] = 0xAAAAAAAA;    // 1010 1010 1010 1010 1010 1010 1010 1010
     p->uTruthVars[1][1] = p->uTruthVars[1][0] = 0xCCCCCCCC;    // 1010 1010 1010 1010 1010 1010 1010 1010
     p->uTruthVars[2][1] = p->uTruthVars[2][0] = 0xF0F0F0F0;    // 1111 0000 1111 0000 1111 0000 1111 0000
@@ -104,13 +96,10 @@ void Cut_ManStop( Cut_Man_t * p )
     Cut_Cut_t * pCut;
     int i;
     Vec_PtrForEachEntry( p->vCuts, pCut, i )
-    {
         if ( pCut != NULL )
         {
             int k = 0;
         }
-    }
-
     if ( p->vCutsNew )   Vec_PtrFree( p->vCutsNew );
     if ( p->vCuts )      Vec_PtrFree( p->vCuts );
     if ( p->vFanCounts ) Vec_IntFree( p->vFanCounts );
@@ -118,7 +107,6 @@ void Cut_ManStop( Cut_Man_t * p )
     if ( p->pPerms53 )   free( p->pPerms53 );
     if ( p->pPerms54 )   free( p->pPerms54 );
     if ( p->vTemp )      Vec_PtrFree( p->vTemp );
-    if ( p->tTable )     Cut_TableStop( p->tTable );
     Extra_MmFixedStop( p->pMmCuts, 0 );
     free( p );
 }
@@ -141,12 +129,13 @@ void Cut_ManPrintStats( Cut_Man_t * p )
     printf( "Peak cuts         = %8d.\n", p->nCutsPeak );
     printf( "Total allocated   = %8d.\n", p->nCutsAlloc );
     printf( "Total deallocated = %8d.\n", p->nCutsDealloc );
+    printf( "Cuts filtered     = %8d.\n", p->nCutsFilter );
+    printf( "Nodes with limit  = %8d.\n", p->nCutsLimit );
     printf( "Cuts per node     = %8.1f\n", ((float)(p->nCutsCur-p->nCutsTriv))/p->nNodes );
     printf( "The cut size      = %8d bytes.\n", p->EntrySize );
     printf( "Peak memory       = %8.2f Mb.\n", (float)p->nCutsPeak * p->EntrySize / (1<<20) );
     PRT( "Merge ", p->timeMerge );
     PRT( "Union ", p->timeUnion );
-    PRT( "Hash  ", Cut_TableReadTime(p->tTable) );
     PRT( "Filter", p->timeFilter );
     PRT( "Truth ", p->timeTruth );
 }
@@ -168,6 +157,22 @@ void Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts )
     p->vFanCounts = vFanCounts;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_ManReadVarsMax( Cut_Man_t * p )
+{
+    return p->pParams->nVarsMax;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/opt/cut/cutNode.c

@@ -25,36 +25,13 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node );
-static inline void        Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut );
-static inline int         Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList );
-
-static void               Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
-static void               Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList );
-
-// iterator through all the cuts of the list
-#define Cut_ListForEachCut( pList, pCut )                 \
-    for ( pCut = pList;                                   \
-          pCut;                                           \
-          pCut = pCut->pNext )
-#define Cut_ListForEachCutStop( pList, pCut, pStop )      \
-    for ( pCut = pList;                                   \
-          pCut != pStop;                                  \
-          pCut = pCut->pNext )
-#define Cut_ListForEachCutSafe( pList, pCut, pCut2 )      \
-    for ( pCut = pList,                                   \
-          pCut2 = pCut? pCut->pNext: NULL;                \
-          pCut;                                           \
-          pCut = pCut2,                                   \
-          pCut2 = pCut? pCut->pNext: NULL )
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the pointer to the linked list of cuts.]
+  Synopsis    [Returns 1 if pDom is contained in pCut.]
 
   Description []
                
@@ -63,49 +40,96 @@ static void               Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList );
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node )
+static inline int Cut_CutCheckDominance( Cut_Cut_t * pDom, Cut_Cut_t * pCut )
 {
-    if ( Node >= p->vCuts->nSize )
-        return NULL;
-    return Vec_PtrEntry( p->vCuts, Node );
+    int i, k;
+    for ( i = 0; i < (int)pDom->nLeaves; i++ )
+    {
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+            if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
+                break;
+        if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
+            return 0;
+    }
+    // every node in pDom is contained in pCut
+    return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the pointer to the linked list of cuts.]
+  Synopsis    [Checks containment for one cut.]
 
-  Description []
+  Description [Returns 1 if the cut is removed.]
                
-  SideEffects []
+  SideEffects [May remove other cuts in the set.]
 
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList )
+static inline int Cut_CutFilterOne( Cut_Man_t * p, Cut_List_t * pSuperList, Cut_Cut_t * pCut )
 {
-    Vec_PtrWriteEntry( p->vCuts, Node, pList );
-}
+    Cut_Cut_t * pTemp, * pTemp2, ** ppTail;
+    int a;
 
-/**Function*************************************************************
-
-  Synopsis    [Sets the trivial cut for the node.]
-
-  Description []
-               
-  SideEffects []
+    // check if this cut is filtered out by smaller cuts
+    for ( a = 2; a <= (int)pCut->nLeaves; a++ )
+    {
+        Cut_ListForEachCut( pSuperList->pHead[a], pTemp )
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
+                continue;
+            // check containment seriously
+            if ( Cut_CutCheckDominance( pTemp, pCut ) )
+            {
+                p->nCutsFilter++;
+                Cut_CutRecycle( p, pCut );
+                return 1;
+            }
+        }
+    }
 
-  SeeAlso     []
+    // filter out other cuts using this one
+    for ( a = pCut->nLeaves + 1; a <= (int)pCut->nVarsMax; a++ )
+    {
+        ppTail = pSuperList->pHead + a;
+        Cut_ListForEachCutSafe( pSuperList->pHead[a], pTemp, pTemp2 )
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
+            {
+                ppTail = &pTemp->pNext;
+                continue;
+            }
+            // check containment seriously
+            if ( Cut_CutCheckDominance( pCut, pTemp ) )
+            {
+                p->nCutsFilter++;
+                p->nNodeCuts--;
+                // move the head
+                if ( pSuperList->pHead[a] == pTemp )
+                    pSuperList->pHead[a] = pTemp->pNext;
+                // move the tail
+                if ( pSuperList->ppTail[a] == &pTemp->pNext )
+                    pSuperList->ppTail[a] = ppTail;
+                // skip the given cut in the list
+                *ppTail = pTemp->pNext;
+                // recycle pTemp
+                Cut_CutRecycle( p, pTemp );
+            }
+            else
+                ppTail = &pTemp->pNext;
+        }
+        assert( ppTail == pSuperList->ppTail[a] );
+        assert( *ppTail == NULL );
+    }
 
-***********************************************************************/
-void Cut_NodeSetTriv( Cut_Man_t * p, int Node )
-{
-    assert( Cut_NodeReadCuts(p, Node) == NULL );
-    Cut_NodeWriteCuts( p, Node, Cut_CutCreateTriv(p, Node) );
+    return 0;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Deallocates the cuts at the node.]
+  Synopsis    [Filters cuts using dominance.]
 
   Description []
                
@@ -114,31 +138,79 @@ void Cut_NodeSetTriv( Cut_Man_t * p, int Node )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_NodeFreeCuts( Cut_Man_t * p, int Node )
-{
-    Cut_Cut_t * pList, * pCut, * pCut2;
-    pList = Cut_NodeReadCuts( p, Node );
-    if ( pList == NULL )
-        return;
-    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
-        Cut_CutRecycle( p, pCut );
-    Cut_NodeWriteCuts( p, Node, NULL );
+static inline void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList )
+{ 
+    Cut_Cut_t * pListR, ** ppListR = &pListR;
+    Cut_Cut_t * pCut, * pCut2, * pDom, * pPrev;
+    // save the first cut
+    *ppListR = pList, ppListR = &pList->pNext;
+    // try to filter out other cuts
+    pPrev = pList;
+    Cut_ListForEachCutSafe( pList->pNext, pCut, pCut2 )
+    {
+        assert( pCut->nLeaves > 1 );
+        // go through all the previous cuts up to pCut
+        Cut_ListForEachCutStop( pList->pNext, pDom, pCut )
+        {
+            if ( pDom->nLeaves > pCut->nLeaves )
+                continue;
+            if ( (pDom->uSign & pCut->uSign) != pDom->uSign )
+                continue;
+            if ( Cut_CutCheckDominance( pDom, pCut ) )
+                break;
+        }
+        if ( pDom != pCut ) // pDom is contained in pCut - recycle pCut
+        {
+            // make sure cuts are connected after removing
+            pPrev->pNext = pCut->pNext;
+            // recycle the cut
+            Cut_CutRecycle( p, pCut );
+        }
+        else // pDom is NOT contained in pCut - save pCut
+        {
+            *ppListR = pCut, ppListR = &pCut->pNext;
+            pPrev = pCut;
+        }
+    }
+    *ppListR = NULL;
 }
 
-
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Processes two cuts.]
 
-  Description []
+  Description [Returns 1 if the limit has been reached.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node )
+static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList )
 {
+    Cut_Cut_t * pCut;
+    int RetValue;
+    // merge the cuts
+    if ( pCut0->nLeaves >= pCut1->nLeaves )
+        pCut = Cut_CutMergeTwo( p, pCut0, pCut1 );
+    else
+        pCut = Cut_CutMergeTwo( p, pCut1, pCut0 );
+    if ( pCut == NULL )
+        return 0;
+    assert( pCut->nLeaves > 1 );
+    // set the signature
+    pCut->uSign = pCut0->uSign | pCut1->uSign;
+    // check containment
+    RetValue = p->pParams->fFilter && Cut_CutFilterOne( p, pSuperList, pCut );
+    if ( RetValue )
+        return 0;
+    // compute the truth table
+    if ( p->pParams->fTruth )
+        Cut_TruthCompute( p, pCut, pCut0, pCut1 );
+    // add to the list
+    Cut_ListAdd( pSuperList, pCut );
+    // return status (0 if okay; 1 if exceeded the limit)
+    return ++p->nNodeCuts == p->pParams->nKeepMax;
 }
 
 /**Function*************************************************************
@@ -159,6 +231,7 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
     int i, Limit = p->pParams->nVarsMax;
     int clk = clock();
     assert( p->pParams->nVarsMax <= 6 );
+
     // start the new list
     Cut_ListStart( &SuperList );
     // get the cut lists of children
@@ -180,27 +253,37 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
     // start with the elementary cut
     pTemp0 = Cut_CutCreateTriv( p, Node );
     Cut_ListAdd( &SuperList, pTemp0 );
-    p->nCutsNode = 1;
+    p->nNodeCuts = 1;
     // small by small
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
         if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
             goto finish;
-    // all by large
-    Cut_ListForEachCut( pList0, pTemp0 )
+    // small by large
+    Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCut( pStop1, pTemp1 )
+    {
+        if ( (pTemp0->uSign & pTemp1->uSign) != pTemp0->uSign )
+            continue;
         if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
             goto finish;
-    // all by large
-    Cut_ListForEachCut( pList1, pTemp1 )
+    }
+    // small by large
+    Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
     Cut_ListForEachCut( pStop0, pTemp0 )
+    {
+        if ( (pTemp0->uSign & pTemp1->uSign) != pTemp1->uSign )
+            continue;
         if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
             goto finish;
+    }
     // large by large
     Cut_ListForEachCut( pStop0, pTemp0 )
     Cut_ListForEachCut( pStop1, pTemp1 )
     {
         assert( pTemp0->nLeaves == (unsigned)Limit && pTemp1->nLeaves == (unsigned)Limit );
+        if ( pTemp0->uSign != pTemp1->uSign )
+            continue;
         for ( i = 0; i < Limit; i++ )
             if ( pTemp0->pLeaves[i] != pTemp1->pLeaves[i] )
                 break;
@@ -210,14 +293,13 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
             goto finish;
     }
 finish :
+    if ( p->nNodeCuts == p->pParams->nKeepMax )
+        p->nCutsLimit++;
     // set the list at the node
     Vec_PtrFillExtra( p->vCuts, Node + 1, NULL );
     assert( Cut_NodeReadCuts(p, Node) == NULL );
     pList0 = Cut_ListFinish( &SuperList );
     Cut_NodeWriteCuts( p, Node, pList0 );
-    // clear the hash table
-    if ( p->pParams->fHash && !p->pParams->fSeq )
-        Cut_TableClear( p->tTable );
     // consider dropping the fanins cuts
     if ( p->pParams->fDrop )
     {
@@ -227,8 +309,8 @@ finish :
 p->timeMerge += clock() - clk;
     // filter the cuts
 clk = clock();
-    if ( p->pParams->fFilter )
-        Cut_CutFilter( p, pList0 );
+//    if ( p->pParams->fFilter )
+//        Cut_CutFilter( p, pList0 );
 p->timeFilter += clock() - clk;
     p->nNodes++;
     return pList0;
@@ -236,46 +318,6 @@ p->timeFilter += clock() - clk;
 
 /**Function*************************************************************
 
-  Synopsis    [Processes two cuts.]
-
-  Description [Returns 1 if the limit has been reached.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList )
-{
-    Cut_Cut_t * pCut;
-    // merge the cuts
-    if ( pCut0->nLeaves >= pCut1->nLeaves )
-        pCut = Cut_CutMergeTwo( p, pCut0, pCut1 );
-    else
-        pCut = Cut_CutMergeTwo( p, pCut1, pCut0 );
-    if ( pCut == NULL )
-        return 0;
-    assert( pCut->nLeaves > 1 );
-    // add the root if sequential
-    if ( p->pParams->fSeq )
-        pCut->pLeaves[pCut->nLeaves] = Root;
-    // check the lookup table
-    if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq  ) )
-    {
-        Cut_CutRecycle( p, pCut );
-        return 0;
-    }
-    // compute the truth table
-    if ( p->pParams->fTruth )
-        Cut_TruthCompute( p, pCut, pCut0, pCut1 );
-    // add to the list
-    Cut_ListAdd( pSuperList, pCut );
-    // return status (0 if okay; 1 if exceeded the limit)
-    return ++p->nCutsNode == p->pParams->nKeepMax;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Computes the cuts by unioning cuts at a choice node.]
 
   Description []
@@ -299,7 +341,7 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
 
     // remember the root node to save the resulting cuts
     Root = Vec_IntEntry( vNodes, 0 );
-    p->nCutsNode = 1;
+    p->nNodeCuts = 1;
 
     // collect small cuts first
     Vec_PtrClear( p->vTemp );
@@ -311,6 +353,7 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
         assert( pList );
         // remember the starting point
         pListStart = pList->pNext;
+        pList->pNext = NULL;
         // save or recycle the elementary cut
         if ( i == 0 )
             Cut_ListAdd( &SuperList, pList ), pTop = pList;
@@ -324,20 +367,19 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
                 Vec_PtrPush( p->vTemp, pCut );
                 break;
             }
-            // check hash tables
-            if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq ) )
-            {
-                Cut_CutRecycle( p, pCut );
+            // check containment
+            if ( p->pParams->fFilter && Cut_CutFilterOne( p, &SuperList, pCut ) )
                 continue;
-            }
             // set the complemented bit by comparing the first cut with the current cut
             pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+            pListStart = pCut->pNext;
+            pCut->pNext = NULL;
             // add to the list
             Cut_ListAdd( &SuperList, pCut );
-            if ( ++p->nCutsNode == p->pParams->nKeepMax )
+            if ( ++p->nNodeCuts == p->pParams->nKeepMax )
             {
                 // recycle the rest of the cuts of this node
-                Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 )
+                Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
                     Cut_CutRecycle( p, pCut );
                 // recycle all cuts of other nodes
                 Vec_IntForEachEntryStart( vNodes, Node, k, i+1 )
@@ -349,25 +391,25 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
                 goto finish;
             }
         }
-    }
+    } 
     // collect larger cuts next
     Vec_PtrForEachEntry( p->vTemp, pList, i )
     {
         Cut_ListForEachCutSafe( pList, pCut, pCut2 )
         {
-            if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq  ) )
-            {
-                Cut_CutRecycle( p, pCut );
+            // check containment
+            if ( p->pParams->fFilter && Cut_CutFilterOne( p, &SuperList, pCut ) )
                 continue;
-            }
             // set the complemented bit
             pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+            pListStart = pCut->pNext;
+            pCut->pNext = NULL;
             // add to the list
             Cut_ListAdd( &SuperList, pCut );
-            if ( ++p->nCutsNode == p->pParams->nKeepMax )
+            if ( ++p->nNodeCuts == p->pParams->nKeepMax )
             {
                 // recycle the rest of the cuts
-                Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 )
+                Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
                     Cut_CutRecycle( p, pCut );
                 // recycle the saved cuts of other nodes
                 Vec_PtrForEachEntryStart( p->vTemp, pList, k, i+1 )
@@ -382,244 +424,16 @@ finish :
     assert( Cut_NodeReadCuts(p, Root) == NULL );
     pList = Cut_ListFinish( &SuperList );
     Cut_NodeWriteCuts( p, Root, pList );
-    // clear the hash table
-    if ( p->pParams->fHash && !p->pParams->fSeq )
-        Cut_TableClear( p->tTable );
 p->timeUnion += clock() - clk;
     // filter the cuts
 clk = clock();
-    if ( p->pParams->fFilter )
-        Cut_CutFilter( p, pList );
+//    if ( p->pParams->fFilter )
+//        Cut_CutFilter( p, pList );
 p->timeFilter += clock() - clk;
     p->nNodes -= vNodes->nSize - 1;
     return pList;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Start the cut computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p )
-{
-    Cut_Cut_t * pCut;
-    // cut allocation
-    pCut = (Cut_Cut_t *)Extra_MmFixedEntryFetch( p->pMmCuts );
-    memset( pCut, 0, sizeof(Cut_Cut_t) );
-    pCut->nVarsMax   = p->pParams->nVarsMax;
-    pCut->fSeq       = p->pParams->fSeq;
-    pCut->fSimul     = p->fSimul;
-    // statistics
-    p->nCutsAlloc++;
-    p->nCutsCur++;
-    if ( p->nCutsPeak < p->nCutsAlloc - p->nCutsDealloc )
-        p->nCutsPeak = p->nCutsAlloc - p->nCutsDealloc;
-    return pCut;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Start the cut computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
-{
-    Cut_Cut_t * pCut;
-    pCut = Cut_CutAlloc( p );
-    pCut->nLeaves = 1;
-    pCut->pLeaves[0] = Node;
-    if ( p->pParams->fTruth )
-        Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
-    p->nCutsTriv++;
-    return pCut;
-} 
-
-/**Function*************************************************************
-
-  Synopsis    [Start the cut computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut )
-{
-    p->nCutsDealloc++;
-    p->nCutsCur--;
-    if ( pCut->nLeaves == 1 )
-        p->nCutsTriv--;
-    Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Consider dropping cuts if they are useless by now.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node )
-{
-    int nFanouts;
-    assert( p->vFanCounts );
-    nFanouts = Vec_IntEntry( p->vFanCounts, Node );
-    assert( nFanouts > 0 );
-    if ( --nFanouts == 0 )
-        Cut_NodeFreeCuts( p, Node );
-    Vec_IntWriteEntry( p->vFanCounts, Node, nFanouts );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Print the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CutPrint( Cut_Cut_t * pCut )
-{
-    int i;
-    assert( pCut->nLeaves > 0 );
-    printf( "%d : {", pCut->nLeaves );
-    for ( i = 0; i < (int)pCut->nLeaves; i++ )
-        printf( " %d", pCut->pLeaves[i] );
-    printf( " }" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Consider dropping cuts if they are useless by now.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
-{
-    printf( "\n" );
-    printf( "%d : %5d %5d %5d %5d %5d\n", 
-        pCut0->nLeaves, 
-        pCut0->nLeaves > 0 ? pCut0->pLeaves[0] : -1, 
-        pCut0->nLeaves > 1 ? pCut0->pLeaves[1] : -1, 
-        pCut0->nLeaves > 2 ? pCut0->pLeaves[2] : -1, 
-        pCut0->nLeaves > 3 ? pCut0->pLeaves[3] : -1, 
-        pCut0->nLeaves > 4 ? pCut0->pLeaves[4] : -1
-        );
-    printf( "%d : %5d %5d %5d %5d %5d\n", 
-        pCut1->nLeaves, 
-        pCut1->nLeaves > 0 ? pCut1->pLeaves[0] : -1, 
-        pCut1->nLeaves > 1 ? pCut1->pLeaves[1] : -1, 
-        pCut1->nLeaves > 2 ? pCut1->pLeaves[2] : -1, 
-        pCut1->nLeaves > 3 ? pCut1->pLeaves[3] : -1, 
-        pCut1->nLeaves > 4 ? pCut1->pLeaves[4] : -1
-        );
-    if ( pCut == NULL )
-        printf( "Cannot merge\n" );
-    else
-        printf( "%d : %5d %5d %5d %5d %5d\n", 
-            pCut->nLeaves, 
-            pCut->nLeaves > 0 ? pCut->pLeaves[0] : -1, 
-            pCut->nLeaves > 1 ? pCut->pLeaves[1] : -1, 
-            pCut->nLeaves > 2 ? pCut->pLeaves[2] : -1, 
-            pCut->nLeaves > 3 ? pCut->pLeaves[3] : -1, 
-            pCut->nLeaves > 4 ? pCut->pLeaves[4] : -1
-            );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Filter the cuts using dominance.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList )
-{ 
-    Cut_Cut_t * pListR, ** ppListR = &pListR;
-    Cut_Cut_t * pCut, * pCut2, * pDom, * pPrev;
-    int i, k;
-    // save the first cut
-    *ppListR = pList, ppListR = &pList->pNext;
-    // try to filter out other cuts
-    pPrev = pList;
-    Cut_ListForEachCutSafe( pList->pNext, pCut, pCut2 )
-    {
-        assert( pCut->nLeaves > 1 );
-        // go through all the previous cuts up to pCut
-        Cut_ListForEachCutStop( pList->pNext, pDom, pCut )
-        {
-            if ( pDom->nLeaves >= pCut->nLeaves )
-                continue;
-            // check if every node in pDom is contained in pCut
-            for ( i = 0; i < (int)pDom->nLeaves; i++ )
-            {
-                for ( k = 0; k < (int)pCut->nLeaves; k++ )
-                    if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
-                        break;
-                if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
-                    break;
-            }
-            if ( i == (int)pDom->nLeaves ) // every node in pDom is contained in pCut
-                break;
-        }
-        if ( pDom != pCut ) // pDom is contained in pCut - recycle pCut
-        {
-            // make sure cuts are connected after removing
-            pPrev->pNext = pCut->pNext;
-/*
-            // report
-            printf( "Recycling cut:   " );
-            Cut_CutPrint( pCut );
-            printf( "\n" );
-            printf( "As contained in: " );
-            Cut_CutPrint( pDom );
-            printf( "\n" );
-*/
-            // recycle the cut
-            Cut_CutRecycle( p, pCut );
-        }
-        else // pDom is NOT contained in pCut - save pCut
-        {
-            *ppListR = pCut, ppListR = &pCut->pNext;
-            pPrev = pCut;
-        }
-    }
-    *ppListR = NULL;
-}
-
-
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/opt/cut/cutTable.c

-/**CFile****************************************************************
-
-  FileName    [cutTable.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [K-feasible cut computation package.]
-
-  Synopsis    [Hashing cuts to prevent duplication.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: cutTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cutInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-struct Cut_HashTableStruct_t_
-{
-    int                  nBins;
-    Cut_Cut_t **         pBins;
-    int                  nEntries;
-    int *                pPlaces;
-    int                  nPlaces;
-    int                  timeLookup;
-};
-
-// iterator through all the cuts of the list
-#define Cut_TableListForEachCut( pList, pCut )               \
-    for ( pCut = pList;                                      \
-          pCut;                                              \
-          pCut = pCut->pData )
-#define Cut_TableListForEachCutSafe( pList, pCut, pCut2 )    \
-    for ( pCut = pList,                                      \
-          pCut2 = pCut? pCut->pData: NULL;                   \
-          pCut;                                              \
-          pCut = pCut2,                                      \
-          pCut2 = pCut? pCut->pData: NULL )
-
-// primes used to compute the hash key
-static int s_HashPrimes[10] = { 109, 499, 557, 619, 631, 709, 797, 881, 907, 991 };
-
-// hashing function
-static inline unsigned Cut_HashKey( Cut_Cut_t * pCut )
-{
-    unsigned i, uRes = pCut->nLeaves * s_HashPrimes[9];
-    for ( i = 0; i < pCut->nLeaves + pCut->fSeq; i++ )
-        uRes += s_HashPrimes[i] * pCut->pLeaves[i];
-    return uRes;
-}
-
-// hashing function
-static inline int Cut_CompareTwo( Cut_Cut_t * pCut1, Cut_Cut_t * pCut2 )
-{
-    unsigned i;
-    if ( pCut1->nLeaves != pCut2->nLeaves )
-        return 1;
-    for ( i = 0; i < pCut1->nLeaves; i++ )
-        if ( pCut1->pLeaves[i] != pCut2->pLeaves[i] )
-            return 1;
-    return 0;
-}
-
-static void Cut_TableResize( Cut_HashTable_t * pTable );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cut_HashTable_t * Cut_TableStart( int Size )
-{
-    Cut_HashTable_t * pTable;
-    pTable = ALLOC( Cut_HashTable_t, 1 );
-    memset( pTable, 0, sizeof(Cut_HashTable_t) );
-    // allocate the table
-    pTable->nBins = Cudd_PrimeCopy( Size );
-    pTable->pBins = ALLOC( Cut_Cut_t *, pTable->nBins );
-    memset( pTable->pBins, 0, sizeof(Cut_Cut_t *) * pTable->nBins );
-    pTable->pPlaces = ALLOC( int, pTable->nBins );
-    return pTable;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TableStop( Cut_HashTable_t * pTable )
-{
-    FREE( pTable->pPlaces );
-    free( pTable->pBins );
-    free( pTable );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Check the existence of a cut in the lookup table]
-
-  Description [Returns 1 if the entry is found.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t * pCut, int fStore )
-{
-    Cut_Cut_t * pEnt;
-    unsigned Key;
-    int clk = clock();
-
-    Key = Cut_HashKey(pCut) % pTable->nBins; 
-    Cut_TableListForEachCut( pTable->pBins[Key], pEnt )
-    {
-        if ( !Cut_CompareTwo( pEnt, pCut ) )
-        {
-pTable->timeLookup += clock() - clk;
-            return 1;
-        }
-    }
-    if ( pTable->nEntries > 2 * pTable->nBins )
-    {
-        Cut_TableResize( pTable );
-        Key = Cut_HashKey(pCut) % pTable->nBins; 
-    }
-    // remember the place
-    if ( fStore && pTable->pBins[Key] == NULL )
-        pTable->pPlaces[ pTable->nPlaces++ ] = Key;
-    // add the cut to the table
-    pCut->pData = pTable->pBins[Key];
-    pTable->pBins[Key] = pCut;
-    pTable->nEntries++;
-pTable->timeLookup += clock() - clk;
-    return 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TableClear( Cut_HashTable_t * pTable )
-{
-    int i;
-    assert( pTable->nPlaces <= pTable->nBins );
-    for ( i = 0; i < pTable->nPlaces; i++ )
-    {
-        assert( pTable->pBins[ pTable->pPlaces[i] ] );
-        pTable->pBins[ pTable->pPlaces[i] ] = NULL;
-    }
-    pTable->nPlaces = 0;
-    pTable->nEntries = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TableResize( Cut_HashTable_t * pTable )
-{
-    Cut_Cut_t ** pBinsNew;
-    Cut_Cut_t * pEnt, * pEnt2;
-    int nBinsNew, Counter, i, clk;
-    unsigned Key;
-
-clk = clock();
-    // get the new table size
-    nBinsNew = Cudd_PrimeCopy( 3 * pTable->nBins ); 
-    // allocate a new array
-    pBinsNew = ALLOC( Cut_Cut_t *, nBinsNew );
-    memset( pBinsNew, 0, sizeof(Cut_Cut_t *) * nBinsNew );
-    // rehash the entries from the old table
-    Counter = 0;
-    for ( i = 0; i < pTable->nBins; i++ )
-        Cut_TableListForEachCutSafe( pTable->pBins[i], pEnt, pEnt2 )
-        {
-            Key = Cut_HashKey(pEnt) % nBinsNew;
-            pEnt->pData   = pBinsNew[Key];
-            pBinsNew[Key] = pEnt;
-            Counter++;
-        }
-    assert( Counter == 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( pTable->pBins );
-    pTable->pBins = pBinsNew;
-    pTable->nBins = nBinsNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cut_TableReadTime( Cut_HashTable_t * pTable )
-{
-    if ( pTable == NULL )
-        return 0;
-    return pTable->timeLookup;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-

src/opt/cut/cutTruth.c

@@ -315,6 +315,7 @@ void Cut_TruthComputeOld( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cu
 p->timeTruth += clock() - clk;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/opt/cut/module.make

-SRC +=  src/opt/cut/cutMan.c \
+SRC +=  src/opt/cut/cutApi.c \
+        src/opt/cut/cutCut.c \
+        src/opt/cut/cutMan.c \
         src/opt/cut/cutMerge.c \
         src/opt/cut/cutNode.c \
         src/opt/cut/cutSeq.c \
-        src/opt/cut/cutTable.c \
         src/opt/cut/cutTruth.c 

src/opt/dec/decFactor.c

@@ -183,7 +183,7 @@ Dec_Edge_t Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
 ***********************************************************************/
 Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple )
 {
-    Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
+    Dec_Man_t * pManDec = Abc_FrameReadManDec();
     Vec_Int_t * vEdgeLits  = pManDec->vLits;
     Mvc_Cover_t * pDiv, * pQuo, * pRem;
     Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
@@ -228,7 +228,7 @@ Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cov
 ***********************************************************************/
 Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
 {
-    Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
+    Dec_Man_t * pManDec = Abc_FrameReadManDec();
     Vec_Int_t * vEdgeCubes = pManDec->vCubes;
     Vec_Int_t * vEdgeLits  = pManDec->vLits;
     Mvc_Manager_t * pMem = pManDec->pMvcMem;
@@ -323,7 +323,7 @@ Dec_Edge_t Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes
 ***********************************************************************/
 Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
 {
-    Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
+    Dec_Man_t * pManDec = Abc_FrameReadManDec();
     Mvc_Manager_t * pMem = pManDec->pMvcMem;
     Mvc_Cover_t * pMvc;
     Mvc_Cube_t * pMvcCube;
@@ -365,7 +365,7 @@ Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
 ***********************************************************************/
 int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
 {
-    DdManager * dd = Abc_FrameReadManDd( Abc_FrameGetGlobalFrame() );
+    DdManager * dd = Abc_FrameReadManDd();
     DdNode * bFunc1, * bFunc2;
     int RetValue;
     bFunc1 = Abc_ConvertSopToBdd( dd, pSop );    Cudd_Ref( bFunc1 );

src/opt/rwr/rwrMan.c

@@ -50,7 +50,7 @@ clk = clock();
     p = ALLOC( Rwr_Man_t, 1 );
     memset( p, 0, sizeof(Rwr_Man_t) );
     p->nFuncs = (1<<16);
-    pManDec   = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
+    pManDec   = Abc_FrameReadManDec();
     p->puCanons = pManDec->puCanons; 
     p->pPhases  = pManDec->pPhases; 
     p->pPerms   = pManDec->pPerms; 

src/sat/asat/solver.h

@@ -43,9 +43,9 @@ typedef int                lit;
 typedef char               lbool;
 
 #ifdef _WIN32
-typedef signed __int64     uint64;   // compatible with MS VS 6.0
+typedef signed __int64  sint64;   // compatible with MS VS 6.0
 #else
-typedef unsigned long long uint64;
+typedef long long       sint64;
 #endif
 
 static const int   var_Undef = -1;
@@ -80,8 +80,8 @@ extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName );
 
 struct stats_t
 {
-    uint64   starts, decisions, propagations, inspects, conflicts;
-    uint64   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
+    sint64   starts, decisions, propagations, inspects, conflicts;
+    sint64   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
 };
 typedef struct stats_t stats;