wip: model builder

src/smt/Sidekick_smt_solver.ml

@@ -8,6 +8,7 @@
 
 module Sigs = Sigs
 module Model = Model
+module Model_builder = Model_builder
 module Registry = Registry
 module Solver_internal = Solver_internal
 module Solver = Solver

src/smt/model_builder.ml

@@ -0,0 +1,60 @@
+open Sidekick_core
+open Sigs
+module T = Term
+
+type t = {
+  tst: Term.store;
+  m: Term.t T.Tbl.t;
+  required: Term.t Queue.t;
+  gensym: Gensym.t;
+}
+
+let create tst : t =
+  {
+    tst;
+    m = T.Tbl.create 8;
+    required = Queue.create ();
+    gensym = Gensym.create tst;
+  }
+
+let pp out (self : t) : unit =
+  let pp_pair out (t, v) = Fmt.fprintf out "(@[%a :=@ %a@])" T.pp t T.pp v in
+  Fmt.fprintf out "(@[model-builder@ :m (@[%a@])@ :q (@[%a@])@])"
+    (Util.pp_iter pp_pair) (T.Tbl.to_iter self.m) (Util.pp_iter T.pp)
+    (Iter.of_queue self.required)
+
+let gensym self ~pre ~ty : Term.t = Gensym.fresh_term self.gensym ~pre ty
+
+let rec pop_required (self : t) : _ option =
+  match Queue.take_opt self.required with
+  | None -> None
+  | Some t when T.Tbl.mem self.m t -> pop_required self
+  | Some t -> Some t
+
+let require_eval (self : t) t : unit =
+  if not @@ T.Tbl.mem self.m t then Queue.push t self.required
+
+let mem self t : bool = T.Tbl.mem self.m t
+
+let add (self : t) ?(subs = []) t v : unit =
+  assert (not @@ T.Tbl.mem self.m t);
+  T.Tbl.add self.m t v;
+  List.iter (fun u -> require_eval self u) subs;
+  ()
+
+type eval_cache = Term.Internal_.cache
+
+let eval ?(cache = Term.Internal_.create_cache 8) (self : t) (t : Term.t) =
+  let t = try T.Tbl.find self.m t with Not_found -> t in
+  T.Internal_.replace_ ~cache self.tst ~recursive:true t ~f:(fun ~recurse:_ u ->
+      T.Tbl.find_opt self.m u)
+
+let to_model (self : t) : Model.t =
+  (* ensure we evaluate each term only once *)
+  let cache = T.Internal_.create_cache 8 in
+  let tbl =
+    T.Tbl.keys self.m
+    |> Iter.map (fun t -> t, eval ~cache self t)
+    |> T.Tbl.of_iter
+  in
+  Model.Internal_.of_tbl tbl

src/smt/model_builder.mli

@@ -0,0 +1,37 @@
+(** Model Builder.
+
+  This contains a partial model, in construction. It is accessible to every
+  theory, so they can contribute partial values.
+
+  TODO: seen values?
+*)
+
+open Sidekick_core
+open Sigs
+
+type t
+
+include Sidekick_sigs.PRINT with type t := t
+
+val create : Term.store -> t
+val mem : t -> Term.t -> bool
+
+val require_eval : t -> Term.t -> unit
+(** Require that this term gets a value. *)
+
+val add : t -> ?subs:Term.t list -> Term.t -> value -> unit
+(** Add a value to the model.
+   @param subs if provided, these terms will be passed to {!require_eval}
+   to ensure they map to a value. *)
+
+val gensym : t -> pre:string -> ty:Term.t -> Term.t
+(** New fresh constant *)
+
+type eval_cache = Term.Internal_.cache
+
+val eval : ?cache:eval_cache -> t -> Term.t -> value
+
+val pop_required : t -> Term.t option
+(** gives the next subterm that is required but has no value yet *)
+
+val to_model : t -> Model.t

src/smt/solver_internal.ml

@@ -63,9 +63,9 @@ type t = {
 and preprocess_hook = t -> preprocess_actions -> term -> unit
 
 and model_ask_hook =
-  recurse:(t -> E_node.t -> term) -> t -> E_node.t -> term option
+  t -> Model_builder.t -> Term.t -> (value * Term.t list) option
 
-and model_completion_hook = t -> add:(term -> term -> unit) -> unit
+and model_completion_hook = t -> add:(term -> value -> unit) -> unit
 
 type solver = t
 
@@ -330,90 +330,70 @@ let rec pop_lvls_theories_ n = function
 
 (* make model from the congruence closure *)
 let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
+  let@ () = Profile.with_ "smt-solver.mk-model" in
   Log.debug 1 "(smt.solver.mk-model)";
-  Profile.with_ "smt-solver.mk-model" @@ fun () ->
+  let module MB = Model_builder in
-  let module M = Term.Tbl in
   let { cc; tst; model_ask = model_ask_hooks; model_complete; _ } = self in
 
-  let model = M.create 128 in
+  let model = Model_builder.create tst in
 
   (* first, add all literals to the model using the given propositional model
-     [lits]. *)
+     induced by the trail [lits]. *)
   lits (fun lit ->
       let t, sign = Lit.signed_term lit in
-      M.replace model t (Term.bool_val tst sign));
+      MB.add model t (Term.bool_val tst sign));
 
