From: vijay_ganesh Date: Wed, 2 Dec 2009 00:52:09 +0000 (+0000) Subject: added -march=native as compile option X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=98ef458d322c4c47e9cfd57ba5a565d5fafc6fe6;p=francis%2Fstp.git 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 7dc15ff..4342f72 100644 --- 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 5fa33a1..ce1c4fc 100644 --- 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 50506a4..fd1d690 100644 --- 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 11db03c..6c417b4 100644 --- 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 c4f09ca..305c765 100644 --- 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 18e8724..541c077 100644 --- 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 ac2be0d..0c1030d 100644 --- 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 5559d75..01a4d8a 100644 --- 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 b375538..6db1d0a 100644 --- 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 450385a..1d9d506 100644 --- 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 28fd9be..7d422c4 100644 --- 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)