aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--3rdparty/alt-ergo/smtlib2_ast.ml (renamed from src/smtlib2/smtlib2_ast.ml)0
-rw-r--r--3rdparty/alt-ergo/smtlib2_ast.mli (renamed from src/smtlib2/smtlib2_ast.mli)0
-rw-r--r--3rdparty/alt-ergo/smtlib2_lex.mll (renamed from src/smtlib2/smtlib2_lex.mll)0
-rw-r--r--3rdparty/alt-ergo/smtlib2_parse.mly (renamed from src/smtlib2/smtlib2_parse.mly)0
-rw-r--r--3rdparty/alt-ergo/smtlib2_util.ml (renamed from src/smtlib2/smtlib2_util.ml)0
-rw-r--r--3rdparty/alt-ergo/smtlib2_util.mli (renamed from src/smtlib2/smtlib2_util.mli)0
-rw-r--r--src/Tactics.v65
-rw-r--r--src/versions/native/Make24
-rw-r--r--src/versions/native/Makefile32
-rw-r--r--src/versions/standard/Makefile.local2
-rw-r--r--src/versions/standard/_CoqProject18
11 files changed, 106 insertions, 35 deletions
diff --git a/src/smtlib2/smtlib2_ast.ml b/3rdparty/alt-ergo/smtlib2_ast.ml
index 65dc3e3..65dc3e3 100644
--- a/src/smtlib2/smtlib2_ast.ml
+++ b/3rdparty/alt-ergo/smtlib2_ast.ml
diff --git a/src/smtlib2/smtlib2_ast.mli b/3rdparty/alt-ergo/smtlib2_ast.mli
index 3d3f126..3d3f126 100644
--- a/src/smtlib2/smtlib2_ast.mli
+++ b/3rdparty/alt-ergo/smtlib2_ast.mli
diff --git a/src/smtlib2/smtlib2_lex.mll b/3rdparty/alt-ergo/smtlib2_lex.mll
index 2b965af..2b965af 100644
--- a/src/smtlib2/smtlib2_lex.mll
+++ b/3rdparty/alt-ergo/smtlib2_lex.mll
diff --git a/src/smtlib2/smtlib2_parse.mly b/3rdparty/alt-ergo/smtlib2_parse.mly
index d618a1a..d618a1a 100644
--- a/src/smtlib2/smtlib2_parse.mly
+++ b/3rdparty/alt-ergo/smtlib2_parse.mly
diff --git a/src/smtlib2/smtlib2_util.ml b/3rdparty/alt-ergo/smtlib2_util.ml
index d503145..d503145 100644
--- a/src/smtlib2/smtlib2_util.ml
+++ b/3rdparty/alt-ergo/smtlib2_util.ml
diff --git a/src/smtlib2/smtlib2_util.mli b/3rdparty/alt-ergo/smtlib2_util.mli
index b4e8916..b4e8916 100644
--- a/src/smtlib2/smtlib2_util.mli
+++ b/3rdparty/alt-ergo/smtlib2_util.mli
diff --git a/src/Tactics.v b/src/Tactics.v
new file mode 100644
index 0000000..95b92d6
--- /dev/null
+++ b/src/Tactics.v
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+Require Import PropToBool BoolToProp. (* Before SMTCoq.State *)
+Require Import Int63 List PArray Bool ZArith.
+Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances QInst.
+
+Declare ML Module "smtcoq_plugin".
+
+
+Tactic Notation "verit_bool" constr_list(h) :=
+ verit_bool_base h; vauto.
+
+Tactic Notation "verit_bool_no_check" constr_list(h) :=
+ verit_bool_no_check_base h; vauto.
+
+
+(** Tactics in Prop **)
+
+Ltac zchaff := prop2bool; zchaff_bool; bool2prop.
+Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop.
+
+Tactic Notation "verit" constr_list(h) := prop2bool; verit_bool h; bool2prop.
+Tactic Notation "verit_no_check" constr_list(h) := prop2bool; verit_bool_no_check h; bool2prop.
+
+Ltac cvc4 := prop2bool; cvc4_bool; bool2prop.
+Ltac cvc4_no_check := prop2bool; cvc4_bool_no_check; bool2prop.
+
+
+(* Ltac smt := prop2bool; *)
+(* repeat *)
+(* match goal with *)
+(* | [ |- context[ CompDec ?t ] ] => try assumption *)
+(* | [ |- _ : bool] => verit_bool *)
+(* | [ |- _ : bool] => try (cvc4_bool; verit_bool) *)
+(* end; *)
+(* bool2prop. *)
+(* Ltac smt_no_check := prop2bool; *)
+(* repeat *)
+(* match goal with *)
+(* | [ |- context[ CompDec ?t ] ] => try assumption *)
+(* | [ |- _ : bool] => verit_bool_no_check *)
+(* | [ |- _ : bool] => try (cvc4_bool_no_check; verit_bool_no_check) *)
+(* end; *)
+(* bool2prop. *)
+
+Tactic Notation "smt" constr_list(h) := (prop2bool; try verit_bool h; cvc4_bool; try verit_bool h; bool2prop).
+Tactic Notation "smt_no_check" constr_list(h) := (prop2bool; try verit_bool_no_check h; cvc4_bool_no_check; try verit_bool_no_check h; bool2prop).
+
+
+
+(*
+ Local Variables:
+ coq-load-path: ((rec "." "SMTCoq"))
+ End:
+*)
diff --git a/src/versions/native/Make b/src/versions/native/Make
index f45eb72..f28d1c9 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -17,7 +17,7 @@
## change CMXSFILES into CMXS and add the same block for CMXA and VCMXS. ##
## 4) Change the "install" target: change CMOFILES into CMXFILES. ##
## 5) 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 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 ##
+## - 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 ../3rdparty/alt-ergo/smtlib2_parse.mli ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli trace/smtcoq.a ##
########################################################################
@@ -35,6 +35,7 @@
-I verit
-I zchaff
-I versions/native
+-I ../3rdparty/alt-ergo
-custom "cd ../unit-tests; make vernac" "" "test"
@@ -43,9 +44,9 @@
-custom "$(CAMLLEX) $<" "%.mll" "%.ml"
-custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
--custom "" "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"
+-custom "" "verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml" "ml"
--custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "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" "$(CMXA)"
+-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "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 ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/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" "$(CMXA)"
-custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
CMXA = smtcoq.cmxa
@@ -88,16 +89,17 @@ trace/smtMisc.mli
trace/smtTrace.ml
trace/smtTrace.mli
-smtlib2/smtlib2_parse.ml
-smtlib2/smtlib2_parse.mli
-smtlib2/smtlib2_lex.ml
-smtlib2/smtlib2_lex.mli
-smtlib2/smtlib2_ast.ml
-smtlib2/smtlib2_ast.mli
+../3rdparty/alt-ergo/smtlib2_parse.ml
+../3rdparty/alt-ergo/smtlib2_parse.mli
+../3rdparty/alt-ergo/smtlib2_lex.ml
+../3rdparty/alt-ergo/smtlib2_lex.mli
+../3rdparty/alt-ergo/smtlib2_ast.ml
+../3rdparty/alt-ergo/smtlib2_ast.mli
+../3rdparty/alt-ergo/smtlib2_util.ml
+../3rdparty/alt-ergo/smtlib2_util.mli
+
smtlib2/smtlib2_genConstr.ml
smtlib2/smtlib2_genConstr.mli
-smtlib2/smtlib2_util.ml
-smtlib2/smtlib2_util.mli
smtlib2/sExprParser.ml
smtlib2/sExprParser.mli
smtlib2/sExprLexer.ml
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
index 3c6bf30..3f0d0f6 100644
--- a/src/versions/native/Makefile
+++ b/src/versions/native/Makefile
@@ -39,7 +39,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
# #
##########################
-OCAMLLIBS?=-I versions/native\
+OCAMLLIBS?=-I ../3rdparty/alt-ergo\
+ -I versions/native\
-I zchaff\
-I verit\
-I trace\
@@ -51,7 +52,8 @@ OCAMLLIBS?=-I versions/native\
-I array\
-I classes\
-I bva
-COQLIBS?=-I versions/native\
+COQLIBS?=-I ../3rdparty/alt-ergo\
+ -I versions/native\
-I zchaff\
-I verit\
-I trace\
@@ -206,11 +208,11 @@ MLFILES:=lia/lia.ml\
smtlib2/sExpr.ml\
smtlib2/sExprLexer.ml\
smtlib2/sExprParser.ml\
- smtlib2/smtlib2_util.ml\
smtlib2/smtlib2_genConstr.ml\
- smtlib2/smtlib2_ast.ml\
- smtlib2/smtlib2_lex.ml\
- smtlib2/smtlib2_parse.ml\
+ ../3rdparty/alt-ergo/smtlib2_util.ml\
+ ../3rdparty/alt-ergo/smtlib2_ast.ml\
+ ../3rdparty/alt-ergo/smtlib2_lex.ml\
+ ../3rdparty/alt-ergo/smtlib2_parse.ml\
trace/smtTrace.ml\
trace/smtMisc.ml\
trace/smtForm.ml\
@@ -243,11 +245,11 @@ MLIFILES:=lia/lia.mli\
smtlib2/smtlib2_solver.mli\
smtlib2/sExpr.mli\
smtlib2/sExprParser.mli\
- smtlib2/smtlib2_util.mli\
smtlib2/smtlib2_genConstr.mli\
- smtlib2/smtlib2_ast.mli\
- smtlib2/smtlib2_lex.mli\
- smtlib2/smtlib2_parse.mli\
+ ../3rdparty/alt-ergo/smtlib2_util.mli\
+ ../3rdparty/alt-ergo/smtlib2_ast.mli\
+ ../3rdparty/alt-ergo/smtlib2_lex.mli\
+ ../3rdparty/alt-ergo/smtlib2_parse.mli\
trace/smtTrace.mli\
trace/smtMisc.mli\
trace/smtForm.mli\
@@ -327,10 +329,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 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
+$(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 ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/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 smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
+ml: verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
%.ml %.mli: %.mly
@@ -368,11 +370,11 @@ install-natdynlink:
install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
done
- for i in $(CMXA); do \
+ for i in $(VCMXS); do \
install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
done
- for i in $(VCMXS); do \
+ for i in $(CMXA); do \
install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
done
@@ -417,7 +419,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 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
+ - 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 ../3rdparty/alt-ergo/smtlib2_parse.mli ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/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
diff --git a/src/versions/standard/Makefile.local b/src/versions/standard/Makefile.local
index 095564d..045af88 100644
--- a/src/versions/standard/Makefile.local
+++ b/src/versions/standard/Makefile.local
@@ -30,4 +30,4 @@ CAMLYACC = $(CAMLBIN)ocamlyacc
$(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
+smtcoq_plugin.mlpack.d : verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject
index f283e00..8b88cb5 100644
--- a/src/versions/standard/_CoqProject
+++ b/src/versions/standard/_CoqProject
@@ -29,6 +29,7 @@
-I versions/standard
-I versions/standard/Int63
-I versions/standard/Array
+-I ../3rdparty/alt-ergo
versions/standard/Int63/Int63.v
versions/standard/Int63/Int63Native.v
@@ -74,16 +75,17 @@ trace/smtMisc.mli
trace/smtTrace.ml
trace/smtTrace.mli
-smtlib2/smtlib2_parse.ml
-smtlib2/smtlib2_parse.mli
-smtlib2/smtlib2_lex.ml
-smtlib2/smtlib2_lex.mli
-smtlib2/smtlib2_ast.ml
-smtlib2/smtlib2_ast.mli
+../3rdparty/alt-ergo/smtlib2_parse.ml
+../3rdparty/alt-ergo/smtlib2_parse.mli
+../3rdparty/alt-ergo/smtlib2_lex.ml
+../3rdparty/alt-ergo/smtlib2_lex.mli
+../3rdparty/alt-ergo/smtlib2_ast.ml
+../3rdparty/alt-ergo/smtlib2_ast.mli
+../3rdparty/alt-ergo/smtlib2_util.ml
+../3rdparty/alt-ergo/smtlib2_util.mli
+
smtlib2/smtlib2_genConstr.ml
smtlib2/smtlib2_genConstr.mli
-smtlib2/smtlib2_util.ml
-smtlib2/smtlib2_util.mli
smtlib2/sExpr.ml
smtlib2/sExpr.mli
smtlib2/smtlib2_solver.ml
generated by cgit (git 2.34.1) at 2024-06-02 08:56:56 +0000