diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index dde472fc3d78ae22b67795a1dbc33a09b70cba32..4cff4487c10d6d9137b3f2bcc7e1643b9241f266 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 fcd757cb0dbf2597193a1056a43887574872bf0a..7bf4fe34c8d8810fe93844e17081208b7ee3ef59 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 5c8d607b78e8880f16c041fb17a7fb518f41c369..5dc9103c079ef04ecc5d017e19dca1a654684d75 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 5ddd688de84090f9f092db80f217071b41229daf..7fdc6569b1ecba1253a54760cf7b0f6a48ca1ead 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 c433b5f1be9b1245670db17c7f77f5826a5d739c..d5c688349b080767b028263d718a9737f84902fe 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 d418ba6989fd067da354adc1c0ba427a492340e8..267e8528a90a388c93a68f0a2a2fd5edcdaa9148 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 65f852eecd69290d2802e5115f38d0513617e209..3088caeac4bf5fef84dba86b6aa2150003519920 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 0000000000000000000000000000000000000000..d62e937692d1aaf5a1adc7151ef0a735c51f4869
--- /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 7774807ea9517923c206671f09362adef1b10801..0290c1dced81dc7ba8bb9dfd88bd20aabf244e28 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 0000000000000000000000000000000000000000..edd5cfedd2cc7484b4ebbbb8388b0ada8030284a
--- /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 626da1e95ad39a901cecf26569a0092f5bef4938..b5dc6e7f4580ab0fee75127125cace3e77834237 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 0dad23a60ab11ff26ca508b3afaef038c930700f..5b7b6cfb12a88496fb0dd47aea3b62443b948183 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