Updated from cvc4 to cvc5

Closes: #9749

.github/actions/build-setup/action.yml

@@ -45,7 +45,7 @@ runs:
         # prepare move lang prover tooling.
         # By setting these values the dev-setup.sh script can detect already installed executables (and check versions).
         echo 'Z3_EXE='/opt/bin/z3 | tee -a $GITHUB_ENV
-        echo 'CVC4_EXE='/opt/bin/cvc4 | tee -a $GITHUB_ENV
+        echo 'CVC5_EXE='/opt/bin/cvc5 | tee -a $GITHUB_ENV
         echo 'DOTNET_ROOT='/opt/dotnet/ | tee -a $GITHUB_ENV
         echo 'BOOGIE_EXE='/opt/dotnet/tools/boogie | tee -a $GITHUB_ENV
         echo 'MVP_TEST_ON_CI'='1' | tee -a $GITHUB_ENV

.github/workflows/daily.yml

@@ -164,7 +164,7 @@ jobs:
           cd /opt/git/diem/
           set -o pipefail
           MVP_TEST_INCONSISTENCY=1 cargo test -p move-prover --release 2>&1 | tee -a $MESSAGE_PAYLOAD_FILE
-          MVP_TEST_FEATURE=cvc4 cargo test -p move-prover --release 2>&1 | tee -a $MESSAGE_PAYLOAD_FILE
+          MVP_TEST_FEATURE=cvc5 cargo test -p move-prover --release 2>&1 | tee -a $MESSAGE_PAYLOAD_FILE
       - uses: ./.github/actions/slack-file
         with:
           webhook: ${{ secrets.WEBHOOK_MOVE_PROVER }}

docker/ci/alpine/Dockerfile

@@ -18,7 +18,7 @@ RUN apk add bash=5.1.4-r0 --no-cache && \
 
 ENV DOTNET_ROOT "/opt/dotnet"
 ENV Z3_EXE "/opt/bin/z3"
-ENV CVC4_EXE "/opt/bin/cvc4"
+ENV CVC5_EXE "/opt/bin/cvc5"
 ENV BOOGIE_EXE "/opt/dotnet/tools/boogie"
 ENV PATH "/opt/cargo/bin:/usr/lib/golang/bin:/opt/bin:${DOTNET_ROOT}:${DOTNET_ROOT}/tools:$PATH"
 

docker/ci/arch/Dockerfile

@@ -24,7 +24,7 @@ RUN patched_glibc=glibc-linux4-2.33-4-x86_64.pkg.tar.zst && \
 
 ENV DOTNET_ROOT "/opt/dotnet"
 ENV Z3_EXE "/opt/bin/z3"
-ENV CVC4_EXE "/opt/bin/cvc4"
+ENV CVC5_EXE "/opt/bin/cvc5"
 ENV BOOGIE_EXE "/opt/dotnet/tools/boogie"
 ENV PATH "/opt/cargo/bin:/usr/lib/golang/bin:/opt/bin:${DOTNET_ROOT}:${DOTNET_ROOT}/tools:$PATH"
 

docker/ci/github/Dockerfile

@@ -20,7 +20,7 @@ RUN mkdir -p /github/home && \
 
 ENV DOTNET_ROOT "/opt/dotnet"
 ENV Z3_EXE "/opt/bin/z3"
-ENV CVC4_EXE "/opt/bin/cvc4"
+ENV CVC5_EXE "/opt/bin/cvc5"
 ENV BOOGIE_EXE "/opt/dotnet/tools/boogie"
 ENV PATH "/opt/cargo/bin:/usr/lib/golang/bin:/opt/bin:${DOTNET_ROOT}:${DOTNET_ROOT}/tools:$PATH"
 

language/move-prover/boogie-backend/src/boogie_wrapper.rs

