[SMT-LIB] Translators to SMT-LIB format

[Cesare Tinelli]

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