Making changes suggested by Mark Jarvin.

10 files changed, 126 insertions, 133 deletions

diff --git a/Makefile b/Makefile
index 4247a799..e9214359 100644
--- a/Makefile
+++ b/Makefile
@@ -37,11 +37,26 @@ arch_flags : arch_flags.c
 ARCHFLAGS := $(shell $(CC) arch_flags.c -o arch_flags && ./arch_flags)
 OPTFLAGS  := -g -O #-DABC_NAMESPACE=xxx
 
-CFLAGS   += -Wall -Wno-unused-function -Wno-unused-but-set-variable $(OPTFLAGS) $(ARCHFLAGS) -I$(PWD)/src
-CXXFLAGS += $(CFLAGS) 
+CFLAGS   += -Wall -Wno-unused-function $(OPTFLAGS) $(ARCHFLAGS) -I$(PWD)/src
+
+ifeq ($(shell $(CC) -dumpversion | awk '{FS="."; print ($$1>=4 && $$2>=6)}'),1)
+# Set -Wno-unused-bug-set-variable for GCC 4.6.0 and greater only
+CFLAGS += -Wno-unused-but-set-variable
+endif
+
+LIBS := -ldl
 
-#LIBS := -m32 -ldl -rdynamic -lreadline -ltermcap
-LIBS := -ldl -lreadline -lpthread
+ifneq ($(READLINE),0)
+CFLAGS += -DABC_USE_READLINE
+LIBS += -lreadline
+endif
+
+ifneq ($(PTHREADS),0)
+CFLAGS += -DABC_USE_PTHREADS
+LIBS += -lpthread
+endif
+
+CXXFLAGS += $(CFLAGS) 
 
 SRC  := 
 GARBAGE := core core.* *.stackdump ./tags $(PROG) arch_flags
@@ -65,7 +80,7 @@ DEP := $(OBJ:.o=.d)
 
 %.o: %.cc
 	@echo "\`\` Compiling:" $(LOCAL_PATH)/$<
-	@$(CC) -c $(CXXFLAGS) $< -o $@
+	@$(CXX) -c $(CXXFLAGS) $< -o $@
 
 %.d: %.c
 	@echo "\`\` Dependency:" $(LOCAL_PATH)/$<
@@ -73,7 +88,7 @@ DEP := $(OBJ:.o=.d)
 
 %.d: %.cc
 	@echo "\`\` Generating dependency:" $(LOCAL_PATH)/$<
-	@./depends.sh $(CXX) `dirname $*.cc` $(CXXFLAGS) $(CFLAGS) $*.cc > $@
+	@./depends.sh $(CXX) `dirname $*.cc` $(CXXFLAGS) $*.cc > $@
 
 -include $(DEP)
 
