#- -*-Mode: Makefile;-*- ------------------------------------------------
#
# File  : Makefile.vars
#
#  Makefile-definitions common to all CLIB-Makefiles
#
# Author: Stephan Schulz`
#
# Changes
#
# <1> Sun Jul  6 22:55:11 MET DST 1997
#     New
#
#------------------------------------------------------------------------

.PHONY: warn depend links tags remove_links tags rebuild install install_exec distrib fulldistrib top tools remake documentation


# EXECPATH is where make install-exec will move the more important
# executables. Edit it to point to wherever you want them to live. 
# Note that ./configure takes care of this automatically.

EXECPATH = /Users/schulz/SOURCES/Projects/E/PROVER
MANPATH = /Users/schulz/SOURCES/Projects/E/DOC/man

# Makefile special variables
#
# If optional programs are missing on your system you can define the
# variables to "echo". Standard Installation and use should be
# unaffected, but certain services or non-essential parts will not be
# available.

SHELL      = /bin/sh
MAKE       = make      # Should also work with GNU make
AR         = ar -rcs
TAR        = tar       # Optional, for building distributions
GZIP       = gzip
MCOPY      = mcopy     # Optional, for building floppy disks
LN         = ln -s     # You can use cp or hard links if your
                       # system does not support symbolic links
LATEX      = latex     # Optional if you don't want or need the
                       # documentation. This needs to be latex2e (or
                       # perhaps later), latex 2.09 wont work.
PDFLATEX   = pdflatex  # As above.
BIBTEX     = bibtex    # Optional, see above
MAKEINDEX  = makeindex # Optional, see above
DVIPS      = dvips     # Optional, see above

# Compile time options
# ======================

# Remove the comment from the following to enable gprof-style
#  profiling 
#  -> This will break some stuff on at least some Solaris 2.6
#     machines, which seem to lack a profiling-enabled libm. I have a
#     simple sqrt() imlementation to circumvent the problem...

PROFFLAGS  = # -pg # -DNEED_MATH_EMULATION
# DEBUGGER   -g -ggdb

# System libraries:

LIBS = -lm

# BUILDFLAGS:
#
# PRINT_SOMEERRORS_STDOUT: Print various error messages (out of
#                          memory, empty input file) to stdout  
#                          (otherwise only to stderr) 
# USE_NEWMEM: Use a memory management system like everybody else,
#             using free lists filled up by allocating large blocks
#             and hacking them  into suitabe pieces. Contrary to
#             common expectations, this slows E down between 5 and 15%
#             (depending on hardware architecture and problem)
#             compared to its native memory management. It's
#             left in as a warning reminder only.
# USE_SYSTEM_MEM: Use normal malloc()/free instead of the build-in
#                  memory management. Does not combine with USE_NEWMEM! 
# CLAUSE_PERM_IDENT: Clauses have an extra unchanging identifier. Useful
#                 for testing some proerties  
#
# MEASURE_EXPENSIVE: Compile counting operations and things into the
#                    code even in time-critical sections.
# PRINT_SHARING: Determine and print the sharing factor of the proof
#                state for each clause activation. 
# PRINT_RW_STATE: Dump R,E,NEW in each loop traversal.
#
# FULL_MEM_STATS: Print size of the most important data types and
#                 information about allocated memory. 
# CONSTANT_MEM_ESTIMATE: Use normalized portable data type estimates
#                        instead of sizeof() to get actual machine data 
#                        sizes. Necessary to make the prover behave _exactly_
#                        the same on different machines, but makes memory 
#                        estimation worse on most machines!
# STACK_SIZE=VALUE: Increase the system stacksize to value and run a
#                   freshly exec()'ed copy of E. This seems to work
#                   well, but is not debug-friendly. Disable and use
#                   limit/ulimit for debuging.
# INSTRUMENT_PERF_CTR: Enable self-profiling with certain performance counters.


BUILDFLAGS = -DPRINT_SOMEERRORS_STDOUT \
             -DMEMORY_RESERVE_PARANOID \
             -DPRINT_TSTP_STATUS \
	     -DSTACK_SIZE=32768 	\
             -DCLAUSE_PERM_IDENT \
	     # -DINSTRUMENT_PERF_CTR\
	     # -DMEASURE_UNIFICATION\
             # -DUSE_SYSTEM_MEM \
             # -DFULL_MEM_STATS\
             # -DPRINT_RW_STATE # -DMEASURE_EXPENSIVE

# The next two flags are dependend - you can only have CLB_MEMORY_DEBUG
# if you don't have NDEBUG!
MEMDEBUG   = # -DCLB_MEMORY_DEBUG # -DCLB_MEMORY_DEBUG2
NODEBUG    = -DNDEBUG -DFAST_EXIT
DEBUGFLAGS = $(PROFFLAGS) $(MEMDEBUG) $(DEBUGGER) $(NODEBUG)

ARCHFLAGS  =  # -mdynamic-no-pic # Helps a tiny bit on Mac
              # -mcpu=v8 -mtune=ultrasparc # Somewhat better than
                                           # without, v9 is 
                                           # worse (!), ultrasparc does
                                           # not work at all (probably
                                           # due to 64 bit include files
                                           # or something...) 
# ARCHFLAGS   = -march=i686  # No detectable improvement

# CFLAGS for different setups:
# 
# Solaris/Linux with gcc
#
#CFLAGS     = -O6 -Wall -Wno-char-subscripts -Wshadow -ansi \
#             -pedantic -I../include $(DEBUGFLAGS) \
#             $(BUILDFLAGS) $(ARCHFLAGS)

CFLAGS     = -O6 -fomit-frame-pointer -Wall -Wno-char-subscripts -std=gnu99 \
             -I../include $(DEBUGFLAGS) \
             $(BUILDFLAGS) $(ARCHFLAGS)

# Version for profiling

# CFLAGS     = -O6 -Wall -Wno-char-subscripts -ansi -std=gnu99 \
#              -I../include $(DEBUGFLAGS) \
#              $(BUILDFLAGS) $(ARCHFLAGS)

# Version for debugging

# CFLAGS     = -Wall -Wno-char-subscripts -std=c99 \
#              -I../include $(DEBUGFLAGS) \
#               $(BUILDFLAGS) $(ARCHFLAGS)

# Workaround for broken Red Hat gcc 2.96 (hah!)

# CFLAGS     = -O6 -fno-strength-reduce -Wall -Wno-char-subscripts -Wshadow -ansi \
#             -pedantic -I../include $(DEBUGFLAGS) \
#             $(BUILDFLAGS) $(ARCHFLAGS)
#
# Solaris with SUN's SUNPro cc
# CFLAGS     = -fast -I../include $(BUILDFLAGS) $(DEBUGFLAGS) -D__inline__=""
#
# HPUX with gcc - someone please hurt an HP employee for me!
#
# CFLAGS     = -O6 -Wall -Wno-char-subscripts -Wshadow \
#             -I../include $(DEBUGFLAGS) \
#             $(BUILDFLAGS) $(ARCHFLAGS) -DHP_UX


LDFLAGS    = $(PROFFLAGS) $(DEBUGGER)
CC         = gcc
# CC         = cc
LD         = $(CC) $(LDFLAGS)

# Both makedepend and a good C compiler can be used to generate
# dependencies. gcc does a better job than makedepend, so it is the
# default. 
#
# MAKEDEPEND = echo "" > Makefile.dependencies; makedepend -- $(CFLAGS) -- -f Makefile.dependencies *.c
MAKEDEPEND = gcc -M $(CFLAGS) *.c > Makefile.dependencies