aboutsummaryrefslogtreecommitdiffstats
path: root/src/smtlib2/smtlib2_genConstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/smtlib2/smtlib2_genConstr.ml')
-rw-r--r--src/smtlib2/smtlib2_genConstr.ml296
1 files changed, 248 insertions, 48 deletions
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index 76dde25..692294d 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -1,13 +1,9 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2016 *)
+(* Copyright (C) 2011 - 2019 *)
(* *)
-(* Michaël Armand *)
-(* Benjamin Grégoire *)
-(* Chantal Keller *)
-(* *)
-(* Inria - École Polytechnique - Université Paris-Sud *)
+(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
@@ -42,45 +38,72 @@ let identifier_of_qualidentifier = function
| QualIdentifierId (_,id) | QualIdentifierAs (_,id,_) -> id
-let string_type s = match s with
- | "Bool" -> Tbool
- | "Int" -> TZ
- | _ -> VeritSyntax.get_btype s
-
+let string_type s =
+ match s with
+ | "Bool" -> fun _ -> Tbool
+ | "Int" -> fun _ -> TZ
+ | "Array" -> (function [ti;te] -> TFArray (ti, te) | _ -> assert false)
+ | _ ->
+ try Scanf.sscanf s "BitVec_%d%!" (fun size -> fun _ -> TBV size)
+ with _ -> fun _ -> VeritSyntax.get_btype s
-let sort_of_string s = (string_type s, [])
+let sort_of_string s = string_type s
let sort_of_symbol s = sort_of_string (string_of_symbol s)
+let rec bigint_binary_size acc i size =
+ let open Big_int in
+ if size = 0 then "#b" ^ String.concat "" acc
+ else
+ if eq_big_int i zero_big_int then
+ bigint_binary_size ("0" :: acc) i (size - 1)
+ else begin
+ assert (gt_big_int i zero_big_int && size > 0);
+ bigint_binary_size (string_of_big_int (and_big_int i unit_big_int) :: acc)
+ (shift_right_big_int i 1) (size - 1)
+ end
+
+let bigint_bv i size = bigint_binary_size [] i size
+
+
+exception DecimalBv of string
+
let string_of_identifier = function
| IdSymbol (_,s) -> (string_of_symbol s)
| IdUnderscoreSymNum (_,s,(_,l)) ->
- List.fold_left (fun c c' -> c^"_"^c') (string_of_symbol s) l
+ let s = string_of_symbol s in
+ let isbvdec =
+ try s.[0] = 'b' && s.[1]= 'v' with Invalid_argument _ -> false in
+ (match isbvdec, l with
+ (* rewrite bitvectors decimal constants *)
+ | true, [size] ->
+ let sbv =
+ Scanf.sscanf s "bv%s" (fun n ->
+ bigint_bv (Big_int.big_int_of_string n) (int_of_string size)) in
+ raise (DecimalBv sbv)
+ | _ -> List.fold_left (fun c c' -> c^"_"^c') s l
+ )
let string_of_qualidentifier id = string_of_identifier (identifier_of_qualidentifier id)
let rec sort_of_sort = function
- | SortIdentifier (_,id) -> sort_of_string (string_of_identifier id)
+ | SortIdentifier (_,id) -> sort_of_string (string_of_identifier id) []
| SortIdSortMulti (_,id,(_,l)) ->
- (string_type (string_of_identifier id), List.map sort_of_sort l)
+ sort_of_string (string_of_identifier id) (List.map sort_of_sort l)
let declare_sort rt sym =
let s = string_of_symbol sym in
let cons_t = declare_new_type (Names.id_of_string ("Smt_sort_"^s)) in
- let eq_t = declare_new_variable (Names.id_of_string ("eq_"^s)) (Term.mkArrow cons_t (Term.mkArrow cons_t (Lazy.force cbool))) in
- let x = mkName "x" in
- let y = mkName "y" in
- let rx = Term.mkRel 2 in
- let ry = Term.mkRel 1 in
- let eq_refl = Term.mkProd (x,cons_t,Term.mkProd (y,cons_t,mklApp creflect [|mklApp ceq [|cons_t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in
- let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl_"^s)) eq_refl in
- let ce = mklApp cTyp_eqb [|cons_t;eq_t;eq_refl_v|] in
- let res = declare rt cons_t ce in
+ let compdec_type = mklApp cCompDec [| cons_t |] in
+ let compdec_var =
+ declare_new_variable (Names.id_of_string ("CompDec_"^s)) compdec_type in
+ let ce = mklApp cTyp_compdec [|cons_t; compdec_var|] in
+ let res = SmtBtype.declare rt cons_t ce in
VeritSyntax.add_btype s res;
res
@@ -89,15 +112,27 @@ let declare_fun rt ro sym arg cod =
let s = string_of_symbol sym in
let tyl = List.map sort_of_sort arg in
let ty = sort_of_sort cod in
-
- let coqTy = List.fold_right (fun typ c -> Term.mkArrow (interp_to_coq rt (fst typ)) c) tyl (interp_to_coq rt (fst ty)) in
+ let coqTy = List.fold_right (fun typ c ->
+ Term.mkArrow (interp_to_coq rt typ) c)
+ tyl (interp_to_coq rt ty) in
let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy in
-
- let op = Op.declare ro cons_v (Array.of_list (List.map fst tyl)) (fst ty) None in
+ let op = Op.declare ro cons_v (Array.of_list tyl) ty None in
VeritSyntax.add_fun s op;
op
+
+let parse_smt2bv s =
+ let l = ref [] in
+ for i = 2 to String.length s - 1 do
+ match s.[i] with
+ | '0' -> l := false :: !l
+ | '1' -> l := true :: !l
+ | _ -> failwith "Not a bitvector"
+ done;
+ !l
+
+
let make_root_specconstant ra = function
| SpecConstsDec _ -> failwith "Smtlib2_genConstr.make_root_specconstant: decimals not implemented yet"
| SpecConstNum (_,s) ->
@@ -110,11 +145,15 @@ let make_root_specconstant ra = function
Atom.hatom_Z_of_bigint ra i)
| SpecConstString _ -> failwith "Smtlib2_genConstr.make_root_specconstant: strings not implemented yet"
| SpecConstsHex _ -> failwith "Smtlib2_genConstr.make_root_specconstant: hexadecimals not implemented yet"
- | SpecConstsBinary _ -> failwith "Smtlib2_genConstr.make_root_specconstant: binaries not implemented yet"
+ | SpecConstsBinary (_, s) -> Atom.mk_bvconst ra (parse_smt2bv s)
+
+
type atom_form = | Atom of SmtAtom.Atom.t | Form of SmtAtom.Form.t
+let startwith prefix s =
+ try Scanf.sscanf s (prefix ^^ "%_s") true with _ -> false
let make_root ra rf t =
@@ -122,11 +161,14 @@ let make_root ra rf t =
let rec make_root_term = function
| TermSpecConst (_,c) -> Atom (make_root_specconstant ra c)
- | TermQualIdentifier (_,id) ->
- let v = string_of_qualidentifier id in
- (try Hashtbl.find hlets v with
- | Not_found ->
- make_root_app v [])
+ | TermQualIdentifier (loc,id) ->
+ (try
+ let v = string_of_qualidentifier id in
+ (try Hashtbl.find hlets v with Not_found -> make_root_app v [])
+ with
+ | DecimalBv sbv ->
+ make_root_term (TermSpecConst (loc, SpecConstsBinary (loc, sbv)))
+ )
| TermQualIdTerm (_,id,(_,l)) ->
let v = string_of_qualidentifier id in
make_root_app v l
@@ -144,43 +186,162 @@ let make_root ra rf t =
match (v,l) with
| "=", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' ->
- (match Atom.type_of a' with
- | Tbool -> Form (Form.get rf (Fapp (Fiff, [|Form.get rf (Fatom a'); Form.get rf (Fatom b')|])))
- | ty -> Atom (Atom.mk_eq ra true ty a' b'))
- | _, _ -> assert false)
+ | Atom a', Atom b' when Atom.type_of a' <> Tbool ->
+ Atom (Atom.mk_eq ra (Atom.type_of a') a' b')
+ | _ -> Form (Form.get rf (Fapp (Fiff, [|make_root a; make_root b|])))
+ )
| "<", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_lt ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_lt ra a' b')
| _, _ -> assert false)
| "<=", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_le ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_le ra a' b')
| _, _ -> assert false)
| ">", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_gt ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_gt ra a' b')
| _, _ -> assert false)
| ">=", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_ge ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_ge ra a' b')
| _, _ -> assert false)
| "+", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_plus ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_plus ra a' b')
| _, _ -> assert false)
| "-", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_minus ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_minus ra a' b')
| _, _ -> assert false)
| "*", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_mult ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_mult ra a' b')
| _, _ -> assert false)
| "-", [a] ->
(match make_root_term a with
| Atom a' -> Atom (Atom.mk_opp ra a')
| _ -> assert false)
+ | "bvnot", [a] ->
+ (match make_root_term a with
+ | Atom a' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvnot ra s a')
+ | _ -> assert false)
+ | _ -> assert false)
+ | "bvneg", [a] ->
+ (match make_root_term a with
+ | Atom a' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvneg ra s a')
+ | _ -> assert false)
+ | _ -> assert false)
+ | "bvand", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvand ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvor", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvor ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvxor", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvxor ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvadd", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvadd ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvmul", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvmult ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvult", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvult ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvslt", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvslt ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvule", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom h1, Atom h2 ->
+ (match Atom.type_of h1 with
+ | TBV s ->
+ let a = Atom.mk_bvult ra s h2 h1 in
+ Form (Form.neg (Form.get rf (Fatom a)))
+ | _ -> assert false)
+ | _,_ -> assert false
+ )
+ | "bvsle", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom h1, Atom h2 ->
+ (match Atom.type_of h1 with
+ | TBV s ->
+ let a = Atom.mk_bvslt ra s h2 h1 in
+ Form (Form.neg (Form.get rf (Fatom a)))
+ | _ -> assert false)
+ | _,_ -> assert false
+ )
+ | "bvshl", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvshl ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvlshr", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvshr ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "concat", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a', Atom.type_of b' with
+ | TBV s1, TBV s2 -> Atom (Atom.mk_bvconcat ra s1 s2 a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "select", [a;i] ->
+ (match make_root_term a, make_root_term i with
+ | Atom a', Atom i' ->
+ (match Atom.type_of a' with
+ | TFArray (ti, te) -> Atom (Atom.mk_select ra ti te a' i')
+ | _ -> assert false)
+ | _ -> assert false)
+
+ | "store", [a;i;v] ->
+ (match make_root_term a, make_root_term i, make_root_term v with
+ | Atom a', Atom i', Atom v' ->
+ (match Atom.type_of a' with
+ | TFArray (ti, te) -> Atom (Atom.mk_store ra ti te a' i' v')
+ | _ -> assert false)
+ | _ -> assert false)
+
| "distinct", _ ->
let make_h h =
match make_root_term h with
@@ -205,10 +366,49 @@ let make_root ra rf t =
| "ite", _ ->
Form (Form.get rf (Fapp (Fite, Array.of_list (List.map make_root l))))
| "not", [a] -> Form (Form.neg (make_root a))
+
+ | _, [a] when startwith "extract_" v ->
+ (try
+ Scanf.sscanf v "extract_%s@_%d" (fun s i ->
+ let j = int_of_string s in
+ (match make_root_term a with
+ | Atom a' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvextr ra ~s ~i ~n:(j-i+1) a')
+ | _ -> assert false)
+ | _ -> assert false)
+ )
+ with _ -> assert false)
+
+ | _, [a] when startwith "zero_extend_" v ->
+ (try
+ Scanf.sscanf v "zero_extend_%d" (fun n ->
+ (match make_root_term a with
+ | Atom a' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvzextn ra ~s ~n a')
+ | _ -> assert false)
+ | _ -> assert false)
+ )
+ with _ -> assert false)
+
+ | _, [a] when startwith "sign_extend_" v ->
+ (try
+ Scanf.sscanf v "sign_extend_%d" (fun n ->
+ (match make_root_term a with
+ | Atom a' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvsextn ra ~s ~n a')
+ | _ -> assert false)
+ | _ -> assert false)
+ )
+ with _ -> assert false)
+
| _, _ ->
let op = VeritSyntax.get_fun v in
- let l' = List.map (fun t -> match make_root_term t with
- | Atom h -> h | Form _ -> assert false) l in
+ let l' = List.map (fun t ->
+ match make_root_term t with
+ | Atom h -> h | Form _ -> assert false) l in
Atom (Atom.get ra (Aapp (op, Array.of_list l')))
and make_root t =
generated by cgit (git 2.34.1) at 2024-06-29 03:51:41 +0000