diff options
Diffstat (limited to 'src/trace/smt_tactic.ml4')
| -rw-r--r-- | src/trace/smt_tactic.ml4 | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/src/trace/smt_tactic.ml4 b/src/trace/smt_tactic.ml4 new file mode 100644 index 0000000..219810d --- /dev/null +++ b/src/trace/smt_tactic.ml4 @@ -0,0 +1,55 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +VERNAC COMMAND EXTEND Parse_certif_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 Parse_certif_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 zchaff +| [ "zchaff" ] -> [ Zchaff.tactic ] +END + +TACTIC EXTEND verit +| [ "verit" ] -> [ Verit.tactic ] +END |