module Smtlib_syntax: sig .. end
Compound syntactic constructs occurring in SMT-LIB terms and formulas.
The current setup for SMT-LIB input makes the following
assumptions:
- the benchmark may contain the sort Int or Real,
but not both
exception Syntax_error
Raised when request is not possible for valid SMT-LIB syntax.
Declaration of the Constants and Predicates
val declare_constant : string -> string list -> Constant.t
declare_constant c declares a function symbol.
- Require
declare_constant has not been called before with c
val declare_predicate : string -> string list -> Constant.t
declare_predicate p declares a predicate symbol.
- Require
declare_predicate has not been called before with p
Constant and Variable Creation
val integer : string -> Constant.t
integer i is an integer constant with value i.
- Require i is convertible to an int
val rational : string -> Constant.t
rational r creates a rational constant with value r.
- Require
r is convertible to a rational
val constant : string -> Constant.t
A symbolic constant.
val variable : string -> Variable.t
A variable.
Term Creation
val application : string -> Term.term list -> Term.term
Application of a named function to a list of arguments.
val predicate : string -> Term.term list -> Term.term
Application of a named predicate to a list of arguments.
val connection : string -> Term.term list -> Term.term
Application of a named logical connective to a list of arguments.
val quantification : string -> Variable.t list -> Term.term -> Term.term
A named quantification over a list of variables.
val local_let : Variable.t -> Term.term -> Term.term -> Term.term
Local binding of an expression variable.
val local_flet : Variable.t -> Term.term -> Term.term -> Term.term
Local binding of a formula variable.
Hosted by the
* web site.
*Other names and brands may be claimed as the property
of others.