blob: d1c934285883b9057907c5618867e2f49c3fefd2 (
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
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
|
########################################################################
## This file is intended to developers, please do not use it to ##
## generate a Makefile, rather use the provided Makefile. ##
########################################################################
########################################################################
## To generate the Makefile: ##
## coq_makefile -f Make -o Makefile ##
## Change the "all" target into: ##
## all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) ##
## Change the "install-natdynlink" target: change CMXSFILES into CMXS and add the same thing for CMXA and VCMXS. ##
## Change the "install" target: change CMO into CMX. ##
## Finally, suppress the "Makefile" target and add to the "clean" target: ##
## - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.mli verit/smtlib2_parse.ml verit/smtlib2_lex.ml ##
########################################################################
-R . SMTCoq
-I cnf
-I euf
-I lia
-I trace
-I verit
-I zchaff
# -custom "cd ../unit-tests; make" "" "logs"
-custom "cd ../unit-tests; make" "" "test"
-custom "$(CAMLLEX) $<" "%.mll" "%.ml"
-custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
-custom "" "verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.ml verit/smtlib2_lex.ml" "ml"
-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx verit/smtlib2_util.cmx verit/smtlib2_ast.cmx verit/smtlib2_parse.cmx verit/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx verit/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)"
-custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
CMXA = trace/smtcoq.cmxa
CMXS = trace/smt_tactic.cmxs
VCMXS = "NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi"
CAMLLEX = $(CAMLBIN)ocamllex
CAMLYACC = $(CAMLBIN)ocamlyacc
trace/coqTerms.ml
trace/satAtom.ml
trace/smtAtom.ml
trace/smtAtom.mli
trace/smtCertif.ml
trace/smtCnf.ml
trace/smtForm.ml
trace/smtForm.mli
trace/smtMisc.ml
trace/smt_tactic.ml4
trace/smtTrace.ml
verit/smtlib2_ast.ml
verit/smtlib2_genConstr.ml
verit/smtlib2_lex.ml
verit/smtlib2_parse.ml
verit/smtlib2_util.ml
verit/veritParser.ml
verit/veritLexer.ml
verit/verit.ml
verit/veritSyntax.ml
verit/veritSyntax.mli
zchaff/cnfParser.ml
zchaff/satParser.ml
zchaff/zchaff.ml
zchaff/zchaffParser.ml
cnf/Cnf.v
euf/Euf.v
lia/lia.ml
lia/Lia.v
spl/Syntactic.v
spl/Arithmetic.v
spl/Operators.v
Misc.v
SMTCoq.v
SMT_terms.v
State.v
Trace.v
# tests/Tests.v
|
