@@ -1741,8 +1741,33 @@ \subsubsection{Other Theories}
1741
1741
In this section, we mention theories that are of interest to synthesis applications
1742
1742
that are not included in the SMT-LIB standard.
1743
1743
1744
- \paragraph {Tables }
1745
- TODO
1744
+ \paragraph {Bags and Tables }
1745
+ An SMT-LIB compliant theory of tables is proposed in~\cite {theoryOfTables }.
1746
+ We give the salient details of this theory here.
1747
+
1748
+ The theory of tables is implemented as an extension of a theory of bags (multisets).
1749
+ The signature of this theory includes all sorts of the form
1750
+ $ \texttt {(Bag\ T)}$
1751
+ for all sorts $ \texttt {T}$ .
1752
+ This sort denotes bags (i.e. multisets) of elements of sort $ \texttt {T}$ .
1753
+ The theory of bags includes a multitude of operators for e.g.
1754
+ taking unions, intersections and differences of bags,
1755
+ as well as higher-order operators like
1756
+ $ \texttt {map}$ , $ \texttt {fold}$ and $ \texttt {partition}$ .
1757
+ A \emph {table } is a bag whose element sort $ T$ is a tuple,
1758
+ where a tuple is a parametric sort taking $ n$ types corresponding to the
1759
+ types of the elements that comprise the tuple.
1760
+ For example, $ \texttt {(Tuple\ Int\ Int)}$ denotes tuples
1761
+ of arity two.
1762
+ The sort $ \texttt {(Table\ Int\ Int)}$ is syntax sugar for
1763
+ $ \texttt {(Bag\ (Tuple\ Int\ Int))}$ and is used to denote tables with two integer
1764
+ columns.
1765
+ A table value is a multiset union of tuple values.
1766
+ The number of rows in a table value is equal to its cardinality.
1767
+ Notice that ordering of rows is not semantically captured,
1768
+ and thus not modelled in this theory.
1769
+ For further details on the complete signature and semantics of this
1770
+ theory is available in~\cite {theoryOfTables }.
1746
1771
1747
1772
\subsection {Features and Feature Sets }
1748
1773
\label {ssec:feature-sets }
0 commit comments