diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml deleted file mode 100644 index bc6c2a452..000000000 --- a/src/lib/reasoners/records.ml +++ /dev/null @@ -1,420 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -module E = Expr -module Sy = Symbols -module DE = Dolmen.Std.Expr - -type 'a abstract = - | Record of (DE.term_cst * 'a abstract) list * Ty.t - | Access of DE.term_cst * 'a abstract * Ty.t - | Other of 'a * Ty.t - -module type ALIEN = sig - include Sig.X - val embed : r abstract -> r - val extract : r -> (r abstract) option -end - -module Shostak (X : ALIEN) = struct - - module XS = Set.Make(struct type t = X.r let compare = X.hash_cmp end) - - let name = "records" - - let timer = Timers.M_Records - - type t = X.r abstract - type r = X.r - - (*BISECT-IGNORE-BEGIN*) - module Debug = struct - - let rec print fmt = function - | Record (lbs, _) -> - Format.fprintf fmt "{"; - let _ = List.fold_left - (fun first (lb, e) -> - Format.fprintf fmt "%s%a = %a" - (if first then "" else "; ") DE.Term.Const.print lb print e; - false - ) true lbs in - Format.fprintf fmt "}" - | Access(a, e, _) -> - Format.fprintf fmt "%a.%a" print e DE.Term.Const.print a - | Other(t, _) -> X.print fmt t - - end - (*BISECT-IGNORE-END*) - - let print = Debug.print - - let rec raw_compare r1 r2 = - match r1, r2 with - | Other (u1, ty1), Other (u2, ty2) -> - let c = Ty.compare ty1 ty2 in - if c <> 0 then c else X.str_cmp u1 u2 - | Other _, _ -> -1 - | _, Other _ -> 1 - | Access (tcst1, u1, ty1), Access (tcst2, u2, ty2) -> - let c = Ty.compare ty1 ty2 in - if c <> 0 then c - else - let c = DE.Term.Const.compare tcst1 tcst2 in - if c <> 0 then c - else raw_compare u1 u2 - | Access _, _ -> -1 - | _, Access _ -> 1 - | Record (lbs1, ty1), Record (lbs2, ty2) -> - let c = Ty.compare ty1 ty2 in - if c <> 0 then c else raw_compare_list lbs1 lbs2 - - and raw_compare_list l1 l2 = - match l1, l2 with - | [], [] -> 0 - | [], _ -> 1 - | _, [] -> -1 - | (_, x1)::l1, (_, x2)::l2 -> - let c = raw_compare x1 x2 in - if c<>0 then c else raw_compare_list l1 l2 - - let rec normalize v = - match v with - | Record (lbs, ty) -> - begin - let lbs_n = List.map (fun (lb, x) -> lb, normalize x) lbs in - match lbs_n with - | (lb1, Access(lb2, x, _)) :: l when DE.Term.Const.equal lb1 lb2 -> - if List.for_all - (function - | (lb1, Access(lb2, y, _)) -> - DE.Term.Const.equal lb1 lb2 && raw_compare x y = 0 - | _ -> false) l - then x - else Record (lbs_n, ty) - | _ -> Record (lbs_n, ty) - end - | Access (a, x, ty) -> - begin - match normalize x with - | Record (lbs, _) -> My_list.assoc DE.Term.Const.equal a lbs - | x_n -> Access (a, x_n, ty) - end - | Other _ -> v - - let embed r = - match X.extract r with - | Some p -> p - | None -> Other(r, X.type_info r) - - let compare_mine t u = raw_compare (normalize t) (normalize u) - - let compare x y = compare_mine (embed x) (embed y) - - let rec equal r1 r2 = - match r1, r2 with - | Other (u1, ty1), Other (u2, ty2) -> - Ty.equal ty1 ty2 && X.equal u1 u2 - - | Access (s1, u1, ty1), Access (s2, u2, ty2) -> - DE.Term.Const.equal s1 s2 && Ty.equal ty1 ty2 && equal u1 u2 - - | Record (lbs1, ty1), Record (lbs2, ty2) -> - Ty.equal ty1 ty2 && equal_list lbs1 lbs2 - - | Other _, _ | _, Other _ | Access _, _ | _, Access _ -> false - - and equal_list l1 l2 = - try List.for_all2 (fun (_,r1) (_,r2) -> equal r1 r2) l1 l2 - with Invalid_argument _ -> false - - let is_mine t = - match normalize t with - | Other(r, _) -> r - | x -> X.embed x - - let type_info = function - | Record (_, ty) | Access (_, _, ty) | Other (_, ty) -> ty - - let make t = - let rec make_rec t ctx = - let { E.f; xs; ty; _ } = E.term_view t in - match f, ty with - | Symbols.Op (Symbols.Record), Ty.Trecord { Ty.lbs; _ } -> - assert (List.length xs = List.length lbs); - let l, ctx = - List.fold_right2 - (fun x (lb, _) (l, ctx) -> - let r, ctx = make_rec x ctx in - let tyr = type_info r in - let dlb = E.mk_term (Symbols.Op (Symbols.Access lb)) [t] tyr in - let c = E.mk_eq ~iff:false dlb x in - (lb, r)::l, c::ctx - ) - xs lbs ([], ctx) - in - Record (l, ty), ctx - | Symbols.Op (Symbols.Access a), _ -> - begin - match xs with - | [x] -> - let r, ctx = make_rec x ctx in - Access (a, r, ty), ctx - | _ -> assert false - end - - | _, _ -> - let r, ctx' = X.make t in - Other (r, ty), ctx'@ctx - in - let r, ctx = make_rec t [] in - let is_m = is_mine r in - is_m, ctx - - let color _ = assert false - - let embed r = - match X.extract r with - | Some p -> p - | None -> Other(r, X.type_info r) - - let xs_of_list = List.fold_left (fun s x -> XS.add x s) XS.empty - - let leaves t = - let rec leaves t = - match normalize t with - | Record (lbs, _) -> - List.fold_left (fun s (_, x) -> XS.union (leaves x) s) XS.empty lbs - | Access (_, x, _) -> leaves x - | Other (x, _) -> xs_of_list (X.leaves x) - in - XS.elements (leaves t) - - let is_constant = - let rec is_constant t = - match normalize t with - | Record (lbs, _) -> - List.for_all (fun (_, x) -> is_constant x) lbs - | Access (_, x, _) -> is_constant x - | Other (x, _) -> X.is_constant x - in is_constant - - let rec hash = function - | Record (lbs, ty) -> - List.fold_left - (fun h (lb, x) -> 17 * hash x + 13 * DE.Term.Const.hash lb + h) - (Ty.hash ty) lbs - | Access (a, x, ty) -> - 19 * hash x + 17 * DE.Term.Const.hash a + Ty.hash ty - | Other (x, ty) -> - Ty.hash ty + 23 * X.hash x - - let rec subst_rec p v r = - match r with - | Other (t, _) -> - embed (if X.equal p t then v else X.subst p v t) - | Access (a, t, ty) -> - Access (a, subst_rec p v t, ty) - | Record (lbs, ty) -> - let lbs = List.map (fun (lb, t) -> lb, subst_rec p v t) lbs in - Record (lbs, ty) - - let subst p v r = is_mine (subst_rec p v r) - - let is_mine_symb sy = - match sy with - | Symbols.Op (Symbols.Record | Symbols.Access _) -> true - | _ -> false - - let abstract_access field e ty acc = - let xe = is_mine e in - let abs_right_xe, acc = - try My_list.assoc X.equal xe acc, acc - with Not_found -> - let left_abs_xe2, acc = X.abstract_selectors xe acc in - match X.type_info left_abs_xe2 with - | (Ty.Trecord { Ty.lbs; _ }) as tyr -> - let flds = - List.map - (fun (lb,ty) -> lb, embed (X.term_embed (E.fresh_name ty))) lbs - in - let record = is_mine (Record (flds, tyr)) in - record, (left_abs_xe2, record) :: acc - | ty -> - Fmt.failwith - "Not a record type: `%a" Ty.print_full ty - in - let abs_access = normalize (Access (field, embed abs_right_xe, ty)) in - is_mine abs_access, acc - - let abstract_selectors v acc = - match v with - (* Handled by combine. Should not happen! *) - | Other _ -> assert false - - (* This is not a selector *) - | Record (fields,ty) -> - let flds, acc = - List.fold_left - (fun (flds,acc) (lbl,e) -> - let e, acc = X.abstract_selectors (is_mine e) acc in - (lbl, embed e)::flds, acc - )([], acc) fields - [@ocaml.ppwarning "TODO: should not rebuild if not changed !"] - in - is_mine (Record (List.rev flds, ty)), acc - - (* Selector ! Interesting case !*) - | Access (field, e, ty) -> abstract_access field e ty acc - - - (* Shostak'pair solver adapted to records *) - - (* unused -- - let mk_fresh_record x info = - let ty = type_info x in - let lbs = match ty with Ty.Trecord r -> r.Ty.lbs | _ -> assert false in - let lbs = - List.map - (fun (lb, ty) -> - match info with - | Some (a, v) when Uid.equal lb a -> lb, v - | _ -> let n = embed (X.term_embed (E.fresh_name ty)) in lb, n) - lbs - in - Record (lbs, ty), lbs - *) - - (* unused -- - let rec occurs x = function - | Record (lbs, _) -> - List.exists (fun (_, v) -> occurs x v) lbs - | Access (_, v, _) -> occurs x v - | Other _ as v -> compare_mine x v = 0 (* XXX *) - *) - - (* unused -- - let rec subst_access x s e = - match e with - | Record (lbs, ty) -> - Record (List.map (fun (n,e') -> n, subst_access x s e') lbs, ty) - | Access (lb, e', _) when compare_mine x e' = 0 -> - My_list.assoc Uid.equal lb s - | Access (lb', e', ty) -> Access (lb', subst_access x s e', ty) - | Other _ -> e - *) - - let fully_interpreted = is_mine_symb - - let rec term_extract r = - match X.extract r with - | Some v -> begin match v with - | Record (lbs, ty) -> - begin - try - let lbs = - List.map - (fun (_, r) -> - match term_extract (is_mine r) with - | None, _ -> raise Not_found - | Some t, _ -> t) - lbs - in - Some (E.mk_term (Symbols.Op Symbols.Record) lbs ty), false - with Not_found -> None, false - end - | Access (a, r, ty) -> - begin - match X.term_extract (is_mine r) with - | None, _ -> None, false - | Some t, _ -> - Some (E.mk_term (Symbols.Op (Symbols.Access a)) [t] ty), false - end - | Other (r, _) -> X.term_extract r - end - | None -> X.term_extract r - - - let orient_solved p v pb = - if List.exists (X.equal p) (X.leaves v) then raise Util.Unsolvable; - Sig.{ pb with sbt = (p,v) :: pb.sbt } - - let solve r1 r2 (pb : _ Sig.solve_pb) = - match embed r1, embed r2 with - | Record (l1, _), Record (l2, _) -> - let eqs = - List.fold_left2 - (fun eqs (a, b) (x, y) -> - assert (DE.Term.Const.compare a x = 0); - (is_mine y, is_mine b) :: eqs - ) pb.eqs l1 l2 - in - {pb with eqs=eqs} - - | Other _, Other _ -> - if X.str_cmp r1 r2 > 0 then { pb with sbt = (r1,r2)::pb.sbt } - else { pb with sbt = (r2,r1)::pb.sbt } - - | Other _, Record _ -> orient_solved r1 r2 pb - | Record _, Other _ -> orient_solved r2 r1 pb - | Access _ , _ -> assert false - | _ , Access _ -> assert false - - let assign_value t _ eq = - match embed t with - | Access _ -> None - - | Record (_, ty) -> - if List.exists (fun (t,_) -> Expr.is_model_term t) eq - then None - else Some (Expr.fresh_name ty, false) - - | Other (_,ty) -> - match ty with - | Ty.Trecord { Ty.lbs; _ } -> - let rev_lbs = List.rev_map (fun (_, ty) -> Expr.fresh_name ty) lbs in - let s = E.mk_term (Symbols.Op Symbols.Record) (List.rev rev_lbs) ty in - Some (s, false) (* false <-> not a case-split *) - | _ -> assert false - - let to_model_term = - let rec to_model_term r = - match r with - | Record (fields, ty) -> - (* We can ignore the names of fields as they are inlined in the - type [ty] of the record. *) - let l = - My_list.try_map (fun (_name, rf) -> to_model_term rf) fields - in - Option.bind l @@ fun l -> - Some (E.mk_term Sy.(Op Record) l ty) - - | Other (a, _) -> - X.to_model_term a - | Access _ -> None - in fun r -> to_model_term (embed r) -end diff --git a/src/lib/reasoners/records.mli b/src/lib/reasoners/records.mli deleted file mode 100644 index 4283685e5..000000000 --- a/src/lib/reasoners/records.mli +++ /dev/null @@ -1,37 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -type 'a abstract - -module type ALIEN = sig - include Sig.X - val embed : r abstract -> r - val extract : r -> (r abstract) option -end - -module Shostak - (X : ALIEN) : Sig.SHOSTAK with type r = X.r and type t = X.r abstract diff --git a/src/lib/reasoners/records_rel.ml b/src/lib/reasoners/records_rel.ml deleted file mode 100644 index 84f2a54ea..000000000 --- a/src/lib/reasoners/records_rel.ml +++ /dev/null @@ -1,49 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -type t = unit - -let src = Logs.Src.create ~doc:"Records" __MODULE__ -module Log = (val Logs.src_log src : Logs.LOG) - -let timer = Timers.M_Records - -let empty uf = (), Uf.domains uf -let assume _ uf _ = - (), Uf.domains uf, { Sig_rel.assume = []; remove = [] } -let query _ _ _ = None -let case_split _env _uf ~for_model:_ = [] -let optimizing_objective _env _uf _o = None -let add env uf _ _ = env, Uf.domains uf, [] -let new_terms _ = Expr.Set.empty -let instantiate ~do_syntactic_matching:_ _ env _ _ = env, [] - -let assume_th_elt t th_elt _ = - match th_elt.Expr.extends with - | Util.Records -> - failwith "This Theory does not support theories extension" - | _ -> t diff --git a/src/lib/reasoners/records_rel.mli b/src/lib/reasoners/records_rel.mli deleted file mode 100644 index cac59a5a1..000000000 --- a/src/lib/reasoners/records_rel.mli +++ /dev/null @@ -1,29 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -include Sig_rel.RELATION -val src : Logs.src diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml index e5bc26035..e6e6efdf6 100644 --- a/src/lib/structures/errors.ml +++ b/src/lib/structures/errors.ml @@ -51,12 +51,9 @@ type typing_error = | ShouldHaveTypeBitv of Ty.t | ArrayIndexShouldHaveTypeInt | ShouldHaveTypeArray - | ShouldHaveTypeRecord of Ty.t - | ShouldBeARecord | ShouldHaveLabel of string * string | NoLabelInType of Hstring.t * Ty.t | ShouldHaveTypeProp - | NoRecordType of Hstring.t | DuplicateLabel of Hstring.t | DuplicatePattern of string | WrongLabel of Hstring.t * Ty.t @@ -175,19 +172,12 @@ let report_typing_error fmt = function Ty.print t | ShouldHaveTypeArray -> fprintf fmt "this expression should have type farray" - | ShouldHaveTypeRecord t -> - fprintf fmt "this expression has type %a but it should have a record type" - Ty.print t - | ShouldBeARecord -> - fprintf fmt "this expression should have a record type" | ShouldHaveLabel (s, a) -> fprintf fmt "this expression has type %s which has no label %s" s a | NoLabelInType (lb, ty) -> fprintf fmt "no label %s in type %a" (Hstring.view lb) Ty.print ty | ShouldHaveTypeProp -> fprintf fmt "this expression should have type prop" - | NoRecordType s -> - fprintf fmt "no record type has label %s" (Hstring.view s) | DuplicateLabel s -> fprintf fmt "label %s is defined several times" (Hstring.view s) | DuplicatePattern s -> diff --git a/src/lib/structures/errors.mli b/src/lib/structures/errors.mli index 7f1794c17..c3d7245df 100644 --- a/src/lib/structures/errors.mli +++ b/src/lib/structures/errors.mli @@ -57,12 +57,9 @@ type typing_error = | ShouldHaveTypeBitv of Ty.t | ArrayIndexShouldHaveTypeInt | ShouldHaveTypeArray - | ShouldHaveTypeRecord of Ty.t - | ShouldBeARecord | ShouldHaveLabel of string * string | NoLabelInType of Hstring.t * Ty.t | ShouldHaveTypeProp - | NoRecordType of Hstring.t | DuplicateLabel of Hstring.t | DuplicatePattern of string | WrongLabel of Hstring.t * Ty.t diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index a541471ff..bfcf2d302 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -437,7 +437,6 @@ val is_pure : t -> bool val is_model_term : t -> bool (** [is_model_term e] checks if the expression [e] is a model terms. A model term can be: - - A record definition involving only model terms. - A constructor application involving only model terms, - A literal of a basic type (integer, real, boolean, unit or bitvector), - A name. *) diff --git a/src/lib/structures/profiling.ml b/src/lib/structures/profiling.ml index 308ea1230..1d129aa6d 100644 --- a/src/lib/structures/profiling.ml +++ b/src/lib/structures/profiling.ml @@ -454,18 +454,6 @@ let columns : (string * string * int * bool option * 'a) list = Format.sprintf "%s~%s" (float_resize curr (sz - 5)) (string_resize (percent gtime curr) 4)); - "Sum", "Time spent in Sum module(s)", 16, Some false, - (fun _ gtime sz -> - let curr = Timers.get_sum (get_timers ()) Timers.M_Sum in - Format.sprintf "%s~%s" - (float_resize curr (sz - 5)) (string_resize (percent gtime curr) 4)); - - "Records", "Time spent in Records module(s)", 16, Some false, - (fun _ gtime sz -> - let curr = Timers.get_sum (get_timers ()) Timers.M_Records in - Format.sprintf "%s~%s" - (float_resize curr (sz - 5)) (string_resize (percent gtime curr) 4)); - "AC", "Time spent in AC module(s)", 16, Some false, (fun _ gtime sz -> let curr = Timers.get_sum (get_timers ()) Timers.M_AC in @@ -480,10 +468,8 @@ let columns : (string * string * int * bool option * 'a) list = let tcc = Timers.get_sum timers Timers.M_CC in let tarith = Timers.get_sum timers Timers.M_Arith in let tarrays = Timers.get_sum timers Timers.M_Arrays in - let tsum = Timers.get_sum timers Timers.M_Sum in - let trecs = Timers.get_sum timers Timers.M_Records in let tac = Timers.get_sum timers Timers.M_AC in - let total = tsat+.tmatch+.tcc+.tarith+.tarrays+.tsum+.trecs+.tac in + let total = tsat+.tmatch+.tcc+.tarith+.tarrays+.tac in float_resize total sz); ] diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 5d96d06a0..ded95d77b 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -451,14 +451,6 @@ let t_adt ?(body=None) s ty_vars = begin match body with | None -> () | Some [] -> assert false - | Some ([_] as cases) -> - if Options.get_debug_adt () then - Printer.print_dbg ~module_name:"Ty" - "should be registered as a record"; - let cases = - List.map (fun (constr, destrs) -> {constr; destrs}) cases - in - Decls.add s ty_vars cases | Some cases -> let cases = List.map (fun (constr, destrs) -> {constr; destrs}) cases diff --git a/src/lib/util/timers.ml b/src/lib/util/timers.ml index c6ca31a9d..732459612 100644 --- a/src/lib/util/timers.ml +++ b/src/lib/util/timers.ml @@ -39,8 +39,6 @@ type ty_module = | M_UF | M_Arith | M_Arrays - | M_Sum - | M_Records | M_Adt | M_Bitv | M_AC @@ -61,8 +59,6 @@ let all_modules = M_UF; M_Arith; M_Arrays; - M_Sum; - M_Records; M_Adt; M_Bitv; M_AC; @@ -136,8 +132,6 @@ let string_of_ty_module k = match k with | M_UF -> "UF" | M_Arith -> "Arith" | M_Arrays -> "Arrays" - | M_Sum -> "Sum" - | M_Records -> "Records" | M_Adt -> "Adt" | M_Bitv -> "Bitv" | M_AC -> "AC" diff --git a/src/lib/util/timers.mli b/src/lib/util/timers.mli index d7143847f..a1ca9ed67 100644 --- a/src/lib/util/timers.mli +++ b/src/lib/util/timers.mli @@ -35,8 +35,6 @@ type ty_module = | M_UF | M_Arith | M_Arrays - | M_Sum - | M_Records | M_Adt | M_Bitv | M_AC diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index 876eea711..838f12e84 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -77,10 +77,8 @@ let pp_sat_solver ppf = function | CDCL_Tableaux -> Format.fprintf ppf "CDCL-Tableaux" type theories_extensions = - | Sum | Adt | Arrays - | Records | Bitv | LIA | LRA @@ -116,10 +114,8 @@ let equal_mode x y = match x, y with let th_ext_of_string ext = match ext with - | "Sum" -> Some Sum | "Adt" -> Some Adt | "Arrays" -> Some Arrays - | "Records" -> Some Records | "Bitv" -> Some Bitv | "LIA" -> Some LIA | "LRA" -> Some LRA @@ -131,10 +127,8 @@ let th_ext_of_string ext = let string_of_th_ext ext = match ext with - | Sum -> "Sum" | Adt -> "Adt" | Arrays -> "Arrays" - | Records -> "Records" | Bitv -> "Bitv" | LIA -> "LIA" | LRA -> "LRA" diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 2ce5175ed..f003f78ef 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -59,10 +59,8 @@ type sat_solver = val pp_sat_solver : Format.formatter -> sat_solver -> unit type theories_extensions = - | Sum | Adt | Arrays - | Records | Bitv | LIA | LRA