diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 17:49:19 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 17:49:19 +0200 |
| commit | efb15aacf1d1c1a8e7c80185bf199757a8edccd3 (patch) | |
| tree | 762c0506d8de0754622151fa758b81bdfc06e2bf /src/trace/smtForm.ml | |
| parent | dc6e8ccbc2f2596d832db44a322703575e0146c7 (diff) | |
| download | smtcoq-efb15aacf1d1c1a8e7c80185bf199757a8edccd3.tar.gz smtcoq-efb15aacf1d1c1a8e7c80185bf199757a8edccd3.zip | |
Tactic zchaff for 8.5
Diffstat (limited to 'src/trace/smtForm.ml')
| -rw-r--r-- | src/trace/smtForm.ml | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index c7856f3..a235859 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -272,9 +272,16 @@ module Make (Atom:ATOM) = | CCifb | CCunknown + module ConstrHash = struct + type t = Constr.constr + let equal = Constr.equal + let hash = Constr.hash + end + module ConstrHashtbl = Hashtbl.Make(ConstrHash) + let op_tbl () = - let tbl = Hashtbl.create 29 in - let add (c1,c2) = Hashtbl.add tbl (Lazy.force c1) c2 in + let tbl = ConstrHashtbl.create 29 in + let add (c1,c2) = ConstrHashtbl.add tbl (Lazy.force c1) c2 in List.iter add [ ctrue,CCtrue; cfalse,CCfalse; @@ -289,7 +296,7 @@ module Make (Atom:ATOM) = let of_coq atom_of_coq reify c = let op_tbl = Lazy.force op_tbl in let get_cst c = - try Hashtbl.find op_tbl c with Not_found -> CCunknown in + try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in let rec mk_hform h = let c, args = Term.decompose_app h in match get_cst c with @@ -308,7 +315,7 @@ module Make (Atom:ATOM) = get reify (Fapp (Fimp, [|l1;l2|])) | _ -> error "SmtForm.Form.of_coq: wrong number of arguments for implb") | CCifb -> - (* We should also be able to syntaxify if then else *) + (* We should also be able to reify if then else *) begin match args with | [b1;b2;b3] -> let l1 = mk_hform b1 in @@ -333,7 +340,7 @@ module Make (Atom:ATOM) = match args with | [t] -> let c,args = Term.decompose_app t in - if c = Lazy.force cnegb then + if Constr.equal c (Lazy.force cnegb) then mk_fnot (i+1) args else let q,r = i lsr 1 , i land 1 in @@ -348,7 +355,7 @@ module Make (Atom:ATOM) = | [t1;t2] -> let l2 = mk_hform t2 in let c, args = Term.decompose_app t1 in - if c = Lazy.force candb then + if Constr.equal c (Lazy.force candb) then mk_fand (l2::acc) args else let l1 = mk_hform t1 in @@ -360,7 +367,7 @@ module Make (Atom:ATOM) = | [t1;t2] -> let l2 = mk_hform t2 in let c, args = Term.decompose_app t1 in - if c = Lazy.force corb then + if Constr.equal c (Lazy.force corb) then mk_for (l2::acc) args else let l1 = mk_hform t1 in |