Rename occurrences of CVC4 to CVC5. (#6351)

This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.

3 files changed, 31 insertions, 31 deletions

diff --git a/test/regress/README.md b/test/regress/README.md
index 0dc1d4eb8..f7fb2b6d3 100644
--- a/test/regress/README.md
+++ b/test/regress/README.md
@@ -2,13 +2,13 @@
 
 ## Regression Levels and Running Regression Tests
 
-CVC4's regression tests are divided into 5 levels (level 0 to 4). Higher
+cvc5's regression tests are divided into 5 levels (level 0 to 4). Higher
 regression levels are reserved for longer running regressions. 
 
 For running regressions tests, 
 see the [INSTALL](https://github.com/CVC4/CVC4/blob/master/INSTALL.md#testing-cvc4) file.
 
-By default, each invocation of CVC4 is done with a 10 minute timeout. To use a
+By default, each invocation of cvc5 is done with a 10 minute timeout. To use a
 different timeout, set the `TEST_TIMEOUT` environment variable:
 
 ```
@@ -36,7 +36,7 @@ The following types of regression files are supported:
 
 - `*.smt`: An [SMT1.x](http://smtlib.cs.uiowa.edu/papers/format-v1.2-r06.08.30.pdf) benchmark
 - `*.smt2`: An [SMT 2.x](http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf) benchmark
-- `*.cvc`: A benchmark that uses [CVC4's native input language](https://github.com/CVC4/CVC4/wiki/CVC4-Native-Input-Language)
+- `*.cvc`: A benchmark that uses [cvc5's native input language](https://github.com/CVC4/CVC4/wiki/CVC4-Native-Input-Language)
 - `*.sy`: A [SyGuS](http://sygus.seas.upenn.edu/files/SyGuS-IF.pdf) benchmark
 - `*.p`: A [TPTP](http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html) benchmark
 
@@ -51,7 +51,7 @@ with the following directives:
 % EXIT: 0
 ```
 
-This example expects an exit status of 0 from CVC4, the single line "stderr" on
+This example expects an exit status of 0 from cvc5, the single line "stderr" on
 stderr, and the single line "stdout" on stdout. You can repeat `EXPECT` and
 `EXPECT-ERROR` lines as many times as you like, and at different points of the
 file.  This is useful for multiple queries:
@@ -61,7 +61,7 @@ file.  This is useful for multiple queries:
 QUERY FALSE;
 % EXPECT: VALID
 QUERY TRUE;
-% EXPECT-ERROR: CVC4 Error:
+% EXPECT-ERROR: cvc5 Error:
 % EXPECT-ERROR: Parse Error: regress.cvc:7.13: Unexpected token: 'error'.
 syntax error;
 % EXIT: 1
@@ -71,7 +71,7 @@ Note that the directives are in comments, so if the benchmark file is an smt2
 file for example, the first character would be `;` instead of `%`.
 
 Benchmark files can also specify the command line options to be used when
-executing CVC4, for example:
+executing cvc5, for example:
 
 ```
 % COMMAND-LINE: --incremental
@@ -98,7 +98,7 @@ string `TERM` to make the regression test robust to the actual term printed
 (e.g. there could be multiple non-linear facts and it is ok if any of them is
 printed).
 
-Sometimes, certain benchmarks only apply to certain CVC4
+Sometimes, certain benchmarks only apply to certain cvc5
 configurations. The `REQUIRES` directive can be used to only run
 a given benchmark when a feature is supported. For example:
 
@@ -108,6 +108,6 @@ a given benchmark when a feature is supported. For example:
 
 This benchmark is only run when symfpu has been configured.  Multiple
 `REQUIRES` directives are supported. For a list of features that can be listed
-as a requirement, refer to CVC4's `--show-config` output. Features can also be
+as a requirement, refer to cvc5's `--show-config` output. Features can also be
 excluded by adding the `no-` prefix, e.g. `no-symfpu` means that the test is
 not valid for builds that include symfpu support.
diff --git a/test/regress/regress0/sygus/no-logic.sy b/test/regress/regress0/sygus/no-logic.sy
index 8c9794986..fd63506d2 100644
--- a/test/regress/regress0/sygus/no-logic.sy
+++ b/test/regress/regress0/sygus/no-logic.sy
@@ -1,7 +1,7 @@
 ; REQUIRES: no-competition
 ; COMMAND-LINE: --sygus-out=status --lang=sygus2
 ; EXPECT-ERROR: no-logic.sy:8.10: No set-logic command was given before this point.
-; EXPECT-ERROR: no-logic.sy:8.10: CVC4 will make all theories available.
+; EXPECT-ERROR: no-logic.sy:8.10: cvc5 will make all theories available.
 ; EXPECT-ERROR: no-logic.sy:8.10: Consider setting a stricter logic for (likely) better performance.
 ; EXPECT-ERROR: no-logic.sy:8.10: To suppress this warning in the future use (set-logic ALL).
 ; EXPECT: unsat
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 58e43df36..5ff9628f0 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -103,10 +103,10 @@ def run_process(args, cwd, timeout, s_input=None):
     return out, err, exit_status
 
 
-def get_cvc4_features(cvc4_binary):
-    """Returns a list of features supported by the CVC4 binary `cvc4_binary`."""
+def get_cvc5_features(cvc5_binary):
+    """Returns a list of features supported by the cvc5 binary `cvc5_binary`."""
 
-    output, _, _ = run_process([cvc4_binary, '--show-config'], None, None)
+    output, _, _ = run_process([cvc5_binary, '--show-config'], None, None)
     if isinstance(output, bytes):
         output = output.decode()
 
@@ -124,17 +124,17 @@ def get_cvc4_features(cvc4_binary):
     return features, disabled_features
 
 
-def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc4_binary,
+def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc5_binary,
                   command_line, benchmark_dir, benchmark_filename, timeout):
-    """Runs CVC4 on the file `benchmark_filename` in the directory
-    `benchmark_dir` using the binary `cvc4_binary` with the command line
+    """Runs cvc5 on the file `benchmark_filename` in the directory
+    `benchmark_dir` using the binary `cvc5_binary` with the command line
     options `command_line`. The output is scrubbed using `scrubber` and
     `error_scrubber` for stdout and stderr, respectively. If dump is true, the
-    function first uses CVC4 to read in and dump the benchmark file and then
+    function first uses cvc5 to read in and dump the benchmark file and then
     uses that as input."""
 
     bin_args = wrapper[:]
-    bin_args.append(cvc4_binary)
+    bin_args.append(cvc5_binary)
 
     output = None
     error = None
@@ -173,22 +173,22 @@ def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc4_binary,
 
 
 def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code,
-                   skip_timeout, wrapper, cvc4_binary, benchmark_path,
+                   skip_timeout, wrapper, cvc5_binary, benchmark_path,
                    timeout):
-    """Determines the expected output for a benchmark, runs CVC4 on it and then
+    """Determines the expected output for a benchmark, runs cvc5 on it and then
     checks whether the output corresponds to the expected output. Optionally
     uses a wrapper `wrapper`, tests unsat cores (if check_unsat_cores is true),
     checks proofs (if check_proofs is true), or dumps a benchmark and uses that as
     the input (if dump is true). `use_skip_return_code` enables/disables
     returning 77 when a test is skipped."""
 
-    if not os.access(cvc4_binary, os.X_OK):
+    if not os.access(cvc5_binary, os.X_OK):
         sys.exit(
-            '"{}" does not exist or is not executable'.format(cvc4_binary))
+            '"{}" does not exist or is not executable'.format(cvc5_binary))
     if not os.path.isfile(benchmark_path):
         sys.exit('"{}" does not exist or is not a file'.format(benchmark_path))
 
-    cvc4_features, cvc4_disabled_features = get_cvc4_features(cvc4_binary)
+    cvc5_features, cvc5_disabled_features = get_cvc5_features(cvc5_binary)
 
     basic_command_line_args = []
 
@@ -287,18 +287,18 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code,
         if req_feature.startswith("no-"):
             req_feature = req_feature[len("no-"):]
             is_negative = True
-        if req_feature not in (cvc4_features + cvc4_disabled_features):
+        if req_feature not in (cvc5_features + cvc5_disabled_features):
             print(
                 'Illegal requirement in regression: {}\nAllowed requirements: {}'
                 .format(req_feature,
-                        ' '.join(cvc4_features + cvc4_disabled_features)))
+                        ' '.join(cvc5_features + cvc5_disabled_features)))
             return EXIT_FAILURE
         if is_negative:
-            if req_feature in cvc4_features:
+            if req_feature in cvc5_features:
                 print('1..0 # Skipped regression: not valid with {}'.format(
                     req_feature))
                 return (EXIT_SKIP if use_skip_return_code else EXIT_OK)
-        elif req_feature not in cvc4_features:
+        elif req_feature not in cvc5_features:
             print('1..0 # Skipped regression: {} not supported'.format(
                 req_feature))
             return (EXIT_SKIP if use_skip_return_code else EXIT_OK)
@@ -360,14 +360,14 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code,
         for extra_arg in extra_command_line_args:
             command_line_args_configs.append(all_args + [extra_arg])
 
-    # Run CVC4 on the benchmark with the different option sets and check
+    # Run cvc5 on the benchmark with the different option sets and check
     # whether the exit status, stdout output, stderr output are as expected.
     print('1..{}'.format(len(command_line_args_configs)))
     print('# Starting')
     exit_code = EXIT_OK
     for command_line_args in command_line_args_configs:
         output, error, exit_status = run_benchmark(dump, wrapper, scrubber,
-                                                   error_scrubber, cvc4_binary,
+                                                   error_scrubber, cvc5_binary,
                                                    command_line_args,
                                                    benchmark_dir,
                                                    benchmark_basename, timeout)
@@ -444,7 +444,7 @@ def main():
     parser.add_argument('--no-check-proofs', dest='check_proofs',
                         action='store_false')
     parser.add_argument('wrapper', nargs='*')
-    parser.add_argument('cvc4_binary')
+    parser.add_argument('cvc5_binary')
     parser.add_argument('benchmark')
 
     argv = sys.argv[1:]
@@ -454,7 +454,7 @@ def main():
 
     args = parser.parse_args(argv)
 
-    cvc4_binary = os.path.abspath(args.cvc4_binary)
+    cvc5_binary = os.path.abspath(args.cvc5_binary)
 
     wrapper = args.wrapper
     if os.environ.get('VALGRIND') == '1' and not wrapper:
@@ -464,7 +464,7 @@ def main():
 
     return run_regression(args.check_unsat_cores, args.check_proofs, args.dump,
                           args.use_skip_return_code, args.skip_timeout,
-                          wrapper, cvc4_binary, args.benchmark, timeout)
+                          wrapper, cvc5_binary, args.benchmark, timeout)
 
 
 if __name__ == "__main__":