added -march=native as compile option

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@446 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 7dc15ffab941cd682da5737797a1c0b59572bab9..4342f72864d6bca07052f141520846f0d8036378 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -10,30 +10,44 @@
 
 #OPTIMIZE     = -g -pg            # Debugging and gprof-style profiling
 OPTIMIZE      = -g                # Debugging
-OPTIMIZE      = -O3 -DNDEBUG      # Maximum optimization
+OPTIMIZE      = -O3 -march=native # Maximum optimization
 #OPTIMIZE     = -O3 -DNDEBUG -DLESSBYTES_PERNODE
 #CFLAGS_M32   = -m32
 CFLAGS_BASE   = $(OPTIMIZE)
 
 # OPTION to compile CRYPTOMiniSAT
-CRYPTOMINISAT = true
-CFLAGS_BASE   = $(OPTIMIZE) -DCRYPTOMINISAT
+CRYPTOMINISAT  = true
+CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT
+MTL            = ../sat/cryptominisat/mtl
+SOLVER_INCLUDE = ../sat/cryptominisat
 
 # OPTION to compile CRYPTOMiniSAT version 2.x
 #CRYPTOMINISAT2 = true
 #CFLAGS_BASE   = $(OPTIMIZE) -DCRYPTOMINISAT2
+#MTL            = ../sat/cryptominisat2/mtl
+#SOLVER_INCLUDE = ../sat/cryptominisat2
+
 
 # OPTION to compile MiniSAT
 #CORE          = true
 #CFLAGS_BASE   = $(OPTIMIZE) -DCORE
+#MTL            = ../sat/mtl
+#SOLVER_INCLUDE = ../sat/core
+
 
 # OPTION to compile UNSOUND MiniSAT
 #UNSOUND       = true
 #CFLAGS_BASE   = $(OPTIMIZE) -DUNSOUND
+#MTL            = ../sat/mtl
+#SOLVER_INCLUDE = ../sat/unsound
+
 
 # OPTION to compile Simplifying MiniSAT
 #SIMP          = true
 #CFLAGS_BASE   = $(OPTIMIZE) -DSIMP
+#MTL            = ../sat/mtl
+#SOLVER_INCLUDE = ../sat/simp
+
 
 SHELL=/bin/bash
 

diff --git a/src/AST/Makefile b/src/AST/Makefile
index 5fa33a1fec342970f1109f971f3181abb8e9ab52..ce1c4fcc0f21b1c4e5ec320294f22f17836116a0 100644 (file)
--- a/src/AST/Makefile
+++ b/src/AST/Makefile
@@ -3,7 +3,7 @@ include ../../scripts/Makefile.common
 SRCS=$(wildcard  *.cpp)
 OBJS = $(SRCS:.cpp=.o)
 OBJS+= ASTKind.o
-CFLAGS += -I../sat/mtl -I../sat/core
+CFLAGS += -I$(MTL)
 
 #Make the ast library for use by other modules
 libast.a:$(OBJS) depend

diff --git a/src/STPManager/Makefile b/src/STPManager/Makefile
index 50506a48e98dfcbf081b5f4b81d31f3d291d43da..fd1d690d09193e020e20c339b5e5dfbcf46abe21 100644 (file)
--- a/src/STPManager/Makefile
+++ b/src/STPManager/Makefile
@@ -2,7 +2,7 @@ include ../../scripts/Makefile.common
 
 SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)
-CFLAGS += -I../sat/mtl -I../sat/simp -I../sat/core
+CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE)
 
 libstpmgr.a:   $(OBJS) depend
                $(AR) rc $@ $(OBJS)

diff --git a/src/absrefine_counterexample/Makefile b/src/absrefine_counterexample/Makefile
index 11db03cf591f6f214383334559239ac6d97279e2..6c417b4903186b7e97a49c9871f3aebb22bc5533 100644 (file)
--- a/src/absrefine_counterexample/Makefile
+++ b/src/absrefine_counterexample/Makefile
@@ -2,7 +2,7 @@ include ../../scripts/Makefile.common
 
 SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)
-CFLAGS += -I../sat/mtl -I../sat/simp -I../sat/core
+CFLAGS += -I$(MTL) -I$(MTRAND) -I$(SOLVER_INCLUDE)
 
 libabstractionrefinement.a:    $(OBJS) depend
                                $(AR) rc $@ $(OBJS)

diff --git a/src/c_interface/Makefile b/src/c_interface/Makefile
index c4f09caaa6349c303ea50452097be0095ede9f71..305c765dba680d123e2aea84f943e8fcbf2088c3 100644 (file)
--- a/src/c_interface/Makefile
+++ b/src/c_interface/Makefile
@@ -2,7 +2,7 @@ include ../../scripts/Makefile.common
 
 SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)
