simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 12:15:48 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: refactor: update theories

Browse source
This commit is contained in:
Simon Cruanes 2019-05-27 19:55:02 -05:00
parent 2978821b6e
commit e4f20d08c7
7 changed files with 164 additions and 303 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/th-bool/Sidekick_th_bool.ml
View file

@ -35,9 +35,9 @@ module Make_dyn_tseitin(A : ARG)
--> maybe, cache the clause inside the literal *)
module A = A
module Solver = A.S.Internal
module T = Solver.A.Term
module Lit = Solver.A.Lit
module SI = A.S.Solver_internal
module T = SI.A.Term
module Lit = SI.A.Lit
type term = T.t
@ -47,12 +47,12 @@ module Make_dyn_tseitin(A : ARG)
expanded: unit T_tbl.t; (* set of literals already expanded *)
}
let tseitin ~final (self:t) (solver:Solver.t) (lit:Lit.t) (lit_t:term) (v:term View.t) : unit =
let tseitin ~final (self:t) (solver:SI.t) (lit:Lit.t) (lit_t:term) (v:term View.t) : unit =
Log.debugf 5 (fun k->k "(@[th_bool.tseitin@ %a@])" Lit.pp lit);
let expanded () = T_tbl.mem self.expanded lit_t in
let add_axiom c =
T_tbl.replace self.expanded lit_t ();
Solver.add_persistent_axiom solver c
SI.add_persistent_axiom solver c
in
match v with
| B_not _ -> assert false (* normalized *)
@ -62,13 +62,13 @@ module Make_dyn_tseitin(A : ARG)
(* propagate [lit => subs_i] *)
IArray.iter
(fun sub ->
let sublit = Solver.mk_lit solver sub in
Solver.propagate_l solver sublit [lit])
let sublit = SI.mk_lit solver sub in
SI.propagate_l solver sublit [lit])
subs
) else if final && not @@ expanded () then (
(* axiom [¬lit => ∨_i ¬ subs_i] *)
let subs = IArray.to_list subs in
let c = Lit.neg lit :: List.map (Solver.mk_lit solver ~sign:false) subs in
let c = Lit.neg lit :: List.map (SI.mk_lit solver ~sign:false) subs in
add_axiom c
)
| B_or subs ->
@ -76,13 +76,13 @@ module Make_dyn_tseitin(A : ARG)
(* propagate [¬lit => ¬subs_i] *)
IArray.iter
(fun sub ->
let sublit = Solver.mk_lit solver ~sign:false sub in
Solver.add_local_axiom solver [Lit.neg lit; sublit])
let sublit = SI.mk_lit solver ~sign:false sub in
SI.add_local_axiom solver [Lit.neg lit; sublit])
subs
) else if final && not @@ expanded () then (
(* axiom [lit => ∨_i subs_i] *)
let subs = IArray.to_list subs in
let c = Lit.neg lit :: List.map (Solver.mk_lit solver ~sign:true) subs in
let c = Lit.neg lit :: List.map (SI.mk_lit solver ~sign:true) subs in
add_axiom c
)
| B_imply (guard,concl) ->
@ -90,17 +90,17 @@ module Make_dyn_tseitin(A : ARG)
(* axiom [lit => ∨_i ¬guard_i ∨ concl] *)
let guard = IArray.to_list guard in
let c =
Solver.mk_lit solver concl :: Lit.neg lit ::
List.map (Solver.mk_lit solver ~sign:false) guard in
SI.mk_lit solver concl :: Lit.neg lit ::
List.map (SI.mk_lit solver ~sign:false) guard in
add_axiom c
) else if not @@ Lit.sign lit then (
(* propagate [¬lit => ¬concl] *)
Solver.propagate_l solver (Solver.mk_lit solver ~sign:false concl) [lit];
SI.propagate_l solver (SI.mk_lit solver ~sign:false concl) [lit];
(* propagate [¬lit => ∧_i guard_i] *)
IArray.iter
(fun sub ->
let sublit = Solver.mk_lit solver ~sign:true sub in
Solver.propagate_l solver sublit [lit])
let sublit = SI.mk_lit solver ~sign:true sub in
SI.propagate_l solver sublit [lit])
guard
)
@ -118,10 +118,10 @@ module Make_dyn_tseitin(A : ARG)
let final_check (self:t) acts (lits:Lit.t Iter.t) =
check_ ~final:true self acts lits
let create_and_setup (solver:Solver.t) : t =
let create_and_setup (solver:SI.t) : t =
let self = {expanded=T_tbl.create 24} in
Solver.on_final_check solver (final_check self);
Solver.on_partial_check solver (partial_check self);
SI.on_final_check solver (final_check self);
SI.on_partial_check solver (partial_check self);
self
let theory =

