DOMAINS :: SMT-LIB :: The use of ~

[QPQ]

Forums QPQ
DOMAINS :: SMT-LIB ::.. The use of ~

tinelli wrote at Feb 09, 2006 - 04:50 PM
---------------------------------------------------------------------
Hi Paulo,

The symbol ~ is unary minus, as described in the specification of the Int theory on the SMT-LIB site. It can be applied to any term of sort Int, not just numerals. The reason to use ~ as opposed to -, which is reserved for binary minus, is that overloading of function symbols is not allowed in the current version of the format. That choice was made to simplify parsing and type checking of SMT-LIB expressions.

The current plan is to allow overloading in the next version of the format, for greater flexibility expecially in future theories, like that of bit vectors which has a very large number of overloaded symbols. In that version, ~ will be replaced by -.

The new version will include a few minor changes and should go out in a few weeks.
We plan however to put the changes up for discussion on this forum first.


Cesare

PS: -1, would not be a legal identifier in the SMT-LIB format. That will remain the same in future versions.



[quote]Hi,

In benchmark : 
QF_IDL/sep/RailRoad_neg_0.smt

one can find (>= (- CVC_ZERO CVC_r_y) (~ 1)). Does (~ 1) mean -1? If not, what does it mean? If it means -1, why not (- 1) or -1? I have the wild guess that - is a binary operator and using it for negating a numeral would cause confusing. Still, if it is so, I think it can only be used in (~ n) where n is a numeral, right?

Cheers,

Paulo Matos
[/quote]
---------------------------------------------------------------------

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

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

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