From cba2e7bc226edfcd0aed3fc169437ac294968f04 Mon Sep 17 00:00:00 2001 From: nilslommen Date: Tue, 18 Aug 2026 11:49:33 +0200 Subject: [PATCH] fix benchmarks --- Complexity_ITS/Lommen_26/README.md | 3 ++- Complexity_ITS/Lommen_26/collatz.ari | 4 ++-- Complexity_ITS/Lommen_26/collatz_mod_div.ari | 4 ++-- Complexity_ITS/Lommen_26/farkas.ari | 10 +++++----- Complexity_ITS/Lommen_26/farkas_mod_div.ari | 6 +++--- Complexity_ITS/Lommen_26/syracuse.ari | 8 ++++---- Complexity_ITS/Lommen_26/syracuse_mod_div.ari | 8 ++++---- Integer_Transition_Systems/Lommen_26/README.md | 3 ++- Integer_Transition_Systems/Lommen_26/collatz.ari | 4 ++-- .../Lommen_26/collatz_mod_div.ari | 4 ++-- Integer_Transition_Systems/Lommen_26/farkas.ari | 10 +++++----- .../Lommen_26/farkas_mod_div.ari | 6 +++--- Integer_Transition_Systems/Lommen_26/syracuse.ari | 8 ++++---- .../Lommen_26/syracuse_mod_div.ari | 8 ++++---- 14 files changed, 44 insertions(+), 42 deletions(-) diff --git a/Complexity_ITS/Lommen_26/README.md b/Complexity_ITS/Lommen_26/README.md index f4f9fcc5..d27ac266 100644 --- a/Complexity_ITS/Lommen_26/README.md +++ b/Complexity_ITS/Lommen_26/README.md @@ -5,4 +5,5 @@ The benchmark set consists of the following files: 2. Hershel M. Farkas' variant of the Collatz function (see, e.g., https://arxiv.org/pdf/2105.14697) 3. Hershel M. Farkas' variant of the Collatz function with mod and div (see, e.g., https://arxiv.org/pdf/2105.14697) 4. Syracuse variant of the Collatz function (see, e.g., https://arxiv.org/pdf/2105.14697) -5. Syracuse variant of the Collatz function (see, e.g., https://arxiv.org/pdf/2105.14697) +5. Syracuse variant of the Collatz function with mod and div (see, e.g., https://arxiv.org/pdf/2105.14697) + diff --git a/Complexity_ITS/Lommen_26/collatz.ari b/Complexity_ITS/Lommen_26/collatz.ari index bcfb3aa8..7ae6ad22 100644 --- a/Complexity_ITS/Lommen_26/collatz.ari +++ b/Complexity_ITS/Lommen_26/collatz.ari @@ -6,5 +6,5 @@ (fun collatz (-> Int Int)) (entrypoint start) (rule (start n) (collatz n)) -(rule (collatz n) (collatz k) :guard (= n (* 2 k))) -(rule (collatz n) (collatz (+ (* 3 n) 1)) :guard (= n (+ (* 2 k) 1))) +(rule (collatz n) (collatz k) :guard (and (> n 1) (= n (* 2 k)))) +(rule (collatz n) (collatz (+ (* 3 n) 1)) :guard (and (> n 1) (= n (+ (* 2 k) 1)))) diff --git a/Complexity_ITS/Lommen_26/collatz_mod_div.ari b/Complexity_ITS/Lommen_26/collatz_mod_div.ari index 12fa7602..03a9b877 100644 --- a/Complexity_ITS/Lommen_26/collatz_mod_div.ari +++ b/Complexity_ITS/Lommen_26/collatz_mod_div.ari @@ -6,5 +6,5 @@ (fun collatz (-> Int Int)) (entrypoint start) (rule (start n) (collatz n)) -(rule (collatz n) (collatz (div n 2)) :guard (= (mod n 2) 0)) -(rule (collatz n) (collatz (+ (* 3 n) 1)) :guard (= (mod n 2) 1)) +(rule (collatz n) (collatz (div n 2)) :guard (and (> n 1) (= (mod n 2) 0))) +(rule (collatz n) (collatz (+ (* 3 n) 1)) :guard (and (> n 1) (= (mod n 2) 1))) diff --git a/Complexity_ITS/Lommen_26/farkas.ari b/Complexity_ITS/Lommen_26/farkas.ari index 67e5fb79..c65c4ce4 100644 --- a/Complexity_ITS/Lommen_26/farkas.ari +++ b/Complexity_ITS/Lommen_26/farkas.ari @@ -6,8 +6,8 @@ (fun farkas (-> Int Int)) (entrypoint start) (rule (start n) (farkas n)) -(rule (farkas n) (farkas k) :guard (= n (+ (* 3 k) 1))) -(rule (farkas n) (farkas (* 3 k)) :guard (= n (* 6 k))) -(rule (farkas n) (farkas (+ (* 3 k) 1)) :guard (= n (+ (* 6 k) 2))) -(rule (farkas n) (farkas (+ (* 9 k) 5)) :guard (= n (+ (* 6 k) 3))) -(rule (farkas n) (farkas (+ (* 9 k) 8)) :guard (= n (+ (* 6 k) 5))) +(rule (farkas n) (farkas k) :guard (and (> n 1) (= n (+ (* 3 k) 1)))) +(rule (farkas n) (farkas (* 3 k)) :guard (and (> n 1) (= n (* 6 k)))) +(rule (farkas n) (farkas (+ (* 3 k) 1)) :guard (and (> n 1) (= n (+ (* 6 k) 2)))) +(rule (farkas n) (farkas (+ (* 9 k) 5)) :guard (and (> n 1) (= n (+ (* 6 k) 3)))) +(rule (farkas n) (farkas (+ (* 9 k) 8)) :guard (and (> n 1) (= n (+ (* 6 k) 5)))) diff --git a/Complexity_ITS/Lommen_26/farkas_mod_div.ari b/Complexity_ITS/Lommen_26/farkas_mod_div.ari index af489e1c..55231f67 100644 --- a/Complexity_ITS/Lommen_26/farkas_mod_div.ari +++ b/Complexity_ITS/Lommen_26/farkas_mod_div.ari @@ -6,6 +6,6 @@ (fun farkas (-> Int Int)) (entrypoint start) (rule (start n) (farkas n)) -(rule (farkas n) (farkas (div (- n 1) 3)) :guard (= (mod n 3) 1)) -(rule (farkas n) (farkas (div n 2)) :guard (or (= (mod n 6) 0) (= (mod n 6) 2))) -(rule (farkas n) (farkas (div (+ (* 3 n) 1) 2)) :guard (or (= (mod n 6) 3) (= (mod n 6) 5))) +(rule (farkas n) (farkas (div (- n 1) 3)) :guard (and (> n 1) (= (mod n 3) 1))) +(rule (farkas n) (farkas (div n 2)) :guard (and (> n 1) (or (= (mod n 6) 0) (= (mod n 6) 2)))) +(rule (farkas n) (farkas (div (+ (* 3 n) 1) 2)) :guard (and (> n 1) (or (= (mod n 6) 3) (= (mod n 6) 5)))) diff --git a/Complexity_ITS/Lommen_26/syracuse.ari b/Complexity_ITS/Lommen_26/syracuse.ari index f59c28a3..3227bdb7 100644 --- a/Complexity_ITS/Lommen_26/syracuse.ari +++ b/Complexity_ITS/Lommen_26/syracuse.ari @@ -1,4 +1,4 @@ -; Syracuse variant of the Collatz function with mod and div (see, e.g., https://arxiv.org/pdf/2105.14697) +; Syracuse variant of the Collatz function (see, e.g., https://arxiv.org/pdf/2105.14697) (format LCTRS) (theory Ints) @@ -6,6 +6,6 @@ (fun syracuse (-> Int Int)) (entrypoint start) (rule (start n) (syracuse n)) -(rule (syracuse n) (syracuse (+ (* 6 k) 1)) :guard (= n (+ (* 8 k) 1))) -(rule (syracuse n) (syracuse (+ (* 2 k) 1)) :guard (= n (+ (* 8 k) 5))) -(rule (syracuse n) (syracuse (+ (* 6 k) 5)) :guard (= n (+ (* 4 k) 3))) +(rule (syracuse n) (syracuse (+ (* 6 k) 1)) :guard (and (> n 1) (= n (+ (* 8 k) 1)))) +(rule (syracuse n) (syracuse (+ (* 2 k) 1)) :guard (and (> n 1) (= n (+ (* 8 k) 5)))) +(rule (syracuse n) (syracuse (+ (* 6 k) 5)) :guard (and (> n 1) (= n (+ (* 4 k) 3)))) diff --git a/Complexity_ITS/Lommen_26/syracuse_mod_div.ari b/Complexity_ITS/Lommen_26/syracuse_mod_div.ari index 4896e5d5..6509c5a3 100644 --- a/Complexity_ITS/Lommen_26/syracuse_mod_div.ari +++ b/Complexity_ITS/Lommen_26/syracuse_mod_div.ari @@ -1,4 +1,4 @@ -; Syracuse variant of the Collatz function (see, e.g., https://arxiv.org/pdf/2105.14697) +; Syracuse variant of the Collatz function with mod and div (see, e.g., https://arxiv.org/pdf/2105.14697) (format LCTRS) (theory Ints) @@ -6,6 +6,6 @@ (fun syracuse (-> Int Int)) (entrypoint start) (rule (start n) (syracuse n)) -(rule (syracuse n) (syracuse (div (+ (* 3 n) 1) 4)) :guard (= (mod n 8) 1)) -(rule (syracuse n) (syracuse (div (- n 1) 4)) :guard (= (mod n 8) 5)) -(rule (syracuse n) (syracuse (div (+ (* 3 n) 1) 2)) :guard (= (mod n 4) 3)) +(rule (syracuse n) (syracuse (div (+ (* 3 n) 1) 4)) :guard (and (> n 1) (= (mod n 8) 1))) +(rule (syracuse n) (syracuse (div (- n 1) 4)) :guard (and (> n 1) (= (mod n 8) 5))) +(rule (syracuse n) (syracuse (div (+ (* 3 n) 1) 2)) :guard (and (> n 1) (= (mod n 4) 3))) diff --git a/Integer_Transition_Systems/Lommen_26/README.md b/Integer_Transition_Systems/Lommen_26/README.md index f4f9fcc5..d27ac266 100644 --- a/Integer_Transition_Systems/Lommen_26/README.md +++ b/Integer_Transition_Systems/Lommen_26/README.md @@ -5,4 +5,5 @@ The benchmark set consists of the following files: 2. Hershel M. Farkas' variant of the Collatz function (see, e.g., https://arxiv.org/pdf/2105.14697) 3. Hershel M. Farkas' variant of the Collatz function with mod and div (see, e.g., https://arxiv.org/pdf/2105.14697) 4. Syracuse variant of the Collatz function (see, e.g., https://arxiv.org/pdf/2105.14697) -5. Syracuse variant of the Collatz function (see, e.g., https://arxiv.org/pdf/2105.14697) +5. Syracuse variant of the Collatz function with mod and div (see, e.g., https://arxiv.org/pdf/2105.14697) + diff --git a/Integer_Transition_Systems/Lommen_26/collatz.ari b/Integer_Transition_Systems/Lommen_26/collatz.ari index bcfb3aa8..7ae6ad22 100644 --- a/Integer_Transition_Systems/Lommen_26/collatz.ari +++ b/Integer_Transition_Systems/Lommen_26/collatz.ari @@ -6,5 +6,5 @@ (fun collatz (-> Int Int)) (entrypoint start) (rule (start n) (collatz n)) -(rule (collatz n) (collatz k) :guard (= n (* 2 k))) -(rule (collatz n) (collatz (+ (* 3 n) 1)) :guard (= n (+ (* 2 k) 1))) +(rule (collatz n) (collatz k) :guard (and (> n 1) (= n (* 2 k)))) +(rule (collatz n) (collatz (+ (* 3 n) 1)) :guard (and (> n 1) (= n (+ (* 2 k) 1)))) diff --git a/Integer_Transition_Systems/Lommen_26/collatz_mod_div.ari b/Integer_Transition_Systems/Lommen_26/collatz_mod_div.ari index 12fa7602..03a9b877 100644 --- a/Integer_Transition_Systems/Lommen_26/collatz_mod_div.ari +++ b/Integer_Transition_Systems/Lommen_26/collatz_mod_div.ari @@ -6,5 +6,5 @@ (fun collatz (-> Int Int)) (entrypoint start) (rule (start n) (collatz n)) -(rule (collatz n) (collatz (div n 2)) :guard (= (mod n 2) 0)) -(rule (collatz n) (collatz (+ (* 3 n) 1)) :guard (= (mod n 2) 1)) +(rule (collatz n) (collatz (div n 2)) :guard (and (> n 1) (= (mod n 2) 0))) +(rule (collatz n) (collatz (+ (* 3 n) 1)) :guard (and (> n 1) (= (mod n 2) 1))) diff --git a/Integer_Transition_Systems/Lommen_26/farkas.ari b/Integer_Transition_Systems/Lommen_26/farkas.ari index 67e5fb79..c65c4ce4 100644 --- a/Integer_Transition_Systems/Lommen_26/farkas.ari +++ b/Integer_Transition_Systems/Lommen_26/farkas.ari @@ -6,8 +6,8 @@ (fun farkas (-> Int Int)) (entrypoint start) (rule (start n) (farkas n)) -(rule (farkas n) (farkas k) :guard (= n (+ (* 3 k) 1))) -(rule (farkas n) (farkas (* 3 k)) :guard (= n (* 6 k))) -(rule (farkas n) (farkas (+ (* 3 k) 1)) :guard (= n (+ (* 6 k) 2))) -(rule (farkas n) (farkas (+ (* 9 k) 5)) :guard (= n (+ (* 6 k) 3))) -(rule (farkas n) (farkas (+ (* 9 k) 8)) :guard (= n (+ (* 6 k) 5))) +(rule (farkas n) (farkas k) :guard (and (> n 1) (= n (+ (* 3 k) 1)))) +(rule (farkas n) (farkas (* 3 k)) :guard (and (> n 1) (= n (* 6 k)))) +(rule (farkas n) (farkas (+ (* 3 k) 1)) :guard (and (> n 1) (= n (+ (* 6 k) 2)))) +(rule (farkas n) (farkas (+ (* 9 k) 5)) :guard (and (> n 1) (= n (+ (* 6 k) 3)))) +(rule (farkas n) (farkas (+ (* 9 k) 8)) :guard (and (> n 1) (= n (+ (* 6 k) 5)))) diff --git a/Integer_Transition_Systems/Lommen_26/farkas_mod_div.ari b/Integer_Transition_Systems/Lommen_26/farkas_mod_div.ari index af489e1c..55231f67 100644 --- a/Integer_Transition_Systems/Lommen_26/farkas_mod_div.ari +++ b/Integer_Transition_Systems/Lommen_26/farkas_mod_div.ari @@ -6,6 +6,6 @@ (fun farkas (-> Int Int)) (entrypoint start) (rule (start n) (farkas n)) -(rule (farkas n) (farkas (div (- n 1) 3)) :guard (= (mod n 3) 1)) -(rule (farkas n) (farkas (div n 2)) :guard (or (= (mod n 6) 0) (= (mod n 6) 2))) -(rule (farkas n) (farkas (div (+ (* 3 n) 1) 2)) :guard (or (= (mod n 6) 3) (= (mod n 6) 5))) +(rule (farkas n) (farkas (div (- n 1) 3)) :guard (and (> n 1) (= (mod n 3) 1))) +(rule (farkas n) (farkas (div n 2)) :guard (and (> n 1) (or (= (mod n 6) 0) (= (mod n 6) 2)))) +(rule (farkas n) (farkas (div (+ (* 3 n) 1) 2)) :guard (and (> n 1) (or (= (mod n 6) 3) (= (mod n 6) 5)))) diff --git a/Integer_Transition_Systems/Lommen_26/syracuse.ari b/Integer_Transition_Systems/Lommen_26/syracuse.ari index f59c28a3..3227bdb7 100644 --- a/Integer_Transition_Systems/Lommen_26/syracuse.ari +++ b/Integer_Transition_Systems/Lommen_26/syracuse.ari @@ -1,4 +1,4 @@ -; Syracuse variant of the Collatz function with mod and div (see, e.g., https://arxiv.org/pdf/2105.14697) +; Syracuse variant of the Collatz function (see, e.g., https://arxiv.org/pdf/2105.14697) (format LCTRS) (theory Ints) @@ -6,6 +6,6 @@ (fun syracuse (-> Int Int)) (entrypoint start) (rule (start n) (syracuse n)) -(rule (syracuse n) (syracuse (+ (* 6 k) 1)) :guard (= n (+ (* 8 k) 1))) -(rule (syracuse n) (syracuse (+ (* 2 k) 1)) :guard (= n (+ (* 8 k) 5))) -(rule (syracuse n) (syracuse (+ (* 6 k) 5)) :guard (= n (+ (* 4 k) 3))) +(rule (syracuse n) (syracuse (+ (* 6 k) 1)) :guard (and (> n 1) (= n (+ (* 8 k) 1)))) +(rule (syracuse n) (syracuse (+ (* 2 k) 1)) :guard (and (> n 1) (= n (+ (* 8 k) 5)))) +(rule (syracuse n) (syracuse (+ (* 6 k) 5)) :guard (and (> n 1) (= n (+ (* 4 k) 3)))) diff --git a/Integer_Transition_Systems/Lommen_26/syracuse_mod_div.ari b/Integer_Transition_Systems/Lommen_26/syracuse_mod_div.ari index 4896e5d5..6509c5a3 100644 --- a/Integer_Transition_Systems/Lommen_26/syracuse_mod_div.ari +++ b/Integer_Transition_Systems/Lommen_26/syracuse_mod_div.ari @@ -1,4 +1,4 @@ -; Syracuse variant of the Collatz function (see, e.g., https://arxiv.org/pdf/2105.14697) +; Syracuse variant of the Collatz function with mod and div (see, e.g., https://arxiv.org/pdf/2105.14697) (format LCTRS) (theory Ints) @@ -6,6 +6,6 @@ (fun syracuse (-> Int Int)) (entrypoint start) (rule (start n) (syracuse n)) -(rule (syracuse n) (syracuse (div (+ (* 3 n) 1) 4)) :guard (= (mod n 8) 1)) -(rule (syracuse n) (syracuse (div (- n 1) 4)) :guard (= (mod n 8) 5)) -(rule (syracuse n) (syracuse (div (+ (* 3 n) 1) 2)) :guard (= (mod n 4) 3)) +(rule (syracuse n) (syracuse (div (+ (* 3 n) 1) 4)) :guard (and (> n 1) (= (mod n 8) 1))) +(rule (syracuse n) (syracuse (div (- n 1) 4)) :guard (and (> n 1) (= (mod n 8) 5))) +(rule (syracuse n) (syracuse (div (+ (* 3 n) 1) 2)) :guard (and (> n 1) (= (mod n 4) 3)))