Allow use of CVC5 through a binary

CHANGELOG.md

@@ -30,6 +30,15 @@ generated in the following situations:
 * New minor version release due to minor API changes and major
   command-line changes.
 
+* When using `--verify` you can now also specify a
+  [CVC5](https://github.com/cvc5/cvc5) executable using
+  `--use-cvc5-binary`. This allows you to use the `--verify` option on
+  platforms where there is no CVC5 PyPI package (i.e. Windows).
+
+* The [PyVCG](https://pypi.org/project/PyVCG) is now required on all
+  platforms. The optional dependency is now
+  [CVC5](https://pypi.org/project/cvc5) instead.
+
 * Remove the `--lint` option. Lint messages are now enabled by
   default, and `.trlc` files are processed as well. Instead there is a
   `--no-lint` option which turns off the extra warnings.

documentation/TUTORIAL-CI.md

@@ -43,8 +43,8 @@ The components of this regular expression are:
 
 The TRLC tools also come with a static analysis mode that performs
 additional checks. To enable this use `--verify`, and it requires the
-optional dependency [PyVCG](https://pypi.org/project/PyVCG/). It is
-strongly suggested to turn this on in CI.
+optional dependency [CVC5](https://pypi.org/project/cvc5/) (GNU/Linux
+only). It is strongly suggested to turn this on in CI.
 
 The TRLC tool goes beyond what the language definition requires and
 produces additional messages that may be helpful. For example it warns

documentation/TUTORIAL-INSTALL.md

@@ -10,15 +10,9 @@ The easiest way to install the tools is through PyPI:
 $ pip3 install --user trlc
 ```
 
-There are currently no required dependencies, all you need is a
-moderatly recent Python 3.9.
-
-If you are on Linux however, you may want to also install PyVCG as
-this enables some advanced features for getting better error messages.
-
-```
-$ pip3 install --user PyVCG
-```
+There are currently one required dependencies (PyVCG which should be
+installed automatically), all you need is a moderatly recent Python
+3.8 / 3.9 / 3.10 / 3.11.
 
 Don't forget to adjust your `PATH` so that `.local/bin` (or the
 equivalent on Windows) is on it; so that the `trlc` executable can be

documentation/TUTORIAL-LINT.md

@@ -5,20 +5,24 @@ This is part of the [TRLC Tutorial](TUTORIAL.md).
 ## Using the linter
 
 The TRLC tools come with a static analysis tool that can diagnose some
-potential issues with `.rsl` files before they are deployed and used.
+potential issues with `.rsl` files before they are deployed and
+used. This is enabled by default, but you can turn these off with the
+`--no-lint` option.
 
-To do this simply use the `--lint` feature:
+To enable more detailed checks you can also use the `--verify`
+feature, but please note that this is only available on Linux, and
+requires you to have installed the optional dependency
+[CVC5](https://pypi.org/project/cvc5).
 
 ```bash
-$ trlc --lint DIRECTORIES_OR_FILES
+$ trlc --verify DIRECTORIES_OR_FILES
 ```
-To enable more detailed checks you can also use the `--lint --verify`
-feature, but please note that this is only available on Linux and OSX,
-and requires you to have installed the optional dependency
-[PyVCG](https://pypi.org/project/PyVCG).
+
+If you are on Windows or Linux, you can also download the CVC5
+executables and ask TRLC to use them directly:
 
 ```bash
-$ trlc --lint --verify DIRECTORIES_OR_FILES
+$ trlc --verify --use-cvc5-binary=path/to/cvc5.exe DIRECTORIES_OR_FILES
 ```
 
 ## Sanity checks
@@ -50,7 +54,7 @@ contexts:
 * division by zero
 * array out of bounds
 
-The `--lint --verify` feature can also find cases where the check
+The `--verify` feature can also find cases where the check
 could be improved to guard against such as problem. For example:
 
 ```trlc
@@ -66,7 +70,7 @@ checks T {
 When running the verifier we can see:
 
 ```plain
-$ trlc.py --lint --verify trivial.rsl
+$ trlc.py --verify trivial.rsl
 x > 0, "please make this positive", x
 ^ trivial.rsl:8: warning: expression could be null [vcg-evaluation-of-null]
 | example record_type triggering error:
@@ -98,16 +102,16 @@ checks T {
 When running the verifier now we no longer get a complaint:
 
 ```plain
-$ trlc.py --lint --verify trivial.rsl
+$ trlc.py --verify trivial.rsl
 Verified 1 model(s) and 0 check(s) and found no issues
 ```
 
 ### Caveat
 
-Please keep in mind two limitations with the `--lint --verify`
+Please keep in mind two limitations with the `--verify`
 feature:
 
-* It currently does not work on Windows
+* It is harder to use and much slower on Windows
 * Under some circumstances the counter-examples generated are
   impossible to achieve, due to how the underlying technology (SMT
   Solvers) works. The current limitations are documented in the

requirements.txt

@@ -2,5 +2,4 @@ pycodestyle>=2.10
 pylint>=2.17
 coverage>=7.2
 sphinx>=7.0
-pyvcg==1.0.5
-cvc5==1.0.8
+pyvcg[api]==1.0.6

setup.py

@@ -33,8 +33,10 @@
 required_packages = []
 python_required = ">=3.8, <4"
 if "--plat-name" in sys.argv or "-p" in sys.argv:
-     required_packages.append("PyVCG==1.0.5")
+     required_packages.append("PyVCG[api]==1.0.6")
      python_required = ">=3.8, <3.12"
+else:
+    required_packages.append("PyVCG==1.0.6")
 
 setuptools.setup(
     name="trlc",

tests-system/Makefile

@@ -2,6 +2,7 @@ RAW_TARGETS=$(filter-out bulk, $(subst ./,,$(shell find . -mindepth 1 -maxdepth
 
 TARGETS=\
 	$(addsuffix /output, $(RAW_TARGETS)) \
+	$(addsuffix /output.smtlib, $(RAW_TARGETS)) \
 	$(addsuffix /output.brief, $(RAW_TARGETS)) \
 	$(addsuffix /output.json, $(RAW_TARGETS))
 
@@ -16,6 +17,13 @@ all: $(TARGETS) bulk/output bulk/output.brief bulk/output.json
 		../trlc.py --verify $(file < $(dir $@)options) \
 			$(dir $@) > $@
 
+%/output.smtlib:
+	-@coverage run -p --rcfile=../coverage.cfg --branch \
+		--data-file ../.coverage \
+		../trlc.py --verify --use-cvc5-binary=cvc5 \
+			$(file < $(dir $@)options) \
+			$(dir $@) > $@
+
 %/output.brief:
 	-@coverage run -p --rcfile=../coverage.cfg --branch \
 		--data-file ../.coverage \

tests-system/array-length/output.smtlib

@@ -0,0 +1,5 @@
+values = ["one", "two", "three"]
+                        ^^^^^^^ array-length/foo.trlc:4: error: this array requires at most 2 elements (3 provided)
+values = ["one"]
+               ^ array-length/foo.trlc:8: error: this array requires at least 2 elements (only 1 provided)
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 error(s)

tests-system/array-membership-1/output.smtlib

@@ -0,0 +1,13 @@
+arr    = [40, 41, 42, 43, 44, 45]
+         ^ array-membership-1/foo.trlc:10: check warning: 42 is not in array
+arr    = [40, 41, 42, 43, 44, 45]
+         ^ array-membership-1/foo.trlc:10: check warning: 42 is in array
+arr    = [1, 2, 3]
+         ^ array-membership-1/foo.trlc:22: check warning: 42 is not in array
+arr    = [1, 2, 3]
+         ^ array-membership-1/foo.trlc:22: check warning: 42 is in array
+arr    = []
+         ^ array-membership-1/foo.trlc:34: check warning: 42 is not in array
+arr    = []
+         ^ array-membership-1/foo.trlc:34: check warning: 42 is in array
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 6 warning(s)

tests-system/array-membership-2/output.smtlib

@@ -0,0 +1,3 @@
+ival in arr, warning "potato"
+^^^^ array-membership-2/foo.rsl:9: error: expected expression of type Builtin_String, got Builtin_Integer instead
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/array-membership-3/output.smtlib

@@ -0,0 +1,3 @@
+kitten in arr, warning "does not reference kitten"
+^^^^^^ array-membership-3/foo.rsl:10: error: unknown symbol kitten
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/arrays-1/output.smtlib

@@ -0,0 +1,3 @@
+arr = [1, 2, 3]
+      ^ arrays-1/example.trlc:8: check error: potato
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s)

tests-system/arrays-2/output.smtlib

@@ -0,0 +1,3 @@
+arr[0] == len(arr), "potato", arr
+^^^ arrays-2/example.rsl:8: error: expression 'arr' has type Integer, which is not an array
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/base-types/output.smtlib

@@ -0,0 +1,5 @@
+checks MyType {
+       ^^^^^^ base-types/checks.check:4: issue: move this check block into bar.rsl:1 [deprecated_feature]
+int_nok = 24
+          ^^ base-types/instances.trlc:10: check error: int must be 42
+Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s)

tests-system/bazel-dirs/output.smtlib

@@ -0,0 +1 @@
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found no issues

tests-system/builtin-1/output.smtlib

@@ -0,0 +1,3 @@
+len = 2
+      ^ builtin-1/example.trlc:10: check warning: potato
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s)

tests-system/builtin-2/output.smtlib

@@ -0,0 +1,3 @@
+len == trlc:len(str), warning "potato", len
+       ^^^^^^^^ builtin-2/legacy.rsl:9: issue: please use function len instead [deprecated_feature]
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s)

tests-system/check-wo-type/output.smtlib

@@ -0,0 +1,3 @@
+checks {
+       ^ check-wo-type/checks.check:3: error: expected identifier, encountered opening brace '{' instead
+Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 error(s)

tests-system/checks-1/output.smtlib

@@ -0,0 +1,14 @@
+checks T {
+       ^ checks-1/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature]
+a < b, "a must be less than b"
+    ^ checks-1/foo.check:4: issue: expression could be null [vcg-evaluation-of-null]
+    | example record_type triggering error:
+    |   T bad_potato {
+    |     a = 0
+    |     /* b is null */
+    |   }
+T Test_1 {
+  ^^^^^^ checks-1/foo.trlc:3: error: rhs of check a < b (foo.check:4) must not be null
+T Test_2 {
+  ^^^^^^ checks-1/foo.trlc:7: check error: a must be less than b
+Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 2 warning(s) and 2 error(s)

tests-system/checks-2/output.smtlib

@@ -0,0 +1,7 @@
+checks T {
+       ^ checks-2/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature]
+T Test_1 {
+  ^^^^^^ checks-2/foo.trlc:3: check error: please define b
+a = 5
+    ^ checks-2/foo.trlc:8: check error: a must be less than b
+Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 2 error(s)

tests-system/checks-3/output.smtlib

@@ -0,0 +1,5 @@
+checks T {
+       ^ checks-3/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature]
+a = 5
+    ^ checks-3/foo.trlc:8: check error: a must be less than b
+Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s)

tests-system/checks-4/output.smtlib

@@ -0,0 +1,14 @@
+checks T {
+       ^ checks-4/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature]
+(forall v in values => v != foo), "value cannot be same as value of foo", values
+             ^^^^^^ checks-4/foo.check:4: issue: expression could be null [vcg-evaluation-of-null]
+                  | example record_type triggering error:
+                  |   T bad_potato {
+                  |     /* foo is null */
+                  |     /* values is null */
+                  |   }
+T Test_1 {
+  ^^^^^^ checks-4/foo.trlc:3: error: values in quantified expression (forall v in values => v != foo) (foo.check:4) must not be null
+values = ["x", "kitten", "z"]
+         ^ checks-4/foo.trlc:9: check error: value cannot be same as value of foo
+Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 2 warning(s) and 2 error(s)

tests-system/checks-5/output.smtlib

@@ -0,0 +1,6 @@
+Requirement Potato {
+            ^^^^^^ checks-5/foo.trlc:3: check error: linkage incorrect
+                 | You must either link this requirement to other requirements
+                 | using the derived_from attribute, or you need to set
+                 | top_level to true.
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s)

tests-system/checks-6/output.smtlib

@@ -0,0 +1,5 @@
+true, """this
+      ^^^^^^^ checks-6/foo.rsl:6: error: error message must not contain a newline
+true, """this
+^^^^ checks-6/foo.rsl:6: issue: expression is always true [vcg-always-true]
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s) and 1 error(s)

tests-system/combined-rsl-file-1/output.smtlib

@@ -0,0 +1,3 @@
+T foo {
+  ^^^ combined-rsl-file-1/example.trlc:3: check error: potato
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s)

tests-system/combined-rsl-file-2/output.smtlib

@@ -0,0 +1,2 @@
+package Example
+        ^^^^^^^ combined-rsl-file-2/b.rsl:1: error: duplicate definition, previous definition at a.rsl:1

tests-system/comments-1/output.smtlib

@@ -0,0 +1 @@
+Processed 0 model(s), 0 check(s) and 1 requirement file(s) and found no issues

tests-system/comments-2/output.smtlib

@@ -0,0 +1 @@
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found no issues

tests-system/cross-refs-in-errors/output.smtlib

@@ -0,0 +1,2 @@
+package Foo
+        ^^^ cross-refs-in-errors/potato/foo.rsl:1: error: duplicate definition, previous definition at kitten/bar.rsl:1

tests-system/cyclic-inheritance/output.smtlib

@@ -0,0 +1,5 @@
+type MyType2 extends MyType3 {
+                     ^^^^^^^ cyclic-inheritance/bar.rsl:5: error: unknown symbol MyType3
+type MyType3 extends MyType2 {
+                     ^^^^^^^ cyclic-inheritance/bar.rsl:9: error: unknown symbol MyType2
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 2 error(s)

tests-system/cyclic-packages/output.smtlib

@@ -0,0 +1,5 @@
+> Bar depends on Baz
+> Baz depends on Bork
+> Bork depends on Bar
+cyclic-packages/bar.rsl: error: circular inheritence
+Processed 4 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/decimal-1/output.smtlib

@@ -0,0 +1,7 @@
+D = 5.0
+    ^^^ decimal-1/foo.trlc:9: check warning: D is not less that I
+D = -5.0
+    ^ decimal-1/foo.trlc:14: check warning: D is not less that I
+D = -5.0
+    ^ decimal-1/foo.trlc:14: check warning: D is not positive
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s)

tests-system/decimal-2/output.smtlib

@@ -0,0 +1,3 @@
+D in 0 .. 10, warning "potato", D
+     ^ decimal-2/foo.rsl:8: error: expected expression of type Decimal, got Integer instead
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/decimal-3/output.smtlib

@@ -0,0 +1,3 @@
+D in 0.0 .. 10, warning "potato", D
+            ^^ decimal-3/foo.rsl:8: error: expected expression of type Decimal, got Integer instead
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/decimal-4/output.smtlib

@@ -0,0 +1 @@
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found no issues

tests-system/decimal-5/output.smtlib

@@ -0,0 +1 @@
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found no issues

tests-system/decimal-6/output.smtlib

@@ -0,0 +1,3 @@
+0.0 + D + D + D == 3.0 * D, warning "rounding error", D
+                ^^ decimal-6/foo.rsl:8: issue: expression is always true [vcg-always-true]
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s)

tests-system/decimal-7/output.smtlib

@@ -0,0 +1,3 @@
+D ** 2 >= 0.0, warning "potato", D
+       ^^ decimal-7/foo.rsl:8: issue: expression is always true [vcg-always-true]
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s)

tests-system/decimal-8/output.smtlib

@@ -0,0 +1,3 @@
+D == I, warning "not equal", D
+  ^^ decimal-8/foo.rsl:9: error: type mismatch: Decimal and Integer do not match
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/delayed-references-1/output.smtlib

@@ -0,0 +1 @@
+Processed 1 model(s), 0 check(s) and 2 requirement file(s) and found no issues

tests-system/derived-type-ref/output.smtlib

@@ -0,0 +1 @@
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found no issues

tests-system/duplicate-imports/output.smtlib

@@ -0,0 +1,3 @@
+import Foo
+       ^^^ duplicate-imports/bar.trlc:4: warning: duplicate import of package Foo
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s)

tests-system/duplicate-late-packages/output.smtlib

@@ -0,0 +1,3 @@
+package Foo
+        ^^^ duplicate-late-packages/foo.trlc:1: warning: duplicate late declaration of package Foo, previous declaration in bar.trlc:1; consider adding an rsl file declaring the package
+Processed 0 model(s), 0 check(s) and 3 requirement file(s) and found 1 warning(s)

tests-system/empty-attributes/output.smtlib

@@ -0,0 +1,5 @@
+checks BaseRequirement {
+       ^^^^^^^^^^^^^^^ empty-attributes/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature]
+bar.BaseRequirement SomeThing {
+                    ^^^^^^^^^ empty-attributes/instances.trlc:4: check error: Asil must be set
+Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s)

tests-system/empty-files/output.smtlib

@@ -0,0 +1,2 @@
+empty-files/foo.trlc:1:1: error: expected keyword package, encountered end-of-file instead
+Processed 0 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s)

tests-system/enum-null/output.smtlib

@@ -0,0 +1,5 @@
+checks MyType {
+       ^^^^^^ enum-null/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature]
+bar.MyType SomeThing {
+           ^^^^^^^^^ enum-null/instances.trlc:4: check error: Status must be not null
+Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s)

tests-system/enum-ok/output.smtlib

@@ -0,0 +1,3 @@
+checks MyType {
+       ^^^^^^ enum-ok/checks.check:4: issue: move this check block into bar.rsl:1 [deprecated_feature]
+Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s)

tests-system/enum/output.smtlib

@@ -0,0 +1,7 @@
+checks MyType {
+       ^^^^^^ enum/checks.check:2: issue: move this check block into bar.rsl:1 [deprecated_feature]
+status != null , "Internal error when evaluating enum value"
+       ^^ enum/checks.check:4: issue: expression is always true [vcg-always-true]
+bar.MyType SomeThing {
+           ^^^^^^^^^ enum/instances.trlc:4: check error: Status must be NEW
+Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 2 warning(s) and 1 error(s)

tests-system/error-in-check/output.smtlib

@@ -0,0 +1,3 @@
+startsXwith(name, "Q"), error "name must start with Q", name
+^^^^^^^^^^^ error-in-check/checks.check:4: error: unknown symbol startsXwith, did you mean startswith?
+Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 error(s)