[SMT-LIB] Auto-discard notification

[Cesare Tinelli]

Laurent,

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  
support.ml.

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.

Thanks,


Cesare


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
>
>
>
> Hi,
>
> 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:
>
> http://goedel.cs.uiowa.edu/smtlib/
>
> 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?
>
> Regards,
>
> -- 
> Laurent Théry
> INRIA Sophia Antipolis, France
>
>