feat(cdsat): add variables (to plugins, to-decide set)

src/cdsat/TVar.ml

@@ -124,6 +124,15 @@ let pp (self : store) out (v : t) : unit =
     (Term.pp_limit ~max_depth:5 ~max_nodes:30)
     t
 
+let pp_with_assignment (self : store) out (v : t) : unit =
+  let t = term self v in
+  match value self v with
+  | Some value ->
+    Fmt.fprintf out "(@[var[%d]@ :term %a@ :value %a@ :level %d@])" v
+      (Term.pp_limit ~max_depth:5 ~max_nodes:30)
+      t Value.pp value (level self v)
+  | None -> pp self out v
+
 module Tbl = Util.Int_tbl
 module Set = Util.Int_set
 module Map = Util.Int_map

src/cdsat/TVar.mli

@@ -59,6 +59,7 @@ val pop_new_var : store -> t option
 (** Pop a new variable if any, or return [None] *)
 
 val pp : store -> t Fmt.printer
+val pp_with_assignment : store -> t Fmt.printer
 
 module Tbl : CCHashtbl.S with type key = t
 module Set : CCSet.S with type elt = t

src/cdsat/core.ml

@@ -24,26 +24,32 @@ type plugin_id = int
 
 type plugin_event = ..
 
-type watch_request =
-  | Watch2 of TVar.t array * plugin_event
-  | Watch1 of TVar.t array * plugin_event
-
 module Watches = Watch_schemes.Make (struct
   type t = plugin_id * plugin_event
 end)
 
