From 64a6d434bb7c0e9c4e9ba8796cd07afb488f86c7 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Wed, 18 Oct 2023 15:06:01 +0200 Subject: [PATCH 1/4] Quoted identifiers --- src/lib/structures/symbols.ml | 15 ++++++++++++- tests/dune.inc | 21 +++++++++++++++++++ tests/smtlib/testfile-quoted1.dolmen.expected | 5 +++++ tests/smtlib/testfile-quoted1.dolmen.smt2 | 6 ++++++ 4 files changed, 46 insertions(+), 1 deletion(-) create mode 100644 tests/smtlib/testfile-quoted1.dolmen.expected create mode 100644 tests/smtlib/testfile-quoted1.dolmen.smt2 diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index cf09bf13d..d6513f0c4 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -294,8 +294,21 @@ let string_of_form f = match f with | F_Iff -> "<->" | F_Xor -> "xor" +let name_to_string = + let no_need_to_quote = + String.for_all + (function + | 'a' .. 'z' + | 'A' .. 'Z' + | '0' .. '9' + | '-' | '_' -> true + | _ -> false + ) + in + fun s -> if no_need_to_quote s then s else Format.sprintf "|%s|" s + let to_string ?(show_vars=true) x = match x with - | Name (n, _, _) -> Hstring.view n + | Name (n, _, _) -> name_to_string @@ Hstring.view n | Var v when show_vars -> Format.sprintf "'%s'" (Var.to_string v) | Var v -> Var.to_string v | Int n -> Z.to_string n diff --git a/tests/dune.inc b/tests/dune.inc index 3b21d9a7f..bead675a8 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -203615,6 +203615,27 @@ (package alt-ergo) (action (diff testfile-reset.dolmen.expected testfile-reset.dolmen_dolmen.output))) + (rule + (target testfile-quoted1.dolmen_dolmen.output) + (deps (:input testfile-quoted1.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-quoted1.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-quoted1.dolmen.expected testfile-quoted1.dolmen_dolmen.output))) (rule (target testfile-push-pop1.err.dolmen_dolmen.output) (deps (:input testfile-push-pop1.err.dolmen.smt2)) diff --git a/tests/smtlib/testfile-quoted1.dolmen.expected b/tests/smtlib/testfile-quoted1.dolmen.expected new file mode 100644 index 000000000..023946068 --- /dev/null +++ b/tests/smtlib/testfile-quoted1.dolmen.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun |fail))| () Int 0) +) diff --git a/tests/smtlib/testfile-quoted1.dolmen.smt2 b/tests/smtlib/testfile-quoted1.dolmen.smt2 new file mode 100644 index 000000000..d171116c9 --- /dev/null +++ b/tests/smtlib/testfile-quoted1.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const |fail))| Int) +(assert (= |fail))| 0)) +(check-sat) +(get-model) \ No newline at end of file From c71154ad530d2b7aed294e27deb29a6ee184ea25 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Wed, 18 Oct 2023 15:27:48 +0200 Subject: [PATCH 2/4] Adding special characters --- src/lib/structures/symbols.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index d6513f0c4..0914ac359 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -301,7 +301,9 @@ let name_to_string = | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' - | '-' | '_' -> true + | '~' | '!' | '@' | '$' | '%' | '^' | '&' + | '*' | '_' | '-' | '+' | '=' | '<' | '>' + | '.' | '?' | '/' -> true | _ -> false ) in From f23fa6752b6eb0a7ac7268c5097ee10521570c62 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Wed, 18 Oct 2023 15:30:16 +0200 Subject: [PATCH 3/4] Not starting with numbers --- src/lib/structures/symbols.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 0914ac359..e904ee80a 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -295,7 +295,9 @@ let string_of_form f = match f with | F_Xor -> "xor" let name_to_string = - let no_need_to_quote = + let no_need_to_quote s = + String.length s > 0 && + (match s.[0] with | '0'..'9' -> false | _ -> true) && String.for_all (function | 'a' .. 'z' @@ -305,7 +307,7 @@ let name_to_string = | '*' | '_' | '-' | '+' | '=' | '<' | '>' | '.' | '?' | '/' -> true | _ -> false - ) + ) s in fun s -> if no_need_to_quote s then s else Format.sprintf "|%s|" s From 38d63ef0ea674f41d26c5b5511d70364d91faac5 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Wed, 18 Oct 2023 15:44:23 +0200 Subject: [PATCH 4/4] Not String forall --- src/lib/structures/symbols.ml | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index e904ee80a..1e6ed1528 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -298,16 +298,19 @@ let name_to_string = let no_need_to_quote s = String.length s > 0 && (match s.[0] with | '0'..'9' -> false | _ -> true) && - String.for_all - (function - | 'a' .. 'z' - | 'A' .. 'Z' - | '0' .. '9' - | '~' | '!' | '@' | '$' | '%' | '^' | '&' - | '*' | '_' | '-' | '+' | '=' | '<' | '>' - | '.' | '?' | '/' -> true - | _ -> false - ) s + try + String.iter + (function + | 'a' .. 'z' + | 'A' .. 'Z' + | '0' .. '9' + | '~' | '!' | '@' | '$' | '%' | '^' | '&' + | '*' | '_' | '-' | '+' | '=' | '<' | '>' + | '.' | '?' | '/' -> () + | _ -> raise Exit + ) s; + true + with Exit -> false in fun s -> if no_need_to_quote s then s else Format.sprintf "|%s|" s