Skip to content

Commit

Permalink
temporary 5
Browse files Browse the repository at this point in the history
  • Loading branch information
@Halbaroth
Halbaroth committed Jan 30, 2025
1 parent 49f24b5 commit 73314bd
Show file tree
Hide file tree
Showing 6 changed files with 108 additions and 107 deletions.
22 changes: 3 additions & 19 deletions src/bin/common/solving_loop.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,20 +32,6 @@ module DO = D_state_option
module Sy = Symbols
module O = Options

let get_basename = function
| DStd.Path.Local { name; }
| Absolute { name; path = []; } -> name
| Absolute { name; path; } ->
Fmt.failwith
"Expected an empty path to the basename: \"%s\" but got: [%a]."
name (fun fmt l ->
match l with
| h :: t ->
Format.fprintf fmt "%s" h;
List.iter (Format.fprintf fmt "; %s") t
| _ -> ()
) path

exception Exit_with_code of int

type solver_ctx = {
Expand Down Expand Up @@ -659,7 +645,7 @@ let process_source ?selector_inst ~print_status src =
*)
let simple_form =
Expr.mk_term
(Sy.name @@ Id.of_term_cst tcst)
(Sy.name @@ Id.of_term_cst ~defined:true tcst)
[]
(Translate.dty_to_ty term.DStd.Expr.term_ty)
in
Expand Down Expand Up @@ -864,10 +850,8 @@ let process_source ?selector_inst ~print_status src =
(fun st def ->
match def with
| `Term_def (_, tcst, _, _, _) ->
let name = get_basename tcst.DStd.Expr.path in
let set =
State.get term_defs st
in
let name = Util.get_basename tcst.DStd.Expr.path in
let set = State.get term_defs st in
let set = Util.MS.add name tcst set in
State.set term_defs set st
| _ -> st
Expand Down
33 changes: 8 additions & 25 deletions src/lib/frontend/translate.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,23 +45,6 @@ module HT =
let hash (Id i)= DE.Id.hash i
end)

(** Helper function: returns the basename of a dolmen path, since in AE
the problems are contained in one-file (for now at least), the path is
irrelevant and only the basename matters *)
let get_basename = function
| DStd.Path.Local { name; }
| Absolute { name; path = []; } -> name
| Absolute { name; path; } ->
Fmt.failwith
"Expected an empty path to the basename: \"%s\" but got: [%a]."
name (fun fmt l ->
match l with
| h :: t ->
Format.fprintf fmt "%s" h;
List.iter (Format.fprintf fmt "; %s") t
| _ -> ()
) path

module Cache = struct

let ae_sy_ht: Sy.t HT.t = HT.create 100
Expand Down Expand Up @@ -124,7 +107,7 @@ module Cache = struct
let store_sy_vl_names (tvl: DE.term_var list) =
List.iter (
fun ({ DE.path; _ } as tv) ->
let name = get_basename path in
let name = Util.get_basename path in
(* TODO : Check this line! *)
store_sy tv (Sy.name @@ Id.of_string ~ns:Internal name)
) tvl
Expand Down Expand Up @@ -177,7 +160,7 @@ let builtin_term t = Dl.Typer.T.builtin_term t
let builtin_ty t = Dl.Typer.T.builtin_ty t

let ty (ty_cst : DE.ty_cst) ty =
let name = get_basename ty_cst.path in
let name = Util.get_basename ty_cst.path in
DStd.Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@
fun env s ->
builtin_ty @@
Expand All @@ -189,7 +172,7 @@ let fpa_rounding_mode, rounding_modes, add_rounding_modes =
let constrs = Fpa_rounding.d_constrs in
let add_constrs map =
List.fold_left (fun map (c : DE.term_cst) ->
let name = get_basename c.path in
let name = Util.get_basename c.path in
DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term }
(fun env _ ->
builtin_term @@
Expand Down Expand Up @@ -819,7 +802,7 @@ end = struct
| Var ({ builtin = B.Base; path; _ } as t_v) ->
(* Should the type be passed as an argument
instead of re-evaluating it here? *)
let v = Var.of_string (get_basename path) in
let v = Var.of_string (Util.get_basename path) in
let sy = Sy.var v in
Cache.store_sy t_v sy;
(* Adding the matched variable to the store *)
Expand Down Expand Up @@ -1441,7 +1424,7 @@ let rec mk_expr
let lsbis =
List.map (
fun ({ DE.path; _ } as tv, t) ->
let name = get_basename path in
let name = Util.get_basename path in
let v = Var.of_string name in
Cache.store_sy tv (Sy.var v);
v, t
Expand Down Expand Up @@ -1488,7 +1471,7 @@ let rec mk_expr
let ntvl = List.rev_map (
fun (DE.{ path; id_ty; _ } as t_v) ->
dty_to_ty id_ty,
Var.of_string (get_basename path),
Var.of_string (Util.get_basename path),
t_v
) tvl
in
Expand Down Expand Up @@ -1968,15 +1951,15 @@ let make dloc_file acc stmt =
| `Term_def ( _, ({ path; tags; _ } as tcst), tyvars, terml, body) ->
Cache.store_tyvl tyvars;
let st_loc = dl_to_ael dloc_file loc in
let name_base = get_basename path in
let name_base = Util.get_basename path in

let binders, defn =
let rty = dty_to_ty body.term_ty in
let binders, rev_args =
List.fold_left (
fun (binders, acc) (DE.{ path; id_ty; _ } as tv) ->
let ty = dty_to_ty id_ty in
let v = Var.of_string (get_basename path) in
let v = Var.of_string (Util.get_basename path) in
let sy = Sy.var v in
Cache.store_sy tv sy;
let e = E.mk_term sy [] ty in
Expand Down
45 changes: 21 additions & 24 deletions src/lib/structures/id.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,26 +18,6 @@

type name_space = Internal | Fresh | Fresh_ac | Skolem | Abstract

let compare_name_space ns1 ns2 =
match ns1, ns2 with
| Internal, Internal -> 0
| Internal, _ -> -1
| _, Internal -> 1

| Fresh, Fresh -> 0
| Fresh, _ -> -1
| _, Fresh -> 1

| Fresh_ac, Fresh_ac -> 0
| Fresh_ac, _ -> -1
| _, Fresh_ac -> 1

| Skolem, Skolem -> 0
| Skolem, _ -> -1
| _, Skolem -> 1

| Abstract, Abstract -> 0

module Make () = struct
let fresh, reset_fresh_cpt =
let cpt = ref 0 in
Expand Down Expand Up @@ -73,9 +53,26 @@ let mangle ns s =
| Skolem -> ".?__" ^ s
| Abstract -> "@a" ^ s

let of_term_cst ?(defined = false) tcst = User { tcst; defined }
let of_term_cst ?(defined = false) tcst =
(* If the name we got from the user starts with either "."
or "@" (which are prefixes reserved for solver use in the SMT-LIB
standard), the name will be printed with an extra ".". So if the user
writes ".x" or "@x", it will be printed as "..x" and ".@x" instead.
Normally, this should not occur, but we do this to ensure no confusion
even if invalid names ever sneak through. *)
assert (
let s = Util.show_term_cst tcst in
not (Compat.String.starts_with ~prefix:"." s) &&
not (Compat.String.starts_with ~prefix:"@" s));
User { tcst; defined }

let of_string ~ns s =
let () =
match ns with
| Fresh | Fresh_ac | Abstract -> invalid_arg "of_string"
| _ -> ()
in
let hs = Hstring.make (mangle ns s) in
Other { hs; ns }

Expand All @@ -100,7 +97,7 @@ let compare i1 i2 =

| Other { hs = hs1; _ }, Other { hs = hs2; _ } ->
(* NB: Internal identifiers are pre-mangled, which means that we do not
need to take the namespace into consideration when comparing. *)
need to take the name space into consideration when comparing. *)
Hstring.compare hs1 hs2

let equal i1 i2 =
Expand All @@ -109,7 +106,7 @@ let equal i1 i2 =
Bool.equal d1 d2 && Dolmen.Std.Expr.Term.Const.equal t1 t2
| Other { hs = hs1; _ }, Other { hs = hs2; _ } ->
(* NB: Internal identifiers are pre-mangled, which means that we do not
need to take the namespace into consideration when comparing. *)
need to take the name space into consideration when comparing. *)
Hstring.equal hs1 hs2
| _ -> false

