1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
|
#- -*-Mode: Makefile;-*- ------------------------------------------------
#
# File : Makefile.vars
#
# Makefile-definitions common to all CLIB-Makefiles
#
# Author: Stephan Schulz
#
#------------------------------------------------------------------------
.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/StarExec/bin
MANPATH = /Users/schulz/StarExec/man
STAREXECPATH=$(HOME)/StarExec
# 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.
MAKE = make # Should also work with GNU make
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
# ======================
# System libraries:
LIBS = -lm -lpicosat
# Use the C compiler to generate dependencies:
MAKEDEPEND = $(CC) -M $(CFLAGS) *.c > Makefile.dependencies
# 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 memorymanagement. 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:
# Try to increase the stack size to the max allowed.
# "Value" is not used anymore.
#
# INSTRUMENT_PERF_CTR:
# Enable self-profiling with certain performance counters.
#
# TAGGED_POINTERS:
# The lower bits of term struct pointers are assumed to be 0 due to alignment
# and are used to store small bits of temporary information.
#
# COMPILE_HEURISTICS_OPTIMIZED:
# Compile heuristic selection functions with optimization flags instead of -O0.
# This makes the binary smaller but increases compile time considerably.
#
BUILDFLAGS = -I/usr/include/picosat \
-DPRINT_SOMEERRORS_STDOUT \
-DMEMORY_RESERVE_PARANOID \
-DPRINT_TSTP_STATUS \
-DSTACK_SIZE=32768 \
-DCLAUSE_PERM_IDENT \
-DTAGGED_POINTERS \
# -DENABLE_LFHO \
# -DUSE_SYSTEM_MEM \
# -DUSE_NEWMEM \
# -DCOMPILE_HEURISTICS_OPTIMIZED \
# -DPDT_COUNT_NODES \
# -DPRINT_INDEX_STATS \
# -DINSTRUMENT_PERF_CTR \
# -DMEASURE_UNIFICATION \
# -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
PROFFLAGS = # -pg
DEBUGGER = # -g -ggdb
LTOFLAGS = # -flto
WFLAGS = -Wall
OPTFLAGS = -O03 -fomit-frame-pointer -fno-common
#OPTFLAGS = -O03 -fno-common
EHOH =
DEBUGFLAGS = $(PROFFLAGS) $(MEMDEBUG) $(DEBUGGER) $(NODEBUG)
CFLAGS = $(OPTFLAGS) $(LTOFLAGS) $(WFLAGS) $(DEBUGFLAGS) $(BUILDFLAGS) -std=gnu99 -I../include
LDFLAGS = $(OPTFLAGS) $(LTOFLAGS) $(PROFFLAGS) $(DEBUGGER)
LD = $(CC) $(LDFLAGS)
# Generic
# AR = sleep 1;ar rcs
AR = ar rcs
CC = gcc
# Builds with link time optimization
#
# Linux (tested on Ubuntu 16.04 LTS)
# AR = gcc-ar rcs
# CC = gcc
# LTOFLAGS = -flto
# OS X Clang (tested on Mac OS X 10.11)
# install clang from Macports: sudo port install llvm-3.9
# AR = llvm-ar-mp-3.9 rcs
# CC = clang-mp-3.9
# LTOFLAGS = -flto
|
