wip: feat(cdsat): plugins, main solver->Asolver.t

src/cdsat/TVar.ml

@@ -8,6 +8,10 @@ module Vec_of = Veci
 (* TODO: GC API, + reuse existing slots that have been GC'd at the
    next [new_var_] allocation *)
 
+type reason =
+  | Decide
+  | Propagate of { level: int; hyps: Vec_of.t; proof: Sidekick_proof.step_id }
+
 type store = {
   tst: Term.store;
   of_term: t Term.Weak_map.t;
@@ -20,10 +24,6 @@ type store = {
   new_vars: Vec_of.t;
 }
 
-and reason =
-  | Decide
-  | Propagate of { level: int; hyps: Vec_of.t; proof: Sidekick_proof.step_id }
-
 (* create a new variable *)
 let new_var_ (self : store) ~term:(term_for_v : Term.t) () : t =
   let v : t = Vec.size self.term in
@@ -86,33 +86,6 @@ let pop_new_var self : _ option =
   else
     Some (Vec_of.pop self.new_vars)
 
-module Reason = struct
-  type t = reason =
-    | Decide
-    | Propagate of { level: int; hyps: Vec_of.t; proof: Sidekick_proof.step_id }
-
-  let pp out (self : t) : unit =
-    match self with
-    | Decide -> Fmt.string out "decide"
-    | Propagate { level; hyps; proof = _ } ->
-      Fmt.fprintf out "(@[propagate[lvl=%d]@ :n-hyps %d@])" level
-        (Vec_of.size hyps)
-
-  let decide : t = Decide
-
-  let[@inline] propagate_ level v proof : t =
-    Propagate { level; hyps = v; proof }
-
-  let propagate_v store v proof : t =
-    let level = Vec_of.fold_left (fun l v -> max l (level store v)) 0 v in
-    propagate_ level v proof
-
-  let propagate_l store l proof : t =
-    let v = Vec_of.create ~cap:(List.length l) () in
-    List.iter (Vec_of.push v) l;
-    propagate_v store v proof
-end
-
 module Store = struct
   type t = store
 

src/cdsat/TVar.mli

@@ -20,18 +20,9 @@ module Vec_of : Vec_sig.S with type elt := t
 
 type store = Store.t
 
-(** Reason for assignment *)
+type reason =
-module Reason : sig
+  | Decide
-  type t =
+  | Propagate of { level: int; hyps: Vec_of.t; proof: Sidekick_proof.step_id }
-    | Decide
-    | Propagate of { level: int; hyps: Vec_of.t; proof: Sidekick_proof.step_id }
-
-  include Sidekick_sigs.PRINT with type t := t
-
-  val decide : t
-  val propagate_v : store -> Vec_of.t -> Sidekick_proof.step_id -> t
-  val propagate_l : store -> var list -> Sidekick_proof.step_id -> t
-end
 
 val of_term : store -> Term.t -> t
 (** Obtain a variable for this term. *)

src/cdsat/core.ml

@@ -0,0 +1,80 @@
+open Sidekick_core
+module Proof = Sidekick_proof
+module Asolver = Sidekick_abstract_solver
+module Check_res = Asolver.Check_res
+
+module Plugin_action = struct
+  type t = { propagate: TVar.t -> Value.t -> Reason.t -> unit }
+
+  let propagate (self : t) var v reas : unit = self.propagate var v reas
+end
+
+(** Core plugin *)
+module Plugin = struct
+  type t = {
+    name: string;
+    push_level: unit -> unit;
+    pop_levels: int -> unit;
+    decide: TVar.t -> Value.t option;
+    propagate: Plugin_action.t -> TVar.t -> Value.t -> unit;
+  }
+
+  let make ~name ~push_level ~pop_levels ~decide ~propagate () : t =
+    { name; push_level; pop_levels; decide; propagate }
+end
+
+type t = {
+  tst: Term.store;
+  vst: TVar.store;
+  trail: Trail.t;
+  plugins: Plugin.t Vec.t;
+  mutable last_res: Check_res.t option;
+  proof_tracer: Proof.Tracer.t;
+}
+
+let create tst vst ~proof_tracer () : t =
+  {
+    tst;
+    vst;
+    trail = Trail.create ();
+    plugins = Vec.create ();
+    last_res = None;
+    proof_tracer;
+  }
+
+let[@inline] trail self = self.trail
+let add_plugin self p = Vec.push self.plugins p
+let[@inline] iter_plugins self f = Vec.iter ~f self.plugins
+let[@inline] tst self = self.tst
+let[@inline] vst self = self.vst
+
+(* solving *)
+
+let add_ty (_self : t) ~ty:_ : unit = ()
+let assert_clause (self : t) lits p : unit = assert false
+let assert_term (self : t) t : unit = assert false
+
+let solve ?on_exit ?on_progress ?should_stop ~assumptions (self : t) :
+    Check_res.t =
+  assert false
+
+(* asolver interface *)
+
+let as_asolver (self : t) : Asolver.t =
+  object (asolver)
+    method tst = self.tst
+    method assert_clause lits p : unit = assert_clause self lits p
+
+    method assert_clause_l lits p : unit =
+      asolver#assert_clause (Array.of_list lits) p
+
+    method add_ty ~ty : unit = add_ty self ~ty
+    method lit_of_term ?sign t = Lit.atom ?sign self.tst t
+    method assert_term t : unit = assert_term self t
+    method last_res = self.last_res
+    method proof_tracer = self.proof_tracer
+
+    method solve ?on_exit ?on_progress ?should_stop ~assumptions ()
+        : Check_res.t =
+      solve ?on_exit ?on_progress ?should_stop ~assumptions self
+  end

src/cdsat/core.mli

@@ -0,0 +1,57 @@
+(** Reasoning core *)
+
+open Sidekick_proof
+
+(** {2 Plugins} *)
+
+module Plugin_action : sig
+  type t
+
+  val propagate : t -> TVar.t -> Value.t -> Reason.t -> unit
+end
+
+(** Core plugin *)
+module Plugin : sig
+  type t = private {
+    name: string;
+    push_level: unit -> unit;
+    pop_levels: int -> unit;
+    decide: TVar.t -> Value.t option;
+    propagate: Plugin_action.t -> TVar.t -> Value.t -> unit;
+  }
+
+  val make :
+    name:string ->
+    push_level:(unit -> unit) ->
+    pop_levels:(int -> unit) ->
+    decide:(TVar.t -> Value.t option) ->
+    propagate:(Plugin_action.t -> TVar.t -> Value.t -> unit) ->
+    unit ->
+    t
+end
+
+(** {2 Basics} *)
+
+type t
+
+val create :
+  Term.store -> TVar.store -> proof_tracer:Sidekick_proof.Tracer.t -> unit -> t
+(** Create new solver *)
+
+val tst : t -> Term.store
+val vst : t -> TVar.store
+val trail : t -> Trail.t
+val add_plugin : t -> Plugin.t -> unit
+val iter_plugins : t -> Plugin.t Iter.t
+
+(** {2 Solving} *)
+
+val as_asolver : t -> Sidekick_abstract_solver.t
+
+(*
+  assert (term -> proof -> unit)
+  solve (assumptions:term list -> res)
+
+  as_asolver (-> asolver)
+
+*)

src/cdsat/reason.ml

@@ -0,0 +1,28 @@
+type t = TVar.reason =
+  | Decide
+  | Propagate of {
+      level: int;
+      hyps: TVar.Vec_of.t;
+      proof: Sidekick_proof.step_id;
+    }
+
+let pp out (self : t) : unit =
+  match self with
+  | Decide -> Fmt.string out "decide"
+  | Propagate { level; hyps; proof = _ } ->
+    Fmt.fprintf out "(@[propagate[lvl=%d]@ :n-hyps %d@])" level
+      (TVar.Vec_of.size hyps)
+
+let decide : t = Decide
+let[@inline] propagate_ level v proof : t = Propagate { level; hyps = v; proof }
+
+let propagate_v store v proof : t =
+  let level =
+    TVar.Vec_of.fold_left (fun l v -> max l (TVar.level store v)) 0 v
+  in
+  propagate_ level v proof
+
+let propagate_l store l proof : t =
+  let v = TVar.Vec_of.create ~cap:(List.length l) () in
+  List.iter (TVar.Vec_of.push v) l;
+  propagate_v store v proof

src/cdsat/reason.mli

@@ -0,0 +1,16 @@
+(** Reason for assignment *)
+
+(** Reason for assignment *)
+type t = TVar.reason =
+  | Decide
+  | Propagate of {
+      level: int;
+      hyps: TVar.Vec_of.t;
+      proof: Sidekick_proof.step_id;
+    }
+
+include Sidekick_sigs.PRINT with type t := t
+
+val decide : t
+val propagate_v : TVar.store -> TVar.Vec_of.t -> Sidekick_proof.step_id -> t
+val propagate_l : TVar.store -> TVar.t list -> Sidekick_proof.step_id -> t

src/cdsat/sidekick_cdsat.ml

@@ -2,5 +2,5 @@
 
 module Trail = Trail
 module TVar = TVar
-module Reason = TVar.Reason
+module Reason = Reason
 module Value = Value