diff options
Diffstat (limited to 'src/versions/native/Makefile')
| -rw-r--r-- | src/versions/native/Makefile | 56 |
1 files changed, 50 insertions, 6 deletions
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile index 61c8c01..afc5523 100644 --- a/src/versions/native/Makefile +++ b/src/versions/native/Makefile @@ -45,16 +45,24 @@ OCAMLLIBS?=-I versions/native\ -I trace\ -I smtlib2\ -I lia\ + -I lfsc\ -I euf\ - -I cnf + -I cnf\ + -I array\ + -I classes\ + -I bva COQLIBS?=-I versions/native\ -I zchaff\ -I verit\ -I trace\ -I smtlib2\ -I lia\ + -I lfsc\ -I euf\ - -I cnf -R . SMTCoq + -I cnf\ + -I array\ + -I classes\ + -I bva -R . SMTCoq COQDOCLIBS?=-R . SMTCoq ########################## @@ -137,6 +145,10 @@ endif VFILES:=Trace.v\ State.v\ SMT_terms.v\ + Tactics.v\ + BoolToProp.v\ + PropToBool.v\ + ReflectFacts.v\ SMTCoq.v\ Misc.v\ Conversion_tactics.v\ @@ -147,7 +159,13 @@ VFILES:=Trace.v\ lia/Lia.v\ euf/Euf.v\ cnf/Cnf.v\ - versions/native/Structures.v + versions/native/Structures.v\ + array/Array_checker.v\ + array/FArray.v\ + classes/SMT_classes_instances.v\ + classes/SMT_classes.v\ + bva/Bva_checker.v\ + bva/BVList.v -include $(addsuffix .d,$(VFILES)) .SECONDARY: $(addsuffix .d,$(VFILES)) @@ -170,10 +188,24 @@ MLFILES:=lia/lia.ml\ zchaff/zchaff.ml\ zchaff/satParser.ml\ zchaff/cnfParser.ml\ + lfsc/lfsc.ml\ + lfsc/converter.ml\ + lfsc/tosmtcoq.ml\ + lfsc/builtin.ml\ + lfsc/ast.ml\ + lfsc/type.ml\ + lfsc/lfscLexer.ml\ + lfsc/lfscParser.ml\ + lfsc/hstring.ml\ + lfsc/shashcons.ml\ verit/veritSyntax.ml\ verit/verit.ml\ verit/veritLexer.ml\ verit/veritParser.ml\ + smtlib2/smtlib2_solver.ml\ + smtlib2/sExpr.ml\ + smtlib2/sExprLexer.ml\ + smtlib2/sExprParser.ml\ smtlib2/smtlib2_util.ml\ smtlib2/smtlib2_genConstr.ml\ smtlib2/smtlib2_ast.ml\ @@ -199,10 +231,18 @@ MLIFILES:=lia/lia.mli\ zchaff/zchaff.mli\ zchaff/satParser.mli\ zchaff/cnfParser.mli\ + lfsc/tosmtcoq.mli\ + lfsc/translator_sig.mli\ + lfsc/ast.mli\ + lfsc/hstring.mli\ + lfsc/shashcons.mli\ verit/veritSyntax.mli\ verit/verit.mli\ verit/veritLexer.mli\ verit/veritParser.mli\ + smtlib2/smtlib2_solver.mli\ + smtlib2/sExpr.mli\ + smtlib2/sExprParser.mli\ smtlib2/smtlib2_util.mli\ smtlib2/smtlib2_genConstr.mli\ smtlib2/smtlib2_ast.mli\ @@ -287,10 +327,10 @@ beautify: $(VFILES:=.beautified) $(CMXS): $(CMXA) $(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^ -$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.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 trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx +$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.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 smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx $(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^ -ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml +ml: 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 %.ml %.mli: %.mly @@ -299,6 +339,9 @@ ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/sm %.ml: %.mll $(CAMLLEX) $< +lfsctest: + cd ../unit-tests; make lfsc + vtest: cd ../unit-tests; make verit @@ -374,10 +417,11 @@ clean: - rm -rf $(CMXS) - rm -rf $(CMXA) - rm -rf ml + - rm -rf lfsctest - 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 smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/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 smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli trace/smtcoq.a archclean: rm -f *.cmx *.o |