+(* TODO: regular GC, where we remove variables with a low activity/high LBD (?)
+   that are also not assigned in current trail.
+
+   need to cooperate with plugins to mark sub-variables kept alive by alive
+   variables.
+*)
+
 type t = {
   tst: Term.store;
   vst: TVar.store;
   arg: (module ARG);
   stats: Stat.t;
-  trail: Trail.t;
+  trail: Trail.t;  (** partial model (stack of assigned variables) *)
-  plugins: plugin Vec.t;
+  plugins: plugin Vec.t;  (** plugins registered to this solver *)
-  term_to_var: Term_to_var.t;
+  term_to_var: Term_to_var.t;  (** convert terms to vars *)
   vars_to_decide: Vars_to_decide.t;
-  pending_assignments: pending_assignment Vec.t;
+      (** set of variables (potentially) undecided *)
+  added_vars: unit TVar.Tbl.t;  (** set of variables added to all plugins *)
+  pending_assignments: pending_assignment Vec.t;  (** assignments to process *)
   watches: Watches.t;
   mutable last_res: Check_res.t option;
+      (** last result, useful to get unsat core/model *)
   proof_tracer: Proof.Tracer.t;
   n_conflicts: int Stat.counter;
   n_propagations: int Stat.counter;
@@ -53,8 +59,7 @@ type t = {
 and plugin_action = t * plugin_id
 
 (* FIXME:
-   - add [on_add_var: TVar.t -> unit]
+   - add [on_remove_var: TVar.t -> unit].
-     and [on_remove_var: TVar.t -> unit].
      these are called when a variable becomes relevant/is removed or GC'd
        (in particular: setup watches + var constraints on add,
         kill watches and remove constraints on remove)
@@ -73,7 +78,9 @@ and plugin =
       on_assign: 'st -> plugin_action -> TVar.t -> Value.t -> unit;
       on_event: 'st -> plugin_action -> unit:bool -> plugin_event -> unit;
       term_to_var_hooks: 'st -> Term_to_var.hook list;
-      on_add_var: 'st -> TVar.t -> watch_request list;
+      iter_theory_view: 'st -> TVar.theory_view -> TVar.t Iter.t;
+          (** return [true] if it iterated *)
+      on_add_var: 'st -> plugin_action -> TVar.t -> unit;
     }
       -> plugin
 
@@ -88,6 +95,7 @@ let create ?(stats = Stat.create ()) ~arg tst vst ~proof_tracer () : t =
     pending_assignments = Vec.create ();
     term_to_var = Term_to_var.create vst;
     vars_to_decide = Vars_to_decide.create ();
+    added_vars = TVar.Tbl.create 32;
     watches = Watches.create vst;
     last_res = None;
     proof_tracer;
@@ -113,13 +121,9 @@ module Plugin = struct
 
   type nonrec event = plugin_event = ..
 
-  type nonrec watch_request = watch_request =
+  let make_builder ~name ~create ~push_level ~pop_levels ~iter_theory_view
-    | Watch2 of TVar.t array * event
-    | Watch1 of TVar.t array * event
-
-  let make_builder ~name ~create ~push_level ~pop_levels
       ?(decide = fun _ _ -> None) ?(on_assign = fun _ _ _ _ -> ())
-      ?(on_event = fun _ _ ~unit:_ _ -> ()) ?(on_add_var = fun _ _ -> [])
+      ?(on_event = fun _ _ ~unit:_ _ -> ()) ?(on_add_var = fun _ _ _ -> ())
       ?(term_to_var_hooks = fun _ -> []) () : builder =
    fun ~id vst ->
     let st = create vst in
@@ -131,6 +135,7 @@ module Plugin = struct
         push_level;
         pop_levels;
         decide;
+        iter_theory_view;
         on_assign;
         on_event;
         term_to_var_hooks;
@@ -159,6 +164,7 @@ let pop_levels (self : t) n : unit =
     term_to_var = _;
     watches = _;
     vars_to_decide = _;
+    added_vars = _;
     pending_assignments;
     last_res = _;
     proof_tracer = _;
@@ -200,7 +206,7 @@ let add_ty (_self : t) ~ty:_ : unit = ()
 
 (** Assign [v <- value] for [reason] at [level].
     This assignment is delayed. *)
-let assign (self : t) (v : TVar.t) ~(value : Value.t) ~level:v_level ~reason :
+let assign_ (self : t) (v : TVar.t) ~(value : Value.t) ~level:v_level ~reason :
     unit =
   Log.debugf 50 (fun k ->
       k "(@[cdsat.core.assign@ `%a`@ @[<- %a@]@ :reason %a@])"
@@ -208,6 +214,21 @@ let assign (self : t) (v : TVar.t) ~(value : Value.t) ~level:v_level ~reason :
   self.last_res <- None;
   Vec.push self.pending_assignments { var = v; value; level = v_level; reason }
 
+let rec add_var_ (self : t) (v : TVar.t) : unit =
+  if not (TVar.Tbl.mem self.added_vars v) then (
+    Log.debugf 50 (fun k -> k "(@[cdsat.add-var@ %a@])" (TVar.pp self.vst) v);
+    TVar.Tbl.add self.added_vars v ();
+    Vars_to_decide.add self.vars_to_decide v;
+
+    (* add variable to plugins *)
+    iter_plugins self ~f:(fun (P p) -> p.on_add_var p.st (self, p.id) v);
+
+    (* add sub-variables as well *)
+    let tview = TVar.theory_view self.vst v in
+    iter_plugins self ~f:(fun (P p) ->
+        p.iter_theory_view p.st tview (fun sub -> add_var_ self sub))
+  )
+
 exception E_conflict of Conflict.t
 
 let raise_conflict (c : Conflict.t) : 'a = raise (E_conflict c)
@@ -255,9 +276,6 @@ let propagate (self : t) : Conflict.t option =
       while Trail.head self.trail < Trail.size self.trail do
         let var = Trail.get self.trail (Trail.head self.trail) in
 
-        (* TODO: call plugins *)
-        Log.debugf 0 (fun k -> k "TODO: propagate %a" (TVar.pp self.vst) var);
-
         let value =
           match TVar.value self.vst var with
           | Some v -> v
@@ -314,13 +332,18 @@ let rec decide (self : t) : [ `Decided | `Full_model ] =
 
         Error.errorf "no plugin can decide %a" (TVar.pp self.vst) v
       with Decided value ->
-        Trail.push_level self.trail;
         let level = Trail.n_levels self.trail in
+        Trail.push_level self.trail;
         Log.debugf 5 (fun k -> k "(@[cdsat.new-level %d@])" level);
-        assign self v ~value ~level ~reason:(Reason.decide level);
+        assign_ self v ~value ~level ~reason:(Reason.decide level);
         `Decided
     )
 
+let assign (self : t) v ~value ~reason : unit =
+  let level = Reason.level reason in
+  add_var_ self v;
+  assign_ self v ~value ~level ~reason
+
 (** Solve satisfiability of the current set of assertions *)
 let solve ~on_exit ~on_progress ~should_stop ~assumptions (self : t) :
     Check_res.t =
@@ -357,6 +380,9 @@ let solve ~on_exit ~on_progress ~should_stop ~assumptions (self : t) :
       (match decide self with
       | `Decided -> ()
       | `Full_model ->
+        Log.debugf 50 (fun k ->
+            k "(@[cdsat.sat.full-trail@ %a@])" (Trail.pp_full self.vst)
+              self.trail);
         let sat = make_sat_res self in
 
         res := Check_res.Sat sat;
@@ -382,11 +408,12 @@ module Plugin_action = struct
   type t = plugin_action
 
   let[@inline] propagate ((self, _) : t) var value reason : unit =
-    assign self var ~value ~level:(Reason.level reason) ~reason
+    assign_ self var ~value ~level:(Reason.level reason) ~reason
 
   let term_to_var (self, _) t : TVar.t = term_to_var self t
 
-  let watch1 ((self, pl_id) : t) (vars : _ array) (ev : plugin_event) : unit =
+  let watch1 ((self, pl_id) : t) (vars : TVar.t list) (ev : plugin_event) : unit
+      =
     let _h : Watches.handle =
       Watches.watch1 self.watches vars (pl_id, ev) ~f:(fun ~unit (_, ev) ->
           let (P p) = get_plugin self pl_id in
@@ -395,7 +422,8 @@ module Plugin_action = struct
     in
     ()
 
-  let watch2 ((self, pl_id) : t) (vars : _ array) (ev : plugin_event) : unit =
+  let watch2 ((self, pl_id) : t) (vars : TVar.t list) (ev : plugin_event) : unit
+      =
     let _h : Watches.handle =
       Watches.watch2 self.watches vars (pl_id, ev) ~f:(fun ~unit (_, ev) ->
           let (P p) = get_plugin self pl_id in

src/cdsat/core.mli

@@ -23,11 +23,11 @@ module Plugin_action : sig
   val term_to_var : t -> Term.t -> TVar.t
   (** Convert a term to a variable *)
 
-  val watch1 : t -> TVar.t array -> plugin_event -> unit
+  val watch1 : t -> TVar.t list -> plugin_event -> unit
   (** Create a watcher for the given set of variables, which will trigger
       the event *)
 
-  val watch2 : t -> TVar.t array -> plugin_event -> unit
+  val watch2 : t -> TVar.t list -> plugin_event -> unit
   (** Create a watcher for the given set of variables, which will trigger
       the event *)
 end
@@ -41,19 +41,16 @@ module Plugin : sig
 
   type event = plugin_event = ..
 
-  type watch_request =
-    | Watch2 of TVar.t array * event
-    | Watch1 of TVar.t array * event
-
   val make_builder :
     name:string ->
     create:(TVar.store -> 'st) ->
     push_level:('st -> unit) ->
     pop_levels:('st -> int -> unit) ->
+    iter_theory_view:('st -> TVar.theory_view -> TVar.t Iter.t) ->
     ?decide:('st -> TVar.t -> Value.t option) ->
     ?on_assign:('st -> Plugin_action.t -> TVar.t -> Value.t -> unit) ->
     ?on_event:('st -> Plugin_action.t -> unit:bool -> event -> unit) ->
-    ?on_add_var:('st -> TVar.t -> watch_request list) ->
+    ?on_add_var:('st -> Plugin_action.t -> TVar.t -> unit) ->
     ?term_to_var_hooks:('st -> Term_to_var.hook list) ->
     unit ->
     builder
@@ -94,8 +91,7 @@ val add_term_to_var_hook : t -> Term_to_var.hook -> unit
 
 (** {2 Main solving API} *)
 
-val assign :
+val assign : t -> TVar.t -> value:Value.t -> reason:Reason.t -> unit
-  t -> TVar.t -> value:Value.t -> level:int -> reason:Reason.t -> unit
 
 val solve :
   on_exit:(unit -> unit) list ->

src/cdsat/plugin_bool.ml

@@ -32,13 +32,26 @@ let decide (self : t) (v : TVar.t) : Value.t option =
     Some (Term.true_ self.tst)
   | _ -> None
 
-let on_assign (self : t) (act : Core.Plugin_action.t) (v : TVar.t)
+type Core.Plugin.event += Eval of TVar.t | BCP of TVar.t
-    (value : Value.t) : unit =
-  Log.debugf 0 (fun k ->
-      k "(@[bool-plugin.on-assign %a@])" (TVar.pp self.vst) v);
-  ()
 
-(* TODO: BCP via on_event *)
+(* create watch *)
+let on_add_var (self : t) acts (v : TVar.t) : unit =
+  match TVar.theory_view self.vst v with
+  | T_and lits | T_or lits ->
+    let vars_of_lits = Util.array_to_list_map TLit.var lits in
+    Core.Plugin_action.watch1 acts vars_of_lits (Eval v);
+    Core.Plugin_action.watch2 acts (v :: vars_of_lits) (BCP v)
+  | _ -> ()
+
+let on_event (self : t) acts ~unit (ev : Core.Plugin.event) : unit =
+  match ev with
+  | Eval v ->
+    (* TODO: evaluate [v] *)
+    Log.debugf 1 (fun k -> k "(@[cdsat.bool.eval@ %a@])" (TVar.pp self.vst) v)
+  | BCP v ->
+    (* TODO: check if we can eval *)
+    Log.debugf 1 (fun k -> k "(@[cdsat.bool.bcp@ %a@])" (TVar.pp self.vst) v)
+  | _ -> ()
 
 let term_to_var_hooks (self : t) : _ list =
   let (module A) = self.arg in
@@ -67,10 +80,15 @@ let term_to_var_hooks (self : t) : _ list =
   in
   [ h ]
 
+let iter_theory_view _ (v : TVar.theory_view) k =
+  match v with
+  | T_and lits | T_or lits -> Array.iter (fun { TLit.var; _ } -> k var) lits
+  | _ -> ()
+
 let builder ((module A : ARG) as arg) : Core.Plugin.builder =
   let create vst : t =
     let tst = TVar.Store.tst vst in
     { arg; vst; tst }
   in
-  Core.Plugin.make_builder ~name:"bool" ~create ~push_level ~pop_levels ~decide
+  Core.Plugin.make_builder ~name:"bool" ~create ~push_level ~pop_levels
-    ~on_assign ~term_to_var_hooks ()
+    ~iter_theory_view ~decide ~on_add_var ~on_event ~term_to_var_hooks ()

src/cdsat/plugin_uninterpreted.ml

@@ -62,8 +62,14 @@ let term_to_var_hooks (self : t) : _ list =
   in
   [ h ]
 
+let iter_theory_view _ (v : TVar.theory_view) k : unit =
+  match v with
+  | Unin_const _ -> ()
+  | Unin_fun { f = _; args } -> Array.iter k args
+  | _ -> ()
+
 (* TODO: congruence rules *)
 
 let builder ((module A : ARG) as arg) : Core.Plugin.builder =
   Core.Plugin.make_builder ~name:"uf" ~create:(create arg) ~push_level
-    ~pop_levels ~decide ~on_assign ~term_to_var_hooks ()
+    ~pop_levels ~iter_theory_view ~decide ~on_assign ~term_to_var_hooks ()

src/cdsat/solver.ml

@@ -57,7 +57,6 @@ let assert_term_ (self : t) (t : Term.t) pr : unit =
     let pr = Proof.Tracer.add_step self.proof_tracer pr in
     Core.assign self.core v
       ~value:(Term.bool_val self.tst sign)
-      ~level:0
       ~reason:(Reason.propagate_l self.vst [] pr)
   | Some value when Term.is_true value && sign -> ()
   | Some value when Term.is_false value && not sign -> ()

src/cdsat/trail.ml

@@ -28,3 +28,8 @@ let pop_levels (self : t) (n : int) ~f : unit =
     (* also reset head *)
     if self.head > idx then self.head <- idx
   )
+
+let pp_full vst out (self : t) : unit =
+  Fmt.fprintf out "(@[<hv>trail@ %a@])"
+    (Util.pp_iter (TVar.pp_with_assignment vst))
+    (VVec.to_iter self.vars)

src/cdsat/trail.mli

@@ -10,3 +10,5 @@ val head : t -> int
 val set_head : t -> int -> unit
 
 include Sidekick_sigs.BACKTRACKABLE0_CB with type t := t and type elt := TVar.t
+
+val pp_full : TVar.store -> t Fmt.printer

src/cdsat/watch_schemes.ml

@@ -79,7 +79,8 @@ struct
     let vec = Handle_v_map.get self.by_var v in
     Veci.push vec h
 
-  let watch1 (self : t) (arr : TVar.t array) (ev : Ev.t) ~(f : cb_) : handle =
+  let watch1 (self : t) (vars : TVar.t list) (ev : Ev.t) ~(f : cb_) : handle =
+    let arr = Array.of_list vars in
     let h = make_watch_ self (Watch1 { arr; ev }) in
     let i, all_set = find_watch_ self.vst arr ~idx0:0 in
     (* put watched var first *)
@@ -88,7 +89,8 @@ struct
     if all_set then f ~unit:false ev;
     h
 
-  let watch2 (self : t) (arr : TVar.t array) (ev : Ev.t) ~(f : cb_) : handle =
+  let watch2 (self : t) (vars : TVar.t list) (ev : Ev.t) ~(f : cb_) : handle =
+    let arr = Array.of_list vars in
     let h = make_watch_ self (Watch2 { arr; ev }) in
     (* put watched vars first *)
     let i0, all_set0 = find_watch_ self.vst arr ~idx0:0 in

src/cdsat/watch_schemes.mli

@@ -10,13 +10,15 @@ end) : sig
   (** New set of watchers *)
 
   val watch2 :
-    t -> TVar.t array -> Ev.t -> f:(unit:bool -> Ev.t -> unit) -> handle
+    t -> TVar.t list -> Ev.t -> f:(unit:bool -> Ev.t -> unit) -> handle
   (** 2-watch scheme on these variables. *)
 
   val watch1 :
-    t -> TVar.t array -> Ev.t -> f:(unit:bool -> Ev.t -> unit) -> handle
+    t -> TVar.t list -> Ev.t -> f:(unit:bool -> Ev.t -> unit) -> handle
   (** 1-watch scheme on these variables. *)
 
+  (* TODO: remove var *)
+
   val kill : t -> handle -> unit
   (** Disable watch *)