blob: 928db7dccdba1ce14b118f7c95ef0dbd10a362b2 (
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
92
93
94
95
96
97
98
99
100
101
102
103
|
# This configuration file was generated by running:
# coq_makefile -f Make -o Makefile
###############################################################################
# #
# Project files. #
# #
###############################################################################
COQMF_VFILES = versions/standard/Int63/Int63.v versions/standard/Int63/Int63Native.v versions/standard/Int63/Int63Op.v versions/standard/Int63/Int63Axioms.v versions/standard/Int63/Int63Properties.v versions/standard/Array/PArray.v versions/standard/Structures.v bva/BVList.v bva/Bva_checker.v classes/SMT_classes.v classes/SMT_classes_instances.v array/FArray.v array/Array_checker.v cnf/Cnf.v euf/Euf.v lia/Lia.v spl/Assumptions.v spl/Syntactic.v spl/Arithmetic.v spl/Operators.v Conversion_tactics.v Misc.v SMTCoq.v ReflectFacts.v PropToBool.v BoolToProp.v Tactics.v SMT_terms.v State.v Trace.v
COQMF_MLIFILES = versions/standard/structures.mli trace/coqTerms.mli trace/smtBtype.mli trace/satAtom.mli trace/smtAtom.mli trace/smtCertif.mli trace/smtCnf.mli trace/smtCommands.mli trace/smtForm.mli trace/smtMisc.mli trace/smtTrace.mli smtlib2/smtlib2_parse.mli smtlib2/smtlib2_lex.mli smtlib2/smtlib2_ast.mli smtlib2/smtlib2_genConstr.mli smtlib2/smtlib2_util.mli smtlib2/sExpr.mli smtlib2/smtlib2_solver.mli smtlib2/sExprParser.mli verit/veritParser.mli verit/veritLexer.mli verit/verit.mli verit/veritSyntax.mli lfsc/shashcons.mli lfsc/hstring.mli lfsc/lfscParser.mli lfsc/ast.mli lfsc/translator_sig.mli lfsc/tosmtcoq.mli zchaff/cnfParser.mli zchaff/satParser.mli zchaff/zchaff.mli zchaff/zchaffParser.mli lia/lia.mli
COQMF_MLFILES = versions/standard/structures.ml trace/coqTerms.ml trace/smtBtype.ml trace/satAtom.ml trace/smtAtom.ml trace/smtCertif.ml trace/smtCnf.ml trace/smtCommands.ml trace/smtForm.ml trace/smtMisc.ml trace/smtTrace.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/smtlib2_ast.ml smtlib2/smtlib2_genConstr.ml smtlib2/smtlib2_util.ml smtlib2/sExpr.ml smtlib2/smtlib2_solver.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml verit/veritParser.ml verit/veritLexer.ml verit/verit.ml verit/veritSyntax.ml lfsc/shashcons.ml lfsc/hstring.ml lfsc/lfscParser.ml lfsc/type.ml lfsc/ast.ml lfsc/builtin.ml lfsc/tosmtcoq.ml lfsc/converter.ml lfsc/lfsc.ml lfsc/lfscLexer.ml zchaff/cnfParser.ml zchaff/satParser.ml zchaff/zchaff.ml zchaff/zchaffParser.ml lia/lia.ml
COQMF_ML4FILES = g_smtcoq.ml4
COQMF_MLPACKFILES = smtcoq_plugin.mlpack
COQMF_MLLIBFILES =
###############################################################################
# #
# Path directives (-I, -R, -Q). #
# #
###############################################################################
COQMF_OCAMLLIBS = -I . -I bva -I classes -I array -I cnf -I euf -I lfsc -I lia -I smtlib2 -I trace -I verit -I zchaff -I versions/standard -I versions/standard/Int63 -I versions/standard/Array -I '$(shell $(COQBIN)coqc -where)/plugins/micromega'
COQMF_SRC_SUBDIRS = . bva classes array cnf euf lfsc lia smtlib2 trace verit zchaff versions/standard versions/standard/Int63 versions/standard/Array '$(shell $(COQBIN)coqc -where)/plugins/micromega'
COQMF_COQLIBS = -I . -I bva -I classes -I array -I cnf -I euf -I lfsc -I lia -I smtlib2 -I trace -I verit -I zchaff -I versions/standard -I versions/standard/Int63 -I versions/standard/Array -I '$(shell $(COQBIN)coqc -where)/plugins/micromega' -R . SMTCoq
COQMF_COQLIBS_NOML = -R . SMTCoq
###############################################################################
# #
# Coq configuration. #
# #
###############################################################################
COQMF_LOCAL=1
COQMF_COQLIB=/home/artemis/Autres/coq-8.7.2//
COQMF_DOCDIR=/home/artemis/Autres/coq-8.7.2/doc/
COQMF_OCAMLFIND=/usr/bin/ocamlfind
COQMF_CAMLP4=camlp5
COQMF_CAMLP4O=/usr/bin/camlp5o
COQMF_CAMLP4BIN=/usr/bin/
COQMF_CAMLP4LIB=/usr/lib/ocaml/camlp5
COQMF_CAMLP4OPTIONS=-loc loc
COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50 -safe-string
COQMF_HASNATDYNLINK=true
COQMF_COQ_SRC_SUBDIRS=config dev lib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml
COQMF_WINDRIVE=/home/artemis/Autres/coq-8.7.2
###############################################################################
# #
# Extra variables. #
# #
###############################################################################
CAMLLEX = $(CAMLBIN)ocamllex
CAMLYACC = $(CAMLBIN)ocamlyacc
COQMF_OTHERFLAGS =
COQMF_INSTALLCOQDOCROOT = SMTCoq
###############################################################################
# #
# Extra targets. (-extra and -extra-phony, DEPRECATED) #
# #
###############################################################################
post-all::
$(MAKE) -f $(SELF) test
clean::
rm -f test
test :
cd ../unit-tests; make
post-all::
$(MAKE) -f $(SELF) ztest
clean::
rm -f ztest
ztest :
cd ../unit-tests; make zchaff
post-all::
$(MAKE) -f $(SELF) vtest
clean::
rm -f vtest
vtest :
cd ../unit-tests; make verit
post-all::
$(MAKE) -f $(SELF) lfsctest
clean::
rm -f lfsctest
lfsctest :
cd ../unit-tests; make lfsc
%.ml : %.mll
$(CAMLLEX) $<
%.ml %.mli : %.mly
$(CAMLYACC) $<
.PHONY: smtcoq_plugin.mlpack.d
smtcoq_plugin.mlpack.d : verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
|
