feat(cdsat): term_to_var conversion, with hooks; solver wrapper

src/cdsat/TVar.ml

@@ -3,6 +3,8 @@ type var = t
 
 let pp = Fmt.int
 
+type theory_view = ..
+
 module Vec_of = Veci
 
 (* TODO: GC API, + reuse existing slots that have been GC'd at the
@@ -12,6 +14,8 @@ type reason =
   | Decide
   | Propagate of { level: int; hyps: Vec_of.t; proof: Sidekick_proof.step_id }
 
+let dummy_level_ = -1
+
 type store = {
   tst: Term.store;
   of_term: t Term.Weak_map.t;
@@ -19,13 +23,14 @@ type store = {
   level: Veci.t;
   value: Value.t option Vec.t;
   reason: reason Vec.t;
+  theory_views: theory_view Vec.t;
   watches: t Vec.t Vec.t;
   has_value: Bitvec.t;
   new_vars: Vec_of.t;
 }
 
 (* create a new variable *)
-let new_var_ (self : store) ~term:(term_for_v : Term.t) () : t =
+let new_var_ (self : store) ~term:(term_for_v : Term.t) ~theory_view () : t =
   let v : t = Vec.size self.term in
   let {
     tst = _;
@@ -35,43 +40,39 @@ let new_var_ (self : store) ~term:(term_for_v : Term.t) () : t =
     value;
     watches;
     reason;
+    theory_views;
     has_value;
     new_vars;
   } =
     self
   in
   Vec.push term term_for_v;
-  Veci.push level (-1);
+  Veci.push level dummy_level_;
   Vec.push value None;
   (* fake *)
   Vec.push reason Decide;
   Vec.push watches (Vec.create ());
+  Vec.push theory_views theory_view;
   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[@inline] get_of_term (self : store) (t : Term.t) : t option =
+  Term.Weak_map.find_opt self.of_term t
 
 let[@inline] has_value (self : store) (v : t) : bool =
   Bitvec.get self.has_value v
 
 let[@inline] level (self : store) (v : t) : int = Veci.get self.level v
 let[@inline] value (self : store) (v : t) : _ option = Vec.get self.value v
+let[@inline] theory_view (self : store) (v : t) = Vec.get self.theory_views v
 
-let[@inline] set_value (self : store) (v : t) value : unit =
-  Vec.set self.value v (Some value)
-
-let[@inline] unset_value (self : store) (v : t) : unit =
-  Vec.set self.value v None
+let[@inline] bool_value (self : store) (v : t) : _ option =
+  match Vec.get self.value v with
+  | Some v when Term.is_true v -> Some true
+  | Some v when Term.is_false v -> Some false
+  | _ -> None
 
 let[@inline] term (self : store) (v : t) : Term.t = Vec.get self.term v
 let[@inline] reason (self : store) (v : t) : reason = Vec.get self.reason v
@@ -80,6 +81,21 @@ let[@inline] watchers (self : store) (v : t) : t Vec.t = Vec.get self.watches v
 let[@inline] add_watcher (self : store) (v : t) ~watcher : unit =
   Vec.push (watchers self v) watcher
 
+let assign (self : store) (v : t) ~value ~level ~reason : unit =
+  Log.debugf 50 (fun k ->
+      k "(@[cdsat.assign[lvl=%d]@ %a@ :val %a@])" level
+        (Term.pp_limit ~max_depth:5 ~max_nodes:30)
+        (term self v) Term.pp value);
+  assert (level >= 0);
+  Vec.set self.value v (Some value);
+  Vec.set self.reason v reason;
+  Veci.set self.level v level
+
+let unassign (self : store) (v : t) : unit =
+  Vec.set self.value v None;
+  Veci.set self.level v dummy_level_;
+  Vec.set self.reason v Decide
+
 let pop_new_var self : _ option =
   if Vec_of.is_empty self.new_vars then
     None
@@ -98,7 +114,22 @@ module Store = struct
       level = Veci.create ();
       watches = Vec.create ();
       value = Vec.create ();
+      theory_views = Vec.create ();
       has_value = Bitvec.create ();
       new_vars = Vec_of.create ();
     }
 end
+
+let pp (self : store) out (v : t) : unit =
+  let t = term self v in
+  Fmt.fprintf out "(@[var[%d]@ :term %a@])" v
+    (Term.pp_limit ~max_depth:5 ~max_nodes:30)
+    t
+
+module Internal = struct
+  let create (self : store) (t : Term.t) ~theory_view : t =
+    assert (not @@ Term.Weak_map.mem self.of_term t);
+    let v = new_var_ self ~term:t ~theory_view () in
+    Term.Weak_map.add self.of_term t v;
+    v
+end

src/cdsat/TVar.mli

@@ -7,6 +7,9 @@
 type t = private int
 type var = t
 
+type theory_view = ..
+(** The theory-specific data *)
+
 (** Store of variables *)
 module Store : sig
   type t
@@ -24,8 +27,8 @@ type reason =
   | Decide
   | Propagate of { level: int; hyps: Vec_of.t; proof: Sidekick_proof.step_id }
 
-val of_term : store -> Term.t -> t
-(** Obtain a variable for this term. *)
+val get_of_term : store -> Term.t -> t option
+(** Get variable from term, if already associated *)
 
 val term : store -> t -> Term.t
 (** Term for this variable *)
@@ -39,8 +42,14 @@ val level : store -> t -> int
 val value : store -> t -> Value.t option
 (** Value in the current assignment *)
 
-val set_value : store -> t -> Value.t -> unit
-val unset_value : store -> t -> unit
+val bool_value : store -> t -> bool option
+(** Value in the current assignment, as a boolean *)
+
+val theory_view : store -> t -> theory_view
+(** Theory-specific view of the variable *)
+
+val assign : store -> t -> value:Value.t -> level:int -> reason:reason -> unit
+val unassign : store -> t -> unit
 
 val watchers : store -> t -> t Vec.t
 (** [watchers store t] is a vector of other variables watching [t],
@@ -51,3 +60,15 @@ val add_watcher : store -> t -> watcher:t -> unit
 
 val pop_new_var : store -> t option
 (** Pop a new variable if any, or return [None] *)
+
+val pp : store -> t Fmt.printer
+
+(**/**)
+
+module Internal : sig
+  val create : store -> Term.t -> theory_view:theory_view -> t
+  (** Obtain a variable for this term. Fails if the term already maps
+      to a variable. *)
+end
+
+(**/**)

src/cdsat/core.ml

@@ -1,7 +1,12 @@
 open Sidekick_core
 module Proof = Sidekick_proof
-module Asolver = Sidekick_abstract_solver
-module Check_res = Asolver.Check_res
+module Check_res = Sidekick_abstract_solver.Check_res
+
+(** Argument to the solver *)
+module type ARG = sig
+  val or_l : Term.store -> Term.t list -> Term.t
+  (** build a disjunction *)
+end
 
 module Plugin_action = struct
   type t = { propagate: TVar.t -> Value.t -> Reason.t -> unit }
@@ -17,68 +22,99 @@ module Plugin = struct
     pop_levels: int -> unit;
     decide: TVar.t -> Value.t option;
     propagate: Plugin_action.t -> TVar.t -> Value.t -> unit;
+    term_to_var_hooks: Term_to_var.hook list;
   }
 
-  let make ~name ~push_level ~pop_levels ~decide ~propagate () : t =
-    { name; push_level; pop_levels; decide; propagate }
+  let make ~name ~push_level ~pop_levels ~decide ~propagate ~term_to_var_hooks
+      () : t =
+    { name; push_level; pop_levels; decide; propagate; term_to_var_hooks }
 end
 
 type t = {
   tst: Term.store;
   vst: TVar.store;
+  arg: (module ARG);
   stats: Stat.t;
   trail: Trail.t;
   plugins: Plugin.t Vec.t;
+  term_to_var: Term_to_var.t;
   mutable last_res: Check_res.t option;
   proof_tracer: Proof.Tracer.t;
 }
 
-let create ?(stats = Stat.create ()) tst vst ~proof_tracer () : t =
+let create ?(stats = Stat.create ()) ~arg tst vst ~proof_tracer () : t =
   {
     tst;
     vst;
+    arg;
     stats;
     trail = Trail.create ();
     plugins = Vec.create ();
+    term_to_var = Term_to_var.create vst;
     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
+let[@inline] last_res self = self.last_res
+
+(* backtracking *)
+
+let n_levels (self : t) : int = Trail.n_levels self.trail
+
+let push_level (self : t) : unit =
+  Log.debugf 50 (fun k -> k "(@[cdsat.core.push-level@])");
+  Trail.push_level self.trail;
+  Vec.iter self.plugins ~f:(fun (p : Plugin.t) -> p.push_level ());
+  ()
+
+let pop_levels (self : t) n : unit =
+  Log.debugf 50 (fun k -> k "(@[cdsat.core.pop-levels %d@])" n);
+  if n > 0 then self.last_res <- None;
+  Trail.pop_levels self.trail n ~f:(fun v -> TVar.unassign self.vst v);
+  Vec.iter self.plugins ~f:(fun (p : Plugin.t) -> p.pop_levels n);
+  ()
+
+(* term to var *)
+
+let[@inline] get_term_to_var self = self.term_to_var
+
+let[@inline] term_to_var self t : TVar.t =
+  Term_to_var.convert self.term_to_var t
+
+let add_term_to_var_hook self h = Term_to_var.add_hook self.term_to_var h
+
+(* plugins *)
+
+let add_plugin self p =
+  Vec.push self.plugins p;
+  List.iter (add_term_to_var_hook self) p.term_to_var_hooks
 
 (* 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 pp_stats out self = Stat.pp out self.stats
 
-let solve ?on_exit ?on_progress ?should_stop ~assumptions (self : t) :
+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@])" (TVar.pp self.vst) v Value.pp value);
+  self.last_res <- None;
+  match TVar.value self.vst v with
+  | None ->
+    TVar.assign self.vst v ~value ~level:v_level ~reason;
+    Trail.push_assignment self.trail v
+  | Some value' when Value.equal value value' -> () (* idempotent *)
+  | Some value' ->
+    (* TODO: conflict *)
+    Log.debugf 0 (fun k -> k "TODO: conflict (incompatible values)");
+    ()
+
+let solve ~on_exit ~on_progress ~should_stop ~assumptions (self : t) :
     Check_res.t =
+  self.last_res <- None;
+  (* TODO: outer loop (propagate; decide)* *)
+  (* TODO: propagation loop, involving plugins *)
   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 pp_stats out () = pp_stats out self
-
-    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

@@ -1,6 +1,13 @@
 (** Reasoning core *)
 
 open Sidekick_proof
+module Check_res = Sidekick_abstract_solver.Check_res
+
+(** Argument to the solver *)
+module type ARG = sig
+  val or_l : Term.store -> Term.t list -> Term.t
+  (** build a disjunction *)
+end
 
 (** {2 Plugins} *)
 
@@ -18,6 +25,7 @@ module Plugin : sig
     pop_levels: int -> unit;
     decide: TVar.t -> Value.t option;
     propagate: Plugin_action.t -> TVar.t -> Value.t -> unit;
+    term_to_var_hooks: Term_to_var.hook list;
   }
 
   val make :
