aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtForm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/trace/smtForm.ml')
-rw-r--r--src/trace/smtForm.ml84
1 files changed, 42 insertions, 42 deletions
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 6f26f24..2d68252 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -25,7 +25,7 @@ module type ATOM =
val is_bool_type : t -> bool
val is_bv_type : t -> bool
- val to_smt : Format.formatter -> t -> unit
+ val to_smt : ?debug:bool -> Format.formatter -> t -> unit
val logic : t -> logic
end
@@ -80,11 +80,11 @@ module type FORM =
val clear : reify -> unit
val get : ?declare:bool -> reify -> pform -> t
- (** Give a coq term, build the corresponding formula *)
- val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t
+ (** Given a coq term, build the corresponding formula *)
+ val of_coq : (CoqInterface.constr -> hatom) -> reify -> CoqInterface.constr -> t
val hash_hform : (hatom -> hatom) -> reify -> t -> t
- (** Flattening of [Fand] and [For], removing of [Fnot2] *)
+ (* Flattening of [Fand] and [For], removing of [Fnot2] *)
val flatten : reify -> t -> t
(** Turn n-ary [Fand] and [For] into their right-associative
@@ -93,20 +93,20 @@ module type FORM =
(** Producing Coq terms *)
- val to_coq : t -> Structures.constr
+ val to_coq : t -> CoqInterface.constr
val pform_tbl : reify -> pform array
val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
- val interp_tbl : reify -> Structures.constr * Structures.constr
+ val interp_tbl : reify -> CoqInterface.constr * CoqInterface.constr
val nvars : reify -> int
- (** Producing a Coq term corresponding to the interpretation
- of a formula *)
- (** [interp_atom] map [hatom] to coq term, it is better if it produce
- shared terms. *)
+ (* Producing a Coq term corresponding to the interpretation
+ of a formula *)
+ (* [interp_atom] map [hatom] to coq term, it is better if it produce
+ shared terms. *)
val interp_to_coq :
- (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
- t -> Structures.constr
+ (hatom -> CoqInterface.constr) -> (int, CoqInterface.constr) Hashtbl.t ->
+ t -> CoqInterface.constr
(* Unstratified terms *)
type atom_form_lit =
@@ -173,12 +173,12 @@ module Make (Atom:ATOM) =
to_smt_pform fmt hp.hval;
Format.fprintf fmt ")"
- and to_smt_pform fmt = function
- | Fatom a -> Atom.to_smt fmt a
+ and to_smt_pform ?(debug=false) fmt = function
+ | Fatom a -> Atom.to_smt ~debug:debug fmt a
| Fapp (op,args) -> to_smt_op fmt op args
(* This is an intermediate object of proofs, it correspond to nothing in SMT *)
| FbbT (a, l) ->
- Format.fprintf fmt "(bbT %a [" Atom.to_smt a;
+ Format.fprintf fmt "(bbT %a [" (Atom.to_smt ~debug:debug) a;
let fi = ref true in
List.iter (fun f -> Format.fprintf fmt "%s%a"
(if !fi then "" else "; ")
@@ -296,34 +296,34 @@ module Make (Atom:ATOM) =
let check pf =
match pf with
| Fatom ha -> if not (Atom.is_bool_type ha) then
- raise (Format.eprintf "nwt: %a" to_smt_pform pf;
+ raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf;
NotWellTyped pf)
| Fapp (op, args) ->
(match op with
| Ftrue | Ffalse ->
if Array.length args <> 0 then
- raise (Format.eprintf "nwt: %a" to_smt_pform pf;
+ raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf;
NotWellTyped pf)
| Fnot2 _ ->
if Array.length args <> 1 then
- raise (Format.eprintf "nwt: %a" to_smt_pform pf;
+ raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf;
NotWellTyped pf)
| Fand | For -> ()
| Fxor | Fimp | Fiff ->
if Array.length args <> 2 then
- raise (Format.eprintf "nwt: %a" to_smt_pform pf;
+ raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf;
NotWellTyped pf)
| Fite ->
if Array.length args <> 3 then
- raise (Format.eprintf "nwt: %a" to_smt_pform pf;
+ raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf;
NotWellTyped pf)
| Fforall l -> ()
)
| FbbT (ha, l) -> if not (Atom.is_bv_type ha) then
- raise (Format.eprintf "nwt: %a" to_smt_pform pf;
+ raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf;
NotWellTyped pf)
let declare reify pf =
@@ -368,9 +368,9 @@ module Make (Atom:ATOM) =
| CCunknown
module ConstrHash = struct
- type t = Structures.constr
- let equal = Structures.eq_constr
- let hash = Structures.hash_constr
+ type t = CoqInterface.constr
+ let equal = CoqInterface.eq_constr
+ let hash = CoqInterface.hash_constr
end
module ConstrHashtbl = Hashtbl.Make(ConstrHash)
@@ -393,7 +393,7 @@ module Make (Atom:ATOM) =
let get_cst c =
try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in
let rec mk_hform h =
- let c, args = Structures.decompose_app h in
+ let c, args = CoqInterface.decompose_app h in
match get_cst c with
| CCtrue -> get reify (Fapp(Ftrue,empty_args))
| CCfalse -> get reify (Fapp(Ffalse,empty_args))
@@ -408,7 +408,7 @@ module Make (Atom:ATOM) =
let l1 = mk_hform b1 in
let l2 = mk_hform b2 in
get reify (Fapp (Fimp, [|l1;l2|]))
- | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb")
+ | _ -> CoqInterface.error "SmtForm.Form.of_coq: wrong number of arguments for implb")
| CCifb ->
(* We should also be able to reify if then else *)
begin match args with
@@ -417,7 +417,7 @@ module Make (Atom:ATOM) =
let l2 = mk_hform b2 in
let l3 = mk_hform b3 in
get reify (Fapp (Fite, [|l1;l2;l3|]))
- | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
+ | _ -> CoqInterface.error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
end
| _ ->
let a = atom_of_coq h in
@@ -429,13 +429,13 @@ module Make (Atom:ATOM) =
let l1 = mk_hform b1 in
let l2 = mk_hform b2 in
get reify (f [|l1; l2|])
- | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments"
+ | _ -> CoqInterface.error "SmtForm.Form.of_coq: wrong number of arguments"
and mk_fnot i args =
match args with
| [t] ->
- let c,args = Structures.decompose_app t in
- if Structures.eq_constr c (Lazy.force cnegb) then
+ let c,args = CoqInterface.decompose_app t in
+ if CoqInterface.eq_constr c (Lazy.force cnegb) then
mk_fnot (i+1) args
else
let q,r = i lsr 1 , i land 1 in
@@ -443,31 +443,31 @@ module Make (Atom:ATOM) =
let l = if r = 0 then l else neg l in
if q = 0 then l
else get reify (Fapp(Fnot2 q, [|l|]))
- | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
+ | _ -> CoqInterface.error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
and mk_fand acc args =
match args with
| [t1;t2] ->
let l2 = mk_hform t2 in
- let c, args = Structures.decompose_app t1 in
- if Structures.eq_constr c (Lazy.force candb) then
+ let c, args = CoqInterface.decompose_app t1 in
+ if CoqInterface.eq_constr c (Lazy.force candb) then
mk_fand (l2::acc) args
else
let l1 = mk_hform t1 in
get reify (Fapp(Fand, Array.of_list (l1::l2::acc)))
- | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb"
+ | _ -> CoqInterface.error "SmtForm.Form.mk_hform: wrong number of arguments for andb"
and mk_for acc args =
match args with
| [t1;t2] ->
let l2 = mk_hform t2 in
- let c, args = Structures.decompose_app t1 in
- if Structures.eq_constr c (Lazy.force corb) then
+ let c, args = CoqInterface.decompose_app t1 in
+ if CoqInterface.eq_constr c (Lazy.force corb) then
mk_for (l2::acc) args
else
let l1 = mk_hform t1 in
get reify (Fapp(For, Array.of_list (l1::l2::acc)))
- | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
+ | _ -> CoqInterface.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
mk_hform c
@@ -546,7 +546,7 @@ module Make (Atom:ATOM) =
let args_to_coq args =
let cargs = Array.make (Array.length args + 1) (mkInt 0) in
Array.iteri (fun i hf -> cargs.(i) <- to_coq hf) args;
- Structures.mkArray (Lazy.force cint, cargs)
+ CoqTerms.mkArray (Lazy.force cint, cargs)
let pf_to_coq = function
| Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|]
@@ -586,12 +586,12 @@ module Make (Atom:ATOM) =
let interp_tbl reify =
let (i,t) = to_array reify (Lazy.force cFtrue) pf_to_coq in
- (mkInt i, Structures.mkArray (Lazy.force cform, t))
+ (mkInt i, CoqTerms.mkArray (Lazy.force cform, t))
let nvars reify = reify.count
- (** Producing a Coq term corresponding to the interpretation of a formula *)
- (** [interp_atom] map [Atom.t] to coq term, it is better if it produce
- shared terms. *)
+ (* Producing a Coq term corresponding to the interpretation of a formula *)
+ (* [interp_atom] map [Atom.t] to coq term, it is better if it produce
+ shared terms. *)
let interp_to_coq interp_atom form_tbl f =
let rec interp_form f =
let l = to_lit f in
generated by cgit (git 2.34.1) at 2024-06-17 22:58:55 +0000