diff --git a/lib/x64/pthreadVC2.dll b/lib/x64/pthreadVC2.dll
new file mode 100644
index 00000000..165b4d26
--- /dev/null
+++ b/lib/x64/pthreadVC2.dll
diff --git a/lib/x64/pthreadVC2.lib b/lib/x64/pthreadVC2.lib
new file mode 100644
index 00000000..1b07e0e9
--- /dev/null
+++ b/lib/x64/pthreadVC2.lib
diff --git a/lib/pthreadVC2.dll b/lib/x86/pthreadVC2.dll
index 93f562ba..93f562ba 100644
--- a/lib/pthreadVC2.dll
+++ b/lib/x86/pthreadVC2.dll
diff --git a/lib/pthreadVC2.lib b/lib/x86/pthreadVC2.lib
index 58733254..58733254 100644
--- a/lib/pthreadVC2.lib
+++ b/lib/x86/pthreadVC2.lib
diff --git a/readme b/readme
deleted file mode 100644
index c1f3fc39..00000000
--- a/readme
+++ /dev/null
@@ -1,112 +0,0 @@
-ABC: System for Sequential Logic Synthesis and Formal Verification
-
-ABC is always changing but the current snapshot is believed to be stable. 
-
-Compiling:
-
-To compile ABC as a binary, download and unzip the code, then type "make".
-
-To compile ABC as a static library, comment out #define _LIB in file 
-"src/base/main/main.c", then type "make libabc.a".
-
-When ABC is used as a static library, two additional procedures, Abc_Start() 
-and Abc_Stop(), are provided for starting and quitting the ABC framework in 
-the calling application. A simple demo program (file src/demo.c) shows how to 
-create a stand-alone program performing DAG-aware AIG rewriting, by calling 
-APIs of ABC compiled as a static library.
-
-To build the demo program
-- Copy demo.cc and libabc.a to the working directory
-- Run "gcc -Wall -g -c demo.c -o demo.o"
-- Run "gcc -g -o demo demo.o libabc.a -lm -ldl -rdynamic -lreadline -ltermcap -lpthread"
-
-To run the demo program, give it a file with the logic network in AIGER or BLIF. For example:
-
-> [alanmi@mima] ~/abc> demo i10.aig
-> i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
-> i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
-> Networks are equivalent.
-> Reading =   0.00 sec   Rewriting =   0.18 sec   Verification =   0.41 sec
-
-The same can be produced by running the binary in the command-line mode:
-
-> [alanmi@mima] ~/abc> ./abc
-> UC Berkeley, ABC 1.01 (compiled Oct  6 2012 19:05:18)
-> abc 01> r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec
-> i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
-> i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
-> Networks are equivalent.
-
-or in the batch mode:
-
-> [alanmi@mima] ~/abc> ./abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec"
-> ABC command line: "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec".
-> i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
-> i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
-> Networks are equivalent.
-
-
-
-Compiling as C or C++
-
-The current version of ABC can be compiled with C compiler or C++ compiler.
-
-To compile as C code (default): make sure that CC=gcc and ABC_NAMESPACE is not defined.
-To compile as C++ code without namespaces: make sure that CC=g++ and ABC_NAMESPACE is not defined.
-To compile as C++ code with namespaces: make sure that CC=g++ and ABC_NAMESPACE is set to
-the name of the requested namespace. For example, add to OPTFLAGS -DABC_NAMESPACE=xxx
-
-
-Bug reporting:
-
-Please try to reproduce all the reported bugs and unexpected features using the latest 
-version of ABC available from https://bitbucket.org/alanmi/abc/
-
-If the bug still persists, please provide the following information:    
-1. ABC version (when it was downloaded from BitBucket)
-2. Linux distribution and version (32-bit or 64-bit)
-3. The exact command-line and error message when trying to run the tool
-4. The output of the 'ldd' command run on the exeutable (e.g. 'ldd abc').
-5. Versions of relevant tools or packages used.
-
-
-Trouble shooting:
-
-(1) If compilation does not start because of the cyclic dependency check, 
-try touching all files as follows:    find ./ -type f -exec touch "{}" \;
-
-(2) If compilation fails because readline is missing, install 'readline' library or
-comment out line 26 "#define ABC_USE_READLINE" in file "src/base/main/mainUtils.c"
-
-(4) If compilation fails because pthreads are missing, install 'pthread' library or
-comment out line 29 "#define ABC_USE_PTHREADS" in file "src/base/cmd/cmdStarter.c" 
-and in file "src/proof/abs/absPth.c"
-
-(5) If compilation fails in file "src/base/main/libSupport.c", try the following:
-- Remove "src/base/main/libSupport.c" from "src/base/main/module.make"
-- Comment out calls to Libs_Init() and Libs_End() in "src/base/main/mainInit.c"
-
-(6) On some systems, readline requires adding '-lcurses' to Makefile.
-
-
-The following comment was added by Krish Sundaresan:
-
-"I found that the code does compile correctly on Solaris if gcc is used (instead of 
-g++ that I was using for some reason). Also readline which is not available by default 
-on most Sol10 systems, needs to be installed. I downloaded the readline-5.2 package 
-from sunfreeware.com and installed it locally. Also modified CFLAGS to add the local 
-include files for readline and LIBS to add the local libreadline.a. Perhaps you can 
-add these steps in the readme to help folks compiling this on Solaris."
-
-The following tutorial is kindly offered by Ana Petkovska from EPFL:
-https://www.dropbox.com/s/qrl9svlf0ylxy8p/ABC_GettingStarted.pdf
-
-Final remarks:
-
-Unfortunately, there is no comprehensive regression test. Good luck!                                
-
-
-This system is maintained by Alan Mishchenko <alanmi@eecs.berkeley.edu>. Consider also 
-using ZZ framework developed by Niklas Een: https://bitbucket.org/niklaseen/abc-zz
-
-This file was last modified on Oct 6, 2012
diff --git a/readme.md b/readme.md
new file mode 100644
index 00000000..7c3481fc
--- /dev/null
+++ b/readme.md
@@ -0,0 +1,103 @@
+# ABC: System for Sequential Logic Synthesis and Formal Verification
+
+ABC is always changing but the current snapshot is believed to be stable. 
+
+## Compiling:
+
+To compile ABC as a binary, download and unzip the code, then type `make`.
+
+To compile ABC as a static library, comment out `#define ABC_LIB` in file 
+"src/base/main/main.c", then type `make libabc.a`.
+
+When ABC is used as a static library, two additional procedures, `Abc_Start()` 
+and `Abc_Stop()`, are provided for starting and quitting the ABC framework in 
+the calling application. A simple demo program (file src/demo.c) shows how to 
+create a stand-alone program performing DAG-aware AIG rewriting, by calling 
+APIs of ABC compiled as a static library.
+
+To build the demo program
+
+ * Copy demo.cc and libabc.a to the working directory
+ * Run `gcc -Wall -g -c demo.c -o demo.o`
+ * Run `gcc -g -o demo demo.o libabc.a -lm -ldl -rdynamic -lreadline -ltermcap -lpthread`
+
+To run the demo program, give it a file with the logic network in AIGER or BLIF. For example:
+
+    [alanmi@mima] ~/abc> demo i10.aig
+    i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
+    i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
+    Networks are equivalent.
+    Reading =   0.00 sec   Rewriting =   0.18 sec   Verification =   0.41 sec
+
+The same can be produced by running the binary in the command-line mode:
+
+    [alanmi@mima] ~/abc> ./abc
+    UC Berkeley, ABC 1.01 (compiled Oct  6 2012 19:05:18)
+    abc 01> r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec
+    i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
+    i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
+    Networks are equivalent.
+
+or in the batch mode:
+
+    [alanmi@mima] ~/abc> ./abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec"
+    ABC command line: "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec".
+    i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
+    i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
+    Networks are equivalent.
+
+## Compiling as C or C++
+
+The current version of ABC can be compiled with C compiler or C++ compiler.
+
+ * To compile as C code (default): make sure that `CC=gcc` and `ABC_NAMESPACE` is not defined.
+ * To compile as C++ code without namespaces: make sure that `CC=g++` and `ABC_NAMESPACE` is not defined.
+ * To compile as C++ code with namespaces: make sure that `CC=g++` and `ABC_NAMESPACE` is set to
+   the name of the requested namespace. For example, add `-DABC_NAMESPACE=xxx` to OPTFLAGS.
+
+## Bug reporting:
+
+Please try to reproduce all the reported bugs and unexpected features using the latest 
+version of ABC available from https://bitbucket.org/alanmi/abc/
+
+If the bug still persists, please provide the following information:    
+
+ 1. ABC version (when it was downloaded from BitBucket)
+ 1. Linux distribution and version (32-bit or 64-bit)
+ 1. The exact command-line and error message when trying to run the tool
+ 1. The output of the `ldd` command run on the exeutable (e.g. `ldd abc`).
+ 1. Versions of relevant tools or packages used.
+
+
+## Troubleshooting:
+
+ 1. If compilation does not start because of the cyclic dependency check, 
+try touching all files as follows: `find ./ -type f -exec touch "{}" \;`
+ 1. If compilation fails because readline is missing, install 'readline' library or
+compile with `make READLINE=0`
+ 1. If compilation fails because pthreads are missing, install 'pthread' library or
+compile with `make PTHREADS=0`
+    * See http://sourceware.org/pthreads-win32/ for pthreads on Windows
+    * Precompiled DLLs are available from ftp://sourceware.org/pub/pthreads-win32/dll-latest
+ 1. If compilation fails in file "src/base/main/libSupport.c", try the following:
+    * Remove "src/base/main/libSupport.c" from "src/base/main/module.make"
+    * Comment out calls to `Libs_Init()` and `Libs_End()` in "src/base/main/mainInit.c"
+ 1. On some systems, readline requires adding '-lcurses' to Makefile.
+
+The following comment was added by Krish Sundaresan:
+
+"I found that the code does compile correctly on Solaris if gcc is used (instead of 
+g++ that I was using for some reason). Also readline which is not available by default 
+on most Sol10 systems, needs to be installed. I downloaded the readline-5.2 package 
+from sunfreeware.com and installed it locally. Also modified CFLAGS to add the local 
+include files for readline and LIBS to add the local libreadline.a. Perhaps you can 
+add these steps in the readme to help folks compiling this on Solaris."
+
+## Final remarks:
+
+Unfortunately, there is no comprehensive regression test. Good luck!                                
+
+This system is maintained by Alan Mishchenko <alanmi@eecs.berkeley.edu>. Consider also 
+using ZZ framework developed by Niklas Een: https://bitbucket.org/niklaseen/abc-zz
+
+This file was last modified on April 25, 2013
diff --git a/src/base/cmd/cmdStarter.c b/src/base/cmd/cmdStarter.c
index 21384930..bfdd480c 100644
--- a/src/base/cmd/cmdStarter.c
+++ b/src/base/cmd/cmdStarter.c
@@ -25,12 +25,9 @@
 #include "misc/util/abc_global.h"
 #include "misc/extra/extra.h"
 