@@ -26,6 +34,7 @@ module Plugin : sig
     pop_levels:(int -> unit) ->
     decide:(TVar.t -> Value.t option) ->
     propagate:(Plugin_action.t -> TVar.t -> Value.t -> unit) ->
+    term_to_var_hooks:Term_to_var.hook list ->
     unit ->
     t
 end
@@ -36,12 +45,13 @@ type t
 
 val create :
   ?stats:Stat.t ->
+  arg:(module ARG) ->
   Term.store ->
   TVar.store ->
   proof_tracer:Sidekick_proof.Tracer.t ->
   unit ->
   t
-(** Create new solver *)
+(** Create new core solver *)
 
 val tst : t -> Term.store
 val vst : t -> TVar.store
@@ -49,14 +59,28 @@ val trail : t -> Trail.t
 val add_plugin : t -> Plugin.t -> unit
 val iter_plugins : t -> Plugin.t Iter.t
 
-(** {2 Solving} *)
+val last_res : t -> Check_res.t option
+(** Last result. Reset on backtracking/assertion *)
 
-val as_asolver : t -> Sidekick_abstract_solver.t
+(** {2 Backtracking} *)
 
-(*
-  assert (term -> proof -> unit)
-  solve (assumptions:term list -> res)
+include Sidekick_sigs.BACKTRACKABLE0 with type t := t
 
-  as_asolver (-> asolver)
+(** {2 Map terms to variables} *)
 
-*)
+val get_term_to_var : t -> Term_to_var.t
+val term_to_var : t -> Term.t -> TVar.t
+val add_term_to_var_hook : t -> Term_to_var.hook -> unit
+
+(** {2 Main solving API} *)
+
+val assign :
+  t -> TVar.t -> value:Value.t -> level:int -> reason:Reason.t -> unit
+
+val solve :
+  on_exit:(unit -> unit) ->
+  on_progress:(unit -> unit) ->
+  should_stop:(unit -> bool) ->
+  assumptions:Term.t list ->
+  t ->
+  Check_res.t

