refactor to get sidekick-base library

.github/workflows/main.yml

@@ -20,7 +20,7 @@ jobs:
       with:
         ocaml-compiler: ${{ matrix.ocaml-compiler }}
     - run: opam pin -n .
-    - run: opam depext -yt sidekick sidekick-arith sidekick-bin
+    - run: opam depext -yt sidekick sidekick-base sidekick-bin
     - run: opam install -t . --deps-only
     - run: opam exec -- dune build
     - run: opam exec -- dune runtest

sidekick-base.opam

@@ -1,7 +1,7 @@
 opam-version: "2.0"
-name: "sidekick"
+name: "sidekick-base"
 license: "Apache"
-synopsis: "SMT solver based on msat and CDCL(T) (functor library)"
+synopsis: "Standalone term definition for the SMT solver library sidekick"
 version: "dev"
 author: ["Simon Cruanes"]
 maintainer: ["simon.cruanes.2007@m4x.org"]

sidekick.opam

@@ -21,6 +21,10 @@ depends: [
 ]
 depopts: [
   "mtime"   # for profiling stuff
+  "zarith" # for arithmetic
+]
+conflicts: [
+  "zarith" { < "1.8" } # for infix ops
 ]
 tags: [ "sat" "smt" ]
 homepage: "https://github.com/c-cube/sidekick"

src/arith/dune

@@ -0,0 +1,5 @@
+(library
+  (name sidekick_arith)
+  (public_name sidekick.arith)
+  (flags :standard -warn-error -a+8)
+  (libraries sidekick.core sidekick.sigs))

src/arith/sidekick_arith.ml

@@ -0,0 +1,51 @@
+
+module type NUM = sig
+  type t
+
+  val zero : t
+  val one : t
+  val minus_one : t
+
+  val sign : t -> int
+
+  val of_int : int -> t
+  include Sidekick_sigs.EQ with type t := t
+  include Sidekick_sigs.ORD with type t := t
+  include Sidekick_sigs.HASH with type t := t
+  include Sidekick_sigs.PRINT with type t := t
+
+  val (+) : t -> t -> t
+  val (-) : t -> t -> t
+  val ( * ) : t -> t -> t
+  val (~-) : t -> t
+
+  val neg : t -> t
+  val min : t -> t -> t
+  val max : t -> t -> t
+
+  val (=) : t -> t -> bool
+  val (<>) : t -> t -> bool
+  val (>) : t -> t -> bool
+  val (>=) : t -> t -> bool
+  val (<) : t -> t -> bool
+  val (<=) : t -> t -> bool
+end
+
+module type INT = sig
+  include NUM
+
+  val succ : t -> t
+end
+
+module type RATIONAL = sig
+  include NUM
+  type bigint
+
+  val (/) : t -> t -> t
+  val num : t -> bigint
+  val denum : t -> bigint
+
+  val pp_approx : int -> Format.formatter -> t -> unit
+  (** Pretty print rational with given amount of precision
+      (for example as a floating point number) *)
+end

src/base/Base_types.ml

@@ -7,13 +7,13 @@ module CC_view = Sidekick_core.CC_view
 type lra_pred = Sidekick_arith_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
 type lra_op = Sidekick_arith_lra.op = Plus | Minus
 
-type 'a lra_view = 'a Sidekick_arith_lra.lra_view =
+type ('num, 'a) lra_view = ('num, 'a) Sidekick_arith_lra.lra_view =
   | LRA_pred of lra_pred * 'a * 'a
   | LRA_op of lra_op * 'a * 'a
-  | LRA_mult of Q.t * 'a
+  | LRA_mult of 'num * 'a
-  | LRA_const of Q.t
+  | LRA_const of 'num
   | LRA_simplex_var of 'a
-  | LRA_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * Q.t
+  | LRA_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * 'num
   | LRA_other of 'a
 
 (* main term cell. *)
@@ -30,7 +30,7 @@ and 'a term_view =
   | Eq of 'a * 'a
   | Not of 'a
   | Ite of 'a * 'a * 'a
