blob: db28f4aeb9d52da0c6fd5db6fd438827a28edea3 (
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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
ZCHAFFSRC=$(wildcard sat*.cnf) hole4.cnf cmu-bmc-barrel6.cnf velev-sss-1.0-05.cnf
VERITSRC=$(wildcard sat*.smt2) hole4.smt2 $(wildcard uf*.smt2) $(wildcard lia*.smt2) $(wildcard let*.smt2)
ZCHAFFLOG=$(ZCHAFFSRC:.cnf=.zlog)
VERITLOG=$(VERITSRC:.smt2=.vtlog)
OBJ=$(ZCHAFFLOG) $(VERITLOG)
COQLIBS?= -R ../src SMTCoq
OPT?=
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
VIOFLAG?=-quick
COQC?=$(COQBIN)coqc
all: zchaff verit lfsc
vernac: zchaffv veritv
tactics: zchafft veritt lfsc
zchaff: zchaffv zchafft
zchaffv: $(ZCHAFFLOG) Tests_zchaff_vernac.vo
zchafft: Tests_zchaff_tactics.vo
verit: veritv veritt
veritv: $(VERITLOG) Tests_verit_vernac.vo
veritt: Tests_verit_tactics.vo
lfsc: Tests_lfsc_tactics.vo
logs: $(OBJ)
%.zlog: %.cnf
./runzchaff.sh $<
%.vtlog: %.smt2
./runverit.sh $<
%.vo %.glob: %.v
$(COQC) $(COQDEBUG) $(COQFLAGS) $*
%.vio: %.v logs
$(COQC) $(VIOFLAG) $(COQDEBUG) $(COQFLAGS) $*
parallel: Tests_zchaff_tactics.vio Tests_verit_tactics.vio Tests_lfsc_tactics.vio
coqc -schedule-vio-checking 3 Tests_zchaff_tactics Tests_verit_tactics Tests_lfsc_tactics
clean: cleanvo
rm -rf *~ $(ZCHAFFLOG) $(VERITLOG)
cleanvo:
rm -rf *~ *.vo *.glob *.vio
|