-CFLAGS += -I../sat/mtl -I../sat/simp -I../sat/core
+CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE)
 
 libcinterface.a: $(OBJS) depend
        $(AR) rc $@ $(OBJS)

diff --git a/src/parser/Makefile b/src/parser/Makefile
index 18e8724396ba578dbd8c98e9dfefffd45fc57033..541c0774714cef045df3cfdb37a1dd606850ff9e 100644 (file)
--- a/src/parser/Makefile
+++ b/src/parser/Makefile
@@ -6,7 +6,7 @@ YACC=bison -d -y --debug -v
 SRCS = lexCVC.cpp parseCVC.cpp parseSMT.cpp lexSMT.cpp let-funcs.cpp
 OBJS = $(SRCS:.cpp=.o)
 LIBS = -L../AST -last -L../sat -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv
-CFLAGS += -I../sat/mtl -I../sat/core  -I../sat/simp -I../sat/unsound
+CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE)
 
 libparser.a: $(OBJS)
        $(AR) rc $@ $^

diff --git a/src/printer/Makefile b/src/printer/Makefile
index ac2be0d680652f4f280d53ee89dd00d4e8a4d9d3..0c1030dcfe58805409b98ed3e776301af51efe66 100644 (file)
--- a/src/printer/Makefile
+++ b/src/printer/Makefile
@@ -2,7 +2,7 @@ include ../../scripts/Makefile.common
 
 SRCS=$(wildcard  *.cpp)
 OBJS = $(SRCS:.cpp=.o)
-CFLAGS += -I../sat/mtl -I../sat/core
+CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE)
 
 #Make the ast library for use by other modules
 libprinter.a:$(OBJS) depend

diff --git a/src/sat/cryptominisat/Solver.cpp b/src/sat/cryptominisat/Solver.cpp
index 5559d753d468855b4f0517fc60d575005c102d1e..01a4d8a586b3e20b344fbc0ec8ab18523b353cfb 100644 (file)
--- a/src/sat/cryptominisat/Solver.cpp
+++ b/src/sat/cryptominisat/Solver.cpp
@@ -1242,7 +1242,7 @@ next:
 
     assert(!failed);
 
-    printf("Verified %d original clauses.\n", clauses.size() + xorclauses.size());
+    //printf("Verified %d original clauses.\n", clauses.size() + xorclauses.size());
 }
 
 

diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile
index b375538fe80253c7cdfebf1ee78de071cc9c4862..6db1d0af88ae4ad5a16b5317588401b6b340eda4 100644 (file)
--- a/src/sat/cryptominisat2/Makefile
+++ b/src/sat/cryptominisat2/Makefile
@@ -1,7 +1,7 @@
 include   ../../../scripts/Makefile.common
 
-MTL       = ../cryptominisat/mtl
-MTRAND    = ../cryptominisat/MTRand
+MTL       = mtl
+MTRAND    = MTRand
 SOURCES   = Conglomerate.cpp  FindUndef.cpp  Gaussian.cpp  Logger.cpp  MatrixFinder.cpp  PackedRow.cpp  Solver.cpp  VarReplacer.cpp  XorFinder.cpp
 OBJECTS   = $(SOURCES:.cpp=.o)
 LIB       = libminisat.a

diff --git a/src/simplifier/Makefile b/src/simplifier/Makefile
index 450385a80dc39bee814254811c29d617a98b9bbe..1d9d506edf4240efe960e85e2aec374b56d04b69 100644 (file)
--- a/src/simplifier/Makefile
+++ b/src/simplifier/Makefile
@@ -2,7 +2,7 @@ include ../../scripts/Makefile.common
 
 SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)
-CFLAGS += -I../sat/mtl -I../sat/simp -I../sat/core
+CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE)
 
 libsimplifier.a:$(OBJS) depend
                $(AR) rc $@ $(OBJS)

diff --git a/src/to-sat/Makefile b/src/to-sat/Makefile
index 28fd9bec0d6329e4b6da0a0b880f92f143107b62..7d422c44693791b6121823d319c0344f71a292cf 100644 (file)
--- a/src/to-sat/Makefile
+++ b/src/to-sat/Makefile
@@ -2,7 +2,7 @@ include ../../scripts/Makefile.common
 
 SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)
-CFLAGS += -I../sat/mtl -I../sat/simp -I../sat/core
+CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE)
 
 libtosat.a:    $(OBJS) depend
                $(AR) rc $@ $(OBJS)