refactor: add solver instance in sidekick base

move some functor instantiations from `sidekick-bin.smtlib` to
`sidekick-base.solver` so they're usable from a library.

doc/deploy

@@ -1,28 +0,0 @@
-#!/bin/bash -e
-
-# Ensure we are on master branch
-git checkout master
-
-# Generate documentation
-make doc
-(cd doc && asciidoc index.txt)
-
-# Checkout gh-pages
-git checkout gh-pages
-git pull
-
-# Copy doc to the right locations
-cp doc/index.html ./
-cp msat.docdir/* ./dev/
-
-# Add potentially new pages
-git add ./dev/*
-git add ./index.html
-
-# Commit it all & push
-git commit -m 'Doc update'
-git push
-
-# Get back to master branch
-git checkout master
-

doc/index.txt

@@ -1,10 +0,0 @@
-
-mSAT
-====
-Guillaume Bury <guillaume.bury@gmail.com>
-
-* link:dev[]
-* link:0.5[]
-* link:0.5.1[]
-* link:0.6[]
-

doc/release

@@ -1,34 +0,0 @@
-#!/bin/bash -e
-
-# Get current verison number
-version=`cat VERSION`
-
-# Enssure we are on master branch
-git checkout master
-
-# Generate documentation
-make doc
-(cd doc && asciidoc index.txt)
-
-# Checkout gh-pages
-git checkout gh-pages
-git pull
-
-# Create doc folder if it does not exists
-mkdir -p ./$version
-
-# Copy doc to the right locations
-cp doc/index.html ./
-cp msat.docdir/* ./$version/
-
-# Add potentially new pages
-git add ./$version/*
-git add ./index.html
-
-# Commit it all & push
-git commit -m "Doc release $version"
-git push
-
-# Get back to master branch
-git checkout master
-

sidekick-base.opam

@@ -20,6 +20,7 @@ depends: [
   "alcotest" {with-test}
   "qcheck" {with-test & >= "0.16" }
   "odoc" {with-doc}
+  "ocaml-mdx" {with-test}
 ]
 tags: [ "sat" "smt" ]
 homepage: "https://github.com/c-cube/sidekick"

src/base-solver/Form.ml

@@ -1,3 +1,13 @@
+
+(** Formulas (boolean terms).
+
+    This module defines function symbols, constants, and views
+    to manipulate boolean formulas in {!Sidekick_base}.
+    This is useful to have the ability to use boolean connectives instead
+    of being limited to clauses; by using {!Sidekick_th_bool_static},
+    the formulas are turned into clauses automatically for you.
+*)
+
 open Sidekick_base
 
 module T = Term

src/base-solver/dune

@@ -0,0 +1,9 @@
+(library
+  (name sidekick_base_solver)
+  (public_name sidekick-base.solver)
+  (synopsis "Instantiation of solver and theories for Sidekick_base")
+  (libraries sidekick-base sidekick.core sidekick.msat-solver
+            sidekick.th-bool-static
+            sidekick.mini-cc sidekick.th-data
+            sidekick.arith-lra sidekick.zarith)
+  (flags :standard -warn-error -a+8 -safe-string -color always -open Sidekick_util))

src/base-solver/sidekick_base_solver.ml

@@ -0,0 +1,119 @@
+
+(** SMT Solver and Theories for [Sidekick_base].
+
+    This contains instances of the SMT solver, and theories,
+    from {!Sidekick_core}, using data structures from
+    {!Sidekick_base}. *)
+
+open Sidekick_base
+
+module Form = Form
+
+(** Argument to the SMT solver *)
+module Solver_arg = struct
+  module T = Sidekick_base
+
+  let cc_view = Term.cc_view
+  let is_valid_literal _ = true
+  module P = Proof
+end
+
+(** SMT solver, obtained from {!Sidekick_msat_solver} *)
+module Solver = Sidekick_msat_solver.Make(Solver_arg)
+
+(** Theory of datatypes *)
+module Th_data = Sidekick_th_data.Make(struct
+    module S = Solver
+    open Base_types
+    open Sidekick_th_data
+    module Cstor = Cstor
+
+    let as_datatype ty = match Ty.view ty with
+      | Ty_atomic {def=Ty_data data;_} ->
+        Ty_data {cstors=Lazy.force data.data.data_cstors |> ID.Map.values}
+      | Ty_atomic {def=_;args;finite=_} ->
+        Ty_app{args=Iter.of_list args}
+      | Ty_bool | Ty_real -> Ty_app {args=Iter.empty}
+
+    let view_as_data t = match Term.view t with
+      | Term.App_fun ({fun_view=Fun.Fun_cstor c;_}, args) -> T_cstor (c, args)
+      | Term.App_fun ({fun_view=Fun.Fun_select sel;_}, args) ->
+        assert (IArray.length args=1);
+        T_select (sel.select_cstor, sel.select_i, IArray.get args 0)
+      | Term.App_fun ({fun_view=Fun.Fun_is_a c;_}, args) ->
+        assert (IArray.length args=1);
+        T_is_a (c, IArray.get args 0)
+      | _ -> T_other t
+
+    let mk_eq = Term.eq
+    let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args
+    let mk_sel tst c i u = Term.app_fun tst (Fun.select_idx c i) (IArray.singleton u)
+    let mk_is_a tst c u : Term.t =
+      if c.cstor_arity=0 then (
+        Term.eq tst u (Term.const tst (Fun.cstor c))
+      ) else (
+        Term.app_fun tst (Fun.is_a c) (IArray.singleton u)
+      )
+
+    let ty_is_finite = Ty.finite
+    let ty_set_is_finite = Ty.set_finite
+
+    let proof_isa_disj = Proof.isa_disj
+    let proof_isa_split = Proof.isa_split
+    let proof_cstor_inj = Proof.cstor_inj
+  end)
+
+(** Reducing boolean formulas to clauses *)
+module Th_bool = Sidekick_th_bool_static.Make(struct
+  module S = Solver
+  type term = S.T.Term.t
+  include Form
+  let proof_bool_eq = Proof.bool_eq
+  let proof_bool_c = Proof.bool_c
+  let proof_ite_true = Proof.ite_true
+  let proof_ite_false = Proof.ite_false
+end)
+
+(** Theory of Linear Rational Arithmetic *)
+module Th_lra = Sidekick_arith_lra.Make(struct
+  module S = Solver
+  module T = Term
+  module Q = Sidekick_zarith.Rational
+  type term = S.T.Term.t
+  type ty = S.T.Ty.t
+
+  let mk_eq = Form.eq
+  let mk_lra = T.lra
+  let mk_bool = T.bool
+  let view_as_lra t = match T.view t with
+    | T.LRA l -> l
+    | T.Eq (a,b) when Ty.equal (T.ty a) (Ty.real()) -> LRA_pred (Eq, a, b)
+    | _ -> LRA_other t
+
+  let ty_lra _st = Ty.real()
+  let has_ty_real t = Ty.equal (T.ty t) (Ty.real())
+
+  let proof_lra = Proof.lra
+  let proof_lra_l = Proof.lra_l
+
+  module Gensym = struct
+    type t = {
+      tst: T.state;
+      mutable fresh: int;
+    }
+
+    let create tst : t = {tst; fresh=0}
+    let tst self = self.tst
+    let copy s = {s with tst=s.tst}
+
+    let fresh_term (self:t) ~pre (ty:Ty.t) : T.t =
+      let name = Printf.sprintf "_sk_lra_%s%d" pre self.fresh in
+      self.fresh <- 1 + self.fresh;
+      let id = ID.make name in
+      Term.const self.tst @@ Fun.mk_undef_const id ty
+  end
+end)
+
+let th_bool : Solver.theory = Th_bool.theory
+let th_data : Solver.theory = Th_data.theory
+let th_lra : Solver.theory = Th_lra.theory

src/base/Sidekick_base.ml

@@ -31,6 +31,11 @@ module Data = Base_types.Data
 module Select = Base_types.Select
 module Proof = Proof
 
+(** Concrete implementation of {!Sidekick_core.TERM}
+
+    this module gathers most definitions above in a form
+    that is compatible with what Sidekick expects for terms, functions, etc.
+*)
 module Arg
   : Sidekick_core.TERM
     with type Term.t = Term.t

src/smtlib/Process.ml

@@ -3,6 +3,7 @@
 module BT = Sidekick_base
 module Profile = Sidekick_util.Profile
 open Sidekick_base
+module SBS = Sidekick_base_solver
 
 [@@@ocaml.warning "-32"]
 
@@ -11,15 +12,7 @@ type 'a or_error = ('a, string) CCResult.t
 module E = CCResult
 module Fmt = CCFormat
 
-(* instantiate solver here *)
+module Solver = SBS.Solver
-module Solver_arg = struct
-  module T = Sidekick_base
-
-  let cc_view = Term.cc_view
-  let is_valid_literal _ = true
-  module P = Proof
-end
-module Solver = Sidekick_msat_solver.Make(Solver_arg)
 
 module Check_cc = struct
   module Lit = Solver.Solver_internal.Lit
@@ -312,95 +305,9 @@ let process_stmt
       Error.errorf "cannot deal with definitions yet"
   end
 
-module Th_data = Sidekick_th_data.Make(struct
+module Th_data = SBS.Th_data
-    module S = Solver
+module Th_bool = SBS.Th_bool
-    open Base_types
+module Th_lra = SBS.Th_lra
-    open Sidekick_th_data
-    module Cstor = Cstor
-
-    let as_datatype ty = match Ty.view ty with
-      | Ty_atomic {def=Ty_data data;_} ->
-        Ty_data {cstors=Lazy.force data.data.data_cstors |> ID.Map.values}
-      | Ty_atomic {def=_;args;finite=_} ->
-        Ty_app{args=Iter.of_list args}
-      | Ty_bool | Ty_real -> Ty_app {args=Iter.empty}
-
-    let view_as_data t = match Term.view t with
-      | Term.App_fun ({fun_view=Fun.Fun_cstor c;_}, args) -> T_cstor (c, args)
-      | Term.App_fun ({fun_view=Fun.Fun_select sel;_}, args) ->
-        assert (IArray.length args=1);
-        T_select (sel.select_cstor, sel.select_i, IArray.get args 0)
-      | Term.App_fun ({fun_view=Fun.Fun_is_a c;_}, args) ->
-        assert (IArray.length args=1);
-        T_is_a (c, IArray.get args 0)
-      | _ -> T_other t
-
-    let mk_eq = Term.eq
-    let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args
-    let mk_sel tst c i u = Term.app_fun tst (Fun.select_idx c i) (IArray.singleton u)
-    let mk_is_a tst c u : Term.t =
-      if c.cstor_arity=0 then (
-        Term.eq tst u (Term.const tst (Fun.cstor c))
-      ) else (
-        Term.app_fun tst (Fun.is_a c) (IArray.singleton u)
-      )
-
-    let ty_is_finite = Ty.finite
-    let ty_set_is_finite = Ty.set_finite
-
-    let proof_isa_disj = Proof.isa_disj
-    let proof_isa_split = Proof.isa_split
-    let proof_cstor_inj = Proof.cstor_inj
-  end)
-
-module Th_bool = Sidekick_th_bool_static.Make(struct
-  module S = Solver
-  type term = S.T.Term.t
-  include Form
-  let proof_bool_eq = Proof.bool_eq
-  let proof_bool_c = Proof.bool_c
-  let proof_ite_true = Proof.ite_true
-  let proof_ite_false = Proof.ite_false
-end)
-
-module Th_lra = Sidekick_arith_lra.Make(struct
-  module S = Solver
-  module T = BT.Term
-  module Q = Sidekick_zarith.Rational
-  type term = S.T.Term.t
-  type ty = S.T.Ty.t
-
-  let mk_eq = Form.eq
-  let mk_lra = T.lra
-  let mk_bool = T.bool
-  let view_as_lra t = match T.view t with
-    | T.LRA l -> l
-    | T.Eq (a,b) when Ty.equal (T.ty a) (Ty.real()) -> LRA_pred (Eq, a, b)
-    | _ -> LRA_other t
-
-  let ty_lra _st = Ty.real()
-  let has_ty_real t = Ty.equal (T.ty t) (Ty.real())
-
-  let proof_lra = Proof.lra
-  let proof_lra_l = Proof.lra_l
-
-  module Gensym = struct
-    type t = {
-      tst: T.state;
-      mutable fresh: int;
-    }
-
-    let create tst : t = {tst; fresh=0}
-    let tst self = self.tst
-    let copy s = {s with tst=s.tst}
-
-    let fresh_term (self:t) ~pre (ty:Ty.t) : T.t =
-      let name = Printf.sprintf "_sk_lra_%s%d" pre self.fresh in
-      self.fresh <- 1 + self.fresh;
-      let id = ID.make name in
-      BT.Term.const self.tst @@ Fun.mk_undef_const id ty
-  end
-end)
 
 let th_bool : Solver.theory = Th_bool.theory
 let th_data : Solver.theory = Th_data.theory

src/smtlib/dune

@@ -2,11 +2,7 @@
  (name sidekick_smtlib)
  (public_name sidekick-bin.smtlib)
  (libraries containers zarith msat sidekick.core sidekick.util
-            sidekick.msat-solver
+            sidekick-base sidekick-base.solver
-            sidekick.th-bool-static
-            sidekick.mini-cc sidekick.th-data
-            sidekick.arith-lra sidekick.zarith
-            sidekick-base
             msat.backend smtlib-utils
             sidekick.tef)
  (flags :standard -warn-error -a+8 -open Sidekick_util))