22
src/th-cstor/Sidekick_th_cstor.ml
View file

@ -19,11 +19,11 @@ end
module Make(A : ARG) : S with module A = A = struct
module A = A
module Solver = A.S.Internal
module SI = A.S.Solver_internal
module T = A.S.A.Term
module N = Solver.N
module N = SI.N
module Fun = A.S.A.Fun
module Expl = Solver.Expl
module Expl = SI.Expl
type data = {
t: T.t;
@ -39,10 +39,10 @@ module Make(A : ARG) : S with module A = A = struct
end
type t = {
k: data Solver.Key.t;
k: data SI.Key.t;
}
let on_merge (solver:Solver.t) n1 tc1 n2 tc2 e_n1_n2 : unit =
let on_merge (solver:SI.t) n1 tc1 n2 tc2 e_n1_n2 : unit =
Log.debugf 5
(fun k->k "(@[th-cstor.on_merge@ @[:c1 %a@ (term %a)@]@ @[:c2 %a@ (term %a)@]@])"
N.pp n1 T.pp tc1.t N.pp n2 T.pp tc2.t);
@ -54,11 +54,11 @@ module Make(A : ARG) : S with module A = A = struct
(* same function: injectivity *)
assert (List.length l1 = List.length l2);
List.iter2
(fun u1 u2 -> Solver.cc_merge_t solver u1 u2 expl)
(fun u1 u2 -> SI.cc_merge_t solver u1 u2 expl)
l1 l2
) else (
(* different function: disjointness *)
Solver.raise_conflict solver expl
SI.raise_conflict solver expl
)
| _ -> assert false
@ -68,10 +68,10 @@ module Make(A : ARG) : S with module A = A = struct
| T_cstor _ -> Some {t;n}
| _ -> None
let create_and_setup (solver:Solver.t) : t =
let k = Solver.Key.create solver ~on_merge (module Data) in
Solver.on_cc_merge solver ~k on_merge;
Solver.on_cc_new_term solver ~k on_new_term;
let create_and_setup (solver:SI.t) : t =
let k = SI.Key.create solver (module Data) in
SI.on_cc_merge solver ~k on_merge;
SI.on_cc_new_term solver ~k on_new_term;
{k}
let theory = A.S.mk_theory ~name ~create_and_setup ()

224
src/th-distinct/Sidekick_th_distinct.ml
View file