-// comment out this line to disable pthreads
-#define ABC_USE_PTHREADS
-
 #ifdef ABC_USE_PTHREADS
 
-#ifdef WIN32
+#ifdef _WIN32
 #include "../lib/pthread.h"
 #else
 #include <pthread.h>
diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c
index 8d24a123..2b4e682b 100644
--- a/src/base/main/mainUtils.c
+++ b/src/base/main/mainUtils.c
@@ -21,11 +21,6 @@
 #include "base/abc/abc.h"
 #include "mainInt.h"
 
-#if !defined(_WIN32) && !defined(AIX) 
-// comment out the following line if 'readline' is not available
-#define ABC_USE_READLINE
-#endif
-
 #ifdef ABC_USE_READLINE
 #include <readline/readline.h>
 #include <readline/history.h>
diff --git a/src/proof/abs/absPth.c b/src/proof/abs/absPth.c
index ef38369c..bd3f2dcb 100644
--- a/src/proof/abs/absPth.c
+++ b/src/proof/abs/absPth.c
@@ -23,14 +23,9 @@
 #include "proof/ssw/ssw.h"
 
 
-
-
-// comment out this line to disable pthreads
-#define ABC_USE_PTHREADS
-
 #ifdef ABC_USE_PTHREADS
 
-#ifdef WIN32
+#ifdef _WIN32
 #include "../lib/pthread.h"
 #else
 #include <pthread.h>