DOMAINS :: SMT-LIB :: let-terms in SMT-LIB

[QPQ]

Forums QPQ
DOMAINS :: SMT-LIB ::.. let-terms in SMT-LIB

tinelli wrote at Apr 14, 2005 - 01:00 AM
---------------------------------------------------------------------
[quote]SMT-LIB has two let-constructs for formulas, but none for constructing terms. (We cannot write 'let x=1 in x'.) Can someone briefly explain the reason for this design choice?

Thanks,

Sava
[/quote]

The reason was simply economy. 
The let construct for terms did not seem necessary, and neither Silvio nor 
I were aware of any SMT benchmarks that actually used one.

But we are certainly open to motivated requests to add it. 
(For instance, we did that in the past for the ite construct for terms, 
which was not present in the original proposal of the format.)


Cesare



 
---------------------------------------------------------------------

Reply to this message:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=reply&topic=162&forum=46

Browse thread:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=viewtopic&topic=162

You are receiving this Email because you are subscribed to be notified of events in forums at: http://www.qpq.org/