feat: add sidekick.abstract solver

this library provides an abstract interface for what a SMT solver provides,
independently of the underlying implementation technology.

src/abstract-solver/asolver.ml

@@ -0,0 +1,65 @@
+(** Abstract interface for a solver *)
+
+open Sidekick_core
+module Unknown = Unknown
+module Check_res = Check_res
+
+class type t =
+  object
+    method assert_term : Term.t -> unit
+    (** Helper that turns the term into an atom, before adding the result
+        to the solver as a unit clause assertion.
+
+        This uses {!Proof_sat.sat_input_clause} to justify the assertion. *)
+
+    method assert_clause : Lit.t array -> Proof_step.id -> unit
+    (** [add_clause solver cs] adds a boolean clause to the solver.
+      Subsequent calls to {!solve} will need to satisfy this clause. *)
+
+    method assert_clause_l : Lit.t list -> Proof_step.id -> unit
+    (** Add a clause to the solver, given as a list. *)
+
+    method add_ty : ty:Term.t -> unit
+    (** Add a new sort/atomic type. *)
+
+    method lit_of_term : ?sign:bool -> Term.t -> Lit.t
+    (** Convert a term into a simplified literal. *)
+
+    method solve :
+      ?on_exit:(unit -> unit) list ->
+      ?on_progress:(unit -> unit) ->
+      ?should_stop:(int -> bool) ->
+      assumptions:Lit.t list ->
+      unit ->
+      Check_res.t
+    (** Checks the satisfiability of the clauses added so far to the solver.
+        @param assumptions a set of atoms held to be true. The unsat core,
+          if any, will be a subset of [assumptions].
+        @param on_progress called regularly during solving.
+        @param should_stop a callback regularly called from within the solver.
+          It is given a number of "steps" done since last call. The exact notion
+          of step is not defined, but is guaranteed to increase regularly.
+          The function should return [true] if it judges solving
+          must stop (returning [Unknown]), [false] if solving can proceed.
+        @param on_exit functions to be run before this returns *)
+
+    method last_res : Check_res.t option
+    (** Returns the result of the last call to {!solve}, if the logic statee
+        has not changed (mostly by asserting new clauses). *)
+
+    method proof : Proof_trace.t
+    (** TODO: remove, use Tracer instead *)
+  end
+
+let assert_term (self : #t) t : unit = self#assert_term t
+let assert_clause (self : #t) c p : unit = self#assert_clause c p
+let assert_clause_l (self : #t) c p : unit = self#assert_clause_l c p
+let add_ty (self : #t) ~ty : unit = self#add_ty ~ty
+let lit_of_term (self : #t) ?sign t : Lit.t = self#lit_of_term ?sign t
+
+let solve (self : #t) ?on_exit ?on_progress ?should_stop ~assumptions () :
+    Check_res.t =
+  self#solve ?on_exit ?on_progress ?should_stop ~assumptions ()
+
+let last_res (self : #t) = self#last_res
+let proof (self : #t) : Proof_trace.t = self#proof

src/abstract-solver/check_res.ml

@@ -0,0 +1,21 @@
+(** Result of solving for the current set of clauses *)
+
+module Model = Sidekick_model
+
+(** Result of calling "check" *)
+type t =
+  | Sat of Model.t  (** Satisfiable *)
+  | Unsat of {
+      unsat_core: unit -> Lit.t Iter.t;
+          (** Unsat core (subset of assumptions), or empty *)
+      unsat_step_id: unit -> Proof_trace.step_id option;
+          (** Proof step for the empty clause *)
+    }  (** Unsatisfiable *)
+  | Unknown of Unknown.t
+      (** Unknown, obtained after a timeout, memory limit, etc. *)
+
+let pp out (self : t) =
+  match self with
+  | Sat _ -> Fmt.string out "Sat"
+  | Unsat _ -> Fmt.string out "Unsat"
+  | Unknown u -> Fmt.fprintf out "Unknown(%a)" Unknown.pp u

src/abstract-solver/dune

@@ -0,0 +1,7 @@
+
+(library
+  (name sidekick_abstract_solver)
+  (public_name sidekick.abstract-solver)
+  (flags :standard -open Sidekick_util -open Sidekick_core)
+  (libraries containers iter
+             sidekick.core sidekick.model))

src/abstract-solver/sidekick_abstract_solver.ml

@@ -0,0 +1,8 @@
+(** Abstract interface for a solver *)
+
+module Unknown = Unknown
+module Check_res = Check_res
+module Asolver = Asolver
+
+class type t = Asolver.t
+(** Main abstract solver type *)

src/abstract-solver/unknown.ml

@@ -0,0 +1,7 @@
+type t = U_timeout | U_max_depth | U_incomplete | U_asked_to_stop
+
+let pp out = function
+  | U_timeout -> Fmt.string out {|"timeout"|}
+  | U_max_depth -> Fmt.string out {|"max depth reached"|}
+  | U_incomplete -> Fmt.string out {|"incomplete fragment"|}
+  | U_asked_to_stop -> Fmt.string out {|"asked to stop by callback"|}

src/abstract-solver/unknown.mli

@@ -0,0 +1,3 @@
+type t = U_timeout | U_max_depth | U_incomplete | U_asked_to_stop
+
+val pp : t Fmt.printer