diff options
| -rw-r--r-- | src/Make | 18 | ||||
| -rw-r--r-- | src/Makefile | 17 | ||||
| -rw-r--r-- | src/smtlib2/smtlib2_ast.ml (renamed from src/verit/smtlib2_ast.ml) | 0 | ||||
| -rw-r--r-- | src/smtlib2/smtlib2_genConstr.ml (renamed from src/verit/smtlib2_genConstr.ml) | 0 | ||||
| -rw-r--r-- | src/smtlib2/smtlib2_lex.mll (renamed from src/verit/smtlib2_lex.mll) | 0 | ||||
| -rw-r--r-- | src/smtlib2/smtlib2_parse.mly (renamed from src/verit/smtlib2_parse.mly) | 0 | ||||
| -rw-r--r-- | src/smtlib2/smtlib2_util.ml (renamed from src/verit/smtlib2_util.ml) | 0 |
7 files changed, 19 insertions, 16 deletions
@@ -14,7 +14,7 @@ ## 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/*.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 ## ######################################################################## @@ -23,6 +23,7 @@ -I cnf -I euf -I lia +-I smtlib2 -I trace -I verit -I zchaff @@ -33,9 +34,9 @@ -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 "" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" "ml" --custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "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)" +-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "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" "$(CMXA)" -custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)" CMXA = trace/smtcoq.cmxa @@ -57,11 +58,12 @@ 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 +smtlib2/smtlib2_ast.ml +smtlib2/smtlib2_genConstr.ml +smtlib2/smtlib2_lex.ml +smtlib2/smtlib2_parse.ml +smtlib2/smtlib2_util.ml + verit/veritParser.ml verit/veritLexer.ml verit/verit.ml 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 diff --git a/src/verit/smtlib2_ast.ml b/src/smtlib2/smtlib2_ast.ml index cce4625..cce4625 100644 --- a/src/verit/smtlib2_ast.ml +++ b/src/smtlib2/smtlib2_ast.ml diff --git a/src/verit/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml index f11d650..f11d650 100644 --- a/src/verit/smtlib2_genConstr.ml +++ b/src/smtlib2/smtlib2_genConstr.ml diff --git a/src/verit/smtlib2_lex.mll b/src/smtlib2/smtlib2_lex.mll index f235403..f235403 100644 --- a/src/verit/smtlib2_lex.mll +++ b/src/smtlib2/smtlib2_lex.mll diff --git a/src/verit/smtlib2_parse.mly b/src/smtlib2/smtlib2_parse.mly index b4e02a7..b4e02a7 100644 --- a/src/verit/smtlib2_parse.mly +++ b/src/smtlib2/smtlib2_parse.mly diff --git a/src/verit/smtlib2_util.ml b/src/smtlib2/smtlib2_util.ml index 1ce5e46..1ce5e46 100644 --- a/src/verit/smtlib2_util.ml +++ b/src/smtlib2/smtlib2_util.ml |