Module Sidekick_smtlib

SMTLib-2.6 Driver

This library provides a parser, a type-checker, and a driver for processing SMTLib-2 problems.

type 'a or_error = ('a, string) CCResult.t
module Term = Sidekick_base.Term
module Driver : sig ... end

Driver.

module Solver : sig ... end
module Check_cc : sig ... end
module Model : sig ... end

Models

val parse : Term.store -> string -> Stmt.t list or_error
val parse_stdin : Term.store -> Stmt.t list or_error