Updates to the theory of tables #28
Conversation
|
PDF compilation was successful. |
|
PDF compilation was successful. |
|
PDF compilation was successful. |
|
PDF compilation was successful. |
|
PDF compilation was successful. |
|
PDF compilation was successful. |
| is the bag containing exactly | ||
| the elements $\syntax{(f\ u)}$ | ||
| for each $\syntax{u}$ that occurs in $\syntax{t}$. | ||
| The multiplicity of $\syntax{(f\ u)}$ | ||
| in $\syntax{(map\ f\ t)}$ | ||
| in $\syntax{(bag.map\ f\ t)}$ |
There was a problem hiding this comment.
The multiplicity here is at least, not the the same
|
PDF compilation was successful. |
Co-authored-by: mudathirmahgoub <[email protected]>
|
PDF compilation was successful. |
| @@ -309,17 +349,17 @@ \subsubsection{Bag Count} | |||
| \begin{itemize} | |||
| \item | |||
| We do not include an explicit membership predicate for bags, although note that | |||
| the formula $\syntax{(>\ (count\ u\ t)\ 0)}$ holds exactly when $\syntax{u}$ | |||
| the formula $\syntax{(>\ (bag.count\ u\ t)\ 0)}$ holds exactly when $\syntax{u}$ | |||
There was a problem hiding this comment.
cvc5 now reads (bag.member u t) as a syntax sugar for (> (bag.count u t) 0)
There was a problem hiding this comment.
We can add this and other syntax sugar later.
Co-authored-by: mudathirmahgoub <[email protected]>
|
PDF compilation was successful. |
|
This line mentions 3 function symbols denoting table operations, but we have 5 operations mentioned in the document (bag.union_max, bag.union_disjoint, bag.intersect_min , bag.difference_subtract , bag.difference_remove). cvc5 supports additional 3 (bag.duplicate_removal, bag.subbag, bag.member). |
tableTheory/tableTheory.tex
Outdated
| $\syntax{intersect\_min}$, $\syntax{difference\_subtract}$ and | ||
| $\syntax{difference\_remove}$. | ||
| $\syntax{bag.union\_max}$, $\syntax{bag.union\_disjoint}$, | ||
| $\syntax{bag.intersect\_min}$, $\syntax{bag.difference\_subtract}$ and |
There was a problem hiding this comment.
This is unfortunate, but in cvc5, we have bag.inter_min, not bag.intersect_min.
There was a problem hiding this comment.
Not a big deal, we can change this now.
|
Type in line |
Co-authored-by: mudathirmahgoub <[email protected]>
|
PDF compilation was successful. |
Adds support for symbolic indices to all indexed operators.
Changes some tokens.
Adds the beginning of the discussion of abstract sorts.
Adds 2 simple examples.