diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-02 13:38:21 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-02 13:38:21 +0100 |
| commit | 607c758e0220d8ba91eaf0e9e96b5ea71c5c6fd2 (patch) | |
| tree | 9333c12809138a6bbaeeb137e81a4fc6c4d34ef9 /src/Makefile | |
| parent | e3ff85dccf62b497cd017d2b55e08e7f49ebd80f (diff) | |
| download | smtcoq-607c758e0220d8ba91eaf0e9e96b5ea71c5c6fd2.tar.gz smtcoq-607c758e0220d8ba91eaf0e9e96b5ea71c5c6fd2.zip | |
Separate verit input (smtlib2) from output
Diffstat (limited to 'src/Makefile')
| -rw-r--r-- | src/Makefile | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/src/Makefile b/src/Makefile index a2a2b18..d81ee84 100644 --- a/src/Makefile +++ b/src/Makefile @@ -42,6 +42,7 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config) OCAMLLIBS?=-I zchaff\ -I verit\ -I trace\ + -I smtlib2\ -I lia\ -I euf\ -I cnf @@ -162,11 +163,11 @@ MLFILES:=lia/lia.ml\ verit/verit.ml\ verit/veritLexer.ml\ verit/veritParser.ml\ - verit/smtlib2_util.ml\ - verit/smtlib2_parse.ml\ - verit/smtlib2_lex.ml\ - verit/smtlib2_genConstr.ml\ - verit/smtlib2_ast.ml\ + smtlib2/smtlib2_util.ml\ + smtlib2/smtlib2_parse.ml\ + smtlib2/smtlib2_lex.ml\ + smtlib2/smtlib2_genConstr.ml\ + smtlib2/smtlib2_ast.ml\ trace/smtTrace.ml\ trace/smtMisc.ml\ trace/smtForm.ml\ @@ -251,10 +252,10 @@ beautify: $(VFILES:=.beautified) $(CMXS): $(CMXA) $(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^ -$(CMXA): trace/structures.cmx 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): trace/structures.cmx 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 smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx $(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^ -ml: verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.ml verit/smtlib2_lex.ml +ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml %.ml %.mli: %.mly @@ -341,7 +342,7 @@ clean: - rm -rf vtest - rm -rf ztest - rm -rf test - - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../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 + - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml archclean: rm -f *.cmx *.o |