chore: add sidekick-arith library, depends on zarith

.travis.yml

@@ -5,11 +5,13 @@ services:
 - docker
 env:
   global:
-  - PINS="sidekick:. sidekick-bin:."
+    - PINS="sidekick:. sidekick-arith:. sidekick-bin:."
   - DISTRO="ubuntu-16.04"
   matrix:
   - PACKAGE="sidekick" CAML_VERSION="4.03"
   - PACKAGE="sidekick" CAML_VERSION="4.06"
   - PACKAGE="sidekick" CAML_VERSION="4.08"
   - PACKAGE="sidekick" CAML_VERSION="4.10"
+  - PACKAGE="sidekick-arith" CAML_VERSION="4.03"
+  - PACKAGE="sidekick-arith" CAML_VERSION="4.10"
   - PACKAGE="sidekick-bin" CAML_VERSION="4.06"

sidekick-arith.opam

@@ -0,0 +1,25 @@
+opam-version: "2.0"
+name: "sidekick"
+license: "Apache"
+synopsis: "SMT solver based on msat and CDCL(T) (functor library)"
+version: "dev"
+author: ["Simon Cruanes"]
+maintainer: ["simon.cruanes.2007@m4x.org"]
+build: [
+  ["dune" "build" "@install" "-p" name "-j" jobs]
+  ["dune" "build" "@doc" "-p" name "-j" jobs ] {with-doc}
+  ["dune" "runtest" "-p" name "-j" jobs] {with-test}
+]
+depends: [
+  "dune" { >= "1.1" }
+  "containers" { >= "3.0" & < "4.0" }
+  "iter" { >= "1.0" & < "2.0" }
+  "ocaml" { >= "4.03" }
+  "zarith"
+  "alcotest" {with-test}
+]
+tags: [ "sat" "smt" ]
+homepage: "https://github.com/c-cube/sidekick"
+dev-repo: "git+https://github.com/c-cube/sidekick.git"
+bug-reports: "https://github.com/c-cube/sidekick/issues/"
+

src/arith/lra/dune

@@ -1,7 +1,7 @@
 
 (library
-  (name sidekick_lra)
+  (name sidekick_arith_lra)
-  (public_name sidekick.th-lra)
+  (public_name sidekick-arith.lra)
   (optional) ; only if deps present
   (flags :standard -warn-error -a+8 -open Sidekick_util)
   (libraries containers sidekick.core zarith))

src/base-term/Base_types.ml

@@ -4,10 +4,10 @@ module Fmt = CCFormat
 
 module CC_view = Sidekick_core.CC_view
 
-type lra_pred = Sidekick_lra.FM.Pred.t = Lt | Leq | Geq | Gt | Neq | Eq
+type lra_pred = Sidekick_arith_lra.FM.Pred.t = Lt | Leq | Geq | Gt | Neq | Eq
-type lra_op = Sidekick_lra.op = Plus | Minus
+type lra_op = Sidekick_arith_lra.op = Plus | Minus
 
-type 'a lra_view = 'a Sidekick_lra.lra_view =
+type 'a lra_view = '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
@@ -726,7 +726,7 @@ end = struct
     | Not u -> Not (f u)
     | Eq (a,b) -> Eq (f a, f b)
     | Ite (a,b,c) -> Ite (f a, f b, f c)
-    | LRA l -> LRA (Sidekick_lra.map_view f l)
+    | LRA l -> LRA (Sidekick_arith_lra.map_view f l)
 
   module Tbl = CCHashtbl.Make(struct
       type t = term view
@@ -964,7 +964,7 @@ end = struct
     | Not u -> not_ tst (f u)
     | Eq (a,b) -> eq tst (f a) (f b)
     | Ite (a,b,c) -> ite tst (f a) (f b) (f c)
-    | LRA l -> lra tst (Sidekick_lra.map_view f l)
+    | LRA l -> lra tst (Sidekick_arith_lra.map_view f l)
 end
 
 module Value : sig

src/base-term/dune

@@ -2,5 +2,5 @@
  (name sidekick_base_term)
  (public_name sidekick.base-term)
  (synopsis "Basic term definitions for the standalone SMT solver")
- (libraries containers sidekick.core sidekick.util sidekick.th-lra zarith)
+ (libraries containers sidekick.core sidekick.util sidekick-arith.lra zarith)
  (flags :standard -w -32 -open Sidekick_util))

src/cc/dune

@@ -4,4 +4,4 @@
   (name Sidekick_cc)
   (public_name sidekick.cc)
   (libraries containers iter sidekick.core sidekick.util)
-  (flags :standard -warn-error -a+8 -open Sidekick_util))
+  (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util))

src/smtlib/Process.ml

@@ -302,7 +302,7 @@ module Th_bool = Sidekick_th_bool_static.Make(struct
   include Form
 end)
 
-module Th_lra = Sidekick_lra.Make(struct
+module Th_lra = Sidekick_arith_lra.Make(struct
   module S = Solver
   module T = BT.Term
   type term = S.T.Term.t

src/smtlib/dune

@@ -3,7 +3,5 @@
  (public_name sidekick-bin.smtlib)
  (libraries containers zarith msat sidekick.core sidekick.util
    sidekick.msat-solver sidekick.base-term sidekick.th-bool-static
-   sidekick.mini-cc sidekick.th-data sidekick.th-lra msat.backend smtlib-utils)
+   sidekick.mini-cc sidekick.th-data sidekick-arith.lra msat.backend smtlib-utils)
  (flags :standard -warn-error -a+8 -open Sidekick_util))
-
-; TODO: enable warn-error again