Expand All @@ -119,7 +116,7 @@ let hash i =
Dolmen.Std.Expr.Term.Const.hash tcst
| Other { hs; _ } ->
(* NB: Internal identifiers are pre-mangled, which means that we do not
need to take the namespace into consideration when hashing. *)
need to take the name space into consideration when hashing. *)
Hstring.hash hs

let pp ppf i =
Expand Down
85 changes: 48 additions & 37 deletions src/lib/structures/id.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,32 +16,33 @@
(* *)
(**************************************************************************)

(** The [name_space] type discriminates the different types of names. The same
string in different name spaces is considered as different names.
(** The [name_space] type discriminates the different types of internal
identifiers. The same string in different name spaces is considered as
different identifiers.
Note that the names stored in the [Name] constructor below are mangled
during creation of the symbol: a special prefix is added depending on the
Note that the identifier stored in the [Other] constructor below are mangled
during its creation: a special prefix is added depending on the
name space. *)
type name_space =
| Internal
(** This symbol is an internal implementation detail of the solver, such as
a proxy formula or the abstracted counterpart of AC symbols.
Internal names are printed with a ".!" prefix. *)
Internal identifiers are printed with a ".!" prefix. *)
| Fresh
(** This symbol is a "fresh" internal name. Fresh internal names play a
similar role as internal names, but they always represent a constant
that was introduced during solving as part of some kind of purification
or abstraction procedure.
(** This symbol is a "fresh" internal identifer. Fresh internal identifiers
play a similar role as internal identifiers, but they always represent a
constant that was introduced during solving as part of some kind of
purification or abstraction procedure.
In order to correctly implement AC(X) in the presence of distributive
symbols, symbols generated for AC(X) abstraction use a special
namespace, [Fresh_ac] below.
To ensure uniqueness, fresh names must always be generated using
To ensure uniqueness, fresh identifiers must always be generated using
[Id.Namespace.Internal.fresh ()].
In particular, fresh names are only used to denote constants, not
In particular, fresh identifiers are only used to denote constants, not
arbitrary functions. *)
| Fresh_ac
(** This symbol has been introduced as part of the AC(X) abstraction process.
Expand All @@ -54,62 +55,72 @@ type name_space =
whether a fresh symbol comes from the AC(X) abstraction procedure in order
to prevent loops.
To ensure uniqueness, AC abstraction names must always be generated using
[fresh ~ns:Fresh_ac ()]. *)
To ensure uniqueness, AC abstraction identifiers must always be generated
using [fresh ~ns:Fresh_ac ()]. *)
| Skolem
(** This symbol has been introduced as part of skolemization, and represents
the (dependent) variable of an existential quantifier. Skolem names can
have arbitrary arity to depend on previous skolem names in binding order
(so if you have `(exists (x y) e)` then there will be a skolem variable
`sko_x` and a skolem function `(sko_y sko_x)`). *)
the (dependent) variable of an existential quantifier. Skolem identifiers
can have arbitrary arity to depend on previous skolem names in binding
order (so if you have `(exists (x y) e)` then there will be a skolem
variable `sko_x` and a skolem function `(sko_y sko_x)`). *)
| Abstract
(** This symbol has been introduced as part of model generation, and
represents an abstract value.
To ensure uniqueness, abstract names must always be generated using
To ensure uniqueness, abstract identifiers must always be generated using
[fresh ~ns:Abstract ()]. *)

