From 0d0751b7d2631b51ec9128553a5075bff6dd09dc Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 30 Jul 2022 23:01:29 -0400 Subject: [PATCH] refactor(theories): remove functors --- src/th-bool-static/Sidekick_th_bool_static.ml | 182 ++------- .../Sidekick_th_bool_static.mli | 11 + src/th-bool-static/dune | 3 +- src/th-bool-static/intf.ml | 65 ++++ src/th-cstor/Sidekick_th_cstor.ml | 57 ++- src/th-cstor/dune | 3 +- src/th-data/Sidekick_th_data.ml | 358 +++++++++--------- src/th-data/Sidekick_th_data.mli | 9 +- src/th-data/dune | 5 +- src/th-data/th_intf.ml | 81 ++-- src/th-lra/intf.ml | 59 +++ src/th-lra/sidekick_arith_lra.ml | 171 +++------ src/th-lra/sidekick_arith_lra.mli | 26 ++ 13 files changed, 502 insertions(+), 528 deletions(-) create mode 100644 src/th-bool-static/Sidekick_th_bool_static.mli create mode 100644 src/th-bool-static/intf.ml create mode 100644 src/th-lra/intf.ml create mode 100644 src/th-lra/sidekick_arith_lra.mli diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index b986cc83..f18edbfd 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -1,146 +1,43 @@ -(** Theory of boolean formulas. +open Sidekick_core +module Intf = Intf +open Intf +module SI = SMT.Solver_internal +module T = Term - This handles formulas containing "and", "or", "=>", "if-then-else", etc. - *) +module type ARG = Intf.ARG -open Sidekick_sigs_smt +module Make (A : ARG) : sig + val theory : SMT.theory +end = struct + type state = { tst: T.store; gensym: A.Gensym.t } -(** Boolean-oriented view of terms *) -type ('a, 'args) bool_view = - | B_bool of bool - | B_not of 'a - | B_and of 'args - | B_or of 'args - | B_imply of 'args * 'a - | B_equiv of 'a * 'a - | B_xor of 'a * 'a - | B_eq of 'a * 'a - | B_neq of 'a * 'a - | B_ite of 'a * 'a * 'a - | B_opaque_bool of 'a (* do not enter *) - | B_atom of 'a - -module type PROOF_RULES = sig - type rule - type term - type lit - - val lemma_bool_tauto : lit Iter.t -> rule - (** Boolean tautology lemma (clause) *) - - val lemma_bool_c : string -> term list -> rule - (** Basic boolean logic lemma for a clause [|- c]. - [proof_bool_c b name cs] is the rule designated by [name]. *) - - val lemma_bool_equiv : term -> term -> rule - (** Boolean tautology lemma (equivalence) *) - - val lemma_ite_true : ite:term -> rule - (** lemma [a ==> ite a b c = b] *) - - val lemma_ite_false : ite:term -> rule - (** lemma [¬a ==> ite a b c = c] *) -end - -(** Argument to the theory *) -module type ARG = sig - module S : SOLVER - - type term = S.T.Term.t - - val view_as_bool : term -> (term, term Iter.t) bool_view - (** Project the term into the boolean view. *) - - val mk_bool : S.T.Term.store -> (term, term array) bool_view -> term - (** Make a term from the given boolean view. *) - - module P : - PROOF_RULES - with type rule := S.Proof_trace.A.rule - and type lit := S.Lit.t - and type term := S.T.Term.t - - (** Fresh symbol generator. - - The theory needs to be able to create new terms with fresh names, - to be used as placeholders for complex formulas during Tseitin - encoding. *) - module Gensym : sig - type t - - val create : S.T.Term.store -> t - (** New (stateful) generator instance. *) - - val fresh_term : t -> pre:string -> S.T.Ty.t -> term - (** Make a fresh term of the given type *) - end -end - -(** Signature *) -module type S = sig - module A : ARG - - type state - - val create : A.S.T.Term.store -> A.S.T.Ty.store -> state - - val simplify : state -> A.S.Solver_internal.simplify_hook - (** Simplify given term *) - - val cnf : state -> A.S.Solver_internal.preprocess_hook - (** preprocesses formulas by giving them names and - adding clauses to equate the name with the boolean formula. *) - - val theory : A.S.theory - (** A theory that can be added to the solver {!A.S}. - - This theory does most of its work during preprocessing, - turning boolean formulas into SAT clauses via - the {{: https://en.wikipedia.org/wiki/Tseytin_transformation} - Tseitin encoding} . *) -end - -module Make (A : ARG) : S with module A = A = struct - module A = A - module Ty = A.S.T.Ty - module T = A.S.T.Term - module Lit = A.S.Solver_internal.Lit - module SI = A.S.Solver_internal - - (* utils *) - open struct - module Pr = A.S.Proof_trace - end - - type state = { tst: T.store; ty_st: Ty.store; gensym: A.Gensym.t } - - let create tst ty_st : state = { tst; ty_st; gensym = A.Gensym.create tst } + let create tst : state = { tst; gensym = A.Gensym.create tst } let[@inline] not_ tst t = A.mk_bool tst (B_not t) let[@inline] eq tst a b = A.mk_bool tst (B_eq (a, b)) let is_true t = - match T.as_bool t with + match T.as_bool_val t with | Some true -> true | _ -> false let is_false t = - match T.as_bool t with + match T.as_bool_val t with | Some false -> true | _ -> false - let simplify (self : state) (simp : SI.Simplify.t) (t : T.t) : - (T.t * SI.step_id Iter.t) option = + let simplify (self : state) (simp : Simplify.t) (t : T.t) : + (T.t * Proof_step.id Iter.t) option = let tst = self.tst in - let proof = SI.Simplify.proof simp in + let proof = Simplify.proof simp in let steps = ref [] in let add_step_ s = steps := s :: !steps in - let mk_step_ r = Pr.add_step proof r in + let mk_step_ r = Proof_trace.add_step proof r in let add_step_eq a b ~using ~c0 : unit = add_step_ @@ mk_step_ - @@ SI.P_core_rules.lemma_rw_clause c0 ~using - ~res:(Iter.return (Lit.atom tst (A.mk_bool tst (B_eq (a, b))))) + @@ Proof_core.lemma_rw_clause c0 ~using + ~res:(Iter.return (Lit.atom (A.mk_bool tst (B_eq (a, b))))) in let[@inline] ret u = Some (u, Iter.of_list !steps) in @@ -152,35 +49,35 @@ module Make (A : ARG) : S with module A = A = struct match A.view_as_bool t with | B_bool _ -> None - | B_not u when is_true u -> ret_bequiv t (T.bool tst false) - | B_not u when is_false u -> ret_bequiv t (T.bool tst true) + | B_not u when is_true u -> ret_bequiv t (T.false_ tst) + | B_not u when is_false u -> ret_bequiv t (T.true_ tst) | B_not _ -> None | B_opaque_bool _ -> None | B_and a -> if Iter.exists is_false a then - ret (T.bool tst false) + ret (T.false_ tst) else if Iter.for_all is_true a then - ret (T.bool tst true) + ret (T.true_ tst) else None | B_or a -> if Iter.exists is_true a then - ret (T.bool tst true) + ret (T.true_ tst) else if Iter.for_all is_false a then - ret (T.bool tst false) + ret (T.false_ tst) else None | B_imply (args, u) -> if Iter.exists is_false args then - ret (T.bool tst true) + ret (T.true_ tst) else if is_true u then - ret (T.bool tst true) + ret (T.true_ tst) else None | B_ite (a, b, c) -> (* directly simplify [a] so that maybe we never will simplify one of the branches *) - let a, prf_a = SI.Simplify.normalize_t simp a in + let a, prf_a = Simplify.normalize_t simp a in Option.iter add_step_ prf_a; (match A.view_as_bool a with | B_bool true -> @@ -201,27 +98,28 @@ module Make (A : ARG) : S with module A = A = struct | B_xor (a, b) when is_false b -> ret_bequiv t a | B_xor (a, b) when is_true b -> ret_bequiv t (not_ tst a) | B_equiv _ | B_xor _ -> None - | B_eq (a, b) when T.equal a b -> ret_bequiv t (T.bool tst true) - | B_neq (a, b) when T.equal a b -> ret_bequiv t (T.bool tst true) + | B_eq (a, b) when T.equal a b -> ret_bequiv t (T.true_ tst) + | B_neq (a, b) when T.equal a b -> ret_bequiv t (T.true_ tst) | B_eq _ | B_neq _ -> None | B_atom _ -> None let fresh_term self ~for_t ~pre ty = let u = A.Gensym.fresh_term self.gensym ~pre ty in Log.debugf 20 (fun k -> - k "(@[sidekick.bool.proxy@ :t %a@ :for %a@])" T.pp u T.pp for_t); - assert (Ty.equal ty (T.ty u)); + k "(@[sidekick.bool.proxy@ :t %a@ :for %a@])" T.pp_debug u T.pp_debug + for_t); + assert (Term.equal ty (T.ty u)); u let fresh_lit (self : state) ~for_t ~mk_lit ~pre : T.t * Lit.t = - let proxy = fresh_term ~for_t ~pre self (Ty.bool self.ty_st) in + let proxy = fresh_term ~for_t ~pre self (Term.bool self.tst) in proxy, mk_lit proxy (* TODO: polarity? *) let cnf (self : state) (si : SI.t) (module PA : SI.PREPROCESS_ACTS) (t : T.t) : unit = - Log.debugf 50 (fun k -> k "(@[th-bool.cnf@ %a@])" T.pp t); - let[@inline] mk_step_ r = Pr.add_step PA.proof r in + Log.debugf 50 (fun k -> k "(@[th-bool.cnf@ %a@])" T.pp_debug t); + let[@inline] mk_step_ r = Proof_trace.add_step PA.proof r in (* handle boolean equality *) let equiv_ _si ~is_xor ~t t_a t_b : unit = @@ -332,10 +230,14 @@ module Make (A : ARG) : S with module A = A = struct let create_and_setup si = Log.debug 2 "(th-bool.setup)"; - let st = create (SI.tst si) (SI.ty_st si) in + let st = create (SI.tst si) in SI.add_simplifier si (simplify st); SI.on_preprocess si (cnf st); st - let theory = A.S.mk_theory ~name:"th-bool" ~create_and_setup () + let theory = SMT.Solver.mk_theory ~name:"th-bool" ~create_and_setup () end + +let theory (module A : ARG) : SMT.theory = + let module M = Make (A) in + M.theory diff --git a/src/th-bool-static/Sidekick_th_bool_static.mli b/src/th-bool-static/Sidekick_th_bool_static.mli new file mode 100644 index 00000000..b83dc6c6 --- /dev/null +++ b/src/th-bool-static/Sidekick_th_bool_static.mli @@ -0,0 +1,11 @@ +(** Theory of boolean formulas. + + This handles formulas containing "and", "or", "=>", "if-then-else", etc. +*) + +module Intf = Intf +open Intf + +module type ARG = Intf.ARG + +val theory : (module ARG) -> SMT.Theory.t diff --git a/src/th-bool-static/dune b/src/th-bool-static/dune index 0cb1c59f..4a4dfc63 100644 --- a/src/th-bool-static/dune +++ b/src/th-bool-static/dune @@ -2,4 +2,5 @@ (name sidekick_th_bool_static) (public_name sidekick.th-bool-static) (flags :standard -open Sidekick_util) - (libraries sidekick.sigs.smt sidekick.util sidekick.cc.plugin)) + (libraries sidekick.core sidekick.smt-solver sidekick.util sidekick.simplify + sidekick.cc)) diff --git a/src/th-bool-static/intf.ml b/src/th-bool-static/intf.ml new file mode 100644 index 00000000..e25335a2 --- /dev/null +++ b/src/th-bool-static/intf.ml @@ -0,0 +1,65 @@ +open Sidekick_core +module SMT = Sidekick_smt_solver +module Simplify = Sidekick_simplify + +type term = Term.t +type ty = Term.t + +(** Boolean-oriented view of terms *) +type ('a, 'args) bool_view = + | B_bool of bool + | B_not of 'a + | B_and of 'args + | B_or of 'args + | B_imply of 'args * 'a + | B_equiv of 'a * 'a + | B_xor of 'a * 'a + | B_eq of 'a * 'a + | B_neq of 'a * 'a + | B_ite of 'a * 'a * 'a + | B_opaque_bool of 'a (* do not enter *) + | B_atom of 'a + +module type PROOF_RULES = sig + val lemma_bool_tauto : Lit.t Iter.t -> Proof_term.t + (** Boolean tautology lemma (clause) *) + + val lemma_bool_c : string -> term list -> Proof_term.t + (** Basic boolean logic lemma for a clause [|- c]. + [proof_bool_c b name cs] is the Proof_term.t designated by [name]. *) + + val lemma_bool_equiv : term -> term -> Proof_term.t + (** Boolean tautology lemma (equivalence) *) + + val lemma_ite_true : ite:term -> Proof_term.t + (** lemma [a ==> ite a b c = b] *) + + val lemma_ite_false : ite:term -> Proof_term.t + (** lemma [¬a ==> ite a b c = c] *) +end + +(** Argument to the theory *) +module type ARG = sig + val view_as_bool : term -> (term, term Iter.t) bool_view + (** Project the term into the boolean view. *) + + val mk_bool : Term.store -> (term, term array) bool_view -> term + (** Make a term from the given boolean view. *) + + module P : PROOF_RULES + + (** Fresh symbol generator. + + The theory needs to be able to create new terms with fresh names, + to be used as placeholders for complex formulas during Tseitin + encoding. *) + module Gensym : sig + type t + + val create : Term.store -> t + (** New (stateful) generator instance. *) + + val fresh_term : t -> pre:string -> ty -> term + (** Make a fresh term of the given type *) + end +end diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index fb5035ac..67a4845a 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -1,55 +1,43 @@ -(** {1 Theory for constructors} *) - -open Sidekick_sigs_smt +open Sidekick_core +module SMT = Sidekick_smt_solver +module SI = SMT.Solver_internal +module T = Term type ('c, 't) cstor_view = T_cstor of 'c * 't array | T_other of 't let name = "th-cstor" module type ARG = sig - module S : SOLVER - - val view_as_cstor : S.T.Term.t -> (S.T.Fun.t, S.T.Term.t) cstor_view - val lemma_cstor : S.Lit.t Iter.t -> S.Proof_trace.A.rule + val view_as_cstor : Term.t -> (Const.t, Term.t) cstor_view + val lemma_cstor : Lit.t Iter.t -> Proof_term.t end -module type S = sig - module A : ARG - - val theory : A.S.theory -end - -module Make (A : ARG) : S with module A = A = struct - module A = A - module SI = A.S.Solver_internal - module T = A.S.T.Term - module N = SI.CC.E_node - module Fun = A.S.T.Fun - module Expl = SI.CC.Expl +module Make (A : ARG) : sig + val theory : SMT.theory +end = struct + open Sidekick_cc module Monoid = struct - module CC = SI.CC - (* associate to each class a unique constructor term in the class (if any) *) - type t = { t: T.t; n: N.t; cstor: Fun.t; args: N.t array } + type t = { t: T.t; n: E_node.t; cstor: Const.t; args: E_node.t array } let name = name let pp out (v : t) = - Fmt.fprintf out "(@[cstor %a@ :term %a@])" Fun.pp v.cstor T.pp v.t + Fmt.fprintf out "(@[cstor %a@ :term %a@])" Const.pp v.cstor T.pp_debug v.t (* attach data to constructor terms *) let of_term cc n (t : T.t) : _ option * _ = match A.view_as_cstor t with | T_cstor (cstor, args) -> - let args = CCArray.map (SI.CC.add_term cc) args in + let args = CCArray.map (CC.add_term cc) args in Some { n; t; cstor; args }, [] | _ -> None, [] let merge _cc n1 v1 n2 v2 e_n1_n2 : _ result = Log.debugf 5 (fun k -> - k "(@[%s.merge@ @[:c1 %a (t %a)@]@ @[:c2 %a (t %a)@]@])" name N.pp n1 - T.pp v1.t N.pp n2 T.pp v2.t); + k "(@[%s.merge@ @[:c1 %a (t %a)@]@ @[:c2 %a (t %a)@]@])" name + E_node.pp n1 T.pp_debug v1.t E_node.pp n2 T.pp_debug v2.t); (* build full explanation of why the constructor terms are equal *) (* FIXME: add a (fun p -> A.lemma_cstor p …) here. probably we need [Some a=Some b => a=b] as a lemma for inj, @@ -57,22 +45,22 @@ module Make (A : ARG) : S with module A = A = struct let expl = Expl.mk_list [ e_n1_n2; Expl.mk_merge n1 v1.n; Expl.mk_merge n2 v2.n ] in - if Fun.equal v1.cstor v2.cstor then ( + if Const.equal v1.cstor v2.cstor then ( (* same function: injectivity *) assert (CCArray.length v1.args = CCArray.length v2.args); let acts = CCArray.map2 - (fun u1 u2 -> SI.CC.Handler_action.Act_merge (u1, u2, expl)) + (fun u1 u2 -> CC.Handler_action.Act_merge (u1, u2, expl)) v1.args v2.args |> Array.to_list in Ok (v1, acts) ) else (* different function: disjointness *) - Error (SI.CC.Handler_action.Conflict expl) + Error (CC.Handler_action.Conflict expl) end - module ST = Sidekick_cc_plugin.Make (Monoid) + module ST = Sidekick_cc.Plugin.Make (Monoid) type t = ST.t @@ -85,5 +73,10 @@ module Make (A : ARG) : S with module A = A = struct let self = ST.create_and_setup ~size:32 (SI.cc si) in self - let theory = A.S.mk_theory ~name ~push_level ~pop_levels ~create_and_setup () + let theory = + SMT.Solver.mk_theory ~name ~push_level ~pop_levels ~create_and_setup () end + +let make (module A : ARG) : SMT.theory = + let module M = Make (A) in + M.theory diff --git a/src/th-cstor/dune b/src/th-cstor/dune index bd39edcf..45db9b7e 100644 --- a/src/th-cstor/dune +++ b/src/th-cstor/dune @@ -1,5 +1,6 @@ (library (name Sidekick_th_cstor) (public_name sidekick.th-cstor) - (libraries containers sidekick.sigs.smt sidekick.util sidekick.cc.plugin) + (libraries containers sidekick.core sidekick.smt-solver sidekick.util + sidekick.cc) (flags :standard -open Sidekick_util)) diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 1c02d6be..bcaae31a 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -1,21 +1,12 @@ (** Theory for datatypes. *) +open Sidekick_core +open Sidekick_cc include Th_intf +module SI = SMT.Solver_internal let name = "th-data" -(** An abtract representation of a datatype *) -module type DATA_TY = sig - type t - type cstor - - val equal : t -> t -> bool - val finite : t -> bool - val set_finite : t -> bool -> unit - val view : t -> (cstor, t) data_ty_view - val cstor_args : cstor -> t Iter.t -end - (** {2 Cardinality of types} *) module C = struct @@ -51,23 +42,22 @@ module Compute_card (A : ARG) : sig type t val create : unit -> t - val base_cstor : t -> A.S.T.Ty.t -> A.Cstor.t option - val is_finite : t -> A.S.T.Ty.t -> bool + val base_cstor : t -> ty -> A.Cstor.t option + val is_finite : t -> ty -> bool end = struct - module Ty = A.S.T.Ty - module Ty_tbl = CCHashtbl.Make (Ty) + module Ty_tbl = Term.Tbl type ty_cell = { mutable card: C.t; mutable base_cstor: A.Cstor.t option } type t = { cards: ty_cell Ty_tbl.t } let create () : t = { cards = Ty_tbl.create 16 } - let find (self : t) (ty0 : Ty.t) : ty_cell = + let find (self : t) (ty0 : ty) : ty_cell = let dr_tbl = Ty_tbl.create 16 in (* to build [ty], do we need to build [ty0]? *) - let rec is_direct_recursion (ty : Ty.t) : bool = - Ty.equal ty0 ty + let rec is_direct_recursion (ty : ty) : bool = + Term.equal ty0 ty || try Ty_tbl.find dr_tbl ty with Not_found -> @@ -89,7 +79,7 @@ end = struct Iter.exists is_direct_recursion (A.Cstor.ty_args c) in - let rec get_cell (ty : Ty.t) : ty_cell = + let rec get_cell (ty : ty) : ty_cell = match Ty_tbl.find self.cards ty with | c -> c | exception Not_found -> @@ -131,8 +121,8 @@ end = struct in cell.card <- card; Log.debugf 5 (fun k -> - k "(@[th-data.card-ty@ %a@ :is %a@ :base-cstor %a@])" Ty.pp ty C.pp - card + k "(@[th-data.card-ty@ %a@ :is %a@ :base-cstor %a@])" Term.pp_debug + ty C.pp card (Fmt.Dump.option A.Cstor.pp) cell.base_cstor); cell @@ -149,103 +139,86 @@ end = struct | C.Infinite -> false end -module type S = sig - module A : ARG - - val theory : A.S.theory -end - -module Make (A : ARG) : S with module A = A = struct - module A = A - module SI = A.S.Solver_internal - module T = A.S.T.Term - module N = SI.CC.E_node - module Ty = A.S.T.Ty - module Expl = SI.CC.Expl +module Make (A : ARG) : sig + val theory : SMT.theory +end = struct module Card = Compute_card (A) - open struct - module Pr = SI.Proof_trace - end - (** Monoid mapping each class to the (unique) constructor it contains, if any *) module Monoid_cstor = struct - module CC = SI.CC - let name = "th-data.cstor" (* associate to each class a unique constructor term in the class (if any) *) - type t = { c_n: N.t; c_cstor: A.Cstor.t; c_args: N.t array } + type t = { c_n: E_node.t; c_cstor: A.Cstor.t; c_args: E_node.t array } let pp out (v : t) = Fmt.fprintf out "(@[%s@ :cstor %a@ :n %a@ :args [@[%a@]]@])" name - A.Cstor.pp v.c_cstor N.pp v.c_n (Util.pp_array N.pp) v.c_args + A.Cstor.pp v.c_cstor E_node.pp v.c_n (Util.pp_array E_node.pp) v.c_args (* attach data to constructor terms *) - let of_term cc n (t : T.t) : _ option * _ list = + let of_term cc n (t : Term.t) : _ option * _ list = match A.view_as_data t with | T_cstor (cstor, args) -> - let args = CCArray.map (SI.CC.add_term cc) args in + let args = CCArray.map (CC.add_term cc) args in Some { c_n = n; c_cstor = cstor; c_args = args }, [] | _ -> None, [] let merge cc n1 c1 n2 c2 e_n1_n2 : _ result = Log.debugf 5 (fun k -> - k "(@[%s.merge@ (@[:c1 %a@ %a@])@ (@[:c2 %a@ %a@])@])" name N.pp n1 pp - c1 N.pp n2 pp c2); + k "(@[%s.merge@ (@[:c1 %a@ %a@])@ (@[:c2 %a@ %a@])@])" name E_node.pp + n1 pp c1 E_node.pp n2 pp c2); let mk_expl t1 t2 pr = Expl.mk_theory t1 t2 [ - ( N.term n1, - N.term n2, + ( E_node.term n1, + E_node.term n2, [ e_n1_n2; Expl.mk_merge n1 c1.c_n; Expl.mk_merge n2 c2.c_n ] ); ] pr in - let proof = SI.CC.proof cc in + let proof = CC.proof cc in if A.Cstor.equal c1.c_cstor c2.c_cstor then ( (* same function: injectivity *) let expl_merge i = - let t1 = N.term c1.c_n in - let t2 = N.term c2.c_n in - mk_expl t1 t2 @@ Pr.add_step proof @@ A.P.lemma_cstor_inj t1 t2 i + let t1 = E_node.term c1.c_n in + let t2 = E_node.term c2.c_n in + mk_expl t1 t2 @@ Proof_trace.add_step proof + @@ A.P.lemma_cstor_inj t1 t2 i in assert (CCArray.length c1.c_args = CCArray.length c2.c_args); let acts = ref [] in Util.array_iteri2 c1.c_args c2.c_args ~f:(fun i u1 u2 -> - acts := - SI.CC.Handler_action.Act_merge (u1, u2, expl_merge i) :: !acts); + acts := CC.Handler_action.Act_merge (u1, u2, expl_merge i) :: !acts); Ok (c1, !acts) ) else ( (* different function: disjointness *) let expl = - let t1 = N.term c1.c_n and t2 = N.term c2.c_n in - mk_expl t1 t2 @@ Pr.add_step proof @@ A.P.lemma_cstor_distinct t1 t2 + let t1 = E_node.term c1.c_n and t2 = E_node.term c2.c_n in + mk_expl t1 t2 @@ Proof_trace.add_step proof + @@ A.P.lemma_cstor_distinct t1 t2 in - Error (SI.CC.Handler_action.Conflict expl) + Error (CC.Handler_action.Conflict expl) ) end (** Monoid mapping each class to the set of is-a/select of which it is the argument *) module Monoid_parents = struct - module CC = SI.CC - let name = "th-data.parents" type select = { - sel_n: N.t; + sel_n: E_node.t; sel_cstor: A.Cstor.t; sel_idx: int; - sel_arg: N.t; + sel_arg: E_node.t; } - type is_a = { is_a_n: N.t; is_a_cstor: A.Cstor.t; is_a_arg: N.t } + type is_a = { is_a_n: E_node.t; is_a_cstor: A.Cstor.t; is_a_arg: E_node.t } (* associate to each class a unique constructor term in the class (if any) *) type t = { @@ -255,10 +228,11 @@ module Make (A : ARG) : S with module A = A = struct let pp_select out s = Fmt.fprintf out "(@[sel[%d]-%a@ :n %a@])" s.sel_idx A.Cstor.pp s.sel_cstor - N.pp s.sel_n + E_node.pp s.sel_n let pp_is_a out s = - Fmt.fprintf out "(@[is-%a@ :n %a@])" A.Cstor.pp s.is_a_cstor N.pp s.is_a_n + Fmt.fprintf out "(@[is-%a@ :n %a@])" A.Cstor.pp s.is_a_cstor E_node.pp + s.is_a_n let pp out (v : t) = Fmt.fprintf out "(@[%s@ @[:sel [@[%a@]]@]@ @[:is-a [@[%a@]]@]@])" name @@ -266,10 +240,10 @@ module Make (A : ARG) : S with module A = A = struct v.parent_is_a (* attach data to constructor terms *) - let of_term cc n (t : T.t) : _ option * _ list = + let of_term cc n (t : Term.t) : _ option * _ list = match A.view_as_data t with | T_select (c, i, u) -> - let u = SI.CC.add_term cc u in + let u = CC.add_term cc u in let m_sel = { parent_select = @@ -279,7 +253,7 @@ module Make (A : ARG) : S with module A = A = struct in None, [ u, m_sel ] | T_is_a (c, u) -> - let u = SI.CC.add_term cc u in + let u = CC.add_term cc u in let m_sel = { parent_is_a = [ { is_a_n = n; is_a_cstor = c; is_a_arg = u } ]; @@ -289,31 +263,31 @@ module Make (A : ARG) : S with module A = A = struct None, [ u, m_sel ] | T_cstor _ | T_other _ -> None, [] - let merge cc n1 v1 n2 v2 _e : _ result = + let merge _cc n1 v1 n2 v2 _e : _ result = Log.debugf 5 (fun k -> - k "(@[%s.merge@ @[:c1 %a@ :v %a@]@ @[:c2 %a@ :v %a@]@])" name N.pp n1 - pp v1 N.pp n2 pp v2); + k "(@[%s.merge@ @[:c1 %a@ :v %a@]@ @[:c2 %a@ :v %a@]@])" name + E_node.pp n1 pp v1 E_node.pp n2 pp v2); let parent_is_a = v1.parent_is_a @ v2.parent_is_a in let parent_select = v1.parent_select @ v2.parent_select in Ok ({ parent_is_a; parent_select }, []) end - module ST_cstors = Sidekick_cc_plugin.Make (Monoid_cstor) - module ST_parents = Sidekick_cc_plugin.Make (Monoid_parents) - module N_tbl = Backtrackable_tbl.Make (N) + module ST_cstors = Sidekick_cc.Plugin.Make (Monoid_cstor) + module ST_parents = Sidekick_cc.Plugin.Make (Monoid_parents) + module N_tbl = Backtrackable_tbl.Make (E_node) type t = { - tst: T.store; - proof: SI.Proof_trace.t; + tst: Term.store; + proof: Proof_trace.t; cstors: ST_cstors.t; (* repr -> cstor for the class *) parents: ST_parents.t; (* repr -> parents for the class *) cards: Card.t; (* remember finiteness *) to_decide: unit N_tbl.t; (* set of terms to decide. *) to_decide_for_complete_model: unit N_tbl.t; (* infinite types but we need a cstor in model*) - case_split_done: unit T.Tbl.t; + case_split_done: unit Term.Tbl.t; (* set of terms for which case split is done *) - single_cstor_preproc_done: unit T.Tbl.t; (* preprocessed terms *) + single_cstor_preproc_done: unit Term.Tbl.t; (* preprocessed terms *) stat_acycl_conflict: int Stat.counter; (* TODO: bitfield for types with less than 62 cstors, to quickly detect conflict? *) } @@ -330,24 +304,25 @@ module Make (A : ARG) : S with module A = A = struct N_tbl.pop_levels self.to_decide n; () - let preprocess (self : t) si (acts : SI.preprocess_actions) (t : T.t) : unit = - let ty = T.ty t in + let preprocess (self : t) _si (acts : SI.preprocess_actions) (t : Term.t) : + unit = + let ty = Term.ty t in match A.view_as_data t, A.as_datatype ty with | T_cstor _, _ -> () | _, Ty_data { cstors; _ } -> (match Iter.take 2 cstors |> Iter.to_rev_list with - | [ cstor ] when not (T.Tbl.mem self.single_cstor_preproc_done t) -> + | [ cstor ] when not (Term.Tbl.mem self.single_cstor_preproc_done t) -> (* single cstor: assert [t = cstor (sel-c-0 t, …, sel-c n t)] *) Log.debugf 50 (fun k -> k "(@[%s.preprocess.single-cstor@ %a@ :ty %a@ :cstor %a@])" name - T.pp t Ty.pp ty A.Cstor.pp cstor); + Term.pp_debug t Term.pp_debug ty A.Cstor.pp cstor); let (module Act) = acts in let u = let sel_args = A.Cstor.ty_args cstor - |> Iter.mapi (fun i ty -> A.mk_sel self.tst cstor i t) + |> Iter.mapi (fun i _ty -> A.mk_sel self.tst cstor i t) |> Iter.to_array in A.mk_cstor self.tst cstor sel_args @@ -357,18 +332,20 @@ module Make (A : ARG) : S with module A = A = struct with exhaustiveness: [|- is-c(t)] *) let proof = let pr_isa = - Pr.add_step self.proof + Proof_trace.add_step self.proof @@ A.P.lemma_isa_split t (Iter.return @@ Act.mk_lit (A.mk_is_a self.tst cstor t)) and pr_eq_sel = - Pr.add_step self.proof @@ A.P.lemma_select_cstor ~cstor_t:u t + Proof_trace.add_step self.proof + @@ A.P.lemma_select_cstor ~cstor_t:u t in - Pr.add_step self.proof @@ SI.P_core_rules.proof_r1 pr_isa pr_eq_sel + Proof_trace.add_step self.proof + @@ Proof_core.proof_r1 pr_isa pr_eq_sel in - T.Tbl.add self.single_cstor_preproc_done t (); + Term.Tbl.add self.single_cstor_preproc_done t (); (* avoid loops *) - T.Tbl.add self.case_split_done t (); + Term.Tbl.add self.case_split_done t (); (* no need to decide *) Act.add_clause [ Act.mk_lit (A.mk_eq self.tst t u) ] proof @@ -376,16 +353,18 @@ module Make (A : ARG) : S with module A = A = struct | _ -> () (* remember terms of a datatype *) - let on_new_term_look_at_ty (self : t) n (t : T.t) : unit = - let ty = T.ty t in + let on_new_term_look_at_ty (self : t) n (t : Term.t) : unit = + let ty = Term.ty t in match A.as_datatype ty with | Ty_data _ -> Log.debugf 20 (fun k -> - k "(@[%s.on-new-term.has-data-ty@ %a@ :ty %a@])" name T.pp t Ty.pp ty); + k "(@[%s.on-new-term.has-data-ty@ %a@ :ty %a@])" name Term.pp_debug t + Term.pp_debug ty); if Card.is_finite self.cards ty && not (N_tbl.mem self.to_decide n) then ( (* must decide this term *) Log.debugf 20 (fun k -> - k "(@[%s.on-new-term.must-decide-finite-ty@ %a@])" name T.pp t); + k "(@[%s.on-new-term.must-decide-finite-ty@ %a@])" name + Term.pp_debug t); N_tbl.add self.to_decide n () ) else if (not (N_tbl.mem self.to_decide n)) @@ -395,13 +374,13 @@ module Make (A : ARG) : S with module A = A = struct N_tbl.add self.to_decide_for_complete_model n () | _ -> () - let on_new_term (self : t) ((cc, n, t) : _ * N.t * T.t) : _ list = + let on_new_term (self : t) ((cc, n, t) : _ * E_node.t * Term.t) : _ list = on_new_term_look_at_ty self n t; (* might have to decide [t] *) match A.view_as_data t with | T_is_a (c_t, u) -> - let n_u = SI.CC.add_term cc u in - let repr_u = SI.CC.find cc n_u in + let n_u = CC.add_term cc u in + let repr_u = CC.find cc n_u in (match ST_cstors.get self.cstors repr_u with | None -> (* needs to be decided *) @@ -413,41 +392,49 @@ module Make (A : ARG) : S with module A = A = struct k "(@[%s.on-new-term.is-a.reduce@ :t %a@ :to %B@ :n %a@ :sub-cstor \ %a@])" - name T.pp t is_true N.pp n Monoid_cstor.pp cstor); + name Term.pp_debug t is_true E_node.pp n Monoid_cstor.pp cstor); let pr = - Pr.add_step self.proof - @@ A.P.lemma_isa_cstor ~cstor_t:(N.term cstor.c_n) t + Proof_trace.add_step self.proof + @@ A.P.lemma_isa_cstor ~cstor_t:(E_node.term cstor.c_n) t in - let n_bool = SI.CC.n_bool cc is_true in + let n_bool = CC.n_bool cc is_true in let expl = Expl.( - mk_theory (N.term n) (N.term n_bool) - [ N.term n_u, N.term cstor.c_n, [ mk_merge n_u cstor.c_n ] ] + mk_theory (E_node.term n) (E_node.term n_bool) + [ + ( E_node.term n_u, + E_node.term cstor.c_n, + [ mk_merge n_u cstor.c_n ] ); + ] pr) in - let a = SI.CC.Handler_action.Act_merge (n, n_bool, expl) in + let a = CC.Handler_action.Act_merge (n, n_bool, expl) in [ a ]) | T_select (c_t, i, u) -> - let n_u = SI.CC.add_term cc u in - let repr_u = SI.CC.find cc n_u in + let n_u = CC.add_term cc u in + let repr_u = CC.find cc n_u in (match ST_cstors.get self.cstors repr_u with | Some cstor when A.Cstor.equal cstor.c_cstor c_t -> Log.debugf 5 (fun k -> k "(@[%s.on-new-term.select.reduce@ :n %a@ :sel get[%d]-%a@])" name - N.pp n i A.Cstor.pp c_t); + E_node.pp n i A.Cstor.pp c_t); assert (i < CCArray.length cstor.c_args); let u_i = CCArray.get cstor.c_args i in let pr = - Pr.add_step self.proof - @@ A.P.lemma_select_cstor ~cstor_t:(N.term cstor.c_n) t + Proof_trace.add_step self.proof + @@ A.P.lemma_select_cstor ~cstor_t:(E_node.term cstor.c_n) t in let expl = Expl.( - mk_theory (N.term n) (N.term u_i) - [ N.term n_u, N.term cstor.c_n, [ mk_merge n_u cstor.c_n ] ] + mk_theory (E_node.term n) (E_node.term u_i) + [ + ( E_node.term n_u, + E_node.term cstor.c_n, + [ mk_merge n_u cstor.c_n ] ); + ] pr) in - [ SI.CC.Handler_action.Act_merge (n, u_i, expl) ] + [ CC.Handler_action.Act_merge (n, u_i, expl) ] | Some _ -> [] | None -> (* needs to be decided *) @@ -455,12 +442,12 @@ module Make (A : ARG) : S with module A = A = struct []) | T_cstor _ | T_other _ -> [] - let cstors_of_ty (ty : Ty.t) : A.Cstor.t Iter.t = + let cstors_of_ty (ty : ty) : A.Cstor.t Iter.t = match A.as_datatype ty with | Ty_data { cstors } -> cstors | _ -> assert false - let on_pre_merge (self : t) (cc, n1, n2, expl) : _ result = + let on_pre_merge (self : t) (cc, n1, n2, _expl) : _ result = let acts = ref [] in let merge_is_a n1 (c1 : Monoid_cstor.t) n2 (is_a2 : Monoid_parents.is_a) = let is_true = A.Cstor.equal c1.c_cstor is_a2.is_a_cstor in @@ -468,18 +455,19 @@ module Make (A : ARG) : S with module A = A = struct k "(@[%s.on-merge.is-a.reduce@ %a@ :to %B@ :n1 %a@ :n2 %a@ \ :sub-cstor %a@])" - name Monoid_parents.pp_is_a is_a2 is_true N.pp n1 N.pp n2 + name Monoid_parents.pp_is_a is_a2 is_true E_node.pp n1 E_node.pp n2 Monoid_cstor.pp c1); let pr = - Pr.add_step self.proof - @@ A.P.lemma_isa_cstor ~cstor_t:(N.term c1.c_n) (N.term is_a2.is_a_n) + Proof_trace.add_step self.proof + @@ A.P.lemma_isa_cstor ~cstor_t:(E_node.term c1.c_n) + (E_node.term is_a2.is_a_n) in - let n_bool = SI.CC.n_bool cc is_true in + let n_bool = CC.n_bool cc is_true in let expl = - Expl.mk_theory (N.term is_a2.is_a_n) (N.term n_bool) + Expl.mk_theory (E_node.term is_a2.is_a_n) (E_node.term n_bool) [ - ( N.term n1, - N.term n2, + ( E_node.term n1, + E_node.term n2, [ Expl.mk_merge n1 c1.c_n; Expl.mk_merge n1 n2; @@ -488,7 +476,7 @@ module Make (A : ARG) : S with module A = A = struct ] pr in - let act = SI.CC.Handler_action.Act_merge (is_a2.is_a_n, n_bool, expl) in + let act = CC.Handler_action.Act_merge (is_a2.is_a_n, n_bool, expl) in acts := act :: !acts in let merge_select n1 (c1 : Monoid_cstor.t) n2 (sel2 : Monoid_parents.select) @@ -496,18 +484,19 @@ module Make (A : ARG) : S with module A = A = struct if A.Cstor.equal c1.c_cstor sel2.sel_cstor then ( Log.debugf 5 (fun k -> k "(@[%s.on-merge.select.reduce@ :n2 %a@ :sel get[%d]-%a@])" name - N.pp n2 sel2.sel_idx Monoid_cstor.pp c1); + E_node.pp n2 sel2.sel_idx Monoid_cstor.pp c1); assert (sel2.sel_idx < CCArray.length c1.c_args); let pr = - Pr.add_step self.proof - @@ A.P.lemma_select_cstor ~cstor_t:(N.term c1.c_n) (N.term sel2.sel_n) + Proof_trace.add_step self.proof + @@ A.P.lemma_select_cstor ~cstor_t:(E_node.term c1.c_n) + (E_node.term sel2.sel_n) in let u_i = CCArray.get c1.c_args sel2.sel_idx in let expl = - Expl.mk_theory (N.term sel2.sel_n) (N.term u_i) + Expl.mk_theory (E_node.term sel2.sel_n) (E_node.term u_i) [ - ( N.term n1, - N.term n2, + ( E_node.term n1, + E_node.term n2, [ Expl.mk_merge n1 c1.c_n; Expl.mk_merge n1 n2; @@ -516,7 +505,7 @@ module Make (A : ARG) : S with module A = A = struct ] pr in - let act = SI.CC.Handler_action.Act_merge (sel2.sel_n, u_i, expl) in + let act = CC.Handler_action.Act_merge (sel2.sel_n, u_i, expl) in acts := act :: !acts ) in @@ -528,7 +517,8 @@ module Make (A : ARG) : S with module A = A = struct k "(@[%s.pre-merge@ (@[:n1 %a@ :c1 %a@])@ (@[:n2 %a@ :p2 \ %a@])@])" - name N.pp n1 Monoid_cstor.pp c1 N.pp n2 Monoid_parents.pp p2); + name E_node.pp n1 Monoid_cstor.pp c1 E_node.pp n2 + Monoid_parents.pp p2); List.iter (fun is_a2 -> merge_is_a n1 c1 n2 is_a2) p2.parent_is_a; List.iter (fun s2 -> merge_select n1 c1 n2 s2) p2.parent_select in @@ -537,13 +527,13 @@ module Make (A : ARG) : S with module A = A = struct Ok !acts module Acyclicity_ = struct - type repr = N.t + type repr = E_node.t (* a node, corresponding to a class that has a constructor element. *) type node = { - repr: N.t; (* repr *) - cstor_n: N.t; (* the cstor node *) - cstor_args: (N.t * repr) list; (* arguments to [cstor_n] *) + repr: E_node.t; (* repr *) + cstor_n: E_node.t; (* the cstor node *) + cstor_args: (E_node.t * repr) list; (* arguments to [cstor_n] *) mutable flag: flag; } @@ -554,15 +544,17 @@ module Make (A : ARG) : S with module A = A = struct let pp_node out (n : node) = Fmt.fprintf out "(@[node@ :repr %a@ :cstor_n %a@ @[:cstor_args %a@]@])" - N.pp n.repr N.pp n.cstor_n - Fmt.(Dump.list @@ hvbox @@ pair ~sep:(return "@ --> ") N.pp N.pp) + E_node.pp n.repr E_node.pp n.cstor_n + Fmt.( + Dump.list @@ hvbox @@ pair ~sep:(return "@ --> ") E_node.pp E_node.pp) n.cstor_args - let pp_path = Fmt.Dump.(list @@ pair N.pp pp_node) + let pp_path = Fmt.Dump.(list @@ pair E_node.pp pp_node) let pp_graph out (g : graph) : unit = let pp_entry out (n, node) = - Fmt.fprintf out "@[<1>@[graph_node[%a]@]@ := %a@]" N.pp n pp_node node + Fmt.fprintf out "@[<1>@[graph_node[%a]@]@ := %a@]" E_node.pp n pp_node + node in if N_tbl.length g = 0 then Fmt.string out "(graph ø)" @@ -573,12 +565,12 @@ module Make (A : ARG) : S with module A = A = struct let g : graph = N_tbl.create ~size:32 () in let traverse_sub cstor : _ list = Util.array_to_list_map - (fun sub_n -> sub_n, SI.CC.find cc sub_n) + (fun sub_n -> sub_n, CC.find cc sub_n) cstor.Monoid_cstor.c_args in (* populate tbl with [repr->node] *) ST_cstors.iter_all self.cstors (fun (repr, cstor) -> - assert (N.is_root repr); + assert (E_node.is_root repr); assert (not @@ N_tbl.mem g repr); let node = { @@ -597,8 +589,8 @@ module Make (A : ARG) : S with module A = A = struct let g = mk_graph self cc in Log.debugf 50 (fun k -> k "(@[%s.acyclicity.graph@ %a@])" name pp_graph g); (* traverse the graph, looking for cycles *) - let rec traverse ~path (n : N.t) (r : repr) : unit = - assert (N.is_root r); + let rec traverse ~path (n : E_node.t) (r : repr) : unit = + assert (E_node.is_root r); match N_tbl.find g r with | exception Not_found -> () | { flag = Done; _ } -> () (* no need *) @@ -606,24 +598,24 @@ module Make (A : ARG) : S with module A = A = struct (* conflict: the [path] forms a cycle *) let path = (n, node) :: path in let pr = - Pr.add_step self.proof + Proof_trace.add_step self.proof @@ A.P.lemma_acyclicity (Iter.of_list path - |> Iter.map (fun (a, b) -> N.term a, N.term b.repr)) + |> Iter.map (fun (a, b) -> E_node.term a, E_node.term b.repr)) in let expl = let subs = CCList.map (fun (n, node) -> - ( N.term n, - N.term node.cstor_n, + ( E_node.term n, + E_node.term node.cstor_n, [ Expl.mk_merge node.cstor_n node.repr; Expl.mk_merge n node.repr; ] )) path in - Expl.mk_theory (N.term n) (N.term cstor_n) subs pr + Expl.mk_theory (E_node.term n) (E_node.term cstor_n) subs pr in Stat.incr self.stat_acycl_conflict; Log.debugf 5 (fun k -> @@ -631,7 +623,7 @@ module Make (A : ARG) : S with module A = A = struct expl pp_path path); let lits, pr = SI.cc_resolve_expl solver expl in (* negate lits *) - let c = List.rev_map SI.Lit.neg lits in + let c = List.rev_map Lit.neg lits in SI.raise_conflict solver acts c pr | { flag = New; _ } as node_r -> node_r.flag <- Open; @@ -645,11 +637,11 @@ module Make (A : ARG) : S with module A = A = struct () end - let check_is_a self solver acts trail = + let check_is_a self solver _acts trail = let check_lit lit = - let t = SI.Lit.term lit in + let t = Lit.term lit in match A.view_as_data t with - | T_is_a (c, u) when SI.Lit.sign lit -> + | T_is_a (c, u) when Lit.sign lit -> (* add [((_ is C) u) ==> u = C(sel-c-0 u, …, sel-c-k u)] *) let rhs = let args = @@ -660,43 +652,42 @@ module Make (A : ARG) : S with module A = A = struct A.mk_cstor self.tst c args in Log.debugf 50 (fun k -> - k "(@[%s.assign-is-a@ :lhs %a@ :rhs %a@ :lit %a@])" name T.pp u T.pp - rhs SI.Lit.pp lit); - let pr = Pr.add_step self.proof @@ A.P.lemma_isa_sel t in + k "(@[%s.assign-is-a@ :lhs %a@ :rhs %a@ :lit %a@])" name + Term.pp_debug u Term.pp_debug rhs Lit.pp lit); + let pr = Proof_trace.add_step self.proof @@ A.P.lemma_isa_sel t in (* merge [u] and [rhs] *) - SI.CC.merge_t (SI.cc solver) u rhs + CC.merge_t (SI.cc solver) u rhs (Expl.mk_theory u rhs - [ t, N.term (SI.CC.n_true @@ SI.cc solver), [ Expl.mk_lit lit ] ] + [ t, E_node.term (CC.n_true @@ SI.cc solver), [ Expl.mk_lit lit ] ] pr) | _ -> () in Iter.iter check_lit trail (* add clauses [\Or_c is-c(n)] and [¬(is-a n) ∨ ¬(is-b n)] *) - let decide_class_ (self : t) (solver : SI.t) acts (n : N.t) : unit = - let t = N.term n in + let decide_class_ (self : t) (solver : SI.t) acts (n : E_node.t) : unit = + let t = E_node.term n in (* [t] might have been expanded already, in case of duplicates in [l] *) - if not @@ T.Tbl.mem self.case_split_done t then ( - T.Tbl.add self.case_split_done t (); + if not @@ Term.Tbl.mem self.case_split_done t then ( + Term.Tbl.add self.case_split_done t (); let c = - cstors_of_ty (T.ty t) + cstors_of_ty (Term.ty t) |> Iter.map (fun c -> A.mk_is_a self.tst c t) |> Iter.map (fun t -> - let lit = SI.mk_lit solver acts t in + let lit = SI.mk_lit solver t in (* TODO: set default polarity, depending on n° of args? *) lit) |> Iter.to_rev_list in SI.add_clause_permanent solver acts c - (Pr.add_step self.proof @@ A.P.lemma_isa_split t (Iter.of_list c)); + (Proof_trace.add_step self.proof + @@ A.P.lemma_isa_split t (Iter.of_list c)); Iter.diagonal_l c (fun (l1, l2) -> let pr = - Pr.add_step self.proof - @@ A.P.lemma_isa_disj (SI.Lit.neg l1) (SI.Lit.neg l2) + Proof_trace.add_step self.proof + @@ A.P.lemma_isa_disj (Lit.neg l1) (Lit.neg l2) in - SI.add_clause_permanent solver acts - [ SI.Lit.neg l1; SI.Lit.neg l2 ] - pr) + SI.add_clause_permanent solver acts [ Lit.neg l1; Lit.neg l2 ] pr) ) (* on final check, check acyclicity, @@ -716,7 +707,7 @@ module Make (A : ARG) : S with module A = A = struct |> Iter.map (fun (n, _) -> SI.cc_find solver n) |> Iter.filter (fun n -> (not (ST_cstors.mem self.cstors n)) - && not (T.Tbl.mem self.case_split_done (N.term n))) + && not (Term.Tbl.mem self.case_split_done (E_node.term n))) |> Iter.to_rev_list in (match remaining_to_decide with @@ -727,7 +718,8 @@ module Make (A : ARG) : S with module A = A = struct () | l -> Log.debugf 10 (fun k -> - k "(@[%s.final-check.must-decide@ %a@])" name (Util.pp_list N.pp) l); + k "(@[%s.final-check.must-decide@ %a@])" name (Util.pp_list E_node.pp) + l); Profile.instant "data.case-split"; List.iter (decide_class_ self solver acts) l); @@ -736,21 +728,22 @@ module Make (A : ARG) : S with module A = A = struct N_tbl.to_iter self.to_decide_for_complete_model |> Iter.map (fun (n, _) -> SI.cc_find solver n) |> Iter.filter (fun n -> - (not (T.Tbl.mem self.case_split_done (N.term n))) + (not (Term.Tbl.mem self.case_split_done (E_node.term n))) && not (ST_cstors.mem self.cstors n)) |> Iter.head in match next_decision with | None -> () (* all decided *) | Some n -> - let t = N.term n in + let t = E_node.term n in Profile.instant "data.decide"; (* use a constructor that will not lead to an infinite loop *) let base_cstor = - match Card.base_cstor self.cards (T.ty t) with - | None -> Error.errorf "th-data:@ %a should have base cstor" N.pp n + match Card.base_cstor self.cards (Term.ty t) with + | None -> + Error.errorf "th-data:@ %a should have base cstor" E_node.pp n | Some c -> c in let cstor_app = @@ -763,16 +756,18 @@ module Make (A : ARG) : S with module A = A = struct in let t_eq_cstor = A.mk_eq self.tst t cstor_app in Log.debugf 20 (fun k -> - k "(@[th-data.final-check.model.decide-cstor@ %a@])" T.pp t_eq_cstor); - let lit = SI.mk_lit solver acts t_eq_cstor in + k "(@[th-data.final-check.model.decide-cstor@ %a@])" Term.pp_debug + t_eq_cstor); + let lit = SI.mk_lit solver t_eq_cstor in SI.push_decision solver acts lit ); () - let on_model_gen (self : t) ~recurse (si : SI.t) (n : N.t) : T.t option = + let on_model_gen (self : t) ~recurse (si : SI.t) (n : E_node.t) : + Term.t option = (* TODO: option to complete model or not (by picking sth at leaves)? *) let cc = SI.cc si in - let repr = SI.CC.find cc n in + let repr = CC.find cc n in match ST_cstors.get self.cstors repr with | None -> None | Some c -> @@ -791,8 +786,8 @@ module Make (A : ARG) : S with module A = A = struct parents = ST_parents.create_and_setup ~size:32 (SI.cc solver); to_decide = N_tbl.create ~size:16 (); to_decide_for_complete_model = N_tbl.create ~size:16 (); - single_cstor_preproc_done = T.Tbl.create 8; - case_split_done = T.Tbl.create 16; + single_cstor_preproc_done = Term.Tbl.create 8; + case_split_done = Term.Tbl.create 16; cards = Card.create (); stat_acycl_conflict = Stat.mk_int (SI.stats solver) "data.acycl.conflict"; @@ -807,5 +802,10 @@ module Make (A : ARG) : S with module A = A = struct SI.on_model solver ~ask:(on_model_gen self); self - let theory = A.S.mk_theory ~name ~push_level ~pop_levels ~create_and_setup () + let theory = + SMT.Solver.mk_theory ~name ~push_level ~pop_levels ~create_and_setup () end + +let make (module A : ARG) = + let module M = Make (A) in + M.theory diff --git a/src/th-data/Sidekick_th_data.mli b/src/th-data/Sidekick_th_data.mli index ce347744..3149f15a 100644 --- a/src/th-data/Sidekick_th_data.mli +++ b/src/th-data/Sidekick_th_data.mli @@ -2,11 +2,4 @@ include module type of Th_intf -module type S = sig - module A : ARG - - val theory : A.S.theory - (** A theory that can be added to {!A.S} to perform datatype reasoning. *) -end - -module Make (A : ARG) : S with module A = A +val make : (module ARG) -> SMT.theory diff --git a/src/th-data/dune b/src/th-data/dune index 8f959c7e..ecc7dbb3 100644 --- a/src/th-data/dune +++ b/src/th-data/dune @@ -1,7 +1,8 @@ (library (name Sidekick_th_data) (public_name sidekick.th-data) - (libraries containers sidekick.sigs.smt sidekick.util sidekick.cc.plugin) - (flags :standard -open Sidekick_util -w -27-32)) + (libraries containers sidekick.core sidekick.util sidekick.cc + sidekick.smt-solver) + (flags :standard -open Sidekick_util -w +32)) ; TODO get warning back diff --git a/src/th-data/th_intf.ml b/src/th-data/th_intf.ml index aa1360d4..1004e5b0 100644 --- a/src/th-data/th_intf.ml +++ b/src/th-data/th_intf.ml @@ -1,4 +1,7 @@ -open Sidekick_sigs_smt +open Sidekick_core +module SMT = Sidekick_smt_solver + +type ty = Term.t (** Datatype-oriented view of terms. @@ -19,46 +22,54 @@ type ('c, 'ty) data_ty_view = | Ty_other module type PROOF_RULES = sig - type term - type lit - type rule - - val lemma_isa_cstor : cstor_t:term -> term -> rule + val lemma_isa_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t (** [lemma_isa_cstor (d …) (is-c t)] returns the clause [(c …) = t |- is-c t] or [(d …) = t |- ¬ (is-c t)] *) - val lemma_select_cstor : cstor_t:term -> term -> rule + val lemma_select_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t (** [lemma_select_cstor (c t1…tn) (sel-c-i t)] returns a proof of [t = c t1…tn |- (sel-c-i t) = ti] *) - val lemma_isa_split : term -> lit Iter.t -> rule + val lemma_isa_split : Term.t -> Lit.t Iter.t -> Proof_term.t (** [lemma_isa_split t lits] is the proof of [is-c1 t \/ is-c2 t \/ … \/ is-c_n t] *) - val lemma_isa_sel : term -> rule + val lemma_isa_sel : Term.t -> Proof_term.t (** [lemma_isa_sel (is-c t)] is the proof of [is-c t |- t = c (sel-c-1 t)…(sel-c-n t)] *) - val lemma_isa_disj : lit -> lit -> rule + val lemma_isa_disj : Lit.t -> Lit.t -> Proof_term.t (** [lemma_isa_disj (is-c t) (is-d t)] is the proof of [¬ (is-c t) \/ ¬ (is-c t)] *) - val lemma_cstor_inj : term -> term -> int -> rule + val lemma_cstor_inj : Term.t -> Term.t -> int -> Proof_term.t (** [lemma_cstor_inj (c t1…tn) (c u1…un) i] is the proof of [c t1…tn = c u1…un |- ti = ui] *) - val lemma_cstor_distinct : term -> term -> rule + val lemma_cstor_distinct : Term.t -> Term.t -> Proof_term.t (** [lemma_isa_distinct (c …) (d …)] is the proof of the unit clause [|- (c …) ≠ (d …)] *) - val lemma_acyclicity : (term * term) Iter.t -> rule + val lemma_acyclicity : (Term.t * Term.t) Iter.t -> Proof_term.t (** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false] by acyclicity. *) end -module type ARG = sig - module S : SOLVER +(* TODO: remove? or make compute_card use that? *) +(** An abtract representation of a datatype *) +module type DATA_TY = sig + type t + type cstor + + val equal : t -> t -> bool + val finite : t -> bool + val set_finite : t -> bool -> unit + val view : t -> (cstor, t) data_ty_view + val cstor_args : cstor -> t Iter.t +end + +module type ARG = sig (** Constructor symbols. A constructor is an injective symbol, part of a datatype (or "sum type"). @@ -68,43 +79,37 @@ module type ARG = sig type t (** Constructor *) - val ty_args : t -> S.T.Ty.t Iter.t + val ty_args : t -> ty Iter.t (** Type arguments, for a polymorphic constructor *) - val pp : t Fmt.printer - - val equal : t -> t -> bool - (** Comparison *) + include Sidekick_sigs.EQ with type t := t + include Sidekick_sigs.PRINT with type t := t end - val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view + val as_datatype : ty -> (Cstor.t Iter.t, ty) data_ty_view (** Try to view type as a datatype (with its constructors) *) - val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view - (** Try to view term as a datatype term *) + val view_as_data : Term.t -> (Cstor.t, Term.t) data_view + (** Try to view Term.t as a datatype Term.t *) - val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t array -> S.T.Term.t - (** Make a constructor application term *) + val mk_cstor : Term.store -> Cstor.t -> Term.t array -> Term.t + (** Make a constructor application Term.t *) - val mk_is_a : S.T.Term.store -> Cstor.t -> S.T.Term.t -> S.T.Term.t - (** Make a [is-a] term *) + val mk_is_a : Term.store -> Cstor.t -> Term.t -> Term.t + (** Make a [is-a] Term.t *) - val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t - (** Make a selector term *) + val mk_sel : Term.store -> Cstor.t -> int -> Term.t -> Term.t + (** Make a selector Term.t *) - val mk_eq : S.T.Term.store -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t - (** Make a term equality *) + val mk_eq : Term.store -> Term.t -> Term.t -> Term.t + (** Make a Term.t equality *) - val ty_is_finite : S.T.Ty.t -> bool + val ty_is_finite : ty -> bool (** Is the given type known to be finite? For example a finite datatype (an "enum" in C parlance), or [Bool], or [Array Bool Bool]. *) - val ty_set_is_finite : S.T.Ty.t -> bool -> unit + val ty_set_is_finite : ty -> bool -> unit (** Modify the "finite" field (see {!ty_is_finite}) *) - module P : - PROOF_RULES - with type rule = S.Proof_trace.A.rule - and type term = S.T.Term.t - and type lit = S.Lit.t + module P : PROOF_RULES end diff --git a/src/th-lra/intf.ml b/src/th-lra/intf.ml new file mode 100644 index 00000000..c9b60c30 --- /dev/null +++ b/src/th-lra/intf.ml @@ -0,0 +1,59 @@ +open Sidekick_core +module SMT = Sidekick_smt_solver +module Predicate = Sidekick_simplex.Predicate +module Linear_expr = Sidekick_simplex.Linear_expr +module Linear_expr_intf = Sidekick_simplex.Linear_expr_intf + +module type INT = Sidekick_arith.INT +module type RATIONAL = Sidekick_arith.RATIONAL + +module S_op = Sidekick_simplex.Op + +type term = Term.t +type ty = Term.t +type pred = Linear_expr_intf.bool_op = Leq | Geq | Lt | Gt | Eq | Neq +type op = Linear_expr_intf.op = Plus | Minus + +type ('num, 'a) lra_view = + | LRA_pred of pred * 'a * 'a + | LRA_op of op * 'a * 'a + | LRA_mult of 'num * 'a + | LRA_const of 'num + | LRA_other of 'a + +let map_view f (l : _ lra_view) : _ lra_view = + match l with + | LRA_pred (p, a, b) -> LRA_pred (p, f a, f b) + | LRA_op (p, a, b) -> LRA_op (p, f a, f b) + | LRA_mult (n, a) -> LRA_mult (n, f a) + | LRA_const q -> LRA_const q + | LRA_other x -> LRA_other (f x) + +module type ARG = sig + module Z : INT + module Q : RATIONAL with type bigint = Z.t + + val view_as_lra : Term.t -> (Q.t, Term.t) lra_view + (** Project the Term.t into the theory view *) + + val mk_lra : Term.store -> (Q.t, Term.t) lra_view -> Term.t + (** Make a Term.t from the given theory view *) + + val ty_lra : Term.store -> ty + + val has_ty_real : Term.t -> bool + (** Does this term have the type [Real] *) + + val lemma_lra : Lit.t Iter.t -> Proof_term.t + + module Gensym : sig + type t + + val create : Term.store -> t + val tst : t -> Term.store + val copy : t -> t + + val fresh_term : t -> pre:string -> ty -> term + (** Make a fresh term of the given type *) + end +end diff --git a/src/th-lra/sidekick_arith_lra.ml b/src/th-lra/sidekick_arith_lra.ml index 5c05ceff..80bd87cd 100644 --- a/src/th-lra/sidekick_arith_lra.ml +++ b/src/th-lra/sidekick_arith_lra.ml @@ -1,140 +1,49 @@ -(** Linear Rational Arithmetic *) - (* Reference: http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LRA *) open Sidekick_core -module SMT = Sidekick_smt_solver -module Predicate = Sidekick_simplex.Predicate -module Linear_expr = Sidekick_simplex.Linear_expr -module Linear_expr_intf = Sidekick_simplex.Linear_expr_intf +open Sidekick_cc +module Intf = Intf +open Intf +module SI = SMT.Solver_internal -module type INT = Sidekick_arith.INT -module type RATIONAL = Sidekick_arith.RATIONAL +module type ARG = Intf.ARG -module S_op = Sidekick_simplex.Op +module Tag = struct + type t = Lit of Lit.t | CC_eq of E_node.t * E_node.t -type term = Term.t -type ty = Term.t -type pred = Linear_expr_intf.bool_op = Leq | Geq | Lt | Gt | Eq | Neq -type op = Linear_expr_intf.op = Plus | Minus + let pp out = function + | Lit l -> Fmt.fprintf out "(@[lit %a@])" Lit.pp l + | CC_eq (n1, n2) -> + Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" E_node.pp n1 E_node.pp n2 -type ('num, 'a) lra_view = - | LRA_pred of pred * 'a * 'a - | LRA_op of op * 'a * 'a - | LRA_mult of 'num * 'a - | LRA_const of 'num - | LRA_other of 'a - -let map_view f (l : _ lra_view) : _ lra_view = - match l with - | LRA_pred (p, a, b) -> LRA_pred (p, f a, f b) - | LRA_op (p, a, b) -> LRA_op (p, f a, f b) - | LRA_mult (n, a) -> LRA_mult (n, f a) - | LRA_const q -> LRA_const q - | LRA_other x -> LRA_other (f x) - -module type ARG = sig - module Z : INT - module Q : RATIONAL with type bigint = Z.t - - val view_as_lra : Term.t -> (Q.t, Term.t) lra_view - (** Project the Term.t into the theory view *) - - val mk_lra : Term.store -> (Q.t, Term.t) lra_view -> Term.t - (** Make a Term.t from the given theory view *) - - val ty_lra : Term.store -> ty - - val has_ty_real : Term.t -> bool - (** Does this term have the type [Real] *) - - val lemma_lra : Lit.t Iter.t -> Proof_term.t - - module Gensym : sig - type t - - val create : Term.store -> t - val tst : t -> Term.store - val copy : t -> t - - val fresh_term : t -> pre:string -> ty -> term - (** Make a fresh term of the given type *) - end + let to_lits si = function + | Lit l -> [ l ] + | CC_eq (n1, n2) -> + let r = CC.explain_eq (SI.cc si) n1 n2 in + (* FIXME + assert (not (SI.CC.Resolved_expl.is_semantic r)); + *) + r.lits end -module type S = sig - module A : ARG +module SimpVar : Linear_expr.VAR with type t = Term.t and type lit = Tag.t = +struct + type t = Term.t - (* - module SimpVar : Sidekick_simplex.VAR with type lit = A.Lit.t - module LE_ : Linear_expr_intf.S with module Var = SimpVar - module LE = LE_.Expr - *) + let pp = Term.pp_debug + let compare = Term.compare - module SimpSolver : Sidekick_simplex.S - (** Simplexe *) + type lit = Tag.t - type state + let pp_lit = Tag.pp - val create : ?stat:Stat.t -> SMT.Solver_internal.t -> state - - (* TODO: be able to declare some variables as ints *) - - (* - val simplex : state -> Simplex.t - *) - - val k_state : state SMT.Registry.key - (** Key to access the state from outside, - available when the theory has been setup *) - - val theory : SMT.Theory.t + let not_lit = function + | Tag.Lit l -> Some (Tag.Lit (Lit.neg l)) + | _ -> None end module Make (A : ARG) = (* : S with module A = A *) struct - module A = A - module SI = SMT.Solver_internal - open Sidekick_cc - - open struct - module Pr = Proof_trace - end - - module Tag = struct - type t = Lit of Lit.t | CC_eq of E_node.t * E_node.t - - let pp out = function - | Lit l -> Fmt.fprintf out "(@[lit %a@])" Lit.pp l - | CC_eq (n1, n2) -> - Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" E_node.pp n1 E_node.pp n2 - - let to_lits si = function - | Lit l -> [ l ] - | CC_eq (n1, n2) -> - let r = CC.explain_eq (SI.cc si) n1 n2 in - (* FIXME - assert (not (SI.CC.Resolved_expl.is_semantic r)); - *) - r.lits - end - - module SimpVar : Linear_expr.VAR with type t = Term.t and type lit = Tag.t = - struct - type t = Term.t - - let pp = Term.pp_debug - let compare = Term.compare - - type lit = Tag.t - - let pp_lit = Tag.pp - - let not_lit = function - | Tag.Lit l -> Some (Tag.Lit (Lit.neg l)) - | _ -> None - end - module LE_ = Linear_expr.Make (A.Q) (SimpVar) module LE = LE_.Expr @@ -339,12 +248,12 @@ module Make (A : ARG) = (* : S with module A = A *) struct proxy) let add_clause_lra_ ?using (module PA : SI.PREPROCESS_ACTS) lits = - let pr = Pr.add_step PA.proof @@ A.lemma_lra (Iter.of_list lits) in + let pr = Proof_trace.add_step PA.proof @@ A.lemma_lra (Iter.of_list lits) in let pr = match using with | None -> pr | Some using -> - Pr.add_step PA.proof + Proof_trace.add_step PA.proof @@ Proof_core.lemma_rw_clause pr ~res:(Iter.of_list lits) ~using in PA.add_clause lits pr @@ -487,12 +396,12 @@ module Make (A : ARG) = (* : S with module A = A *) struct let simplify (self : state) (_recurse : _) (t : Term.t) : (Term.t * Proof_step.id Iter.t) option = let proof_eq t u = - Pr.add_step self.proof + Proof_trace.add_step self.proof @@ A.lemma_lra (Iter.return (Lit.atom (Term.eq self.tst t u))) in let proof_bool t ~sign:b = let lit = Lit.atom ~sign:b t in - Pr.add_step self.proof @@ A.lemma_lra (Iter.return lit) + Proof_trace.add_step self.proof @@ A.lemma_lra (Iter.return lit) in match A.view_as_lra t with @@ -557,7 +466,9 @@ module Make (A : ARG) = (* : S with module A = A *) struct |> CCList.flat_map (Tag.to_lits si) |> List.rev_map Lit.neg in - let pr = Pr.add_step (SI.proof si) @@ A.lemma_lra (Iter.of_list confl) in + let pr = + Proof_trace.add_step (SI.proof si) @@ A.lemma_lra (Iter.of_list confl) + in SI.raise_conflict si acts confl pr let on_propagate_ si acts lit ~reason = @@ -567,7 +478,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct SI.propagate si acts lit ~reason:(fun () -> let lits = CCList.flat_map (Tag.to_lits si) reason in let pr = - Pr.add_step (SI.proof si) + Proof_trace.add_step (SI.proof si) @@ A.lemma_lra Iter.(cons lit (of_list lits)) in CCList.flat_map (Tag.to_lits si) reason, pr) @@ -613,7 +524,9 @@ module Make (A : ARG) = (* : S with module A = A *) struct if A.Q.(le_const <> zero) then ( (* [c=0] when [c] is not 0 *) let lit = Lit.atom ~sign:false @@ Term.eq self.tst t1 t2 in - let pr = Pr.add_step self.proof @@ A.lemma_lra (Iter.return lit) in + let pr = + Proof_trace.add_step self.proof @@ A.lemma_lra (Iter.return lit) + in SI.add_clause_permanent si acts [ lit ] pr ) ) else ( @@ -808,3 +721,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct SMT.Solver.mk_theory ~name:"th-lra" ~create_and_setup ~push_level ~pop_levels () end + +let theory (module A : ARG) : SMT.theory = + let module M = Make (A) in + M.theory diff --git a/src/th-lra/sidekick_arith_lra.mli b/src/th-lra/sidekick_arith_lra.mli new file mode 100644 index 00000000..fdb34b33 --- /dev/null +++ b/src/th-lra/sidekick_arith_lra.mli @@ -0,0 +1,26 @@ +(** Linear Rational Arithmetic *) + +module Intf = Intf +open Intf + +module type ARG = Intf.ARG + +(* TODO + type state + + val k_state : state SMT.Registry.key + (** Key to access the state from outside, + available when the theory has been setup *) + + val create : (module ARG) -> ?stat:Stat.t -> SMT.Solver_internal.t -> state + + (* TODO: be able to declare some variables as ints *) + + (* + val simplex : state -> Simplex.t + *) + + val theory_of_state : state -> SMT.Theory.t +*) + +val theory : (module ARG) -> SMT.Theory.t