mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 11:15:43 -05:00
feat(cc): adapt to the new CC_view
This commit is contained in:
Simon Cruanes
parent
2a8eb0c166
commit
f17e689a3c
13 changed files with 19 additions and 669 deletions
32
src/cc/CC.ml
32
src/cc/CC.ml
|
|
@ -1,6 +1,6 @@
|
||||||
open Types_
|
open Types_
|
||||||
|
|
||||||
type view_as_cc = Term.t -> (Const.t, Term.t, Term.t Iter.t) View.t
|
type view_as_cc = Term.t -> (Const.t, Term.t, Term.t list) CC_view.t
|
||||||
|
|
||||||
type e_node = E_node.t
|
type e_node = E_node.t
|
||||||
(** A node of the congruence closure *)
|
(** A node of the congruence closure *)
|
||||||
|
|
@ -165,7 +165,7 @@ end
|
||||||
|
|
||||||
(* compute up-to-date signature *)
|
(* compute up-to-date signature *)
|
||||||
let update_sig (s : signature) : Signature.t =
|
let update_sig (s : signature) : Signature.t =
|
||||||
View.map_view s ~f_f:(fun x -> x) ~f_t:find_ ~f_ts:(List.map find_)
|
CC_view.map_view s ~f_f:(fun x -> x) ~f_t:find_ ~f_ts:(List.map find_)
|
||||||
|
|
||||||
(* find whether the given (parent) term corresponds to some signature
|
(* find whether the given (parent) term corresponds to some signature
|
||||||
in [signatures_] *)
|
in [signatures_] *)
|
||||||
|
|
@ -466,19 +466,19 @@ and compute_sig0 (self : t) (n : e_node) : Signature.t option =
|
||||||
| Eq (a, b) ->
|
| Eq (a, b) ->
|
||||||
let a = deref_sub a in
|
let a = deref_sub a in
|
||||||
let b = deref_sub b in
|
let b = deref_sub b in
|
||||||
return @@ View.Eq (a, b)
|
return @@ CC_view.Eq (a, b)
|
||||||
| Not u -> return @@ View.Not (deref_sub u)
|
| Not u -> return @@ CC_view.Not (deref_sub u)
|
||||||
| App_fun (f, args) ->
|
| App_fun (f, args) ->
|
||||||
let args = args |> Iter.map deref_sub |> Iter.to_list in
|
let args = List.map deref_sub args in
|
||||||
if args <> [] then
|
if args <> [] then
|
||||||
return @@ View.App_fun (f, args)
|
return @@ CC_view.App_fun (f, args)
|
||||||
else
|
else
|
||||||
None
|
None
|
||||||
| App_ho (f, a) ->
|
| App_ho (f, a) ->
|
||||||
let f = deref_sub f in
|
let f = deref_sub f in
|
||||||
let a = deref_sub a in
|
let a = deref_sub a in
|
||||||
return @@ View.App_ho (f, a)
|
return @@ CC_view.App_ho (f, a)
|
||||||
| If (a, b, c) -> return @@ View.If (deref_sub a, deref_sub b, deref_sub c)
|
| If (a, b, c) -> return @@ CC_view.If (deref_sub a, deref_sub b, deref_sub c)
|
||||||
|
|
||||||
let[@inline] add_term self t : e_node = add_term_rec_ self t
|
let[@inline] add_term self t : e_node = add_term_rec_ self t
|
||||||
let mem_term = mem
|
let mem_term = mem
|
||||||
|
|
@ -950,19 +950,9 @@ module Make (A : ARG) : BUILD = struct
|
||||||
create_ ?stat ?size tst proof ~view_as_cc:A.view_as_cc
|
create_ ?stat ?size tst proof ~view_as_cc:A.view_as_cc
|
||||||
end
|
end
|
||||||
|
|
||||||
module Default = struct
|
module Default = Make (Sidekick_core.Default_cc_view)
|
||||||
include Make (struct
|
|
||||||
let view_as_cc (t : Term.t) : _ View.t =
|
|
||||||
let f, args = Term.unfold_app t in
|
|
||||||
match Term.view f, args with
|
|
||||||
| _, [ _; t; u ] when Term.is_eq f -> View.Eq (t, u)
|
|
||||||
| _ ->
|
|
||||||
(match Term.view t with
|
|
||||||
| Term.E_app (f, a) -> View.App_ho (f, a)
|
|
||||||
| Term.E_const c -> View.App_fun (c, Iter.empty)
|
|
||||||
| _ -> View.Opaque t)
|
|
||||||
end)
|
|
||||||
end
|
|
||||||
|
|
||||||
let create (module A : ARG) ?stat ?size tst proof : t =
|
let create (module A : ARG) ?stat ?size tst proof : t =
|
||||||
create_ ?stat ?size tst proof ~view_as_cc:A.view_as_cc
|
create_ ?stat ?size tst proof ~view_as_cc:A.view_as_cc
|
||||||
|
|
||||||
|
let create_default = Default.create
|
||||||
|
|
|
||||||
|
|
@ -255,7 +255,7 @@ val pop_levels : t -> int -> unit
|
||||||
val get_model : t -> E_node.t Iter.t Iter.t
|
val get_model : t -> E_node.t Iter.t Iter.t
|
||||||
(** get all the equivalence classes so they can be merged in the model *)
|
(** get all the equivalence classes so they can be merged in the model *)
|
||||||
|
|
||||||
type view_as_cc = Term.t -> (Const.t, Term.t, Term.t Iter.t) View.t
|
type view_as_cc = Term.t -> (Const.t, Term.t, Term.t list) CC_view.t
|
||||||
|
|
||||||
(** Arguments to a congruence closure's implementation *)
|
(** Arguments to a congruence closure's implementation *)
|
||||||
module type ARG = sig
|
module type ARG = sig
|
||||||
|
|
@ -275,7 +275,6 @@ module type BUILD = sig
|
||||||
end
|
end
|
||||||
|
|
||||||
module Make (_ : ARG) : BUILD
|
module Make (_ : ARG) : BUILD
|
||||||
module Default : BUILD
|
|
||||||
|
|
||||||
val create :
|
val create :
|
||||||
(module ARG) ->
|
(module ARG) ->
|
||||||
|
|
@ -291,6 +290,10 @@ val create :
|
||||||
as well.
|
as well.
|
||||||
*)
|
*)
|
||||||
|
|
||||||
|
val create_default :
|
||||||
|
?stat:Stat.t -> ?size:[ `Small | `Big ] -> Term.store -> Proof_trace.t -> t
|
||||||
|
(** Same as {!create} but with the default CC view *)
|
||||||
|
|
||||||
(**/**)
|
(**/**)
|
||||||
|
|
||||||
module Debug_ : sig
|
module Debug_ : sig
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,3 @@
|
||||||
open Sidekick_core
|
|
||||||
module View = View
|
module View = View
|
||||||
module E_node = E_node
|
module E_node = E_node
|
||||||
module Expl = Expl
|
module Expl = Expl
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,5 @@
|
||||||
(** Congruence Closure Implementation *)
|
(** Congruence Closure Implementation *)
|
||||||
|
|
||||||
open Sidekick_core
|
|
||||||
|
|
||||||
module type DYN_MONOID_PLUGIN = Sigs_plugin.DYN_MONOID_PLUGIN
|
module type DYN_MONOID_PLUGIN = Sigs_plugin.DYN_MONOID_PLUGIN
|
||||||
module type MONOID_PLUGIN_ARG = Sigs_plugin.MONOID_PLUGIN_ARG
|
module type MONOID_PLUGIN_ARG = Sigs_plugin.MONOID_PLUGIN_ARG
|
||||||
module type MONOID_PLUGIN_BUILDER = Sigs_plugin.MONOID_PLUGIN_BUILDER
|
module type MONOID_PLUGIN_BUILDER = Sigs_plugin.MONOID_PLUGIN_BUILDER
|
||||||
|
|
|
||||||
|
|
@ -1,337 +0,0 @@
|
||||||
open Sidekick_core
|
|
||||||
module CC_view = Sidekick_cc.View
|
|
||||||
|
|
||||||
module type ARG = sig
|
|
||||||
val view_as_cc : Term.t -> (Const.t, Term.t, Term.t Iter.t) CC_view.t
|
|
||||||
end
|
|
||||||
|
|
||||||
module type S = sig
|
|
||||||
type t
|
|
||||||
|
|
||||||
val create : Term.store -> t
|
|
||||||
val clear : t -> unit
|
|
||||||
val add_lit : t -> Term.t -> bool -> unit
|
|
||||||
val check_sat : t -> bool
|
|
||||||
val classes : t -> Term.t Iter.t Iter.t
|
|
||||||
end
|
|
||||||
|
|
||||||
module Make (A : ARG) = struct
|
|
||||||
open CC_view
|
|
||||||
module T = Term
|
|
||||||
module T_tbl = Term.Tbl
|
|
||||||
|
|
||||||
type node = {
|
|
||||||
n_t: Term.t;
|
|
||||||
mutable n_next: node; (* next in class *)
|
|
||||||
mutable n_size: int; (* size of class *)
|
|
||||||
mutable n_parents: node list;
|
|
||||||
mutable n_root: node; (* root of the class *)
|
|
||||||
}
|
|
||||||
|
|
||||||
type signature = (Const.t, node, node list) CC_view.t
|
|
||||||
|
|
||||||
module Node = struct
|
|
||||||
type t = node
|
|
||||||
|
|
||||||
let[@inline] equal (n1 : t) n2 = T.equal n1.n_t n2.n_t
|
|
||||||
let[@inline] hash (n : t) = T.hash n.n_t
|
|
||||||
let[@inline] size (n : t) = n.n_size
|
|
||||||
let[@inline] is_root n = n == n.n_root
|
|
||||||
let[@inline] root n = n.n_root
|
|
||||||
let[@inline] term n = n.n_t
|
|
||||||
let pp out n = T.pp_debug out n.n_t
|
|
||||||
let add_parent (self : t) ~p : unit = self.n_parents <- p :: self.n_parents
|
|
||||||
|
|
||||||
let make (t : T.t) : t =
|
|
||||||
let rec n =
|
|
||||||
{ n_t = t; n_size = 1; n_next = n; n_parents = []; n_root = n }
|
|
||||||
in
|
|
||||||
n
|
|
||||||
|
|
||||||
(* iterate over the class *)
|
|
||||||
let iter_cls (n0 : t) f : unit =
|
|
||||||
let rec aux n =
|
|
||||||
f n;
|
|
||||||
let n' = n.n_next in
|
|
||||||
if equal n' n0 then
|
|
||||||
()
|
|
||||||
else
|
|
||||||
aux n'
|
|
||||||
in
|
|
||||||
aux n0
|
|
||||||
end
|
|
||||||
|
|
||||||
module Signature = struct
|
|
||||||
type t = signature
|
|
||||||
|
|
||||||
let equal (s1 : t) s2 : bool =
|
|
||||||
match s1, s2 with
|
|
||||||
| Bool b1, Bool b2 -> b1 = b2
|
|
||||||
| App_fun (f1, []), App_fun (f2, []) -> Const.equal f1 f2
|
|
||||||
| App_fun (f1, l1), App_fun (f2, l2) ->
|
|
||||||
Const.equal f1 f2 && CCList.equal Node.equal l1 l2
|
|
||||||
| App_ho (f1, a1), App_ho (f2, a2) -> Node.equal f1 f2 && Node.equal a1 a2
|
|
||||||
| Not n1, Not n2 -> Node.equal n1 n2
|
|
||||||
| If (a1, b1, c1), If (a2, b2, c2) ->
|
|
||||||
Node.equal a1 a2 && Node.equal b1 b2 && Node.equal c1 c2
|
|
||||||
| Eq (a1, b1), Eq (a2, b2) -> Node.equal a1 a2 && Node.equal b1 b2
|
|
||||||
| Opaque u1, Opaque u2 -> Node.equal u1 u2
|
|
||||||
| Bool _, _
|
|
||||||
| App_fun _, _
|
|
||||||
| App_ho _, _
|
|
||||||
| If _, _
|
|
||||||
| Eq _, _
|
|
||||||
| Opaque _, _
|
|
||||||
| Not _, _ ->
|
|
||||||
false
|
|
||||||
|
|
||||||
let hash (s : t) : int =
|
|
||||||
let module H = CCHash in
|
|
||||||
match s with
|
|
||||||
| Bool b -> H.combine2 10 (H.bool b)
|
|
||||||
| App_fun (f, l) -> H.combine3 20 (Const.hash f) (H.list Node.hash l)
|
|
||||||
| App_ho (f, a) -> H.combine3 30 (Node.hash f) (Node.hash a)
|
|
||||||
| Eq (a, b) -> H.combine3 40 (Node.hash a) (Node.hash b)
|
|
||||||
| Opaque u -> H.combine2 50 (Node.hash u)
|
|
||||||
| If (a, b, c) -> H.combine4 60 (Node.hash a) (Node.hash b) (Node.hash c)
|
|
||||||
| Not u -> H.combine2 70 (Node.hash u)
|
|
||||||
|
|
||||||
let pp out = function
|
|
||||||
| Bool b -> Fmt.bool out b
|
|
||||||
| App_fun (f, []) -> Const.pp out f
|
|
||||||
| App_fun (f, l) ->
|
|
||||||
Fmt.fprintf out "(@[%a@ %a@])" Const.pp f (Util.pp_list Node.pp) l
|
|
||||||
| App_ho (f, a) -> Fmt.fprintf out "(@[%a@ %a@])" Node.pp f Node.pp a
|
|
||||||
| Opaque t -> Node.pp out t
|
|
||||||
| Not u -> Fmt.fprintf out "(@[not@ %a@])" Node.pp u
|
|
||||||
| Eq (a, b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" Node.pp a Node.pp b
|
|
||||||
| If (a, b, c) ->
|
|
||||||
Fmt.fprintf out "(@[ite@ %a@ %a@ %a@])" Node.pp a Node.pp b Node.pp c
|
|
||||||
end
|
|
||||||
|
|
||||||
module Sig_tbl = CCHashtbl.Make (Signature)
|
|
||||||
|
|
||||||
type t = {
|
|
||||||
mutable ok: bool; (* unsat? *)
|
|
||||||
tbl: node T_tbl.t;
|
|
||||||
sig_tbl: node Sig_tbl.t;
|
|
||||||
mutable combine: (node * node) list;
|
|
||||||
mutable pending: node list; (* refresh signature *)
|
|
||||||
true_: node;
|
|
||||||
false_: node;
|
|
||||||
}
|
|
||||||
|
|
||||||
let create tst : t =
|
|
||||||
let true_ = Term.true_ tst in
|
|
||||||
let false_ = Term.false_ tst in
|
|
||||||
let self =
|
|
||||||
{
|
|
||||||
ok = true;
|
|
||||||
tbl = T_tbl.create 128;
|
|
||||||
sig_tbl = Sig_tbl.create 128;
|
|
||||||
combine = [];
|
|
||||||
pending = [];
|
|
||||||
true_ = Node.make true_;
|
|
||||||
false_ = Node.make false_;
|
|
||||||
}
|
|
||||||
in
|
|
||||||
T_tbl.add self.tbl true_ self.true_;
|
|
||||||
T_tbl.add self.tbl false_ self.false_;
|
|
||||||
self
|
|
||||||
|
|
||||||
let clear (self : t) : unit =
|
|
||||||
let { ok = _; tbl; sig_tbl; pending = _; combine = _; true_; false_ } =
|
|
||||||
self
|
|
||||||
in
|
|
||||||
self.ok <- true;
|
|
||||||
self.pending <- [];
|
|
||||||
self.combine <- [];
|
|
||||||
T_tbl.clear tbl;
|
|
||||||
Sig_tbl.clear sig_tbl;
|
|
||||||
T_tbl.add tbl true_.n_t true_;
|
|
||||||
T_tbl.add tbl false_.n_t false_;
|
|
||||||
()
|
|
||||||
|
|
||||||
let sub_ t k : unit =
|
|
||||||
match A.view_as_cc t with
|
|
||||||
| Bool _ | Opaque _ -> ()
|
|
||||||
| App_fun (_, args) -> args k
|
|
||||||
| App_ho (f, a) ->
|
|
||||||
k f;
|
|
||||||
k a
|
|
||||||
| Eq (a, b) ->
|
|
||||||
k a;
|
|
||||||
k b
|
|
||||||
| Not u -> k u
|
|
||||||
| If (a, b, c) ->
|
|
||||||
k a;
|
|
||||||
k b;
|
|
||||||
k c
|
|
||||||
|
|
||||||
let rec add_t (self : t) (t : Term.t) : node =
|
|
||||||
match T_tbl.find self.tbl t with
|
|
||||||
| n -> n
|
|
||||||
| exception Not_found ->
|
|
||||||
let node = Node.make t in
|
|
||||||
T_tbl.add self.tbl t node;
|
|
||||||
(* add sub-terms, and add [t] to their parent list *)
|
|
||||||
sub_ t (fun u ->
|
|
||||||
let n_u = Node.root @@ add_t self u in
|
|
||||||
Node.add_parent n_u ~p:node);
|
|
||||||
(* need to compute signature *)
|
|
||||||
self.pending <- node :: self.pending;
|
|
||||||
node
|
|
||||||
|
|
||||||
let find_t_ (self : t) (t : Term.t) : node =
|
|
||||||
try T_tbl.find self.tbl t |> Node.root
|
|
||||||
with Not_found ->
|
|
||||||
Error.errorf "mini-cc.find_t: no node for %a" T.pp_debug t
|
|
||||||
|
|
||||||
exception E_unsat
|
|
||||||
|
|
||||||
let compute_sig (self : t) (n : node) : Signature.t option =
|
|
||||||
let[@inline] return x = Some x in
|
|
||||||
match A.view_as_cc n.n_t with
|
|
||||||
| Bool _ | Opaque _ -> None
|
|
||||||
| Eq (a, b) ->
|
|
||||||
let a = find_t_ self a in
|
|
||||||
let b = find_t_ self b in
|
|
||||||
return @@ Eq (a, b)
|
|
||||||
| Not u -> return @@ Not (find_t_ self u)
|
|
||||||
| App_fun (f, args) ->
|
|
||||||
let args = args |> Iter.map (find_t_ self) |> Iter.to_list in
|
|
||||||
if args <> [] then
|
|
||||||
return @@ App_fun (f, args)
|
|
||||||
else
|
|
||||||
None
|
|
||||||
| App_ho (f, a) ->
|
|
||||||
let f = find_t_ self f in
|
|
||||||
let a = find_t_ self a in
|
|
||||||
return @@ App_ho (f, a)
|
|
||||||
| If (a, b, c) ->
|
|
||||||
return @@ If (find_t_ self a, find_t_ self b, find_t_ self c)
|
|
||||||
|
|
||||||
let update_sig_ (self : t) (n : node) : unit =
|
|
||||||
match compute_sig self n with
|
|
||||||
| None -> ()
|
|
||||||
| Some (Eq (a, b)) ->
|
|
||||||
if Node.equal a b then (
|
|
||||||
(* reduce to [true] *)
|
|
||||||
let n2 = self.true_ in
|
|
||||||
Log.debugf 5 (fun k ->
|
|
||||||
k "(@[mini-cc.congruence-by-eq@ %a@ %a@])" Node.pp n Node.pp n2);
|
|
||||||
self.combine <- (n, n2) :: self.combine
|
|
||||||
)
|
|
||||||
| Some (Not u) when Node.equal u self.true_ ->
|
|
||||||
self.combine <- (n, self.false_) :: self.combine
|
|
||||||
| Some (Not u) when Node.equal u self.false_ ->
|
|
||||||
self.combine <- (n, self.true_) :: self.combine
|
|
||||||
| Some (If (a, b, _)) when Node.equal a self.true_ ->
|
|
||||||
self.combine <- (n, b) :: self.combine
|
|
||||||
| Some (If (a, _, c)) when Node.equal a self.false_ ->
|
|
||||||
self.combine <- (n, c) :: self.combine
|
|
||||||
| Some s ->
|
|
||||||
Log.debugf 5 (fun k -> k "(@[mini-cc.update-sig@ %a@])" Signature.pp s);
|
|
||||||
(match Sig_tbl.find self.sig_tbl s with
|
|
||||||
| n2 when Node.equal n n2 -> ()
|
|
||||||
| n2 ->
|
|
||||||
(* collision, merge *)
|
|
||||||
Log.debugf 5 (fun k ->
|
|
||||||
k "(@[mini-cc.congruence-by-sig@ %a@ %a@])" Node.pp n Node.pp n2);
|
|
||||||
self.combine <- (n, n2) :: self.combine
|
|
||||||
| exception Not_found -> Sig_tbl.add self.sig_tbl s n)
|
|
||||||
|
|
||||||
let[@inline] is_bool self n =
|
|
||||||
Node.equal self.true_ n || Node.equal self.false_ n
|
|
||||||
|
|
||||||
(* merge the two classes *)
|
|
||||||
let merge_ self n1 n2 : unit =
|
|
||||||
let n1 = Node.root n1 in
|
|
||||||
let n2 = Node.root n2 in
|
|
||||||
if not @@ Node.equal n1 n2 then (
|
|
||||||
(* merge into largest class, or into a boolean *)
|
|
||||||
let n1, n2 =
|
|
||||||
if is_bool self n1 then
|
|
||||||
n1, n2
|
|
||||||
else if is_bool self n2 then
|
|
||||||
n2, n1
|
|
||||||
else if Node.size n1 > Node.size n2 then
|
|
||||||
n1, n2
|
|
||||||
else
|
|
||||||
n2, n1
|
|
||||||
in
|
|
||||||
Log.debugf 5 (fun k ->
|
|
||||||
k "(@[mini-cc.merge@ :into %a@ %a@])" Node.pp n1 Node.pp n2);
|
|
||||||
|
|
||||||
if is_bool self n1 && is_bool self n2 then (
|
|
||||||
Log.debugf 5 (fun k -> k "(mini-cc.conflict.merge-true-false)");
|
|
||||||
self.ok <- false;
|
|
||||||
raise E_unsat
|
|
||||||
);
|
|
||||||
|
|
||||||
self.pending <- List.rev_append n2.n_parents self.pending;
|
|
||||||
|
|
||||||
(* will change signature *)
|
|
||||||
|
|
||||||
(* merge parent lists *)
|
|
||||||
n1.n_parents <- List.rev_append n2.n_parents n1.n_parents;
|
|
||||||
n1.n_size <- n2.n_size + n1.n_size;
|
|
||||||
|
|
||||||
(* update root pointer in [n2.class] *)
|
|
||||||
Node.iter_cls n2 (fun n -> n.n_root <- n1);
|
|
||||||
|
|
||||||
(* merge classes [next] pointers *)
|
|
||||||
let n1_next = n1.n_next in
|
|
||||||
n1.n_next <- n2.n_next;
|
|
||||||
n2.n_next <- n1_next
|
|
||||||
)
|
|
||||||
|
|
||||||
let[@inline] check_ok_ self = if not self.ok then raise_notrace E_unsat
|
|
||||||
|
|
||||||
(* fixpoint of the congruence closure *)
|
|
||||||
let fixpoint (self : t) : unit =
|
|
||||||
while not (CCList.is_empty self.pending && CCList.is_empty self.combine) do
|
|
||||||
check_ok_ self;
|
|
||||||
while not @@ CCList.is_empty self.pending do
|
|
||||||
let n = List.hd self.pending in
|
|
||||||
self.pending <- List.tl self.pending;
|
|
||||||
update_sig_ self n
|
|
||||||
done;
|
|
||||||
while not @@ CCList.is_empty self.combine do
|
|
||||||
let n1, n2 = List.hd self.combine in
|
|
||||||
self.combine <- List.tl self.combine;
|
|
||||||
merge_ self n1 n2
|
|
||||||
done
|
|
||||||
done
|
|
||||||
|
|
||||||
(* API *)
|
|
||||||
|
|
||||||
let add_lit (self : t) (p : T.t) (sign : bool) : unit =
|
|
||||||
match A.view_as_cc p with
|
|
||||||
| Eq (t1, t2) when sign ->
|
|
||||||
let n1 = add_t self t1 in
|
|
||||||
let n2 = add_t self t2 in
|
|
||||||
self.combine <- (n1, n2) :: self.combine
|
|
||||||
| _ ->
|
|
||||||
(* just merge with true/false *)
|
|
||||||
let n = add_t self p in
|
|
||||||
let n2 =
|
|
||||||
if sign then
|
|
||||||
self.true_
|
|
||||||
else
|
|
||||||
self.false_
|
|
||||||
in
|
|
||||||
self.combine <- (n, n2) :: self.combine
|
|
||||||
|
|
||||||
let check_sat (self : t) : bool =
|
|
||||||
try
|
|
||||||
fixpoint self;
|
|
||||||
true
|
|
||||||
with E_unsat ->
|
|
||||||
self.ok <- false;
|
|
||||||
false
|
|
||||||
|
|
||||||
let classes self : _ Iter.t =
|
|
||||||
T_tbl.values self.tbl |> Iter.filter Node.is_root
|
|
||||||
|> Iter.map (fun n -> Node.iter_cls n |> Iter.map Node.term)
|
|
||||||
end
|
|
||||||
|
|
@ -1,44 +0,0 @@
|
||||||
(** Mini congruence closure
|
|
||||||
|
|
||||||
This implementation is as simple as possible, and doesn't provide
|
|
||||||
backtracking, theories, or explanations.
|
|
||||||
It just decides the satisfiability of a set of (dis)equations.
|
|
||||||
*)
|
|
||||||
|
|
||||||
open Sidekick_core
|
|
||||||
module CC_view = Sidekick_cc.View
|
|
||||||
|
|
||||||
(** Argument for the functor {!Make}
|
|
||||||
|
|
||||||
It only requires a Term.t structure, and a congruence-oriented view. *)
|
|
||||||
module type ARG = sig
|
|
||||||
val view_as_cc : Term.t -> (Const.t, Term.t, Term.t Iter.t) CC_view.t
|
|
||||||
end
|
|
||||||
|
|
||||||
(** Main signature for an instance of the mini congruence closure *)
|
|
||||||
module type S = sig
|
|
||||||
type t
|
|
||||||
(** An instance of the congruence closure. Mutable *)
|
|
||||||
|
|
||||||
val create : Term.store -> t
|
|
||||||
(** New instance *)
|
|
||||||
|
|
||||||
val clear : t -> unit
|
|
||||||
(** Fully reset the congruence closure's state *)
|
|
||||||
|
|
||||||
val add_lit : t -> Term.t -> bool -> unit
|
|
||||||
(** [add_lit cc p sign] asserts that [p] is true if [sign],
|
|
||||||
or [p] is false if [not sign]. If [p] is an equation and [sign]
|
|
||||||
is [true], this adds a new equation to the congruence relation. *)
|
|
||||||
|
|
||||||
val check_sat : t -> bool
|
|
||||||
(** [check_sat cc] returns [true] if the current state is satisfiable, [false]
|
|
||||||
if it's unsatisfiable. *)
|
|
||||||
|
|
||||||
val classes : t -> Term.t Iter.t Iter.t
|
|
||||||
(** Traverse the set of classes in the congruence closure.
|
|
||||||
This should be called only if {!check} returned [Sat]. *)
|
|
||||||
end
|
|
||||||
|
|
||||||
(** Instantiate the congruence closure for the given Term.t structure. *)
|
|
||||||
module Make (_ : ARG) : S
|
|
||||||
|
|
@ -1,5 +0,0 @@
|
||||||
(library
|
|
||||||
(name Sidekick_mini_cc)
|
|
||||||
(public_name sidekick.mini-cc)
|
|
||||||
(libraries containers iter sidekick.cc sidekick.core sidekick.util)
|
|
||||||
(flags :standard -warn-error -a+8 -w -32 -open Sidekick_util))
|
|
||||||
|
|
@ -1,4 +0,0 @@
|
||||||
(library
|
|
||||||
(name sidekick_test_minicc)
|
|
||||||
(libraries sidekick.mini-cc sidekick-base alcotest)
|
|
||||||
(flags :standard -warn-error -a+8))
|
|
||||||
|
|
@ -1,179 +0,0 @@
|
||||||
open! Sidekick_base
|
|
||||||
module A = Alcotest
|
|
||||||
|
|
||||||
module CC = Sidekick_mini_cc.Make (struct
|
|
||||||
module T = Sidekick_base.Solver_arg
|
|
||||||
|
|
||||||
let view_as_cc = Term.cc_view
|
|
||||||
end)
|
|
||||||
|
|
||||||
module Setup () = struct
|
|
||||||
let tst = Term.create ()
|
|
||||||
let ( @-> ) l ret = Ty.Fun.mk l ret
|
|
||||||
let ty_i = Ty.atomic_uninterpreted (ID.make "$i")
|
|
||||||
let ty_bool = Ty.bool ()
|
|
||||||
let fun_f = Fun.mk_undef (ID.make "f") ([ ty_i ] @-> ty_i)
|
|
||||||
let fun_g = Fun.mk_undef (ID.make "g") ([ ty_i; ty_i ] @-> ty_i)
|
|
||||||
let fun_p = Fun.mk_undef (ID.make "p") ([ ty_i ] @-> ty_bool)
|
|
||||||
let fun_a = Fun.mk_undef_const (ID.make "a") ty_i
|
|
||||||
let fun_b = Fun.mk_undef_const (ID.make "b") ty_i
|
|
||||||
let fun_c = Fun.mk_undef_const (ID.make "c") ty_i
|
|
||||||
let fun_d1 = Fun.mk_undef_const (ID.make "d1") ty_i
|
|
||||||
let fun_d2 = Fun.mk_undef_const (ID.make "d2") ty_i
|
|
||||||
let true_ = Term.true_ tst
|
|
||||||
let false_ = Term.false_ tst
|
|
||||||
let const c = Term.const tst c
|
|
||||||
let app_a f l = Term.app_fun tst f l
|
|
||||||
let app_l f l = Term.app_fun tst f (CCArray.of_list l)
|
|
||||||
let not_ x = Term.not_ tst x
|
|
||||||
let eq a b = Term.eq tst a b
|
|
||||||
let neq a b = Term.not_ tst (eq a b)
|
|
||||||
let ite a b c = Term.ite tst a b c
|
|
||||||
let a = const fun_a
|
|
||||||
let b = const fun_b
|
|
||||||
let c = const fun_c
|
|
||||||
let d1 = const fun_d1
|
|
||||||
let d2 = const fun_d2
|
|
||||||
let f t1 = app_l fun_f [ t1 ]
|
|
||||||
let g t1 t2 = app_l fun_g [ t1; t2 ]
|
|
||||||
let p t1 = app_l fun_p [ t1 ]
|
|
||||||
end
|
|
||||||
|
|
||||||
let l : unit Alcotest.test_case list ref = ref []
|
|
||||||
let mk_test name f = l := (name, `Quick, f) :: !l
|
|
||||||
|
|
||||||
let () =
|
|
||||||
mk_test "test_p_a_b" @@ fun () ->
|
|
||||||
let module S = Setup () in
|
|
||||||
let cc = CC.create S.tst in
|
|
||||||
CC.add_lit cc S.(p a) true;
|
|
||||||
CC.add_lit cc S.(p b) false;
|
|
||||||
A.(check bool) "is-sat" (CC.check_sat cc) true;
|
|
||||||
CC.add_lit cc S.(eq a b) true;
|
|
||||||
A.(check bool) "is-unsat" (CC.check_sat cc) false;
|
|
||||||
()
|
|
||||||
|
|
||||||
let () =
|
|
||||||
mk_test "test_p_a_b_2" @@ fun () ->
|
|
||||||
let module S = Setup () in
|
|
||||||
let cc = CC.create S.tst in
|
|
||||||
CC.add_lit cc S.(p a) true;
|
|
||||||
CC.add_lit cc S.(not_ @@ p b) true;
|
|
||||||
A.(check bool) "is-sat" (CC.check_sat cc) true;
|
|
||||||
CC.add_lit cc S.(eq a b) true;
|
|
||||||
A.(check bool) "is-unsat" (CC.check_sat cc) false;
|
|
||||||
()
|
|
||||||
|
|
||||||
let () =
|
|
||||||
mk_test "test_f_f_f_a" @@ fun () ->
|
|
||||||
let module S = Setup () in
|
|
||||||
let cc = CC.create S.tst in
|
|
||||||
CC.add_lit cc S.(neq a (f (f (f (f (f (f a))))))) true;
|
|
||||||
A.(check bool) "is-sat" (CC.check_sat cc) true;
|
|
||||||
CC.add_lit cc S.(eq a (f a)) true;
|
|
||||||
A.(check bool) "is-unsat" (CC.check_sat cc) false;
|
|
||||||
()
|
|
||||||
|
|
||||||
let () =
|
|
||||||
mk_test "test_repeated_f_f_f_a" @@ fun () ->
|
|
||||||
let module S = Setup () in
|
|
||||||
let cc = CC.create S.tst in
|
|
||||||
for _i = 0 to 10 do
|
|
||||||
CC.add_lit cc S.(neq a (f (f (f (f (f (f a))))))) true;
|
|
||||||
A.(check bool) "is-sat" (CC.check_sat cc) true;
|
|
||||||
CC.add_lit cc S.(eq a (f a)) true;
|
|
||||||
A.(check bool) "is-unsat" (CC.check_sat cc) false;
|
|
||||||
CC.clear cc
|
|
||||||
done;
|
|
||||||
()
|
|
||||||
|
|
||||||
let () =
|
|
||||||
mk_test "test_trans" @@ fun () ->
|
|
||||||
let module S = Setup () in
|
|
||||||
let cc = CC.create S.tst in
|
|
||||||
CC.add_lit cc S.(eq a b) true;
|
|
||||||
CC.add_lit cc S.(eq b c) true;
|
|
||||||
A.(check bool) "is-sat" (CC.check_sat cc) true;
|
|
||||||
CC.add_lit cc S.(neq (f a) (f c)) true;
|
|
||||||
A.(check bool) "is-unsat" (CC.check_sat cc) false;
|
|
||||||
()
|
|
||||||
|
|
||||||
let () =
|
|
||||||
mk_test "test_true" @@ fun () ->
|
|
||||||
let module S = Setup () in
|
|
||||||
let cc = CC.create S.tst in
|
|
||||||
CC.add_lit cc S.true_ true;
|
|
||||||
A.(check bool) "is-sat" (CC.check_sat cc) true;
|
|
||||||
CC.add_lit cc S.false_ true;
|
|
||||||
A.(check bool) "is-unsat" (CC.check_sat cc) false;
|
|
||||||
()
|
|
||||||
|
|
||||||
let () =
|
|
||||||
mk_test "test_repeated_true" @@ fun () ->
|
|
||||||
let module S = Setup () in
|
|
||||||
let cc = CC.create S.tst in
|
|
||||||
for _i = 0 to 10 do
|
|
||||||
CC.add_lit cc S.true_ true;
|
|
||||||
A.(check bool) "is-sat" (CC.check_sat cc) true;
|
|
||||||
CC.add_lit cc S.false_ true;
|
|
||||||
A.(check bool) "is-unsat" (CC.check_sat cc) false;
|
|
||||||
CC.clear cc
|
|
||||||
done;
|
|
||||||
()
|
|
||||||
|
|
||||||
let () =
|
|
||||||
mk_test "test_false" @@ fun () ->
|
|
||||||
let module S = Setup () in
|
|
||||||
let cc = CC.create S.tst in
|
|
||||||
CC.add_lit cc S.false_ true;
|
|
||||||
A.(check bool) "is-unsat" (CC.check_sat cc) false;
|
|
||||||
()
|
|
||||||
|
|
||||||
let () =
|
|
||||||
mk_test "test_not_false" @@ fun () ->
|
|
||||||
let module S = Setup () in
|
|
||||||
let cc = CC.create S.tst in
|
|
||||||
CC.add_lit cc S.(not_ false_) true;
|
|
||||||
A.(check bool) "is-sat" (CC.check_sat cc) true;
|
|
||||||
()
|
|
||||||
|
|
||||||
let () =
|
|
||||||
mk_test "test_ite" @@ fun () ->
|
|
||||||
let module S = Setup () in
|
|
||||||
let cc = CC.create S.tst in
|
|
||||||
for _i = 0 to 10 do
|
|
||||||
CC.add_lit cc S.(eq a b) true;
|
|
||||||
CC.add_lit cc S.(p (ite (eq a c) d1 d2)) true;
|
|
||||||
CC.add_lit cc S.(not_ (p d1)) true;
|
|
||||||
CC.add_lit cc S.(p d2) true;
|
|
||||||
A.(check bool) "is-sat" (CC.check_sat cc) true;
|
|
||||||
CC.add_lit cc S.(eq b c) true;
|
|
||||||
(* force (p d1) *)
|
|
||||||
A.(check bool) "is-unsat" (CC.check_sat cc) false;
|
|
||||||
CC.clear cc
|
|
||||||
done;
|
|
||||||
()
|
|
||||||
|
|
||||||
(* from the following PO:
|
|
||||||
`cl (- a = (g a c)),
|
|
||||||
(- b = (g a c)),
|
|
||||||
(- c = (g c b)),
|
|
||||||
(- a = (g c c)),
|
|
||||||
(- (g c (g c b)) = (g (g c c) b)),
|
|
||||||
(+ (g a b) = (g a c))))`
|
|
||||||
*)
|
|
||||||
let () =
|
|
||||||
mk_test "test_reg_1" @@ fun () ->
|
|
||||||
let module S = Setup () in
|
|
||||||
let cc = CC.create S.tst in
|
|
||||||
CC.add_lit cc S.(eq a (g a c)) true;
|
|
||||||
CC.add_lit cc S.(eq b (g a c)) true;
|
|
||||||
CC.add_lit cc S.(eq c (g c b)) true;
|
|
||||||
CC.add_lit cc S.(eq a (g c c)) true;
|
|
||||||
CC.add_lit cc S.(eq (g c (g c b)) (g (g c c) b)) true;
|
|
||||||
CC.add_lit cc S.(eq (g a b) (g a c)) false;
|
|
||||||
(* goal *)
|
|
||||||
A.(check bool) "is-unsat" (CC.check_sat cc) false;
|
|
||||||
()
|
|
||||||
|
|
||||||
let tests = "mini-cc", List.rev !l
|
|
||||||
|
|
@ -1,13 +1,13 @@
|
||||||
(** A signature is a shallow term shape where immediate subterms
|
(** A signature is a shallow term shape where immediate subterms
|
||||||
are representative *)
|
are representative *)
|
||||||
|
|
||||||
open View
|
open Sidekick_core.CC_view
|
||||||
open Types_
|
open Types_
|
||||||
|
|
||||||
type t = signature
|
type t = signature
|
||||||
|
|
||||||
let equal (s1 : t) s2 : bool =
|
let equal (s1 : t) s2 : bool =
|
||||||
let open View in
|
let open CC_view in
|
||||||
match s1, s2 with
|
match s1, s2 with
|
||||||
| Bool b1, Bool b2 -> b1 = b2
|
| Bool b1, Bool b2 -> b1 = b2
|
||||||
| App_fun (f1, []), App_fun (f2, []) -> Const.equal f1 f2
|
| App_fun (f1, []), App_fun (f2, []) -> Const.equal f1 f2
|
||||||
|
|
|
||||||
|
|
@ -18,7 +18,7 @@ type e_node = {
|
||||||
An equivalence class is represented by its "root" element,
|
An equivalence class is represented by its "root" element,
|
||||||
the representative. *)
|
the representative. *)
|
||||||
|
|
||||||
and signature = (Const.t, e_node, e_node list) View.t
|
and signature = (Const.t, e_node, e_node list) CC_view.t
|
||||||
|
|
||||||
and explanation_forest_link =
|
and explanation_forest_link =
|
||||||
| FL_none
|
| FL_none
|
||||||
|
|
|
||||||
|
|
@ -1,38 +0,0 @@
|
||||||
type ('f, 't, 'ts) t =
|
|
||||||
| Bool of bool
|
|
||||||
| App_fun of 'f * 'ts
|
|
||||||
| App_ho of 't * 't
|
|
||||||
| If of 't * 't * 't
|
|
||||||
| Eq of 't * 't
|
|
||||||
| Not of 't
|
|
||||||
| Opaque of 't
|
|
||||||
(* do not enter *)
|
|
||||||
|
|
||||||
let map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t =
|
|
||||||
match v with
|
|
||||||
| Bool b -> Bool b
|
|
||||||
| App_fun (f, args) -> App_fun (f_f f, f_ts args)
|
|
||||||
| App_ho (f, a) -> App_ho (f_t f, f_t a)
|
|
||||||
| Not t -> Not (f_t t)
|
|
||||||
| If (a, b, c) -> If (f_t a, f_t b, f_t c)
|
|
||||||
| Eq (a, b) -> Eq (f_t a, f_t b)
|
|
||||||
| Opaque t -> Opaque (f_t t)
|
|
||||||
|
|
||||||
let iter_view ~f_f ~f_t ~f_ts (v : _ t) : unit =
|
|
||||||
match v with
|
|
||||||
| Bool _ -> ()
|
|
||||||
| App_fun (f, args) ->
|
|
||||||
f_f f;
|
|
||||||
f_ts args
|
|
||||||
| App_ho (f, a) ->
|
|
||||||
f_t f;
|
|
||||||
f_t a
|
|
||||||
| Not t -> f_t t
|
|
||||||
| If (a, b, c) ->
|
|
||||||
f_t a;
|
|
||||||
f_t b;
|
|
||||||
f_t c
|
|
||||||
| Eq (a, b) ->
|
|
||||||
f_t a;
|
|
||||||
f_t b
|
|
||||||
| Opaque t -> f_t t
|
|
||||||
|
|
@ -1,33 +0,0 @@
|
||||||
(** View terms through the lens of the Congruence Closure *)
|
|
||||||
|
|
||||||
(** A view of a term fron the point of view of the congruence closure.
|
|
||||||
|
|
||||||
- ['f] is the type of function symbols
|
|
||||||
- ['t] is the type of terms
|
|
||||||
- ['ts] is the type of sequences of terms (arguments of function application)
|
|
||||||
*)
|
|
||||||
type ('f, 't, 'ts) t =
|
|
||||||
| Bool of bool
|
|
||||||
| App_fun of 'f * 'ts
|
|
||||||
| App_ho of 't * 't
|
|
||||||
| If of 't * 't * 't
|
|
||||||
| Eq of 't * 't
|
|
||||||
| Not of 't
|
|
||||||
| Opaque of 't (** do not enter *)
|
|
||||||
|
|
||||||
val map_view :
|
|
||||||
f_f:('a -> 'b) ->
|
|
||||||
f_t:('c -> 'd) ->
|
|
||||||
f_ts:('e -> 'f) ->
|
|
||||||
('a, 'c, 'e) t ->
|
|
||||||
('b, 'd, 'f) t
|
|
||||||
(** Map function over a view, one level deep.
|
|
||||||
Each function maps over a different type, e.g. [f_t] maps over terms *)
|
|
||||||
|
|
||||||
val iter_view :
|
|
||||||
f_f:('a -> unit) ->
|
|
||||||
f_t:('b -> unit) ->
|
|
||||||
f_ts:('c -> unit) ->
|
|
||||||
('a, 'b, 'c) t ->
|
|
||||||
unit
|
|
||||||
(** Iterate over a view, one level deep. *)
|
|
||||||
Loading…
Add table
Reference in a new issue