mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Update SMT types docs
This commit is contained in:
parent
7b26c099b3
commit
7d9c080050
@ -448,19 +448,21 @@ The SMT encoding tries to be as precise as possible, mapping Solidity types
|
||||
and expressions to their closest `SMT-LIB <http://smtlib.cs.uiowa.edu/>`_
|
||||
representation, as shown in the table below.
|
||||
|
||||
+-----------------------+--------------+-----------------------------+
|
||||
|Solidity type |SMT sort |Theories (quantifier-free) |
|
||||
+=======================+==============+=============================+
|
||||
|Boolean |Bool |Bool |
|
||||
+-----------------------+--------------+-----------------------------+
|
||||
|intN, uintN, address, |Integer |LIA, NIA |
|
||||
|bytesN, enum | | |
|
||||
+-----------------------+--------------+-----------------------------+
|
||||
|array, mapping, bytes, |Array |Arrays |
|
||||
|string | | |
|
||||
+-----------------------+--------------+-----------------------------+
|
||||
|other types |Integer |LIA |
|
||||
+-----------------------+--------------+-----------------------------+
|
||||
+-----------------------+--------------------------------+-----------------------------+
|
||||
|Solidity type |SMT sort |Theories (quantifier-free) |
|
||||
+=======================+================================+=============================+
|
||||
|Boolean |Bool |Bool |
|
||||
+-----------------------+--------------------------------+-----------------------------+
|
||||
|intN, uintN, address, |Integer |LIA, NIA |
|
||||
|bytesN, enum | | |
|
||||
+-----------------------+--------------------------------+-----------------------------+
|
||||
|array, mapping, bytes, |Tuple |Datatypes, Arrays, LIA |
|
||||
|string |(Array elements, Integer length)| |
|
||||
+-----------------------+--------------------------------+-----------------------------+
|
||||
|struct |Tuple |Datatypes |
|
||||
+-----------------------+--------------------------------+-----------------------------+
|
||||
|other types |Integer |LIA |
|
||||
+-----------------------+--------------------------------+-----------------------------+
|
||||
|
||||
Types that are not yet supported are abstracted by a single 256-bit unsigned
|
||||
integer, where their unsupported operations are ignored.
|
||||
|
Loading…
Reference in New Issue
Block a user