mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-10 13:14:09 -05:00
get rid of dependency on unix
This commit is contained in:
parent
facfe336a1
commit
6e5d737b42
5 changed files with 4 additions and 59 deletions
2
META
2
META
|
|
@ -1,7 +1,7 @@
|
||||||
name="msat"
|
name="msat"
|
||||||
version="dev"
|
version="dev"
|
||||||
description="MSAT is a modular SAT solver, plus extensions"
|
description="MSAT is a modular SAT solver, plus extensions"
|
||||||
requires="num unix"
|
requires=""
|
||||||
archive(byte) = "msat.cma"
|
archive(byte) = "msat.cma"
|
||||||
archive(byte, plugin) = "msat.cma"
|
archive(byte, plugin) = "msat.cma"
|
||||||
archive(native) = "msat.cmxa"
|
archive(native) = "msat.cmxa"
|
||||||
|
|
|
||||||
4
_tags
4
_tags
|
|
@ -1,5 +1,5 @@
|
||||||
<util/*.cmx>: for-pack(Msat), package(unix)
|
<util/*.cmx>: for-pack(Msat)
|
||||||
<util/*.native>: package(unix)
|
#<util/*.native>:
|
||||||
<smt/*.cmx>: for-pack(Msat)
|
<smt/*.cmx>: for-pack(Msat)
|
||||||
<sat/*.cmx>: for-pack(Msat)
|
<sat/*.cmx>: for-pack(Msat)
|
||||||
<solver/*.cmx>: for-pack(Msat)
|
<solver/*.cmx>: for-pack(Msat)
|
||||||
|
|
|
||||||
2
opam
2
opam
|
|
@ -15,7 +15,7 @@ remove: [
|
||||||
]
|
]
|
||||||
depends: [
|
depends: [
|
||||||
"ocamlfind" {build}
|
"ocamlfind" {build}
|
||||||
"base-unix"
|
"ocamlbuild" {build}
|
||||||
]
|
]
|
||||||
available: [
|
available: [
|
||||||
ocaml-version >= "4.02.1"
|
ocaml-version >= "4.02.1"
|
||||||
|
|
|
||||||
|
|
@ -1,35 +0,0 @@
|
||||||
(**************************************************************************)
|
|
||||||
(* *)
|
|
||||||
(* Cubicle *)
|
|
||||||
(* Combining model checking algorithms and SMT solvers *)
|
|
||||||
(* *)
|
|
||||||
(* Sylvain Conchon and Alain Mebsout *)
|
|
||||||
(* Universite Paris-Sud 11 *)
|
|
||||||
(* *)
|
|
||||||
(* Copyright 2011. This file is distributed under the terms of the *)
|
|
||||||
(* Apache Software License version 2.0 *)
|
|
||||||
(* *)
|
|
||||||
(**************************************************************************)
|
|
||||||
|
|
||||||
module type S = sig
|
|
||||||
val start : unit -> unit
|
|
||||||
val pause : unit -> unit
|
|
||||||
val get : unit -> float
|
|
||||||
end
|
|
||||||
|
|
||||||
module Make (X : sig end) = struct
|
|
||||||
|
|
||||||
open Unix
|
|
||||||
|
|
||||||
let u = ref 0.0
|
|
||||||
|
|
||||||
let cpt = ref 0.0
|
|
||||||
|
|
||||||
let start () = u:=(times()).tms_utime
|
|
||||||
|
|
||||||
let pause () = cpt := !cpt +. ((times()).tms_utime -. !u)
|
|
||||||
|
|
||||||
let get () =
|
|
||||||
!cpt
|
|
||||||
|
|
||||||
end
|
|
||||||
|
|
@ -1,20 +0,0 @@
|
||||||
(**************************************************************************)
|
|
||||||
(* *)
|
|
||||||
(* Cubicle *)
|
|
||||||
(* Combining model checking algorithms and SMT solvers *)
|
|
||||||
(* *)
|
|
||||||
(* Sylvain Conchon and Alain Mebsout *)
|
|
||||||
(* Universite Paris-Sud 11 *)
|
|
||||||
(* *)
|
|
||||||
(* Copyright 2011. This file is distributed under the terms of the *)
|
|
||||||
(* Apache Software License version 2.0 *)
|
|
||||||
(* *)
|
|
||||||
(**************************************************************************)
|
|
||||||
|
|
||||||
module type S = sig
|
|
||||||
val start : unit -> unit
|
|
||||||
val pause : unit -> unit
|
|
||||||
val get : unit -> float
|
|
||||||
end
|
|
||||||
|
|
||||||
module Make (X : sig end) : S
|
|
||||||
Loading…
Add table
Reference in a new issue