From 3adeaaf6f33825bc59d5fc9b55809ee11432173c Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Thu, 5 Jan 2023 16:38:16 +0100
Subject: [PATCH] [NSeq] fix types of builtins
---
.../tests/solve/smt_array/errors/ite_2.txt | 13 -------
.../tests/solve/smt_array/errors/notes.txt | 3 +-
colibri2/tests/solve/smt_array/sat/dune.inc | 3 ++
.../{errors/ite_1.txt => sat/imp1.smt2} | 6 ---
colibri2/theories/array/common.ml | 5 ++-
colibri2/theories/nseq/nseq.ml | 38 +++++++++----------
6 files changed, 26 insertions(+), 42 deletions(-)
delete mode 100644 colibri2/tests/solve/smt_array/errors/ite_2.txt
rename colibri2/tests/solve/smt_array/{errors/ite_1.txt => sat/imp1.smt2} (70%)
diff --git a/colibri2/tests/solve/smt_array/errors/ite_2.txt b/colibri2/tests/solve/smt_array/errors/ite_2.txt
deleted file mode 100644
index b88968a72..000000000
--- a/colibri2/tests/solve/smt_array/errors/ite_2.txt
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic ALL)
-(declare-fun i () Int)
-(declare-fun a () (Array Int Int))
-(declare-fun j () Int)
-(declare-fun v1 () Int)
-(declare-fun v2 () Int)
-(assert (not
- (ite
- (= (store a j v1) (store (store a i v2) j v1))
- (= i j)
- true
- )))
-(check-sat)
\ No newline at end of file
diff --git a/colibri2/tests/solve/smt_array/errors/notes.txt b/colibri2/tests/solve/smt_array/errors/notes.txt
index 16453a420..339eeef09 100644
--- a/colibri2/tests/solve/smt_array/errors/notes.txt
+++ b/colibri2/tests/solve/smt_array/errors/notes.txt
@@ -1,4 +1,3 @@
- eq.txt: timeout
-- ite_1.txt: unsound (--array-res-ext)
-- ite_2.txt: timeout (--array-res-ext)
+
diff --git a/colibri2/tests/solve/smt_array/sat/dune.inc b/colibri2/tests/solve/smt_array/sat/dune.inc
index 8e94dfc7e..ffb6db07f 100644
--- a/colibri2/tests/solve/smt_array/sat/dune.inc
+++ b/colibri2/tests/solve/smt_array/sat/dune.inc
@@ -1,3 +1,6 @@
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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 --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 --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_array/errors/ite_1.txt b/colibri2/tests/solve/smt_array/sat/imp1.smt2
similarity index 70%
rename from colibri2/tests/solve/smt_array/errors/ite_1.txt
rename to colibri2/tests/solve/smt_array/sat/imp1.smt2
index fb808e901..a6c9d6fff 100644
--- a/colibri2/tests/solve/smt_array/errors/ite_1.txt
+++ b/colibri2/tests/solve/smt_array/sat/imp1.smt2
@@ -6,12 +6,6 @@
(declare-fun j () I)
(declare-fun v1 () E)
(declare-fun v2 () E)
-; (assert (not
-; (ite
-; (= (store a j v1) (store (store a i v2) j v1))
-; (= i j)
-; true
-; )))
(assert (= (store a j v1) (store (store a i v2) j v1)))
(assert (not (= i j)))
(check-sat)
diff --git a/colibri2/theories/array/common.ml b/colibri2/theories/array/common.ml
index 63dfe2c86..afaac70e9 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -175,8 +175,9 @@ module Builtin = struct
apply_cst array_diff [ ind_ty; val_ty ] [ a; b ]
let apply_array_const v =
- let wildcard = Expr.Ty.Var.wildcard () in
- apply_cst array_const [ Expr.Ty.of_var wildcard; v.Expr.term_ty ] [ v ]
+ apply_cst array_const
+ [ Expr.Ty.of_var (Expr.Ty.Var.wildcard ()); v.Expr.term_ty ]
+ [ v ]
let apply_array_def_index a =
let ind_ty, val_ty = array_ty_args a.Expr.term_ty in
diff --git a/colibri2/theories/nseq/nseq.ml b/colibri2/theories/nseq/nseq.ml
index 71dda86de..ef41aa585 100644
--- a/colibri2/theories/nseq/nseq.ml
+++ b/colibri2/theories/nseq/nseq.ml
@@ -114,7 +114,7 @@ module Builtin = struct
(Expr.Ty.pi [ val_ty_var ]
(Expr.Ty.arrow [ val_nseq_ty; int_ty; int_ty ] val_nseq_ty))
- let get_nseq_val : Expr.ty -> Expr.ty = function
+ let get_nseq_arg : Expr.ty -> Expr.ty = function
| { ty_descr = TyApp ({ builtin = NSeq; _ }, [ val_ty ]); _ } -> val_ty
| ty -> failwith (Fmt.str "'%a' is not an nseq type!" Expr.Ty.print ty)
@@ -126,57 +126,57 @@ module Builtin = struct
env s
(fun ty -> Expr.Ty.apply f [ ty ]))
in
- let app1 env s f =
+ let app1 ?(get_nseq_arg = Fun.id) env s f =
`Term
(Dolmen_type.Base.term_app1
(module Dolmen_loop.Typer.T)
env s
(fun a ->
- Expr.Term.apply_cst f [ get_nseq_val a.Expr.term_ty ] [ a ]))
+ Expr.Term.apply_cst f [ get_nseq_arg a.Expr.term_ty ] [ a ]))
in
- let app2 env s f =
+ let app2 ?(get_nseq_arg = Fun.id) env s f =
`Term
(Dolmen_type.Base.term_app2
(module Dolmen_loop.Typer.T)
env s
(fun a b ->
- Expr.Term.apply_cst f [ get_nseq_val a.Expr.term_ty ] [ a; b ]))
+ Expr.Term.apply_cst f [ get_nseq_arg a.Expr.term_ty ] [ a; b ]))
in
- let app3 env s f =
+ let app3 env ?(get_nseq_arg = Fun.id) s f =
`Term
(Dolmen_type.Base.term_app2
(module Dolmen_loop.Typer.T)
env s
(fun a b ->
- Expr.Term.apply_cst f [ get_nseq_val a.Expr.term_ty ] [ a; b ]))
+ Expr.Term.apply_cst f [ get_nseq_arg a.Expr.term_ty ] [ a; b ]))
in
Expr.add_builtins (fun env s ->
match s with
| Dolmen_loop.Typer.T.Id { ns = Sort; name = Simple "NSeq" } ->
ty_app1 env s nseq_ty_const
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_get" } ->
+ app2 ~get_nseq_arg env s nseq_get
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_set" } ->
+ app3 ~get_nseq_arg env s nseq_set
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_first" } ->
- app1 env s nseq_first
+ app1 ~get_nseq_arg env s nseq_first
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_last" } ->
- app1 env s nseq_last
+ app1 ~get_nseq_arg env s nseq_last
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_content" } ->
- app1 env s nseq_content
+ app1 ~get_nseq_arg env s nseq_content
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_length" } ->
- app1 env s nseq_length
- | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_get" } ->
- app2 env s nseq_get
- | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_set" } ->
- app3 env s nseq_set
+ app1 ~get_nseq_arg env s nseq_length
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_eq" } ->
- app2 env s nseq_get
+ app2 ~get_nseq_arg env s nseq_get
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_const" } ->
app3 env s nseq_const
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_empty" } ->
app2 env s nseq_empty
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_concat" } ->
- app2 env s nseq_concat
+ app2 ~get_nseq_arg env s nseq_concat
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_relocate" } ->
- app2 env s nseq_relocate
+ app2 ~get_nseq_arg env s nseq_relocate
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_slice" } ->
- app3 env s nseq_slice
+ app3 ~get_nseq_arg env s nseq_slice
| _ -> `Not_found)
end
--
GitLab