src/cdsat/sidekick_cdsat.ml

@@ -5,3 +5,5 @@ module TVar = TVar
 module Reason = Reason
 module Value = Value
 module Core = Core
+module Solver = Solver
+module Term_to_var = Term_to_var

src/cdsat/solver.ml

@@ -0,0 +1,87 @@
+open Sidekick_core
+module Proof = Sidekick_proof
+module Asolver = Sidekick_abstract_solver
+module Check_res = Asolver.Check_res
+module Plugin_action = Core.Plugin_action
+module Plugin = Core.Plugin
+
+module type ARG = Core.ARG
+
+type t = {
+  tst: Term.store;
+  vst: TVar.store;
+  core: Core.t;
+  stats: Stat.t;
+  proof_tracer: Proof.Tracer.t;
+}
+
+let create ?(stats = Stat.create ()) ~arg tst vst ~proof_tracer () : t =
+  let core = Core.create ~stats ~arg tst vst ~proof_tracer () in
+  { tst; vst; core; stats; proof_tracer }
+
+let[@inline] core self = self.core
+let add_plugin self p = Core.add_plugin self.core p
+let[@inline] iter_plugins self f = Core.iter_plugins self.core f
+let[@inline] tst self = self.tst
+let[@inline] vst self = self.vst
+
+(* solving *)
+
+let add_ty (_self : t) ~ty:_ : unit = ()
+
+let assert_term_ (self : t) (t : Term.t) pr : unit =
+  Log.debugf 50 (fun k -> k "(@[cdsat.core.assert@ %a@])" Term.pp t);
+  let sign, t = Term.abs self.tst t in
+  let v = Core.term_to_var self.core t in
+  match TVar.value self.vst v with
+  | None ->
+    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 -> ()
+  | Some value when Term.is_true value && not sign -> () (* TODO: conflict *)
+  | Some value when Term.is_false value && sign -> () (* TODO: conflict *)
+  (* TODO: conflict *)
+  | Some value ->
+    Error.errorf "cdsat.assert@ value for %a@ should be true or false,@ not %a"
+      (TVar.pp self.vst) v Value.pp value
+
+let assert_term self t : unit =
+  let pr () =
+    let lit = Lit.atom self.tst t in
+    Proof.Sat_rules.sat_input_clause [ lit ]
+  in
+  assert_term_ self t pr
+
+let assert_clause (self : t) lits p : unit = assert false (* TODO *)
+
+let pp_stats out self = Stat.pp out self.stats
+
+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 = Core.last_res self.core
+    method proof_tracer = self.proof_tracer
+    method pp_stats out () = pp_stats out self
+
+    method solve ?on_exit ?on_progress ?should_stop ~assumptions ()
+        : Check_res.t =
+      solve ?on_exit ?on_progress ?should_stop ~assumptions self
+  end

