aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/standard
diff options
context:
space:
mode:
Diffstat (limited to 'src/versions/standard')
-rw-r--r--src/versions/standard/Make11
-rw-r--r--src/versions/standard/Makefile10
-rw-r--r--src/versions/standard/smtcoq_plugin_standard.ml458
3 files changed, 69 insertions, 10 deletions
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 42d0552..c833f4d 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -15,7 +15,7 @@
## Change the "install" target: change CMO into CMX. ##
## Remove the automatically generated line with %.cmxs: %.cmx ##
## Finally, suppress the "Makefile" target and add to the "clean" target: ##
-## - rm -f ../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 ../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 smtcoq.a ##
########################################################################
@@ -40,11 +40,11 @@
-custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
-custom "" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" "ml"
--custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/standard/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 trace/smtCommands.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)"
+-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/standard/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 trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx" "$(CMXA)"
-custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
-CMXA = trace/smtcoq.cmxa
-CMXS = trace/smt_tactic.cmxs
+CMXA = smtcoq.cmxa
+CMXS = smtcoq_plugin.cmxs
CAMLLEX = $(CAMLBIN)ocamllex
CAMLYACC = $(CAMLBIN)ocamlyacc
@@ -70,7 +70,6 @@ trace/smtCommands.ml
trace/smtForm.ml
trace/smtForm.mli
trace/smtMisc.ml
-trace/smt_tactic.ml4
trace/smtTrace.ml
smtlib2/smtlib2_parse.ml
@@ -109,3 +108,5 @@ SMTCoq.v
SMT_terms.v
State.v
Trace.v
+
+smtcoq_plugin.ml4
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index cb92e59..da82e43 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -80,8 +80,8 @@ COQDOCLIBS?=\
# #
##########################
-CMXA=trace/smtcoq.cmxa
-CMXS=trace/smt_tactic.cmxs
+CMXA=smtcoq.cmxa
+CMXS=smtcoq_plugin.cmxs
CAMLLEX=$(CAMLBIN)ocamllex
CAMLYACC=$(CAMLBIN)ocamlyacc
@@ -207,7 +207,7 @@ GHTMLFILES:=$(VFILES:.v=.g.html)
OBJFILES=$(call vo_to_obj,$(VOFILES))
ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
-ML4FILES:=trace/smt_tactic.ml4
+ML4FILES:=smtcoq_plugin.ml4
ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
-include $(addsuffix .d,$(ML4FILES))
@@ -358,7 +358,7 @@ vtest:
ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml
-$(CMXA): versions/standard/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 trace/smtCommands.cmx verit/verit.cmx trace/smt_tactic.cmx
+$(CMXA): versions/standard/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 trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx
$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
$(CMXS): $(CMXA)
@@ -477,7 +477,7 @@ clean::
- rm -rf ml
- rm -rf $(CMXA)
- rm -rf $(CMXS)
- - rm -f ../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 ../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 smtcoq.a
cleanall:: clean
rm -f $(patsubst %.v,.%.aux,$(VFILES))
diff --git a/src/versions/standard/smtcoq_plugin_standard.ml4 b/src/versions/standard/smtcoq_plugin_standard.ml4
new file mode 100644
index 0000000..3666ee1
--- /dev/null
+++ b/src/versions/standard/smtcoq_plugin_standard.ml4
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+DECLARE PLUGIN "smtcoq_plugin"
+
+VERNAC COMMAND EXTEND Vernac_zchaff
+| [ "Parse_certif_zchaff"
+ ident(dimacs) ident(trace) string(fdimacs) string(fproof) ] ->
+ [
+ Zchaff.parse_certif dimacs trace fdimacs fproof
+ ]
+| [ "Zchaff_Checker" string(fdimacs) string(fproof) ] ->
+ [
+ Zchaff.checker fdimacs fproof
+ ]
+| [ "Zchaff_Theorem" ident(name) string(fdimacs) string(fproof) ] ->
+ [
+ Zchaff.theorem name fdimacs fproof
+ ]
+END
+
+VERNAC COMMAND EXTEND Vernac_verit
+| [ "Parse_certif_verit"
+ ident(t_i) ident(t_func) ident(t_atom) ident(t_form) ident(root) ident(used_roots) ident(trace) string(fsmt) string(fproof) ] ->
+ [
+ Verit.parse_certif t_i t_func t_atom t_form root used_roots trace fsmt fproof
+ ]
+| [ "Verit_Checker" string(fsmt) string(fproof) ] ->
+ [
+ Verit.checker fsmt fproof
+ ]
+| [ "Verit_Theorem" ident(name) string(fsmt) string(fproof) ] ->
+ [
+ Verit.theorem name fsmt fproof
+ ]
+END
+
+
+TACTIC EXTEND Tactic_zchaff
+| [ "zchaff" ] -> [ Structures.mk_sat_tactic Zchaff.tactic ]
+END
+
+TACTIC EXTEND Tactic_verit
+| [ "verit" ] -> [ Structures.mk_smt_tactic Verit.tactic ]
+END
generated by cgit (git 2.34.1) at 2024-07-01 13:38:43 +0000