From edb80c75da585e5eaf031b4e96ee240ddc4fdb7c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 16 Mar 2021 22:49:31 +0100
Subject: [PATCH] Fix adt model generation
---
src_colibri2/core/interp.ml | 52 +++++++++++++++----
src_colibri2/core/interp.mli | 7 ++-
src_colibri2/popop_lib/extmap.ml | 11 ++--
src_colibri2/popop_lib/extset.ml | 2 +-
src_colibri2/popop_lib/intmap.ml | 10 ++--
src_colibri2/solver/scheduler.ml | 1 +
src_colibri2/tests/solve/smt_adt/sat/dune.inc | 2 +
.../tests/solve/smt_adt/sat/enum.smt2 | 16 ++++++
.../tests/solve/smt_adt/unsat/dune.inc | 2 +
.../tests/solve/smt_adt/unsat/enum.smt2 | 17 ++++++
src_colibri2/theories/ADT/adt.ml | 6 ++-
src_colibri2/theories/ADT/adt_value.ml | 6 ++-
12 files changed, 109 insertions(+), 23 deletions(-)
create mode 100644 src_colibri2/tests/solve/smt_adt/sat/enum.smt2
create mode 100644 src_colibri2/tests/solve/smt_adt/unsat/enum.smt2
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index dde472fc3..4cff4487c 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -91,11 +91,11 @@ module Register = struct
let ty d f = Datastructure.Queue.push ty d f
end
-let get_registered (type a) exn db d x =
+let get_registered (type a) exn db call d x =
let exception Found of a in
match
Datastructure.Queue.iter
- ~f:(fun f -> Option.iter (f d x) ~f:(fun s -> raise (Found s)))
+ ~f:(fun f -> Option.iter (call f d x) ~f:(fun s -> raise (Found s)))
db d
with
| exception Found s -> s
@@ -104,17 +104,44 @@ let get_registered (type a) exn db d x =
exception CantInterpretTy of Ground.Ty.t
-let ty d ty = get_registered (fun ty -> raise (CantInterpretTy ty)) Data.ty d ty
+let ty d ty =
+ get_registered
+ (fun ty -> raise (CantInterpretTy ty))
+ Data.ty
+ (fun f d x -> f d x)
+ d ty
exception CantInterpretNode of Node.t
let node d n =
- get_registered (fun n -> raise (CantInterpretNode n)) Data.node d n
+ let parent = Node.H.create 5 in
+ let rec aux d n' =
+ if Node.H.mem parent n' then (
+ Debug.dprintf4 debug "Interp.node recursive value: %a starting at %a"
+ Node.pp n' Node.pp n;
+ Egraph.contradiction d)
+ else (
+ Node.H.replace parent n' ();
+ let r =
+ get_registered
+ (fun n -> raise (CantInterpretNode n))
+ Data.node
+ (fun f d x -> f aux d x)
+ d n
+ in
+ Node.H.remove parent n';
+ r)
+ in
+ aux d n
exception CantCheckGround of Ground.t
let check d n =
- get_registered (fun n -> raise (CantCheckGround n)) Data.check d n
+ get_registered
+ (fun n -> raise (CantCheckGround n))
+ Data.check
+ (fun f d x -> f d x)
+ d n
exception GroundTermWithoutValueAfterModelFixing of Ground.t
@@ -216,6 +243,7 @@ module Fix_model = struct
| Some _ -> aux nextnode
| None ->
Debug.dprintf2 debug "FixModel %a has no value" Node.pp n;
+ assert (Egraph.is_current_env d);
let seq =
let tys = Ground.tys d n in
try node d n
@@ -223,11 +251,15 @@ module Fix_model = struct
| CantInterpretNode _ when not (Ground.Ty.S.is_empty tys) ->
ty d (Ground.Ty.S.choose tys)
in
- Sequence.map seq ~f:(fun v d ->
- Egraph.set_env d Data.env (During { r with nextnode });
- Debug.dprintf4 debug "FixModel by setting %a to %a"
- Node.pp n Value.pp v;
- Egraph.set_value d n v))
+ let seq = Sequence.of_list (Sequence.to_list seq) in
+ let seq =
+ Sequence.map seq ~f:(fun v d ->
+ Egraph.set_env d Data.env (During { r with nextnode });
+ Debug.dprintf4 debug "FixModel by setting %a to %a"
+ Node.pp n Value.pp v;
+ Egraph.set_value d n v)
+ in
+ seq)
in
aux r.nextnode
end
diff --git a/src_colibri2/core/interp.mli b/src_colibri2/core/interp.mli
index fcd757cb0..7bf4fe34c 100644
--- a/src_colibri2/core/interp.mli
+++ b/src_colibri2/core/interp.mli
@@ -50,10 +50,13 @@ module Register : sig
val node :
Egraph.t ->
- (Egraph.t -> Nodes.Node.t -> Nodes.Value.t SeqLim.t option) ->
+ ((Egraph.t -> Nodes.Node.t -> Nodes.Value.t SeqLim.t) ->
+ Egraph.t ->
+ Nodes.Node.t ->
+ Nodes.Value.t SeqLim.t option) ->
unit
(** Register the computation of possible values for a node using the
- information on the domains *)
+ information on the domains. It could ask the computation of other nodes *)
val ty :
Egraph.t ->
diff --git a/src_colibri2/popop_lib/extmap.ml b/src_colibri2/popop_lib/extmap.ml
index 5c8d607b7..5dc9103c0 100644
--- a/src_colibri2/popop_lib/extmap.ml
+++ b/src_colibri2/popop_lib/extmap.ml
@@ -285,10 +285,13 @@ module Make(Ord: Map_intf.OrderedType) = struct
in equal_aux (cons_enum m1 End) (cons_enum m2 End)
- let pp pp fmt m =
- Pp.iter2 iter Pp.comma Pp.arrow
- Ord.pp pp
- fmt m
+ let pp pp =
+ if pp == Fmt.nop || pp == Pp.nothing then
+ Pp.iter2 iter Pp.comma Fmt.nop
+ Ord.pp Fmt.nop
+ else
+ Pp.iter2 iter Pp.comma Pp.arrow
+ Ord.pp pp
let rec cardinal = function
Empty -> 0
diff --git a/src_colibri2/popop_lib/extset.ml b/src_colibri2/popop_lib/extset.ml
index 5ddd688de..7fdc6569b 100644
--- a/src_colibri2/popop_lib/extset.ml
+++ b/src_colibri2/popop_lib/extset.ml
@@ -57,7 +57,7 @@ module MakeOfMap (M: Map_intf.MapUnit) = struct
let add_new e x s = M.add_new e x () s
let is_num_elt n m = M.is_num_elt n m
let of_list l = List.fold_left (fun acc a -> add a acc) empty l
- let pp = M.pp (fun _ () -> ())
+ let pp = M.pp Fmt.nop
end
module Make(Ord: Map_intf.OrderedType) = MakeOfMap(Extmap.Make(Ord))
diff --git a/src_colibri2/popop_lib/intmap.ml b/src_colibri2/popop_lib/intmap.ml
index c433b5f1b..d5c688349 100644
--- a/src_colibri2/popop_lib/intmap.ml
+++ b/src_colibri2/popop_lib/intmap.ml
@@ -1496,9 +1496,13 @@ module Make(K:Map_intf.TaggedEqualType) :
| Br (_,t1,t2) -> aux t1 && aux t2 in
aux m
- let pp pp fmt m =
- Pp.iter2 iter Pp.arrow Pp.colon
- K.pp pp fmt m
+ let pp pp =
+ if pp == Fmt.nop || pp == Pp.nothing then
+ Pp.iter2 iter Pp.comma Fmt.nop
+ K.pp Fmt.nop
+ else
+ Pp.iter2 iter Pp.comma Pp.arrow
+ K.pp pp
end
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index d418ba698..267e8528a 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -367,6 +367,7 @@ let run_one_step ~nodec t d =
| Some _ as s -> s
| None when nodec -> None
| None ->
+ Debug.dprintf0 debug "[Scheduler] FixModel";
Context.Ref.set t.solve_step FixModel;
Some d
end
diff --git a/src_colibri2/tests/solve/smt_adt/sat/dune.inc b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
index 65f852eec..3088caeac 100644
--- a/src_colibri2/tests/solve/smt_adt/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
@@ -1,4 +1,6 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
+(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:enum.smt2}))))
+(rule (alias runtest) (action (diff oracle enum.smt2.res)))
(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list0.smt2}))))
(rule (alias runtest) (action (diff oracle list0.smt2.res)))
(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list1.smt2}))))
diff --git a/src_colibri2/tests/solve/smt_adt/sat/enum.smt2 b/src_colibri2/tests/solve/smt_adt/sat/enum.smt2
new file mode 100644
index 000000000..d62e93769
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_adt/sat/enum.smt2
@@ -0,0 +1,16 @@
+;; produced by colibri.drv ;;
+(set-logic ALL)
+
+(declare-datatype enum (
+ ( A )
+ ( B )
+ ( C )))
+
+(declare-fun f (enum) Bool)
+(declare-fun x () enum)
+
+(assert (f A))
+(assert (f B))
+(assert (not (f x)))
+
+(check-sat)
diff --git a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
index 7774807ea..0290c1dce 100644
--- a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
@@ -1,4 +1,6 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
+(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:enum.smt2}))))
+(rule (alias runtest) (action (diff oracle enum.smt2.res)))
(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list0.smt2}))))
(rule (alias runtest) (action (diff oracle list0.smt2.res)))
(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list1.smt2}))))
diff --git a/src_colibri2/tests/solve/smt_adt/unsat/enum.smt2 b/src_colibri2/tests/solve/smt_adt/unsat/enum.smt2
new file mode 100644
index 000000000..edd5cfedd
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_adt/unsat/enum.smt2
@@ -0,0 +1,17 @@
+;; produced by colibri.drv ;;
+(set-logic ALL)
+
+(declare-datatype enum (
+ ( A )
+ ( B )
+ ( C )))
+
+(declare-fun f (enum) Bool)
+(declare-fun x () enum)
+
+(assert (f A))
+(assert (f B))
+(assert (f C))
+(assert (not (f x)))
+
+(check-sat)
diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml
index 626da1e95..b5dc6e7f4 100644
--- a/src_colibri2/theories/ADT/adt.ml
+++ b/src_colibri2/theories/ADT/adt.ml
@@ -6,7 +6,11 @@ module D = struct
type t =
| Unk of Case.S.t
| One of { case : Case.t; fields : Node.t Field.M.t }
- [@@deriving eq, show]
+ [@@deriving eq]
+
+ let pp fmt = function
+ | Unk s -> Fmt.pf fmt "{%a}" Case.S.pp s
+ | One c -> Fmt.pf fmt "%i(%a)" c.case (Field.M.pp Node.pp) c.fields
let key =
DomKind.create_key
diff --git a/src_colibri2/theories/ADT/adt_value.ml b/src_colibri2/theories/ADT/adt_value.ml
index 0dad23a60..5b7b6cfb1 100644
--- a/src_colibri2/theories/ADT/adt_value.ml
+++ b/src_colibri2/theories/ADT/adt_value.ml
@@ -13,7 +13,9 @@ module T' = struct
case : Case.t;
fields : Value.t Field.M.t;
}
- [@@deriving eq, ord, show, hash]
+ [@@deriving eq, ord, hash]
+
+ let pp fmt c = Fmt.pf fmt "%i(%a)" c.case (Field.M.pp Value.pp) c.fields
end
include T
@@ -87,7 +89,7 @@ let propagate_value d g =
Interp.TwoWatchLiteral.create d f g
let init_ty d =
- Interp.Register.ty d (fun _ ty ->
+ Interp.Register.ty d (fun d ty ->
match ty with
| { app = { builtin = Dolmen_std.Expr.Base; _ } as sym; args } -> (
match Ground.Ty.definition sym with
--
GitLab