src/cdsat/solver.mli

@@ -0,0 +1,36 @@
+(** Main solver interface.
+
+   This is the interface to the user, presenting SMT solver operations.
+   It relies on {!Core} to implement the CDSAT calculus, and
+   implements the {!Sidekick_abstract_solver} generic interface on top of it.
+*)
+
+open Sidekick_proof
+module Plugin_action = Core.Plugin_action
+module Plugin = Core.Plugin
+
+module type ARG = Core.ARG
+
+(** {2 Basics} *)
+
+type t
+
+val create :
+  ?stats:Stat.t ->
+  arg:(module ARG) ->
+  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 core : t -> Core.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

src/cdsat/term_to_var.ml

@@ -0,0 +1,24 @@
+type t = { vst: TVar.store; mutable hooks: hook list }
+and hook = t -> Term.t -> TVar.theory_view option
+
+let create vst : t = { vst; hooks = [] }
+let add_hook self h = self.hooks <- h :: self.hooks
+
+let rec convert (self : t) (t : Term.t) : TVar.t =
+  let rec try_hooks = function
+    | [] ->
+      (* no hook worked *)
+      Error.errorf "cdsat.term-to-var: no hook accepted term `%a`"
+        (Term.pp_limit ~max_depth:5 ~max_nodes:30)
+        t
+    | h :: tl_h ->
+      (match h self t with
+      | Some theory_view ->
+        let v = TVar.Internal.create self.vst t ~theory_view in
+        v
+      | None -> try_hooks tl_h)
+  in
+
+  match TVar.get_of_term self.vst t with
+  | Some v -> v
+  | None -> try_hooks self.hooks

