helpers

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

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)

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

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} *)

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 assert_term self t = assert_terms self [t]
-    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 mk_model (self:t) (lits:lit Iter.t) : Model.t =
     Log.debug 1 "(smt.solver.mk-model)";