DOMAINS :: SMT-LIB :: ANY in extrasorts

[QPQ]

Forums QPQ
DOMAINS :: SMT-LIB ::.. ANY in extrasorts

pocm wrote at Mar 08, 2006 - 11:23 PM
---------------------------------------------------------------------
[quote]From Leonardo:

> Clark,
> 
> My SMT-LIB account is not working, and I couldn't answer his email.
> The SAL2CVC translator maps all uninterpreted types in SAL to the
> ANY type. The translator always defines this type, even when it is not
> required.
> Anyway, I agree with you, we should remove it from the SMT-LIB
> benchmarks.
> 
> Leonardo.
[/quote]

Ok, thanks for the reply and the forwarding of Leonardo's comment.

Another thing for this years. Since we already have multiple argument operators like and, or, iff, and xor, why not allow + to be a multiple argument operator and disallow the use of -. This way (- x y) would become (+ x (* (~ 1) y)) and (+ (+ (+ x y) z) w) would simply be (+ x y z w). Unless there's a theoretical objection this extension seems both logical and more readable (I know benchmark readability is not a priority, but helps).

Paulo Matos
---------------------------------------------------------------------

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

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

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