blob: 7b9b4f657672202347a702137cd4e620ca068b7c (
plain)
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
|
include ../../Makefile.config
CC=../../ccomp
ifeq ($(OCAML_LM_PROF), true)
override CCOMPOPTS+=-S
endif
CFLAGS=$(CCOMPOPTS) -stdlib ../../runtime -dparse -dclight -dasm -fstruct-return
SRCS=analyze.c clause.c clock.c closure.c cnf.c component.c \
condensing.c context.c defs.c dfgparser.c dfgscanner.c doc-proof.c \
flags.c foldfg.c graph.c hash.c hasharray.c iaparser.c iascanner.c \
kbo.c list.c memory.c misc.c options.c order.c partition.c \
proofcheck.c renaming.c resolution.c rpos.c rules-inf.c rules-red.c \
rules-sort.c rules-split.c rules-ur.c search.c sharing.c sort.c st.c \
stack.c strings.c subst.c subsumption.c symbol.c table.c tableau.c \
term.c terminator.c top.c unify.c vector.c
all: spass
all_s: all
spass: $(SRCS:.c=.o)
$(CC) $(CFLAGS) -o spass $(SRCS:.c=.o) $(LIBMATH)
clean:
rm -f spass
rm -f *.o *.s *.parsed.c *.light.c *.sdump
test:
$(SIMU) ./spass small_problem.dfg | grep 'Proof found'
TIME=ocaml unix.cma ../../tools/xtime.ml -o /dev/null -mintime 5.0
bench:
@$(TIME) -name spass -- ./spass problem.dfg
depend:
gcc -MM $(SRCS) > .depend
include .depend
|