Uniformization of internal identifiers generation #905

Stevendeo · 2023-10-18T12:38:32Z

This PR centralizes how internal identifiers are created. This work is a first step before a simpler task, which is to replace the '!' by '.' in name identifiers.

Halbaroth · 2023-10-18T14:54:39Z

src/lib/frontend/typechecker.ml

@@ -2152,7 +2152,7 @@ let axioms_of_rules loc name lf acc env =
  let acc =
    List.fold_left
      (fun acc f ->
-         let name = (Hstring.fresh_string ()) ^ "_" ^ name in
+         let name = (Symbols.InternalNameId.fresh ()) ^ "_" ^ name in


I suggest to use InternalId instead of InternalNameId.

Halbaroth · 2023-10-18T15:00:41Z

src/lib/structures/symbols.mli

+  val fresh : ?base:string -> unit -> string
+  val reset_fresh_cpt : unit -> unit
+  val is_id : string -> bool
+  val make_as_fresh : string -> string


Is it necessary to expose the function make_as_fresh?

Unfortunately, yes... https://github.com/OCamlPro/alt-ergo/pull/905/files#diff-89722ab84fe15db7d6cd1e3a8533c9d5e0660599698ae64313faae9cf6f23730L1720

You only need make_as_fresh_skolem here ;)

Oh okay I get your point; if I remove the make_as_fresh, I can also remove the reset_fresh_counter and hide the whole module.

We may need to keep reset_fresh_counter for alt-ergo-fuzz, @hra687261 can you confirm?

We may need to keep reset_fresh_counter for alt-ergo-fuzz, @hra687261 can you confirm?

I meant hide the module by wrapping the reset_fresh_cpt in a specific function (which is what I did in the last version of the PR)

hra687261

LGTM modulo a couple of minor details
If my memory serves me right, these fresh names are used for comparisons in some cases, out of prudence, we should probably run some benchmarks, before merging.

hra687261 · 2023-10-18T15:00:43Z

src/lib/structures/symbols.ml

+      else
+        Char.equal (String.unsafe_get s i) (String.unsafe_get S.prefix i)
+        && aux (i + 1)
+    in len_s >= len_pre && aux 0


Suggested change

in len_s >= len_pre && aux 0

in len_s > len_pre && aux 0

Assuming that names as empty strings don't occur

|| is a valid SMTLib2 identifier corresponding to the empty string.

Oh gosh... the SMT-LIB accepts too much things as identifiers...

I think this is a reimplementation of Compat.String.starts_with ~prefix:S.prefix?

I think this is a reimplementation of Compat.String.starts_with ~prefix:S.prefix?

Oh yes indeed

hra687261 · 2023-10-18T15:04:38Z

src/lib/structures/symbols.mli

+val fresh_name : unit -> t
+val is_internal_name : t -> bool
+
+val fresh_skolem : ?is_var:bool -> string -> t
+val make_as_fresh_skolem : string -> t
+val is_skolem : t -> bool


Suggestion, just for consistency:
fresh_name -> fresh_interna_name
is_internal_name -> is_fresh_internal_name
is_skolem -> is_fresh_skolem

bclement-ocp

Agree with @hra687261 — this needs to be tested at least on ae-format and benchtop-tests. Marking as "change requested" so that we don't merge by mistake yet.

