[SMT-LIB] Auto-discard notification
tinelli at cs.uiowa.edu
Thu Oct 1 12:36:03 EDT 2009
with regards to your request below, George Hagen, the main developer
of the parser, says the following:
"You should be able to clear out all of the persistent data structures
as part of a loop, and then re-start the parser from scratch. There
is currently no functionality for this, but I believe that all the
relevant tables and refs are in tables.ml, with a few more in
In order to call the parser incrementally on different benchmarks
would require significantly more work."
I hope this helps for now.
Since George moved to bigger and better things, if anybody in this
list is willing to modify the parser to make it restartable or
incremental as a service to the SMT-LIB community, please let know.
PS: You must subscribe to this email list first to be able to send
messages to it.
On 1 Oct 2009, at 04:52, smt-lib-bounces at cs.nyu.edu wrote:
> The attached message has been automatically discarded.
> From: Laurent Théry <Laurent.Thery at sophia.inria.fr>
> Date: 1 October 2009 04:52:00 CDT
> To: smt-lib at cs.nyu.edu
> Subject: ocaml smtlib-parser
> I am trying to import smtlib files into the Coq theorem prover, for
> this I am using the smtlib parser 3.0
> written in ocaml at:
> Unfortunately, the function parse_benchmark that is provided has
> side-effects. It is then
> impossible to call it twice in a single program. Does anyone know an
> easy fix to this?
> Laurent Théry
> INRIA Sophia Antipolis, France
More information about the SMT-LIB