Module Smtlib_syntax


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:


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.


val declare_predicate : string -> string list -> Constant.t
declare_predicate p declares a predicate symbol.



Constant and Variable Creation


val integer : string -> Constant.t
integer i is an integer constant with value i.


val rational : string -> Constant.t
rational r creates a rational constant with value r.


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 SourceForge.net Logo* web site.
*Other names and brands may be claimed as the property of others.