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