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

refactor(theories): remove functors

Browse source
This commit is contained in:
Simon Cruanes 2022-07-30 23:01:29 -04:00
parent df9fa11507
commit 0d0751b7d2
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
13 changed files with 502 additions and 528 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

182
src/th-bool-static/Sidekick_th_bool_static.ml
View file

@ -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

11
src/th-bool-static/Sidekick_th_bool_static.mli Normal file
View file

@ -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

3
src/th-bool-static/dune
View file

@ -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))

65
src/th-bool-static/intf.ml Normal file
View file

@ -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

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

@ -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

3
src/th-cstor/dune
View file

@ -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))

358
src/th-data/Sidekick_th_data.ml
View file

@ -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
"(@[<hv>%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

9
src/th-data/Sidekick_th_data.mli
View file

@ -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

5
src/th-data/dune
View file

@ -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

81
src/th-data/th_intf.ml
View file

@ -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

59
src/th-lra/intf.ml Normal file
View file

@ -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

171
src/th-lra/sidekick_arith_lra.ml
View file

@ -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

26
src/th-lra/sidekick_arith_lra.mli Normal file
View file

@ -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