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

move form to sidekick_base; rename {Term,Ty}.state into store

Browse source
This commit is contained in:
Simon Cruanes 2021-07-03 22:48:44 -04:00
parent 80b50e8744
commit 6578ea9136
19 changed files with 111 additions and 107 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/base-solver/sidekick_base_solver.ml
View file

@ -7,8 +7,6 @@
open Sidekick_base open Sidekick_base
module Form = Form
(** Argument to the SMT solver *) (** Argument to the SMT solver *)
module Solver_arg = struct module Solver_arg = struct
module T = Sidekick_base module T = Sidekick_base
@ -98,7 +96,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct
module Gensym = struct module Gensym = struct
type t = { type t = {
tst: T.state; tst: T.store;
mutable fresh: int; mutable fresh: int;
} }

52
src/base/Base_types.ml
View file

@ -270,7 +270,7 @@ let pp_term_view = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:pp_term
(** Types *) (** Types *)
module Ty : sig module Ty : sig
type t = ty type t = ty
type state = unit type store = unit
type view = ty_view = type view = ty_view =
| Ty_bool | Ty_bool
| Ty_real | Ty_real
@ -294,8 +294,8 @@ module Ty : sig
val id : t -> int val id : t -> int
val view : t -> view val view : t -> view
val bool : state -> t val bool : store -> t
val real : state -> t val real : store -> t
val atomic : def -> t list -> t val atomic : def -> t list -> t
val id_of_def : def -> ID.t val id_of_def : def -> ID.t
@ -328,7 +328,7 @@ module Ty : sig
end end
end = struct end = struct
type t = ty type t = ty
type state = unit type store = unit
type view = ty_view = type view = ty_view =
| Ty_bool | Ty_bool
| Ty_real | Ty_real
@ -792,27 +792,27 @@ module Term : sig
val compare : t -> t -> int val compare : t -> t -> int
val hash : t -> int val hash : t -> int
type state type store
val create : ?size:int -> unit -> state val create : ?size:int -> unit -> store
val make : state -> t view -> t val make : store -> t view -> t
val true_ : state -> t val true_ : store -> t
val false_ : state -> t val false_ : store -> t
val bool : state -> bool -> t val bool : store -> bool -> t
val const : state -> fun_ -> t val const : store -> fun_ -> t
val app_fun : state -> fun_ -> t IArray.t -> t val app_fun : store -> fun_ -> t IArray.t -> t
val eq : state -> t -> t -> t val eq : store -> t -> t -> t
val not_ : state -> t -> t val not_ : store -> t -> t
val ite : state -> t -> t -> t -> t val ite : store -> t -> t -> t -> t
val select : state -> select -> t -> t val select : store -> select -> t -> t
val app_cstor : state -> cstor -> t IArray.t -> t val app_cstor : store -> cstor -> t IArray.t -> t
val is_a : state -> cstor -> t -> t val is_a : store -> cstor -> t -> t
val lra : state -> (Q.t,t) lra_view -> t val lra : store -> (Q.t,t) lra_view -> t
(** Obtain unsigned version of [t], + the sign as a boolean *) (** Obtain unsigned version of [t], + the sign as a boolean *)
val abs : state -> t -> t * bool val abs : store -> t -> t * bool
module Iter_dag : sig module Iter_dag : sig
type t type t
@ -824,7 +824,7 @@ module Term : sig
val iter_dag_with : order:Iter_dag.order -> t -> t Iter.t val iter_dag_with : order:Iter_dag.order -> t -> t Iter.t
val iter_dag : t -> t Iter.t val iter_dag : t -> t Iter.t
val map_shallow : state -> (t -> t) -> t -> t val map_shallow : store -> (t -> t) -> t -> t
val pp : t Fmt.printer val pp : t Fmt.printer
@ -877,7 +877,7 @@ end = struct
t.term_id <- id t.term_id <- id
end) end)
type state = { type store = {
tbl : H.t; tbl : H.t;
mutable n: int; mutable n: int;
true_ : t lazy_t; true_ : t lazy_t;
@ -896,7 +896,7 @@ end = struct
let[@inline] false_ st = Lazy.force st.false_ let[@inline] false_ st = Lazy.force st.false_
let bool st b = if b then true_ st else false_ st let bool st b = if b then true_ st else false_ st
let create ?(size=1024) () : state = let create ?(size=1024) () : store =
let rec st ={ let rec st ={
n=2; n=2;
tbl=H.create ~size (); tbl=H.create ~size ();
@ -920,7 +920,7 @@ end = struct
let is_a st c t : t = app_fun st (Fun.is_a c) (IArray.singleton t) let is_a st c t : t = app_fun st (Fun.is_a c) (IArray.singleton t)
let app_cstor st c args : t = app_fun st (Fun.cstor c) args let app_cstor st c args : t = app_fun st (Fun.cstor c) args
let[@inline] lra (st:state) (l:(Q.t,t) lra_view) : t = let[@inline] lra (st:store) (l:(Q.t,t) lra_view) : t =
match l with match l with
| LRA_other x -> x (* normalize *) | LRA_other x -> x (* normalize *)
| _ -> make st (Term_cell.lra l) | _ -> make st (Term_cell.lra l)
@ -930,7 +930,7 @@ end = struct
| Bool false -> true_ tst, false | Bool false -> true_ tst, false
| Not u -> u, false | Not u -> u, false
| App_fun ({fun_view=Fun_def def; _}, args) -> | App_fun ({fun_view=Fun_def def; _}, args) ->
def.abs ~self:t args (* TODO: pass state *) def.abs ~self:t args (* TODO: pass store *)
| LRA (LRA_pred (Neq, a, b)) -> | LRA (LRA_pred (Neq, a, b)) ->
lra tst (LRA_pred (Eq,a,b)), false (* != is just not eq *) lra tst (LRA_pred (Eq,a,b)), false (* != is just not eq *)
| _ -> t, true | _ -> t, true
@ -1001,7 +1001,7 @@ end = struct
let iter_dag t yield = iter_dag_with ~order:Pre t yield let iter_dag t yield = iter_dag_with ~order:Pre t yield
let map_shallow (tst:state) f (t:t) : t = let map_shallow (tst:store) f (t:t) : t =
match view t with match view t with
| Bool _ -> t | Bool _ -> t
| App_fun (hd, a) -> app_fun tst hd (IArray.map f a) | App_fun (hd, a) -> app_fun tst hd (IArray.map f a)

11
src/base-solver/Form.ml → src/base/Form.ml
View file

@ -8,10 +8,13 @@
the formulas are turned into clauses automatically for you. the formulas are turned into clauses automatically for you.
*) *)
open Sidekick_base module T = Base_types.Term
module Ty = Base_types.Ty
module Fun = Base_types.Fun
module Value = Base_types.Value
module T = Term
open Sidekick_th_bool_static open Sidekick_th_bool_static
exception Not_a_th_term exception Not_a_th_term
let id_and = ID.make "and" let id_and = ID.make "and"
@ -83,7 +86,7 @@ module Funs = struct
let and_ = mk_fun id_and let and_ = mk_fun id_and
let or_ = mk_fun id_or let or_ = mk_fun id_or
let imply = mk_fun id_imply let imply = mk_fun id_imply
let ite = Term.ite let ite = T.ite
end end
let as_id id (t:T.t) : T.t IArray.t option = let as_id id (t:T.t) : T.t IArray.t option =
@ -173,7 +176,7 @@ let mk_bool st = function
module Gensym = struct module Gensym = struct
type t = { type t = {
tst: T.state; tst: T.store;
mutable fresh: int; mutable fresh: int;
} }

3
src/base/Sidekick_base.ml
View file

@ -30,6 +30,7 @@ module Statement = Base_types.Statement
module Data = Base_types.Data module Data = Base_types.Data
module Select = Base_types.Select module Select = Base_types.Select
module Proof = Proof module Proof = Proof
module Form = Form
(** Concrete implementation of {!Sidekick_core.TERM} (** Concrete implementation of {!Sidekick_core.TERM}
@ -41,7 +42,7 @@ module Arg
with type Term.t = Term.t with type Term.t = Term.t
and type Fun.t = Fun.t and type Fun.t = Fun.t
and type Ty.t = Ty.t and type Ty.t = Ty.t
and type Term.state = Term.state and type Term.store = Term.store
= struct = struct
module Term = Term module Term = Term
module Fun = Fun module Fun = Fun

3
src/base/dune
View file

@ -2,6 +2,7 @@
(name sidekick_base) (name sidekick_base)
(public_name sidekick-base) (public_name sidekick-base)
(synopsis "Base term definitions for the standalone SMT solver and library") (synopsis "Base term definitions for the standalone SMT solver and library")
(libraries containers sidekick.core sidekick.util sidekick.arith-lra (libraries containers sidekick.core sidekick.util
sidekick.arith-lra sidekick.th-bool-static
sidekick.zarith zarith) sidekick.zarith zarith)
(flags :standard -w -32 -open Sidekick_util)) (flags :standard -w -32 -open Sidekick_util))

8
src/cc/Sidekick_cc.ml
View file

@ -23,7 +23,7 @@ module Make (A: CC_ARG)
module Lit = A.Lit module Lit = A.Lit
module Actions = A.Actions module Actions = A.Actions
type term = T.Term.t type term = T.Term.t
type term_state = T.Term.state type term_store = T.Term.store
type lit = Lit.t type lit = Lit.t
type fun_ = T.Fun.t type fun_ = T.Fun.t
type proof = P.t type proof = P.t
@ -243,7 +243,7 @@ module Make (A: CC_ARG)
| CT_merge of node * node * explanation | CT_merge of node * node * explanation
type t = { type t = {
tst: term_state; tst: term_store;
tbl: node T_tbl.t; tbl: node T_tbl.t;
(* internalization [term -> node] *) (* internalization [term -> node] *)
signatures_tbl : node Sig_tbl.t; signatures_tbl : node Sig_tbl.t;
@ -290,7 +290,7 @@ module Make (A: CC_ARG)
let[@inline] n_true cc = Lazy.force cc.true_ let[@inline] n_true cc = Lazy.force cc.true_
let[@inline] n_false cc = Lazy.force cc.false_ let[@inline] n_false cc = Lazy.force cc.false_
let n_bool cc b = if b then n_true cc else n_false cc let n_bool cc b = if b then n_true cc else n_false cc
let[@inline] term_state cc = cc.tst let[@inline] term_store cc = cc.tst
let allocate_bitfield ~descr cc = let allocate_bitfield ~descr cc =
Log.debugf 5 (fun k->k "(@[cc.allocate-bit-field@ :descr %s@])" descr); Log.debugf 5 (fun k->k "(@[cc.allocate-bit-field@ :descr %s@])" descr);
Bits.mk_field cc.bitgen Bits.mk_field cc.bitgen
@ -907,7 +907,7 @@ module Make (A: CC_ARG)
?(on_pre_merge=[]) ?(on_post_merge=[]) ?(on_new_term=[]) ?(on_pre_merge=[]) ?(on_post_merge=[]) ?(on_new_term=[])
?(on_conflict=[]) ?(on_propagate=[]) ?(on_is_subterm=[]) ?(on_conflict=[]) ?(on_propagate=[]) ?(on_is_subterm=[])
?(size=`Big) ?(size=`Big)
(tst:term_state) : t = (tst:term_store) : t =
let size = match size with `Small -> 128 | `Big -> 2048 in let size = match size with `Small -> 128 | `Big -> 2048 in
let bitgen = Bits.mk_gen () in let bitgen = Bits.mk_gen () in
let field_marked_explain = Bits.mk_field bitgen in let field_marked_explain = Bits.mk_field bitgen in

46
src/core/Sidekick_core.ml
View file

@ -76,9 +76,9 @@ module type TERM = sig
val hash : t -> int val hash : t -> int
val pp : t Fmt.printer val pp : t Fmt.printer
type state type store
val bool : state -> t val bool : store -> t
val is_bool : t -> bool val is_bool : t -> bool
end end
@ -94,19 +94,19 @@ module type TERM = sig
val hash : t -> int val hash : t -> int
val pp : t Fmt.printer val pp : t Fmt.printer
(** A state used to create new terms. It is where the hashconsing (** A store used to create new terms. It is where the hashconsing
table should live, along with other all-terms related state. *) table should live, along with other all-terms related store. *)
type state type store
val ty : t -> Ty.t val ty : t -> Ty.t
val bool : state -> bool -> t (** build true/false *) val bool : store -> bool -> t (** build true/false *)
val as_bool : t -> bool option val as_bool : t -> bool option
(** [as_bool t] is [Some true] if [t] is the term [true], and similarly (** [as_bool t] is [Some true] if [t] is the term [true], and similarly
for [false]. For other terms it is [None]. *) for [false]. For other terms it is [None]. *)
val abs : state -> t -> t * bool val abs : store -> t -> t * bool
(** [abs t] returns an "absolute value" for the term, along with the (** [abs t] returns an "absolute value" for the term, along with the
sign of [t]. sign of [t].
@ -114,9 +114,9 @@ module type TERM = sig
or [(a != b)] into [(a=b, false)]. For terms without a negation this or [(a != b)] into [(a=b, false)]. For terms without a negation this
should return [(t, true)]. should return [(t, true)].
The state is passed in case a new term needs to be created. *) The store is passed in case a new term needs to be created. *)
val map_shallow : state -> (t -> t) -> t -> t val map_shallow : store -> (t -> t) -> t -> t
(** Map function on immediate subterms. This should not be recursive. *) (** Map function on immediate subterms. This should not be recursive. *)
val iter_dag : t -> (t -> unit) -> unit val iter_dag : t -> (t -> unit) -> unit
@ -314,7 +314,7 @@ module type CC_S = sig
module P : PROOF with type term = T.Term.t module P : PROOF with type term = T.Term.t
module Lit : LIT with module T = T module Lit : LIT with module T = T
module Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P module Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P
type term_state = T.Term.state type term_store = T.Term.store
type term = T.Term.t type term = T.Term.t
type fun_ = T.Fun.t type fun_ = T.Fun.t
type lit = Lit.t type lit = Lit.t
@ -402,7 +402,7 @@ module type CC_S = sig
(** {3 Accessors} *) (** {3 Accessors} *)
val term_state : t -> term_state val term_store : t -> term_store
val find : t -> node -> repr val find : t -> node -> repr
(** Current representative *) (** Current representative *)
@ -459,11 +459,11 @@ module type CC_S = sig
?on_propagate:ev_on_propagate list -> ?on_propagate:ev_on_propagate list ->
?on_is_subterm:ev_on_is_subterm list -> ?on_is_subterm:ev_on_is_subterm list ->
?size:[`Small | `Big] -> ?size:[`Small | `Big] ->
term_state -> term_store ->
t t
(** Create a new congruence closure. (** Create a new congruence closure.
@param term_state used to be able to create new terms. All terms @param term_store used to be able to create new terms. All terms
interacting with this congruence closure must belong in this term state interacting with this congruence closure must belong in this term state
as well. *) as well. *)
@ -578,16 +578,16 @@ module type SOLVER_INTERNAL = sig
type ty = T.Ty.t type ty = T.Ty.t
type term = T.Term.t type term = T.Term.t
type term_state = T.Term.state type term_store = T.Term.store
type ty_state = T.Ty.state type ty_store = T.Ty.store
type proof = P.t type proof = P.t
(** {3 Main type for a solver} *) (** {3 Main type for a solver} *)
type t type t
type solver = t type solver = t
val tst : t -> term_state val tst : t -> term_store
val ty_st : t -> ty_state val ty_st : t -> ty_store
val stats : t -> Stat.t val stats : t -> Stat.t
(** {3 Actions for the theories} *) (** {3 Actions for the theories} *)
@ -629,8 +629,8 @@ module type SOLVER_INTERNAL = sig
module Simplify : sig module Simplify : sig
type t type t
val tst : t -> term_state val tst : t -> term_store
val ty_st : t -> ty_state val ty_st : t -> ty_store
val clear : t -> unit val clear : t -> unit
(** Reset internal cache, etc. *) (** Reset internal cache, etc. *)
@ -952,8 +952,8 @@ module type SOLVER = sig
(** {3 Main API} *) (** {3 Main API} *)
val stats : t -> Stat.t val stats : t -> Stat.t
val tst : t -> T.Term.state val tst : t -> T.Term.store
val ty_st : t -> T.Ty.state val ty_st : t -> T.Ty.store
val create : val create :
?stat:Stat.t -> ?stat:Stat.t ->
@ -961,8 +961,8 @@ module type SOLVER = sig
(* TODO? ?config:Config.t -> *) (* TODO? ?config:Config.t -> *)
?store_proof:bool -> ?store_proof:bool ->
theories:theory list -> theories:theory list ->
T.Term.state -> T.Term.store ->
T.Ty.state -> T.Ty.store ->
unit -> unit ->
t t
(** Create a new solver. (** Create a new solver.

20
src/lra/sidekick_arith_lra.ml
View file

@ -47,14 +47,14 @@ module type ARG = sig
val view_as_lra : term -> (Q.t, term) lra_view val view_as_lra : term -> (Q.t, term) lra_view
(** Project the term into the theory view *) (** Project the term into the theory view *)
val mk_bool : S.T.Term.state -> bool -> term val mk_bool : S.T.Term.store -> bool -> term
val mk_lra : S.T.Term.state -> (Q.t, term) lra_view -> term val mk_lra : S.T.Term.store -> (Q.t, term) lra_view -> term
(** Make a term from the given theory view *) (** Make a term from the given theory view *)
val ty_lra : S.T.Term.state -> ty val ty_lra : S.T.Term.store -> ty
val mk_eq : S.T.Term.state -> term -> term -> term val mk_eq : S.T.Term.store -> term -> term -> term
(** syntactic equality *) (** syntactic equality *)
val has_ty_real : term -> bool val has_ty_real : term -> bool
@ -67,9 +67,9 @@ module type ARG = sig
module Gensym : sig module Gensym : sig
type t type t
val create : S.T.Term.state -> t val create : S.T.Term.store -> t
val tst : t -> S.T.Term.state val tst : t -> S.T.Term.store
val copy : t -> t val copy : t -> t
@ -84,8 +84,8 @@ module type S = sig
type state type state
val create : ?stat:Stat.t -> val create : ?stat:Stat.t ->
A.S.T.Term.state -> A.S.T.Term.store ->
A.S.T.Ty.state -> A.S.T.Ty.store ->
state state
val theory : A.S.theory val theory : A.S.theory
@ -141,8 +141,8 @@ module Make(A : ARG) : S with module A = A = struct
module Comb_map = CCMap.Make(LE_.Comb) module Comb_map = CCMap.Make(LE_.Comb)
type state = { type state = {
tst: T.state; tst: T.store;
ty_st: Ty.state; ty_st: Ty.store;
simps: T.t T.Tbl.t; (* cache *) simps: T.t T.Tbl.t; (* cache *)
gensym: A.Gensym.t; gensym: A.Gensym.t;
encoded_eqs: unit T.Tbl.t; (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *) encoded_eqs: unit T.Tbl.t; (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *)

6
src/mini-cc/Sidekick_mini_cc.ml
View file

@ -9,11 +9,11 @@ end
module type S = sig module type S = sig
type term type term
type fun_ type fun_
type term_state type term_store
type t type t
val create : term_state -> t val create : term_store -> t
val clear : t -> unit val clear : t -> unit
@ -31,7 +31,7 @@ module Make(A: ARG) = struct
module T = A.T.Term module T = A.T.Term
type fun_ = A.T.Fun.t type fun_ = A.T.Fun.t
type term = T.t type term = T.t
type term_state = T.state type term_store = T.store
module T_tbl = CCHashtbl.Make(T) module T_tbl = CCHashtbl.Make(T)

6
src/mini-cc/Sidekick_mini_cc.mli
View file

@ -20,12 +20,12 @@ end
module type S = sig module type S = sig
type term type term
type fun_ type fun_
type term_state type term_store
type t type t
(** An instance of the congruence closure. Mutable *) (** An instance of the congruence closure. Mutable *)
val create : term_state -> t val create : term_store -> t
(** New instance *) (** New instance *)
val clear : t -> unit val clear : t -> unit
@ -49,4 +49,4 @@ end
module Make(A: ARG) module Make(A: ARG)
: S with type term = A.T.Term.t : S with type term = A.T.Term.t
and type fun_ = A.T.Fun.t and type fun_ = A.T.Fun.t
and type term_state = A.T.Term.state and type term_store = A.T.Term.store

14
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -112,8 +112,8 @@ module Make(A : ARG)
type term = Term.t type term = Term.t
type ty = Ty.t type ty = Ty.t
type lit = Lit.t type lit = Lit.t
type term_state = Term.state type term_store = Term.store
type ty_state = Ty.state type ty_store = Ty.store
type th_states = type th_states =
| Ths_nil | Ths_nil
@ -128,8 +128,8 @@ module Make(A : ARG)
module Simplify = struct module Simplify = struct
type t = { type t = {
tst: term_state; tst: term_store;
ty_st: ty_state; ty_st: ty_store;
mutable hooks: hook list; mutable hooks: hook list;
cache: Term.t Term.Tbl.t; cache: Term.t Term.Tbl.t;
} }
@ -182,8 +182,8 @@ module Make(A : ARG)
type simplify_hook = Simplify.hook type simplify_hook = Simplify.hook
type t = { type t = {
tst: Term.state; (** state for managing terms *) tst: Term.store; (** state for managing terms *)
ty_st: Ty.state; ty_st: Ty.store;
cc: CC.t lazy_t; (** congruence closure *) cc: CC.t lazy_t; (** congruence closure *)
stat: Stat.t; stat: Stat.t;
count_axiom: int Stat.counter; count_axiom: int Stat.counter;
@ -480,7 +480,7 @@ module Make(A : ARG)
let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit = let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit =
check_ ~final:true self acts check_ ~final:true self acts
let create ~stat (tst:Term.state) (ty_st:Ty.state) () : t = let create ~stat (tst:Term.store) (ty_st:Ty.store) () : t =
let rec self = { let rec self = {
tst; tst;
ty_st; ty_st;

2
src/smtlib/Process.ml
View file

@ -18,7 +18,7 @@ module Check_cc = struct
module Lit = Solver.Solver_internal.Lit module Lit = Solver.Solver_internal.Lit
module SI = Solver.Solver_internal module SI = Solver.Solver_internal
module CC = Solver.Solver_internal.CC module CC = Solver.Solver_internal.CC
module MCC = Sidekick_mini_cc.Make(Solver_arg) module MCC = Sidekick_mini_cc.Make(SBS.Solver_arg)
let pp_c out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" ∨ " Lit.pp) c let pp_c out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" ∨ " Lit.pp) c
let pp_and out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" ∧ " Lit.pp) c let pp_and out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" ∧ " Lit.pp) c

4
src/smtlib/Process.mli
View file

@ -4,9 +4,9 @@ open Sidekick_base
module Solver module Solver
: Sidekick_msat_solver.S with type T.Term.t = Term.t : Sidekick_msat_solver.S with type T.Term.t = Term.t
and type T.Term.state = Term.state and type T.Term.store = Term.store
and type T.Ty.t = Ty.t and type T.Ty.t = Ty.t
and type T.Ty.state = Ty.state and type T.Ty.store = Ty.store
val th_bool : Solver.theory val th_bool : Solver.theory
val th_data : Solver.theory val th_data : Solver.theory

4
src/smtlib/Sidekick_smtlib.mli
View file

@ -11,6 +11,6 @@ module Stmt = Sidekick_base.Statement
module Process = Process module Process = Process
module Solver = Process.Solver module Solver = Process.Solver
val parse : Term.state -> string -> Stmt.t list or_error val parse : Term.store -> string -> Stmt.t list or_error
val parse_stdin : Term.state -> Stmt.t list or_error val parse_stdin : Term.store -> Stmt.t list or_error

5
src/smtlib/Typecheck.ml
View file

@ -12,6 +12,7 @@ module BT = Sidekick_base
module Ty = BT.Ty module Ty = BT.Ty
module T = BT.Term module T = BT.Term
module Fun = BT.Fun module Fun = BT.Fun
module Form = BT.Form
module Stmt = BT.Statement module Stmt = BT.Statement
type 'a or_error = ('a, string) CCResult.t type 'a or_error = ('a, string) CCResult.t
@ -31,13 +32,13 @@ module Ctx = struct
| K_atomic of Ty.def | K_atomic of Ty.def
type t = { type t = {
tst: T.state; tst: T.store;
names: (ID.t * kind) StrTbl.t; names: (ID.t * kind) StrTbl.t;
lets: T.t StrTbl.t; lets: T.t StrTbl.t;
mutable loc: Loc.t option; (* current loc *) mutable loc: Loc.t option; (* current loc *)
} }
let create (tst:T.state) : t = { let create (tst:T.store) : t = {
tst; tst;
names=StrTbl.create 64; names=StrTbl.create 64;
lets=StrTbl.create 16; lets=StrTbl.create 16;

2
src/smtlib/Typecheck.mli
View file

@ -13,7 +13,7 @@ type 'a or_error = ('a, string) CCResult.t
module Ctx : sig module Ctx : sig
type t type t
val create: T.state -> t val create: T.store -> t
end end
val conv_term : Ctx.t -> PA.term -> T.t val conv_term : Ctx.t -> PA.term -> T.t

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

@ -39,7 +39,7 @@ module type ARG = sig
(** Basic boolean logic for a clause [|- c] *) (** Basic boolean logic for a clause [|- c] *)
val proof_bool_c : string -> term list -> S.P.t val proof_bool_c : string -> term list -> S.P.t
val mk_bool : S.T.Term.state -> (term, term IArray.t) bool_view -> term val mk_bool : S.T.Term.store -> (term, term IArray.t) bool_view -> term
(** Make a term from the given boolean view. *) (** Make a term from the given boolean view. *)
val check_congruence_classes : bool val check_congruence_classes : bool
@ -56,7 +56,7 @@ module type ARG = sig
module Gensym : sig module Gensym : sig
type t type t
val create : S.T.Term.state -> t val create : S.T.Term.store -> t
(** New (stateful) generator instance. *) (** New (stateful) generator instance. *)
val fresh_term : t -> pre:string -> S.T.Ty.t -> term val fresh_term : t -> pre:string -> S.T.Ty.t -> term
@ -70,7 +70,7 @@ module type S = sig
type state type state
val create : A.S.T.Term.state -> A.S.T.Ty.state -> state val create : A.S.T.Term.store -> A.S.T.Ty.store -> state
val simplify : state -> A.S.Solver_internal.simplify_hook val simplify : state -> A.S.Solver_internal.simplify_hook
(** Simplify given term *) (** Simplify given term *)
@ -96,8 +96,8 @@ module Make(A : ARG) : S with module A = A = struct
module SI = A.S.Solver_internal module SI = A.S.Solver_internal
type state = { type state = {
tst: T.state; tst: T.store;
ty_st: Ty.state; ty_st: Ty.store;
cnf: (Lit.t * SI.P.t) T.Tbl.t; (* tseitin CNF *) cnf: (Lit.t * SI.P.t) T.Tbl.t; (* tseitin CNF *)
gensym: A.Gensym.t; gensym: A.Gensym.t;
} }

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

@ -67,10 +67,10 @@ module type ARG = sig
val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view
val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view
val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t
val mk_is_a: S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t val mk_is_a: S.T.Term.store -> Cstor.t -> S.T.Term.t -> S.T.Term.t
val mk_sel : S.T.Term.state -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t
val mk_eq : S.T.Term.state -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t val mk_eq : S.T.Term.store -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t
val ty_is_finite : S.T.Ty.t -> bool val ty_is_finite : S.T.Ty.t -> bool
val ty_set_is_finite : S.T.Ty.t -> bool -> unit val ty_set_is_finite : S.T.Ty.t -> bool -> unit
@ -326,7 +326,7 @@ module Make(A : ARG) : S with module A = A = struct
module N_tbl = Backtrackable_tbl.Make(N) module N_tbl = Backtrackable_tbl.Make(N)
type t = { type t = {
tst: T.state; tst: T.store;
cstors: ST_cstors.t; (* repr -> cstor for the class *) cstors: ST_cstors.t; (* repr -> cstor for the class *)
parents: ST_parents.t; (* repr -> parents for the class *) parents: ST_parents.t; (* repr -> parents for the class *)
cards: Card.t; (* remember finiteness *) cards: Card.t; (* remember finiteness *)

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

@ -53,16 +53,16 @@ module type ARG = sig
val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view
(** Try to view term as a datatype term *) (** Try to view term as a datatype term *)
val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t
(** Make a constructor application term *) (** Make a constructor application term *)
val mk_is_a: S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.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 *) (** Make a [is-a] term *)
val mk_sel : S.T.Term.state -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t
(** Make a selector term *) (** Make a selector term *)
val mk_eq : S.T.Term.state -> S.T.Term.t -> S.T.Term.t -> S.T.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 *) (** Make a term equality *)
val ty_is_finite : S.T.Ty.t -> bool val ty_is_finite : S.T.Ty.t -> bool