@@ -163,13 +163,13 @@ impl<'env> BoogieWrapper<'env> {
         {
             return Err(anyhow!(
                 "The configured prover `{}` could not be found{}",
-                if self.options.use_cvc4 {
-                    &self.options.cvc4_exe
+                if self.options.use_cvc5 {
+                    &self.options.cvc5_exe
                 } else {
                     &self.options.z3_exe
                 },
-                if self.options.use_cvc4 {
-                    " (--use-cvc4 is set)"
+                if self.options.use_cvc5 {
+                    " (--use-cvc5 is set)"
                 } else {
                     ""
                 }

language/move-prover/boogie-backend/src/options.rs

@@ -20,7 +20,7 @@ const DEFAULT_BOOGIE_FLAGS: &[&str] = &[
 
 const MIN_BOOGIE_VERSION: &str = "2.9.0";
 const MIN_Z3_VERSION: &str = "4.8.9";
-const EXPECTED_CVC4_VERSION: &str = "aac53f51";
+const MIN_CVC5_VERSION: &str = "0.0.3";
 
 #[derive(Debug, Clone, Copy, Serialize, Deserialize)]
 pub enum VectorTheory {
@@ -50,10 +50,10 @@ pub struct BoogieOptions {
     pub use_exp_boogie: bool,
     /// Path to the z3 executable.
     pub z3_exe: String,
-    /// Whether to use cvc4.
-    pub use_cvc4: bool,
-    /// Path to the cvc4 executable.
-    pub cvc4_exe: String,
+    /// Whether to use cvc5.
+    pub use_cvc5: bool,
+    /// Path to the cvc5 executable.
+    pub cvc5_exe: String,
     /// Whether to generate debug trace code.
     pub debug_trace: bool,
     /// List of flags to pass on to boogie.
@@ -114,8 +114,8 @@ impl Default for BoogieOptions {
             boogie_exe: read_env_var("BOOGIE_EXE"),
             use_exp_boogie: false,
             z3_exe: read_env_var("Z3_EXE"),
-            use_cvc4: false,
-            cvc4_exe: read_env_var("CVC4_EXE"),
+            use_cvc5: false,
+            cvc5_exe: read_env_var("CVC5_EXE"),
             boogie_flags: vec![],
             debug_trace: false,
             use_array_theory: false,
@@ -169,10 +169,10 @@ impl BoogieOptions {
 
         let mut add = |sl: &[&str]| result.extend(sl.iter().map(|s| (*s).to_string()));
         add(DEFAULT_BOOGIE_FLAGS);
-        if self.use_cvc4 {
+        if self.use_cvc5 {
             add(&[
                 "-proverOpt:SOLVER=cvc5",
-                &format!("-proverOpt:PROVER_PATH={}", &self.cvc4_exe),
+                &format!("-proverOpt:PROVER_PATH={}", &self.cvc5_exe),
             ]);
         } else {
             add(&[&format!("-proverOpt:PROVER_PATH={}", &self.z3_exe)]);
@@ -252,26 +252,15 @@ impl BoogieOptions {
             )?;
             Self::check_version_is_greater("boogie", &version, MIN_BOOGIE_VERSION)?;
         }
-        if !self.z3_exe.is_empty() && !self.use_cvc4 {
+        if !self.z3_exe.is_empty() && !self.use_cvc5 {
             let version =
                 Self::get_version("z3", &self.z3_exe, &["--version"], r"version ([0-9.]*)")?;
             Self::check_version_is_greater("z3", &version, MIN_Z3_VERSION)?;
         }
-        if !self.cvc4_exe.is_empty() && self.use_cvc4 {
-            // Currently there is no metric version but a github hash we need to check
-            let version = Self::get_version(
-                "cvc4",
-                &self.cvc4_exe,
-                &["--version"],
-                r"git master ([0-9a-f]*)",
-            )?;
-            if version != EXPECTED_CVC4_VERSION {
-                return Err(anyhow!(
-                    "expected git hash {} but found {} for `cvc4`",
-                    EXPECTED_CVC4_VERSION,
-                    version
-                ));
-            }
+        if !self.cvc5_exe.is_empty() && self.use_cvc5 {
+            let version =
+                Self::get_version("cvc5", &self.cvc5_exe, &["--version"], r"version ([0-9.]*)")?;
+            Self::check_version_is_greater("cvc5", &version, MIN_CVC5_VERSION)?;
         }
         Ok(())
     }

language/move-prover/doc/dev/cvc4.md → language/move-prover/doc/dev/cvc5.md

@@ -1,46 +1,46 @@
-# CVC4 Integration
+# cvc5 Integration
 
-The [CVC4] integration is an experimental feature which is still evolving. This page documents,
-for tool developers, how to use CVC4 as a backend and extend the Move prover to use it right.
+The [cvc5] integration is an experimental feature which is still evolving. This page documents,
+for tool developers, how to use cvc5 as a backend and extend the Move prover to use it right.
 
-## Selecting CVC4
+## Selecting cvc5
 
 In the following we assume a command line for the move prover as in `mvp <arguments>`. See
 the [user documentation](../user/prover-guide.md) how to set this up. For development, it
 is recommended to use a `~/.mvprc` file for configuring the prover; the user documentation shows
 how. Specifically, this file can be used to point to the Move standard library and
 Diem framework as found in the local branch of the Diem repo.
 
-To choose CVC4 as a backend, call the prover as in:
+To choose cvc5 as a backend, call the prover as in:
 
 ```shell
-# mvp --use-cvc4 source.move
+# mvp --use-cvc5 source.move
 
 ```
 
-## Testing with CVC4
+## Testing with cvc5
 
 The provers testsuite supports multiple *feature groups* which constitute a particular
 set of tests which are run with a specific configuration. By default, when `cargo test`
 is executed in the prover crate, all groups are executed.
 
-There is one group called `cvc4` which contains the enabled tests for CVC4. This group
+There is one group called `cvc5` which contains the enabled tests for cvc5. This group
 is configured as follows at this point:
 
 - Only unit tests contained in `move-prover/tests` are included. Diem framework tests
   are skipped.
 - Those tests are only run locally and nightly, but not in CI.
-- By default, cvc4 tests share the same baseline (`.exp` file) with the `default` test group
+- By default, cvc5 tests share the same baseline (`.exp` file) with the `default` test group
   which uses [Z3].
-- Some cvc4 tests have their separate baseline, which is indicated by the
-  tag `// separate_baseline: cvc4` in the source. Those tests represent cases where
+- Some cvc5 tests have their separate baseline, which is indicated by the
+  tag `// separate_baseline: cvc5` in the source. Those tests represent cases where
   there is an issue (most of the time false positives); in some cases those are also legit
   differences resulting from different choices in the model.
 
 For the configuration logic, see the [testsuite.rs](../../tests/testsuite.rs) code.
 
 During development, it is often useful to focus on only running a specific test group.
-This is done using `MVP_TEST_FEATURE=cvc4 cargo test`. For documentation of all test parameters, see
+This is done using `MVP_TEST_FEATURE=cvc5 cargo test`. For documentation of all test parameters, see
 [here](../../tests/README.md).
 
 ## Obtaining the smtlib file
@@ -57,7 +57,7 @@ This will generate a file ending with `.smt` for each function in the Move sourc
 of those files is hermetic and contains all the settings which have been passed from upstream
 to the solver.
 
-## Specializing the Encoding for CVC4
+## Specializing the Encoding for cvc5
 
 There are multiple extension points which can be used to customize the prover. They are centered
 around the [Tera] template system which provides conditionals and macro expansion. Tera is
@@ -72,8 +72,8 @@ multisets, as well as implementations of native Move types found in
 ### Accessing Backend Options
 
 Inside of templates one has access to the backend options of the prover (`[backend]` section
-in the toml config). To test in a template whether CVC4 is selected as a backend, use `{{options.
-use_cvc4}}`. New options can be also added to `BoogieOptions` in Rust and will be accessible
+in the toml config). To test in a template whether cvc5 is selected as a backend, use `{{options.
+use_cvc5}}`. New options can be also added to `BoogieOptions` in Rust and will be accessible
 this way.
 
 ### Replacing Vector Theories
@@ -83,7 +83,7 @@ vector theories. There are multiple theories selectable via the option `--vector
 For a benchmark and description of the theories, see
 [here](../../lab/data/vector-theories/notebook.pdf).
 
-In order to add a new vector theory specific for CVC4, the following steps are needed:
+In order to add a new vector theory specific for cvc5, the following steps are needed:
 
 - Write the theory, starting e.g. from the
   [vector_array_theory](../../boogie-backend/src/prelude/vector-array-theory.bpl). A new theory
@@ -109,14 +109,14 @@ The Move prover comes with tool support and conventions to systematically perfor
 and other data-driven experiments. The crate which contains this support is found
 at [move-prover/lab](../../lab).
 
-> TODO: we should create a `lab/data/z3-cvc4` for a comparison test once the cvc4 integration
+> TODO: we should create a `lab/data/z3-cvc5` for a comparison test once the cvc5 integration
 > passes unit tests. The existing `lab/data/new-boogie` can be used as a starting point.
 
 For testing new vector theories, the existing [vector theory lab](../../lab/data/vector-theories)
 can be extended, or a new lab created from it.
 
 
 [Boogie]: https://github.com/boogie-org/boogie
-[CVC4]: https://cvc4.github.io/
+[cvc5]: https://cvc5.github.io/
 [Z3]: https://github.com/Z3Prover/z3
 [Tera]: https://tera.netlify.app/docs

language/move-prover/lab/data/cvc/README.md

@@ -2,7 +2,7 @@
 
 This lab is used to compare cvc5 and z3. The scope of the comparison is the full Diem framework.
 
-The configurations of the Move prover for cvc4/z3 are found in the `experiments/*.toml` files, which
+The configurations of the Move prover for cvc5/z3 are found in the `experiments/*.toml` files, which
 are in the standard format for Move prover options in files (see the user guide). Currently, only
 basic configurations, with the non-extensional, boogie-array based theory for vectors, are compared.
 

language/move-prover/lab/data/cvc/experiments/cvc_boogie_array.toml

@@ -1,3 +1,3 @@
 [backend]
-use_cvc4 = true
+use_cvc5 = true
 vector_theory = "BoogieArray"

language/move-prover/src/cli.rs

@@ -465,9 +465,9 @@ impl Options {
                      be non-deterministic, and may do other things to keep output stable.")
             )
             .arg(
-                Arg::with_name("use-cvc4")
-                    .long("use-cvc4")
-                    .help("uses cvc4 solver instead of z3")
+                Arg::with_name("use-cvc5")
+                    .long("use-cvc5")
+                    .help("uses cvc5 solver instead of z3")
             )
             .arg(
                 Arg::with_name("use-exp-boogie")
@@ -739,8 +739,8 @@ impl Options {
                 .unwrap()
                 .parse::<usize>()?;
         }
-        if matches.is_present("use-cvc4") {
-            options.backend.use_cvc4 = true;
+        if matches.is_present("use-cvc5") {
+            options.backend.use_cvc5 = true;
         }
         if matches.is_present("use-exp-boogie") {
             options.backend.use_exp_boogie = true;

language/move-prover/tests/README.md

@@ -64,7 +64,7 @@ Currently, the following features are available:
 - `default`: runs tests with all default flags.
 - `no_opaque`: runs tests in a special mode where the `opaque` pragma is ignored. This increases the load on the prover,
   and functions as a stress test.
-- `cvc4`: runs tests configured to use the CVC4/5 solver as a backend.
+- `cvc5`: runs tests configured to use the cvc5 solver as a backend.
 
 ## Conventions
 

language/move-prover/tests/sources/functional/choice.move

@@ -1,5 +1,5 @@
-// separate_baseline: cvc4
-// TODO(cvc4): this test requires a separate baseline because cvc4 produces false positives for some of choices
+// separate_baseline: cvc5
+// TODO(cvc5): this test requires a separate baseline because cvc5 produces false positives for some of choices
 // separate_baseline: simplify
 module 0x42::TestSome {
     use Std::Signer;