From 0c66cfe6ba19fbb4a1263f81b59a46b1b2124133 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 22 Sep 2022 14:40:00 +0200
Subject: [PATCH] [Array] Start the theory
---
Makefile | 19 ++++--
colibri2/bin/dune | 3 +-
colibri2/core/ground.ml | 2 +-
colibri2/core/options.ml | 20 ++++++
colibri2/solver/scheduler.ml | 2 +-
colibri2/tests/solve/smt_array/sat/dune | 12 ++++
colibri2/tests/solve/smt_array/sat/dune.inc | 0
colibri2/tests/solve/smt_array/unsat/dune | 12 ++++
colibri2/tests/solve/smt_array/unsat/dune.inc | 6 ++
.../tests/solve/smt_array/unsat/select.smt2 | 9 +++
.../tests/solve/smt_array/unsat/store.smt2 | 7 ++
colibri2/theories/array/.ocamlformat | 0
colibri2/theories/array/array.ml | 68 +++++++++++++++++++
colibri2/theories/array/array.mli | 21 ++++++
colibri2/theories/array/dune | 34 ++++++++++
colibri2/theories/quantifier/callback.ml | 20 ++++++
colibri2/theories/quantifier/callback.mli | 20 ++++++
.../quantifier/congruence_closure.mli | 1 +
misc/header_cea_ocamlpro.txt | 18 +++++
19 files changed, 264 insertions(+), 10 deletions(-)
create mode 100644 colibri2/tests/solve/smt_array/sat/dune
create mode 100644 colibri2/tests/solve/smt_array/sat/dune.inc
create mode 100644 colibri2/tests/solve/smt_array/unsat/dune
create mode 100644 colibri2/tests/solve/smt_array/unsat/dune.inc
create mode 100644 colibri2/tests/solve/smt_array/unsat/select.smt2
create mode 100644 colibri2/tests/solve/smt_array/unsat/store.smt2
create mode 100644 colibri2/theories/array/.ocamlformat
create mode 100644 colibri2/theories/array/array.ml
create mode 100644 colibri2/theories/array/array.mli
create mode 100644 colibri2/theories/array/dune
create mode 100644 misc/header_cea_ocamlpro.txt
diff --git a/Makefile b/Makefile
index 79d97d703..8b9998196 100644
--- a/Makefile
+++ b/Makefile
@@ -82,12 +82,12 @@ uninstall:
###############
WHY3_FILES = $(addprefix colibri2/popop_lib/, cmdline.ml cmdline.mli \
- debug.ml debug.mli exn_printer.ml exn_printer.mli hashcons.ml \
- hashcons.mli lists.ml lists.mli loc.ml loc.mli number.ml number.mli \
+ exn_printer.ml exn_printer.mli hashcons.ml \
+ hashcons.mli lists.ml lists.mli number.ml number.mli \
opt.ml opt.mli pp.ml pp.mli print_tree.ml print_tree.mli \
popop_stdlib.ml popop_stdlib.mli strings.ml strings.mli sysutil.ml \
- sysutil.mli util.ml util.mli warning.ml warning.mli weakhtbl.ml \
- weakhtbl.mli )
+ sysutil.mli util.ml util.mli weakhtbl.ml \
+ weakhtbl.mli ) $(addprefix colibri2/stdlib/, debug.ml debug.mli)
OCAML_FILES = $(addprefix colibri2/popop_lib/, map_intf.ml exthtbl.ml \
exthtbl.mli extmap.ml extmap.mli extset.ml extset.mli )
@@ -106,9 +106,12 @@ WITAN_FILES = colibri2/stdlib/std.ml colibri2/stdlib/std.mli \
colibri2/stdlib/keys_sig.ml colibri2/stdlib/comp_keys.ml \
colibri2/stdlib/comp_keys.mli colibri2/bin/options.ml
-COLIBRI2_FILES = Makefile \
- $(filter-out $(WHY3_FILES) $(OCAML_FILES) $(FRAMAC_FILES) $(JC_FILES) $(WITAN_FILES) \
- , $(wildcard colibri2/*/*/*.ml* colibri2/*/*.ml* colibri2/*.ml*))
+OCAMLPRO_FILES = $(filter-out colibri2/theories/array/dune, $(wildcard colibri2/theories/array/*))
+
+
+COLIBRI2_FILES = Makefile $(filter-out $(WHY3_FILES) $(OCAML_FILES) \
+ $(FRAMAC_FILES) $(JC_FILES) $(WITAN_FILES) $(OCAMLPRO_FILES) , \
+ $(wildcard colibri2/*/*/*.ml* colibri2/*/*.ml* colibri2/*.ml*))
COLIBRICS_FILES =
@@ -124,6 +127,8 @@ headers:
$(WHY3_FILES)
headache -c misc/headache_config.txt -h misc/header_ocaml.txt \
$(OCAML_FILES)
+ headache -c misc/headache_config.txt -h misc/header_cea_ocamlpro.txt \
+ $(OCAMLPRO_FILES)
headache -c misc/headache_config.txt -h \
misc/header_framac.txt $(FRAMAC_FILES)
headache -c misc/headache_config.txt -h \
diff --git a/colibri2/bin/dune b/colibri2/bin/dune
index ecb413746..b4abf839c 100644
--- a/colibri2/bin/dune
+++ b/colibri2/bin/dune
@@ -21,7 +21,8 @@
colibri2.theories.LRA
colibri2.theories.quantifiers
colibri2.theories.fp
- colibri2.theories.adt)
+ colibri2.theories.adt
+ colibri2.theories.array)
(modules main options))
; Colibri2 stage0
diff --git a/colibri2/core/ground.ml b/colibri2/core/ground.ml
index 3f1eb2fb9..6da604e16 100644
--- a/colibri2/core/ground.ml
+++ b/colibri2/core/ground.ml
@@ -1,4 +1,4 @@
-(************************************************************************)
+(*************************************************************************)
(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2014-2021 *)
diff --git a/colibri2/core/options.ml b/colibri2/core/options.ml
index d418f0cb1..465415d92 100644
--- a/colibri2/core/options.ml
+++ b/colibri2/core/options.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* 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). *)
+(*************************************************************************)
+
module K = Keys.Make_key ()
module Data = struct
diff --git a/colibri2/solver/scheduler.ml b/colibri2/solver/scheduler.ml
index 6adbd5395..0de9e991b 100644
--- a/colibri2/solver/scheduler.ml
+++ b/colibri2/solver/scheduler.ml
@@ -1,4 +1,4 @@
-(************************************************************************)
+(*************************************************************************)
(* This file is part of Colibri2. *)
(* *)
(* Copyright (C) 2014-2021 *)
diff --git a/colibri2/tests/solve/smt_array/sat/dune b/colibri2/tests/solve/smt_array/sat/dune
new file mode 100644
index 000000000..87aec8cee
--- /dev/null
+++ b/colibri2/tests/solve/smt_array/sat/dune
@@ -0,0 +1,12 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+ (glob_files *.cnf)
+ (glob_files *.smt2))
+ (action
+ (with-stdout-to
+ dune.inc
+ (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
+ (mode promote))
diff --git a/colibri2/tests/solve/smt_array/sat/dune.inc b/colibri2/tests/solve/smt_array/sat/dune.inc
new file mode 100644
index 000000000..e69de29bb
diff --git a/colibri2/tests/solve/smt_array/unsat/dune b/colibri2/tests/solve/smt_array/unsat/dune
new file mode 100644
index 000000000..959922d11
--- /dev/null
+++ b/colibri2/tests/solve/smt_array/unsat/dune
@@ -0,0 +1,12 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+ (glob_files *.cnf)
+ (glob_files *.smt2))
+ (action
+ (with-stdout-to
+ dune.inc
+ (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote))
diff --git a/colibri2/tests/solve/smt_array/unsat/dune.inc b/colibri2/tests/solve/smt_array/unsat/dune.inc
new file mode 100644
index 000000000..cd3b42412
--- /dev/null
+++ b/colibri2/tests/solve/smt_array/unsat/dune.inc
@@ -0,0 +1,6 @@
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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 --check-status unsat
+--dont-print-result %{dep:store.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:store.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_array/unsat/select.smt2 b/colibri2/tests/solve/smt_array/unsat/select.smt2
new file mode 100644
index 000000000..487a5e172
--- /dev/null
+++ b/colibri2/tests/solve/smt_array/unsat/select.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL)
+
+(declare-fun a () (Array Int Int))
+
+(assert (= (select a 1) 1))
+
+(assert (= (select a 1) 2))
+
+(check-sat)
diff --git a/colibri2/tests/solve/smt_array/unsat/store.smt2 b/colibri2/tests/solve/smt_array/unsat/store.smt2
new file mode 100644
index 000000000..c7ae8b996
--- /dev/null
+++ b/colibri2/tests/solve/smt_array/unsat/store.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+
+(declare-fun a () (Array Int Int))
+
+(assert (= (select (store a 1 2) 1) 1))
+
+(check-sat)
diff --git a/colibri2/theories/array/.ocamlformat b/colibri2/theories/array/.ocamlformat
new file mode 100644
index 000000000..e69de29bb
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
new file mode 100644
index 000000000..49add0aa5
--- /dev/null
+++ b/colibri2/theories/array/array.ml
@@ -0,0 +1,68 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
+open Colibri2_core
+open Colibri2_popop_lib
+
+let converter env (f : Ground.t) =
+ let _r = Ground.node f in
+ match Ground.sem f with
+ | { app = { builtin = Expr.Select; _ }; args; tyargs = _; _ } ->
+ let a, k = IArray.extract2_exn args in
+ Egraph.register env a;
+ Egraph.register env k
+ | { app = { builtin = Expr.Store; _ }; args; tyargs = _; _ } ->
+ let a, k, v = IArray.extract3_exn args in
+ Egraph.register env a;
+ Egraph.register env k;
+ Egraph.register env v
+ | _ -> ()
+
+let debug = Debug.register_info_flag ~desc:"For array theory" "Array"
+
+module Select_store = struct
+ let a = Expr.Term.Var.mk "a" (Expr.Ty.array Expr.Ty.int Expr.Ty.int)
+ let k = Expr.Term.Var.mk "k" Expr.Ty.int
+ let v = Expr.Term.Var.mk "v" Expr.Ty.int
+ let ta = Expr.Term.of_var a
+ let tk = Expr.Term.of_var k
+ let tv = Expr.Term.of_var v
+ let t = Expr.Term.select (Expr.Term.store ta tk tv) tk
+
+ let pattern =
+ Colibri2_theories_quantifiers.Pattern.of_term_exn ~subst:Ground.Subst.empty
+ t
+
+ let run env subst =
+ Debug.dprintf2 debug "Found select store with %a" Ground.Subst.pp subst;
+ let n = Ground.convert ~subst env t in
+ let v = Expr.Term.Var.M.find_exn Impossible v subst.term in
+ Egraph.merge env n v
+
+ let init env =
+ Colibri2_theories_quantifiers.InvertedPath.add_callback env pattern run
+end
+
+let init env : unit =
+ Ground.register_converter env converter;
+ Select_store.init env
+
+let () = Init.add_default_theory init
diff --git a/colibri2/theories/array/array.mli b/colibri2/theories/array/array.mli
new file mode 100644
index 000000000..b04ecb6fc
--- /dev/null
+++ b/colibri2/theories/array/array.mli
@@ -0,0 +1,21 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
diff --git a/colibri2/theories/array/dune b/colibri2/theories/array/dune
new file mode 100644
index 000000000..928124146
--- /dev/null
+++ b/colibri2/theories/array/dune
@@ -0,0 +1,34 @@
+(library
+ (name colibri2_theories_array)
+ (public_name colibri2.theories.array)
+ (synopsis "theory array for colibri2")
+ (libraries
+ containers
+ ocamlgraph
+ colibri2.stdlib
+ colibri2.popop_lib
+ colibri2.core
+ colibri2.theories.quantifiers)
+ (preprocess
+ (pps ppx_deriving.std ppx_hash))
+ (flags
+ :standard
+ -w
+ +a-4-42-44-48-50-58-32-60-40-9@8
+ -color
+ always
+ -open
+ Colibri2_stdlib
+ -open
+ Std
+ -open
+ Colibri2_core
+ -open
+ Colibri2_theories_bool)
+ (ocamlopt_flags
+ :standard
+ -O3
+ -bin-annot
+ -unbox-closures
+ -unbox-closures-factor
+ 20))
diff --git a/colibri2/theories/quantifier/callback.ml b/colibri2/theories/quantifier/callback.ml
index 4b24893dd..425b852b2 100644
--- a/colibri2/theories/quantifier/callback.ml
+++ b/colibri2/theories/quantifier/callback.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* 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). *)
+(*************************************************************************)
+
open Common
open Colibri2_popop_lib
diff --git a/colibri2/theories/quantifier/callback.mli b/colibri2/theories/quantifier/callback.mli
index c2948a6a6..7f9455259 100644
--- a/colibri2/theories/quantifier/callback.mli
+++ b/colibri2/theories/quantifier/callback.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* 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 Colibri2_popop_lib.Popop_stdlib.Datatype
val pattern : t -> Pattern.t
diff --git a/colibri2/theories/quantifier/congruence_closure.mli b/colibri2/theories/quantifier/congruence_closure.mli
index b0d9c6db5..616184a9c 100644
--- a/colibri2/theories/quantifier/congruence_closure.mli
+++ b/colibri2/theories/quantifier/congruence_closure.mli
@@ -17,3 +17,4 @@
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
+
diff --git a/misc/header_cea_ocamlpro.txt b/misc/header_cea_ocamlpro.txt
new file mode 100644
index 000000000..5032c6095
--- /dev/null
+++ b/misc/header_cea_ocamlpro.txt
@@ -0,0 +1,18 @@
+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).
--
GitLab