module Smtlib_parser: sig .. end
Combined SMT-LIB file parser interface.
A parser for the SMT-LIB syntax as described in
The SMT-LIB
Standard Version 1.2 (30 August 2006).
type 'a tokenizer = Lexing.lexbuf -> 'a
Generic tokenizer.
type ('a, 'b) recognizer = 'a tokenizer -> Lexing.lexbuf -> 'b
Generic parser.
val initialized : unit -> bool
Has the parser been initialized?
val initialize : string ->
'a tokenizer ->
('a, Smtlib_attribute.attribute list) recognizer ->
('a, Smtlib_attribute.attribute list) recognizer ->
('a, Smtlib_attribute.attribute list) recognizer -> unit
initialize smtlib tokenizer theory_parser logic_parser
benchmark_parser initializes the combined smtlib file parser.
smtlib is the path to the standard SMT-LIB library filestokenizer is the tokenizer to usetheory_parser is the entry point for the theory nonterminallogic_parser is the entry point for the logic nonterminalbenchmark_parser is the entry point for the benchmark nonterminal
val smtlib_theory_file : string -> string
smtlib_theory_file name is the path to the SMT-LIB theory file
describing the theory called
name.
val smtlib_logic_file : string -> string
smtlib_logic_file name is the path to the SMT-LIB logic file
describing the logic called
name.
val parse_theory : string -> Smtlib_attribute.attribute list
parse_theory path parses the SMT-LIB theory file at the
specified path and returns the attributes of theory.
val parse_logic : string -> Smtlib_attribute.attribute list
parse_logic path parses the SMT-LIB logic file at the
specified path and returns the attributes of logic.
val parse_benchmark : string -> Smtlib_attribute.attribute list
parse_logic path parses the SMT-LIB benchmark file at the
specified path and returns the attributes of benchmark.
Hosted by the
* web site.
*Other names and brands may be claimed as the property
of others.