@ -1,130 +1,93 @@
module type ARG = sig
include Sidekick_core.TERM_LIT
module Arg_distinct : sig
val as_distinct : Term.t -> Term.t Iter.t option
val mk_eq : Term.state -> Term.t -> Term.t -> Term.t
end
module S : Sidekick_core.SOLVER
val as_distinct : S.A.Term.t -> S.A.Term.t Iter.t option
val mk_eq : S.A.Term.state -> S.A.Term.t -> S.A.Term.t -> S.A.Term.t
end
module type S = sig
type term
type term_state
type lit
module Data : sig
type t
val empty : t
val merge : t -> t -> t
end
val th : Sidekick_smt.Theory.t
module A : ARG
val theory : A.S.theory
end
module Make(A : ARG with type Lit.t = Sidekick_smt.Lit.t
and type T.t = Sidekick_smt.Term.t
and type T.state = Sidekick_smt.Term.state) = struct
module T = A.T
module Lit = A.Lit
module Make(A : ARG) : S with module A = A = struct
module A = A
module SI = A.S.Solver_internal
module T = A.S.A.Term
module Lit = A.S.A.Lit
module IM = CCMap.Make(Lit)
module N = SI.N
module Expl = SI.Expl
type term = T.t
type term_state = T.state
type lit = A.Lit.t
type data = term IM.t (* "distinct" lit -> term appearing under it*)
let pp_data out m =
Fmt.fprintf out
"{@[%a@]}" Fmt.(seq ~sep:(return ",@ ") @@ pair Lit.pp T.pp) (IM.to_seq m)
module Data = struct
type t = T.t IM.t (* "distinct" lit -> term appearing under it*)
let key : (term,lit,data) Sidekick_cc.Key.t =
let merge m1 m2 =
IM.merge_safe m1 m2
~f:(fun _ pair -> match pair with
| `Left x | `Right x -> Some x
| `Both (x,_) -> Some x)
and eq = IM.equal T.equal in
Sidekick_cc.Key.create
~pp:pp_data
~name:"distinct"
~merge ~eq ()
(* micro theory *)
module Micro(CC : Sidekick_cc.Congruence_closure.S
with type term = T.t
and type lit = Lit.t
and module Key = Sidekick_cc.Key) = struct
exception E_exit
let on_merge cc n1 m1 n2 m2 expl12 =
Log.debugf 5
(fun k->k "(@[th_distinct.on_merge@ @[:n1 %a@ :map2 %a@]@ @[:n2 %a@ :map2 %a@]@])"
CC.N.pp n1 pp_data m1 CC.N.pp n2 pp_data m2);
try
let _i =
IM.merge
(fun lit o1 o2 ->
match o1, o2 with
| Some t1, Some t2 ->
(* conflict! two terms under the same "distinct" [lit]
are merged, where [lit = distinct(t1,t2,…)].
The conflict is:
[lit, t1=n1, t2=n2, expl-merge(n1,n2) ==> false]
*)
assert (not @@ T.equal t1 t2);
let expl = CC.Expl.mk_list
[expl12;
CC.Expl.mk_lit lit;
CC.Expl.mk_merge n1 (CC.Theory.add_term cc t1);
CC.Expl.mk_merge n2 (CC.Theory.add_term cc t2);
] in
CC.Theory.raise_conflict cc expl;
raise_notrace E_exit
| _ -> None)
m1 m2
in
()
with E_exit -> ()
let on_new_term _ _ _ = None
let th =
CC.Theory.make ~key ~on_merge ~on_new_term ()
let pp out m =
Fmt.fprintf out
"{@[%a@]}" Fmt.(seq ~sep:(return ",@ ") @@ pair Lit.pp T.pp) (IM.to_seq m)
end
(* called when two classes with "distinct" sets are merged *)
let on_merge (solver:SI.t) n1 m1 n2 m2 expl12 =
Log.debugf 5
(fun k->k "(@[th_distinct.on_merge@ @[:n1 %a@ :map2 %a@]@ @[:n2 %a@ :map2 %a@]@])"
N.pp n1 Data.pp m1 N.pp n2 Data.pp m2);
let _i: Data.t =
IM.merge
(fun lit o1 o2 ->
match o1, o2 with
| Some t1, Some t2 ->
(* conflict! two terms under the same "distinct" [lit]
are merged, where [lit = distinct(t1,t2,…)].
The conflict is:
[lit, t1=n1, t2=n2, expl-merge(n1,n2) ==> false]
*)
assert (not @@ T.equal t1 t2);
let expl = Expl.mk_list
[expl12;
Expl.mk_lit lit;
Expl.mk_merge n1 (SI.cc_add_term solver t1);
Expl.mk_merge n2 (SI.cc_add_term solver t2);
] in
SI.raise_conflict solver expl
| _ -> None)
m1 m2
in ()
module T_tbl = CCHashtbl.Make(T)
type st = {
tst: T.state;
type t = {
k: Data.t SI.Key.t;
expanded: unit T_tbl.t; (* negative "distinct" that have been case-split on *)
}
let create tst : st = { expanded=T_tbl.create 12; tst; }
let pp_c out c = Fmt.fprintf out "(@[<hv>%a@])" (Util.pp_list Lit.pp) c
module CC = Sidekick_smt.CC
let process_lit (st:st) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (subs:term Iter.t) : unit =
let (module A) = acts in
(* process one new assertion *)
let process_lit (self:t) (solver:SI.t) (lit:Lit.t) (lit_t:term) (subs:term Iter.t) : unit =
Log.debugf 5 (fun k->k "(@[th_distinct.process@ %a@])" Lit.pp lit);
let add_axiom c = A.add_persistent_axiom c in
let cc = A.cc in
let add_axiom c = SI.add_persistent_axiom solver c in
if Lit.sign lit then (
(* assert [distinct subs], so we update the node of each [t in subs]
with [lit] *)
(* FIXME: detect if some subs are already equal *)
(* assert [distinct subs], so we update the node of each [t in subs] with [lit] *)
subs
(fun sub ->
let n = CC.Theory.add_term cc sub in
CC.Theory.add_data cc n key (IM.singleton lit sub));
) else if not @@ T_tbl.mem st.expanded lit_t then (
let n = SI.cc_add_term solver sub in
SI.cc_add_data solver n ~k:self.k (IM.singleton lit sub));
) else if not @@ T_tbl.mem self.expanded lit_t then (
(* add clause [distinct t1…tn ∨ ∨_{i,j>i} t_i=j] *)
T_tbl.add st.expanded lit_t ();
T_tbl.add self.expanded lit_t ();
let l = Iter.to_list subs in
let c =
Iter.diagonal_l l
|> Iter.map (fun (t,u) -> Lit.atom st.tst @@ T.mk_eq st.tst t u)
|> Iter.map
(fun (t,u) -> SI.mk_lit solver @@ A.mk_eq (SI.tst solver) t u)
|> Iter.to_rev_list
in
let c = Lit.neg lit :: c in
@ -132,74 +95,21 @@ module Make(A : ARG with type Lit.t = Sidekick_smt.Lit.t
add_axiom c
)
let partial_check st (acts:Theory.actions) lits : unit =
let partial_check st (solver: SI.t) lits : unit =
lits
(fun lit ->
let t = Lit.term lit in
match T.as_distinct t with
match A.as_distinct t with
| None -> ()
| Some subs -> process_lit st acts lit t subs)
| Some subs -> process_lit st solver lit t subs)
let cc_th = let module T = Micro(CC) in T.th
let create_and_setup (solver:SI.t) : t =
let k = SI.Key.create solver (module Data) in
let self = { expanded=T_tbl.create 8; k; } in
SI.on_cc_merge solver ~k on_merge;
SI.on_final_check solver (partial_check self);
self
let th =
Sidekick_smt.Theory.make
~name:"distinct"
~partial_check
~final_check:(fun _ _ _ -> ())
~cc_th:(fun _ -> [cc_th])
~create ()
let theory =
A.S.mk_theory ~name:"distinct" ~create_and_setup ()
end
module Arg = struct
open Sidekick_smt
open Sidekick_smt.Solver_types
let id_distinct = ID.make "distinct"
let relevant _id _ _ = true
let get_ty _ _ = Ty.prop
let abs ~self _a = self, true
module T = struct
include Term
let mk_eq = eq
let as_distinct t : _ option =
match view t with
| App_cst ({cst_id;_}, args) when ID.equal cst_id id_distinct ->
Some (IArray.to_seq args)
| _ -> None
end
module Lit = Sidekick_smt.Lit
let eval args =
let module Value = Sidekick_smt.Value in
Log.debugf 5
(fun k->k "(@[distinct.eval@ %a@])" (Fmt.seq Value.pp) (IArray.to_seq args));
if
Iter.diagonal (IArray.to_seq args)
|> Iter.for_all (fun (x,y) -> not @@ Value.equal x y)
then Value.true_
else Value.false_
let c_distinct =
{cst_id=id_distinct;
cst_view=Cst_def {
pp=None; abs; ty=get_ty; relevant; do_cc=true; eval; }; }
let distinct st a =
if IArray.length a <= 1
then T.true_ st
else T.app_cst st c_distinct a
let distinct_l st = function
| [] | [_] -> T.true_ st
| xs -> distinct st (IArray.of_list xs)
end
let distinct = Arg.distinct
let distinct_l = Arg.distinct_l
include Make(Arg)

46
src/th-distinct/Sidekick_th_distinct.mli
View file

@ -5,49 +5,15 @@
"distinct" efficiently.
*)
module Term = Sidekick_smt.Term
module type ARG = sig
module T : sig
type t
type state
val pp : t Fmt.printer
val equal : t -> t -> bool
val hash : t -> int
val as_distinct : t -> t Iter.t option
val mk_eq : state -> t -> t -> t
end
module Lit : sig
type t
val term : t -> T.t
val neg : t -> t
val sign : t -> bool
val compare : t -> t -> int
val atom : T.state -> ?sign:bool -> T.t -> t
val pp : t Fmt.printer
end
module S : Sidekick_core.SOLVER
val as_distinct : S.A.Term.t -> S.A.Term.t Iter.t option
val mk_eq : S.A.Term.state -> S.A.Term.t -> S.A.Term.t -> S.A.Term.t
end
module type S = sig
type term
type term_state
type lit
type data
val key : (term, lit, data) Sidekick_cc.Key.t
val th : Sidekick_smt.Theory.t
module A : ARG
val theory : A.S.theory
end
(* TODO: generalize theories *)
module Make(A : ARG with type T.t = Sidekick_smt.Term.t
and type T.state = Sidekick_smt.Term.state
and type Lit.t = Sidekick_smt.Lit.t) :
S with type term = A.T.t
and type lit = A.Lit.t
and type term_state = A.T.state
val distinct : Term.state -> Term.t IArray.t -> Term.t
val distinct_l : Term.state -> Term.t list -> Term.t
(** Default instance *)
include S with type term = Term.t and type lit = Sidekick_smt.Lit.t
module Make(A : ARG) : S with module A = A

2
src/th-distinct/dune
View file

@ -1,7 +1,7 @@
(library
(name Sidekick_th_distinct)
(public_name sidekick.smt.th-distinct)
(public_name sidekick.th-distinct)
(libraries containers sidekick.core sidekick.util)
(flags :standard -open Sidekick_util))

131
src/th-ite/Sidekick_th_ite.ml
View file

@ -1,79 +1,73 @@
(** {1 Theory for if-then-else} *)
type 't ite_view =
| T_ite of 't * 't * 't
| T_bool of bool
| T_other of 't
module type S = sig
type lit
type term
val th : Sidekick_smt.Theory.t
module Ite_view = struct
type 't t =
| T_ite of 't * 't * 't
| T_bool of bool
| T_other of 't
end
module type ARG = sig
module T : sig
type t
type state
val pp : t Fmt.printer
val equal : t -> t -> bool
val view_as_ite : t -> t ite_view
module S : Sidekick_core.SOLVER
type term = S.A.Term.t
module Set : CCSet.S with type elt = t
end
module Lit : sig
type t
val term : t -> T.t
val atom : T.state -> ?sign:bool -> T.t -> t
val pp : t Fmt.printer
end
val view_as_ite : term -> term Ite_view.t
module T_set : CCSet.S with type elt = term
end
module Make(Arg : ARG with type T.state = Sidekick_smt.Term.state and type T.t = Sidekick_smt.Term.t)
: S with type lit = Arg.Lit.t and type term = Arg.T.t
= struct
module Th = Sidekick_smt.Theory
module N = Th.CC_eq_class
module Expl = Th.CC_expl
module CC = Sidekick_smt.CC
module type S = sig
module A : ARG
val theory : A.S.theory
end
open Arg
type lit = Lit.t
module Make(A : ARG)
(* : S with module A = A *)
= struct
module A = A
module Solver = A.S.Solver_internal
module N = Solver.N
module Expl = Solver.Expl
module T = A.S.A.Term
type lit = A.S.A.Lit.t
type term = T.t
type data = T.Set.t
(* associate to each class [t] the set of [ite a b c] where [a=t] *)
module Data = struct
type t = A.T_set.t
(* associate to each class [t] the set of [ite a b c] where [a=t] *)
let pp_data = Fmt.(map T.Set.to_seq @@ seq ~sep:(return ",@ ") T.pp)
let pp = Fmt.(map A.T_set.to_seq @@ seq ~sep:(return ",@ ") T.pp)
let merge = A.T_set.union
end
let key : (_,_,data) Sidekick_cc.Key.t = Sidekick_cc.Key.create
~pp:pp_data ~name:"ite" ~eq:T.Set.equal ~merge:T.Set.union ()
type t = {
k: Data.t Solver.Key.t;
}
type t = T.state
let on_merge (_st:t) (acts:Sidekick_smt.Theory.actions) n1 n2 e_n1_n2 : unit =
let (module A) = acts in
let on_merge (self:t) (solver:Solver.t) n1 n2 e_n1_n2 : unit =
Log.debugf 5
(fun k->k "(@[th-ite.on_merge@ :c1 %a@ :c2 %a@])" N.pp n1 N.pp n2);
(* check if [n1] has some [ite] parents, and if [n2] is true/false *)
let check_ n1 n2 =
match CC.Theory.get_data A.cc n1 key, T.view_as_ite (N.term n2) with
match Solver.cc_data solver ~k:self.k n1, A.view_as_ite (N.term n2) with
| Some set, T_bool n2_true ->
assert (not @@ T.Set.is_empty set);
T.Set.iter
(fun parent_1 -> match T.view_as_ite parent_1 with
assert (not @@ A.T_set.is_empty set);
A.T_set.iter
(fun parent_1 -> match A.view_as_ite parent_1 with
| T_ite (a1,b1,c1) ->
let n_parent1 = CC.add_term A.cc parent_1 in
let expl = Expl.mk_list [e_n1_n2; Expl.mk_merge n1 (CC.add_term A.cc a1)] in
let n_parent1 = Solver.cc_add_term solver parent_1 in
let expl =
Expl.mk_list [
e_n1_n2;
Expl.mk_merge n1 (Solver.cc_add_term solver a1)] in
if n2_true then (
(* [a1 = n1 = n2 = true] so [if a1 b1 c1 = b1] *)
CC.Theory.merge A.cc n_parent1 (CC.add_term A.cc b1) expl
Solver.cc_merge solver n_parent1 (Solver.cc_add_term solver b1) expl
) else (
(* [a1 = n1 = n2 = false] so [if a1 b1 c1 = c1] *)
CC.Theory.merge A.cc n_parent1 (CC.add_term A.cc c1) expl
Solver.cc_merge solver n_parent1 (Solver.cc_add_term solver c1) expl
)
| _ -> assert false)
set
@ -83,31 +77,22 @@ module Make(Arg : ARG with type T.state = Sidekick_smt.Term.state and type T.t =
check_ n2 n1;
()
let on_new_term _ (acts:Sidekick_smt.Theory.actions) (t:T.t) =
let (module A) = acts in
match T.view_as_ite t with
let on_new_term (self:t) (solver:Solver.t) _n (t:T.t) =
match A.view_as_ite t with
| T_ite (a,_,_) ->
(* add [t] to parents of [a] *)
let n_a = CC.find A.cc @@ CC.add_term A.cc a in
CC.Theory.add_data A.cc n_a key (T.Set.singleton t)
| _ -> ()
let n_a = Solver.cc_find solver @@ Solver.cc_add_term solver a in
Solver.cc_add_data solver n_a ~k:self.k (A.T_set.singleton t);
None
| _ -> None
let th =
Sidekick_smt.Theory.make ~name:"ite" ~create:(fun st->st)
~on_merge ~final_check:(fun _ _ _ -> ())
~on_new_term
()
let create_and_setup (solver:Solver.t) : t =
let k = Solver.Key.create solver (module Data) in
let self = {k} in
Solver.on_cc_merge_all solver (on_merge self);
Solver.on_cc_new_term solver ~k (on_new_term self);
self
let theory = A.S.mk_theory ~name:"ite" ~create_and_setup ()
end
include Make(struct
module T = struct
include Sidekick_smt.Term
let[@inline] view_as_ite t = match view t with
| If (a,b,c) -> T_ite (a,b,c)
| Bool b -> T_bool b
| _ -> T_other t
end
module Lit = Sidekick_smt.Lit
end)

4
src/th-ite/dune
View file

@ -2,7 +2,7 @@
(library
(name Sidekick_th_ite)
(public_name sidekick.smt.th-ite)
(libraries containers sidekick.smt)
(public_name sidekick.th-ite)
(libraries containers sidekick.core)
(flags :standard -open Sidekick_util))