diff options
-rw-r--r-- | src/trace/coqTerms.ml | 3 | ||||
-rw-r--r-- | src/versions/native/smtcoq_plugin_native.ml4 | 7 | ||||
-rw-r--r-- | src/zchaff/zchaff.ml | 8 |
3 files changed, 16 insertions, 2 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index a58fcfa..6c76f9d 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -165,6 +165,9 @@ let cFite = gen_constant smt_modules "Fite" let cis_true = gen_constant smt_modules "is_true" +let cvalid_sat_checker = gen_constant [["SMTCoq";"Trace";"Sat_Checker"]] "valid" +let cinterp_var_sat_checker = gen_constant [["SMTCoq";"Trace";"Sat_Checker"]] "interp_var" + let make_certif_ops modules args = let gen_constant c = match args with diff --git a/src/versions/native/smtcoq_plugin_native.ml4 b/src/versions/native/smtcoq_plugin_native.ml4 index 6dae9dd..da0671e 100644 --- a/src/versions/native/smtcoq_plugin_native.ml4 +++ b/src/versions/native/smtcoq_plugin_native.ml4 @@ -30,6 +30,13 @@ VERNAC COMMAND EXTEND Vernac_zchaff ] END +VERNAC COMMAND EXTEND Vernac_zchaff_abs +| [ "Zchaff_Theorem_Abs" ident(name) string(fdimacs) string(fproof) ] -> + [ + Zchaff.theorem_abs 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) ] -> diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index 106c0b5..e7f842c 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -216,7 +216,7 @@ let ccertif = gen_constant sat_checker_modules "certif" let ctheorem_checker = gen_constant sat_checker_modules "theorem_checker" let cchecker = gen_constant sat_checker_modules "checker" -let theorem name fdimacs ftrace = +let theorems interp name fdimacs ftrace = SmtTrace.clear (); let _,first,last,reloc = import_cnf fdimacs in let d = make_roots first last in @@ -227,7 +227,7 @@ let theorem name fdimacs ftrace = let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in - let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots first last|] |] in + let theorem_concl = mklApp cnot [|mklApp cis_true [|interp d first last|] |] in let vtype = Term.mkProd(Names.Anonymous, Lazy.force cint, Lazy.force cbool) in let theorem_type = Term.mkProd (mkName "v", vtype, theorem_concl) in @@ -255,6 +255,10 @@ let theorem name fdimacs ftrace = let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in () +let theorem = theorems (fun _ -> interp_roots) +let theorem_abs = + theorems (fun d _ _ -> mklApp cvalid_sat_checker [|mklApp cinterp_var_sat_checker [|Term.mkRel 1(*v*)|]; d|]) + let checker fdimacs ftrace = SmtTrace.clear (); |