[SMT-LIB] Translators to SMT-LIB format

Cesare Tinelli tinelli at cs.uiowa.edu
Wed May 10 19:55:35 EDT 2006


Alessandro,

Clark Barrett wrote:
> A script that uses CVC Lite to translate from CVC format to SMT format is
> included in the "tools" section of the SMT-COMP web page:
> http://www.csl.sri.com/users/demoura/smt-comp/
> 
> -Clark
> 
> 
>> Dear all,
>>
>> what are the available translators to the SMT-LIB format?
>>
>> In particular, is there:
>>
>> - a translator from TPTP syntax to SMT-LIB or
 >>
There is no translator for this yet. But we hope to have one after the 
summer.

The main problem with this translation is not so much the syntax of TPTP 
but the fact that TPTP's logic is unsorted, so a completely automated 
translation is not possible. We are looking at semi-automatic approaches 
in which the user manually provides a sorted signature for the benchmarks.


Cesare


>> - a translator from CVC syntax to SMT-LIB ?
>>
>> Thanks in advance,
>>
>> alessandro
>>
>> -- 
>> Alessandro Armando		    e-mail: armando at dist.unige.it
>> Artificial Intelligence Laboratory  http://www.ai.dist.unige.it/armando
>> DIST - Universita' di Genova,       phone:  +39-0103532216
>> viale Causa 13,                     fax:    +39-0103532948
>> 16145 GENOVA, ITALY                 mobile: +39-3281003201
>> _______________________________________________
>> SMT-LIB mailing list
>> SMT-LIB at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>>
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib



More information about the SMT-LIB mailing list