type t = private
| User of { tcst : Dolmen.Std.Expr.term_cst; defined : bool }
(** This identifier was defined by the user, and appears as is somewhere in a
source file.
(** This identifier was declared or defined by the user, and appears as is
somewhere in a source file. *)

As an exception, if the name we got from the user starts with either "."
or "@" (which are prefixes reserved for solver use in the SMT-LIB
standard), the name will be printed with an extra ".". So if the user
writes ".x" or "@x", it will be printed as "..x" and ".@x" instead.
Normally, this shouldn't occur, but we do this to ensure no confusion
even if invalid names ever sneak through. *)
| Other of { hs : Hstring.t; ns : name_space }

type typed = Dolmen.Std.Expr.term_cst * Ty.t list * Ty.t
val compare_typed : typed -> typed -> int

val of_term_cst : ?defined:bool -> Dolmen.Std.Expr.term_cst -> t
(** [of_term_cst ?defined t] creates an identifier from a constant term.
The argument [defined] is used to determine if the identifier is
declared or defined by user. *)

val of_string : ns:name_space -> string -> t
(* [of_string ~ns s] creates an identifier in the name space [ns] from the
string [s].
(** [of_string ~ns s] creates an identifier in the name space [ns] from the
string [s].
Note that identifiers are pre-mangled: the [hs] field of the resulting
identifier may not be exactly the string that was passed to this function
(however, calling [of_string] with the same string but two different name
spaces is guaranteed to return two identifiers with distinct [hs] fields).
Note that identifiers are pre-mangled: the [hs] field of the resulting
identifier may not be exactly the string that was passed to this function
(however, calling [of_string] with the same string but two different name
spaces is guaranteed to return two identifiers with distinct [hs] fields). *)
@raise Invalid_argument if the name space is [Fresh], [Fresh_ac] or
[Abstract]. *)

