mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-13 22:40:54 -05:00
17 lines
505 B
OCaml
17 lines
505 B
OCaml
(** {1 SMTLib-2 Interface} *)
|
|
|
|
(** This library provides a parser, a type-checker, and a solver interface
|
|
for processing SMTLib-2 problems.
|
|
*)
|
|
|
|
type 'a or_error = ('a, string) CCResult.t
|
|
|
|
module Term = Sidekick_base.Term
|
|
module Stmt = Sidekick_base.Statement
|
|
module Process = Process
|
|
module Solver = Process.Solver
|
|
module Proof = Sidekick_base.Proof_stub (* FIXME: actual DRUP(T) proof *)
|
|
|
|
val parse : Term.store -> string -> Stmt.t list or_error
|
|
|
|
val parse_stdin : Term.store -> Stmt.t list or_error
|