From 9cfaecec99335fc403c71ffcac39ae81ecdc3774 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 3 Jul 2021 23:39:20 -0400 Subject: [PATCH] helpers --- src/base/Base_types.ml | 29 +++++++++++++++++++++++++ src/base/Form.ml | 8 +++---- src/base/Hashcons.ml | 6 +++-- src/core/Sidekick_core.ml | 14 ++++++++++++ src/msat-solver/Sidekick_msat_solver.ml | 20 ++++++++--------- 5 files changed, 60 insertions(+), 17 deletions(-) diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml index 4f336558..387d9ccb 100644 --- a/src/base/Base_types.ml +++ b/src/base/Base_types.ml @@ -448,6 +448,7 @@ end (** Function symbols *) module Fun : sig + (** Possible definitions for a function symbol *) type view = fun_view = | Fun_undef of fun_ty (* simple undefined constant *) | Fun_select of select @@ -461,6 +462,8 @@ module Fun : sig ty : ID.t -> term IArray.t -> ty; (* compute type *) eval: value IArray.t -> value; (* evaluate term *) } + + (** A function symbol *) type t = fun_ = { fun_id: ID.t; fun_view: fun_view; @@ -481,8 +484,12 @@ module Fun : sig val do_cc : t -> bool val mk_undef : ID.t -> Ty.Fun.t -> t + (** Make a new uninterpreted function. *) + val mk_undef' : ID.t -> Ty.t list -> Ty.t -> t + val mk_undef_const : ID.t -> Ty.t -> t + (** Make a new uninterpreted constant. *) val pp : t CCFormat.printer module Map : CCMap.S with type key = t @@ -806,6 +813,15 @@ module Term : sig val not_ : store -> t -> t val ite : store -> t -> t -> t -> t + val const_undefined_fun : store -> ID.t -> Ty.Fun.t -> t + (** [const_undefined_fun store f ty] is [const store (Fun.mk_undef f ty)]. + It builds a function symbol and turns it into a term immediately *) + + val const_undefined_const : store -> ID.t -> Ty.t -> t + (** [const_undefined_const store f ty] is [const store (Fun.mk_undef_const f ty)]. + It builds a constant function symbol and makes it into a term + immediately. *) + val select : store -> select -> t -> t val app_cstor : store -> cstor -> t IArray.t -> t val is_a : store -> cstor -> t -> t @@ -840,6 +856,11 @@ module Term : sig val as_fun_undef : t -> (fun_ * Ty.Fun.t) option val as_bool : t -> bool option + (** {3 Store} *) + + val store_size : store -> int + val store_iter : store -> term Iter.t + (** {3 Containers} *) module Tbl : CCHashtbl.S with type key = t @@ -925,6 +946,11 @@ end = struct | LRA_other x -> x (* normalize *) | _ -> make st (Term_cell.lra l) + let const_undefined_fun store id ty : t = + const store (Fun.mk_undef id ty) + let const_undefined_const store id ty : t = + const store (Fun.mk_undef_const id ty) + (* might need to tranfer the negation from [t] to [sign] *) let abs tst t : t * bool = match view t with | Bool false -> true_ tst, false @@ -1009,6 +1035,9 @@ end = struct | Eq (a,b) -> eq tst (f a) (f b) | Ite (a,b,c) -> ite tst (f a) (f b) (f c) | LRA l -> lra tst (Sidekick_arith_lra.map_view f l) + + let store_size tst = H.size tst.tbl + let store_iter tst = H.to_iter tst.tbl end (** Values (used in models) *) diff --git a/src/base/Form.ml b/src/base/Form.ml index 92cd5c6e..58623633 100644 --- a/src/base/Form.ml +++ b/src/base/Form.ml @@ -27,9 +27,9 @@ let view_id fid args = ) else if ID.equal fid id_or then ( B_or (IArray.to_iter args) ) else if ID.equal fid id_imply && IArray.length args >= 2 then ( - (* conclusion is stored first *) + (* conclusion is stored last *) let len = IArray.length args in - B_imply (IArray.to_iter_sub args 1 (len-1), IArray.get args 0) + B_imply (IArray.to_iter_sub args 0 (len-1), IArray.get args (len-1)) ) else ( raise_notrace Not_a_th_term ) @@ -141,11 +141,11 @@ let neq st a b = not_ st @@ eq st a b let imply_a st xs y = if IArray.is_empty xs then y - else T.app_fun st Funs.imply (IArray.append (IArray.singleton y) xs) + else T.app_fun st Funs.imply (IArray.append xs (IArray.singleton y)) let imply_l st xs y = match xs with | [] -> y - | _ -> T.app_fun st Funs.imply (IArray.of_list @@ y :: xs) + | _ -> imply_a st (IArray.of_list xs) y let imply st a b = imply_a st (IArray.singleton a) b let xor st a b = not_ st (equiv st a b) diff --git a/src/base/Hashcons.ml b/src/base/Hashcons.ml index ec9fa59c..3dd07dcb 100644 --- a/src/base/Hashcons.ml +++ b/src/base/Hashcons.ml @@ -10,7 +10,8 @@ module Make(A : ARG): sig type t val create : ?size:int -> unit -> t val hashcons : t -> A.t -> A.t - val to_seq : t -> A.t Iter.t + val size : t -> int + val to_iter : t -> A.t Iter.t end = struct module W = Weak.Make(A) @@ -30,6 +31,7 @@ end = struct ); t' - let to_seq st yield = + let size st = W.count st.tbl + let to_iter st yield = W.iter yield st.tbl end diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index f33921d5..6f2f4a3b 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -993,11 +993,17 @@ module type SOLVER = sig where [atom] is an internal atom for the solver, and [pr] is a proof of [|- lit = atom] *) + val mk_atom_lit' : t -> lit -> Atom.t + (** Like {!mk_atom_t} but skips the proof *) + val mk_atom_t : t -> ?sign:bool -> term -> Atom.t * P.t (** [mk_atom_t _ ~sign t] returns [atom, pr] where [atom] is an internal representation of [± t], and [pr] is a proof of [|- atom = (± t)] *) + val mk_atom_t' : t -> ?sign:bool -> term -> Atom.t + (** Like {!mk_atom_t} but skips the proof *) + val add_clause : t -> Atom.t IArray.t -> P.t -> unit (** [add_clause solver cs] adds a boolean clause to the solver. Subsequent calls to {!solve} will need to satisfy this clause. *) @@ -1005,6 +1011,14 @@ module type SOLVER = sig val add_clause_l : t -> Atom.t list -> P.t -> unit (** Add a clause to the solver, given as a list. *) + val assert_terms : t -> term list -> unit + (** Helper that turns each term into an atom, before adding the result + to the solver as an assertion *) + + val assert_term : t -> term -> unit + (** Helper that turns the term into an atom, before adding the result + to the solver as a unit clause assertion *) + (** {2 Internal representation of proofs} A type or state convertible into {!P.t} *) diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index f3f661f5..139d2694 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -774,6 +774,9 @@ module Make(A : ARG) let lit = Lit.atom (tst self) ?sign t in mk_atom_lit self lit + let mk_atom_t' self ?sign t = mk_atom_t self ?sign t |> fst + let mk_atom_lit' self lit = mk_atom_lit self lit |> fst + (** {2 Result} *) module Unknown = struct @@ -832,19 +835,14 @@ module Make(A : ARG) Sat_solver.add_clause_a self.solver (c:> Atom.t array) proof; Profile.exit pb - let add_clause_l self c = add_clause self (IArray.of_list c) + let add_clause_l self c p = add_clause self (IArray.of_list c) p + let assert_terms self c = + let p = P.assertion_c_l (List.map P.lit_a c) in + let c = CCList.map (mk_atom_t' self) c in + add_clause_l self c p - (* TODO - let mk_model (self:t) lits : Model.t = - let m = - Iter.fold - (fun m (Th_state ((module Th),st)) -> Th.mk_model st lits m) - Model.empty (theories self) - in - (* now complete model using CC *) - CC.mk_model (cc self) m - *) + let assert_term self t = assert_terms self [t] let mk_model (self:t) (lits:lit Iter.t) : Model.t = Log.debug 1 "(smt.solver.mk-model)";