-  (* populate with information from the CC *)
+  (* complete model with theory specific values using the completion hooks.
-  (* FIXME
+     This generally adds values that theories already explicitly have
-     CC.get_model_for_each_class cc (fun (_, ts, v) ->
+     computed in their theory-specific models, e.g. in the simplexe. *)
-         Iter.iter
-           (fun n ->
-             let t = E_node.term n in
-             M.replace model t v)
-           ts);
-  *)
-
-  (* complete model with theory specific values *)
   let complete_with f =
-    f self ~add:(fun t u ->
+    f self ~add:(fun t v ->
-        if not (M.mem model t) then (
+        if not (MB.mem model t) then (
           Log.debugf 20 (fun k ->
-              k "(@[smt.model-complete@ %a@ :with-val %a@])" Term.pp_debug t
+              k "(@[smt.model-complete@ %a@ :with-val %a@])" Term.pp t Term.pp v);
-                Term.pp_debug u);
+          MB.add model t v
-          M.replace model t u
         ))
   in
   List.iter complete_with model_complete;
 
-  (* compute a value for [n]. *)
+  (* require a value for each class that doesn't already have one *)
-  let rec val_for_class (n : E_node.t) : term =
+  CC.all_classes cc (fun repr ->
-    Log.debugf 5 (fun k -> k "val-for-term %a" E_node.pp n);
+      let t = E_node.term repr in
-    let repr = CC.find cc n in
+      MB.require_eval model t);
-    Log.debugf 5 (fun k -> k "val-for-term.repr %a" E_node.pp repr);
+
+  (* now for the fixpoint. This is typically where composite theories such
+     as arrays and datatypes contribute their skeleton values. *)
+  let rec compute_fixpoint () =
+    match MB.pop_required model with
+    | None -> ()
+    | Some t ->
+      (* compute a value for [t] *)
+      Log.debugf 5 (fun k ->
+          k "(@[model.fixpoint.compute-for-required@ %a@])" Term.pp t);
 
-    (* see if a value is found already (always the case if it's a boolean) *)
-    match M.get model (E_node.term repr) with
-    | Some t_val ->
-      Log.debugf 5 (fun k -> k "cached val is %a" Term.pp_debug t_val);
-      t_val
-    | None ->
       (* try each model hook *)
       let rec try_hooks_ = function
-        | [] -> E_node.term repr
+        | [] ->
+          let c = MB.gensym model ~pre:"@c" ~ty:(Term.ty t) in
+          Log.debugf 10 (fun k ->
+              k "(@[model.fixpoint.pick-default-val@ %a@ :for %a@])" Term.pp c
+                Term.pp t);
+          MB.add model t c
         | h :: hooks ->
-          (match h ~recurse:(fun _ n -> val_for_class n) self repr with
+          (match h self model t with
           | None -> try_hooks_ hooks
-          | Some t -> t)
+          | Some (v, subs) ->
+            MB.add model ~subs t v;
+            ())
       in
 
-      let t_val =
+      try_hooks_ model_ask_hooks;
-        try_hooks_ model_ask_hooks
+      (* continue to next value *)
-        (* FIXME: the more complete version?
+      (compute_fixpoint [@tailcall]) ()
-           match
-             (* look for a value in the model for any term in the class *)
-             E_node.iter_class repr
-             |> Iter.find_map (fun n -> M.get model (E_node.term n))
-           with
-           | Some v -> v
-           | None -> try_hooks_ model_ask_hooks
-        *)
-      in
-
-      M.replace model (E_node.term repr) t_val;
-      (* be sure to cache the value *)
-      Log.debugf 5 (fun k -> k "val is %a" Term.pp_debug t_val);
-      t_val
   in
 
-  (* map terms of each CC class to the value computed for their class. *)
+  compute_fixpoint ();
-  CC.all_classes cc (fun repr ->
+  MB.to_model model
-      let t_val = val_for_class repr in
-      (* value for this class *)
-      E_node.iter_class repr (fun u ->
-          let t_u = E_node.term u in
-          if (not (E_node.equal u repr)) && not (Term.equal t_u t_val) then
-            M.replace model t_u t_val));
-  Model.Internal_.of_tbl model
 
 (* do theory combination using the congruence closure. Each theory
    can merge classes, *)

src/smt/solver_internal.mli

@@ -234,20 +234,24 @@ val declare_pb_is_incomplete : t -> unit
 (** {3 Model production} *)
 
 type model_ask_hook =
-  recurse:(t -> E_node.t -> term) -> t -> E_node.t -> term option
+  t -> Model_builder.t -> Term.t -> (value * Term.t list) option
 (** A model-production hook to query values from a theory.
 
-      It takes the solver, a class, and returns
+    It takes the solver, a class, and returns an optional value for this class
-      a term for this class. For example, an arithmetic theory
+    (potentially with sub-terms to find values for, if the value is actually a
-      might detect that a class contains a numeric constant, and return
+    skeleton).
-      this constant as a model value.
 
-      If no hook assigns a value to a class, a fake value is created for it.
+    For example, an arithmetic theory might detect that a class contains a
-  *)
+    numeric constant, and return this constant as a model value. The theory
+    of arrays might return [array.const $v] for an array [Array A B],
+    where [$v] will be picked by the theory of the sort [B].
 
-type model_completion_hook = t -> add:(term -> term -> unit) -> unit
+    If no hook assigns a value to a class, a fake value is created for it.
+*)
+
+type model_completion_hook = t -> add:(term -> value -> unit) -> unit
 (** A model production hook, for the theory to add values.
-      The hook is given a [add] function to add bindings to the model. *)
+    The hook is given a [add] function to add bindings to the model. *)
 
 val on_model :
   ?ask:model_ask_hook -> ?complete:model_completion_hook -> t -> unit

src/th-data/Sidekick_th_data.ml

@@ -4,6 +4,7 @@ open Sidekick_core
 open Sidekick_cc
 include Th_intf
 module SI = SMT.Solver_internal
+module Model_builder = SMT.Model_builder
 
 let name = "th-data"
 
@@ -749,52 +750,38 @@ end = struct
             l);
       Profile.instant "data.case-split";
       List.iter (decide_class_ self solver acts) l);