(Note that preserving the exact names of the symbols don't matter; if there is no change in the problems solved — but the comments hint that there may be some)

bclement-ocp · 2023-10-18T16:57:55Z

src/lib/structures/symbols.mli

+  val fresh : ?base:string -> unit -> string
+  val reset_fresh_cpt : unit -> unit
+  val is_id : string -> bool
+  val make_as_fresh : string -> string


We may need to keep reset_fresh_counter for alt-ergo-fuzz, @hra687261 can you confirm?

bclement-ocp · 2023-10-18T16:59:09Z

src/lib/structures/symbols.ml

+      else
+        Char.equal (String.unsafe_get s i) (String.unsafe_get S.prefix i)
+        && aux (i + 1)
+    in len_s >= len_pre && aux 0


I think this is a reimplementation of Compat.String.starts_with ~prefix:S.prefix?

bclement-ocp · 2023-10-18T17:02:41Z

src/lib/structures/expr.ml

@@ -1230,7 +1226,7 @@ let is_skolem_cst v =

 let get_skolem =
  let hsko = Hsko.create 17 in
-  let gen_sko ty = mk_term (Sy.fresh "@sko") [] ty in
+  let gen_sko ty = mk_term (Sy.fresh_skolem "@sko") [] ty in


I think that Sy.fresh used to add an extra __ prefix (with the comment "(* garder le suffixe "__" car cela influence l'ordre *)") but it looks like Sy.fresh_skolem doesn't, so unless I missed something we used to get !?__@sko and we now get !?@sko here.

As it is outdated I can't reply to the right comment, but reset_id_builders will do instead of reset_fresh_counter, thanks for noticing that @bclement-ocp !

I think that Sy.fresh used to add an extra __ prefix (with the comment "(* garder le suffixe "__" car cela influence l'ordre *)") but it looks like Sy.fresh_skolem doesn't, so unless I missed something we used to get !?__@sko and we now get !?@sko here.

That makes me think this whole check system is unsound, because an identifier can start with .? if is has been defined quoted.

This is why we want to replace ! with .! Identifiers starting with . or @ are reserved for solver usage and cannot be used in scripts, dolmen ensures this (or will in the next release, see Gbury/dolmen#185 ).

Ah, sorry, I misread your remark — indeed, according to the SMT-LIB it can, but I think after Gbury/dolmen#185 identifiers starting with .? are rejected even in quoted form (which is incorrect from a strict reading of the standard).

Ah, sorry, I misread your remark — indeed, according to the SMT-LIB it can, but I think after Gbury/dolmen#185 identifiers starting with .? are rejected even in quoted form (which is incorrect from a strict reading of the standard).

You did not, I miswrote it and edited, you might have seen the old version :)

bclement-ocp

I believe these changes are correct and should not change the identifiers we generate, so there should be zero performance impact here, but please run benchmarks on ae-format and benchtop-tests to confirm.

bclement-ocp · 2023-10-19T14:23:50Z

I am not sure why you re-requested a review from me — I think we are good and just waiting on benchmark results, or is there a specific part you want me to look at?

Stevendeo · 2023-10-23T09:39:24Z

I am not sure why you re-requested a review from me — I think we are good and just waiting on benchmark results, or is there a specific part you want me to look at?

Still me discovering github, sorry about that

Stevendeo · 2023-10-24T10:32:48Z

No regressions (and even 1 improvement), we can merge!

Stevendeo · 2023-10-27T09:35:56Z

@bclement-ocp Can we merge now?

bclement-ocp · 2023-10-27T09:49:40Z

I think so — sorry I got confused somehow, thought I had approved already.

CHANGES: ### Command-line interface - Enable FPA theory by default (OCamlPro/alt-ergo#1177) - Remove deprecated output channels (OCamlPro/alt-ergo#782) - Deprecate the --use-underscore since it produces models that are not SMT-LIB compliant (OCamlPro/alt-ergo#805) - Add --dump-models-on to dump models on a specific output channel (OCamlPro/alt-ergo#838) - Use consistent return codes (OCamlPro/alt-ergo#842) - Add --continue-on-error flag to set the SMT-LIB error behavior (OCamlPro/alt-ergo#853) - Make dolmen the default value for the --frontend option (OCamlPro/alt-ergo#857) - Restore functionality to broken `--profiling` option (OCamlPro/alt-ergo#947) - Add bare-bones support for interactive input in SMT-LIB format (OCamlPro/alt-ergo#949) - Less confusing behavior on timeout (OCamlPro/alt-ergo#982, OCamlPro/alt-ergo#984) - Add `--strict` option for SMT-LIB compliant mode (OCamlPro/alt-ergo#916, OCamlPro/alt-ergo#1133) - Deprecate `sum`, `typing` and `warnings` debug flags (OCamlPro/alt-ergo#1204) ### SMT-LIB support - Add support for the many new SMT-LIB commands (OCamlPro/alt-ergo#837, OCamlPro/alt-ergo#848, OCamlPro/alt-ergo#852, OCamlPro/alt-ergo#863, OCamlPro/alt-ergo#911, OCamlPro/alt-ergo#942, OCamlPro/alt-ergo#945, OCamlPro/alt-ergo#961, OCamlPro/alt-ergo#975, OCamlPro/alt-ergo#1069) - Expose the FPA rounding builtin in the SMT-LIB format (OCamlPro/alt-ergo#876, OCamlPro/alt-ergo#1135) - Allow changing the SAT solver using (set-option) (OCamlPro/alt-ergo#880) - Add support for the `:named` attribute (OCamlPro/alt-ergo#957) - Add support for quoted identifiers (OCamlPro/alt-ergo#909, OCamlPro/alt-ergo#972) - Add support for naming lemmas in SMT-LIB syntax (OCamlPro/alt-ergo#1141, OCamlPro/alt-ergo#1143) ### Model generation - Use post-solve SAT environment in model generation, fixing issues where incorrect models were generated (OCamlPro/alt-ergo#789) - Restore support for records in models (OCamlPro/alt-ergo#793) - Use abstract values instead of dummy values in models where the actual value does not matter (OCamlPro/alt-ergo#804, OCamlPro/alt-ergo#835) - Use fresh names for all abstract values to prevent accidental captures (OCamlPro/alt-ergo#811) - Add support for model generation with the default CDCL solver (OCamlPro/alt-ergo#829) - Support model generation for the BV theory (OCamlPro/alt-ergo#841, OCamlPro/alt-ergo#968) - Add support for optimization (MaxSMT / OptiSMT) with lexicographic Int and Real objectives (OCamlPro/alt-ergo#861, OCamlPro/alt-ergo#921) - Add a SMT-LIB printer for expressions (OCamlPro/alt-ergo#952, OCamlPro/alt-ergo#981, OCamlPro/alt-ergo#1082, OCamlPro/alt-ergo#931, OCamlPro/alt-ergo#932) - Ensure models have a value for all constants in the problem (OCamlPro/alt-ergo#1019) - Fix a rare soundness issue with integer constraints when model generation is enabled (OCamlPro/alt-ergo#1025) - Support model generation for the ADT theory (OCamlPro/alt-ergo#1093, OCamlPro/alt-ergo#1153) ### Theory reasoning - Add word-level propagators for the BV theory (OCamlPro/alt-ergo#944, OCamlPro/alt-ergo#1004, OCamlPro/alt-ergo#1007, OCamlPro/alt-ergo#1010, OCamlPro/alt-ergo#1011, OCamlPro/alt-ergo#1012, OCamlPro/alt-ergo#1040, OCamlPro/alt-ergo#1044, OCamlPro/alt-ergo#1054, OCamlPro/alt-ergo#1055, OCamlPro/alt-ergo#1056, OCamlPro/alt-ergo#1057, OCamlPro/alt-ergo#1065, OCamlPro/alt-ergo#1073, OCamlPro/alt-ergo#1144, OCamlPro/alt-ergo#1152) - Add interval domains and arithmetic propagators for the BV theory (OCamlPro/alt-ergo#1058, OCamlPro/alt-ergo#1083, OCamlPro/alt-ergo#1084, OCamlPro/alt-ergo#1085) - Native support for bv2nat of bit-vector normal forms (OCamlPro/alt-ergo#1154) - Fix incompleteness issues in the BV solver (OCamlPro/alt-ergo#978, OCamlPro/alt-ergo#979) - Abstract more arguments of AC symbols to avoid infinite loops when they contain other AC symbols (OCamlPro/alt-ergo#990) - Do not make irrelevant decisions in CDCL solver, improving performance slightly (OCamlPro/alt-ergo#1041) - Rewrite the ADT theory to use domains and integrate the enum theory into the ADT theory (OCamlPro/alt-ergo#1078, OCamlPro/alt-ergo#1086, OCamlPro/alt-ergo#1087, OCamlPro/alt-ergo#1091, OCamlPro/alt-ergo#1094, OCamlPro/alt-ergo#1138) - Rewrite the Intervals module entirely (OCamlPro/alt-ergo#1108) - Add maximize/minimize terms for matching (OCamlPro/alt-ergo#1166) - Internalize `sign_extend` and `repeat` (OCamlPro/alt-ergo#1192) - Run cross-propagators to completion (OCamlPro/alt-ergo#1221) - Support binary distinct on arbitrary bit-widths (OCamlPro/alt-ergo#1222) - Only perform optimization when building a model (OCamlPro/alt-ergo#1224) - Make sure domains do not overflow the default domain (OCamlPro/alt-ergo#1225) - Do not build unnormalized values in `zero_extend` (OCamlPro/alt-ergo#1226) ### Internal/library changes - Rewrite the Vec module (OCamlPro/alt-ergo#607) - Move printer definitions closer to type definitions (OCamlPro/alt-ergo#808) - Mark proxy names as reserved (OCamlPro/alt-ergo#836) - Use a Zarith-based representation for numbers and bit-vectors (OCamlPro/alt-ergo#850, OCamlPro/alt-ergo#943) - Add native support for (bvnot) in the BV solver (OCamlPro/alt-ergo#856) - Add constant propagators for partially interpreted functions (OCamlPro/alt-ergo#869) - Remove `Util.failwith` in favor of `Fmt.failwith` (OCamlPro/alt-ergo#872) - Add more `Expr` smart constructors (OCamlPro/alt-ergo#877, OCamlPro/alt-ergo#878) - Do not use existential variables for integer division (OCamlPro/alt-ergo#881) - Preserve `Subst` literals to prevent accidental incompleteness (OCamlPro/alt-ergo#886) - Properly start timers (OCamlPro/alt-ergo#924) - Compute a concrete representation of a model instead of performing (OCamlPro/alt-ergo#925) - Allow direct access to the SAT API in the Alt-Ergo library computations during printing (OCamlPro/alt-ergo#927) - Better handling for step limit (OCamlPro/alt-ergo#936) - Add a generic option manager to deal with the dolmen state (OCamlPro/alt-ergo#951) - Expose an imperative SAT API in the Alt-Ergo library (OCamlPro/alt-ergo#962) - Keep track of the SMT-LIB mode (OCamlPro/alt-ergo#971) - Add ability to decide on semantic literals (OCamlPro/alt-ergo#1027, OCamlPro/alt-ergo#1118) - Preserve trigger order when parsing quantifiers with multiple trigger (OCamlPro/alt-ergo#1046). - Store domains inside the union-find module (OCamlPro/alt-ergo#1119) - Remove some polymorphic hashtables (OCamlPro/alt-ergo#1219) ### Build and integration - Drop support for OCaml <4.08.1 (OCamlPro/alt-ergo#803) - Use dune-site for the inequalities plugins. External pluginsm ust now be registered through the dune-site plugin mechanism in the `(alt-ergo plugins)` site to be picked up by Alt-Ergo (OCamlPro/alt-ergo#1049). - Add a release workflow (OCamlPro/alt-ergo#827) - Add a Windows workflow (OCamlPro/alt-ergo#1203) - Mark the dune.inc file as linguist-generated to avoid huge diffs (OCamlPro/alt-ergo#830) - Use GitHub Actions badges in the README (OCamlPro/alt-ergo#882) - Use `dune build @check` to build the project (OCamlPro/alt-ergo#887) - Enable warnings as errors on the CI (OCamlPro/alt-ergo#888) - Uniformization of internal identifiers generation (OCamlPro/alt-ergo#905, OCamlPro/alt-ergo#918) - Use an efficient `String.starts_with` implementation (OCamlPro/alt-ergo#912) - Fix the Makefile (OCamlPro/alt-ergo#914) - Add `Logs` dependency (OCamlPro/alt-ergo#1206) - Use `dynamic_include` to include the generated file `dune.inc` (OCamlPro/alt-ergo#1199) - Support Windows (OCamlPro/alt-ergo#1184,OCamlPro/alt-ergo#1189,OCamlPro/alt-ergo#1195,OCamlPro/alt-ergo#1199,OCamlPro/alt-ergo#1200) - Wrap the library `Alt_ergo_prelude` (OCamlPro/alt-ergo#1223) ### Testing - Use --enable-assertions in tests (OCamlPro/alt-ergo#809) - Add a test for push/pop (OCamlPro/alt-ergo#843) - Use the CDCL solver when testing model generation (OCamlPro/alt-ergo#938) - Do not test .smt2 files with the legacy frontend (OCamlPro/alt-ergo#939) - Restore automatic creation of .expected files (OCamlPro/alt-ergo#941) ### Documentation - Add a new example for model generation (OCamlPro/alt-ergo#826) - Add a Pygments lexer for the Alt-Ergo native language (OCamlPro/alt-ergo#862) - Update the current authors (OCamlPro/alt-ergo#865) - Documentation of the `Enum` theory (OCamlPro/alt-ergo#871) - Document `Th_util.lit_origin` (OCamlPro/alt-ergo#915) - Document the CDCL-Tableaux solver (OCamlPro/alt-ergo#995) - Document Windows support (OCamlPro/alt-ergo#1216) - Remove instructions to install Alt-Ergo on Debian (OCamlPro/alt-ergo#1217) - Document optimization feature (OCamlPro/alt-ergo#1231)

Halbaroth added this to the 2.6.0 milestone Oct 18, 2023

Stevendeo marked this pull request as ready for review October 18, 2023 14:12

Stevendeo requested review from bclement-ocp, hra687261 and Halbaroth and removed request for bclement-ocp and hra687261 October 18, 2023 14:12

Halbaroth reviewed Oct 18, 2023

View reviewed changes

Halbaroth added the clean-up label Oct 18, 2023

hra687261 approved these changes Oct 18, 2023

View reviewed changes

Stevendeo requested a review from Halbaroth October 18, 2023 15:43

bclement-ocp requested changes Oct 18, 2023

View reviewed changes

Stevendeo requested a review from bclement-ocp October 19, 2023 08:54

bclement-ocp reviewed Oct 19, 2023

View reviewed changes

Stevendeo requested a review from bclement-ocp October 19, 2023 13:59

Stevendeo added 6 commits October 24, 2023 10:06

Uniformization of internal identifiers generation

9a508a8

Format

4baf40d

Poetry

b757690

Using Compat

0576b04

Poetry

059d490

Keeping the '__'

fd4e4be

Stevendeo force-pushed the id-string branch from 5205d8a to fd4e4be Compare October 24, 2023 08:16

bclement-ocp approved these changes Oct 27, 2023

View reviewed changes

bclement-ocp merged commit 6a16170 into OCamlPro:next Oct 27, 2023
14 checks passed

Stevendeo mentioned this pull request Oct 27, 2023

Changing the internal variables prefix #918

Merged

bclement-ocp mentioned this pull request Sep 24, 2024

[new release] alt-ergo (4 packages) (2.6.0) ocaml/opam-repository#26609

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uniformization of internal identifiers generation #905

Uniformization of internal identifiers generation #905

Stevendeo commented Oct 18, 2023

Halbaroth Oct 18, 2023

Halbaroth Oct 18, 2023

Stevendeo Oct 18, 2023

Halbaroth Oct 18, 2023

Stevendeo Oct 18, 2023

bclement-ocp Oct 18, 2023

Stevendeo Oct 19, 2023

hra687261 left a comment

hra687261 Oct 18, 2023

Stevendeo Oct 18, 2023

Halbaroth Oct 18, 2023

bclement-ocp Oct 18, 2023

Stevendeo Oct 19, 2023

hra687261 Oct 18, 2023

bclement-ocp left a comment •

edited

Loading

bclement-ocp Oct 18, 2023

bclement-ocp Oct 18, 2023

bclement-ocp Oct 18, 2023

hra687261 Oct 19, 2023

Stevendeo Oct 19, 2023 •

edited

Loading

bclement-ocp Oct 19, 2023

bclement-ocp Oct 19, 2023

Stevendeo Oct 19, 2023

bclement-ocp left a comment

bclement-ocp commented Oct 19, 2023

Stevendeo commented Oct 23, 2023

Stevendeo commented Oct 24, 2023

Stevendeo commented Oct 27, 2023

bclement-ocp commented Oct 27, 2023

Uniformization of internal identifiers generation #905

Uniformization of internal identifiers generation #905

Conversation

Stevendeo commented Oct 18, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hra687261 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bclement-ocp left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Stevendeo Oct 19, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bclement-ocp left a comment

Choose a reason for hiding this comment

bclement-ocp commented Oct 19, 2023

Stevendeo commented Oct 23, 2023

Stevendeo commented Oct 24, 2023

Stevendeo commented Oct 27, 2023

bclement-ocp commented Oct 27, 2023

bclement-ocp left a comment •

edited

Loading

Stevendeo Oct 19, 2023 •

edited

Loading