From cd9aa883b2c379b35208e7efe0cc7e6422584250 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 23 Oct 2022 23:51:16 -0400
Subject: [PATCH] wip: feat: start cdsat solver

---
 src/cdsat/TVar.ml           | 106 ++++++++++++++++++++++++++++++++++++
 src/cdsat/TVar.mli          |  52 ++++++++++++++++++
 src/cdsat/dune              |   8 +++
 src/cdsat/sidekick_cdsat.ml |   6 ++
 src/cdsat/trail.ml          |  22 ++++++++
 src/cdsat/trail.mli         |   9 +++
 src/cdsat/types_.ml         |   0
 src/cdsat/value.ml          |   1 +
 src/cdsat/value.mli         |   5 ++
 9 files changed, 209 insertions(+)
 create mode 100644 src/cdsat/TVar.ml
 create mode 100644 src/cdsat/TVar.mli
 create mode 100644 src/cdsat/dune
 create mode 100644 src/cdsat/sidekick_cdsat.ml
 create mode 100644 src/cdsat/trail.ml
 create mode 100644 src/cdsat/trail.mli
 create mode 100644 src/cdsat/types_.ml
 create mode 100644 src/cdsat/value.ml
 create mode 100644 src/cdsat/value.mli

diff --git a/src/cdsat/TVar.ml b/src/cdsat/TVar.ml
new file mode 100644
index 00000000..858a2307
--- /dev/null
+++ b/src/cdsat/TVar.ml
@@ -0,0 +1,106 @@
+type t = int
+type var = t
+
+let pp = Fmt.int
+
+module Vec_of = Veci
+
+(* TODO: GC API, + reuse existing slots that have been GC'd at the
+   next [new_var_] allocation *)
+
+type store = {
+  tst: Term.store;
+  of_term: t Term.Weak_map.t;
+  term: Term.t Vec.t;
+  level: Veci.t;
+  value: Value.t option Vec.t;
+  reason: reason Vec.t;
+  has_value: Bitvec.t;
+  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
+  let { tst = _; of_term = _; term; level; value; reason; has_value; new_vars }
+      =
+    self
+  in
+  Vec.push term term_for_v;
+  Veci.push level (-1);
+  Vec.push value None;
+  Vec.push reason Decide;
+  (* fake *)
+  Bitvec.ensure_size has_value (v + 1);
+  Bitvec.set has_value v false;
+  Vec_of.push new_vars v;
+  v
+
+let of_term (self : store) (t : Term.t) : t =
+  match Term.Weak_map.find_opt self.of_term t with
+  | Some v -> v
+  | None ->
+    let v = new_var_ self ~term:t () in
+    Term.Weak_map.add self.of_term t v;
+    (* TODO: map sub-terms to variables. Perhaps preprocess-like hooks that
+       will allow the variable to be properly defined in one theory? *)
+    v
+
+let has_value (self : store) (v : t) : bool = Bitvec.get self.has_value v
+let level (self : store) (v : t) : int = Veci.get self.level v
+let value (self : store) (v : t) : _ option = Vec.get self.value v
+let term (self : store) (v : t) : Term.t = Vec.get self.term v
+let reason (self : store) (v : t) : reason = Vec.get self.reason v
+
+let pop_new_var self : _ option =
+  if Vec_of.is_empty self.new_vars then
+    None
+  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
+
+  let create tst : t =
+    {
+      tst;
+      of_term = Term.Weak_map.create 256;
+      reason = Vec.create ();
+      term = Vec.create ();
+      level = Veci.create ();
+      value = Vec.create ();
+      has_value = Bitvec.create ();
+      new_vars = Vec_of.create ();
+    }
+end
diff --git a/src/cdsat/TVar.mli b/src/cdsat/TVar.mli
new file mode 100644
index 00000000..13999160
--- /dev/null
+++ b/src/cdsat/TVar.mli
@@ -0,0 +1,52 @@
+(** Variables.
+
+  A variable is a term in the finite basis for CDSAT. It must be assigned
+  a value before the solver can answer "sat".
+*)
+
+type t = private int
+type var = t
+
+(** Store of variables *)
+module Store : sig
+  type t
+
+  val create : Term.store -> t
+  (** Create a new store *)
+end
+
+module Vec_of : Vec_sig.S with type elt := t
+(** Vector of variables *)
+
+type store = Store.t
+
+(** Reason for assignment *)
+module Reason : sig
+  type t =
+    | 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. *)
+
+val term : store -> t -> Term.t
+(** Term for this variable *)
+
+val has_value : store -> t -> bool
+(** Does the variable have a value in the current assignment? *)
+
+val level : store -> t -> int
+(** Level of the current assignment, or [-1] *)
+
+val value : store -> t -> Value.t option
+(** Value in the current assignment *)
+
+val pop_new_var : store -> t option
+(** Pop a new variable if any, or return [None] *)
diff --git a/src/cdsat/dune b/src/cdsat/dune
new file mode 100644
index 00000000..c1f22107
--- /dev/null
+++ b/src/cdsat/dune
@@ -0,0 +1,8 @@
+(library
+ (name sidekick_cdsat)
+ (public_name sidekick.cdsat)
+ (synopsis "CDSAT-based SMT core for sidekick")
+ (flags :standard -open Sidekick_util -open Sidekick_core)
+ (private_modules types_)
+ (libraries containers sidekick.util sidekick.core sidekick.sigs
+   sidekick.proof sidekick.abstract-solver))
diff --git a/src/cdsat/sidekick_cdsat.ml b/src/cdsat/sidekick_cdsat.ml
new file mode 100644
index 00000000..ec81534a
--- /dev/null
+++ b/src/cdsat/sidekick_cdsat.ml
@@ -0,0 +1,6 @@
+(** CDSAT core *)
+
+module Trail = Trail
+module TVar = TVar
+module Reason = TVar.Reason
+module Value = Value
diff --git a/src/cdsat/trail.ml b/src/cdsat/trail.ml
new file mode 100644
index 00000000..008812e8
--- /dev/null
+++ b/src/cdsat/trail.ml
@@ -0,0 +1,22 @@
+module VVec = TVar.Vec_of
+
+type t = { vars: VVec.t; levels: Veci.t }
+
+let create () : t = { vars = VVec.create (); levels = Veci.create () }
+
+let[@inline] push_assignment (self : t) (v : TVar.t) : unit =
+  VVec.push self.vars v
+
+let[@inline] var_at (self : t) (i : int) : TVar.t = VVec.get self.vars i
+let[@inline] n_levels self = Veci.size self.levels
+let push_level (self : t) : unit = Veci.push self.levels (VVec.size self.vars)
+
+let pop_levels (self : t) (n : int) ~f : unit =
+  if n <= n_levels self then (
+    let idx = Veci.get self.levels n in
+    Veci.shrink self.levels n;
+    while VVec.size self.vars > idx do
+      let elt = VVec.pop self.vars in
+      f elt
+    done
+  )
diff --git a/src/cdsat/trail.mli b/src/cdsat/trail.mli
new file mode 100644
index 00000000..00b8b5a1
--- /dev/null
+++ b/src/cdsat/trail.mli
@@ -0,0 +1,9 @@
+(** Trail *)
+
+type t
+
+val create : unit -> t
+val var_at : t -> int -> TVar.t
+val push_assignment : t -> TVar.t -> unit
+
+include Sidekick_sigs.BACKTRACKABLE0_CB with type t := t and type elt := TVar.t
diff --git a/src/cdsat/types_.ml b/src/cdsat/types_.ml
new file mode 100644
index 00000000..e69de29b
diff --git a/src/cdsat/value.ml b/src/cdsat/value.ml
new file mode 100644
index 00000000..45aff785
--- /dev/null
+++ b/src/cdsat/value.ml
@@ -0,0 +1 @@
+include Term
diff --git a/src/cdsat/value.mli b/src/cdsat/value.mli
new file mode 100644
index 00000000..c8e5608d
--- /dev/null
+++ b/src/cdsat/value.mli
@@ -0,0 +1,5 @@
+(** Values *)
+
+type t = Term.t
+
+include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t