diff --git a/Makefile b/Makefile
index 79d97d703bfe3847ee0bec5509a47df8df198d8f..8b9998196e290110334e7541df5b729f85353b43 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 ecb413746853c06ccbf7eb4eb09fc7a86331085d..b4abf839cd472266de95a12b1eeaf72b41ae2d42 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 3f1eb2fb9a4cad227de86d965f222f58551a7beb..6da604e16bcea7f67d1bd2044c8b731bf9fff65e 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 d418f0cb1d573254495f50155f3cc803142c65a0..465415d92dd0a3f17e85059d00dc2533993cd7f3 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 6adbd53951cad76c09afdcdeafc6e32e933f571a..0de9e991b57afd3a60031439f6ee5f9110e669c5 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 0000000000000000000000000000000000000000..87aec8cee7b54a9b5770453bb688a103592210ab
--- /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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/colibri2/tests/solve/smt_array/unsat/dune b/colibri2/tests/solve/smt_array/unsat/dune
new file mode 100644
index 0000000000000000000000000000000000000000..959922d115ac3b89aec38904a6221b2730b37e08
--- /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 0000000000000000000000000000000000000000..cd3b42412b46b7b632c7bb695e0a8af65abbdbe8
--- /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 0000000000000000000000000000000000000000..487a5e172b771b358bb6b62c66dda8ea60ed5b72
--- /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 0000000000000000000000000000000000000000..c7ae8b996c6f323887f494d058d2b771a95aab03
--- /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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
new file mode 100644
index 0000000000000000000000000000000000000000..49add0aa51db3a87d2c6d7890f8c96830729377f
--- /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 0000000000000000000000000000000000000000..b04ecb6fcc41c5e1ba8299fc85197c5da227df74
--- /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 0000000000000000000000000000000000000000..92812414603f5a422d2e1d63da90d67ec630fb08
--- /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 4b24893dd5005146b5422b1310e04b33d1119275..425b852b237bd0c29a1c70a84e3d44d432b0855a 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 c2948a6a6326459a5285f8f6accf9d29a4921b65..7f94552598c2a1d181a327498a440f9c2741a3c1 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 b0d9c6db572e9e4e29630512f78c215f1d192de5..616184a9c8a111b1fec90801dc7b7a46dc3a8fbe 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 0000000000000000000000000000000000000000..5032c60951473887aac9a067c94e46cfb038d0b0
--- /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).