-
-    if remaining_to_decide = [] then (
-      let next_decision = None in
-      match next_decision with
-      | None -> () (* all decided *)
-      | Some n ->
-        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 (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 =
-          let args =
-            A.Cstor.ty_args base_cstor
-            |> List.mapi (fun i _ -> A.mk_sel self.tst base_cstor i t)
-          in
-          A.mk_cstor self.tst base_cstor args
-        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@])" 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 : E_node.t) :
+  let on_model_gen (self : t) (si : SI.t) (model : Model_builder.t) (t : Term.t)
-      Term.t option =
+      : _ option =
     (* TODO: option to complete model or not (by picking sth at leaves)? *)
     let cc = SI.cc si in
-    let repr = CC.find cc n in
+    match
-    match ST_cstors.get self.cstors repr with
+      try
-    | None -> None
+        let repr = CC.find_t cc t in
+        ST_cstors.get self.cstors repr
+      with Not_found -> None
+    with
     | Some c ->
+      (* return the known constructor for this class *)
       Log.debugf 5 (fun k ->
           k "(@[th-data.mk-model.find-cstor@ %a@])" Monoid_cstor.pp c);
-      let args = List.map (recurse si) c.c_args in
+      let args = List.map E_node.term c.c_args in
       let t = A.mk_cstor self.tst c.c_cstor args in
-      Some t
+      Some (t, args)
+    | None when is_data_ty (Term.ty t) ->
+      (* datatype not split upon, use the base constructor for it *)
+      (match Card.base_cstor self.cards (Term.ty t) with
+      | None -> None
+      | Some c ->
+        (* invent new args *)
+        let args =
+          A.Cstor.ty_args c
+          |> List.map (fun ty -> Model_builder.gensym model ~pre:"c_arg" ~ty)
+        in
+        let c = A.mk_cstor self.tst c args in
+        Some (c, args))
+    | None -> None
 
   let create_and_setup (solver : SI.t) : t =
     let self =

src/th-lra/sidekick_th_lra.ml

@@ -664,15 +664,14 @@ module Make (A : ARG) = (* : S with module A = A *) struct
     ()
 
   (* help generating model *)
-  let model_ask_ (self : state) ~recurse:_ _si n : _ option =
+  let model_ask_ (self : state) _si _model (t : Term.t) : _ option =
-    let t = E_node.term n in
     match self.last_res with
     | Some (SimpSolver.Sat m) ->
       Log.debugf 50 (fun k -> k "(@[lra.model-ask@ %a@])" Term.pp_debug t);
       (match A.view_as_lra t with
       | LRA_const n -> Some n (* always eval constants to themselves *)
       | _ -> SimpSolver.V_map.get t m)
-      |> Option.map (t_const self)
+      |> Option.map (fun t -> t_const self t, [])
     | _ -> None
 
   (* help generating model *)