src/cdsat/term_to_var.mli

@@ -0,0 +1,30 @@
+(** Conversion from terms to variables.
+
+   Terms are context free and can undergo simplification, rewriting, etc.
+   In contrast, CDSAT is concerned with the stateful manipulation of a finite
+   set of variables and their assignment in the current (partial) model.
+ *)
+
+type t
+(** The converter *)
+
+val create : TVar.store -> t
+
+(** {2 Conversion} *)
+
+val convert : t -> Term.t -> TVar.t
+(** Convert a term into a variable.
+    This will fail if there is no hook that recognizes the term (meaning the
+    term is not handled by any theory) *)
+
+(** {2 Hooks}
+
+    Hooks are responsible for converting {b some} terms (the terms their theory
+    knows) into variables. *)
+
+type hook = t -> Term.t -> TVar.theory_view option
+(** A hook, responsible to keep some internal state and assigning a theory
+    view if it "accepts" the term. A term that is recognized by no hook
+    cannot be turned into a variable. *)
+
+val add_hook : t -> hook -> unit

src/core-logic/t_builtins.ml

@@ -126,6 +126,16 @@ let is_bool t =
   | E_const { c_view = C_bool; _ } -> true
   | _ -> false
 
+let is_true t =
+  match view t with
+  | E_const { c_view = C_true; _ } -> true
+  | _ -> false
+
+let is_false t =
+  match view t with
+  | E_const { c_view = C_false; _ } -> true
+  | _ -> false
+
 let is_eq t =
   match view t with
   | E_const { c_view = C_eq; _ } -> true

src/core-logic/t_builtins.mli

@@ -25,6 +25,8 @@ val ite : store -> t -> t -> t -> t
 
 val is_eq : t -> bool
 val is_bool : t -> bool
+val is_true : t -> bool
+val is_false : t -> bool
 
 val abs : store -> t -> bool * t
 (** [abs t] returns an "absolute value" for the term, along with the

src/main/main.ml

@@ -189,8 +189,13 @@ let main_smt ~config () : _ result =
     if !cdsat then
       let open Sidekick_cdsat in
       let vst = TVar.Store.create tst in
-      Core.create tst vst ~proof_tracer:(tracer :> Proof.Tracer.t) ()
-      |> Core.as_asolver
+      let arg =
+        (module struct
+          let or_l = Sidekick_base.Form.or_l
+        end : Solver.ARG)
+      in
+      Solver.create tst vst ~arg ~proof_tracer:(tracer :> Proof.Tracer.t) ()
+      |> Solver.as_asolver
     else (
       (* TODO: probes, to load only required theories *)
       let theories =