~james/reorder

2
40efec59037c8cfdff06a3d121284b6212866a65
main
reorder/solver.mli -rw-r--r--651 bytes ViewLogBlameView rawPermalink 908ea7335d feat(core): initialise tso checking and fence synthesis 29 days ago
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
type value = Bits of int64 | Truth of bool
type answer = Sat of value list | Unsat | Unknown of string
type query = { source : string; probes : (string * string) list }
val strategy : string
val solve : ?timeout:int -> ?tick:(unit -> unit) -> query -> answer
val script : ?timeout:int -> ?tick:(unit -> unit) -> string -> string
val compile : ?timeout:int -> ?fixed:int array -> ?require_goal:bool ->
  ?blocks:(int64 * int64) list -> Syntax.t -> Syntax.model -> Syntax.location list -> int -> query
val candidate : count:int -> budget:int -> int list list -> query
val standalone : query -> string
val bits : value -> int64
val truth : value -> bool