diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-09-28 13:47:24 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-09-28 13:47:24 +0200 |
| commit | e54e5bbee68de0e6b1dce4cd5a99e991fe3cf84e (patch) | |
| tree | b199d791dfc94a6edac7b3f431bff05973c77ab8 /src/zchaff/zchaff.ml | |
| parent | a1421e02870ce0c976de4014ddcc6545a7aa4e22 (diff) | |
| download | smtcoq-e54e5bbee68de0e6b1dce4cd5a99e991fe3cf84e.tar.gz smtcoq-e54e5bbee68de0e6b1dce4cd5a99e991fe3cf84e.zip | |
Improved performance with coq-8.5
Diffstat (limited to 'src/zchaff/zchaff.ml')
| -rw-r--r-- | src/zchaff/zchaff.ml | 27 |
1 files changed, 19 insertions, 8 deletions
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index 74ae918..c9ed267 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -231,16 +231,27 @@ let theorem name fdimacs ftrace = let vtype = Term.mkProd(Names.Anonymous, Lazy.force cint, Lazy.force cbool) in let theorem_type = Term.mkProd (mkName "v", vtype, theorem_concl) in - let theorem_proof = - Term.mkLetIn (mkName "d", d, Lazy.force cdimacs, - Term.mkLetIn (mkName "c", certif, Lazy.force ccertif, - Term.mkLambda (mkName "v", vtype, - mklApp ctheorem_checker + let theorem_proof_cast = + Term.mkCast ( + Term.mkLetIn (mkName "d", d, Lazy.force cdimacs, + Term.mkLetIn (mkName "c", certif, Lazy.force ccertif, + Term.mkLambda (mkName "v", vtype, + mklApp ctheorem_checker [| Term.mkRel 3(*d*); Term.mkRel 2(*c*); - vm_cast_true + vm_cast_true (mklApp cchecker [|Term.mkRel 3(*d*); Term.mkRel 2(*c*)|]); - Term.mkRel 1(*v*)|]))) in - let ce = Structures.mkTConst theorem_proof theorem_type in + Term.mkRel 1(*v*)|]))), + Term.VMcast, + theorem_type) + in + let theorem_proof_nocast = + Term.mkLetIn (mkName "d", d, Lazy.force cdimacs, + Term.mkLetIn (mkName "c", certif, Lazy.force ccertif, + Term.mkLambda (mkName "v", vtype, + mklApp ctheorem_checker + [| Term.mkRel 3(*d*); Term.mkRel 2(*c*)|]))) + in + let ce = Structures.mkTConst theorem_proof_cast theorem_proof_nocast theorem_type in let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in () |