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

[QPQ]

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

pocm wrote at Feb 06, 2006 - 05:29 PM
---------------------------------------------------------------------
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

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

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/