From b1c21169e10e8a39db128e5be6d725ba0bf77af7 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Fri, 21 Jun 2024 10:53:14 +0200 Subject: [PATCH] Remove uncessary stuff and fix rebase --- lib/colibri2_mappings.default.ml | 38 +++++++++++++++++++++----------- lib/cvc5_mappings.default.ml | 2 +- lib/eval.ml | 2 +- lib/expr.ml | 28 +++-------------------- lib/expr.mli | 2 -- lib/mappings.ml | 23 +++++++------------ lib/ty.ml | 6 +---- lib/ty.mli | 2 -- lib/z3_mappings.default.ml | 23 ++++++------------- 9 files changed, 46 insertions(+), 80 deletions(-) diff --git a/lib/colibri2_mappings.default.ml b/lib/colibri2_mappings.default.ml index e3ad5b65..d29fa3df 100644 --- a/lib/colibri2_mappings.default.ml +++ b/lib/colibri2_mappings.default.ml @@ -184,7 +184,7 @@ module Fresh = struct | Ty_bitv 64 -> DTy.bitv 64 | Ty_fp 32 -> float32_ty | Ty_fp 64 -> float64_ty - | Ty_fp _ | Ty_bitv _ | Ty_list | Ty_array | Ty_tuple -> assert false + | Ty_fp _ | Ty_bitv _ | Ty_list | Ty_app -> assert false let tty_to_etype (ty : DTerm.ty) : Ty.t = match ty with @@ -412,7 +412,6 @@ module Fresh = struct let op' = match op with | At -> assert false - | Concat -> assert false | String_prefix -> assert false | String_suffix -> assert false | String_contains -> assert false @@ -657,7 +656,9 @@ module Fresh = struct | Ty.Ty_str -> Str.encode_unop | Ty.Ty_bitv _ -> Bv.encode_unop | Ty.Ty_fp _ -> Fp.encode_unop - | Ty.Ty_list | Ty_array | Ty_tuple -> assert false + | (Ty.Ty_list | Ty_app) as op -> + err "Colibri2_mappings: Trying to code unsupported op of type %a" Ty.pp + op let encode_binop = function | Ty.Ty_int -> I.encode_binop @@ -666,7 +667,9 @@ module Fresh = struct | Ty.Ty_str -> Str.encode_binop | Ty.Ty_bitv _ -> Bv.encode_binop | Ty.Ty_fp _ -> Fp.encode_binop - | Ty.Ty_list | Ty_array | Ty_tuple -> assert false + | (Ty.Ty_list | Ty_app) as op -> + err "Colibri2_mappings: Trying to code unsupported op of type %a" Ty.pp + op let encode_triop = function | Ty.Ty_int -> I.encode_triop @@ -675,7 +678,9 @@ module Fresh = struct | Ty.Ty_str -> Str.encode_triop | Ty.Ty_bitv _ -> Bv.encode_triop | Ty.Ty_fp _ -> Fp.encode_triop - | Ty.Ty_list | Ty_array | Ty_tuple -> assert false + | (Ty.Ty_list | Ty_app) as op -> + err "Colibri2_mappings: Trying to code unsupported op of type %a" Ty.pp + op let encode_relop = function | Ty.Ty_int -> I.encode_relop @@ -684,7 +689,9 @@ module Fresh = struct | Ty.Ty_str -> Str.encode_relop | Ty.Ty_bitv _ -> Bv.encode_relop | Ty.Ty_fp _ -> Fp.encode_relop - | Ty.Ty_list | Ty_array | Ty_tuple -> assert false + | (Ty.Ty_list | Ty_app) as op -> + err "Colibri2_mappings: Trying to code unsupported op of type %a" Ty.pp + op let encode_cvtop = function | Ty.Ty_int -> I.encode_cvtop @@ -693,7 +700,9 @@ module Fresh = struct | Ty.Ty_str -> Str.encode_cvtop | Ty.Ty_bitv sz -> Bv.encode_cvtop sz | Ty.Ty_fp sz -> Fp.encode_cvtop sz - | Ty.Ty_list | Ty_array | Ty_tuple -> assert false + | (Ty.Ty_list | Ty_app) as op -> + err "Colibri2_mappings: Trying to code unsupported op of type %a" Ty.pp + op (*let symbol_to_var v = DExpr.Term.Var.mk (Symbol.to_string v) (tty_of_etype (Symbol.type_of v))*) @@ -719,6 +728,10 @@ module Fresh = struct let base' = encode_val (Num (I32 base)) in let offset' = aux offset in DTerm.Bitv.add base' offset' + | Symbol s -> + let cst = tcst_of_symbol s in + record_sym cst; + DTerm.of_cst cst | Unop (ty, op, e) -> let e' = aux e in encode_unop ty op e' @@ -738,10 +751,7 @@ module Fresh = struct | Cvtop (ty, op, e) -> let e' = aux e in encode_cvtop ty op e' - | Symbol s -> - let cst = tcst_of_symbol s in - record_sym cst; - DTerm.of_cst cst + | Naryop _ -> err "Colibri2_mappings: Trying to encode naryop" | Extract (e, h, l) -> let e' = aux e in DTerm.Bitv.extract ((h * 8) - 1) (l * 8) e' @@ -749,7 +759,7 @@ module Fresh = struct let e1' = aux e1 and e2' = aux e2 in DTerm.Bitv.concat e1' e2' - | List _ | Array _ | Tuple _ | App _ -> assert false + | List _ | App _ -> assert false (* | Quantifier (t, vars, body, patterns) -> ( let body' = aux body in let encode_pattern (p : t list) = @@ -1024,7 +1034,9 @@ module Fresh = struct | 64 -> F64 (Int64.bits_of_float (Farith.F.to_float Farith.Mode.NE a)) | _ -> assert false ) ) ) - | Ty_str | Ty_list | Ty_array | Ty_tuple -> assert false + | Ty_str | Ty_list | Ty_app -> + err "Colibri2_mappings2: Unsuppoted model generation of type %a" Ty.pp + ty (* let value_of_const ((d, _l) : model) (e : Expr.t) : Value.t option = let e' = encore_expr_aux e in diff --git a/lib/cvc5_mappings.default.ml b/lib/cvc5_mappings.default.ml index 7b8a5ee8..320a2826 100644 --- a/lib/cvc5_mappings.default.ml +++ b/lib/cvc5_mappings.default.ml @@ -174,7 +174,7 @@ module Fresh_cvc5 () = struct let one = Term.mk_int tm 1 in Term.mk_term tm Kind.String_substr [| t; pos; one |] - let concat t1 t2 = Term.mk_term tm Kind.String_concat [| t1; t2 |] + let concat ts = Term.mk_term tm Kind.String_concat (Array.of_list ts) let contains t1 ~sub = Term.mk_term tm Kind.String_contains [| t1; sub |] diff --git a/lib/eval.ml b/lib/eval.ml index c7043ea3..30e315fa 100644 --- a/lib/eval.ml +++ b/lib/eval.ml @@ -972,7 +972,7 @@ let op int real bool str lst i32 i64 f32 f64 ty op = | Ty_bitv 64 -> i64 op | Ty_fp 32 -> f32 op | Ty_fp 64 -> f64 op - | Ty_bitv _ | Ty_fp _ | Ty_array | Ty_tuple | Ty_app -> assert false + | Ty_bitv _ | Ty_fp _ | Ty_app -> assert false [@@inline] let unop = diff --git a/lib/expr.ml b/lib/expr.ml index 4dd3d3fd..4fe4ca69 100644 --- a/lib/expr.ml +++ b/lib/expr.ml @@ -25,8 +25,6 @@ and expr = | Ptr of int32 * t | Symbol of Symbol.t | List of t list - | Array of t array - | Tuple of t list | App : [> `Op of string ] * t list -> expr | Unop of Ty.t * unop * t | Binop of Ty.t * binop * t * t @@ -49,9 +47,6 @@ module Expr = struct | Ptr (b1, o1), Ptr (b2, o2) -> b1 = b2 && o1 == o2 | Symbol s1, Symbol s2 -> Symbol.equal s1 s2 | List l1, List l2 -> list_eq l1 l2 - | Array a1, Array a2 -> - Array.(length a1 = length a2) && Array.for_all2 ( == ) a1 a2 - | Tuple l1, Tuple l2 -> list_eq l1 l2 | App (`Op x1, l1), App (`Op x2, l2) -> String.equal x1 x2 && list_eq l1 l2 | Unop (t1, op1, e1), Unop (t2, op2, e2) -> Ty.equal t1 t2 && op1 = op2 && e1 == e2 @@ -77,8 +72,6 @@ module Expr = struct | Ptr (b, o) -> h (b, o.tag) | Symbol s -> h s | List v -> h v - | Array es -> h es - | Tuple es -> h es | App (x, es) -> h (x, es) | Unop (ty, op, e) -> h (ty, op, e.tag) | Cvtop (ty, op, e) -> h (ty, op, e.tag) @@ -114,8 +107,6 @@ let rec ty (hte : t) : Ty.t = | Ptr _ -> Ty_bitv 32 | Symbol x -> Symbol.type_of x | List _ -> Ty_list - | Array _ -> Ty_array - | Tuple _ -> Ty_tuple | App _ -> assert false | Unop (ty, _, _) -> ty | Binop (ty, _, _, _) -> ty @@ -134,8 +125,7 @@ let rec is_symbolic (v : t) : bool = | Val _ -> false | Symbol _ -> true | Ptr (_, offset) -> is_symbolic offset - | List vs | Tuple vs -> List.exists is_symbolic vs - | Array vs -> Array.exists is_symbolic vs + | List vs -> List.exists is_symbolic vs | App (_, vs) -> List.exists is_symbolic vs | Unop (_, _, v) -> is_symbolic v | Binop (_, _, v1, v2) -> is_symbolic v1 || is_symbolic v2 @@ -154,8 +144,7 @@ let get_symbols (hte : t list) = | Val _ -> () | Ptr (_, offset) -> symbols offset | Symbol s -> Hashtbl.replace tbl s () - | List es | Tuple es -> List.iter symbols es - | Array es -> Array.iter symbols es + | List es -> List.iter symbols es | App (_, es) -> List.iter symbols es | Unop (_, _, e1) -> symbols e1 | Binop (_, _, e1, e2) -> @@ -198,21 +187,12 @@ let negate_relop (hte : t) : (t, string) Result.t = module Pp = struct open Format - let pp_print_array pp_v fmt v = - let is_first = ref true in - Array.iter - (fun v -> - if !is_first then is_first := false else pp_print_string fmt " "; - pp_v fmt v ) - v - let rec pp fmt (hte : t) = match view hte with | Val v -> Value.pp fmt v | Ptr (base, offset) -> fprintf fmt "(Ptr (i32 %ld) %a)" base pp offset | Symbol s -> Symbol.pp fmt s - | List v | Tuple v -> fprintf fmt "(%a)" (pp_print_list pp) v - | Array v -> fprintf fmt "(%a)" (pp_print_array pp) v + | List v -> fprintf fmt "(%a)" (pp_print_list pp) v | App (`Op x, v) -> fprintf fmt "(%s %a)" x (pp_print_list pp) v | Unop (ty, op, e) -> fprintf fmt "(%a.%a %a)" Ty.pp ty pp_unop op pp e | Binop (ty, op, e1, e2) -> @@ -486,8 +466,6 @@ let rec simplify_expr ?(rm_extract = true) (hte : t) : t = | Val _ | Symbol _ -> hte | Ptr (base, offset) -> make @@ Ptr (base, simplify_expr offset) | List es -> make @@ List (List.map simplify_expr es) - | Array es -> make @@ Array (Array.map simplify_expr es) - | Tuple es -> make @@ Tuple (List.map simplify_expr es) | App (x, es) -> make @@ App (x, List.map simplify_expr es) | Unop (ty, op, e) -> let e = simplify_expr e in diff --git a/lib/expr.mli b/lib/expr.mli index c356c796..1bfd7e6b 100644 --- a/lib/expr.mli +++ b/lib/expr.mli @@ -24,8 +24,6 @@ and expr = | Ptr of int32 * t | Symbol of Symbol.t | List of t list - | Array of t array - | Tuple of t list | App : [> `Op of string ] * t list -> expr | Unop of Ty.t * Ty.unop * t | Binop of Ty.t * Ty.binop * t * t diff --git a/lib/mappings.ml b/lib/mappings.ml index 58f4c695..27cbd7ef 100644 --- a/lib/mappings.ml +++ b/lib/mappings.ml @@ -63,8 +63,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct | Ty_bitv 64 -> i64 | Ty_fp 32 -> f32 | Ty_fp 64 -> f64 - | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app -> - assert false + | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false let make_symbol (symbol_table : sym_tbl) (s : Symbol.t) : M.term = match Hashtbl.find_opt symbol_table s with @@ -487,8 +486,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct | Ty.Ty_bitv 64 -> I64.unop | Ty.Ty_fp 32 -> Float32_impl.unop | Ty.Ty_fp 64 -> Float64_impl.unop - | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app -> - assert false + | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false let binop = function | Ty.Ty_int -> Int_impl.binop @@ -500,8 +498,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct | Ty.Ty_bitv 64 -> I64.binop | Ty.Ty_fp 32 -> Float32_impl.binop | Ty.Ty_fp 64 -> Float64_impl.binop - | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app -> - assert false + | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false let triop = function | Ty.Ty_int | Ty.Ty_real -> assert false @@ -512,8 +509,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct | Ty.Ty_bitv 64 -> I64.triop | Ty.Ty_fp 32 -> Float32_impl.triop | Ty.Ty_fp 64 -> Float64_impl.triop - | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app -> - assert false + | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false let relop = function | Ty.Ty_int -> Int_impl.relop @@ -525,8 +521,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct | Ty.Ty_bitv 64 -> I64.relop | Ty.Ty_fp 32 -> Float32_impl.relop | Ty.Ty_fp 64 -> Float64_impl.relop - | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app -> - assert false + | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false let cvtop = function | Ty.Ty_int -> Int_impl.cvtop @@ -538,8 +533,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct | Ty.Ty_bitv 64 -> I64.cvtop | Ty.Ty_fp 32 -> Float32_impl.cvtop | Ty.Ty_fp 64 -> Float64_impl.cvtop - | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app -> - assert false + | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false let naryop = function | Ty.Ty_str -> String_impl.naryop @@ -582,7 +576,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct let e1 = encode_expr symbol_table e1 in let e2 = encode_expr symbol_table e2 in M.Bitv.concat e1 e2 - | List _ | Array _ | Tuple _ | App _ -> assert false + | List _ | App _ -> assert false (* TODO: pp_smt *) let pp_smt ?status:_ _ _ = assert false @@ -611,8 +605,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct | Ty_fp 64 -> let float = M.Interp.to_float v 11 53 in Value.Num (F64 (Int64.bits_of_float float)) - | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app -> - assert false + | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false let value ({ model = m; symbol_table } : model) (c : Expr.t) : Value.t = value_of_term m (Expr.ty c) (encode_expr symbol_table c) diff --git a/lib/ty.ml b/lib/ty.ml index e6118a64..a8eab4a6 100644 --- a/lib/ty.ml +++ b/lib/ty.ml @@ -33,8 +33,6 @@ type t = | Ty_bitv of int | Ty_fp of int | Ty_list - | Ty_tuple - | Ty_array | Ty_app type unop = @@ -274,8 +272,6 @@ let pp fmt = function | Ty_bitv n -> fprintf fmt "i%d" n | Ty_fp n -> fprintf fmt "f%d" n | Ty_list -> pp_string fmt "list" - | Ty_tuple -> pp_string fmt "tuple" - | Ty_array -> pp_string fmt "array" | Ty_app -> pp_string fmt "app" let pp_logic fmt : logic -> unit = function @@ -319,4 +315,4 @@ let size (ty : t) : int = match ty with | Ty_bitv n | Ty_fp n -> n / 8 | Ty_int | Ty_bool -> 4 - | Ty_real | Ty_str | Ty_list | Ty_array | Ty_tuple | Ty_app -> assert false + | Ty_real | Ty_str | Ty_list | Ty_app -> assert false diff --git a/lib/ty.mli b/lib/ty.mli index 180412e2..d9e7ec50 100644 --- a/lib/ty.mli +++ b/lib/ty.mli @@ -29,8 +29,6 @@ type t = | Ty_bitv of int | Ty_fp of int | Ty_list - | Ty_tuple - | Ty_array | Ty_app type unop = diff --git a/lib/z3_mappings.default.ml b/lib/z3_mappings.default.ml index e80a5c9c..6fa63334 100644 --- a/lib/z3_mappings.default.ml +++ b/lib/z3_mappings.default.ml @@ -71,8 +71,7 @@ module Fresh = struct | Ty_bitv 64 -> bv64_sort | Ty_fp 32 -> fp32_sort | Ty_fp 64 -> fp64_sort - | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_tuple | Ty_array | Ty_app -> - assert false + | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false module Arithmetic = struct open Ty @@ -505,8 +504,7 @@ module Fresh = struct | Ty.Ty_bitv 64 -> I64.encode_unop | Ty.Ty_fp 32 -> F32.encode_unop | Ty.Ty_fp 64 -> F64.encode_unop - | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app -> - assert false + | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false let encode_binop = function | Ty.Ty_int | Ty.Ty_real -> Arithmetic.encode_binop @@ -517,8 +515,7 @@ module Fresh = struct | Ty.Ty_bitv 64 -> I64.encode_binop | Ty.Ty_fp 32 -> F32.encode_binop | Ty.Ty_fp 64 -> F64.encode_binop - | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app -> - assert false + | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false let encode_triop = function | Ty.Ty_int | Ty_real -> Arithmetic.encode_triop @@ -529,8 +526,7 @@ module Fresh = struct | Ty.Ty_bitv 64 -> I64.encode_triop | Ty.Ty_fp 32 -> F32.encode_triop | Ty.Ty_fp 64 -> F64.encode_triop - | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app -> - assert false + | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false let encode_relop = function | Ty.Ty_int | Ty.Ty_real -> Arithmetic.encode_relop @@ -541,8 +537,7 @@ module Fresh = struct | Ty.Ty_bitv 64 -> I64.encode_relop | Ty.Ty_fp 32 -> F32.encode_relop | Ty.Ty_fp 64 -> F64.encode_relop - | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app -> - assert false + | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false let encode_cvtop = function | Ty.Ty_int -> Arithmetic.Integer.encode_cvtop @@ -554,8 +549,7 @@ module Fresh = struct | Ty.Ty_bitv 64 -> I64.encode_cvtop | Ty.Ty_fp 32 -> F32.encode_cvtop | Ty.Ty_fp 64 -> F64.encode_cvtop - | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app -> - assert false + | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false let encode_naryop = function | Ty.Ty_bool -> Boolean.encode_naryop @@ -586,10 +580,6 @@ module Fresh = struct let open Expr in match view hte with | Val v -> encode_val v - | List _es -> assert false - | Tuple _es -> assert false - | Array _es -> assert false - | App _ -> assert false | Ptr (base, offset) -> let base' = encode_val (Num (I32 base)) in let offset' = encode_expr offset in @@ -624,6 +614,7 @@ module Fresh = struct let e1' = encode_expr e1 and e2' = encode_expr e2 in Z3.BitVector.mk_concat ctx e1' e2' + | List _ | App _ -> assert false (* | Quantifier (t, vars, body, patterns) -> *) (* let body' = encode_expr body in *) (* let encode_pattern p = *)