diff --git a/src_colibri2/core/datastructure.ml b/src_colibri2/core/datastructure.ml
index 9731f24949d9b2484c79d871bd35a2f508b261e9..ae03ab0d6d061327768b3a0713f2e3b0f9fc300c 100644
--- a/src_colibri2/core/datastructure.ml
+++ b/src_colibri2/core/datastructure.ml
@@ -167,26 +167,26 @@ module Hashtbl2(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig2 with type key
end
-module type Sig3 = sig
+module type Memo = sig
type 'a t
type key
- val create: 'a Format.printer -> string -> (Context.creator -> 'a) -> 'a t
+ val create: 'a Format.printer -> string -> (Context.creator -> key -> 'a) -> 'a t
val find : 'a t -> Egraph.t -> key -> 'a
val iter : (key -> 'a -> unit) -> 'a t -> Egraph.t -> unit
val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> Egraph.t -> 'acc -> 'acc
end
-module Memo(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig3 with type key := S.t = struct
+module Memo(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo with type key := S.t = struct
type 'a t' = {
h: 'a S.H.t;
- def: (Context.creator -> 'a);
+ def: (Context.creator -> S.t -> 'a);
}
type 'a t = 'a t' Env.Unsaved.t
- let create : type a. a Colibri2_popop_lib.Pp.pp -> _ -> (Context.creator -> a) -> a t = fun pp name def ->
+ let create : type a. a Colibri2_popop_lib.Pp.pp -> _ -> (Context.creator -> S.t -> a) -> a t = fun pp name def ->
let module M = struct
type t = a t'
let name = name end
@@ -203,7 +203,7 @@ module Memo(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig3 with type key :=
match S.H.find_opt h.h k with
| Some r -> r
| None ->
- let r = h.def (Egraph.context d) in
+ let r = h.def (Egraph.context d) k in
S.H.add h.h k r;
r
diff --git a/src_colibri2/core/datastructure.mli b/src_colibri2/core/datastructure.mli
index be6adf80359792f91b3ea7cdac2e44cf6e8229d0..07a79d56793e03f5f31097f500dda4baca301145 100644
--- a/src_colibri2/core/datastructure.mli
+++ b/src_colibri2/core/datastructure.mli
@@ -18,6 +18,8 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
+(** {2 An hashtable context aware } *)
+
module type Sig = sig
type 'a t
type key
@@ -39,6 +41,8 @@ end
module Hashtbl (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key := S.t
+(** {2 An hashtable context aware, where data are automatically initialized } *)
+
module type Sig2 = sig
type 'a t
type key
@@ -52,17 +56,20 @@ end
module Hashtbl2 (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig2 with type key := S.t
-module type Sig3 = sig
+(** {2 A table where data are initialized on the fly, and can't be modified. It
+ is used with other context aware mutable data-structure as data } *)
+
+module type Memo = sig
type 'a t
type key
- val create: 'a Format.printer -> string -> (Context.creator -> 'a) -> 'a t
+ val create: 'a Format.printer -> string -> (Context.creator -> key -> 'a) -> 'a t
val find : 'a t -> Egraph.t -> key -> 'a
val iter : (key -> 'a -> unit) -> 'a t -> Egraph.t -> unit
val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> Egraph.t -> 'acc -> 'acc
end
-module Memo (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig3 with type key := S.t
+module Memo (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo with type key := S.t
module HNode : Sig with type key := Nodes.Node.t
diff --git a/src_colibri2/core/demon.ml b/src_colibri2/core/demon.ml
index b2358dda69df4fda35d9d38af2338a36251b8730..11bd1dacdd668af2d78044b339b374b82eccb0a2 100644
--- a/src_colibri2/core/demon.ml
+++ b/src_colibri2/core/demon.ml
@@ -705,6 +705,7 @@ module Fast = struct
type waiter = {
for_dom: 'a. Egraph.t -> 'a DomKind.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit;
for_value: 'a. Egraph.t -> 'a ValueKind.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit;
+ for_any_value: 'a. Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit;
}
let register_simply
@@ -740,6 +741,12 @@ module Fast = struct
| None -> ()
| Some _ -> f d n
in
- RDaemonInit.init, {for_dom; for_value}
+ let for_any_value d n f =
+ attach d DaemonInit.key [Create.EventAnyValue(n,f)];
+ match Egraph.get_value d n with
+ | None -> ()
+ | Some _ -> f d n
+ in
+ RDaemonInit.init, {for_dom; for_value; for_any_value}
end
diff --git a/src_colibri2/core/demon.mli b/src_colibri2/core/demon.mli
index 7c4dbde8bb070c994cf649f0ec07a30ff21405e1..d44791dd1b499c5bee5c3aba399abad6abff323e 100644
--- a/src_colibri2/core/demon.mli
+++ b/src_colibri2/core/demon.mli
@@ -208,6 +208,7 @@ module Fast: sig
type waiter = {
for_dom: 'a. Egraph.t -> 'a DomKind.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit;
for_value: 'a. Egraph.t -> 'a ValueKind.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit;
+ for_any_value: 'a. Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit;
}
(** helper *)
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index 505ac731444db8951288d19285e1b94fe5fd8f5f..4f12899b8b09135617048e381fb45d7550752db2 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -718,7 +718,7 @@ module Delayed = struct
in
VDomTable.iter_initializedi {VDomTable.iteri} t.env.dom;
- (** move value events *)
+ (** move value events by valuekind *)
let mapi _ events =
match Node.M.find_opt other_node events with
| None -> events
@@ -729,6 +729,19 @@ module Delayed = struct
t.env.value <- { t.env.value with events =
ValueKind.M.mapi {mapi} t.env.value.events
};
+ begin
+ let event, other_event = Node.M.find_remove other_node t.env.event_value in
+
+ (** move value events *)
+ begin match other_event with
+ | None -> ()
+ | Some other_event ->
+ t.env.event_value <-
+ Node.M.add_change (fun x -> x) Bag.concat repr_node other_event
+ event
+ end;
+ end;
+
(** wakeup the daemons *)
Wait.wakeup_events_bag
diff --git a/src_colibri2/core/events.mli b/src_colibri2/core/events.mli
index 5bd66017a7339dcc92240665fe65ff15f6a78aee..df4af5f05529b9d70502abb90b9c665a1cad9c6e 100644
--- a/src_colibri2/core/events.mli
+++ b/src_colibri2/core/events.mli
@@ -92,6 +92,9 @@ module Wait : sig
type runable
val print_runable : runable Format.printer
val run : delayed -> runable -> runable option
+ (** The function run after the delay,
+ a new run can be scheduled using the result *)
+
type event
val print_event : event Format.printer
val enqueue : delayed_ro -> event Fired.event -> runable enqueue
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index 74aced0be13fce86277ca86449180c8bcecbb9ba..8183c53b1322c5eff080707616781ce534674f3f 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -9,7 +9,10 @@ module All = struct
[@@deriving eq, ord, hash]
let rec pp_ty fmt ty =
- Fmt.pf fmt "%a%a" Expr.Ty.Const.pp ty.app Fmt.(list ~sep:comma pp_ty) ty.args
+ match ty.args with
+ | [] -> Fmt.pf fmt "%a" Expr.Ty.Const.pp ty.app
+ | _ ->
+ Fmt.pf fmt "%a(%a)" Expr.Ty.Const.pp ty.app Fmt.(list ~sep:comma pp_ty) ty.args
type term = {
app: Expr.Term.Const.t;
@@ -74,6 +77,10 @@ module Ty = struct
let real = convert Expr.Ty.Var.M.empty Expr.Ty.real
let string = convert Expr.Ty.Var.M.empty Expr.Ty.string
let string_reg_lang = convert Expr.Ty.Var.M.empty Expr.Ty.string_reg_lang
+ let definition sym =
+ match Expr.Ty.definition sym with
+ | None -> Expr.Ty.Abstract
+ | Some x -> x
end
module Term = struct
@@ -222,12 +229,46 @@ let registered_converter = Datastructure.Queue.create Fmt.nop "Ground.converters
let register_converter d f =
Datastructure.Queue.push registered_converter d f
+let dom_tys =
+ DomKind.create_key
+ (module struct
+ type nonrec t = Ty.S.t
+
+ let name = "Ground.tys"
+ end)
+
+let () = Egraph.register_dom (module struct
+ include Ty.S
+ let key = dom_tys
+ let merged tys0 tys1 =
+ Option.equal equal tys0 tys1
+
+ let merge d (tys0,n0) (tys1,n1) _ =
+ let s = (Ty.S.union
+ (Base.Option.value ~default:Ty.S.empty tys0)
+ (Base.Option.value ~default:Ty.S.empty tys1)
+ ) in
+ Egraph.set_dom d key n0 s;
+ Egraph.set_dom d key n1 s
+ end)
+
+let tys d n = (Base.Option.value ~default:Ty.S.empty (Egraph.get_dom d dom_tys n))
+
let init d =
Demon.Fast.register_init_daemon ~name:"Ground.convert"
(module ThTerm)
- (fun d s ->
- Defs.converter d s;
- Datastructure.Queue.iter registered_converter d ~f:(fun f -> f d s))
+ (fun d g ->
+ let n = ThTerm.node g in
+ let s = ThTerm.sem g in
+ (match Egraph.get_dom d dom_tys n with
+ | None -> Egraph.set_dom d dom_tys n (Ty.S.singleton s.ty)
+ | Some tys ->
+ match Ty.S.add_new Exit s.ty tys with
+ | exception Exit -> ()
+ | tys -> Egraph.set_dom d dom_tys n tys
+ );
+ Defs.converter d g;
+ Datastructure.Queue.iter registered_converter d ~f:(fun f -> f d g))
d
include ThTerm
diff --git a/src_colibri2/core/ground.mli b/src_colibri2/core/ground.mli
index 4f9d94f0d173736994d0803c6495f925a4558fa4..8321dac26b9c3a9418b23fefebb3fd229544e480 100644
--- a/src_colibri2/core/ground.mli
+++ b/src_colibri2/core/ground.mli
@@ -67,6 +67,7 @@ module Ty: sig
val string_reg_lang : t
(** The type of regular language over strings. *)
+ val definition: Expr.Ty.Const.t -> Expr.Ty.def
end
module Term: sig
@@ -94,6 +95,8 @@ val register_converter:
Egraph.t -> (Egraph.t -> t -> unit) -> unit
(** register callback called for each new ground term registered *)
+val tys: Egraph.t -> Node.t -> Ty.S.t
+
module Defs : sig
val add:
Egraph.t ->
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index 7b0fd07648ef7cd5ce318bfd72e5778da2a23707..dde472fc3d78ae22b67795a1dbc33a09b70cba32 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -20,15 +20,22 @@
open Base
open Colibri2_popop_lib
+open Nodes
-type env =
- | Before (** fixing model *)
- | During of { limitreached : bool ref; limit : int; nextnode : int }
+let debug =
+ Debug.register_info_flag ~desc:"for the scheduler in the simple version"
+ "interp"
+
+type during = {
+ limitreached : bool ref; (** it is non backtrable variable *)
+ limit : int;
+ nextnode : Node.t Sequence.t; [@opaque]
+}
[@@deriving show]
-module Data = struct
- let ground = Datastructure.Queue.create Fmt.nop "Interp.ground"
+type env = Before (** fixing model *) | During of during [@@deriving show]
+module Data = struct
let check = Datastructure.Queue.create Fmt.nop "Interp.check"
let node = Datastructure.Queue.create Fmt.nop "Interp.node"
@@ -37,14 +44,14 @@ module Data = struct
let reg_ground = Datastructure.Queue.create Fmt.nop "Interp.reg_ground"
- let reg_node = Datastructure.Queue.create Fmt.nop "Interp.reg_node"
+ (* let reg_node = Datastructure.Queue.create Fmt.nop "Interp.reg_node" *)
let env =
Env.Saved.create_key
(module struct
type t = env
- let name = "Interp.name"
+ let name = "Interp.env"
end)
let () = Env.Saved.register pp_env env
@@ -63,6 +70,10 @@ module SeqLim = struct
d.limitreached := true;
Sequence.Step.Done))
+ let map = Sequence.map
+
+ let unfold_with = Sequence.unfold_with
+
let ( let+ ) = Sequence.( >>| )
let ( let* ) t f = Sequence.bind t ~f
@@ -95,83 +106,128 @@ exception CantInterpretTy of Ground.Ty.t
let ty d ty = get_registered (fun ty -> raise (CantInterpretTy ty)) Data.ty d ty
-exception CantInterpretNode of Nodes.Node.t
+exception CantInterpretNode of Node.t
let node d n =
get_registered (fun n -> raise (CantInterpretNode n)) Data.node d n
exception CantCheckGround of Ground.t
-let ground d n =
- get_registered (fun n -> raise (CantCheckGround n)) Data.ground d n
+let check d n =
+ get_registered (fun n -> raise (CantCheckGround n)) Data.check d n
-let check_ground_terms d =
- Datastructure.Queue.iter Data.reg_ground d ~f:(fun g ->
- if not (ground d g) then Egraph.contradiction d)
-
-(* module WTO = Colibri2_stdlib.Wto.Make (Ground) *)
+exception GroundTermWithoutValueAfterModelFixing of Ground.t
-(* let compute_wto d =
- * let g = Nodes.Node.H.create 100 in *)
+exception ArgOfGroundTermWithoutValueAfterModelFixing of Ground.t * Node.t
-let init d =
- Egraph.set_env d Data.env Before;
- Demon.Fast.register_any_new_node_daemon ~name:"Interp.new_node"
- (fun d g -> Datastructure.Queue.push Data.reg_node d g)
- d;
- Ground.register_converter d (fun d g ->
- Datastructure.Queue.push Data.reg_ground d g)
+let check_ground_terms d =
+ Datastructure.Queue.iter Data.reg_ground d ~f:(fun g ->
+ if Option.is_none (Egraph.get_value d (Ground.node g)) then
+ raise (GroundTermWithoutValueAfterModelFixing g);
+ List.iter (Ground.sem g).args ~f:(fun n ->
+ if Option.is_none (Egraph.get_value d n) then
+ raise (ArgOfGroundTermWithoutValueAfterModelFixing (g, n)));
+ if not (check d g) then (
+ Debug.dprintf2 debug "Interp: checking of %a failed" Ground.Term.pp
+ (Ground.sem g);
+ Egraph.contradiction d))
+
+module WTO = Colibri2_stdlib.Wto.Make (Node)
+
+let rec component_to_seq p =
+ let open Sequence.Generator in
+ match p with
+ | Wto.Component (n, part) -> yield n >>= fun () -> partition_to_seq part
+ | Wto.Node n -> yield n
+
+and partition_to_seq' l =
+ let open Sequence.Generator in
+ match l with
+ | [] -> return ()
+ | a :: l -> component_to_seq a >>= fun () -> partition_to_seq' l
+
+and partition_to_seq l = partition_to_seq' (List.rev l)
+
+let sequence_of_ground d =
+ let open Base in
+ let n2g = Hashtbl.create (module Node) in
+ let inits = Queue.create () in
+ let push n =
+ if not (Hashtbl.mem n2g n) then (
+ if Option.is_none (Egraph.get_value d n) then Queue.enqueue inits n;
+ Hashtbl.set n2g ~key:n ~data:[])
+ in
+ Datastructure.Queue.iter Data.reg_ground d ~f:(fun g ->
+ let n = Egraph.find d (Ground.node g) in
+ push n;
+ List.iter ~f:push (Ground.sem g).args;
+ Hashtbl.add_multi n2g ~key:n ~data:g);
+ let partition =
+ WTO.partition ?pref:None ~inits:(Queue.to_list inits) ~succs:(fun n ->
+ if Option.is_some (Egraph.get_value d n) then []
+ else
+ let gs = Hashtbl.find_multi n2g n in
+ List.concat_map gs ~f:(fun g -> (Ground.sem g).args))
+ in
+ Debug.dprintf2 debug "FixModel wto:%a" (Wto.pp_partition Node.pp) partition;
+ Sequence.Generator.run (partition_to_seq partition)
module Fix_model = struct
let init d =
let env =
- During
- {
- limitreached =
- (* true because we want to continue (i.e start) *)
- ref true;
- nextnode = Datastructure.Queue.length Data.reg_node d - 1;
- limit = 1;
- }
+ {
+ limitreached =
+ (* true because we want to continue (i.e start) *)
+ ref true;
+ nextnode = sequence_of_ground d;
+ limit = 1;
+ }
in
- Egraph.set_env d Data.env env
+ Debug.dprintf0 debug "FixModel with ground terms";
+ Egraph.set_env d Data.env (During env);
+ env
let next_dec d =
match Egraph.get_env d Data.env with
| Before ->
(* The first branching is about the limit *)
- init d;
- Sequence.unfold ~init:(1, d) ~f:(fun (i, d) ->
- match Egraph.get_env d Data.env with
- | Before -> assert false
- | During r ->
- if !(r.limitreached) then
- let limit = i * 2 in
- let dec d =
- match Egraph.get_env d Data.env with
- | Before -> assert false
- | During r ->
- Egraph.set_env d Data.env (During { r with limit })
- in
- Some (dec, (limit, d))
- else None)
+ let r = init d in
+ Sequence.unfold ~init:1 ~f:(fun i ->
+ if !(r.limitreached) then (
+ r.limitreached := false;
+ if i > Base.Int.shift_left 1 25 then raise Impossible;
+ let limit = i * 2 in
+ Debug.dprintf1 debug "FixModel with limit at %i" limit;
+ let dec d = Egraph.set_env d Data.env (During { r with limit }) in
+ Some (dec, limit))
+ else None)
| During r ->
let rec aux nextnode =
- if nextnode < 0 then (
- check_ground_terms d;
- Egraph.set_env d Data.env Before;
- Sequence.empty)
- else
- (* The others are about the values *)
- let n = Datastructure.Queue.get Data.reg_node d r.nextnode in
- match Egraph.get_value d n with
- | Some _ -> aux (nextnode - 1)
- | None ->
- let seq = node d n in
- Sequence.map seq ~f:(fun v d ->
- Egraph.set_env d Data.env
- (During { r with nextnode = nextnode - 1 });
- Egraph.set_value d n v)
+ match Sequence.next nextnode with
+ | None ->
+ Debug.dprintf0 debug "FixModel check_ground terms";
+ check_ground_terms d;
+ Egraph.set_env d Data.env Before;
+ Sequence.empty
+ | Some (n, nextnode) -> (
+ (* The others are about the values *)
+ Debug.dprintf2 debug "FixModel look at %a" Node.pp n;
+ match Egraph.get_value d n with
+ | Some _ -> aux nextnode
+ | None ->
+ Debug.dprintf2 debug "FixModel %a has no value" Node.pp n;
+ let seq =
+ let tys = Ground.tys d n in
+ try node d n
+ with
+ | 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))
in
aux r.nextnode
end
@@ -180,9 +236,129 @@ let () =
Exn_printer.register (fun fmt exn ->
match exn with
| CantInterpretNode t ->
- Fmt.pf fmt "Can't interpret the node %a." Nodes.Node.pp t
- | CantCheckGround t ->
- Fmt.pf fmt "Can't check ground term %a." Ground.pp t
+ Fmt.pf fmt "Can't interpret the node %a." Node.pp t
+ | CantCheckGround g ->
+ Fmt.pf fmt "Can't check ground term %a of type %a." Ground.Term.pp
+ (Ground.sem g) Ground.Ty.pp (Ground.sem g).ty
| CantInterpretTy t ->
Fmt.pf fmt "Can't interpret the type %a." Ground.Ty.pp t
+ | GroundTermWithoutValueAfterModelFixing g ->
+ Fmt.pf fmt "After model fixing %a of type %a has no value"
+ Ground.Term.pp (Ground.sem g) Ground.Ty.pp (Ground.sem g).ty
+ | ArgOfGroundTermWithoutValueAfterModelFixing (g, n) ->
+ Fmt.pf fmt
+ "After model fixing arguments %a of %a of type %a has no value"
+ Node.pp n Ground.Term.pp (Ground.sem g) Ground.Ty.pp
+ (Ground.sem g).ty
| exn -> raise exn)
+
+(** Helpers *)
+module TwoWatchLiteral = struct
+ (** todo move the check to enqueue; but it requires to be able to attach event
+ in delayed_ro *)
+
+ module Daemon = struct
+ type t = {
+ callback : Egraph.t -> Ground.t -> unit;
+ ground : Ground.t; (** perhaps ground should have an array for args *)
+ args : Node.t array;
+ from_start : int Context.Ref.t; (** already set before *)
+ from_end : int Context.Ref.t; (** already set after *)
+ }
+
+ type runable = t
+
+ let print_runable = Fmt.nop
+
+ type event = t
+
+ let print_event = Fmt.nop
+
+ let enqueue _ event =
+ match event with
+ | Events.Fired.EventValue (_, _, d) -> Events.Wait.EnqRun d
+ | _ -> raise Impossible
+
+ let key =
+ Events.Dem.create_key
+ (module struct
+ type d = runable
+
+ type t = event
+
+ let name = "Interp.TwoWatchLiteral"
+ end)
+
+ let delay = Events.FixingModel
+
+ let rec check_if_set d args incr stop i =
+ if Option.is_none (Egraph.get_value d args.(i)) then i
+ else
+ let i = incr + i in
+ if i = stop then stop else check_if_set d args incr stop i
+
+ let attach d r i = Egraph.attach_any_value d r.args.(i) key r
+
+ let run d r =
+ let o_from_start = Context.Ref.get r.from_start in
+ let o_from_end = Context.Ref.get r.from_end in
+ (if o_from_end < o_from_start then ()
+ else
+ let from_start =
+ check_if_set d r.args 1 (o_from_end + 1) o_from_start
+ in
+ if o_from_end < from_start then (
+ Context.Ref.set r.from_start from_start;
+ r.callback d r.ground)
+ else (
+ if from_start <> o_from_start then (
+ Context.Ref.set r.from_start from_start;
+ attach d r from_start);
+ if o_from_end = from_start then ()
+ else
+ let from_end = check_if_set d r.args (-1) from_start o_from_end in
+ Context.Ref.set r.from_end from_end));
+ None
+
+ let create d callback ground =
+ match (Ground.sem ground).args with
+ | [] -> callback d ground
+ | _ ->
+ let args = Array.of_list (Ground.sem ground).args in
+ let r from_start from_end =
+ assert (from_start <= from_end);
+ Debug.dprintf4 debug "Interp create %a (%i-%i)" Ground.pp ground
+ from_start from_end;
+ {
+ callback;
+ ground;
+ args;
+ from_start = Context.Ref.create (Egraph.context d) from_start;
+ from_end = Context.Ref.create (Egraph.context d) from_end;
+ }
+ in
+ let from_start = check_if_set d args 1 (Array.length args) 0 in
+ if from_start = Array.length args then callback d ground
+ else if from_start = Array.length args - 1 then
+ attach d (r from_start from_start) from_start
+ else
+ let from_end =
+ check_if_set d args (-1) from_start (Array.length args - 1)
+ in
+ let r = r from_start from_end in
+ attach d r from_start;
+ attach d r from_end
+ end
+
+ let () = Egraph.Wait.register_dem (module Daemon)
+
+ let create = Daemon.create
+end
+
+let init d =
+ Egraph.set_env d Data.env Before;
+ (* Demon.Fast.register_any_new_node_daemon ~name:"Interp.new_node"
+ * (fun d g -> Datastructure.Queue.push Data.reg_node d g)
+ * d; *)
+ Ground.register_converter d (fun d g ->
+ Datastructure.Queue.push Data.reg_ground d g)
diff --git a/src_colibri2/core/interp.mli b/src_colibri2/core/interp.mli
index e2df2c8e162b7b63f0082d7fe8e7fd099f14fdc2..fcd757cb0dbf2597193a1056a43887574872bf0a 100644
--- a/src_colibri2/core/interp.mli
+++ b/src_colibri2/core/interp.mli
@@ -37,6 +37,11 @@ module SeqLim : sig
(** cartesian product {!Base.Sequence.cartesian_product} *)
val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+
+ val map : 'a t -> f:('a -> 'b) -> 'b t
+
+ val unfold_with :
+ 'a t -> init:'b -> f:('b -> 'a -> ('c, 'b) Sequence.Step.t) -> 'c t
end
module Register : sig
@@ -73,3 +78,8 @@ module Fix_model : sig
(** Add a level of decision for fixing the model, another level could be
needed. Could raise unsatisfiable if all the model have been tried *)
end
+
+module TwoWatchLiteral : sig
+ val create : Egraph.t -> (Egraph.t -> Ground.t -> unit) -> Ground.t -> unit
+ (** call the given function when all the arguments of the ground term have a value *)
+end
diff --git a/src_colibri2/popop_lib/popop_stdlib.ml b/src_colibri2/popop_lib/popop_stdlib.ml
index 78fc690efe31a1a10df85ed6b71be9548431d9be..8d981e9e37e57eb8a300796bbbaf5ec133c3a2f8 100644
--- a/src_colibri2/popop_lib/popop_stdlib.ml
+++ b/src_colibri2/popop_lib/popop_stdlib.ml
@@ -23,6 +23,9 @@ module XHashtbl = Exthtbl.Hashtbl
(* Set, Map, Hashtbl on structures with a unique tag *)
+let sexp_of_t_of_pp pp x =
+ Base.Sexp.Atom (Fmt.str "%a" pp x)
+
module type TaggedType =
sig
type t
@@ -50,24 +53,13 @@ struct
let hash_fold_t s x = Base.Hash.fold_int s (X.tag x)
end
-module OrderedHashedList (X : TaggedType) =
-struct
- type t = X.t list
- let hash = Lists.hash X.tag 3
- let equ_ts ts1 ts2 = X.tag ts1 == X.tag ts2
- let equal = Lists.equal equ_ts
- let cmp_ts ts1 ts2 = Stdlib.compare (X.tag ts1) (X.tag ts2)
- let compare = Lists.compare cmp_ts
- let pp = Pp.list Pp.comma X.pp
- let hash_fold_t s x =
- Base.hash_fold_list (fun s x -> Base.Hash.fold_int s (X.tag x)) s x
-end
-
module MakeMSH (X : TaggedType) =
struct
module T = OrderedHashed(X)
include T
let hash_fold_t state t = Base.Hash.fold_int state (X.tag t)
+ let sexp_of_t = sexp_of_t_of_pp pp
+ let tag = X.tag
module MGen = Intmap.Make(struct
include X
let equal ts1 ts2 = X.tag ts1 == X.tag ts2
@@ -100,6 +92,7 @@ module type Datatype = sig
module S : Map_intf.Set with type 'a M.t = 'a M.t
and type M.key = M.key
module H : Exthtbl.Hashtbl.S with type key = t
+ include Base.Hashtbl.Key.S with type t := t
end
module type Printable = sig
@@ -109,6 +102,7 @@ end
module MkDatatype(T : OrderedHashedType) = struct
let hash_fold_t state t = Base.Hash.fold_int state (T.hash t)
+ let sexp_of_t = sexp_of_t_of_pp T.pp
module M = Map.Make(T)
module S = Extset.MakeOfMap(M)
module H = XHashtbl.Make(T)
@@ -127,7 +121,7 @@ module Int = struct
module DInt = struct
- include Int
+ include Base.Int
let pp fmt x = Format.pp_print_int fmt x
let hash_fold_t = Base.Int.hash_fold_t
module GM = Intmap.Make(Int)
@@ -138,46 +132,32 @@ end
module DIntOrd = DInt
-module DUnit = Unit
-
-module Bool = struct
- open! Base
- type t = bool
- [@@deriving eq, ord, hash, show]
+module DUnit = struct
+ include Unit
+ let sexp_of_t = Base.Unit.sexp_of_t
end
module DBool = struct
- include Bool
- let hash_fold_t = Base.Bool.hash_fold_t
- module M = Map.Make(Bool)
+ include Base.Bool
+ module M = Map.Make(Base.Bool)
module S = Extset.MakeOfMap(M)
- module H = XHashtbl.Make(Bool)
+ module H = XHashtbl.Make(Base.Bool)
end
module DStr = struct
- module Str = struct
- open! Base
- type t = String.t
- [@@deriving show,eq,ord,hash]
- end
- include Str
+ include Base.String
let hash_fold_t = Base.String.hash_fold_t
- module M = Map.Make(Str)
+ module M = Map.Make(Base.String)
module S = Extset.MakeOfMap(M)
- module H = XHashtbl.Make(Str)
+ module H = XHashtbl.Make(Base.String)
end
module DFloat = struct
- module Float = struct
- open! Base
- type t = float
- [@@deriving show,eq,ord,hash]
- end
- include Float
+ include Base.Float
let hash_fold_t = Base.Float.hash_fold_t
- module M = Map.Make(Float)
+ module M = Map.Make(Base.Float)
module S = Extset.MakeOfMap(M)
- module H = XHashtbl.Make(Float)
+ module H = XHashtbl.Make(Base.Float)
end
diff --git a/src_colibri2/popop_lib/popop_stdlib.mli b/src_colibri2/popop_lib/popop_stdlib.mli
index a27d4c17b77d56464d878d6e0592e91ca172fb7a..5223769cc60fb9c7299a55933030908697546439 100644
--- a/src_colibri2/popop_lib/popop_stdlib.mli
+++ b/src_colibri2/popop_lib/popop_stdlib.mli
@@ -23,6 +23,8 @@ module XHashtbl : Exthtbl.Hashtbl
(* Set, Map, Hashtbl on structures with a unique tag *)
+val sexp_of_t_of_pp: 'a Fmt.t -> 'a -> Base.Sexp.t
+
module type TaggedType =
sig
type t
@@ -48,6 +50,7 @@ module type Datatype = sig
module S : Map_intf.Set with type 'a M.t = 'a M.t
and type M.key = M.key
module H : Exthtbl.Hashtbl.S with type key = t
+ include Base.Hashtbl.Key.S with type t := t
end
module type Printable = sig
@@ -61,14 +64,12 @@ module MkDatatype(T : OrderedHashedType) : sig
module S : Map_intf.Set with type 'a M.t = 'a M.t
and type M.key = M.key
module H : Exthtbl.Hashtbl.S with type key = T.t
+ val sexp_of_t: T.t -> Base.Sexp.t
end
module OrderedHashed (X : TaggedType) :
OrderedHashedType with type t = X.t
-module OrderedHashedList (X : TaggedType) :
- OrderedHashedType with type t = X.t list
-
module MakeMSH (X : TaggedType) : Datatype with type t = X.t
module MakeMSHW (X : Weakhtbl.Weakey) :
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 572aadd85efc16c56558664bdfbfef0f88aea2bb..d418ba6989fd067da354adc1c0ba427a492340e8 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -41,6 +41,7 @@ let stats_lasteffort = Debug.register_stats_int ~name:"Scheduler.lasteffort" ~in
let stats_dec = Debug.register_stats_int ~name:"Scheduler.decision" ~init:0
let stats_con = Debug.register_stats_int ~name:"Scheduler.conflict" ~init:0
let stats_step = Debug.register_stats_int ~name:"Scheduler.step" ~init:0
+let stats_fix_model = Debug.register_stats_int ~name:"Scheduler.fix_model" ~init:0
exception NeedStopDelayed
exception Contradiction
@@ -65,7 +66,7 @@ end
module Prio = Leftistheap.Make(Att)
type bp_kind =
- | Choices of (Egraph.t -> unit) list
+ | Choices of (Egraph.t -> unit) Base.Sequence.t
| External
type bp =
@@ -76,11 +77,15 @@ type bp =
pre_level : int;
}
+type solve_step =
+ | Propagate
+ | FixModel
+
type t =
{ mutable choices : Prio.t;
daemons : Events.Wait.daemon_key Context.TimeWheel.t;
lasteffort : Events.Wait.daemon_key Context.TimeWheel.t;
- mutable fixing_model : Events.Wait.daemon_key list;
+ fixing_model : Events.Wait.daemon_key list Context.Ref.t;
mutable prev_scheduler_state : bp option;
solver_state : Egraph.Backtrackable.t;
mutable delayed : Egraph.t option;
@@ -89,6 +94,7 @@ type t =
var_inc : float ref;
context : Context.context;
mutable level: int;
+ solve_step: solve_step Context.Ref.t;
}
(** To treat in the reverse order *)
@@ -116,7 +122,7 @@ let new_solver () =
{ choices = Prio.empty;
daemons = Context.TimeWheel.create (Context.creator context);
lasteffort = Context.TimeWheel.create (Context.creator context);
- fixing_model = [];
+ fixing_model = Context.Ref.create (Context.creator context) [];
prev_scheduler_state = None;
solver_state = Egraph.Backtrackable.new_t (Context.creator context);
context;
@@ -124,6 +130,7 @@ let new_solver () =
decprio = Node.H.create 100;
var_inc = ref 1.;
level = 0;
+ solve_step = Context.Ref.create (Context.creator context) (Propagate);
}
let push kind t =
@@ -172,7 +179,7 @@ let new_delayed =
| LastEffort offset ->
Context.TimeWheel.add t.lasteffort att offset
| FixingModel ->
- t.fixing_model <- att :: t.fixing_model
+ Context.Ref.set t.fixing_model (att :: (Context.Ref.get t.fixing_model))
in
let sched_decision dec =
incr dec_count;
@@ -240,9 +247,12 @@ let rec conflict_analysis t =
pop_to t prev;
t.choices <- Prio.reprio t.decprio t.choices;
match prev.kind with
- | Choices [] -> rewind ()
- | Choices (choice::choices) ->
- make_choice t choice choices
+ | Choices seq -> begin
+ match Base.Sequence.next seq with
+ | None -> rewind ()
+ | Some (choice,choices) ->
+ make_choice t choice choices
+ end
| External -> raise Contradiction
in
rewind ()
@@ -261,7 +271,7 @@ and try_run_dec:
t.choices <- prio;
Debug.incr stats_dec;
Egraph.Backtrackable.delayed_stop d;
- make_choice t todo todos
+ make_choice t todo (Base.Sequence.of_list todos)
and make_choice t todo todos =
ignore (push (Choices todos) t);
@@ -286,48 +296,81 @@ and make_choice t todo todos =
* end
* | Some (Att.Decision (_,_)) | None -> () *)
+let [@inline always] protect_against_contradiction t d f g =
+ match f d with
+ | exception Egraph.Contradiction ->
+ Debug.dprintf0 debug "[Scheduler] Contradiction";
+ Some (conflict_analysis t)
+ | r -> g d r
-let run_one_step t d =
+let run_one_step_propagation ~nodec t d =
Debug.incr stats_step;
match Context.TimeWheel.next t.daemons with
| Some att -> begin
Debug.incr stats_propa;
- try
- Egraph.Backtrackable.run_daemon d att; d
- with Egraph.Contradiction ->
- Debug.dprintf0 debug "[Scheduler] Contradiction";
- conflict_analysis t
+ protect_against_contradiction t d (fun d ->
+ Egraph.Backtrackable.run_daemon d att
+ ) (fun d () -> Some d)
end
+ | None when nodec -> None
| None ->
match Context.TimeWheel.next_at_same_time t.lasteffort with
| Some att -> begin
Debug.dprintf1 debug "[Scheduler] LastEffort mode remaining: %t"
(fun fmt -> Fmt.int fmt (Context.TimeWheel.size_at_current_time t.lasteffort));
Debug.incr stats_lasteffort;
- try
- Egraph.Backtrackable.run_daemon d att; d
- with Egraph.Contradiction ->
- Debug.dprintf0 debug "[Scheduler] Contradiction";
- conflict_analysis t
+ protect_against_contradiction t d (fun d ->
+ Egraph.Backtrackable.run_daemon d att
+ ) (fun d () -> Some d)
end
| None ->
match Prio.extract_min t.choices with
| Att.Decision (_,chogen), prio ->
Debug.dprintf0 debug "[Scheduler] decision";
- try_run_dec t d prio chogen
+ Some (try_run_dec t d prio chogen)
| exception Leftistheap.Empty ->
Debug.dprintf1 debug "[Scheduler] LastEffort: %i" (Context.TimeWheel.size t.lasteffort);
match Context.TimeWheel.next t.lasteffort with
| Some att -> begin
Debug.incr stats_lasteffort;
- try
- Egraph.Backtrackable.run_daemon d att; d
- with Egraph.Contradiction ->
- Debug.dprintf0 debug "[Scheduler] Contradiction";
- conflict_analysis t
+ protect_against_contradiction t d (fun d ->
+ Egraph.Backtrackable.run_daemon d att
+ ) (fun d () -> Some d)
end
| None ->
- d
+ None
+
+let run_one_step_fix_model t d =
+ Debug.incr stats_fix_model;
+ match Context.Ref.get t.fixing_model with
+ | att::l -> begin
+ Context.Ref.set t.fixing_model l;
+ protect_against_contradiction t d (fun d ->
+ Egraph.Backtrackable.run_daemon d att
+ ) (fun d () -> Some d)
+ end
+ | [] ->
+ protect_against_contradiction t d (fun d ->
+ Interp.Fix_model.next_dec d
+ ) (fun d seq ->
+ match Base.Sequence.next seq with
+ | None -> None
+ | Some (todo,todos) ->
+ Egraph.Backtrackable.delayed_stop d;
+ Some (make_choice t todo todos)
+ )
+
+let run_one_step ~nodec t d =
+ match Context.Ref.get t.solve_step with
+ | Propagate -> begin
+ match run_one_step_propagation ~nodec t d with
+ | Some _ as s -> s
+ | None when nodec -> None
+ | None ->
+ Context.Ref.set t.solve_step FixModel;
+ Some d
+ end
+ | FixModel -> run_one_step_fix_model t d
let rec flush t d =
try
@@ -342,19 +385,11 @@ exception ReachStepLimit
let rec run_inf_step ?limit ~nodec t d =
(match limit with | Some n when n <= 0 -> raise ReachStepLimit | _ -> ());
let d = flush t d in
- let run =
- 0 < Context.TimeWheel.size t.daemons ||
- match Prio.min t.choices with
- | Some (Att.Decision _) -> not nodec
- | None -> 0 < Context.TimeWheel.size t.lasteffort
- in
- if run
- then
- let d = run_one_step t d in
+ match run_one_step ~nodec t d with
+ | Some d ->
run_inf_step ?limit:(Opt.map pred limit) ~nodec t d
- else begin
+ | None ->
Egraph.Backtrackable.delayed_stop d
- end
let run_inf_step ?limit ?(nodec=false) t =
if t.delayed <> None then raise NeedStopDelayed;
@@ -395,7 +430,7 @@ let stop_delayed t =
let init_theories ~theories t =
try
let d = get_delayed t in
- List.iter (fun f -> f d) (Ground.init::theories);
+ List.iter (fun f -> f d) (Ground.init::Interp.init::theories);
Egraph.Backtrackable.flush d;
let d = flush t d in
stop t d
diff --git a/src_colibri2/stdlib/context.ml b/src_colibri2/stdlib/context.ml
index 8e2bfdf0ce33a725f181e4d391e5d221bf012e41..d890f6f21414b7b64b1f25a403b5d8ce5b103233 100644
--- a/src_colibri2/stdlib/context.ml
+++ b/src_colibri2/stdlib/context.ml
@@ -326,6 +326,12 @@ module Queue = struct
let fold f acc t = refresh t; Vector.fold f acc t.v
let length t = refresh t; Vector.length t.v
let get t i = refresh t; Vector.get t.v i
+ let of_seq t = refresh t;
+ Base.Sequence.unfold
+ ~init:(Vector.length t.v)
+ ~f:(fun i -> if i = 0 then None else
+ let i = i - 1 in
+ Some(Vector.get t.v i,i))
let pp ?sep pp fmt v = Vector.pp ?pp_sep:sep pp fmt v.v
end
@@ -342,71 +348,71 @@ module RefOpt = struct
end
-module Hashtbl = struct
- module type Sig = sig
- type 'a t
- type key
+module type Hashtbl = sig
+ type 'a t
+ type key
- val create: creator -> 'a t
+ val create: creator -> 'a t
- val remove : 'a t -> key -> unit
- val set : 'a t -> key -> 'a -> unit
- val find: 'a t -> key -> 'a
- val find_opt: 'a t -> key -> 'a option
- val change : ('a option -> 'a option) -> 'a t -> key -> unit
- end
-
- module Make(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key := S.t = struct
-
-
- type 'a t = {
- h: 'a RefOpt.t S.H.t;
- context: context;
- }
-
- let create context = { h = S.H.create 10; context }
+ val remove : 'a t -> key -> unit
+ val set : 'a t -> key -> 'a -> unit
+ val find: 'a t -> key -> 'a
+ val find_opt: 'a t -> key -> 'a option
+ val mem: 'a t -> key -> bool
+ val change : ('a option -> 'a option) -> 'a t -> key -> unit
+end
- let find t k =
- let r = S.H.find t.h k in
- match RefOpt.get r with
- | Some v -> v
- | None -> raise Not_found
+module Hashtbl(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Hashtbl with type key := S.t = struct
- let find_opt t k =
- let open Option in
- let* r = S.H.find_opt t.h k in
- RefOpt.get r
+ type 'a t = {
+ h: 'a RefOpt.t S.H.t;
+ context: context;
+ }
- let set t k v =
- let r = match S.H.find_opt t.h k with
- | Some r -> r
- | None ->
- let r = RefOpt.create t.context in
- S.H.add t.h k r;
- r
- in
- RefOpt.set r v
-
- let remove t k =
- match S.H.find_opt t.h k with
- | Some r -> RefOpt.unset r
- | None -> ()
-
- let change f (t:'a t) k =
- let change = function
- | Some r as o ->
- let v = f (RefOpt.get r) in
- Ref.set r v;
- o
- | None ->
- let r = RefOpt.create t.context in
- let v = f None in
- Ref.set r v;
- (Some r)
- in
- S.H.change change t.h k
+ let create context = { h = S.H.create 10; context }
+
+ let find t k =
+ let r = S.H.find t.h k in
+ match RefOpt.get r with
+ | Some v -> v
+ | None -> raise Not_found
+
+ let find_opt t k =
+ let open Option in
+ let* r = S.H.find_opt t.h k in
+ RefOpt.get r
+
+ let mem t k = Option.is_some (find_opt t k)
+
+ let set t k v =
+ let r = match S.H.find_opt t.h k with
+ | Some r -> r
+ | None ->
+ let r = RefOpt.create t.context in
+ S.H.add t.h k r;
+ r
+ in
+ RefOpt.set r v
+
+ let remove t k =
+ match S.H.find_opt t.h k with
+ | Some r -> RefOpt.unset r
+ | None -> ()
+
+ let change f (t:'a t) k =
+ let change = function
+ | Some r as o ->
+ let v = f (RefOpt.get r) in
+ Ref.set r v;
+ o
+ | None ->
+ let r = RefOpt.create t.context in
+ let v = f None in
+ Ref.set r v;
+ (Some r)
+ in
+ S.H.change change t.h k
- end
end
module Array = struct
@@ -419,3 +425,83 @@ end
module TimeWheel = Colibri2_popop_lib.TimeWheel.Make
(struct type t = creator end)
(Array)(Ref)
+
+module type HashtblWithDefault = sig
+ type 'a t
+ type key
+
+ val create: creator -> (creator -> 'a) -> 'a t
+
+ val set : 'a t -> key -> 'a -> unit
+ val find : 'a t -> key -> 'a
+ val change : ('a -> 'a) -> 'a t -> key -> unit
+end
+
+module HashtblWithDefault(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : HashtblWithDefault with type key := S.t = struct
+
+ type 'a t = {
+ h: 'a Ref.t S.H.t;
+ def: (creator -> 'a);
+ creator: creator;
+ }
+
+ let create creator def =
+ { h = S.H.create 5; def; creator }
+
+ let find_aux t k =
+ match S.H.find_opt t.h k with
+ | Some r -> r
+ | None ->
+ let r = Ref.create t.creator (t.def t.creator) in
+ S.H.add t.h k r;
+ r
+
+ let find t k =
+ Ref.get (find_aux t k)
+
+ let set t k v =
+ let r = find_aux t k in
+ Ref.set r v
+
+ let change f t k =
+ let r = find_aux t k in
+ let v = f (Ref.get r) in
+ Ref.set r v
+
+end
+
+module type Memo = sig
+ type 'a t
+ type key
+
+ val create: creator -> (creator -> key -> 'a) -> 'a t
+ val find : 'a t -> key -> 'a
+ val iter : (key -> 'a -> unit) -> 'a t -> unit
+ val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
+end
+
+module Memo(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo with type key := S.t = struct
+
+ type 'a t = {
+ h: 'a S.H.t;
+ def: (creator -> S.t -> 'a);
+ creator: creator;
+ }
+
+ let create creator def =
+ { h = S.H.create 5; def; creator }
+
+ let find t k =
+ match S.H.find_opt t.h k with
+ | Some r -> r
+ | None ->
+ let r = t.def t.creator k in
+ S.H.add t.h k r;
+ r
+
+ let iter f t =
+ S.H.iter f t.h
+
+ let fold f t =
+ S.H.fold f t.h
+end
diff --git a/src_colibri2/stdlib/context.mli b/src_colibri2/stdlib/context.mli
index 17b6ca326ea45202de5ddf7b6e81c1b84a48d476..8fb3f8b6567efde54a749127313f50bc12f28a7c 100644
--- a/src_colibri2/stdlib/context.mli
+++ b/src_colibri2/stdlib/context.mli
@@ -178,6 +178,8 @@ module Queue: sig
val fold: ('acc -> 'a -> 'acc) -> 'acc -> 'a t -> 'acc
val length: 'a t -> int
val get: 'a t -> int -> 'a
+ val of_seq: 'a t -> 'a Base.Sequence.t
+ (** From last current element to first *)
val pp: ?sep:unit Fmt.t -> 'a Fmt.t -> 'a t Fmt.t
end
@@ -191,3 +193,44 @@ module Array: sig
end
module TimeWheel: Colibri2_popop_lib.TimeWheel.S with type context := creator
+
+module type Hashtbl = sig
+ type 'a t
+ type key
+
+ val create: creator -> 'a t
+
+ val remove : 'a t -> key -> unit
+ val set : 'a t -> key -> 'a -> unit
+ val find: 'a t -> key -> 'a
+ val find_opt: 'a t -> key -> 'a option
+ val mem: 'a t -> key -> bool
+ val change : ('a option -> 'a option) -> 'a t -> key -> unit
+end
+
+module Hashtbl (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Hashtbl with type key := S.t
+
+module type HashtblWithDefault = sig
+ type 'a t
+ type key
+
+ val create: creator -> (creator -> 'a) -> 'a t
+
+ val set : 'a t -> key -> 'a -> unit
+ val find : 'a t -> key -> 'a
+ val change : ('a -> 'a) -> 'a t -> key -> unit
+end
+
+module HashtblWithDefault (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : HashtblWithDefault with type key := S.t
+
+module type Memo = sig
+ type 'a t
+ type key
+
+ val create: creator -> (creator -> key -> 'a) -> 'a t
+ val find : 'a t -> key -> 'a
+ val iter : (key -> 'a -> unit) -> 'a t -> unit
+ val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
+end
+
+module Memo (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo with type key := S.t
diff --git a/src_colibri2/stdlib/wto.ml b/src_colibri2/stdlib/wto.ml
index defb3ba9937ebb2b485161f08012d65c60265ebd..a53a7bd6cecd10bf4aacb4d88ad2a19d549de02d 100644
--- a/src_colibri2/stdlib/wto.ml
+++ b/src_colibri2/stdlib/wto.ml
@@ -226,11 +226,15 @@ module Make(N:sig
type pref = N.t -> N.t -> int
- let partition ?pref ~init ~succs =
+ let partition ?pref ~inits ~succs =
let state = {dfn = DFN.create 17; num = 0; succs;
stack = Stack.create () } in
- let loop,component = visit ~pref state init [] in
- assert (is_no_loop loop);
- component
+ let partition = List.fold_left (fun partition succ ->
+ let (loop',partition) = visit ~pref state succ partition in
+ assert (is_no_loop loop');
+ partition
+ ) [] inits
+ in
+ partition
end
diff --git a/src_colibri2/stdlib/wto.mli b/src_colibri2/stdlib/wto.mli
index 82d6f5b1921f4469616a4cd87a428db9563f1f4d..d09bd5a537687ced45cdfda8d37a5e7463eb0f05 100644
--- a/src_colibri2/stdlib/wto.mli
+++ b/src_colibri2/stdlib/wto.mli
@@ -40,6 +40,9 @@ type 'n component =
(** A list of strongly connected components, sorted topologically *)
and 'n partition = 'n component list
+val pp_partition: 'n Fmt.t -> 'n partition Fmt.t
+val pp_component: 'n Fmt.t -> 'n component Fmt.t
+
val flatten: 'n partition -> 'n list
val fold_heads: ('a -> 'n -> 'a) -> 'a -> 'n partition -> 'a
@@ -57,7 +60,7 @@ module Make(Node:sig
(** Implements Bourdoncle "Efficient chaotic iteration strategies with
widenings" algorithm to compute a WTO. *)
- val partition: ?pref:pref -> init:Node.t -> succs:(Node.t -> Node.t list) -> Node.t partition
+ val partition: ?pref:pref -> inits:Node.t list -> succs:(Node.t -> Node.t list) -> Node.t partition
val equal_component: Node.t component -> Node.t component -> bool
val equal_partition: Node.t partition -> Node.t partition -> bool
diff --git a/src_colibri2/tests/solve/smt_lra/sat/arith_mult_not_linear_in_conflict.smt2 b/src_colibri2/tests/solve/smt_lra/sat/arith_mult_not_linear_in_conflict.smt2
index 1feebcb70c1c8178096c4dd20d08028d6e52baef..52ed73ff6d5efd60c883e29d67e490d2a3e0290a 100644
--- a/src_colibri2/tests/solve/smt_lra/sat/arith_mult_not_linear_in_conflict.smt2
+++ b/src_colibri2/tests/solve/smt_lra/sat/arith_mult_not_linear_in_conflict.smt2
@@ -1,7 +1,7 @@
(set-logic QF_LRA)
-(declare-fun v2 () Real)
-(declare-fun v1 () Real)
-(declare-fun v0 () Real)
+(declare-fun v2 () Real) ; 1.0
+(declare-fun v1 () Real) ; 0.5
+(declare-fun v0 () Real) ; 0.0
(assert
(let ((?n2 (= 0 v1)))
(let ((?n3 (ite ?n2 v2 v0)))
diff --git a/src_colibri2/tests/solve/smt_uf/sat/boolexpup.smt2 b/src_colibri2/tests/solve/smt_uf/sat/boolexpup.smt2
index ff84773fb83b09f905064fd7c74b81ede125070f..8cf5f1cee289822d5acd4bc66f4b223dd9bc79d6 100644
--- a/src_colibri2/tests/solve/smt_uf/sat/boolexpup.smt2
+++ b/src_colibri2/tests/solve/smt_uf/sat/boolexpup.smt2
@@ -1,8 +1,8 @@
(set-logic QF_UF)
(declare-sort S0 0)
-(declare-fun p3 ( S0) Bool)
-(declare-fun v0 () S0)
-(declare-fun v1 () S0)
+(declare-fun p3 ( S0) Bool); false
+(declare-fun v0 () S0) ; @us_S0_0
+(declare-fun v1 () S0) ; @us_S0_1
(assert
(let ((?n1 true))
(let ((?n2 (distinct v0 v1)))
diff --git a/src_colibri2/tests/tests_LRA.ml b/src_colibri2/tests/tests_LRA.ml
index 7c6aac47964728e7ecaae55f070f81e970d0faef..0f2074808912beced31eca8cd6e8f7cc56bcf5fd 100644
--- a/src_colibri2/tests/tests_LRA.ml
+++ b/src_colibri2/tests/tests_LRA.ml
@@ -27,7 +27,8 @@ open Colibri2_core
open Colibri2_stdlib.Std
open Colibri2_stdlib
-let theories = [Boolean.th_register; Equality.th_register; Uninterp.th_register; LRA.th_register]
+let theories = [Boolean.th_register; Equality.th_register;
+ Colibri2_theories_quantifiers.Uninterp.th_register; LRA.th_register]
let ($$) f x = f x
diff --git a/src_colibri2/tests/tests_bool.ml b/src_colibri2/tests/tests_bool.ml
index b10915ee59409dbac7aba707f7e562bab3e81af4..07cdfb4e1e70421b09e12b9bc6345250adc6814f 100644
--- a/src_colibri2/tests/tests_bool.ml
+++ b/src_colibri2/tests/tests_bool.ml
@@ -24,7 +24,7 @@ open Colibri2_core
open Tests_lib
open Colibri2_theories_bool
-let theories = [(* Uninterp.th_register; *) Boolean.th_register]
+let theories = [Colibri2_theories_quantifiers.Uninterp.th_register; Boolean.th_register]
let ($$) f x = f x
diff --git a/src_colibri2/tests/tests_uf.ml b/src_colibri2/tests/tests_uf.ml
index 52ba777e06fd616c0b64cc09e6cbc9e457106210..af42f372e511e40c7ac8716dd78379b1a75ef12e 100644
--- a/src_colibri2/tests/tests_uf.ml
+++ b/src_colibri2/tests/tests_uf.ml
@@ -24,7 +24,8 @@ open Colibri2_core
open Tests_lib
open Colibri2_theories_bool
-let theories = [Boolean.th_register; Equality.th_register; Uninterp.th_register;
+let theories = [Boolean.th_register; Equality.th_register;
+ Colibri2_theories_quantifiers.Uninterp.th_register;
Colibri2_theories_quantifiers.Quantifier.th_register ]
let run = Tests_lib.run_exn ~theories ~nodec:()
let ($$) f x = f x
diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml
index f77b2dcfb1b652abbe783a966e8d35ae8cd6f395..626da1e95ad39a901cecf26569a0092f5bef4938 100644
--- a/src_colibri2/theories/ADT/adt.ml
+++ b/src_colibri2/theories/ADT/adt.ml
@@ -63,9 +63,9 @@ let upd_dom d n d2 =
Egraph.set_dom d D.key n s
let case_of_adt ty =
- match Expr.Ty.definition ty with
- | None | Some Expr.Ty.Abstract -> assert false (* absurd: must be an adt *)
- | Some (Expr.Ty.Adt { cases; _ }) ->
+ match Ground.Ty.definition ty with
+ | Expr.Ty.Abstract -> assert false (* absurd: must be an adt *)
+ | Expr.Ty.Adt { cases; _ } ->
Case.S.of_list (List.init (Array.length cases) (fun i -> i))
(** Decide for destructors *)
@@ -168,14 +168,16 @@ let converter d (f : Ground.t) =
(let+ ve = get e in
match ve with
| Unk s -> if Case.S.mem case s then None else Some false
- | One { case = case'; _ } -> Some (Case.equal case case')))
+ | One { case = case'; _ } -> Some (Case.equal case case')));
+ Adt_value.propagate_value d f
| { app = { builtin = Expr.Constructor { case; _ }; _ }; args; _ } ->
List.iter reg args;
let fields =
Base.List.foldi ~init:Field.M.empty args ~f:(fun field acc a ->
Field.M.add field a acc)
in
- upd_dom d r (One { case; fields })
+ upd_dom d r (One { case; fields });
+ Adt_value.propagate_value d f
| {
app = { builtin = Expr.Destructor { case; field; adt; _ }; _ };
args = [ e ];
@@ -195,10 +197,12 @@ let converter d (f : Ground.t) =
if Case.S.mem case s then upd else nothing
| Unk _ -> nothing
| One { case = case'; _ } ->
- if Case.equal case case' then upd else nothing))
+ if Case.equal case case' then upd else nothing));
+ Adt_value.propagate_value d f
| _ -> ()
let init env : unit =
+ Adt_value.th_register env;
Ground.register_converter env converter;
init_got_value_bool env
diff --git a/src_colibri2/theories/ADT/adt_value.ml b/src_colibri2/theories/ADT/adt_value.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0dad23a60ab11ff26ca508b3afaef038c930700f
--- /dev/null
+++ b/src_colibri2/theories/ADT/adt_value.ml
@@ -0,0 +1,130 @@
+open Base
+open Colibri2_core
+open Colibri2_popop_lib.Popop_stdlib
+open Colibri2_popop_lib
+module Case = DInt
+module Field = DInt
+
+module T' = struct
+ module T = struct
+ type t = {
+ adt : Expr.Ty.Const.t;
+ tyargs : Ground.Ty.t list;
+ case : Case.t;
+ fields : Value.t Field.M.t;
+ }
+ [@@deriving eq, ord, show, hash]
+ end
+
+ include T
+ include MkDatatype (T)
+
+ let key =
+ ValueKind.create_key
+ (module struct
+ include T
+
+ let name = "ADT.value"
+ end)
+end
+
+module V = ValueKind.Register (T')
+include T'
+
+let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
+
+let compute d g =
+ match Ground.sem g with
+ | { app = { builtin = Expr.Tester { case; _ }; _ }; args = [ e ]; _ } ->
+ let v = V.coerce_nodevalue (interp d e) in
+ let v = V.value v in
+ `Some
+ (Colibri2_theories_bool.Boolean.values_of_bool (Case.equal case v.case))
+ | {
+ app = { builtin = Expr.Constructor { adt; case; _ }; _ };
+ args;
+ tyargs;
+ _;
+ } ->
+ let fields =
+ Base.List.foldi ~init:Field.M.empty args ~f:(fun field acc a ->
+ Field.M.add field (interp d a) acc)
+ in
+ let v = { tyargs; adt; case; fields } in
+ `Some (V.nodevalue (V.index v))
+ | {
+ app = { builtin = Expr.Destructor { case; field; _ }; _ };
+ args = [ e ];
+ _;
+ } ->
+ let v = V.coerce_nodevalue (interp d e) in
+ let v = V.value v in
+ if Case.equal case v.case then
+ let v = Field.M.find_opt field v.fields in
+ match v with None -> raise Impossible | Some v -> `Some v
+ else `Uninterpreted
+ | _ -> `None
+
+let init_check d =
+ Interp.Register.check d (fun d t ->
+ match compute d t with
+ | `None -> None
+ | `Some r -> Some (Value.equal r (interp d (Ground.node t)))
+ | `Uninterpreted ->
+ Some
+ (Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain
+ .check d t))
+
+let propagate_value d g =
+ let f d g =
+ match compute d g with
+ | `None -> raise Impossible
+ | `Some v -> Egraph.set_value d (Ground.node g) v
+ | `Uninterpreted ->
+ Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain.propagate
+ d g
+ in
+ Interp.TwoWatchLiteral.create d f g
+
+let init_ty d =
+ Interp.Register.ty d (fun _ ty ->
+ match ty with
+ | { app = { builtin = Dolmen_std.Expr.Base; _ } as sym; args } -> (
+ match Ground.Ty.definition sym with
+ | Abstract -> None
+ | Adt { ty; record = _; cases } ->
+ Some
+ (let open Interp.SeqLim in
+ let cases =
+ Sequence.unfold ~init:0 ~f:(fun i ->
+ if i < Array.length cases then Some ((i, cases.(i)), i + 1)
+ else None)
+ in
+ let* case, { cstr; _ } = of_seq d cases in
+ let subst =
+ List.fold2_exn
+ ~f:(fun acc v ty -> Expr.Ty.Var.M.add v ty acc)
+ ~init:Expr.Ty.Var.M.empty cstr.ty.fun_vars args
+ in
+ let args =
+ List.map ~f:(Ground.Ty.convert subst) cstr.ty.fun_args
+ in
+ let rec aux seq i = function
+ | [] -> seq
+ | ty :: args ->
+ let seq =
+ let+ l = seq and* a = Interp.ty d ty in
+ Field.M.add i a l
+ in
+ aux seq (i + 1) args
+ in
+ let+ fields =
+ aux (of_seq d (Sequence.singleton Field.M.empty)) 0 args
+ in
+ V.nodevalue (V.index { tyargs = args; adt = ty; case; fields }))
+ )
+ | _ -> None)
+
+let th_register d =
+ init_check d;
+ init_ty d
diff --git a/src_colibri2/theories/ADT/adt_value.mli b/src_colibri2/theories/ADT/adt_value.mli
new file mode 100644
index 0000000000000000000000000000000000000000..3f2f3f0ce9ab6429787cebf0a302b1cd807726ce
--- /dev/null
+++ b/src_colibri2/theories/ADT/adt_value.mli
@@ -0,0 +1,3 @@
+val th_register : Egraph.t -> unit
+
+val propagate_value : Egraph.t -> Ground.t -> unit
diff --git a/src_colibri2/theories/ADT/dune b/src_colibri2/theories/ADT/dune
index d18eac71dce3d34ac50b768e3f98bb517b8b0335..ecb846e0b02f0e2faf08febe7b38c88d9492c46a 100644
--- a/src_colibri2/theories/ADT/dune
+++ b/src_colibri2/theories/ADT/dune
@@ -3,7 +3,9 @@
(public_name colibri2.theories.adt)
(synopsis "theory of algebraic datatype for colibri2")
(libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
- colibri2.core.structures colibri2.core colibri2.theories.bool)
+ colibri2.core.structures colibri2.core colibri2.theories.bool
+ colibri2.theories.quantifiers
+ )
(preprocess
(pps ppx_deriving.std ppx_hash))
(flags :standard -open Containers -open Colibri2_stdlib -open Std -open
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index 4c2480f446fd43c48ac469902a74078591ba022f..3065286b53b42ae216d10d6958d30d31935cba1f 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -19,52 +19,10 @@
(*************************************************************************)
open Colibri2_core
-open Colibri2_popop_lib
open Colibri2_stdlib.Std
let default_value = Q.zero
-let init_check d =
- Interp.Register.check d (fun d t ->
- let exception False in
- try
- let interp n = Opt.get_exn False (Egraph.get_value d n) in
- let (!>) t = RealValue.value (RealValue.coerce_nodevalue (interp t)) in
- let check r =
- Some (Value.equal r (interp (Ground.node t)))
- in
- let (!<) v = check (RealValue.nodevalue (RealValue.index v)) in
- let (!<<) b =
- let r = if b then Boolean.values_true else Boolean.values_false in
- check r
- in
- match Ground.sem t with
- | { app = {builtin = Expr.Integer s}; tyargs = []; args = []; ty = _ } ->
- !< (Q.of_string s)
- | { app = {builtin = Expr.Decimal s}; tyargs = []; args = []; ty = _ } ->
- !< (Q.of_string_decimal s)
- | { app = {builtin = Expr.Rational s}; tyargs = []; args = []; ty = _ } ->
- !< (Q.of_string_decimal s)
- | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; ty = _ } ->
- !< (Q.add !>a !>b)
- | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; ty = _ } ->
- !< (Q.sub !>a !>b)
- | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; ty = _ } ->
- !< (Q.neg !>a)
- | { app = {builtin = Expr.Mul}; tyargs = []; args = [a;b]; ty = _ } ->
- !< (Q.mul !>a !>b)
- | { app = {builtin = Expr.Lt}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
- !<< (Q.lt !>arg1 !>arg2)
- | { app = {builtin = Expr.Leq}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
- !<< (Q.leq !>arg1 !>arg2)
- | { app = {builtin = Expr.Gt}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
- !<< (Q.gt !>arg1 !>arg2)
- | { app = {builtin = Expr.Geq}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
- !<< (Q.geq !>arg1 !>arg2)
- | _ -> None
- with False -> Some false
- )
-
module RealValue = RealValue
let th_register env =
@@ -74,7 +32,6 @@ let th_register env =
Fourier.init env;
Mul.init env;
Dom_product.init env;
- init_check env;
()
let () = Egraph.add_default_theory th_register
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index c6a2e8f33bf465b00acb9292a69cfb4e6ac8877d..70d14e86d5d655ef0c0073398f2a579b46a553bd 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -19,6 +19,7 @@
(*************************************************************************)
open Colibri2_core
+open Colibri2_popop_lib
open Colibri2_stdlib.Std
module RealValue = ValueKind.Register(struct
@@ -29,7 +30,6 @@ module RealValue = ValueKind.Register(struct
include RealValue
let cst' c = index ~basename:(Format.asprintf "%aR" Q.pp c) c
-
let cst c = node (cst' c)
let zero = cst Q.zero
@@ -56,6 +56,7 @@ module Monad : sig
val getb: Node.t -> (bool,bool option) monad
val setb: Node.t -> ('a,bool option) monad -> ('a,unit) monad
val (let+): ('a,'b option) monad -> ('b -> 'c) -> ('a,'c option) monad
+ val (let*): ('a,'b option) monad -> ('b -> 'c option) -> ('a,'c option) monad
val (and+): ('a,'b option) monad -> ('a,'c option) monad -> ('a,('b * 'c) option) monad
val (&&): ('a,unit) monad -> ('a,unit) monad -> ('a,unit) monad
end = struct
@@ -79,13 +80,112 @@ end = struct
let getb a = get' Boolean.BoolValue.key a
let setb a = set' (module Boolean.BoolValue) a
let [@ocaml.always inline] (let+) a (f:'b -> 'a) = fun d n v -> Option.map f (a d n v)
+ let [@ocaml.always inline] (let*) a (f:'b -> 'a option) = fun d n v -> Option.bind (a d n v) f
let [@ocaml.always inline] (and+) a b = fun d n v -> match a d n v, b d n v with
| Some a, Some b -> Some (a,b) | _ -> None
let [@ocaml.always inline] (&&) a b = fun d n v -> a d n v; b d n v
end
-(** {2 Initialization} *)
+
+let int_sequence_without_zero =
+ let open Base.Sequence.Generator in
+ let rec loop i =
+ yield i >>= fun () -> yield (Z.neg i) >>= (fun () -> loop (Z.succ i))
+ in
+ run (loop Z.one)
+
+let int_sequence =
+ Base.Sequence.shift_right int_sequence_without_zero Z.zero
+
+let init_ty d =
+ Interp.Register.ty d (fun d ty ->
+ match ty with
+ | {app={builtin = Expr.Int;_};_} ->
+ Some (Interp.SeqLim.map (Interp.SeqLim.of_seq d int_sequence)
+ ~f:(fun i -> nodevalue (cst' (Q.of_bigint i)))
+ )
+ | {app={builtin = Expr.Real;_};_} ->
+ let seq =
+ let open Interp.SeqLim in
+ let+ num = of_seq d int_sequence
+ and* den = of_seq d int_sequence_without_zero in
+ (Q.make num den)
+ in
+ let seq = Interp.SeqLim.unfold_with seq ~init:Q.S.empty
+ ~f:(fun s v -> if Q.S.mem v s then Skip s
+ else Yield(nodevalue (cst' v),Q.S.add v s)) in
+ Some seq
+ | _ -> None)
+
+module Check = struct
+ let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
+ let compute_ground d t =
+ let (!>) t = RealValue.value (RealValue.coerce_nodevalue (interp d t)) in
+ let (!<) v = `Some (RealValue.nodevalue (RealValue.index v)) in
+ let (!<<) b =
+ let r = if b then Boolean.values_true else Boolean.values_false in
+ `Some r
+ in
+ match Ground.sem t with
+ | { app = {builtin = Expr.Coercion};
+ tyargs =
+ ( [{app={builtin = (Expr.Int|Expr.Rat);_};_};{app={builtin = Expr.Real;_};_}]
+ | [{app={builtin = Expr.Int;_};_};{app={builtin = Expr.Rat;_};_}]
+ );
+ args = [a] } ->
+ !< (!> a)
+ | { app = {builtin = Expr.Integer s}; tyargs = []; args = []; ty = _ } ->
+ !< (Q.of_string s)
+ | { app = {builtin = Expr.Decimal s}; tyargs = []; args = []; ty = _ } ->
+ !< (Q.of_string_decimal s)
+ | { app = {builtin = Expr.Rational s}; tyargs = []; args = []; ty = _ } ->
+ !< (Q.of_string_decimal s)
+ | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; ty = _ } ->
+ !< (Q.add !>a !>b)
+ | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; ty = _ } ->
+ !< (Q.sub !>a !>b)
+ | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; ty = _ } ->
+ !< (Q.neg !>a)
+ | { app = {builtin = Expr.Mul}; tyargs = []; args = [a;b]; ty = _ } ->
+ !< (Q.mul !>a !>b)
+ | { app = {builtin = Expr.Div}; tyargs = []; args = [a;b]; ty = _ } ->
+ if Q.is_zero !>b then `Uninterp
+ else !< (Q.div !>a !>b)
+ | { app = {builtin = Expr.Lt}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
+ !<< (Q.lt !>arg1 !>arg2)
+ | { app = {builtin = Expr.Leq}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
+ !<< (Q.leq !>arg1 !>arg2)
+ | { app = {builtin = Expr.Gt}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
+ !<< (Q.gt !>arg1 !>arg2)
+ | { app = {builtin = Expr.Geq}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
+ !<< (Q.geq !>arg1 !>arg2)
+ | { app = {builtin = Expr.Floor}; tyargs = []; args = [a]; _ } ->
+ !< (Q.floor (!> a))
+ | _ -> `None
+
+ let init d =
+ Interp.Register.check d (fun d t ->
+ let check r =
+ Value.equal r (interp d (Ground.node t))
+ in
+ match compute_ground d t with
+ | `None -> None
+ | `Some v -> Some (check v)
+ | `Uninterp -> Some (Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain.check d t)
+ )
+
+ let attach d g =
+ let f d g =
+ match compute_ground d g with
+ | `None -> raise Impossible
+ | `Some v -> Egraph.set_value d (Ground.node g) v
+ | `Uninterp -> Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain.propagate d g
+ in
+ Interp.TwoWatchLiteral.create d f g
+end
+
+ (** {2 Initialization} *)
let converter d (f:Ground.t) =
let r = Ground.node f in
let reg n = Egraph.register d n in
@@ -105,7 +205,7 @@ let converter d (f:Ground.t) =
| [{app={builtin = Expr.Int;_};_};{app={builtin = Expr.Rat;_};_}]
);
args = [a] } ->
- merge a
+ merge a; Check.attach d f
| { app = {builtin = Expr.Integer s}; tyargs = []; args = []; _ } ->
merge (cst (Q.of_string s))
| { app = {builtin = Expr.Decimal s}; tyargs = []; args = []; _ } ->
@@ -113,7 +213,7 @@ let converter d (f:Ground.t) =
| { app = {builtin = Expr.Rational s}; tyargs = []; args = []; _ } ->
merge (cst (Q.of_string_decimal s))
| { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
- reg a; reg b;
+ reg a; reg b; Check.attach d f;
let wait =
set r (let+ va = get a and+ vb = get b in Q.add va vb) &&
set a (let+ vb = get b and+ vr = get r in Q.sub vr vb) &&
@@ -121,33 +221,44 @@ let converter d (f:Ground.t) =
in
List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
| { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
- reg a; reg b;
+ reg a; reg b; Check.attach d f;
let wait =
set r (let+ va = get a and+ vb = get b in Q.sub va vb) &&
set a (let+ vb = get b and+ vr = get r in Q.add vr vb) &&
set b (let+ va = get a and+ vr = get r in Q.sub va vr)
in
List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
+ | { app = {builtin = Expr.Mul}; tyargs = []; args = [a;b]; _ } ->
+ reg a; reg b; Check.attach d f;
+ let wait =
+ set r (let+ va = get a and+ vb = get b in Q.mul va vb) &&
+ set a (let* vb = get b and+ vr = get r in if Q.is_zero vb then None else Some (Q.div vr vb)) &&
+ set b (let* va = get a and+ vr = get r in if Q.is_zero va then None else Some (Q.div vr va))
+ in
+ List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
| { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; _ } ->
- reg a;
+ reg a; Check.attach d f;
let wait =
set r (let+ va = get a in Q.neg va) &&
set a (let+ vr = get r in Q.neg vr)
in
List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;r]
| { app = {builtin = Expr.Lt}; tyargs = []; args = [a;b]; _ } ->
- cmp Q.lt a b
+ cmp Q.lt a b; Check.attach d f;
| { app = {builtin = Expr.Leq}; tyargs = []; args = [a;b]; _ } ->
- cmp Q.le a b
+ cmp Q.le a b; Check.attach d f;
| { app = {builtin = Expr.Gt}; tyargs = []; args = [a;b]; _ } ->
- cmp Q.gt a b
+ cmp Q.gt a b; Check.attach d f;
| { app = {builtin = Expr.Geq}; tyargs = []; args = [a;b]; _ } ->
- cmp Q.ge a b
+ cmp Q.ge a b; Check.attach d f;
| { app = {builtin = Expr.Floor}; tyargs = []; args = [a]; _ } ->
- reg a
+ reg a; Check.attach d f;
| _ -> ()
+
let init env =
Ground.register_converter env converter;
init_got_value_bool env;
- init_got_value env
+ init_got_value env;
+ init_ty env;
+ Check.init env
diff --git a/src_colibri2/theories/bool/.ocamlformat b/src_colibri2/theories/bool/.ocamlformat
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src_colibri2/theories/bool/.ocamlformat-ignore b/src_colibri2/theories/bool/.ocamlformat-ignore
new file mode 100644
index 0000000000000000000000000000000000000000..79df3ce7b5a14dceda726de31dd2728842dc0de5
--- /dev/null
+++ b/src_colibri2/theories/bool/.ocamlformat-ignore
@@ -0,0 +1,4 @@
+equality.ml
+boolean.ml
+boolean.mli
+equality.mli
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index 4492b29a5a300904ed27a30b7f11d62a0be9f915..89fd485417fd2fb4bea3c7b2276af896d7c40ba8 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -44,6 +44,9 @@ let value_false = BoolValue.index ~basename:"⊥" false
let values_false = BoolValue.nodevalue value_false
let node_false = BoolValue.node value_false
+let value_of_bool b = if b then value_true else value_false
+let values_of_bool b = if b then values_true else values_false
+
(* Function is not used. Don't know what the types of b1 and b2 are. *)
(* let union_disjoint m1 m2 =
* Node.M.union (fun _ b1 b2 -> assert (Equal.physical b1 b2); Some b1) m1 m2 *)
@@ -446,32 +449,31 @@ let converter d (f:Ground.t) =
let init_check d =
Interp.Register.check d (fun d t ->
- let exception False in
- try
- let interp n = Opt.get_exn False (Egraph.get_value d n) in
- let (!>) t = BoolValue.value (BoolValue.coerce_nodevalue (interp t)) in
- let check r =
- Some (Value.equal r (interp (Ground.node t)))
- in
- let (!<) b =
- let r = if b then values_true else values_false in
- check r
- in
- match Ground.sem t with
- | { app = {builtin = Expr.Or}; tyargs = []; args = args; ty = _ } ->
- !< (List.fold_left (||) false (List.map (!>) args))
- | { app = {builtin = Expr.And}; tyargs = []; args = args; ty = _ } ->
- !< (List.fold_left (&&) true (List.map (!>) args))
- | { app = {builtin = Expr.Imply}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
- !< ( not (!> arg1) || !> arg2 )
- | { app = {builtin = Expr.Neg}; tyargs = []; args = [arg]; ty = _ } ->
- !< (not (!> arg))
- | { app = {builtin = Expr.True}; tyargs = []; args = []; ty = _ } ->
- check values_true
- | { app = {builtin = Expr.False}; tyargs = []; args = []; ty = _ } ->
- check values_false
- | _ -> None
- with False -> Some false
+ let interp n = Opt.get_exn Impossible (Egraph.get_value d n) in
+ let (!>) t = BoolValue.value (BoolValue.coerce_nodevalue (interp t)) in
+ let check r =
+ Some (Value.equal r (interp (Ground.node t)))
+ in
+ let (!<) b =
+ let r = if b then values_true else values_false in
+ check r
+ in
+ match Ground.sem t with
+ | { app = {builtin = Expr.Or}; tyargs = []; args = args; ty = _ } ->
+ !< (List.fold_left (||) false (List.map (!>) args))
+ | { app = {builtin = Expr.And}; tyargs = []; args = args; ty = _ } ->
+ !< (List.fold_left (&&) true (List.map (!>) args))
+ | { app = {builtin = Expr.Imply}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
+ !< ( not (!> arg1) || !> arg2 )
+ | { app = {builtin = Expr.Xor}; tyargs = []; args = [arg1;arg2]; _ } ->
+ !< ( not (Bool.equal (!> arg1) (!> arg2) ))
+ | { app = {builtin = Expr.Neg}; tyargs = []; args = [arg]; ty = _ } ->
+ !< (not (!> arg))
+ | { app = {builtin = Expr.True}; tyargs = []; args = []; ty = _ } ->
+ check values_true
+ | { app = {builtin = Expr.False}; tyargs = []; args = []; ty = _ } ->
+ check values_false
+ | _ -> None
)
let th_register env =
diff --git a/src_colibri2/theories/bool/boolean.mli b/src_colibri2/theories/bool/boolean.mli
index 3bd258bfbe0968715515cafe347bdb46defe9cc5..e605b717a5154b9024ad85aecb1785bc8aeabef0 100644
--- a/src_colibri2/theories/bool/boolean.mli
+++ b/src_colibri2/theories/bool/boolean.mli
@@ -56,3 +56,5 @@ val value_true : BoolValue.t
val value_false: BoolValue.t
val values_true : Value.t
val values_false: Value.t
+val value_of_bool: bool -> BoolValue.t
+val values_of_bool: bool -> Value.t
diff --git a/src_colibri2/theories/bool/dune b/src_colibri2/theories/bool/dune
index 4d9ae28830166d50a51643cd6953a4043027943a..1b294acbe56d529984963c6719b2625bf67f227d 100644
--- a/src_colibri2/theories/bool/dune
+++ b/src_colibri2/theories/bool/dune
@@ -2,7 +2,7 @@
(name colibri2_theories_bool)
(public_name colibri2.theories.bool)
(synopsis "theories for colibri2")
- (modules Boolean Equality Uninterp)
+ (modules Boolean Equality)
(libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
colibri2.core.structures colibri2.core dolmen.std)
(preprocess
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index 3a26d463557ffaaf7ce767451fd31792fc9209b0..29bef0af8486fe492dc1207670cffa304078b935 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -565,39 +565,36 @@ let bool_init_diff_to_value d =
let init_check d =
Interp.Register.check d (fun d t ->
- let exception False in
- try
- let interp n = Opt.get_exn False (Egraph.get_value d n) in
- let (!>) n =
- Boolean.BoolValue.value
- (Boolean.BoolValue.coerce_nodevalue (interp n))
- in
- let check r =
- Some (Value.equal r (interp (Ground.node t)))
- in
- let (!<) b =
- let r = if b then Boolean.values_true else Boolean.values_false in
- check r
- in
- match Ground.sem t with
- | { app = {builtin = Expr.Equal}; tyargs = [_]; args = a::l; ty = _ } ->
- let a = interp a in
- !< (List.for_all (fun t -> Value.equal a (interp t)) l)
- | { app = {builtin = Expr.Equiv}; tyargs = [_]; args = [a;b]; ty = _ } ->
- !< (Value.equal (interp a) (interp b))
- | { app = {builtin = Expr.Distinct}; tyargs = [_]; args = args; ty = _ } ->
- begin
- try
- let fold acc v = Value.S.add_new Exit (interp v) acc in
- let _ = List.fold_left fold Value.S.empty args in
- check Boolean.values_false
- with Exit ->
- check Boolean.values_true
- end
- | { app = {builtin = Expr.Ite}; tyargs = [_]; args = [c;a;b]; ty = _ } ->
- check (if (!> c) then interp a else interp b)
- | _ -> None
- with False -> Some false
+ let interp n = Opt.get_exn Impossible (Egraph.get_value d n) in
+ let (!>) n =
+ Boolean.BoolValue.value
+ (Boolean.BoolValue.coerce_nodevalue (interp n))
+ in
+ let check r =
+ Some (Value.equal r (interp (Ground.node t)))
+ in
+ let (!<) b =
+ let r = if b then Boolean.values_true else Boolean.values_false in
+ check r
+ in
+ match Ground.sem t with
+ | { app = {builtin = Expr.Equal}; tyargs = [_]; args = a::l; ty = _ } ->
+ let a = interp a in
+ !< (List.for_all (fun t -> Value.equal a (interp t)) l)
+ | { app = {builtin = Expr.Equiv}; tyargs = [_]; args = [a;b]; ty = _ } ->
+ !< (Value.equal (interp a) (interp b))
+ | { app = {builtin = Expr.Distinct}; tyargs = [_]; args = args; ty = _ } ->
+ begin
+ try
+ let fold acc v = Value.S.add_new Exit (interp v) acc in
+ let _ = List.fold_left fold Value.S.empty args in
+ check Boolean.values_true
+ with Exit ->
+ check Boolean.values_false
+ end
+ | { app = {builtin = Expr.Ite}; tyargs = [_]; args = [c;a;b]; ty = _ } ->
+ check (if (!> c) then interp a else interp b)
+ | _ -> None
)
diff --git a/src_colibri2/theories/quantifier/FA.ml b/src_colibri2/theories/quantifier/FA.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3e0c8f7612b4da815f36cdea2974d1144c1e322d
--- /dev/null
+++ b/src_colibri2/theories/quantifier/FA.ml
@@ -0,0 +1,12 @@
+(** instantiated function symbol *)
+module T = struct
+ let hash_fold_list = Base.hash_fold_list
+
+ type t = { tc : F.t; ta : Expr.Ty.t list } [@@deriving eq, ord, hash]
+
+ let pp fmt { tc; ta } =
+ Format.fprintf fmt "%a[%a]" F.pp tc Fmt.(list ~sep:comma Expr.Ty.pp) ta
+end
+
+include T
+include Colibri2_popop_lib.Popop_stdlib.MkDatatype (T)
diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml
index a485a4cf27a1198f4b42207846d9a8b37f953db1..daa271b5373d057cc9502f1814e53612d3909c75 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.ml
+++ b/src_colibri2/theories/quantifier/InvertedPath.ml
@@ -12,7 +12,10 @@ type t' = {
matches : t Pattern.M.t;
triggers : Trigger.t list;
ups :
- (Expr.Ty.t list * Pattern.t list * int (* from which argument we come *) * t)
+ (Expr.Ty.t list
+ * Pattern.t list
+ * int (* from which argument we come *)
+ * t)
list
F_Pos.M.t;
}
@@ -83,16 +86,17 @@ module HPT = Datastructure.Memo (F_Pos)
module HPN = Datastructure.Memo (PN)
(** parent-child, wait for a subterm with the right application *)
-let pc_ips = HPC.create Fmt.nop "Quantifier.pc" create
+let pc_ips = HPC.create Fmt.nop "Quantifier.pc" (fun c _ -> create c)
(** parent-parent, a variable appears two times *)
-let pp_ips = HPP.create Fmt.nop "Quantifier.pp" create
+let pp_ips = HPP.create Fmt.nop "Quantifier.pp" (fun c _ -> create c)
(** parent-type, wait for a type to match a variable *)
-let pt_ips = HPT.create Fmt.nop "Quantifier.pt" Context.Queue.create
+let pt_ips =
+ HPT.create Fmt.nop "Quantifier.pt" (fun c _ -> Context.Queue.create c)
(** parent-node, wait for a subterm with the right class *)
-let pn_ips = HPN.create Fmt.nop "Quantifier.pn" create
+let pn_ips = HPN.create Fmt.nop "Quantifier.pn" (fun c _ -> create c)
let add_pattern pat ip =
Context.Ref.set ip
diff --git a/src_colibri2/theories/quantifier/InvertedPath.mli b/src_colibri2/theories/quantifier/InvertedPath.mli
index a4b64a06d13b6c9bd6e3587363b918ecc1a6020e..c2551744b710523b0c167020b69b9811f1c9994f 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.mli
+++ b/src_colibri2/theories/quantifier/InvertedPath.mli
@@ -19,23 +19,23 @@ val insert_pattern : Egraph.t -> Trigger.t -> unit
(** [insert_pattern d tri] insert the pattern in the database of inverted path
for all its subterms *)
-module HPP : Datastructure.Sig3 with type key := PP.t
+module HPP : Datastructure.Memo with type key := PP.t
val pp_ips : t HPP.t
(** The database of inverted path for each parent-parent pairs *)
-module HPC : Datastructure.Sig3 with type key := PC.t
+module HPC : Datastructure.Memo with type key := PC.t
val pc_ips : t HPC.t
(** The database of inverted path for each parent-child pairs *)
-module HPT : Datastructure.Sig3 with type key := F_Pos.t
+module HPT : Datastructure.Memo with type key := F_Pos.t
val pt_ips : (Ty.t * t) Context.Queue.t HPT.t
(** The database of inverted path for each parent-type, needed for polymorphic
variables *)
-module HPN : Datastructure.Sig3 with type key := PN.t
+module HPN : Datastructure.Memo with type key := PN.t
val pn_ips : t HPN.t
(** The database of inverted path for each parent-node pairs *)
diff --git a/src_colibri2/theories/quantifier/dune b/src_colibri2/theories/quantifier/dune
index dbf85cf3e97adb77fa34de14c856ad6861b51827..addf72911482e3977c2c5cbea6d1037f06c33abe 100644
--- a/src_colibri2/theories/quantifier/dune
+++ b/src_colibri2/theories/quantifier/dune
@@ -2,7 +2,7 @@
(name colibri2_theories_quantifiers)
(public_name colibri2.theories.quantifiers)
(synopsis "theories for colibri2")
- (libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
+ (libraries containers base ocamlgraph colibri2.stdlib colibri2.popop_lib
colibri2.core.structures colibri2.core colibri2.theories.bool)
(preprocess
(pps ppx_deriving.std ppx_hash))
diff --git a/src_colibri2/theories/quantifier/info.ml b/src_colibri2/theories/quantifier/info.ml
index a9a0703227dacef78a1f403cb15de254cda7aec9..2f566d44bbb701123bbea8b52a32efcb55bb912d 100644
--- a/src_colibri2/theories/quantifier/info.ml
+++ b/src_colibri2/theories/quantifier/info.ml
@@ -3,7 +3,6 @@
type t = {
parents : Ground.S.t F_Pos.M.t; (** parents *)
apps : Ground.S.t F.M.t; (** parent parent *)
- tys : Ground.Ty.S.t;
}
[@@deriving show]
@@ -54,16 +53,14 @@ let merge d ~other ~repr info info' =
parents = congruence_closure d ~other ~repr info.parents info'.parents;
apps =
F.M.union (fun _ a b -> Some (Ground.S.union a b)) info.apps info'.apps;
- tys = Ground.Ty.S.union info.tys info'.tys;
}
-let empty =
- { parents = F_Pos.M.empty; apps = F.M.empty; tys = Ground.Ty.S.empty }
+let empty = { parents = F_Pos.M.empty; apps = F.M.empty }
let dom =
DomKind.create_key
- ( module struct
+ (module struct
type nonrec t = t
let name = "Quantifier.info"
- end )
+ end)
diff --git a/src_colibri2/theories/quantifier/info.mli b/src_colibri2/theories/quantifier/info.mli
index 82834017100df6eac512fc0560857f767d4ed3b5..2b8dc01718aa3bd8b69be51c34b18e880cce7614 100644
--- a/src_colibri2/theories/quantifier/info.mli
+++ b/src_colibri2/theories/quantifier/info.mli
@@ -1,7 +1,6 @@
type t = {
parents : Ground.S.t F_Pos.M.t; (** parents *)
apps : Ground.S.t F.M.t; (** parent parent *)
- tys : Ground.Ty.S.t;
}
[@@deriving show]
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
index 5cd7975ca0ce5063ca8d4e884aff7763cc93f9f6..79dc1057cc60618e1099562390f700648ccf1ec9 100644
--- a/src_colibri2/theories/quantifier/pattern.ml
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -31,7 +31,7 @@ let rec of_term ~subst (t : Expr.Term.t) =
| Var v -> (
match Expr.Term.Var.M.find v subst.Ground.Subst.term with
| exception Not_found -> Var v (* todo type substitution *)
- | n -> Node n )
+ | n -> Node n)
| App ({ builtin = Expr.Coercion; _ }, _, [ a ]) -> of_term ~subst a
| App (f, tys, tl) ->
(* todo type substitution *)
@@ -72,10 +72,7 @@ let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) :
Ground.Subst.S.union (match_ty substs ty v.ty) acc
in
let substs =
- match Egraph.get_dom d Info.dom n with
- | None -> Ground.Subst.S.empty
- | Some info ->
- Ground.Ty.S.fold_left match_ty Ground.Subst.S.empty info.tys
+ Ground.Ty.S.fold_left match_ty Ground.Subst.S.empty (Ground.tys d n)
in
Ground.Subst.S.fold_left
(fun acc subst ->
@@ -115,7 +112,7 @@ let rec check_ty subst (ty : Ground.Ty.t) (p : Expr.Ty.t) : bool =
| Var v -> (
match Expr.Ty.Var.M.find v subst.Ground.Subst.ty with
| exception Not_found -> false
- | ty' -> Ground.Ty.equal ty ty' )
+ | ty' -> Ground.Ty.equal ty ty')
| App (cst', tyl') ->
Expr.Ty.Const.equal ty.app cst'
&& List.for_all2 (check_ty subst) ty.args tyl'
@@ -124,14 +121,11 @@ let rec check_term d (subst : Ground.Subst.t) (n : Node.t) (p : t) : bool =
Debug.dprintf4 debug "[Quant] check %a %a" pp p Node.pp n;
match p with
| Var v -> (
- match Egraph.get_dom d Info.dom n with
- | None -> false
- | Some info -> (
- Ground.Ty.S.exists (fun ty -> check_ty subst ty v.ty) info.tys
- &&
- match Expr.Term.Var.M.find v subst.term with
- | exception Not_found -> false
- | n' -> Egraph.is_equal d n n' ) )
+ Ground.Ty.S.exists (fun ty -> check_ty subst ty v.ty) (Ground.tys d n)
+ &&
+ match Expr.Term.Var.M.find v subst.term with
+ | exception Not_found -> false
+ | n' -> Egraph.is_equal d n n')
| App (pf, ptyl, pargs) ->
let s =
Opt.get_def Ground.S.empty
@@ -158,14 +152,12 @@ let rec check_term_exists_exn d (subst : Ground.Subst.t) (p : t) : Node.S.t =
| Var v -> (
match Expr.Term.Var.M.find v subst.term with
| exception Not_found -> raise IncompleteSubstitution
- | n -> (
- match Egraph.get_dom d Info.dom n with
- | None -> raise Not_found
- | Some info ->
- if
- (Ground.Ty.S.exists (fun ty -> check_ty subst ty v.ty)) info.tys
- then Node.S.singleton (Egraph.find_def d n)
- else raise Not_found ) )
+ | n ->
+ if
+ (Ground.Ty.S.exists (fun ty -> check_ty subst ty v.ty))
+ (Ground.tys d n)
+ then Node.S.singleton (Egraph.find_def d n)
+ else raise Not_found)
| App (pf, ptyl, []) ->
let g =
Ground.apply pf (List.map (Ground.Ty.convert subst.ty) ptyl) []
@@ -234,16 +226,14 @@ let get_pps pattern =
m
let env_ground_by_apps =
- F.EnvApps.create
- (Context.Queue.pp ~sep:Fmt.semi Ground.pp)
- "Quantifier.Trigger.ground_by_apps" Context.Queue.create
+ F.EnvApps.create (Context.Queue.pp ~sep:Fmt.semi Ground.pp)
+ "Quantifier.Trigger.ground_by_apps" (fun c _ -> Context.Queue.create c)
module EnvTy = Datastructure.Memo (Ground.Ty)
let env_node_by_ty =
- EnvTy.create
- (Context.Queue.pp ~sep:Fmt.semi Node.pp)
- "Quantifier.Trigger.node_by_ty" Context.Queue.create
+ EnvTy.create (Context.Queue.pp ~sep:Fmt.semi Node.pp)
+ "Quantifier.Trigger.node_by_ty" (fun c _ -> Context.Queue.create c)
let match_any_term d (p : t) : Ground.Subst.S.t =
Debug.dprintf2 debug "[Quant] matching any for %a" pp p;
diff --git a/src_colibri2/theories/quantifier/pattern.mli b/src_colibri2/theories/quantifier/pattern.mli
index e68c6ef09566ef2727fae4d4ccd67a02c32ba0b9..c8e528bfb03dc584542b9c4b59f1c95bc6f16049 100644
--- a/src_colibri2/theories/quantifier/pattern.mli
+++ b/src_colibri2/theories/quantifier/pattern.mli
@@ -43,7 +43,7 @@ val get_pps : t -> PP.t list Term.Var.M.t
val env_ground_by_apps : Ground.t Context.Queue.t F.EnvApps.t
(** The set of ground terms sorted by their top function *)
-module EnvTy : Datastructure.Sig3 with type key := Ground.Ty.t
+module EnvTy : Datastructure.Memo with type key := Ground.Ty.t
val env_node_by_ty : Node.t Context.Queue.t EnvTy.t
(** The set of nodes sorted by their type. A node can have multiple types *)
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index f0750206a5e545c09fac03a3a850c693e6cd98ce..15da41554e9a460f278dd02bcbc56a621fc2b22e 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -69,12 +69,12 @@ let find_new_event d n (info : Info.t) n' (info' : Info.t) =
symmetric aux acc n info n' info'
in
let do_pt f_pos q acc =
- let aux acc _ info1 _ info2 =
+ let aux acc n info1 n' _ =
match F_Pos.M.find_opt f_pos info1.Info.parents with
| Some _ ->
Context.Queue.fold
(fun acc (vty, ip) ->
- let substs_by info =
+ let substs_by n0 =
let match_ty (acc : Ground.Subst.S.t) ty : Ground.Subst.S.t =
Ground.Subst.S.union
(Pattern.match_ty Pattern.init ty vty)
@@ -82,20 +82,19 @@ let find_new_event d n (info : Info.t) n' (info' : Info.t) =
in
let substs =
Ground.Ty.S.fold_left match_ty Ground.Subst.S.empty
- info.Info.tys
+ (Ground.tys d n0)
in
substs
in
- let substs2 = substs_by info2 in
+ let substs2 = substs_by n in
let substs1 =
- if Equal.physical info1 info2 then Ground.Subst.S.empty
- else substs_by info1
+ if Node.equal n n' then Ground.Subst.S.empty else substs_by n'
in
if Ground.Subst.S.subset substs2 substs1 then acc
else (
Debug.dprintf6 debug_full "[Quant] PT %a %a found for %a"
F_Pos.pp f_pos Expr.Ty.pp vty Node.pp n;
- ip :: acc ))
+ ip :: acc))
acc q
| None -> acc
in
@@ -127,13 +126,13 @@ module Delayed_find_new_event = struct
let key =
Events.Dem.create_key
- ( module struct
+ (module struct
type d = Node.t * InvertedPath.t list
type t = unit
let name = "Quantifier.new_event"
- end )
+ end)
let delay = Events.Delayed_by 10
@@ -150,7 +149,7 @@ let () = Egraph.Wait.register_dem (module Delayed_find_new_event)
let () =
DomKind.register
- ( module struct
+ (module struct
type t = Info.t [@@deriving show]
let key = Info.dom
@@ -178,7 +177,7 @@ let () =
if not (List.is_empty ips) then
Egraph.register_delayed_event d Delayed_find_new_event.key
(repr, ips)
- end )
+ end)
let skolemize d (e : Ground.ClosedQuantifier.t) =
if not (Base.List.is_empty e.ty_vars) then
@@ -268,11 +267,7 @@ let add_info_on_ground_terms d thg =
in
List.iteri add_pc g.args;
merge_info res
- {
- Info.empty with
- apps = F.M.singleton g.app (Ground.S.singleton thg);
- tys = Ground.Ty.S.singleton g.ty;
- };
+ { Info.empty with apps = F.M.singleton g.app (Ground.S.singleton thg) };
Context.Queue.push (F.EnvApps.find Pattern.env_ground_by_apps d g.app) thg;
Context.Queue.push (Pattern.EnvTy.find Pattern.env_node_by_ty d g.ty) res;
(* Try pattern from the start *)
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index 1b74443536a74452d896a2472eada6e659409fc9..c2b9728ecdcc49691e121d162ac3867ec212a817 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -61,13 +61,13 @@ let compute_top_triggers (cq : Ground.ThClosedQuantifier.t) =
| [] -> acc
| a :: l ->
aux
- ( {
- pat = a;
- checks = other @ l @ pats_partial;
- form = cq;
- eager = true;
- }
- :: acc )
+ ({
+ pat = a;
+ checks = other @ l @ pats_partial;
+ form = cq;
+ eager = true;
+ }
+ :: acc)
(a :: other) l
in
aux [] [] pats_full
@@ -109,7 +109,7 @@ let compute_all_triggers (cq : Ground.ThClosedQuantifier.t) =
| None -> (pats, None)
| Some (sty, st) ->
let fv = (List.fold_left Expr.Ty.free_vars sty tyl, st) in
- (add t fv pats, union fv acc_fv) )
+ (add t fv pats, union fv acc_fv))
| Expr.Binder (_, _) -> (pats, None) (* todo *)
| Expr.Match (_, _) -> (pats, None)
(* todo *)
@@ -136,9 +136,8 @@ let compute_all_triggers (cq : Ground.ThClosedQuantifier.t) =
let env_vars = Datastructure.Queue.create pp "Quantifier.Trigger.vars"
let env_tri_by_apps =
- F.EnvApps.create
- (Context.Queue.pp ~sep:Fmt.semi pp)
- "Quantifier.Trigger.tri_by_apps" Context.Queue.create
+ F.EnvApps.create (Context.Queue.pp ~sep:Fmt.semi pp)
+ "Quantifier.Trigger.tri_by_apps" (fun c _ -> Context.Queue.create c)
let add_trigger d t =
match t.pat with
@@ -174,13 +173,13 @@ module Delayed_instantiation = struct
let key =
Events.Dem.create_key
- ( module struct
+ (module struct
type d = t * Ground.Subst.t
type t = unit
let name = "delayed_instantiation"
- end )
+ end)
let delay = Events.LastEffort 1
@@ -222,7 +221,7 @@ let instantiate d tri subst =
then instantiate_aux d tri subst
else (
Debug.dprintf0 debug "[Quant] Delayed";
- Egraph.register_delayed_event d Delayed_instantiation.key (tri, subst) )
+ Egraph.register_delayed_event d Delayed_instantiation.key (tri, subst))
let match_ d tri n =
Debug.dprintf4 debug "[Quant] match %a %a" pp tri Node.pp n;
diff --git a/src_colibri2/theories/bool/uninterp.ml b/src_colibri2/theories/quantifier/uninterp.ml
similarity index 62%
rename from src_colibri2/theories/bool/uninterp.ml
rename to src_colibri2/theories/quantifier/uninterp.ml
index ae18b0b4b5c91c699f7c5359413ab2fbe179957c..81c29343f3b6fdc636ec7a3b614c4d91fe3c5979 100644
--- a/src_colibri2/theories/bool/uninterp.ml
+++ b/src_colibri2/theories/quantifier/uninterp.ml
@@ -19,12 +19,12 @@
(*************************************************************************)
open Colibri2_popop_lib
-(* open Popop_stdlib *)
+open Popop_stdlib
open Colibri2_core
-let debug = Debug.register_info_flag
- ~desc:"for the uninterpreted function theory"
- "uninterp"
+(* let debug =
+ * Debug.register_info_flag ~desc:"for the uninterpreted function theory"
+ * "uninterp" *)
(* module Th = struct
* module T = struct
@@ -202,14 +202,158 @@ let debug = Debug.register_info_flag
*
* let () = Egraph.add_default_theory th_register *)
-let converter d (t:Ground.t) =
+(** uninterpreted sorts *)
+module USModel = struct
+ type usv = { id : DInt.t; ty : Ground.Ty.t }
+
+ module US = ValueKind.Register (struct
+ module T = struct
+ type t = usv = { id : DInt.t; ty : Ground.Ty.t }
+ [@@deriving eq, ord, hash]
+
+ let pp fmt v = Fmt.pf fmt "@us_%a_%i" Ground.Ty.pp v.ty v.id
+ end
+
+ include T
+ include MkDatatype (T)
+
+ let key =
+ ValueKind.create_key
+ (module struct
+ type nonrec t = t
+
+ let name = "US"
+ end)
+ end)
+
+ module H = Datastructure.Memo (Ground.Ty)
+ (** The value created for uninterpreted sorts *)
+
+ let create_value q ty =
+ US.nodevalue @@ US.index { id = Context.Queue.length q; ty }
+
+ (** The values are generated so we could just store the current id,
+ and pay the small cost of indexing *)
+ let env =
+ H.create (Context.Queue.pp Value.pp) "Uninterp.Model.env" (fun creator _ ->
+ Context.Queue.create creator)
+
+ let new_value d ty =
+ let q = H.find env d ty in
+ let v = create_value q ty in
+ Context.Queue.push q v;
+ (v, q)
+end
+
+let init_ty d =
+ Interp.Register.ty d (fun d ty ->
+ match ty with
+ | { app = { builtin = Dolmen_std.Expr.Base; _ } as sym; _ } -> (
+ match Ground.Ty.definition sym with
+ | Abstract ->
+ let _, q = USModel.new_value d ty in
+ Some (Interp.SeqLim.of_seq d (Context.Queue.of_seq q))
+ | _ -> None)
+ | _ -> None)
+
+module UFModel = struct
+ module FA = struct
+ module T = struct
+ let hash_fold_list = Base.hash_fold_list
+
+ type t = { tc : F.t; ta : Ground.Ty.t list } [@@deriving eq, ord, hash]
+
+ let pp fmt { tc; ta } =
+ Format.fprintf fmt "%a[%a]" F.pp tc
+ Fmt.(list ~sep:comma Ground.Ty.pp)
+ ta
+ end
+
+ include T
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype (T)
+ end
+
+ module HConst = Datastructure.Memo (FA)
+
+ module Values = struct
+ (** instantiated function symbol *)
+ module T = struct
+ let hash_fold_list = Base.hash_fold_list
+
+ type t = Value.t list [@@deriving eq, ord, hash]
+
+ let pp fmt l = Fmt.(list ~sep:comma Value.pp) fmt l
+ end
+
+ include T
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype (T)
+ end
+
+ module Hargs = Context.Hashtbl (Values)
+
+ let env =
+ HConst.create Fmt.nop "Uninterp.UFModel.env" (fun c _ -> Hargs.create c)
+
+ let find d (g : Ground.Term.t) lv =
+ let h = HConst.find env d { tc = g.app; ta = g.tyargs } in
+ Hargs.find_opt h lv
+
+ let set d (g : Ground.Term.t) lv v =
+ let h = HConst.find env d { tc = g.app; ta = g.tyargs } in
+ Hargs.set h lv v
+
+ let init, waiter =
+ Demon.Fast.register_simply ~delay:FixingModel
+ "Uninterp.UFModel.propagate_value"
+
+ let on_uninterpreted_domain d g =
+ let check_or_update g d _ =
+ let interp n = Option.get_exn (Egraph.get_value d n) in
+ let s = Ground.sem g in
+ let lv = List.map interp s.args in
+ let v = interp (Ground.node g) in
+ match find d s lv with
+ | Some v' -> if not (Value.equal v v') then Egraph.contradiction d
+ | None -> set d s lv v
+ in
+ let f d g = waiter.for_any_value d (Ground.node g) (check_or_update g) in
+ f d g
+
+ let init_attach_value d g =
+ Interp.TwoWatchLiteral.create d on_uninterpreted_domain g
+end
+
+module On_uninterpreted_domain = struct
+ (** For model fixing *)
+
+ let propagate = UFModel.on_uninterpreted_domain
+
+ let check d t =
+ let interp n = Option.get_exn (Egraph.get_value d n) in
+ let s = Ground.sem t in
+ let lv = List.map interp s.args in
+ let v = interp (Ground.node t) in
+ match UFModel.find d s lv with Some v' -> Value.equal v v' | None -> false
+end
+
+let init_check d =
+ Interp.Register.check d (fun d t ->
+ match Ground.sem t with
+ | { app = { builtin = Dolmen_std.Expr.Base; _ }; _ } ->
+ Some (On_uninterpreted_domain.check d t)
+ | _ -> None)
+
+let converter d (t : Ground.t) =
match Ground.sem t with
- | { app = {builtin = Dolmen_std.Expr.Base; _ }; args; _ } ->
- List.iter (Egraph.register d) args
+ | { app = { builtin = Dolmen_std.Expr.Base; _ }; args; _ } ->
+ List.iter (Egraph.register d) args;
+ UFModel.init_attach_value d t
| _ -> ()
let th_register env =
Ground.register_converter env converter;
- ()
+ init_check env;
+ init_ty env;
+ UFModel.init env
let () = Egraph.add_default_theory th_register
diff --git a/src_colibri2/theories/bool/uninterp.mli b/src_colibri2/theories/quantifier/uninterp.mli
similarity index 93%
rename from src_colibri2/theories/bool/uninterp.mli
rename to src_colibri2/theories/quantifier/uninterp.mli
index 9e80e4ffb453b83b1119c34bb1443b44f112f7f6..952f5027f455f345b23dc94a86afd6618e392910 100644
--- a/src_colibri2/theories/bool/uninterp.mli
+++ b/src_colibri2/theories/quantifier/uninterp.mli
@@ -50,3 +50,11 @@ open Colibri2_core
(* val app_fun: Node.t -> Node.t list -> Node.t *)
val th_register : Egraph.t -> unit
+
+module On_uninterpreted_domain : sig
+ (** For model fixing *)
+
+ val propagate : Egraph.t -> Ground.t -> unit
+
+ val check : Egraph.t -> Ground.t -> bool
+end