val fresh : ns:name_space -> unit -> t
(* [fresh ?base ~ns ()] creates a fresh identifier in the name space [ns]
from the base string [base]. The empty string is the default for [base]. *)
(** [fresh ?base ~ns ()] creates a fresh identifier in the name space [ns]
from the base string [base]. The empty string is the default for [base].
The identifier is pre-mangled as in [of_string]. *)

val compare : t -> t -> int

val equal : t -> t -> bool

val hash : t -> int
(** [hash i] computes a hash for the identifier [i]. On the user identifier,
this hash is perfect. *)

val pp : t Fmt.t
(** [pp ppf i] prints the identifier [i] on the formatter [ppf], quoting the
string, if it needs. *)

val show : t -> string
(** Same as [pp] but outputs the result as a string. *)

val is_suspicious : t -> bool

val reinit : unit -> unit
(** Resets the [fresh_internal_name], [fresh_skolem] and [fresh_abstract]
counters. *)
(** Resets the internal counters of the [fresh] function. *)

module Map : Map.S with type key = t
25 changes: 23 additions & 2 deletions src/lib/util/util.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -203,7 +203,28 @@ let rec print_list_pp ~sep ~pp fmt = function
let internal_error msg =
Format.kasprintf (fun s -> raise (Internal_error s)) msg

module DStd = Dolmen.Std

let pp_term_cst ppf t =
let show = Fmt.to_to_string Dolmen.Std.Expr.Term.Const.print in
let show = Fmt.to_to_string DStd.Expr.Term.Const.print in
Dolmen.Smtlib2.Script.Poly.Print.id ppf
@@ Dolmen.Std.Name.simple (show t)
@@ DStd.Name.simple (show t)

let show_term_cst = Fmt.to_to_string pp_term_cst

(** Helper function: returns the basename of a dolmen path, since in AE
the problems are contained in one-file (for now at least), the path is
irrelevant and only the basename matters *)
let get_basename = function
| DStd.Path.Local { name; }
| Absolute { name; path = []; } -> name
| Absolute { name; path; } ->
Fmt.failwith
"Expected an empty path to the basename: \"%s\" but got: [%a]."
name (fun fmt l ->
match l with
| h :: t ->
Format.fprintf fmt "%s" h;
List.iter (Format.fprintf fmt "; %s") t
| _ -> ()
) path
Loading

0 comments on commit 73314bd

Please sign in to comment.