Skip to content

Commit 838cda0

Browse files
Update README
1 parent ccddb98 commit 838cda0

File tree

1 file changed

+6
-2
lines changed

1 file changed

+6
-2
lines changed

README.md

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,10 @@ features:
2424
[String](https://cvc5.github.io/docs-ci/docs-main/theories/strings.html)
2525
* Parametric sorts:
2626
[Sequences](https://cvc5.github.io/docs-ci/docs-main/theories/sequences.html)
27-
* Datatype sorts: Enumerations and Records (including self-recursive records)
27+
* Convenience wrappers around datatype sorts:
28+
* Enumerations
29+
* Records (including self-recursive records)
30+
* Optionals
2831
* Uninterpreted functions
2932
* Quantifiers
3033
* Boolean expressions: not, and, or, xor, implication
@@ -39,7 +42,8 @@ features:
3942
* Binary Real arithmetic: +, -, *, /
4043
* String operations: length, contains, prefix, suffix, concatenation
4144
* Sequence operations: length, contains, access, concatenation
42-
* Record operations: access
45+
* Record operations: access, check for null (for recursive records)
46+
* Optional operations: value, check for null
4347

4448
In addition this library provides a graph to build VCs with multiple
4549
paths; and generating VCs for all paths. FastWP and higher-level

0 commit comments

Comments
 (0)