diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 6a88a374..26efc36d 100644 --- a/.github/workflows/main.yml +++ b/.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 diff --git a/sidekick-arith.opam b/sidekick-base.opam similarity index 88% rename from sidekick-arith.opam rename to sidekick-base.opam index f3d5cdb6..09a600e6 100644 --- a/sidekick-arith.opam +++ b/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"] diff --git a/sidekick.opam b/sidekick.opam index 2216081c..7f27208f 100644 --- a/sidekick.opam +++ b/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" diff --git a/src/arith/dune b/src/arith/dune new file mode 100644 index 00000000..b7b0394a --- /dev/null +++ b/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)) diff --git a/src/arith/sidekick_arith.ml b/src/arith/sidekick_arith.ml new file mode 100644 index 00000000..86433456 --- /dev/null +++ b/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 diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml index 15fc467c..24951f77 100644 --- a/src/base/Base_types.ml +++ b/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_const of Q.t + | LRA_mult of 'num * 'a + | 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) diff --git a/src/base/dune b/src/base/dune index 166a4547..0a4f5d5e 100644 --- a/src/base/dune +++ b/src/base/dune @@ -1,6 +1,7 @@ (library - (name sidekick_base_term) - (public_name sidekick-arith.base-term) - (synopsis "Basic term definitions for the standalone SMT solver") - (libraries containers sidekick.core sidekick.util sidekick-arith.lra zarith) + (name sidekick_base) + (public_name sidekick-base) + (synopsis "Base term definitions for the standalone SMT solver and library") + (libraries containers sidekick.core sidekick.util sidekick.arith-lra + sidekick.zarith zarith) (flags :standard -w -32 -open Sidekick_util)) diff --git a/src/lra/dune b/src/lra/dune index 145750fd..74ba4ece 100644 --- a/src/lra/dune +++ b/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)) diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index be1b9de5..9188fd5b 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/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_const of Q.t + | LRA_mult of 'num * 'a + | 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 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) - | Geq -> Q.(c >= zero) - | Lt -> Q.(c < zero) - | Gt -> Q.(c > zero) - | Eq -> Q.(c = zero) - | Neq -> Q.(c <> zero) + | Leq -> A.Q.(c <= zero) + | Geq -> A.Q.(c >= zero) + | Lt -> A.Q.(c < zero) + | Gt -> A.Q.(c > zero) + | Eq -> A.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 diff --git a/src/lra/simplex2.ml b/src/lra/simplex2.ml index faba6681..0dd86552 100644 --- a/src/lra/simplex2.ml +++ b/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) - : S with module V = Var +module Make(Q : RATIONAL)(Var: 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_float n out q = Fmt.fprintf out "%*.1f" n (Q.to_float q) - let pp_q_dbg = pp_q_float 1 + let pp_q_dbg = Q.pp_approx 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 "@,{@[%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 diff --git a/src/lra/simplex_intf.ml b/src/lra/simplex_intf.ml index a466d26d..fe0302d7 100644 --- a/src/lra/simplex_intf.ml +++ b/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 diff --git a/src/lra/tests/dune b/src/lra/tests/dune index 006b7b5f..5661451c 100644 --- a/src/lra/tests/dune +++ b/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 diff --git a/src/lra/tests/test_simplex2.real.ml b/src/lra/tests/test_simplex2.real.ml index 4920cc18..65d1bf5f 100644 --- a/src/lra/tests/test_simplex2.real.ml +++ b/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 diff --git a/src/main/dune b/src/main/dune index 5a8ae94c..621bc88c 100644 --- a/src/main/dune +++ b/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 - sidekick.msat-solver sidekick-bin.smtlib sidekick.tef) + (libraries containers iter result msat sidekick.core sidekick-base + sidekick.msat-solver sidekick-bin.smtlib sidekick.tef) (flags :standard -safe-string -color always -open Sidekick_util)) (rule diff --git a/src/main/main.ml b/src/main/main.ml index ec72a84d..8b61bb49 100644 --- a/src/main/main.ml +++ b/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 diff --git a/src/mini-cc/tests/dune b/src/mini-cc/tests/dune index 29dc21ae..6b0fb30d 100644 --- a/src/mini-cc/tests/dune +++ b/src/mini-cc/tests/dune @@ -1,6 +1,6 @@ (tests (names tests) - (libraries sidekick.mini-cc sidekick-arith.base-term alcotest) - (package sidekick-arith) + (libraries sidekick.mini-cc sidekick-base alcotest) + (package sidekick-base) (locks /test) (modes native)) diff --git a/src/mini-cc/tests/tests.ml b/src/mini-cc/tests/tests.ml index aff28efa..8f6326af 100644 --- a/src/mini-cc/tests/tests.ml +++ b/src/mini-cc/tests/tests.ml @@ -1,10 +1,9 @@ open Sidekick_util - -open Sidekick_base_term +open Sidekick_base 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) diff --git a/src/sigs/dune b/src/sigs/dune new file mode 100644 index 00000000..80c324e5 --- /dev/null +++ b/src/sigs/dune @@ -0,0 +1,4 @@ +(library + (name sidekick_sigs) + (public_name sidekick.sigs) + (libraries containers iter)) diff --git a/src/util/Intf.ml b/src/sigs/sidekick_sigs.ml similarity index 100% rename from src/util/Intf.ml rename to src/sigs/sidekick_sigs.ml diff --git a/src/smtlib/Form.ml b/src/smtlib/Form.ml index da1709a7..74e68e33 100644 --- a/src/smtlib/Form.ml +++ b/src/smtlib/Form.ml @@ -1,4 +1,4 @@ -open Sidekick_base_term +open Sidekick_base module T = Term open Sidekick_th_bool_static diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 5dba5e27..f972aa17 100644 --- a/src/smtlib/Process.ml +++ b/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 diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index abe20f0b..451f096f 100644 --- a/src/smtlib/Process.mli +++ b/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 diff --git a/src/smtlib/Sidekick_smtlib.ml b/src/smtlib/Sidekick_smtlib.ml index 8af04dec..3cbeb07b 100644 --- a/src/smtlib/Sidekick_smtlib.ml +++ b/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 Stmt = Sidekick_base_term.Statement -module Proof = Proof +module Term = Sidekick_base.Term +module Stmt = Sidekick_base.Statement type 'a or_error = ('a, string) CCResult.t diff --git a/src/smtlib/Sidekick_smtlib.mli b/src/smtlib/Sidekick_smtlib.mli index 6c9a3c6b..c9d0acbb 100644 --- a/src/smtlib/Sidekick_smtlib.mli +++ b/src/smtlib/Sidekick_smtlib.mli @@ -6,8 +6,8 @@ type 'a or_error = ('a, string) CCResult.t -module Term = Sidekick_base_term.Term -module Stmt = Sidekick_base_term.Statement +module Term = Sidekick_base.Term +module Stmt = Sidekick_base.Statement module Process = Process module Solver = Process.Solver diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 1199255a..1ee83b81 100644 --- a/src/smtlib/Typecheck.ml +++ b/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 diff --git a/src/smtlib/Typecheck.mli b/src/smtlib/Typecheck.mli index ca0caf72..ca63f595 100644 --- a/src/smtlib/Typecheck.mli +++ b/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 Stmt = Sidekick_base_term.Statement +module T = Sidekick_base.Term +module Stmt = Sidekick_base.Statement type 'a or_error = ('a, string) CCResult.t diff --git a/src/smtlib/dune b/src/smtlib/dune index 2e0a0136..0ed9ebdd 100644 --- a/src/smtlib/dune +++ b/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.mini-cc sidekick.th-data sidekick-arith.lra msat.backend smtlib-utils - sidekick.tef) + sidekick.msat-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)) diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml index 53b0b2a3..01ae1f46 100644 --- a/src/util/Sidekick_util.ml +++ b/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 diff --git a/src/util/dune b/src/util/dune index a8802b38..93411a31 100644 --- a/src/util/dune +++ b/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)) diff --git a/src/zarith/dune b/src/zarith/dune new file mode 100644 index 00000000..c72885d1 --- /dev/null +++ b/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)) diff --git a/src/zarith/sidekick_zarith.ml b/src/zarith/sidekick_zarith.ml new file mode 100644 index 00000000..00601f4c --- /dev/null +++ b/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 + diff --git a/src/zarith/sidekick_zarith.mli b/src/zarith/sidekick_zarith.mli new file mode 100644 index 00000000..d41bf118 --- /dev/null +++ b/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