Command to bypass typechecking when generating a zchaff theorem

1 files changed, 6 insertions, 2 deletions

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 ();