-  | LRA of 'a lra_view
+  | LRA of (Q.t, 'a) lra_view
 
 and fun_ = {
   fun_id: ID.t;
@@ -548,7 +548,7 @@ module Term_cell : sig
     | Eq of 'a * 'a
     | Not of 'a
     | Ite of 'a * 'a * 'a
-    | LRA of 'a lra_view
+    | LRA of (Q.t, 'a) lra_view
 
   type t = term view
 
@@ -562,7 +562,7 @@ module Term_cell : sig
   val eq : term -> term -> t
   val not_ : term -> t
   val ite : term -> term -> term -> t
-  val lra : term lra_view -> t
+  val lra : (Q.t,term) lra_view -> t
 
   val ty : t -> Ty.t
   (** Compute the type of this term cell. Not totally free *)
@@ -591,7 +591,7 @@ end = struct
     | Eq of 'a * 'a
     | Not of 'a
     | Ite of 'a * 'a * 'a
-    | LRA of 'a lra_view
+    | LRA of (Q.t,'a) lra_view
 
   type t = term view
 
@@ -771,7 +771,7 @@ module Term : sig
     | Eq of 'a * 'a
     | Not of 'a
     | Ite of 'a * 'a * 'a
-    | LRA of 'a lra_view
+    | LRA of (Q.t,'a) lra_view
 
   val id : t -> int
   val view : t -> term view
@@ -797,7 +797,7 @@ module Term : sig
   val select : state -> select -> t -> t
   val app_cstor : state -> cstor -> t IArray.t -> t
   val is_a : state -> cstor -> t -> t
-  val lra : state -> t lra_view -> t
+  val lra : state -> (Q.t,t) lra_view -> t
 
   (** Obtain unsigned version of [t], + the sign as a boolean *)
   val abs : state -> t -> t * bool
@@ -846,7 +846,7 @@ end = struct
     | Eq of 'a * 'a
     | Not of 'a
     | Ite of 'a * 'a * 'a
-    | LRA of 'a lra_view
+    | LRA of (Q.t,'a) lra_view
 
   let[@inline] id t = t.term_id
   let[@inline] ty t = t.term_ty
@@ -908,7 +908,7 @@ end = struct
   let is_a st c t : t = app_fun st (Fun.is_a c) (IArray.singleton t)
   let app_cstor st c args : t = app_fun st (Fun.cstor c) args
 
-  let[@inline] lra (st:state) (l:t lra_view) : t =
+  let[@inline] lra (st:state) (l:(Q.t,t) lra_view) : t =
     match l with
     | LRA_other x -> x (* normalize *)
     | _ -> make st (Term_cell.lra l)

src/base/dune

@@ -1,6 +1,7 @@
 (library
- (name sidekick_base_term)
+ (name sidekick_base)
- (public_name sidekick-arith.base-term)
+ (public_name sidekick-base)
- (synopsis "Basic term definitions for the standalone SMT solver")
+ (synopsis "Base term definitions for the standalone SMT solver and library")
- (libraries containers sidekick.core sidekick.util sidekick-arith.lra zarith)
+ (libraries containers sidekick.core sidekick.util sidekick.arith-lra
+            sidekick.zarith zarith)
  (flags :standard -w -32 -open Sidekick_util))

src/lra/dune

@@ -1,6 +1,6 @@
 
 (library
   (name sidekick_arith_lra)
-  (public_name sidekick-arith.lra)
+  (public_name sidekick.arith-lra)
   (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util)
-  (libraries containers sidekick.core zarith))
+  (libraries containers sidekick.core sidekick.arith))

src/lra/sidekick_arith_lra.ml

@@ -10,18 +10,20 @@ module Simplex2 = Simplex2
 module Predicate = Predicate
 module Linear_expr = Linear_expr
 
+module type RATIONAL = Sidekick_arith.RATIONAL
+
 module S_op = Simplex2.Op
 
 type pred = Linear_expr_intf.bool_op = Leq | Geq | Lt | Gt | Eq | Neq
 type op = Plus | Minus
 
-type 'a lra_view =
+type ('num, 'a) lra_view =
   | LRA_pred of pred * 'a * 'a
   | LRA_op of op * 'a * 'a
-  | LRA_mult of Q.t * 'a
+  | LRA_mult of 'num * 'a
-  | LRA_const of Q.t
+  | LRA_const of 'num
   | LRA_simplex_var of 'a (* an opaque variable *)
-  | LRA_simplex_pred of 'a * S_op.t * Q.t (* an atomic constraint *)
+  | LRA_simplex_pred of 'a * S_op.t * 'num (* an atomic constraint *)
   | LRA_other of 'a
 
 let map_view f (l:_ lra_view) : _ lra_view =
@@ -37,16 +39,17 @@ let map_view f (l:_ lra_view) : _ lra_view =
 
 module type ARG = sig
   module S : Sidekick_core.SOLVER
+  module Q : RATIONAL
 
   type term = S.T.Term.t
   type ty = S.T.Ty.t
 
-  val view_as_lra : term -> term lra_view
+  val view_as_lra : term -> (Q.t, term) lra_view
   (** Project the term into the theory view *)
 
   val mk_bool : S.T.Term.state -> bool -> term
 
-  val mk_lra : S.T.Term.state -> term lra_view -> term
+  val mk_lra : S.T.Term.state -> (Q.t, term) lra_view -> term
   (** Make a term from the given theory view *)
 
   val ty_lra : S.T.Term.state -> ty
@@ -129,9 +132,9 @@ module Make(A : ARG) : S with module A = A = struct
       | _ -> None
   end
 
-  module LE_ = Linear_expr.Make(struct include Q let pp=pp_print end)(SimpVar)
+  module LE_ = Linear_expr.Make(A.Q)(SimpVar)
   module LE = LE_.Expr
-  module SimpSolver = Simplex2.Make(SimpVar)
+  module SimpSolver = Simplex2.Make(A.Q)(SimpVar)
   module LConstr = SimpSolver.Constraint
   module Subst = SimpSolver.Subst
 
@@ -205,7 +208,7 @@ module Make(A : ARG) : S with module A = A = struct
   (* return a variable that is equal to [le_comb] in the simplex. *)
   let var_encoding_comb ~pre self (le_comb:LE_.Comb.t) : T.t =
     match LE_.Comb.as_singleton le_comb with
-    | Some (c, x) when Q.(c = one) -> x (* trivial linexp *)
+    | Some (c, x) when A.Q.(c = one) -> x (* trivial linexp *)
     | _ ->
       match Comb_map.find le_comb self.encoded_le with
       | x -> x (* already encoded that *)
@@ -222,10 +225,10 @@ module Make(A : ARG) : S with module A = A = struct
           Log.debug 50 "(lra.encode-le.is-trivially-0)";
           SimpSolver.add_constraint self.simplex
             ~on_propagate:(fun _ ~reason:_ -> ())
-            (SimpSolver.Constraint.leq proxy Q.zero) Tag.By_def;
+            (SimpSolver.Constraint.leq proxy A.Q.zero) Tag.By_def;
           SimpSolver.add_constraint self.simplex
             ~on_propagate:(fun _ ~reason:_ -> ())
-            (SimpSolver.Constraint.geq proxy Q.zero) Tag.By_def;
+            (SimpSolver.Constraint.geq proxy A.Q.zero) Tag.By_def;
         ) else (
           LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
           SimpSolver.define self.simplex proxy (LE_.Comb.to_list le_comb);
@@ -282,7 +285,7 @@ module Make(A : ARG) : S with module A = A = struct
       let l2 = as_linexp ~f:preproc_t t2 in
       let le = LE.(l1 - l2) in
       let le_comb, le_const = LE.comb le, LE.const le in
-      let le_const = Q.neg le_const in
+      let le_const = A.Q.neg le_const in
       (* now we have [le_comb <pred> le_const] *)
 
       begin match LE_.Comb.as_singleton le_comb, pred with
@@ -314,7 +317,7 @@ module Make(A : ARG) : S with module A = A = struct
 
         | Some (coeff, v), pred ->
           (* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *)
-          let q = Q.div le_const coeff in
+          let q = A.Q.( le_const / coeff ) in
           declare_term_to_cc v;
 
           let op = match pred with
@@ -325,7 +328,7 @@ module Make(A : ARG) : S with module A = A = struct
             | Eq | Neq -> assert false
           in
           (* make sure to swap sides if multiplying with a negative coeff *)
-          let op = if Q.(coeff < zero) then S_op.neg_sign op else op in
+          let op = if A.Q.(coeff < zero) then S_op.neg_sign op else op in
 
           let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in
           begin
@@ -343,7 +346,7 @@ module Make(A : ARG) : S with module A = A = struct
       let le = as_linexp ~f:preproc_t t in
       let le_comb, le_const = LE.comb le, LE.const le in
 
-      if Q.(le_const = zero) then (
+      if A.Q.(le_const = zero) then (
         (* if there is no constant, define [proxy] as [proxy := le_comb] and
            return [proxy] *)
         let proxy = var_encoding_comb self ~pre:"_le" le_comb in
@@ -366,7 +369,7 @@ module Make(A : ARG) : S with module A = A = struct
         LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
 
         SimpSolver.define self.simplex proxy2
-          ((Q.minus_one, proxy) :: LE_.Comb.to_list le_comb);
+          ((A.Q.minus_one, proxy) :: LE_.Comb.to_list le_comb);
 
         Log.debugf 50
           (fun k->k "(@[lra.encode-le.with-offset@ %a@ :var %a@ :diff-var %a@])"
@@ -376,10 +379,10 @@ module Make(A : ARG) : S with module A = A = struct
         declare_term_to_cc proxy2;
 
         add_clause [
-          mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, Q.neg le_const)))
+          mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
         ] A.S.P.sorry; (* TODO: by-def proxy2 + LRA *)
         add_clause [
-          mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, Q.neg le_const)))
+          mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
         ] A.S.P.sorry; (* TODO: by-def proxy2 + LRA *)
 
         (* FIXME: actual proof *)
@@ -403,18 +406,18 @@ module Make(A : ARG) : S with module A = A = struct
       if LE.is_const le then (
         let c = LE.const le in
         let is_true = match pred with
-          | Leq -> Q.(c <= zero)
+          | Leq -> A.Q.(c <= zero)
-          | Geq -> Q.(c >= zero)
+          | Geq -> A.Q.(c >= zero)
-          | Lt -> Q.(c < zero)
+          | Lt -> A.Q.(c < zero)
-          | Gt -> Q.(c > zero)
+          | Gt -> A.Q.(c > zero)
-          | Eq -> Q.(c = zero)
+          | Eq -> A.Q.(c = zero)
-          | Neq -> Q.(c <> zero)
+          | Neq -> A.Q.(c <> zero)
         in
         Some (A.mk_bool self.tst is_true, A.S.P.sorry)
       ) else None
     | _ -> None
 
-  module Q_map = CCMap.Make(Q)
+  module Q_map = CCMap.Make(A.Q)
 
   let plit_of_lit lit =
     let t, sign = Lit.signed_term lit in
@@ -471,7 +474,7 @@ module Make(A : ARG) : S with module A = A = struct
 
     let le = LE.(as_linexp_id t1 - as_linexp_id t2) in
     let le_comb, le_const = LE.comb le, LE.const le in
-    let le_const = Q.neg le_const in
+    let le_const = A.Q.neg le_const in
 
     let v = var_encoding_comb ~pre:"le_local_eq" self le_comb in
     let lit = Tag.CC_eq (n1,n2) in
@@ -524,7 +527,7 @@ module Make(A : ARG) : S with module A = A = struct
                  (fun (t1,t2) ->
                     Log.debugf 50
                       (fun k->k "(@[LRA.th-comb.check-pair[val=%a]@ %a@ %a@])"
-                          Q.pp_print _q T.pp t1 T.pp t2);
+                          A.Q.pp _q T.pp t1 T.pp t2);
                     assert(SI.cc_mem_term si t1);
                     assert(SI.cc_mem_term si t2);
                     (* if both [t1] and [t2] are relevant to the congruence

src/lra/simplex2.ml

@@ -7,6 +7,7 @@
 
 open CCMonomorphic
 
+module type RATIONAL = Sidekick_arith.RATIONAL
 module type VAR = Linear_expr_intf.VAR
 
 (** {2 Basic operator} *)
@@ -40,6 +41,7 @@ end
 module type S = sig
   module V : VAR
   module V_map : CCMap.S with type key = V.t
+  module Q : RATIONAL
 
   type num = Q.t (** Numbers *)
 
@@ -139,16 +141,15 @@ end
    by Gaussian elimination) as a preprocessing step, and this removes one column
    and maybe one row if it was basic. *)
 
-module Make(Var: VAR)
+module Make(Q : RATIONAL)(Var: VAR)
-  : S with module V = Var
+  : S with module V = Var and module Q = Q
 = struct
   module V = Var
   module V_map = CCMap.Make(Var)
+  module Q = Q
 
   type num = Q.t (** Numbers *)
-
+  let pp_q_dbg = Q.pp_approx 1
-  let pp_q_float n out q = Fmt.fprintf out "%*.1f" n (Q.to_float q)
-  let pp_q_dbg = pp_q_float 1
 
   module Constraint = struct
     type op = Op.t
@@ -313,7 +314,7 @@ module Make(Var: VAR)
             CCString.pad ~side:`Left 6 @@
             Printf.sprintf "r%d (v%d)" i row.vs.idx in
           Fmt.fprintf out "@,{@[<hov2>%9s: %a@]}" hd
-            (Fmt.iter ~sep:(Fmt.return "@ ") (pp_q_float 6)) (Vec.to_seq row.cols))
+            (Fmt.iter ~sep:(Fmt.return "@ ") (Q.pp_approx 6)) (Vec.to_seq row.cols))
         self.rows;
       Fmt.fprintf out "@;<0 -1>}@]"
     let to_string = Fmt.to_string pp
@@ -1091,11 +1092,11 @@ module Make(Var: VAR)
              | Op.(Geq | Gt), _ when CCBool.equal is_lower Q.(c > zero) ->
                Error.errorf
                  "invalid simplex cert:@ %a@ variable %a has coeff of the wrong sign %a"
-                 Unsat_cert.pp cert Var.pp x Q.pp_print c
+                 Unsat_cert.pp cert Var.pp x pp_q_dbg c
              | Op.(Lt | Leq), _ when CCBool.equal is_lower Q.(c < zero) ->
                Error.errorf
                  "invalid simplex cert:@ %a@ variable %a has coeff of the wrong sign %a"
-                 Unsat_cert.pp cert Var.pp x Q.pp_print c
+                 Unsat_cert.pp cert Var.pp x pp_q_dbg c
              | _, b -> Erat.(sum + c * b.b_val))
           Erat.zero le
       in

src/lra/simplex_intf.ml

@@ -11,7 +11,11 @@
     implementation at https://gbury.eu/public/papers/stage-m2.pdf
 *)
 
+module type RATIONAL = Sidekick_arith.RATIONAL
+
 module type S = sig
+  module Q : RATIONAL
+
   (** The given type of the variables *)
   type var
 

src/lra/tests/dune

@@ -1,13 +1,14 @@
 (executable
  (name run_tests)
  (modules run_tests test_simplex2)
- (libraries containers sidekick-arith.lra zarith iter alcotest qcheck)
+ (libraries containers sidekick.arith-lra
+            sidekick.zarith zarith iter alcotest qcheck)
  (flags :standard -warn-error -a+8 -color always))
 
 (alias
  (name runtest)
  (locks /test)
- (package sidekick-arith)
+ (package sidekick)
  (action
    (progn
      (run ./run_tests.exe alcotest) ; run regressions first

src/lra/tests/test_simplex2.real.ml

@@ -17,7 +17,11 @@ module Var = struct
   let not_lit i = Some (- i)
 end
 
-module Spl = Sidekick_arith_lra.Simplex2.Make(Var)
+module Spl = Sidekick_arith_lra.Simplex2.Make(Sidekick_zarith.Rational)(Var)
+
+let unwrap_opt_ msg = function
+  | Some x -> x
+  | None -> failwith msg
 
 let rand_n low n : Z.t QC.arbitrary =
   QC.map ~rev:Z.to_int Z.of_int QC.(low -- n)
@@ -32,7 +36,7 @@ let rand_q_with u l : Q.t QC.arbitrary =
   in
   (* avoid [undef] when shrinking *)
   let shrink q yield =
-    CCOpt.get_exn qc.QC.shrink q (fun x -> if Q.is_real x then yield x)
+    unwrap_opt_ "no shrinker" qc.QC.shrink q (fun x -> if Q.is_real x then yield x)
   in
   QC.set_shrink shrink qc
 

src/main/dune

@@ -4,8 +4,8 @@
  (name main)
  (public_name sidekick)
  (package sidekick-bin)
- (libraries containers iter result msat sidekick.core sidekick-arith.base-term
+ (libraries containers iter result msat sidekick.core sidekick-base
-   sidekick.msat-solver sidekick-bin.smtlib sidekick.tef)
+            sidekick.msat-solver sidekick-bin.smtlib sidekick.tef)
  (flags :standard -safe-string -color always -open Sidekick_util))
 
 (rule

src/main/main.ml

@@ -8,7 +8,7 @@ open CCResult.Infix
 
 module E = CCResult
 module Fmt = CCFormat
-module Term = Sidekick_base_term.Term
+module Term = Sidekick_base.Term
 module Solver = Sidekick_smtlib.Solver
 module Process = Sidekick_smtlib.Process
 module Vec = Msat.Vec
@@ -89,7 +89,7 @@ let argspec = Arg.align [
   ] |> List.sort compare
 
 module Dimacs = struct
-  open Sidekick_base_term
+  open Sidekick_base
   module T = Term
 
   let parse_file tst (file:string) : Statement.t list or_error =
@@ -99,7 +99,7 @@ module Dimacs = struct
         match Util.Int_tbl.find atoms (abs i) with
         | x -> Term.const tst x
         | exception Not_found ->
-          let f = Sidekick_base_term.Fun.mk_undef_const
+          let f = Sidekick_base.Fun.mk_undef_const
               (ID.makef "%d" (abs i)) (Ty.bool()) in
           Util.Int_tbl.add atoms (abs i) f;
           Term.const tst f

src/mini-cc/tests/dune

@@ -1,6 +1,6 @@
 (tests
  (names tests)
- (libraries sidekick.mini-cc sidekick-arith.base-term alcotest)
+ (libraries sidekick.mini-cc sidekick-base alcotest)
- (package sidekick-arith)
+ (package sidekick-base)
  (locks /test)
  (modes native))

src/mini-cc/tests/tests.ml

@@ -1,10 +1,9 @@
 open Sidekick_util
-
+open Sidekick_base
-open Sidekick_base_term
 
 module A = Alcotest
 module CC = Sidekick_mini_cc.Make(struct
-  module T = Sidekick_base_term.Arg
+  module T = Sidekick_base.Arg
   let cc_view = Term.cc_view
 end)
 

src/sigs/dune

@@ -0,0 +1,4 @@
+(library
+  (name sidekick_sigs)
+  (public_name sidekick.sigs)
+  (libraries containers iter))

src/smtlib/Form.ml

@@ -1,4 +1,4 @@
-open Sidekick_base_term
+open Sidekick_base
 
 module T = Term
 open Sidekick_th_bool_static

src/smtlib/Process.ml

@@ -1,8 +1,8 @@
 (** {2 Conversion into {!Term.t}} *)
 
-module BT = Sidekick_base_term
+module BT = Sidekick_base
 module Profile = Sidekick_util.Profile
-open Sidekick_base_term
+open Sidekick_base
 
 [@@@ocaml.warning "-32"]
 
@@ -13,7 +13,7 @@ module Fmt = CCFormat
 
 (* instantiate solver here *)
 module Solver_arg = struct
-  module T = Sidekick_base_term
+  module T = Sidekick_base
 
   let cc_view = Term.cc_view
   let is_valid_literal _ = true
@@ -366,6 +366,7 @@ 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
 

src/smtlib/Process.mli

@@ -1,6 +1,6 @@
 (** {1 Process Statements} *)
 
-open Sidekick_base_term
+open Sidekick_base
 
 module Solver
   : Sidekick_msat_solver.S with type T.Term.t = Term.t

src/smtlib/Sidekick_smtlib.ml

@@ -1,14 +1,13 @@
 (** {1 Process Statements} *)
 
-module ID = Sidekick_base_term.ID
+module ID = Sidekick_base.ID
 module E = CCResult
 module Loc = Smtlib_utils.V_2_6.Loc
 module Parse_ast = Smtlib_utils.V_2_6.Ast
 module Process = Process
 module Solver = Process.Solver
-module Term = Sidekick_base_term.Term
+module Term = Sidekick_base.Term
-module Stmt = Sidekick_base_term.Statement
+module Stmt = Sidekick_base.Statement
-module Proof = Proof
 
 type 'a or_error = ('a, string) CCResult.t
 

src/smtlib/Sidekick_smtlib.mli

@@ -6,8 +6,8 @@
 
 type 'a or_error = ('a, string) CCResult.t
 
-module Term = Sidekick_base_term.Term
+module Term = Sidekick_base.Term
-module Stmt = Sidekick_base_term.Statement
+module Stmt = Sidekick_base.Statement
 module Process = Process
 module Solver = Process.Solver
 

src/smtlib/Typecheck.ml

@@ -2,13 +2,13 @@
 
 (** {1 Preprocessing AST} *)
 
-open Sidekick_base_term
+open Sidekick_base
 module Loc = Smtlib_utils.V_2_6.Loc
 module Fmt = CCFormat
 module Log = Msat.Log
 
 module PA = Smtlib_utils.V_2_6.Ast
-module BT = Sidekick_base_term
+module BT = Sidekick_base
 module Ty = BT.Ty
 module T = BT.Term
 module Fun = BT.Fun

src/smtlib/Typecheck.mli

@@ -4,8 +4,8 @@
 
 module Loc = Smtlib_utils.V_2_6.Loc
 module PA = Smtlib_utils.V_2_6.Ast
-module T = Sidekick_base_term.Term
+module T = Sidekick_base.Term
-module Stmt = Sidekick_base_term.Statement
+module Stmt = Sidekick_base.Statement
 
 type 'a or_error = ('a, string) CCResult.t
 

src/smtlib/dune

@@ -2,7 +2,11 @@
  (name sidekick_smtlib)
  (public_name sidekick-bin.smtlib)
  (libraries containers zarith msat sidekick.core sidekick.util
-   sidekick.msat-solver sidekick-arith.base-term sidekick.th-bool-static
+            sidekick.msat-solver
-   sidekick.mini-cc sidekick.th-data sidekick-arith.lra msat.backend smtlib-utils
+            sidekick.th-bool-static
-   sidekick.tef)
+            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))

src/util/Sidekick_util.ml

@@ -8,8 +8,9 @@ module Backtrack_stack = Backtrack_stack
 module Backtrackable_tbl = Backtrackable_tbl
 module Error = Error
 module IArray = IArray
-module Intf = Intf
 module Bag = Bag
 module Stat = Stat
 module Hash = Hash
 module Profile = Profile
+
+module Intf = Sidekick_sigs

src/util/dune

@@ -1,4 +1,4 @@
 (library
   (name sidekick_util)
   (public_name sidekick.util)
-  (libraries containers iter msat))
+  (libraries containers iter msat sidekick.sigs))

src/zarith/dune

@@ -0,0 +1,6 @@
+(library
+  (name sidekick_zarith)
+  (public_name sidekick.zarith)
+  (optional) ; dep on zarith
+  (flags :standard -warn-error -a+8)
+  (libraries sidekick.core sidekick.arith zarith))

src/zarith/sidekick_zarith.ml

@@ -0,0 +1,20 @@
+
+
+module Int : Sidekick_arith.INT with type t = Z.t = struct
+  include Z
+  include Z.Compare
+  let pp = pp_print
+end
+
+module Rational
+  : Sidekick_arith.RATIONAL with type t = Q.t and type bigint = Z.t
+= struct
+  type bigint = Z.t
+  include Q
+  let denum = den
+  let pp = pp_print
+  let hash a = Hashtbl.hash (Z.hash (num a), Z.hash (den a))
+
+  let pp_approx n out q = Format.fprintf out "%*.1f" n (Q.to_float q)
+end
+

src/zarith/sidekick_zarith.mli

@@ -0,0 +1,4 @@
+
+module Int : Sidekick_arith.INT with type t = Z.t
+
+module Rational : Sidekick_arith.RATIONAL with type t = Q.t and type bigint = Z.t