From 52cd9797ed538d0f9a2bca2725641f1472543ffc Mon Sep 17 00:00:00 2001
From: "Hichem R. A" <hichem.ait-el-hara@ocamlpro.com>
Date: Sun, 12 Mar 2023 19:23:11 +0100
Subject: [PATCH] [Array] Improved converter, added some tests, cleaned some
code
---
colibri2/tests/solve/smt_array/sat/dune | 8 -
colibri2/tests/solve/smt_array/sat/dune.inc | 66 ++---
.../{step_limit_reached => sat}/test1.smt2 | 0
.../smt_array/step_limit_reached/notes.txt | 18 +-
.../smt_array/step_limit_reached/test3.smt2 | 10 +
.../smt_array/step_limit_reached/test4.smt2 | 12 +
.../tests/solve/smt_array/unknown/test.smt2 | 5 -
colibri2/tests/solve/smt_array/unsat/dune | 8 -
colibri2/tests/solve/smt_array/unsat/dune.inc | 192 --------------
colibri2/theories/array/Array_Id_dom.ml | 26 --
colibri2/theories/array/Array_Id_dom.mli | 22 --
.../theories/array/{Index_Id_dom.ml => Id.ml} | 12 +-
.../array/{Index_Id_dom.mli => Id.mli} | 3 +-
colibri2/theories/array/RWRules.ml | 75 +++---
colibri2/theories/array/WEGraph.ml | 241 +++++++++---------
colibri2/theories/array/WEGraph.mli | 1 +
colibri2/theories/array/array.ml | 59 ++---
colibri2/theories/array/array_value.ml | 58 +++--
colibri2/theories/array/common.ml | 25 +-
colibri2/theories/array/common.mli | 7 +-
20 files changed, 305 insertions(+), 543 deletions(-)
rename colibri2/tests/solve/smt_array/{step_limit_reached => sat}/test1.smt2 (100%)
create mode 100644 colibri2/tests/solve/smt_array/step_limit_reached/test3.smt2
create mode 100644 colibri2/tests/solve/smt_array/step_limit_reached/test4.smt2
delete mode 100644 colibri2/tests/solve/smt_array/unknown/test.smt2
delete mode 100644 colibri2/theories/array/Array_Id_dom.ml
delete mode 100644 colibri2/theories/array/Array_Id_dom.mli
rename colibri2/theories/array/{Index_Id_dom.ml => Id.ml} (85%)
rename colibri2/theories/array/{Index_Id_dom.mli => Id.mli} (96%)
diff --git a/colibri2/tests/solve/smt_array/sat/dune b/colibri2/tests/solve/smt_array/sat/dune
index c645c9fbd..1a9a66cd4 100644
--- a/colibri2/tests/solve/smt_array/sat/dune
+++ b/colibri2/tests/solve/smt_array/sat/dune
@@ -19,14 +19,6 @@
--options
"array-wegraph"
--options
- "array-choice"
- --options
- "array-res-ext array-choice"
- --options
- "array-res-ext array-res-aup array-choice"
- --options
- "array-wegraph array-choice"
- --options
"array-wegraph array-res-ext"
--options
"array-wegraph array-res-ext array-res-aup"
diff --git a/colibri2/tests/solve/smt_array/sat/dune.inc b/colibri2/tests/solve/smt_array/sat/dune.inc
index b97809dc1..a857a17e3 100644
--- a/colibri2/tests/solve/smt_array/sat/dune.inc
+++ b/colibri2/tests/solve/smt_array/sat/dune.inc
@@ -8,6 +8,9 @@
--dont-print-result %{dep:neq.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat
--dont-print-result %{dep:test2.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat
@@ -20,6 +23,9 @@
--dont-print-result %{dep:neq.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat
--dont-print-result %{dep:test2.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat
@@ -32,6 +38,9 @@
--dont-print-result %{dep:neq.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat
--dont-print-result %{dep:test2.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat
@@ -44,56 +53,11 @@
--dont-print-result %{dep:neq.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat
--dont-print-result %{dep:test2.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat
---dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat
---dont-print-result %{dep:imp1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat
---dont-print-result %{dep:neq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat
---dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat
---dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat
---dont-print-result %{dep:imp1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat
---dont-print-result %{dep:neq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat
---dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat
---dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat
---dont-print-result %{dep:imp1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat
---dont-print-result %{dep:neq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat
---dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat
---dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat
---dont-print-result %{dep:imp1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat
---dont-print-result %{dep:neq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat
---dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat
--dont-print-result %{dep:eq.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
@@ -104,6 +68,9 @@
--dont-print-result %{dep:neq.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat
--dont-print-result %{dep:test2.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat
@@ -116,5 +83,8 @@
--dont-print-result %{dep:neq.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat
--dont-print-result %{dep:test2.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_array/step_limit_reached/test1.smt2 b/colibri2/tests/solve/smt_array/sat/test1.smt2
similarity index 100%
rename from colibri2/tests/solve/smt_array/step_limit_reached/test1.smt2
rename to colibri2/tests/solve/smt_array/sat/test1.smt2
diff --git a/colibri2/tests/solve/smt_array/step_limit_reached/notes.txt b/colibri2/tests/solve/smt_array/step_limit_reached/notes.txt
index bea66e0bf..fbc29c056 100644
--- a/colibri2/tests/solve/smt_array/step_limit_reached/notes.txt
+++ b/colibri2/tests/solve/smt_array/step_limit_reached/notes.txt
@@ -1,6 +1,14 @@
-- sat/test1.smt2:
- "--array-wegraph --array-res-ext"
- "--array-wegraph --array-res-ext --array-res-aup"
+- sat/test3.smt2:
+ works with:
+ - "--array-res-ext"
+ - "--array-wegraph --array-res-ext"
+
+- sat/test4.smt2:
+ works with:
+ - ""
+ - "--array-wegraph"
+
- unsat/distinct2:
- ""
- "--array-wegraph"
\ No newline at end of file
+ fails with:
+ - ""
+ - "--array-wegraph"
diff --git a/colibri2/tests/solve/smt_array/step_limit_reached/test3.smt2 b/colibri2/tests/solve/smt_array/step_limit_reached/test3.smt2
new file mode 100644
index 000000000..9a9c9357c
--- /dev/null
+++ b/colibri2/tests/solve/smt_array/step_limit_reached/test3.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_ALIA)
+(declare-fun a () (Array Int Int))
+(declare-fun i () Int)
+(declare-fun j () Int)
+(assert (not
+ (=
+ (store a j (select a j))
+ (store (store a i (select a j)) j (select a i))
+ )))
+(check-sat)
diff --git a/colibri2/tests/solve/smt_array/step_limit_reached/test4.smt2 b/colibri2/tests/solve/smt_array/step_limit_reached/test4.smt2
new file mode 100644
index 000000000..1723526e7
--- /dev/null
+++ b/colibri2/tests/solve/smt_array/step_limit_reached/test4.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AX)
+(declare-sort I 0)
+(declare-sort E 0)
+(declare-fun a () (Array I E))
+(declare-fun i () I)
+(declare-fun i5 () I)
+(assert (not
+ (=
+ (store a i5 (select a i5))
+ (store (store a i (select a i5)) i5 (select a i))
+ )))
+(check-sat)
diff --git a/colibri2/tests/solve/smt_array/unknown/test.smt2 b/colibri2/tests/solve/smt_array/unknown/test.smt2
deleted file mode 100644
index 5fe0c9fbf..000000000
--- a/colibri2/tests/solve/smt_array/unknown/test.smt2
+++ /dev/null
@@ -1,5 +0,0 @@
-(set-logic ALIRA)
-(declare-fun s_ () (Array Int Real))
-(declare-fun s () (Array Int (Array Int Real)))
-(assert (and (forall ((_? Int)) false) (or false (exists ((_? Int)) (and true (exists ((__? Int)) (distinct (select s_ 0) (select (select s 0) 0))))))))
-(check-sat)
diff --git a/colibri2/tests/solve/smt_array/unsat/dune b/colibri2/tests/solve/smt_array/unsat/dune
index 442cde88b..96fdbfc04 100644
--- a/colibri2/tests/solve/smt_array/unsat/dune
+++ b/colibri2/tests/solve/smt_array/unsat/dune
@@ -19,14 +19,6 @@
--options
"array-wegraph"
--options
- "array-choice"
- --options
- "array-res-ext array-choice"
- --options
- "array-res-ext array-res-aup array-choice"
- --options
- "array-wegraph array-choice"
- --options
"array-wegraph array-res-ext"
--options
"array-wegraph array-res-ext array-res-aup"
diff --git a/colibri2/tests/solve/smt_array/unsat/dune.inc b/colibri2/tests/solve/smt_array/unsat/dune.inc
index da28d39ec..2f106c45c 100644
--- a/colibri2/tests/solve/smt_array/unsat/dune.inc
+++ b/colibri2/tests/solve/smt_array/unsat/dune.inc
@@ -190,198 +190,6 @@
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat
--dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:distinct.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:eq2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:eq3.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:eq4.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:impls1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:impls2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:impls3.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:impls4.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:impls5.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:impls6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:out.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:out.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:select.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
---dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:distinct.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:eq2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:eq3.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:eq4.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:impls1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:impls2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:impls3.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:impls4.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:impls5.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:impls6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:out.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:out.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:select.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
---dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:distinct.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:eq2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:eq3.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:eq4.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:impls1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:impls2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:impls3.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:impls4.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:impls5.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:impls6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:out.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:out.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:select.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
---dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:distinct.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:eq2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:eq3.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:eq4.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:impls1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:impls2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:impls3.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:impls4.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:impls5.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:impls6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:out.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:out.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:select.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
---dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status unsat
--dont-print-result %{dep:distinct.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
diff --git a/colibri2/theories/array/Array_Id_dom.ml b/colibri2/theories/array/Array_Id_dom.ml
deleted file mode 100644
index 3c8928ebd..000000000
--- a/colibri2/theories/array/Array_Id_dom.ml
+++ /dev/null
@@ -1,26 +0,0 @@
-(*************************************************************************)
-(* This file is part of Colibri2. *)
-(* *)
-(* Copyright (C) 2014-2021 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* OCamlPro *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
-
-include Common.MkIdDom (struct
- let n1 = "Array.Array_Id_dom.merge_hooks"
- let n2 = "Array.Id"
- let n3 = "Array.Array_Id_dom.new_id_hooks"
-end)
diff --git a/colibri2/theories/array/Array_Id_dom.mli b/colibri2/theories/array/Array_Id_dom.mli
deleted file mode 100644
index 438f2ca30..000000000
--- a/colibri2/theories/array/Array_Id_dom.mli
+++ /dev/null
@@ -1,22 +0,0 @@
-(*************************************************************************)
-(* This file is part of Colibri2. *)
-(* *)
-(* Copyright (C) 2014-2021 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* OCamlPro *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
-
-include Common.IdDomSig
diff --git a/colibri2/theories/array/Index_Id_dom.ml b/colibri2/theories/array/Id.ml
similarity index 85%
rename from colibri2/theories/array/Index_Id_dom.ml
rename to colibri2/theories/array/Id.ml
index cc31f2a45..e79df540f 100644
--- a/colibri2/theories/array/Index_Id_dom.ml
+++ b/colibri2/theories/array/Id.ml
@@ -19,8 +19,14 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-include Common.MkIdDom (struct
- let n1 = "Array.Index_Id_dom.merge_hooks"
+module Array = Common.MkIdDom (struct
+ let n1 = "Array.Id.Array.merge_hooks"
+ let n2 = "Array.Id"
+ let n3 = "Array.Id.Array.new_id_hooks"
+end)
+
+module Index = Common.MkIdDom (struct
+ let n1 = "Array.Id.Index.merge_hooks"
let n2 = "Array.Index_id"
- let n3 = "Array.Index_Id_dom.new_id_hooks"
+ let n3 = "Array.Id.Index.new_id_hooks"
end)
diff --git a/colibri2/theories/array/Index_Id_dom.mli b/colibri2/theories/array/Id.mli
similarity index 96%
rename from colibri2/theories/array/Index_Id_dom.mli
rename to colibri2/theories/array/Id.mli
index 438f2ca30..452ee58cf 100644
--- a/colibri2/theories/array/Index_Id_dom.mli
+++ b/colibri2/theories/array/Id.mli
@@ -19,4 +19,5 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-include Common.IdDomSig
+module Array : Common.IdDomSig
+module Index : Common.IdDomSig
diff --git a/colibri2/theories/array/RWRules.ml b/colibri2/theories/array/RWRules.ml
index 91cab7705..5283b457b 100644
--- a/colibri2/theories/array/RWRules.ml
+++ b/colibri2/theories/array/RWRules.ml
@@ -108,14 +108,14 @@ let raup_pattern, raup_run =
let term = mk_store_term STV.tb STV.ti STV.tv in
let raup_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
let raup_run env subst =
- Debug.dprintf2 debug "Found raup1 with %a" Ground.Subst.pp subst;
let n = convert ~subst env term in
Egraph.register env n;
+ Debug.dprintf2 debug "Found raup1 with %a" Ground.Subst.pp subst;
let term_bis = mk_select_term STV.tb STV.tj in
let raup_pattern_bis = Pattern.of_term_exn ~subst term_bis in
let raup_run_bis env subst_bis =
- Debug.dprintf2 debug "Found raup2 with %a" Ground.Subst.pp subst;
let subst = Ground.Subst.distinct_union subst_bis subst in
+ Debug.dprintf2 debug "Found raup2 with %a" Ground.Subst.pp subst;
let bn = convert ~subst env STV.tb in
match Egraph.get_dom env Linearity_dom.key bn with
| Some NonLinear ->
@@ -129,9 +129,12 @@ let raup_pattern, raup_run =
(mk_select_term STV.tb STV.tj);
])
in
+ Debug.dprintf2 debug "Apply raup2: set %a to true" Node.pp v;
Egraph.register env v;
Boolean.set_true env v
- | _ -> ()
+ | _ ->
+ Debug.dprintf2 debug "Do not apply raup2: %a is not non-linear"
+ Node.pp bn
in
InvertedPath.add_callback env raup_pattern_bis raup_run_bis
in
@@ -202,9 +205,7 @@ let apply_res_ext_1_2_aux env ind_gty val_gty l tyvt =
(fun (cnt, tsubst, tns) node ->
let anv = Expr.Term.Var.mk (Format.sprintf "a%d" cnt) tyvt in
let anvt = Expr.Term.of_var anv in
- ( cnt + 1,
- (anv, node) :: tsubst,
- (anvt, Array_Id_dom.get_id env node) :: tns ))
+ (cnt + 1, (anv, node) :: tsubst, (anvt, Id.Array.get_id env node) :: tns))
(0, [], []) l
in
let tysubst = [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ] in
@@ -239,44 +240,46 @@ let apply_res_ext_1_1, apply_res_ext_1_2 =
applies res-ext-2 on the new foreign array and all the other foregin arrays
which are its neighbours in the WEGraph *)
let get_foreign_neighbours env a arr_set =
- let aid = Array_Id_dom.get_id env a in
+ let aid = Id.Array.get_id env a in
let nps = WEGraph.get_neighbours env aid in
Node.S.fold
(fun node acc ->
- if DInt.S.mem (Array_Id_dom.get_id env node) nps then Node.S.add node acc
+ if DInt.S.mem (Id.Array.get_id env node) nps then Node.S.add node acc
else acc)
arr_set Node.S.empty
+let apply_ext env a b =
+ let ind_gty, val_gty = array_gty_args (get_array_gty env a) in
+ let eq = Equality.equality env [ a; b ] in
+ let diseq = mk_distinct_arrays env a b ind_gty val_gty in
+ Debug.dprintf4 debug "Application of the extensionality rule on %a and %a"
+ Node.pp a Node.pp b;
+ Egraph.register env eq;
+ Egraph.register env diseq;
+ Choice.register_global env
+ {
+ Choice.print_cho = "Decision from extensionality application.";
+ Choice.prio = 1;
+ choice =
+ (fun env ->
+ match (Boolean.is env eq, Boolean.is env diseq) with
+ | Some true, Some false -> Choice.DecNo
+ | Some false, Some true -> Choice.DecNo
+ | _ ->
+ Choice.DecTodo
+ [
+ (fun env ->
+ Boolean.set_true env eq;
+ Boolean.set_false env diseq);
+ (fun env ->
+ Boolean.set_false env eq;
+ Boolean.set_true env diseq);
+ ]);
+ }
+
(* a, b, {a,b} ⊆ foreign |> (a = b) ⋠(a[k] ≠b[k]) *)
let apply_res_ext_2_1, apply_res_ext_2_2 =
let foreign_array_db = GTHT.create Node.S.pp "foreign_array_db" in
- let apply_ext ?(choice = false) env a b =
- let ind_gty, val_gty = array_gty_args (get_array_gty env a) in
- let eq = Equality.equality env [ a; b ] in
- let dist = mk_distinct_arrays env a b ind_gty val_gty in
- let disj = mk_or env eq dist in
- Debug.dprintf4 debug "Application of the extensionality rule on %a and %a"
- Node.pp a Node.pp b;
- Egraph.register env disj;
- if choice then
- Choice.register_global env
- {
- Choice.print_cho = "Decision from WEGraph_merge_neighbours.";
- Choice.prio = 1;
- choice =
- (fun env ->
- match Boolean.is env disj with
- | Some true -> Choice.DecNo
- | Some false -> Choice.DecNo
- | None ->
- Choice.DecTodo
- [
- (fun env -> Boolean.set_true env eq);
- (fun env -> Boolean.set_true env dist);
- ]);
- }
- else Boolean.set_true env disj
- in
let apply_res_ext_2 f env aty a =
match aty with
| Ground.Ty.{ app = { builtin = Expr.Array; _ }; _ } ->
@@ -324,7 +327,7 @@ let new_array =
let b = Ground.node f2 in
let adist = mk_distinct_arrays env a b ind_gty val_gty in
let aeq = Equality.equality env [ a; b ] in
- let n = mk_or env adist aeq in
+ let n = mk_or env [ adist; aeq ] in
Debug.dprintf4 debug "Found ext with %a and %a" Ground.pp f2
Ground.pp f;
Egraph.register env n;
diff --git a/colibri2/theories/array/WEGraph.ml b/colibri2/theories/array/WEGraph.ml
index 47a1f26bf..31a20ca85 100644
--- a/colibri2/theories/array/WEGraph.ml
+++ b/colibri2/theories/array/WEGraph.ml
@@ -587,77 +587,6 @@ let are_neighbours env id1 id2 =
| None -> false
| Some (_, m) -> DInt.M.mem id2 m
-let add_neighbour env (srcid, srcn) (destid, destn) ind ind_gty val_gty =
- let iid = Index_Id_dom.get_id env ind in
- Debug.dprintf6 debug "WEGraph: add_neighbour %a to %a through %a" (pp_eid env)
- srcid (pp_eid env) destid (pp_vid env) iid;
- WEG.change env destid ~f:(function
- | None ->
- Some
- ( DInt.M.singleton iid (DInt.S.singleton srcid),
- DInt.M.singleton srcid iid )
- | Some (m1, m2) ->
- Some
- ( DInt.M.change
- (function
- | Some nps -> Some (DInt.S.add srcid nps)
- | None -> Some (DInt.S.singleton srcid))
- iid m1,
- DInt.M.change
- (function
- | Some iid' ->
- let ind' = VHT.find env iid' in
- if not (Egraph.is_equal env ind ind') then (
- (* if a and b are already neighbours and k and k' are not
- equal then set (k = k' \/ a[k] = b[k] \/ a[k'] = b[k']) to true *)
- let eq1 = Equality.equality env [ ind; ind' ] in
- let eq2 =
- Equality.equality env
- [
- mk_select env srcn ind ind_gty val_gty;
- mk_select env destn ind ind_gty val_gty;
- ]
- in
- let eq3 =
- Equality.equality env
- [
- mk_select env srcn ind' ind_gty val_gty;
- mk_select env destn ind' ind_gty val_gty;
- ]
- in
- let disj = mk_or env eq1 (mk_or env eq2 eq3) in
- Egraph.register env disj;
- if Options.get env use_choice then
- Choice.register_global env
- {
- Choice.print_cho = "Decision from add_neighbour.";
- Choice.prio = 1;
- choice =
- (fun env ->
- match Boolean.is env disj with
- | Some true -> Choice.DecNo
- | Some false -> Choice.DecNo
- | None ->
- Choice.DecTodo
- [
- (fun env -> Boolean.set_true env eq1);
- (fun env -> Boolean.set_true env eq2);
- (fun env -> Boolean.set_true env eq3);
- ]);
- }
- else Boolean.set_true env disj;
- Debug.dprintf10 debug
- "WEGraph: adding %a as a neighbour to %a through %a: \
- setting %a = %a to true"
- Node.pp srcn Node.pp destn Node.pp ind Node.pp ind
- Node.pp ind');
- (* Don't do anything right away, assume that the
- activation of the equality hook will take care of
- normalizing the graph. *)
- Some iid
- | None -> Some iid)
- srcid m2 ))
-
let rm_neighbour env (kid, knode) (rid, rnode) iid =
let ind = VHT.find env iid in
Debug.dprintf6 debug "WEGraph: rm_neighbour %a of %a through %a" (pp_eid env)
@@ -701,6 +630,88 @@ let are_k_neibnours env aid bid iid =
| None -> false
| Some iid' -> iid = iid')
+let add_neighbour vid aid = function
+ | None ->
+ Some
+ (DInt.M.singleton vid (DInt.S.singleton aid), DInt.M.singleton aid vid)
+ | Some (m1, m2) ->
+ Some
+ ( DInt.M.change
+ (function
+ | None -> Some (DInt.S.singleton aid)
+ | Some s -> Some (DInt.S.add aid s))
+ vid m1,
+ DInt.M.add aid vid m2 )
+
+let add_edge_aux env (a, aid) (b, bid) (i, iid) ind_gty val_gty =
+ Debug.dprintf6 debug "WEGraph: add_edge_aux %a between %a and %a" (pp_vid env)
+ iid (pp_eid env) aid (pp_eid env) bid;
+ match DInt.M.find_opt bid (snd (WEG.find env aid)) with
+ | Some jid when iid = jid -> ()
+ | None ->
+ WEG.change env aid ~f:(add_neighbour iid bid);
+ WEG.change env bid ~f:(add_neighbour iid aid)
+ | Some jid ->
+ let j = VHT.find env jid in
+ let ij_eq = Equality.equality env [ i; j ] in
+ let ij_neq = Equality.disequality env [ i; j ] in
+ Egraph.register env ij_eq;
+ Egraph.register env ij_neq;
+ Choice.register_global env
+ {
+ Choice.print_cho = "Decision from adding an edge in the WEGgraph.";
+ Choice.prio = 1;
+ choice =
+ (fun env ->
+ let ai = mk_select env a i ind_gty val_gty in
+ let aj = mk_select env a j ind_gty val_gty in
+ let bi = mk_select env b i ind_gty val_gty in
+ let bj = mk_select env b j ind_gty val_gty in
+ match (Boolean.is env ij_eq, Boolean.is env ij_neq) with
+ | Some true, _ ->
+ (* if i = j then a[i] = a[j] & b[i] = b[j] *)
+ let eq =
+ mk_and env
+ [
+ Equality.equality env [ ai; aj ];
+ Equality.equality env [ bi; bj ];
+ ]
+ in
+ Egraph.register env eq;
+ Boolean.set_true env eq;
+ WEG.change env aid ~f:(add_neighbour iid bid);
+ WEG.change env bid ~f:(add_neighbour iid aid);
+ Choice.DecNo
+ | _, Some true -> (
+ (* if i =/= j then a[i] = b[i] or a[j] = b[j] *)
+ let ieq = Equality.equality env [ ai; bi ] in
+ let jeq = Equality.equality env [ aj; bj ] in
+ Egraph.register env ieq;
+ Egraph.register env jeq;
+ match (Boolean.is env ieq, Boolean.is env jeq) with
+ | Some true, Some true ->
+ (* if a[i] = b[i] & a[j] = b[j] then a = b *)
+ let eq = Equality.equality env [ a; b ] in
+ Egraph.register env eq;
+ Boolean.set_true env eq;
+ Choice.DecNo
+ | Some true, _ ->
+ WEG.change env aid ~f:(add_neighbour jid bid);
+ WEG.change env bid ~f:(add_neighbour jid aid);
+ Choice.DecNo
+ | _, Some true ->
+ WEG.change env aid ~f:(add_neighbour iid bid);
+ WEG.change env bid ~f:(add_neighbour iid aid);
+ Choice.DecNo
+ | _ -> Choice.DecNo)
+ | _ ->
+ Choice.DecTodo
+ [
+ (fun env -> Boolean.set_true env ij_eq);
+ (fun env -> Boolean.set_true env ij_neq);
+ ]);
+ }
+
let add_edge env aid bid iid =
(* when adding a node dest as a neighbour to a node src, dest is also added
as a neighbour to all the nodes in the complete graph formed by all the
@@ -724,8 +735,7 @@ let add_edge env aid bid iid =
Vertices.change env iid ~f:(function
| Some s -> Some (Vertex.S.add (id1, id2) s)
| None -> Some (Vertex.S.singleton (id1, id2)));
- add_neighbour env (id1, n1) (id2, n2) ind ind_gty val_gty;
- add_neighbour env (id2, n2) (id1, n1) ind ind_gty val_gty))
+ add_edge_aux env (n1, id1) (n2, id2) (ind, iid) ind_gty val_gty))
(DInt.S.add bid bnk))
(DInt.S.add aid ank)
@@ -764,50 +774,43 @@ let rm_edge_aux env aid bid iid =
(pp_vid env) iid)
env ()
-let merge_neigbours_aux env (kn, kid) (rn, rid) nid kk_opt kr_opt () =
+let merge_neigbours_aux env (a, aid) (b, bid) nid kk_opt kr_opt () =
match (kk_opt, kr_opt) with
- | Some iid1, Some iid2 ->
- let ind1 = VHT.find env iid1 in
- let ind2 = VHT.find env iid2 in
+ | Some iid, Some jid ->
+ let i = VHT.find env iid in
+ let j = VHT.find env jid in
Debug.dprintf6 debug
"WEGraph: _merge_neigbours_aux: iter1: found the neighbour %a through \
%a and %a"
- (pp_eid env) nid (pp_vid env) iid1 (pp_vid env) iid2;
- (* if a node X is a neighbour of both A and B through the edges
- ind1 and ind2 (resp.) then (ind1 = ind2) must be set to true, and
- only the ind1 edge should be kept. *)
- if not (Egraph.is_equal env ind1 ind2) then (
- let nidn = EHT.find env nid in
- let eq1 = Equality.equality env [ ind1; ind2 ] in
- let eq2 = Equality.equality env [ kn; nidn ] in
- let disj = mk_or env eq1 eq2 in
- Egraph.register env disj;
- if Options.get env use_choice then
- Choice.register_global env
- {
- Choice.print_cho = "Decision from WEGraph_merge_neighbours.";
- Choice.prio = 1;
- choice =
- (fun env ->
- match Boolean.is env disj with
- | Some true -> Choice.DecNo
- | Some false -> Choice.DecNo
- | None ->
- Choice.DecTodo
- [
- (fun env -> Boolean.set_true env eq1);
- (fun env -> Boolean.set_true env eq2);
- ]);
- }
- else Boolean.set_true env disj);
- rm_edge_aux env nid rid iid2
+ (pp_eid env) nid (pp_vid env) iid (pp_vid env) jid;
+ if not (Egraph.is_equal env i j) then (
+ let ijeq = Equality.equality env [ i; j ] in
+ let aneq = Equality.equality env [ a; EHT.find env nid ] in
+ Egraph.register env ijeq;
+ Egraph.register env aneq;
+ Choice.register_global env
+ {
+ Choice.print_cho = "Decision from merging nodes in the WEGgraph.";
+ Choice.prio = 1;
+ choice =
+ (fun env ->
+ match (Boolean.is env ijeq, Boolean.is env aneq) with
+ | Some true, _ | _, Some true -> Choice.DecNo
+ | _ ->
+ Choice.DecTodo
+ [
+ (fun env -> Boolean.set_true env ijeq);
+ (fun env -> Boolean.set_true env aneq);
+ ]);
+ });
+ rm_edge_aux env nid bid jid
| None, Some iid ->
Debug.dprintf4 debug
"WEGraph: _merge_neigbours_aux: iter2: found the neighbour %a through \
%a"
(pp_eid env) nid (pp_vid env) iid;
- rm_edge_aux env nid rid iid;
- add_edge_aux kn rn env nid kid iid
+ rm_edge_aux env nid bid iid;
+ add_edge_aux a b env nid aid iid
| _ -> ()
let merge_neighbours env (kn, kid) (rn, rid) b =
@@ -888,7 +891,7 @@ let ineq_indices_norm env s =
let ns =
List.filter_map
(fun n ->
- match Index_Id_dom.get_id env n with
+ match Id.Index.get_id env n with
| id -> Some id
| exception NoIdFound _ -> None)
(Node.S.elements s)
@@ -896,9 +899,9 @@ let ineq_indices_norm env s =
KnownValues.ineq_indices_norm env ns
let new_store env a b ind v =
- let aid = Array_Id_dom.get_id env a in
- let bid = Array_Id_dom.get_id env b in
- let iid = Index_Id_dom.get_id env ind in
+ let aid = Id.Array.get_id env a in
+ let bid = Id.Array.get_id env b in
+ let iid = Id.Index.get_id env ind in
Debug.dprintf6 debug "WEGraph.new_store: %a %a %a" (pp_eid env) aid
(pp_eid env) bid (pp_vid env) iid;
add_edge env aid bid iid;
@@ -911,8 +914,8 @@ let new_store env a b ind v =
env ()
let new_select env r a i =
- let aid = Array_Id_dom.get_id env a in
- let iid = Index_Id_dom.get_id env i in
+ let aid = Id.Array.get_id env a in
+ let iid = Id.Index.get_id env i in
Debug.dprintf4 debug "WEGraph.new_select: %a %a" (pp_eid env) aid (pp_vid env)
iid;
match KnownValues.HT.find_opt env aid with
@@ -945,3 +948,13 @@ let new_id_hook env id n =
let new_index_id_hook env id n =
Vertices.set env id Vertex.S.empty;
VHT.set env id n
+
+let get_array_kvs env n =
+ match KnownValues.HT.find_opt env (Id.Array.get_id env n) with
+ | Some kv ->
+ DInt.M.fold
+ (fun i v acc ->
+ let indn = VHT.find env i in
+ Node.M.add indn v acc)
+ kv Node.M.empty
+ | None -> Node.M.empty
diff --git a/colibri2/theories/array/WEGraph.mli b/colibri2/theories/array/WEGraph.mli
index cec8868ed..151e2fa8f 100644
--- a/colibri2/theories/array/WEGraph.mli
+++ b/colibri2/theories/array/WEGraph.mli
@@ -36,3 +36,4 @@ val new_select : Egraph.wt -> Node.t -> Node.t -> Node.t -> unit
val get_neighbours : Egraph.wt -> int -> DInt.S.t
val new_id_hook : Egraph.wt -> int -> Node.t -> unit
val new_index_id_hook : Egraph.wt -> int -> Node.t -> unit
+val get_array_kvs : Egraph.wt -> Node.t -> Node.t Node.M.t
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 9e7c81d26..af663f3e7 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -45,7 +45,7 @@ let converter env (f : Ground.t) =
match s.ty with
| { app = { builtin = Expr.Array; _ }; args = [ ind_gty; val_gty ]; _ } ->
add_array_gty env fn ind_gty val_gty;
- Array_Id_dom.set_id env fn;
+ Id.Array.set_id env fn;
new_array env ind_gty val_gty f;
true
| _ -> false
@@ -74,7 +74,7 @@ let converter env (f : Ground.t) =
let gty = Ground.Ty.convert subst (List.nth arg_tys i) in
match gty with
| { app = { builtin = Expr.Array; _ }; _ } ->
- Array_Id_dom.set_id env n;
+ Id.Array.set_id env n;
Ground.add_ty env n gty;
Foreign_dom.set_dom env gty n IsForeign
| _ -> ())
@@ -90,8 +90,8 @@ let converter env (f : Ground.t) =
Egraph.register env a;
Egraph.register env i;
add_array_gty env a ind_gty val_gty;
- Array_Id_dom.set_id env a;
- Index_Id_dom.set_id env i;
+ Id.Array.set_id env a;
+ Id.Index.set_id env i;
Ground.add_ty env i ind_gty;
if Options.get env use_wegraph then WEGraph.new_select env fn a i;
(* update of the Foreign domain *)
@@ -133,39 +133,30 @@ let converter env (f : Ground.t) =
add_array_gty env b ind_gty val_gty;
Ground.add_ty env v val_gty;
Ground.add_ty env k ind_gty;
- Array_Id_dom.set_id env a;
- Array_Id_dom.set_id env b;
- Index_Id_dom.set_id env k;
+ Id.Array.set_id env a;
+ Id.Array.set_id env b;
+ Id.Index.set_id env k;
(* update of the Linearity domain *)
if Options.get env restrict_aup then
Linearity_dom.upd_dom env fn (Linear b);
(* application of the `idx` rule *)
- let store_n = mk_store env b k v ind_gty val_gty in
- let rn =
- Equality.equality env [ mk_select env store_n k ind_gty val_gty; v ]
- in
+ let rn = Equality.equality env [ mk_select env a k ind_gty val_gty; v ] in
Egraph.register env rn;
Boolean.set_true env rn;
(* application of the `Uð›¿` rule *)
if Options.get env default_values then (
- let eq_node = Equality.equality env [ store_n; b ] in
+ let eq_node =
+ Equality.equality env
+ [
+ ground_apply env Builtin.array_default_value [ ind_gty; val_gty ]
+ [ a ];
+ ground_apply env Builtin.array_default_value [ ind_gty; val_gty ]
+ [ b ];
+ ]
+ in
Egraph.register env eq_node;
Boolean.set_true env eq_node);
- if Options.get env use_wegraph then (
- let ak = mk_select env a k ind_gty val_gty in
- Egraph.register env ak;
- if not (Egraph.is_equal env ak v) then (
- let akv_eq = Equality.equality env [ ak; v ] in
- Egraph.register env akv_eq;
- Boolean.set_true env akv_eq);
- let bk = mk_select env b k ind_gty val_gty in
- Egraph.register env bk;
- if Egraph.is_equal env bk v then (
- (* is this necessary? *)
- let eqn = Equality.equality env [ a; b ] in
- Egraph.register env eqn;
- Boolean.set_true env eqn)
- else WEGraph.new_store env a b k v)
+ if Options.get env use_wegraph then WEGraph.new_store env a b k v
| {
app = { builtin = Builtin.Array_diff; _ };
args;
@@ -176,8 +167,8 @@ let converter env (f : Ground.t) =
let a, b = IArray.extract2_exn args in
Egraph.register env a;
Egraph.register env b;
- Array_Id_dom.set_id env a;
- Array_Id_dom.set_id env b;
+ Id.Array.set_id env a;
+ Id.Array.set_id env b;
add_array_gty env a ind_gty val_gty;
add_array_gty env b ind_gty val_gty
| {
@@ -212,7 +203,7 @@ let converter env (f : Ground.t) =
let f_arity = IArray.length args - 1 in
IArray.iteri args ~f:(fun i n ->
if i > 0 then (
- Array_Id_dom.set_id env n;
+ Id.Array.set_id env n;
add_array_gty env n bi_ind_ty bi_val_ty;
Array_dom.add_map_parent env n f
{ bi_ind_ty; bi_val_ty; a_val_ty; f_arity })));
@@ -224,10 +215,10 @@ let init env =
Array_value.init_check env;
Ground.register_converter env converter;
if Options.get env use_wegraph then (
- Array_Id_dom.register_new_id_hook env WEGraph.new_id_hook;
- Array_Id_dom.register_merge_hook env WEGraph.eq_arrays_norm;
- Index_Id_dom.register_new_id_hook env WEGraph.new_index_id_hook;
- Index_Id_dom.register_merge_hook env WEGraph.eq_indices_norm;
+ Id.Array.register_new_id_hook env WEGraph.new_id_hook;
+ Id.Array.register_merge_hook env WEGraph.eq_arrays_norm;
+ Id.Index.register_new_id_hook env WEGraph.new_index_id_hook;
+ Id.Index.register_merge_hook env WEGraph.eq_indices_norm;
Equality.register_hook_new_disequality env WEGraph.ineq_indices_norm);
(* extáµ£ (restricted extensionality):
- (a = b) ≡ false |> (a[k] ≠b[k])
diff --git a/colibri2/theories/array/array_value.ml b/colibri2/theories/array/array_value.ml
index e07bdba48..d7d78a521 100644
--- a/colibri2/theories/array/array_value.ml
+++ b/colibri2/theories/array/array_value.ml
@@ -27,8 +27,8 @@ open Colibri2_theories_quantifiers
module ArrayModelVal = struct
type aval = {
- ind_ty : Ground.Ty.t;
- val_ty : Ground.Ty.t;
+ ind_gty : Ground.Ty.t;
+ val_gty : Ground.Ty.t;
vals : Value.t Value.M.t;
other : Value.t;
}
@@ -36,20 +36,20 @@ module ArrayModelVal = struct
include Value.Register (struct
module T = struct
type t = aval = {
- ind_ty : Ground.Ty.t;
- val_ty : Ground.Ty.t;
+ ind_gty : Ground.Ty.t;
+ val_gty : Ground.Ty.t;
vals : Value.t Value.M.t;
other : Value.t;
}
[@@deriving eq, ord, hash]
- let pp fmt { ind_ty; val_ty; other; vals } =
+ let pp fmt { ind_gty; val_gty; other; vals } =
if false then
- Format.fprintf fmt "Array(%a => %a)" Ground.Ty.pp ind_ty Ground.Ty.pp
- val_ty
+ Format.fprintf fmt "Array(%a => %a)" Ground.Ty.pp ind_gty Ground.Ty.pp
+ val_gty
else
- Format.fprintf fmt "Array(%a => %a: %a: %a)" Ground.Ty.pp ind_ty
- Ground.Ty.pp val_ty Value.pp other (Value.M.pp Value.pp) vals
+ Format.fprintf fmt "Array(%a => %a: %a: %a)" Ground.Ty.pp ind_gty
+ Ground.Ty.pp val_gty Value.pp other (Value.M.pp Value.pp) vals
end
include T
@@ -68,14 +68,14 @@ module ArrayModelVal = struct
let of_value v = nodevalue (index v)
end
-let add_to_seq seq d ind_ty val_ty =
+let add_to_seq seq d ind_gty val_gty =
let open Interp.SeqLim in
let+ vals = seq
- and* indv = Interp.ty d ind_ty
- and* valv = Interp.ty d val_ty in
+ and* indv = Interp.ty d ind_gty
+ and* valv = Interp.ty d val_gty in
Value.M.add indv valv vals
-let all_arrays d ind_ty val_ty =
+let all_arrays d ind_gty val_gty =
let size =
Interp.SeqLim.of_seq d
(Base.Sequence.unfold ~init:() ~f:(fun () -> Some ((), ())))
@@ -84,36 +84,38 @@ let all_arrays d ind_ty val_ty =
Interp.SeqLim.unfold_with size
~init:(Interp.SeqLim.of_seq d (Base.Sequence.singleton Value.M.empty))
~f:(fun seq () ->
- let seq = add_to_seq seq d ind_ty val_ty in
+ let seq = add_to_seq seq d ind_gty val_gty in
Yield (seq, seq))
in
let vals_ = Interp.SeqLim.limit d (Interp.SeqLim.concat vals_) in
let open Interp.SeqLim in
- let+ vals = vals_ and* other = Interp.ty d val_ty in
- ArrayModelVal.nodevalue (ArrayModelVal.index { ind_ty; val_ty; vals; other })
+ let+ vals = vals_ and* other = Interp.ty d val_gty in
+ ArrayModelVal.nodevalue
+ (ArrayModelVal.index { ind_gty; val_gty; vals; other })
-let add_vals d n ind_ty val_ty k acc =
+let add_ind d n ind_gty val_gty k acc =
let open Interp.SeqLim in
let+ vals = acc
and* indv =
match Egraph.get_value d k with
- | None -> Interp.ty d ind_ty
- | Some v -> Interp.SeqLim.of_seq d (Base.Sequence.singleton v)
+ | None -> Interp.ty d ind_gty
+ | Some kv -> Interp.SeqLim.of_seq d (Base.Sequence.singleton kv)
and* valv =
- let nk = mk_select d n k ind_ty val_ty in
+ let nk = mk_select d n k ind_gty val_gty in
match Egraph.get_value d nk with
- | Some v -> Interp.SeqLim.of_seq d (Base.Sequence.singleton v)
- | None | (exception Egraph.NotRegistered) -> Interp.ty d val_ty
+ | Some nkv -> Interp.SeqLim.of_seq d (Base.Sequence.singleton nkv)
+ | None | (exception Egraph.NotRegistered) -> Interp.ty d val_gty
in
Value.M.add indv valv vals
let array_reads d reads n =
let open Interp.SeqLim in
- let ind_ty, val_ty = array_gty_args (get_node_ty d n) in
+ let ind_gty, val_gty = array_gty_args (get_node_ty d n) in
let init = Interp.SeqLim.of_seq d (Base.Sequence.singleton Value.M.empty) in
- let+ other = Interp.ty d val_ty
- and* vals = Node.S.fold (add_vals d n ind_ty val_ty) reads init in
- ArrayModelVal.nodevalue (ArrayModelVal.index { ind_ty; val_ty; vals; other })
+ let+ other = Interp.ty d val_gty
+ and* vals = Node.S.fold (add_ind d n ind_gty val_gty) reads init in
+ ArrayModelVal.nodevalue
+ (ArrayModelVal.index { ind_gty; val_gty; vals; other })
let init_ty d =
Interp.Register.node d (fun _ d n ->
@@ -122,8 +124,8 @@ let init_ty d =
| Some { reads; _ } -> Some (array_reads d reads n));
Interp.Register.ty d (fun d ty ->
match ty with
- | { app = { builtin = Expr.Array; _ }; args = [ ind_ty; val_ty ]; _ } ->
- Some (all_arrays d ind_ty val_ty)
+ | { app = { builtin = Expr.Array; _ }; args = [ ind_gty; val_gty ]; _ } ->
+ Some (all_arrays d ind_gty val_gty)
| _ -> None)
let interp env n = Opt.get_exn Impossible (Egraph.get_value env n)
diff --git a/colibri2/theories/array/common.ml b/colibri2/theories/array/common.ml
index 9674033a5..fd6775b79 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -60,13 +60,6 @@ let use_wegraph =
value & flag
& info [ "array-wegraph" ] ~doc:"Use the array's weak equivalency graph")
-let use_choice =
- Options.register ~pp:Fmt.bool "Array.choice"
- Cmdliner.Arg.(
- value & flag
- & info [ "array-choice" ]
- ~doc:"Use choice instead of propagating disjunctions")
-
let debug =
Debug.register_info_flag ~desc:"Debugging messages of the array theory"
"Array"
@@ -77,6 +70,9 @@ let convert ~subst env =
(* exceptions *)
exception Not_An_Array of Node.t
+exception Not_An_Array_gty of Ground.Ty.t
+exception Not_An_Array_ty of Expr.ty
+exception Type_Not_Set of Node.t
exception NoIdFound of string * Node.t
exception Not_a_neighbour of (Node.t * Node.t * Node.t)
exception Empty_neighbour_set of (Node.t * Node.t * Node.t)
@@ -124,17 +120,17 @@ let apply_cst = Expr.Term.apply_cst
let array_ty_args : Expr.ty -> Expr.ty * Expr.ty = function
| { ty_descr = TyApp ({ builtin = Expr.Array; _ }, [ ind_ty; val_ty ]); _ } ->
(ind_ty, val_ty)
- | ty -> failwith (Fmt.str "'%a' is not an array type!" Expr.Ty.print ty)
+ | ty -> raise (Not_An_Array_ty ty)
let array_gty_args : Ground.Ty.t -> Ground.Ty.t * Ground.Ty.t = function
| { app = { builtin = Expr.Array; _ }; args = [ ind_gty; val_gty ] } ->
(ind_gty, val_gty)
- | ty -> failwith (Fmt.str "'%a' is not an array ground type!" Ground.Ty.pp ty)
+ | ty -> raise (Not_An_Array_gty ty)
let get_node_ty env n =
match Ground.Ty.S.elements (Ground.tys env n) with
| h :: _ -> h
- | [] -> failwith (Fmt.str "The type of the node %a was not set" Node.pp n)
+ | [] -> raise (Type_Not_Set n)
let get_array_gty env n =
try
@@ -296,7 +292,8 @@ let mk_subst term_l ty_l =
let ground_apply env cstr tyl nl =
sem_to_node (Ground.apply env cstr tyl (IArray.of_list nl))
-let mk_or env a b = ground_apply env Expr.Term.Const.or_ [] [ a; b ]
+let mk_or env l = ground_apply env Expr.Term.Const.or_ [] l
+let mk_and env l = ground_apply env Expr.Term.Const.and_ [] l
let mk_distinct env l gty =
ground_apply env (Expr.Term.Const.distinct (List.length l)) [ gty ] l
@@ -402,6 +399,12 @@ end
let () =
Printexc.register_printer (function
| Not_An_Array n -> Some (Fmt.str "%a is not an array!" Node.pp n)
+ | Not_An_Array_gty gty ->
+ Some (Fmt.str "%a is not an array ground type!" Ground.Ty.pp gty)
+ | Not_An_Array_ty ty ->
+ Some (Fmt.str "%a is not an array type!" Expr.Ty.pp ty)
+ | Type_Not_Set n ->
+ Some (Fmt.str "the type of the node %a was not set!" Node.pp n)
| NoIdFound (s, n) ->
Some (Fmt.str "get_id(%s) of %a: No Id found!" s Node.pp n)
| Not_a_neighbour (kn, rn, k) ->
diff --git a/colibri2/theories/array/common.mli b/colibri2/theories/array/common.mli
index 9f95879a2..44bbc1767 100644
--- a/colibri2/theories/array/common.mli
+++ b/colibri2/theories/array/common.mli
@@ -25,11 +25,13 @@ val extended_comb : bool Options.t
val blast_rule : bool Options.t
val default_values : bool Options.t
val use_wegraph : bool Options.t
-val use_choice : bool Options.t
val debug : Debug.flag
val convert : subst:Ground.Subst.t -> 'a Egraph.t -> Expr.term -> Node.t
exception Not_An_Array of Node.t
+exception Not_An_Array_gty of Ground.Ty.t
+exception Not_An_Array_ty of Expr.ty
+exception Type_Not_Set of Node.t
exception NoIdFound of string * Node.t
exception Not_a_neighbour of (Node.t * Node.t * Node.t)
exception Empty_neighbour_set of (Node.t * Node.t * Node.t)
@@ -114,7 +116,8 @@ val ground_apply :
Node.t list ->
Node.t
-val mk_or : 'a Egraph.t -> Node.t -> Node.t -> Node.t
+val mk_or : 'a Egraph.t -> Node.t list -> Node.t
+val mk_and : 'a Egraph.t -> Node.t list -> Node.t
val mk_store :
'a Egraph.t ->
--
GitLab