diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-15 13:04:55 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-15 20:04:55 +0000 |
commit | 77bca094a140b35341257f125a55212ff0108250 (patch) | |
tree | 1d3369b9be5fc4c3e8cb279ae5ea662e59cbcb3e /test | |
parent | 63647b1d79df6f287ea6599958b16fce44b8271d (diff) |
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.
Diffstat (limited to 'test')
-rw-r--r-- | test/api/interactive_shell.py | 14 | ||||
-rw-r--r-- | test/api/ouroborous.cpp | 10 | ||||
-rw-r--r-- | test/api/sep_log_api.cpp | 4 | ||||
-rw-r--r-- | test/regress/README.md | 16 | ||||
-rw-r--r-- | test/regress/regress0/sygus/no-logic.sy | 2 | ||||
-rwxr-xr-x | test/regress/run_regression.py | 44 | ||||
-rw-r--r-- | test/unit/api/datatype_api_black.cpp | 16 | ||||
-rw-r--r-- | test/unit/api/grammar_black.cpp | 36 | ||||
-rw-r--r-- | test/unit/api/op_black.cpp | 12 | ||||
-rw-r--r-- | test/unit/api/op_white.cpp | 2 | ||||
-rw-r--r-- | test/unit/api/solver_black.cpp | 662 | ||||
-rw-r--r-- | test/unit/api/sort_black.cpp | 58 | ||||
-rw-r--r-- | test/unit/api/term_black.cpp | 496 | ||||
-rw-r--r-- | test/unit/main/interactive_shell_black.cpp | 2 | ||||
-rw-r--r-- | test/unit/node/node_black.cpp | 2 | ||||
-rw-r--r-- | test/unit/parser/parser_black.cpp | 2 | ||||
-rw-r--r-- | test/unit/parser/parser_builder_black.cpp | 12 | ||||
-rw-r--r-- | test/unit/theory/theory_sets_type_rules_white.cpp | 2 | ||||
-rw-r--r-- | test/unit/util/boolean_simplification_black.cpp | 2 | ||||
-rw-r--r-- | test/unit/util/output_black.cpp | 10 |
20 files changed, 702 insertions, 702 deletions
diff --git a/test/api/interactive_shell.py b/test/api/interactive_shell.py index 6660ebe2e..3c8a1d5a8 100644 --- a/test/api/interactive_shell.py +++ b/test/api/interactive_shell.py @@ -11,7 +11,7 @@ # directory for licensing information. # ############################################################################# # -# A simple test file to interact with CVC4 with line editing +# A simple test file to interact with cvc5 with line editing ## import sys @@ -19,15 +19,15 @@ import pexpect def check_iteractive_shell(): """ - Interacts with CVC4's interactive shell and checks that things such a tab + Interacts with cvc5's interactive shell and checks that things such a tab completion and "pressing up" works. """ - # Open CVC4 + # Open cvc5 child = pexpect.spawnu("bin/cvc4", timeout=1) - # We expect to see the CVC4 prompt - child.expect("CVC4>") + # We expect to see the cvc5 prompt + child.expect("cvc5>") # If we send a line with just 'BOOLE' ... child.sendline("BOOLE") @@ -56,8 +56,8 @@ def check_iteractive_shell(): # Send enter child.sendcontrol("m") - # We expect to see the CVC4 prompt - child.expect("CVC4>") + # We expect to see the cvc5 prompt + child.expect("cvc5>") # Now send an up key child.send("\033[A") diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index d4aeaf427..3f1fa6733 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -47,7 +47,7 @@ int main() { return runTest(); } - catch (api::CVC4ApiException& e) + catch (api::CVC5ApiException& e) { std::cerr << e.getMessage() << std::endl; } @@ -97,7 +97,7 @@ std::string parse(std::string instr, api::Solver solver; InputLanguage ilang = - input_language == "smt2" ? input::LANG_SMTLIB_V2 : input::LANG_CVC4; + input_language == "smt2" ? input::LANG_SMTLIB_V2 : input::LANG_CVC; solver.setOption("input-language", input_language); solver.setOption("output-language", output_language); @@ -131,10 +131,10 @@ std::string translate(std::string instr, std::cout << "==============================================" << std::endl << "translating from " << (input_language == "smt2" ? input::LANG_SMTLIB_V2 - : input::LANG_CVC4) + : input::LANG_CVC) << " to " << (output_language == "smt2" ? output::LANG_SMTLIB_V2 - : output::LANG_CVC4) + : output::LANG_CVC) << " this string:" << std::endl << instr << std::endl; std::string outstr = parse(instr, input_language, output_language); @@ -142,7 +142,7 @@ std::string translate(std::string instr, << outstr << std::endl << "reparsing as " << (output_language == "smt2" ? input::LANG_SMTLIB_V2 - : input::LANG_CVC4) + : input::LANG_CVC) << std::endl; std::string poutstr = parse(outstr, output_language, output_language); assert(outstr == poutstr); diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp index 2d37d5c36..c01d16bfc 100644 --- a/test/api/sep_log_api.cpp +++ b/test/api/sep_log_api.cpp @@ -85,7 +85,7 @@ int validate_exception(void) { Term heap_expr = slv.getSeparationHeap(); } - catch (const CVC4ApiException& e) + catch (const CVC5ApiException& e) { caught_on_heap = true; @@ -101,7 +101,7 @@ int validate_exception(void) { Term nil_expr = slv.getSeparationNilTerm(); } - catch (const CVC4ApiException& e) + catch (const CVC5ApiException& e) { caught_on_nil = true; 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__": diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp index 7c85f84e0..3fbdcc0b5 100644 --- a/test/unit/api/datatype_api_black.cpp +++ b/test/unit/api/datatype_api_black.cpp @@ -37,7 +37,7 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSort) Datatype d = listSort.getDatatype(); DatatypeConstructor consConstr = d[0]; DatatypeConstructor nilConstr = d[1]; - ASSERT_THROW(d[2], CVC4ApiException); + ASSERT_THROW(d[2], CVC5ApiException); ASSERT_NO_THROW(consConstr.getConstructorTerm()); ASSERT_NO_THROW(nilConstr.getConstructorTerm()); } @@ -104,7 +104,7 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSorts) std::vector<DatatypeDecl> dtdeclsBad; DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD"); dtdeclsBad.push_back(emptyD); - ASSERT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException); + ASSERT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC5ApiException); } TEST_F(TestApiBlackDatatype, datatypeStructs) @@ -118,7 +118,7 @@ TEST_F(TestApiBlackDatatype, datatypeStructs) cons.addSelector("head", intSort); cons.addSelectorSelf("tail"); Sort nullSort; - ASSERT_THROW(cons.addSelector("null", nullSort), CVC4ApiException); + ASSERT_THROW(cons.addSelector("null", nullSort), CVC5ApiException); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); @@ -200,14 +200,14 @@ TEST_F(TestApiBlackDatatype, datatypeNames) ASSERT_EQ(dt.getName(), std::string("list")); ASSERT_NO_THROW(dt.getConstructor("nil")); ASSERT_NO_THROW(dt["cons"]); - ASSERT_THROW(dt.getConstructor("head"), CVC4ApiException); - ASSERT_THROW(dt.getConstructor(""), CVC4ApiException); + ASSERT_THROW(dt.getConstructor("head"), CVC5ApiException); + ASSERT_THROW(dt.getConstructor(""), CVC5ApiException); DatatypeConstructor dcons = dt[0]; ASSERT_EQ(dcons.getName(), std::string("cons")); ASSERT_NO_THROW(dcons.getSelector("head")); ASSERT_NO_THROW(dcons["tail"]); - ASSERT_THROW(dcons.getSelector("cons"), CVC4ApiException); + ASSERT_THROW(dcons.getSelector("cons"), CVC5ApiException); // get selector DatatypeSelector dselTail = dcons[1]; @@ -215,7 +215,7 @@ TEST_F(TestApiBlackDatatype, datatypeNames) ASSERT_EQ(dselTail.getRangeSort(), dtypeSort); // possible to construct null datatype declarations if not using solver - ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException); + ASSERT_THROW(DatatypeDecl().getName(), CVC5ApiException); } TEST_F(TestApiBlackDatatype, parametricDatatype) @@ -543,7 +543,7 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons) ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt)); ASSERT_NE(testConsTerm, nilc.getConstructorTerm()); // error to get the specialized constructor term for Int - ASSERT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException); + ASSERT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC5ApiException); } } // namespace test } // namespace cvc5 diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp index ccab121db..7b7556539 100644 --- a/test/unit/api/grammar_black.cpp +++ b/test/unit/api/grammar_black.cpp @@ -39,15 +39,15 @@ TEST_F(TestApiBlackGrammar, addRule) ASSERT_NO_THROW(g.addRule(start, d_solver.mkBoolean(false))); ASSERT_THROW(g.addRule(nullTerm, d_solver.mkBoolean(false)), - CVC4ApiException); - ASSERT_THROW(g.addRule(start, nullTerm), CVC4ApiException); - ASSERT_THROW(g.addRule(nts, d_solver.mkBoolean(false)), CVC4ApiException); - ASSERT_THROW(g.addRule(start, d_solver.mkInteger(0)), CVC4ApiException); - ASSERT_THROW(g.addRule(start, nts), CVC4ApiException); + CVC5ApiException); + ASSERT_THROW(g.addRule(start, nullTerm), CVC5ApiException); + ASSERT_THROW(g.addRule(nts, d_solver.mkBoolean(false)), CVC5ApiException); + ASSERT_THROW(g.addRule(start, d_solver.mkInteger(0)), CVC5ApiException); + ASSERT_THROW(g.addRule(start, nts), CVC5ApiException); d_solver.synthFun("f", {}, boolean, g); - ASSERT_THROW(g.addRule(start, d_solver.mkBoolean(false)), CVC4ApiException); + ASSERT_THROW(g.addRule(start, d_solver.mkBoolean(false)), CVC5ApiException); } TEST_F(TestApiBlackGrammar, addRules) @@ -64,16 +64,16 @@ TEST_F(TestApiBlackGrammar, addRules) ASSERT_NO_THROW(g.addRules(start, {d_solver.mkBoolean(false)})); ASSERT_THROW(g.addRules(nullTerm, {d_solver.mkBoolean(false)}), - CVC4ApiException); - ASSERT_THROW(g.addRules(start, {nullTerm}), CVC4ApiException); - ASSERT_THROW(g.addRules(nts, {d_solver.mkBoolean(false)}), CVC4ApiException); - ASSERT_THROW(g.addRules(start, {d_solver.mkInteger(0)}), CVC4ApiException); - ASSERT_THROW(g.addRules(start, {nts}), CVC4ApiException); + CVC5ApiException); + ASSERT_THROW(g.addRules(start, {nullTerm}), CVC5ApiException); + ASSERT_THROW(g.addRules(nts, {d_solver.mkBoolean(false)}), CVC5ApiException); + ASSERT_THROW(g.addRules(start, {d_solver.mkInteger(0)}), CVC5ApiException); + ASSERT_THROW(g.addRules(start, {nts}), CVC5ApiException); d_solver.synthFun("f", {}, boolean, g); ASSERT_THROW(g.addRules(start, {d_solver.mkBoolean(false)}), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackGrammar, addAnyConstant) @@ -89,12 +89,12 @@ TEST_F(TestApiBlackGrammar, addAnyConstant) ASSERT_NO_THROW(g.addAnyConstant(start)); ASSERT_NO_THROW(g.addAnyConstant(start)); - ASSERT_THROW(g.addAnyConstant(nullTerm), CVC4ApiException); - ASSERT_THROW(g.addAnyConstant(nts), CVC4ApiException); + ASSERT_THROW(g.addAnyConstant(nullTerm), CVC5ApiException); + ASSERT_THROW(g.addAnyConstant(nts), CVC5ApiException); d_solver.synthFun("f", {}, boolean, g); - ASSERT_THROW(g.addAnyConstant(start), CVC4ApiException); + ASSERT_THROW(g.addAnyConstant(start), CVC5ApiException); } TEST_F(TestApiBlackGrammar, addAnyVariable) @@ -113,12 +113,12 @@ TEST_F(TestApiBlackGrammar, addAnyVariable) ASSERT_NO_THROW(g1.addAnyVariable(start)); ASSERT_NO_THROW(g2.addAnyVariable(start)); - ASSERT_THROW(g1.addAnyVariable(nullTerm), CVC4ApiException); - ASSERT_THROW(g1.addAnyVariable(nts), CVC4ApiException); + ASSERT_THROW(g1.addAnyVariable(nullTerm), CVC5ApiException); + ASSERT_THROW(g1.addAnyVariable(nts), CVC5ApiException); d_solver.synthFun("f", {}, boolean, g1); - ASSERT_THROW(g1.addAnyVariable(start), CVC4ApiException); + ASSERT_THROW(g1.addAnyVariable(start), CVC5ApiException); } } // namespace test } // namespace cvc5 diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp index 0b67c0013..e7b83f455 100644 --- a/test/unit/api/op_black.cpp +++ b/test/unit/api/op_black.cpp @@ -43,13 +43,13 @@ TEST_F(TestApiBlackOp, isNull) TEST_F(TestApiBlackOp, opFromKind) { ASSERT_NO_THROW(d_solver.mkOp(PLUS)); - ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException); + ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC5ApiException); } TEST_F(TestApiBlackOp, getIndicesString) { Op x; - ASSERT_THROW(x.getIndices<std::string>(), CVC4ApiException); + ASSERT_THROW(x.getIndices<std::string>(), CVC5ApiException); Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4); ASSERT_TRUE(divisible_ot.isIndexed()); @@ -59,7 +59,7 @@ TEST_F(TestApiBlackOp, getIndicesString) Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test"); std::string record_update_idx = record_update_ot.getIndices<std::string>(); ASSERT_EQ(record_update_idx, "test"); - ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC4ApiException); + ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC5ApiException); } TEST_F(TestApiBlackOp, getIndicesUint) @@ -70,7 +70,7 @@ TEST_F(TestApiBlackOp, getIndicesUint) ASSERT_EQ(bitvector_repeat_idx, 5); ASSERT_THROW( (bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()), - CVC4ApiException); + CVC5ApiException); Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6); uint32_t bitvector_zero_extend_idx = @@ -109,7 +109,7 @@ TEST_F(TestApiBlackOp, getIndicesUint) Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5); uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>(); ASSERT_EQ(tuple_update_idx, 5); - ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC4ApiException); + ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC5ApiException); } TEST_F(TestApiBlackOp, getIndicesPairUint) @@ -168,7 +168,7 @@ TEST_F(TestApiBlackOp, getIndicesPairUint) ASSERT_TRUE((floatingpoint_to_fp_generic_indices == std::pair<uint32_t, uint32_t>{4, 25})); ASSERT_THROW(floatingpoint_to_fp_generic_ot.getIndices<std::string>(), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackOp, opScopingToString) diff --git a/test/unit/api/op_white.cpp b/test/unit/api/op_white.cpp index 4953cdd60..39952739b 100644 --- a/test/unit/api/op_white.cpp +++ b/test/unit/api/op_white.cpp @@ -29,7 +29,7 @@ TEST_F(TestApiWhiteOp, opFromKind) { Op plus(&d_solver, PLUS); ASSERT_FALSE(plus.isIndexed()); - ASSERT_THROW(plus.getIndices<uint32_t>(), CVC4ApiException); + ASSERT_THROW(plus.getIndices<uint32_t>(), CVC5ApiException); ASSERT_EQ(plus, d_solver.mkOp(PLUS)); } } // namespace test diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index c5cdf4f8c..361bfa8aa 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -30,7 +30,7 @@ TEST_F(TestApiBlackSolver, recoverableException) d_solver.setOption("produce-models", "true"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x).notTerm()); - ASSERT_THROW(d_solver.getValue(x), CVC4ApiRecoverableException); + ASSERT_THROW(d_solver.getValue(x), CVC5ApiRecoverableException); } TEST_F(TestApiBlackSolver, supportsFloatingPoint) @@ -42,7 +42,7 @@ TEST_F(TestApiBlackSolver, supportsFloatingPoint) else { ASSERT_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN), - CVC4ApiException); + CVC5ApiException); } } @@ -84,7 +84,7 @@ TEST_F(TestApiBlackSolver, getRoundingModeSort) } else { - ASSERT_THROW(d_solver.getRoundingModeSort(), CVC4ApiException); + ASSERT_THROW(d_solver.getRoundingModeSort(), CVC5ApiException); } } @@ -109,13 +109,13 @@ TEST_F(TestApiBlackSolver, mkArraySort) } Solver slv; - ASSERT_THROW(slv.mkArraySort(boolSort, boolSort), CVC4ApiException); + ASSERT_THROW(slv.mkArraySort(boolSort, boolSort), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkBitVectorSort) { ASSERT_NO_THROW(d_solver.mkBitVectorSort(32)); - ASSERT_THROW(d_solver.mkBitVectorSort(0), CVC4ApiException); + ASSERT_THROW(d_solver.mkBitVectorSort(0), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkFloatingPointSort) @@ -123,12 +123,12 @@ TEST_F(TestApiBlackSolver, mkFloatingPointSort) if (d_solver.supportsFloatingPoint()) { ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8)); - ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException); - ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException); + ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC5ApiException); + ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC5ApiException); } else { - ASSERT_THROW(d_solver.mkFloatingPointSort(4, 8), CVC4ApiException); + ASSERT_THROW(d_solver.mkFloatingPointSort(4, 8), CVC5ApiException); } } @@ -143,10 +143,10 @@ TEST_F(TestApiBlackSolver, mkDatatypeSort) ASSERT_NO_THROW(d_solver.mkDatatypeSort(dtypeSpec)); Solver slv; - ASSERT_THROW(slv.mkDatatypeSort(dtypeSpec), CVC4ApiException); + ASSERT_THROW(slv.mkDatatypeSort(dtypeSpec), CVC5ApiException); DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list"); - ASSERT_THROW(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException); + ASSERT_THROW(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkDatatypeSorts) @@ -168,11 +168,11 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts) std::vector<DatatypeDecl> decls = {dtypeSpec1, dtypeSpec2}; ASSERT_NO_THROW(d_solver.mkDatatypeSorts(decls)); - ASSERT_THROW(slv.mkDatatypeSorts(decls), CVC4ApiException); + ASSERT_THROW(slv.mkDatatypeSorts(decls), CVC5ApiException); DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list"); std::vector<DatatypeDecl> throwsDecls = {throwsDtypeSpec}; - ASSERT_THROW(d_solver.mkDatatypeSorts(throwsDecls), CVC4ApiException); + ASSERT_THROW(d_solver.mkDatatypeSorts(throwsDecls), CVC5ApiException); /* with unresolved sorts */ Sort unresList = d_solver.mkUninterpretedSort("ulist"); @@ -187,7 +187,7 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts) std::vector<DatatypeDecl> udecls = {ulist}; ASSERT_NO_THROW(d_solver.mkDatatypeSorts(udecls, unresSorts)); - ASSERT_THROW(slv.mkDatatypeSorts(udecls, unresSorts), CVC4ApiException); + ASSERT_THROW(slv.mkDatatypeSorts(udecls, unresSorts), CVC5ApiException); /* Note: More tests are in datatype_api_black. */ } @@ -203,9 +203,9 @@ TEST_F(TestApiBlackSolver, mkFunctionSort) // non-first-class arguments are not allowed Sort reSort = d_solver.getRegExpSort(); ASSERT_THROW(d_solver.mkFunctionSort(reSort, d_solver.getIntegerSort()), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort), - CVC4ApiException); + CVC5ApiException); ASSERT_NO_THROW(d_solver.mkFunctionSort( {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()}, d_solver.getIntegerSort())); @@ -218,24 +218,24 @@ TEST_F(TestApiBlackSolver, mkFunctionSort) ASSERT_THROW(d_solver.mkFunctionSort({d_solver.getIntegerSort(), d_solver.mkUninterpretedSort("u")}, funSort2), - CVC4ApiException); + CVC5ApiException); Solver slv; ASSERT_THROW(slv.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.mkFunctionSort(slv.mkUninterpretedSort("u"), d_solver.getIntegerSort()), - CVC4ApiException); + CVC5ApiException); std::vector<Sort> sorts1 = {d_solver.getBooleanSort(), slv.getIntegerSort(), d_solver.getIntegerSort()}; std::vector<Sort> sorts2 = {slv.getBooleanSort(), slv.getIntegerSort()}; ASSERT_NO_THROW(slv.mkFunctionSort(sorts2, slv.getIntegerSort())); ASSERT_THROW(slv.mkFunctionSort(sorts1, slv.getIntegerSort()), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.mkFunctionSort(sorts2, d_solver.getIntegerSort()), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackSolver, mkParamSort) @@ -247,7 +247,7 @@ TEST_F(TestApiBlackSolver, mkParamSort) TEST_F(TestApiBlackSolver, mkPredicateSort) { ASSERT_NO_THROW(d_solver.mkPredicateSort({d_solver.getIntegerSort()})); - ASSERT_THROW(d_solver.mkPredicateSort({}), CVC4ApiException); + ASSERT_THROW(d_solver.mkPredicateSort({}), CVC5ApiException); Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()); // functions as arguments are allowed @@ -256,7 +256,7 @@ TEST_F(TestApiBlackSolver, mkPredicateSort) Solver slv; ASSERT_THROW(slv.mkPredicateSort({d_solver.getIntegerSort()}), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackSolver, mkRecordSort) @@ -272,7 +272,7 @@ TEST_F(TestApiBlackSolver, mkRecordSort) ASSERT_NO_THROW(recSort.getDatatype()); Solver slv; - ASSERT_THROW(slv.mkRecordSort(fields), CVC4ApiException); + ASSERT_THROW(slv.mkRecordSort(fields), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkSetSort) @@ -281,7 +281,7 @@ TEST_F(TestApiBlackSolver, mkSetSort) ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.getIntegerSort())); ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.mkBitVectorSort(4))); Solver slv; - ASSERT_THROW(slv.mkSetSort(d_solver.mkBitVectorSort(4)), CVC4ApiException); + ASSERT_THROW(slv.mkSetSort(d_solver.mkBitVectorSort(4)), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkBagSort) @@ -290,7 +290,7 @@ TEST_F(TestApiBlackSolver, mkBagSort) ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.getIntegerSort())); ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.mkBitVectorSort(4))); Solver slv; - ASSERT_THROW(slv.mkBagSort(d_solver.mkBitVectorSort(4)), CVC4ApiException); + ASSERT_THROW(slv.mkBagSort(d_solver.mkBitVectorSort(4)), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkSequenceSort) @@ -299,7 +299,7 @@ TEST_F(TestApiBlackSolver, mkSequenceSort) ASSERT_NO_THROW(d_solver.mkSequenceSort( d_solver.mkSequenceSort(d_solver.getIntegerSort()))); Solver slv; - ASSERT_THROW(slv.mkSequenceSort(d_solver.getIntegerSort()), CVC4ApiException); + ASSERT_THROW(slv.mkSequenceSort(d_solver.getIntegerSort()), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkUninterpretedSort) @@ -312,7 +312,7 @@ TEST_F(TestApiBlackSolver, mkSortConstructorSort) { ASSERT_NO_THROW(d_solver.mkSortConstructorSort("s", 2)); ASSERT_NO_THROW(d_solver.mkSortConstructorSort("", 2)); - ASSERT_THROW(d_solver.mkSortConstructorSort("", 0), CVC4ApiException); + ASSERT_THROW(d_solver.mkSortConstructorSort("", 0), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkTupleSort) @@ -321,10 +321,10 @@ TEST_F(TestApiBlackSolver, mkTupleSort) Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()); ASSERT_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}), - CVC4ApiException); + CVC5ApiException); Solver slv; - ASSERT_THROW(slv.mkTupleSort({d_solver.getIntegerSort()}), CVC4ApiException); + ASSERT_THROW(slv.mkTupleSort({d_solver.getIntegerSort()}), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkBitVector) @@ -339,13 +339,13 @@ TEST_F(TestApiBlackSolver, mkBitVector) ASSERT_NO_THROW(d_solver.mkBitVector("1010", 16)); ASSERT_NO_THROW(d_solver.mkBitVector("a09f", 16)); ASSERT_NO_THROW(d_solver.mkBitVector(8, "-127", 10)); - ASSERT_THROW(d_solver.mkBitVector(size0, val1), CVC4ApiException); - ASSERT_THROW(d_solver.mkBitVector(size0, val2), CVC4ApiException); - ASSERT_THROW(d_solver.mkBitVector("", 2), CVC4ApiException); - ASSERT_THROW(d_solver.mkBitVector("10", 3), CVC4ApiException); - ASSERT_THROW(d_solver.mkBitVector("20", 2), CVC4ApiException); - ASSERT_THROW(d_solver.mkBitVector(8, "101010101", 2), CVC4ApiException); - ASSERT_THROW(d_solver.mkBitVector(8, "-256", 10), CVC4ApiException); + ASSERT_THROW(d_solver.mkBitVector(size0, val1), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector(size0, val2), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector("", 2), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector("10", 3), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector("20", 2), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector(8, "101010101", 2), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector(8, "-256", 10), CVC5ApiException); ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("10", 10)); ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("a", 16)); ASSERT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101"); @@ -363,10 +363,10 @@ TEST_F(TestApiBlackSolver, mkVar) ASSERT_NO_THROW(d_solver.mkVar(funSort)); ASSERT_NO_THROW(d_solver.mkVar(boolSort, std::string("b"))); ASSERT_NO_THROW(d_solver.mkVar(funSort, "")); - ASSERT_THROW(d_solver.mkVar(Sort()), CVC4ApiException); - ASSERT_THROW(d_solver.mkVar(Sort(), "a"), CVC4ApiException); + ASSERT_THROW(d_solver.mkVar(Sort()), CVC5ApiException); + ASSERT_THROW(d_solver.mkVar(Sort(), "a"), CVC5ApiException); Solver slv; - ASSERT_THROW(slv.mkVar(boolSort, "x"), CVC4ApiException); + ASSERT_THROW(slv.mkVar(boolSort, "x"), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkBoolean) @@ -384,27 +384,27 @@ TEST_F(TestApiBlackSolver, mkRoundingMode) else { ASSERT_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO), - CVC4ApiException); + CVC5ApiException); } } TEST_F(TestApiBlackSolver, mkUninterpretedConst) { ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC4ApiException); + ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC5ApiException); Solver slv; ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackSolver, mkAbstractValue) { ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1"))); - ASSERT_THROW(d_solver.mkAbstractValue(std::string("0")), CVC4ApiException); - ASSERT_THROW(d_solver.mkAbstractValue(std::string("-1")), CVC4ApiException); - ASSERT_THROW(d_solver.mkAbstractValue(std::string("1.2")), CVC4ApiException); - ASSERT_THROW(d_solver.mkAbstractValue("1/2"), CVC4ApiException); - ASSERT_THROW(d_solver.mkAbstractValue("asdf"), CVC4ApiException); + ASSERT_THROW(d_solver.mkAbstractValue(std::string("0")), CVC5ApiException); + ASSERT_THROW(d_solver.mkAbstractValue(std::string("-1")), CVC5ApiException); + ASSERT_THROW(d_solver.mkAbstractValue(std::string("1.2")), CVC5ApiException); + ASSERT_THROW(d_solver.mkAbstractValue("1/2"), CVC5ApiException); + ASSERT_THROW(d_solver.mkAbstractValue("asdf"), CVC5ApiException); ASSERT_NO_THROW(d_solver.mkAbstractValue((uint32_t)1)); ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)1)); @@ -412,7 +412,7 @@ TEST_F(TestApiBlackSolver, mkAbstractValue) ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)1)); ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)-1)); ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)-1)); - ASSERT_THROW(d_solver.mkAbstractValue(0), CVC4ApiException); + ASSERT_THROW(d_solver.mkAbstractValue(0), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkFloatingPoint) @@ -426,18 +426,18 @@ TEST_F(TestApiBlackSolver, mkFloatingPoint) } else { - ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t1), CVC4ApiException); + ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t1), CVC5ApiException); } - ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, Term()), CVC4ApiException); - ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, t1), CVC4ApiException); - ASSERT_THROW(d_solver.mkFloatingPoint(3, 0, t1), CVC4ApiException); - ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException); - ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException); + ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, Term()), CVC5ApiException); + ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, t1), CVC5ApiException); + ASSERT_THROW(d_solver.mkFloatingPoint(3, 0, t1), CVC5ApiException); + ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC5ApiException); + ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC5ApiException); if (d_solver.supportsFloatingPoint()) { Solver slv; - ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC4ApiException); + ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC5ApiException); } } @@ -448,8 +448,8 @@ TEST_F(TestApiBlackSolver, mkEmptySet) ASSERT_NO_THROW(d_solver.mkEmptySet(Sort())); ASSERT_NO_THROW(d_solver.mkEmptySet(s)); ASSERT_THROW(d_solver.mkEmptySet(d_solver.getBooleanSort()), - CVC4ApiException); - ASSERT_THROW(slv.mkEmptySet(s), CVC4ApiException); + CVC5ApiException); + ASSERT_THROW(slv.mkEmptySet(s), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkEmptyBag) @@ -459,8 +459,8 @@ TEST_F(TestApiBlackSolver, mkEmptyBag) ASSERT_NO_THROW(d_solver.mkEmptyBag(Sort())); ASSERT_NO_THROW(d_solver.mkEmptyBag(s)); ASSERT_THROW(d_solver.mkEmptyBag(d_solver.getBooleanSort()), - CVC4ApiException); - ASSERT_THROW(slv.mkEmptyBag(s), CVC4ApiException); + CVC5ApiException); + ASSERT_THROW(slv.mkEmptyBag(s), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkEmptySequence) @@ -469,7 +469,7 @@ TEST_F(TestApiBlackSolver, mkEmptySequence) Sort s = d_solver.mkSequenceSort(d_solver.getBooleanSort()); ASSERT_NO_THROW(d_solver.mkEmptySequence(s)); ASSERT_NO_THROW(d_solver.mkEmptySequence(d_solver.getBooleanSort())); - ASSERT_THROW(slv.mkEmptySequence(s), CVC4ApiException); + ASSERT_THROW(slv.mkEmptySequence(s), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkFalse) @@ -486,7 +486,7 @@ TEST_F(TestApiBlackSolver, mkNaN) } else { - ASSERT_THROW(d_solver.mkNaN(3, 5), CVC4ApiException); + ASSERT_THROW(d_solver.mkNaN(3, 5), CVC5ApiException); } } @@ -498,7 +498,7 @@ TEST_F(TestApiBlackSolver, mkNegZero) } else { - ASSERT_THROW(d_solver.mkNegZero(3, 5), CVC4ApiException); + ASSERT_THROW(d_solver.mkNegZero(3, 5), CVC5ApiException); } } @@ -510,7 +510,7 @@ TEST_F(TestApiBlackSolver, mkNegInf) } else { - ASSERT_THROW(d_solver.mkNegInf(3, 5), CVC4ApiException); + ASSERT_THROW(d_solver.mkNegInf(3, 5), CVC5ApiException); } } @@ -522,7 +522,7 @@ TEST_F(TestApiBlackSolver, mkPosInf) } else { - ASSERT_THROW(d_solver.mkPosInf(3, 5), CVC4ApiException); + ASSERT_THROW(d_solver.mkPosInf(3, 5), CVC5ApiException); } } @@ -534,29 +534,29 @@ TEST_F(TestApiBlackSolver, mkPosZero) } else { - ASSERT_THROW(d_solver.mkPosZero(3, 5), CVC4ApiException); + ASSERT_THROW(d_solver.mkPosZero(3, 5), CVC5ApiException); } } TEST_F(TestApiBlackSolver, mkOp) { // mkOp(Kind kind, Kind k) - ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL), CVC4ApiException); + ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL), CVC5ApiException); // mkOp(Kind kind, const std::string& arg) ASSERT_NO_THROW(d_solver.mkOp(RECORD_UPDATE, "asdf")); ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, "2147483648")); - ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, "asdf"), CVC4ApiException); + ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, "asdf"), CVC5ApiException); // mkOp(Kind kind, uint32_t arg) ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, 1)); ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 1)); ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 1)); - ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1), CVC4ApiException); + ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1), CVC5ApiException); // mkOp(Kind kind, uint32_t arg1, uint32_t arg2) ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1, 1)); - ASSERT_THROW(d_solver.mkOp(DIVISIBLE, 1, 2), CVC4ApiException); + ASSERT_THROW(d_solver.mkOp(DIVISIBLE, 1, 2), CVC5ApiException); // mkOp(Kind kind, std::vector<uint32_t> args) std::vector<uint32_t> args = {1, 2, 2}; @@ -568,32 +568,32 @@ TEST_F(TestApiBlackSolver, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); } TEST_F(TestApiBlackSolver, mkInteger) { ASSERT_NO_THROW(d_solver.mkInteger("123")); - ASSERT_THROW(d_solver.mkInteger("1.23"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("1/23"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("12/3"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(".2"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("2."), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(""), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("asdf"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("1.2/3"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("."), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("/"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("2/"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("/2"), CVC4ApiException); + ASSERT_THROW(d_solver.mkInteger("1.23"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("1/23"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("12/3"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(".2"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("2."), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(""), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("asdf"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("1.2/3"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("."), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("/"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("2/"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("/2"), CVC5ApiException); ASSERT_NO_THROW(d_solver.mkReal(std::string("123"))); - ASSERT_THROW(d_solver.mkInteger(std::string("1.23")), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(std::string("1/23")), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(std::string("12/3")), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(std::string(".2")), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(std::string("2.")), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(std::string("")), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(std::string("asdf")), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(std::string("1.2/3")), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(std::string(".")), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(std::string("/")), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(std::string("2/")), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger(std::string("/2")), CVC4ApiException); + ASSERT_THROW(d_solver.mkInteger(std::string("1.23")), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(std::string("1/23")), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(std::string("12/3")), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(std::string(".2")), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(std::string("2.")), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(std::string("")), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(std::string("asdf")), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(std::string("1.2/3")), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(std::string(".")), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(std::string("/")), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(std::string("2/")), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger(std::string("/2")), CVC5ApiException); int32_t val1 = 1; int64_t val2 = -1; @@ -614,13 +614,13 @@ TEST_F(TestApiBlackSolver, mkReal) ASSERT_NO_THROW(d_solver.mkReal("12/3")); ASSERT_NO_THROW(d_solver.mkReal(".2")); ASSERT_NO_THROW(d_solver.mkReal("2.")); - ASSERT_THROW(d_solver.mkReal(""), CVC4ApiException); - ASSERT_THROW(d_solver.mkReal("asdf"), CVC4ApiException); - ASSERT_THROW(d_solver.mkReal("1.2/3"), CVC4ApiException); - ASSERT_THROW(d_solver.mkReal("."), CVC4ApiException); - ASSERT_THROW(d_solver.mkReal("/"), CVC4ApiException); - ASSERT_THROW(d_solver.mkReal("2/"), CVC4ApiException); - ASSERT_THROW(d_solver.mkReal("/2"), CVC4ApiException); + ASSERT_THROW(d_solver.mkReal(""), CVC5ApiException); + ASSERT_THROW(d_solver.mkReal("asdf"), CVC5ApiException); + ASSERT_THROW(d_solver.mkReal("1.2/3"), CVC5ApiException); + ASSERT_THROW(d_solver.mkReal("."), CVC5ApiException); + ASSERT_THROW(d_solver.mkReal("/"), CVC5ApiException); + ASSERT_THROW(d_solver.mkReal("2/"), CVC5ApiException); + ASSERT_THROW(d_solver.mkReal("/2"), CVC5ApiException); ASSERT_NO_THROW(d_solver.mkReal(std::string("123"))); ASSERT_NO_THROW(d_solver.mkReal(std::string("1.23"))); @@ -628,13 +628,13 @@ TEST_F(TestApiBlackSolver, mkReal) ASSERT_NO_THROW(d_solver.mkReal(std::string("12/3"))); ASSERT_NO_THROW(d_solver.mkReal(std::string(".2"))); ASSERT_NO_THROW(d_solver.mkReal(std::string("2."))); - ASSERT_THROW(d_solver.mkReal(std::string("")), CVC4ApiException); - ASSERT_THROW(d_solver.mkReal(std::string("asdf")), CVC4ApiException); - ASSERT_THROW(d_solver.mkReal(std::string("1.2/3")), CVC4ApiException); - ASSERT_THROW(d_solver.mkReal(std::string(".")), CVC4ApiException); - ASSERT_THROW(d_solver.mkReal(std::string("/")), CVC4ApiException); - ASSERT_THROW(d_solver.mkReal(std::string("2/")), CVC4ApiException); - ASSERT_THROW(d_solver.mkReal(std::string("/2")), CVC4ApiException); + ASSERT_THROW(d_solver.mkReal(std::string("")), CVC5ApiException); + ASSERT_THROW(d_solver.mkReal(std::string("asdf")), CVC5ApiException); + ASSERT_THROW(d_solver.mkReal(std::string("1.2/3")), CVC5ApiException); + ASSERT_THROW(d_solver.mkReal(std::string(".")), CVC5ApiException); + ASSERT_THROW(d_solver.mkReal(std::string("/")), CVC5ApiException); + ASSERT_THROW(d_solver.mkReal(std::string("2/")), CVC5ApiException); + ASSERT_THROW(d_solver.mkReal(std::string("/2")), CVC5ApiException); int32_t val1 = 1; int64_t val2 = -1; @@ -670,9 +670,9 @@ TEST_F(TestApiBlackSolver, mkRegexpSigma) TEST_F(TestApiBlackSolver, mkSepNil) { ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort())); - ASSERT_THROW(d_solver.mkSepNil(Sort()), CVC4ApiException); + ASSERT_THROW(d_solver.mkSepNil(Sort()), CVC5ApiException); Solver slv; - ASSERT_THROW(slv.mkSepNil(d_solver.getIntegerSort()), CVC4ApiException); + ASSERT_THROW(slv.mkSepNil(d_solver.getIntegerSort()), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkString) @@ -689,9 +689,9 @@ TEST_F(TestApiBlackSolver, mkChar) { ASSERT_NO_THROW(d_solver.mkChar(std::string("0123"))); ASSERT_NO_THROW(d_solver.mkChar("aA")); - ASSERT_THROW(d_solver.mkChar(""), CVC4ApiException); - ASSERT_THROW(d_solver.mkChar("0g0"), CVC4ApiException); - ASSERT_THROW(d_solver.mkChar("100000"), CVC4ApiException); + ASSERT_THROW(d_solver.mkChar(""), CVC5ApiException); + ASSERT_THROW(d_solver.mkChar("0g0"), CVC5ApiException); + ASSERT_THROW(d_solver.mkChar("100000"), CVC5ApiException); ASSERT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC")); } @@ -712,44 +712,44 @@ TEST_F(TestApiBlackSolver, mkTerm) ASSERT_NO_THROW(d_solver.mkTerm(PI)); ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_EMPTY)); ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_SIGMA)); - ASSERT_THROW(d_solver.mkTerm(CONST_BITVECTOR), CVC4ApiException); + ASSERT_THROW(d_solver.mkTerm(CONST_BITVECTOR), CVC5ApiException); // mkTerm(Kind kind, Term child) const ASSERT_NO_THROW(d_solver.mkTerm(NOT, d_solver.mkTrue())); - ASSERT_THROW(d_solver.mkTerm(NOT, Term()), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(NOT, a), CVC4ApiException); - ASSERT_THROW(slv.mkTerm(NOT, d_solver.mkTrue()), CVC4ApiException); + ASSERT_THROW(d_solver.mkTerm(NOT, Term()), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(NOT, a), CVC5ApiException); + ASSERT_THROW(slv.mkTerm(NOT, d_solver.mkTrue()), CVC5ApiException); // mkTerm(Kind kind, Term child1, Term child2) const ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, a, b)); - ASSERT_THROW(d_solver.mkTerm(EQUAL, Term(), b), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(EQUAL, a, Term()), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(EQUAL, a, d_solver.mkTrue()), CVC4ApiException); - ASSERT_THROW(slv.mkTerm(EQUAL, a, b), CVC4ApiException); + ASSERT_THROW(d_solver.mkTerm(EQUAL, Term(), b), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(EQUAL, a, Term()), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(EQUAL, a, d_solver.mkTrue()), CVC5ApiException); + ASSERT_THROW(slv.mkTerm(EQUAL, a, b), CVC5ApiException); // mkTerm(Kind kind, Term child1, Term child2, Term child3) const ASSERT_NO_THROW(d_solver.mkTerm( ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue())); ASSERT_THROW( d_solver.mkTerm(ITE, Term(), d_solver.mkTrue(), d_solver.mkTrue()), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW( d_solver.mkTerm(ITE, d_solver.mkTrue(), Term(), d_solver.mkTrue()), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW( d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), Term()), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), b), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW( slv.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()), - CVC4ApiException); + CVC5ApiException); // mkTerm(Kind kind, const std::vector<Term>& children) const ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, v1)); - ASSERT_THROW(d_solver.mkTerm(EQUAL, v2), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(EQUAL, v3), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(DISTINCT, v6), CVC4ApiException); + ASSERT_THROW(d_solver.mkTerm(EQUAL, v2), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(EQUAL, v3), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(DISTINCT, v6), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkTermFromOp) @@ -795,25 +795,25 @@ TEST_F(TestApiBlackSolver, mkTermFromOp) // mkTerm(Op op, Term term) const ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)); ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm2)); - ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, nilTerm1), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, consTerm1), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm2), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(opterm1), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, headTerm1), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(opterm1), CVC4ApiException); - ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1), CVC4ApiException); + ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, nilTerm1), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, consTerm1), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm2), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, headTerm1), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException); + ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1), CVC5ApiException); // mkTerm(Op op, Term child) const ASSERT_NO_THROW(d_solver.mkTerm(opterm1, a)); ASSERT_NO_THROW(d_solver.mkTerm(opterm2, d_solver.mkInteger(1))); ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, headTerm1, c)); ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, tailTerm2, c)); - ASSERT_THROW(d_solver.mkTerm(opterm2, a), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(opterm1, Term()), CVC4ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm2, a), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm1, Term()), CVC5ApiException); ASSERT_THROW( d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver.mkInteger(0)), - CVC4ApiException); - ASSERT_THROW(slv.mkTerm(opterm1, a), CVC4ApiException); + CVC5ApiException); + ASSERT_THROW(slv.mkTerm(opterm1, a), CVC5ApiException); // mkTerm(Op op, Term child1, Term child2) const ASSERT_NO_THROW( @@ -823,31 +823,31 @@ TEST_F(TestApiBlackSolver, mkTermFromOp) d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1))); ASSERT_THROW( d_solver.mkTerm(opterm2, d_solver.mkInteger(1), d_solver.mkInteger(2)), - CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(opterm1, a, b), CVC4ApiException); + CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm1, a, b), CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(opterm2, d_solver.mkInteger(1), Term()), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(opterm2, Term(), d_solver.mkInteger(1)), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver.mkInteger(0), d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)), - CVC4ApiException); + CVC5ApiException); // mkTerm(Op op, Term child1, Term child2, Term child3) const - ASSERT_THROW(d_solver.mkTerm(opterm1, a, b, a), CVC4ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm1, a, b, a), CVC5ApiException); ASSERT_THROW( d_solver.mkTerm( opterm2, d_solver.mkInteger(1), d_solver.mkInteger(1), Term()), - CVC4ApiException); + CVC5ApiException); // mkTerm(Op op, const std::vector<Term>& children) const ASSERT_NO_THROW(d_solver.mkTerm(opterm2, v4)); - ASSERT_THROW(d_solver.mkTerm(opterm2, v1), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(opterm2, v2), CVC4ApiException); - ASSERT_THROW(d_solver.mkTerm(opterm2, v3), CVC4ApiException); - ASSERT_THROW(slv.mkTerm(opterm2, v4), CVC4ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm2, v1), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm2, v2), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(opterm2, v3), CVC5ApiException); + ASSERT_THROW(slv.mkTerm(opterm2, v4), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkTrue) @@ -864,28 +864,28 @@ TEST_F(TestApiBlackSolver, mkTuple) d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkInteger("5")})); ASSERT_THROW(d_solver.mkTuple({}, {d_solver.mkBitVector("101", 2)}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(4)}, {d_solver.mkBitVector("101", 2)}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW( d_solver.mkTuple({d_solver.getIntegerSort()}, {d_solver.mkReal("5.3")}), - CVC4ApiException); + CVC5ApiException); Solver slv; ASSERT_THROW( slv.mkTuple({d_solver.mkBitVectorSort(3)}, {slv.mkBitVector("101", 2)}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW( slv.mkTuple({slv.mkBitVectorSort(3)}, {d_solver.mkBitVector("101", 2)}), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackSolver, mkUniverseSet) { ASSERT_NO_THROW(d_solver.mkUniverseSet(d_solver.getBooleanSort())); - ASSERT_THROW(d_solver.mkUniverseSet(Sort()), CVC4ApiException); + ASSERT_THROW(d_solver.mkUniverseSet(Sort()), CVC5ApiException); Solver slv; - ASSERT_THROW(slv.mkUniverseSet(d_solver.getBooleanSort()), CVC4ApiException); + ASSERT_THROW(slv.mkUniverseSet(d_solver.getBooleanSort()), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkConst) @@ -899,11 +899,11 @@ TEST_F(TestApiBlackSolver, mkConst) ASSERT_NO_THROW(d_solver.mkConst(intSort, std::string("i"))); ASSERT_NO_THROW(d_solver.mkConst(funSort, "f")); ASSERT_NO_THROW(d_solver.mkConst(funSort, "")); - ASSERT_THROW(d_solver.mkConst(Sort()), CVC4ApiException); - ASSERT_THROW(d_solver.mkConst(Sort(), "a"), CVC4ApiException); + ASSERT_THROW(d_solver.mkConst(Sort()), CVC5ApiException); + ASSERT_THROW(d_solver.mkConst(Sort(), "a"), CVC5ApiException); Solver slv; - ASSERT_THROW(slv.mkConst(boolSort), CVC4ApiException); + ASSERT_THROW(slv.mkConst(boolSort), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkConstArray) @@ -914,16 +914,16 @@ TEST_F(TestApiBlackSolver, mkConstArray) Term constArr = d_solver.mkConstArray(arrSort, zero); ASSERT_NO_THROW(d_solver.mkConstArray(arrSort, zero)); - ASSERT_THROW(d_solver.mkConstArray(Sort(), zero), CVC4ApiException); - ASSERT_THROW(d_solver.mkConstArray(arrSort, Term()), CVC4ApiException); + ASSERT_THROW(d_solver.mkConstArray(Sort(), zero), CVC5ApiException); + ASSERT_THROW(d_solver.mkConstArray(arrSort, Term()), CVC5ApiException); ASSERT_THROW(d_solver.mkConstArray(arrSort, d_solver.mkBitVector(1, 1)), - CVC4ApiException); - ASSERT_THROW(d_solver.mkConstArray(intSort, zero), CVC4ApiException); + CVC5ApiException); + ASSERT_THROW(d_solver.mkConstArray(intSort, zero), CVC5ApiException); Solver slv; Term zero2 = slv.mkInteger(0); Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort()); - ASSERT_THROW(slv.mkConstArray(arrSort2, zero), CVC4ApiException); - ASSERT_THROW(slv.mkConstArray(arrSort, zero2), CVC4ApiException); + ASSERT_THROW(slv.mkConstArray(arrSort2, zero), CVC5ApiException); + ASSERT_THROW(slv.mkConstArray(arrSort, zero2), CVC5ApiException); } TEST_F(TestApiBlackSolver, declareDatatype) @@ -941,11 +941,11 @@ TEST_F(TestApiBlackSolver, declareDatatype) ASSERT_NO_THROW(d_solver.declareDatatype(std::string(""), ctors3)); std::vector<DatatypeConstructorDecl> ctors4; ASSERT_THROW(d_solver.declareDatatype(std::string("c"), ctors4), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.declareDatatype(std::string(""), ctors4), - CVC4ApiException); + CVC5ApiException); Solver slv; - ASSERT_THROW(slv.declareDatatype(std::string("a"), ctors1), CVC4ApiException); + ASSERT_THROW(slv.declareDatatype(std::string("a"), ctors1), CVC5ApiException); } TEST_F(TestApiBlackSolver, declareFun) @@ -956,13 +956,13 @@ TEST_F(TestApiBlackSolver, declareFun) ASSERT_NO_THROW(d_solver.declareFun("f1", {}, bvSort)); ASSERT_NO_THROW( d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort)); - ASSERT_THROW(d_solver.declareFun("f2", {}, funSort), CVC4ApiException); + ASSERT_THROW(d_solver.declareFun("f2", {}, funSort), CVC5ApiException); // functions as arguments is allowed ASSERT_NO_THROW(d_solver.declareFun("f4", {bvSort, funSort}, bvSort)); ASSERT_THROW(d_solver.declareFun("f5", {bvSort, bvSort}, funSort), - CVC4ApiException); + CVC5ApiException); Solver slv; - ASSERT_THROW(slv.declareFun("f1", {}, bvSort), CVC4ApiException); + ASSERT_THROW(slv.declareFun("f1", {}, bvSort), CVC5ApiException); } TEST_F(TestApiBlackSolver, declareSort) @@ -1006,30 +1006,30 @@ TEST_F(TestApiBlackSolver, defineFun) ASSERT_NO_THROW(d_solver.defineFun("ff", {b1, b2}, bvSort, v1)); ASSERT_NO_THROW(d_solver.defineFun(f1, {b1, b11}, v1)); ASSERT_THROW(d_solver.defineFun("ff", {v1, b2}, bvSort, v1), - CVC4ApiException); - ASSERT_THROW(d_solver.defineFun("fff", {b1}, bvSort, v3), CVC4ApiException); + CVC5ApiException); + ASSERT_THROW(d_solver.defineFun("fff", {b1}, bvSort, v3), CVC5ApiException); ASSERT_THROW(d_solver.defineFun("ffff", {b1}, funSort2, v3), - CVC4ApiException); + CVC5ApiException); // b3 has function sort, which is allowed as an argument ASSERT_NO_THROW(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1)); - ASSERT_THROW(d_solver.defineFun(f1, {v1, b11}, v1), CVC4ApiException); - ASSERT_THROW(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException); - ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException); - ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException); - ASSERT_THROW(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException); - ASSERT_THROW(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException); + ASSERT_THROW(d_solver.defineFun(f1, {v1, b11}, v1), CVC5ApiException); + ASSERT_THROW(d_solver.defineFun(f1, {b1}, v1), CVC5ApiException); + ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v2), CVC5ApiException); + ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v3), CVC5ApiException); + ASSERT_THROW(d_solver.defineFun(f2, {b1}, v2), CVC5ApiException); + ASSERT_THROW(d_solver.defineFun(f3, {b1}, v1), CVC5ApiException); Solver slv; Sort bvSort2 = slv.mkBitVectorSort(32); Term v12 = slv.mkConst(bvSort2, "v1"); Term b12 = slv.mkVar(bvSort2, "b1"); Term b22 = slv.mkVar(slv.getIntegerSort(), "b2"); - ASSERT_THROW(slv.defineFun("f", {}, bvSort, v12), CVC4ApiException); - ASSERT_THROW(slv.defineFun("f", {}, bvSort2, v1), CVC4ApiException); - ASSERT_THROW(slv.defineFun("ff", {b1, b22}, bvSort2, v12), CVC4ApiException); - ASSERT_THROW(slv.defineFun("ff", {b12, b2}, bvSort2, v12), CVC4ApiException); - ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort, v12), CVC4ApiException); - ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort2, v1), CVC4ApiException); + ASSERT_THROW(slv.defineFun("f", {}, bvSort, v12), CVC5ApiException); + ASSERT_THROW(slv.defineFun("f", {}, bvSort2, v1), CVC5ApiException); + ASSERT_THROW(slv.defineFun("ff", {b1, b22}, bvSort2, v12), CVC5ApiException); + ASSERT_THROW(slv.defineFun("ff", {b12, b2}, bvSort2, v12), CVC5ApiException); + ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort, v12), CVC5ApiException); + ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort2, v1), CVC5ApiException); } TEST_F(TestApiBlackSolver, defineFunGlobal) @@ -1076,18 +1076,18 @@ TEST_F(TestApiBlackSolver, defineFunRec) ASSERT_NO_THROW(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1)); ASSERT_NO_THROW(d_solver.defineFunRec(f1, {b1, b11}, v1)); ASSERT_THROW(d_solver.defineFunRec("fff", {b1}, bvSort, v3), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.defineFunRec("ff", {b1, v2}, bvSort, v1), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.defineFunRec("ffff", {b1}, funSort2, v3), - CVC4ApiException); + CVC5ApiException); // b3 has function sort, which is allowed as an argument ASSERT_NO_THROW(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1)); - ASSERT_THROW(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException); - ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException); - ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException); - ASSERT_THROW(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException); - ASSERT_THROW(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException); + ASSERT_THROW(d_solver.defineFunRec(f1, {b1}, v1), CVC5ApiException); + ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC5ApiException); + ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC5ApiException); + ASSERT_THROW(d_solver.defineFunRec(f2, {b1}, v2), CVC5ApiException); + ASSERT_THROW(d_solver.defineFunRec(f3, {b1}, v1), CVC5ApiException); Solver slv; Sort bvSort2 = slv.mkBitVectorSort(32); @@ -1096,16 +1096,16 @@ TEST_F(TestApiBlackSolver, defineFunRec) Term b22 = slv.mkVar(slv.getIntegerSort(), "b2"); ASSERT_NO_THROW(slv.defineFunRec("f", {}, bvSort2, v12)); ASSERT_NO_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v12)); - ASSERT_THROW(slv.defineFunRec("f", {}, bvSort, v12), CVC4ApiException); - ASSERT_THROW(slv.defineFunRec("f", {}, bvSort2, v1), CVC4ApiException); + ASSERT_THROW(slv.defineFunRec("f", {}, bvSort, v12), CVC5ApiException); + ASSERT_THROW(slv.defineFunRec("f", {}, bvSort2, v1), CVC5ApiException); ASSERT_THROW(slv.defineFunRec("ff", {b1, b22}, bvSort2, v12), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.defineFunRec("ff", {b12, b2}, bvSort2, v12), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort, v12), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v1), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackSolver, defineFunRecWrongLogic) @@ -1116,8 +1116,8 @@ TEST_F(TestApiBlackSolver, defineFunRecWrongLogic) Term b = d_solver.mkVar(bvSort, "b"); Term v = d_solver.mkConst(bvSort, "v"); Term f = d_solver.mkConst(funSort, "f"); - ASSERT_THROW(d_solver.defineFunRec("f", {}, bvSort, v), CVC4ApiException); - ASSERT_THROW(d_solver.defineFunRec(f, {b, b}, v), CVC4ApiException); + ASSERT_THROW(d_solver.defineFunRec("f", {}, bvSort, v), CVC5ApiException); + ASSERT_THROW(d_solver.defineFunRec(f, {b, b}, v), CVC5ApiException); } TEST_F(TestApiBlackSolver, defineFunRecGlobal) @@ -1166,15 +1166,15 @@ TEST_F(TestApiBlackSolver, defineFunsRec) ASSERT_NO_THROW( d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{v1, b11}, {b4}}, {v1, v2}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}), - CVC4ApiException); + CVC5ApiException); Solver slv; Sort uSort2 = slv.mkUninterpretedSort("u"); @@ -1191,19 +1191,19 @@ TEST_F(TestApiBlackSolver, defineFunsRec) ASSERT_NO_THROW( slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v22})); ASSERT_THROW(slv.defineFunsRec({f1, f22}, {{b12, b112}, {b42}}, {v12, v22}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.defineFunsRec({f12, f2}, {{b12, b112}, {b42}}, {v12, v22}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b1, b112}, {b42}}, {v12, v22}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b11}, {b42}}, {v12, v22}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b4}}, {v12, v22}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v1, v22}), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v2}), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackSolver, defineFunsRecWrongLogic) @@ -1220,7 +1220,7 @@ TEST_F(TestApiBlackSolver, defineFunsRecWrongLogic) Term f1 = d_solver.mkConst(funSort1, "f1"); Term f2 = d_solver.mkConst(funSort2, "f2"); ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b, b}, {u}}, {v1, v2}), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackSolver, defineFunsRecGlobal) @@ -1267,7 +1267,7 @@ TEST_F(TestApiBlackSolver, uFIteration) TEST_F(TestApiBlackSolver, getInfo) { ASSERT_NO_THROW(d_solver.getInfo("name")); - ASSERT_THROW(d_solver.getInfo("asdf"), CVC4ApiException); + ASSERT_THROW(d_solver.getInfo("asdf"), CVC5ApiException); } TEST_F(TestApiBlackSolver, getInterpolant) @@ -1307,7 +1307,7 @@ TEST_F(TestApiBlackSolver, getOp) Term exta = d_solver.mkTerm(ext, a); ASSERT_FALSE(a.hasOp()); - ASSERT_THROW(a.getOp(), CVC4ApiException); + ASSERT_THROW(a.getOp(), CVC5ApiException); ASSERT_TRUE(exta.hasOp()); ASSERT_EQ(exta.getOp(), ext); @@ -1339,14 +1339,14 @@ TEST_F(TestApiBlackSolver, getOp) TEST_F(TestApiBlackSolver, getOption) { ASSERT_NO_THROW(d_solver.getOption("incremental")); - ASSERT_THROW(d_solver.getOption("asdf"), CVC4ApiException); + ASSERT_THROW(d_solver.getOption("asdf"), CVC5ApiException); } TEST_F(TestApiBlackSolver, getUnsatAssumptions1) { d_solver.setOption("incremental", "false"); d_solver.checkSatAssuming(d_solver.mkFalse()); - ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException); + ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getUnsatAssumptions2) @@ -1354,7 +1354,7 @@ TEST_F(TestApiBlackSolver, getUnsatAssumptions2) d_solver.setOption("incremental", "true"); d_solver.setOption("produce-unsat-assumptions", "false"); d_solver.checkSatAssuming(d_solver.mkFalse()); - ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException); + ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getUnsatAssumptions3) @@ -1364,7 +1364,7 @@ TEST_F(TestApiBlackSolver, getUnsatAssumptions3) d_solver.checkSatAssuming(d_solver.mkFalse()); ASSERT_NO_THROW(d_solver.getUnsatAssumptions()); d_solver.checkSatAssuming(d_solver.mkTrue()); - ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException); + ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getUnsatCore1) @@ -1372,7 +1372,7 @@ TEST_F(TestApiBlackSolver, getUnsatCore1) d_solver.setOption("incremental", "false"); d_solver.assertFormula(d_solver.mkFalse()); d_solver.checkSat(); - ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException); + ASSERT_THROW(d_solver.getUnsatCore(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getUnsatCore2) @@ -1381,7 +1381,7 @@ TEST_F(TestApiBlackSolver, getUnsatCore2) d_solver.setOption("produce-unsat-cores", "false"); d_solver.assertFormula(d_solver.mkFalse()); d_solver.checkSat(); - ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException); + ASSERT_THROW(d_solver.getUnsatCore(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getUnsatCore3) @@ -1431,7 +1431,7 @@ TEST_F(TestApiBlackSolver, getValue1) Term t = d_solver.mkTrue(); d_solver.assertFormula(t); d_solver.checkSat(); - ASSERT_THROW(d_solver.getValue(t), CVC4ApiException); + ASSERT_THROW(d_solver.getValue(t), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValue2) @@ -1440,7 +1440,7 @@ TEST_F(TestApiBlackSolver, getValue2) Term t = d_solver.mkFalse(); d_solver.assertFormula(t); d_solver.checkSat(); - ASSERT_THROW(d_solver.getValue(t), CVC4ApiException); + ASSERT_THROW(d_solver.getValue(t), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValue3) @@ -1479,7 +1479,7 @@ TEST_F(TestApiBlackSolver, getValue3) ASSERT_NO_THROW(d_solver.getValue(p_f_y)); Solver slv; - ASSERT_THROW(slv.getValue(x), CVC4ApiException); + ASSERT_THROW(slv.getValue(x), CVC5ApiException); } TEST_F(TestApiBlackSolver, getQuantifierElimination) @@ -1489,9 +1489,9 @@ TEST_F(TestApiBlackSolver, getQuantifierElimination) d_solver.mkTerm(FORALL, d_solver.mkTerm(BOUND_VAR_LIST, x), d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x))); - ASSERT_THROW(d_solver.getQuantifierElimination(Term()), CVC4ApiException); + ASSERT_THROW(d_solver.getQuantifierElimination(Term()), CVC5ApiException); ASSERT_THROW(d_solver.getQuantifierElimination(Solver().mkBoolean(false)), - CVC4ApiException); + CVC5ApiException); ASSERT_NO_THROW(d_solver.getQuantifierElimination(forall)); } @@ -1503,10 +1503,10 @@ TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct) d_solver.mkTerm(BOUND_VAR_LIST, x), d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x))); ASSERT_THROW(d_solver.getQuantifierEliminationDisjunct(Term()), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW( d_solver.getQuantifierEliminationDisjunct(Solver().mkBoolean(false)), - CVC4ApiException); + CVC5ApiException); ASSERT_NO_THROW(d_solver.getQuantifierEliminationDisjunct(forall)); } @@ -1517,7 +1517,7 @@ TEST_F(TestApiBlackSolver, declareSeparationHeap) ASSERT_NO_THROW(d_solver.declareSeparationHeap(integer, integer)); // cannot declare separation logic heap more than once ASSERT_THROW(d_solver.declareSeparationHeap(integer, integer), - CVC4ApiException); + CVC5ApiException); } namespace { @@ -1547,7 +1547,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm1) d_solver.setOption("produce-models", "true"); Term t = d_solver.mkTrue(); d_solver.assertFormula(t); - ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException); + ASSERT_THROW(d_solver.getSeparationHeap(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getSeparationHeapTerm2) @@ -1556,7 +1556,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm2) d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "false"); checkSimpleSeparationConstraints(&d_solver); - ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException); + ASSERT_THROW(d_solver.getSeparationHeap(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getSeparationHeapTerm3) @@ -1567,7 +1567,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm3) Term t = d_solver.mkFalse(); d_solver.assertFormula(t); d_solver.checkSat(); - ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException); + ASSERT_THROW(d_solver.getSeparationHeap(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getSeparationHeapTerm4) @@ -1578,7 +1578,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm4) Term t = d_solver.mkTrue(); d_solver.assertFormula(t); d_solver.checkSat(); - ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException); + ASSERT_THROW(d_solver.getSeparationHeap(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getSeparationHeapTerm5) @@ -1597,7 +1597,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm1) d_solver.setOption("produce-models", "true"); Term t = d_solver.mkTrue(); d_solver.assertFormula(t); - ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException); + ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getSeparationNilTerm2) @@ -1606,7 +1606,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm2) d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "false"); checkSimpleSeparationConstraints(&d_solver); - ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException); + ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getSeparationNilTerm3) @@ -1617,7 +1617,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm3) Term t = d_solver.mkFalse(); d_solver.assertFormula(t); d_solver.checkSat(); - ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException); + ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getSeparationNilTerm4) @@ -1628,7 +1628,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm4) Term t = d_solver.mkTrue(); d_solver.assertFormula(t); d_solver.checkSat(); - ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException); + ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getSeparationNilTerm5) @@ -1644,26 +1644,26 @@ TEST_F(TestApiBlackSolver, push1) { d_solver.setOption("incremental", "true"); ASSERT_NO_THROW(d_solver.push(1)); - ASSERT_THROW(d_solver.setOption("incremental", "false"), CVC4ApiException); - ASSERT_THROW(d_solver.setOption("incremental", "true"), CVC4ApiException); + ASSERT_THROW(d_solver.setOption("incremental", "false"), CVC5ApiException); + ASSERT_THROW(d_solver.setOption("incremental", "true"), CVC5ApiException); } TEST_F(TestApiBlackSolver, push2) { d_solver.setOption("incremental", "false"); - ASSERT_THROW(d_solver.push(1), CVC4ApiException); + ASSERT_THROW(d_solver.push(1), CVC5ApiException); } TEST_F(TestApiBlackSolver, pop1) { d_solver.setOption("incremental", "false"); - ASSERT_THROW(d_solver.pop(1), CVC4ApiException); + ASSERT_THROW(d_solver.pop(1), CVC5ApiException); } TEST_F(TestApiBlackSolver, pop2) { d_solver.setOption("incremental", "true"); - ASSERT_THROW(d_solver.pop(1), CVC4ApiException); + ASSERT_THROW(d_solver.pop(1), CVC5ApiException); } TEST_F(TestApiBlackSolver, pop3) @@ -1671,7 +1671,7 @@ TEST_F(TestApiBlackSolver, pop3) d_solver.setOption("incremental", "true"); ASSERT_NO_THROW(d_solver.push(1)); ASSERT_NO_THROW(d_solver.pop(1)); - ASSERT_THROW(d_solver.pop(1), CVC4ApiException); + ASSERT_THROW(d_solver.pop(1), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModel1) @@ -1680,7 +1680,7 @@ TEST_F(TestApiBlackSolver, blockModel1) Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); - ASSERT_THROW(d_solver.blockModel(), CVC4ApiException); + ASSERT_THROW(d_solver.blockModel(), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModel2) @@ -1689,7 +1689,7 @@ TEST_F(TestApiBlackSolver, blockModel2) Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); - ASSERT_THROW(d_solver.blockModel(), CVC4ApiException); + ASSERT_THROW(d_solver.blockModel(), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModel3) @@ -1698,7 +1698,7 @@ TEST_F(TestApiBlackSolver, blockModel3) d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); - ASSERT_THROW(d_solver.blockModel(), CVC4ApiException); + ASSERT_THROW(d_solver.blockModel(), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModel4) @@ -1718,10 +1718,10 @@ TEST_F(TestApiBlackSolver, blockModelValues1) Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); - ASSERT_THROW(d_solver.blockModelValues({}), CVC4ApiException); - ASSERT_THROW(d_solver.blockModelValues({Term()}), CVC4ApiException); + ASSERT_THROW(d_solver.blockModelValues({}), CVC5ApiException); + ASSERT_THROW(d_solver.blockModelValues({Term()}), CVC5ApiException); ASSERT_THROW(d_solver.blockModelValues({Solver().mkBoolean(false)}), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModelValues2) @@ -1730,7 +1730,7 @@ TEST_F(TestApiBlackSolver, blockModelValues2) Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); - ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException); + ASSERT_THROW(d_solver.blockModelValues({x}), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModelValues3) @@ -1739,7 +1739,7 @@ TEST_F(TestApiBlackSolver, blockModelValues3) Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); - ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException); + ASSERT_THROW(d_solver.blockModelValues({x}), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModelValues4) @@ -1748,7 +1748,7 @@ TEST_F(TestApiBlackSolver, blockModelValues4) d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); - ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException); + ASSERT_THROW(d_solver.blockModelValues({x}), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModelValues5) @@ -1763,9 +1763,9 @@ TEST_F(TestApiBlackSolver, blockModelValues5) TEST_F(TestApiBlackSolver, setInfo) { - ASSERT_THROW(d_solver.setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException); - ASSERT_THROW(d_solver.setInfo("cvc2-logic", "QF_BV"), CVC4ApiException); - ASSERT_THROW(d_solver.setInfo("cvc4-logic", "asdf"), CVC4ApiException); + ASSERT_THROW(d_solver.setInfo("cvc4-lagic", "QF_BV"), CVC5ApiException); + ASSERT_THROW(d_solver.setInfo("cvc2-logic", "QF_BV"), CVC5ApiException); + ASSERT_THROW(d_solver.setInfo("cvc4-logic", "asdf"), CVC5ApiException); ASSERT_NO_THROW(d_solver.setInfo("source", "asdf")); ASSERT_NO_THROW(d_solver.setInfo("category", "asdf")); @@ -1779,17 +1779,17 @@ TEST_F(TestApiBlackSolver, setInfo) ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.0")); ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.5")); ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.6")); - ASSERT_THROW(d_solver.setInfo("smt-lib-version", ".0"), CVC4ApiException); + ASSERT_THROW(d_solver.setInfo("smt-lib-version", ".0"), CVC5ApiException); ASSERT_NO_THROW(d_solver.setInfo("status", "sat")); ASSERT_NO_THROW(d_solver.setInfo("status", "unsat")); ASSERT_NO_THROW(d_solver.setInfo("status", "unknown")); - ASSERT_THROW(d_solver.setInfo("status", "asdf"), CVC4ApiException); + ASSERT_THROW(d_solver.setInfo("status", "asdf"), CVC5ApiException); } TEST_F(TestApiBlackSolver, simplify) { - ASSERT_THROW(d_solver.simplify(Term()), CVC4ApiException); + ASSERT_THROW(d_solver.simplify(Term()), CVC5ApiException); Sort bvSort = d_solver.mkBitVectorSort(32); Sort uSort = d_solver.mkUninterpretedSort("u"); @@ -1819,7 +1819,7 @@ TEST_F(TestApiBlackSolver, simplify) ASSERT_NE(d_solver.mkTrue(), x_eq_b); ASSERT_NE(d_solver.mkTrue(), d_solver.simplify(x_eq_b)); Solver slv; - ASSERT_THROW(slv.simplify(x), CVC4ApiException); + ASSERT_THROW(slv.simplify(x), CVC5ApiException); Term i1 = d_solver.mkConst(d_solver.getIntegerSort(), "i1"); ASSERT_NO_THROW(d_solver.simplify(i1)); @@ -1865,18 +1865,18 @@ TEST_F(TestApiBlackSolver, simplify) TEST_F(TestApiBlackSolver, assertFormula) { ASSERT_NO_THROW(d_solver.assertFormula(d_solver.mkTrue())); - ASSERT_THROW(d_solver.assertFormula(Term()), CVC4ApiException); + ASSERT_THROW(d_solver.assertFormula(Term()), CVC5ApiException); Solver slv; - ASSERT_THROW(slv.assertFormula(d_solver.mkTrue()), CVC4ApiException); + ASSERT_THROW(slv.assertFormula(d_solver.mkTrue()), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkEntailed) { d_solver.setOption("incremental", "false"); ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue())); - ASSERT_THROW(d_solver.checkEntailed(d_solver.mkTrue()), CVC4ApiException); + ASSERT_THROW(d_solver.checkEntailed(d_solver.mkTrue()), CVC5ApiException); Solver slv; - ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException); + ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkEntailed1) @@ -1887,11 +1887,11 @@ TEST_F(TestApiBlackSolver, checkEntailed1) Term z = d_solver.mkTerm(AND, x, y); d_solver.setOption("incremental", "true"); ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue())); - ASSERT_THROW(d_solver.checkEntailed(Term()), CVC4ApiException); + ASSERT_THROW(d_solver.checkEntailed(Term()), CVC5ApiException); ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue())); ASSERT_NO_THROW(d_solver.checkEntailed(z)); Solver slv; - ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException); + ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkEntailed2) @@ -1936,27 +1936,27 @@ TEST_F(TestApiBlackSolver, checkEntailed2) ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTerm(DISTINCT, x, y))); ASSERT_NO_THROW(d_solver.checkEntailed( {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)})); - ASSERT_THROW(d_solver.checkEntailed(n), CVC4ApiException); + ASSERT_THROW(d_solver.checkEntailed(n), CVC5ApiException); ASSERT_THROW(d_solver.checkEntailed({n, d_solver.mkTerm(DISTINCT, x, y)}), - CVC4ApiException); + CVC5ApiException); Solver slv; - ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException); + ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkSat) { d_solver.setOption("incremental", "false"); ASSERT_NO_THROW(d_solver.checkSat()); - ASSERT_THROW(d_solver.checkSat(), CVC4ApiException); + ASSERT_THROW(d_solver.checkSat(), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkSatAssuming) { d_solver.setOption("incremental", "false"); ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue())); - ASSERT_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException); + ASSERT_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()), CVC5ApiException); Solver slv; - ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException); + ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkSatAssuming1) @@ -1967,11 +1967,11 @@ TEST_F(TestApiBlackSolver, checkSatAssuming1) Term z = d_solver.mkTerm(AND, x, y); d_solver.setOption("incremental", "true"); ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue())); - ASSERT_THROW(d_solver.checkSatAssuming(Term()), CVC4ApiException); + ASSERT_THROW(d_solver.checkSatAssuming(Term()), CVC5ApiException); ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue())); ASSERT_NO_THROW(d_solver.checkSatAssuming(z)); Solver slv; - ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException); + ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkSatAssuming2) @@ -2016,28 +2016,28 @@ TEST_F(TestApiBlackSolver, checkSatAssuming2) ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTerm(DISTINCT, x, y))); ASSERT_NO_THROW(d_solver.checkSatAssuming( {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)})); - ASSERT_THROW(d_solver.checkSatAssuming(n), CVC4ApiException); + ASSERT_THROW(d_solver.checkSatAssuming(n), CVC5ApiException); ASSERT_THROW(d_solver.checkSatAssuming({n, d_solver.mkTerm(DISTINCT, x, y)}), - CVC4ApiException); + CVC5ApiException); Solver slv; - ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException); + ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC5ApiException); } TEST_F(TestApiBlackSolver, setLogic) { ASSERT_NO_THROW(d_solver.setLogic("AUFLIRA")); - ASSERT_THROW(d_solver.setLogic("AF_BV"), CVC4ApiException); + ASSERT_THROW(d_solver.setLogic("AF_BV"), CVC5ApiException); d_solver.assertFormula(d_solver.mkTrue()); - ASSERT_THROW(d_solver.setLogic("AUFLIRA"), CVC4ApiException); + ASSERT_THROW(d_solver.setLogic("AUFLIRA"), CVC5ApiException); } TEST_F(TestApiBlackSolver, setOption) { ASSERT_NO_THROW(d_solver.setOption("bv-sat-solver", "minisat")); - ASSERT_THROW(d_solver.setOption("bv-sat-solver", "1"), CVC4ApiException); + ASSERT_THROW(d_solver.setOption("bv-sat-solver", "1"), CVC5ApiException); d_solver.assertFormula(d_solver.mkTrue()); ASSERT_THROW(d_solver.setOption("bv-sat-solver", "minisat"), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackSolver, resetAssertions) @@ -2065,11 +2065,11 @@ TEST_F(TestApiBlackSolver, mkSygusVar) ASSERT_NO_THROW(d_solver.mkSygusVar(funSort)); ASSERT_NO_THROW(d_solver.mkSygusVar(boolSort, std::string("b"))); ASSERT_NO_THROW(d_solver.mkSygusVar(funSort, "")); - ASSERT_THROW(d_solver.mkSygusVar(Sort()), CVC4ApiException); + ASSERT_THROW(d_solver.mkSygusVar(Sort()), CVC5ApiException); ASSERT_THROW(d_solver.mkSygusVar(d_solver.getNullSort(), "a"), - CVC4ApiException); + CVC5ApiException); Solver slv; - ASSERT_THROW(slv.mkSygusVar(boolSort), CVC4ApiException); + ASSERT_THROW(slv.mkSygusVar(boolSort), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkSygusGrammar) @@ -2081,16 +2081,16 @@ TEST_F(TestApiBlackSolver, mkSygusGrammar) ASSERT_NO_THROW(d_solver.mkSygusGrammar({}, {intVar})); ASSERT_NO_THROW(d_solver.mkSygusGrammar({boolVar}, {intVar})); - ASSERT_THROW(d_solver.mkSygusGrammar({}, {}), CVC4ApiException); - ASSERT_THROW(d_solver.mkSygusGrammar({}, {nullTerm}), CVC4ApiException); - ASSERT_THROW(d_solver.mkSygusGrammar({}, {boolTerm}), CVC4ApiException); - ASSERT_THROW(d_solver.mkSygusGrammar({boolTerm}, {intVar}), CVC4ApiException); + ASSERT_THROW(d_solver.mkSygusGrammar({}, {}), CVC5ApiException); + ASSERT_THROW(d_solver.mkSygusGrammar({}, {nullTerm}), CVC5ApiException); + ASSERT_THROW(d_solver.mkSygusGrammar({}, {boolTerm}), CVC5ApiException); + ASSERT_THROW(d_solver.mkSygusGrammar({boolTerm}, {intVar}), CVC5ApiException); Solver slv; Term boolVar2 = slv.mkVar(slv.getBooleanSort()); Term intVar2 = slv.mkVar(slv.getIntegerSort()); ASSERT_NO_THROW(slv.mkSygusGrammar({boolVar2}, {intVar2})); - ASSERT_THROW(slv.mkSygusGrammar({boolVar}, {intVar2}), CVC4ApiException); - ASSERT_THROW(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC4ApiException); + ASSERT_THROW(slv.mkSygusGrammar({boolVar}, {intVar2}), CVC5ApiException); + ASSERT_THROW(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC5ApiException); } TEST_F(TestApiBlackSolver, synthFun) @@ -2115,16 +2115,16 @@ TEST_F(TestApiBlackSolver, synthFun) ASSERT_NO_THROW(d_solver.synthFun("f1", {x}, boolean)); ASSERT_NO_THROW(d_solver.synthFun("f2", {x}, boolean, g1)); - ASSERT_THROW(d_solver.synthFun("f3", {nullTerm}, boolean), CVC4ApiException); - ASSERT_THROW(d_solver.synthFun("f4", {}, null), CVC4ApiException); - ASSERT_THROW(d_solver.synthFun("f6", {x}, boolean, g2), CVC4ApiException); + ASSERT_THROW(d_solver.synthFun("f3", {nullTerm}, boolean), CVC5ApiException); + ASSERT_THROW(d_solver.synthFun("f4", {}, null), CVC5ApiException); + ASSERT_THROW(d_solver.synthFun("f6", {x}, boolean, g2), CVC5ApiException); Solver slv; Term x2 = slv.mkVar(slv.getBooleanSort()); ASSERT_NO_THROW(slv.synthFun("f1", {x2}, slv.getBooleanSort())); ASSERT_THROW(slv.synthFun("", {}, d_solver.getBooleanSort()), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.synthFun("f1", {x}, d_solver.getBooleanSort()), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackSolver, synthInv) @@ -2148,8 +2148,8 @@ TEST_F(TestApiBlackSolver, synthInv) ASSERT_NO_THROW(d_solver.synthInv("i1", {x})); ASSERT_NO_THROW(d_solver.synthInv("i2", {x}, g1)); - ASSERT_THROW(d_solver.synthInv("i3", {nullTerm}), CVC4ApiException); - ASSERT_THROW(d_solver.synthInv("i4", {x}, g2), CVC4ApiException); + ASSERT_THROW(d_solver.synthInv("i3", {nullTerm}), CVC5ApiException); + ASSERT_THROW(d_solver.synthInv("i4", {x}, g2), CVC5ApiException); } TEST_F(TestApiBlackSolver, addSygusConstraint) @@ -2159,11 +2159,11 @@ TEST_F(TestApiBlackSolver, addSygusConstraint) Term intTerm = d_solver.mkInteger(1); ASSERT_NO_THROW(d_solver.addSygusConstraint(boolTerm)); - ASSERT_THROW(d_solver.addSygusConstraint(nullTerm), CVC4ApiException); - ASSERT_THROW(d_solver.addSygusConstraint(intTerm), CVC4ApiException); + ASSERT_THROW(d_solver.addSygusConstraint(nullTerm), CVC5ApiException); + ASSERT_THROW(d_solver.addSygusConstraint(intTerm), CVC5ApiException); Solver slv; - ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC4ApiException); + ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC5ApiException); } TEST_F(TestApiBlackSolver, addSygusInvConstraint) @@ -2188,36 +2188,36 @@ TEST_F(TestApiBlackSolver, addSygusInvConstraint) ASSERT_NO_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, post)); ASSERT_THROW(d_solver.addSygusInvConstraint(nullTerm, pre, trans, post), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.addSygusInvConstraint(inv, nullTerm, trans, post), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, nullTerm, post), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, nullTerm), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.addSygusInvConstraint(intTerm, pre, trans, post), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.addSygusInvConstraint(inv1, pre, trans, post), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.addSygusInvConstraint(inv, trans, trans, post), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, intTerm, post), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, pre, post), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans1, post), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans2, post), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans3, post), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, trans), - CVC4ApiException); + CVC5ApiException); Solver slv; Sort boolean2 = slv.getBooleanSort(); Sort real2 = slv.getRealSort(); @@ -2227,13 +2227,13 @@ TEST_F(TestApiBlackSolver, addSygusInvConstraint) Term post22 = slv.declareFun("post", {real2}, boolean2); ASSERT_NO_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post22)); ASSERT_THROW(slv.addSygusInvConstraint(inv, pre22, trans22, post22), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre, trans22, post22), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre22, trans, post22), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackSolver, getSynthSolution) @@ -2245,18 +2245,18 @@ TEST_F(TestApiBlackSolver, getSynthSolution) Term x = d_solver.mkBoolean(false); Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort()); - ASSERT_THROW(d_solver.getSynthSolution(f), CVC4ApiException); + ASSERT_THROW(d_solver.getSynthSolution(f), CVC5ApiException); d_solver.checkSynth(); ASSERT_NO_THROW(d_solver.getSynthSolution(f)); ASSERT_NO_THROW(d_solver.getSynthSolution(f)); - ASSERT_THROW(d_solver.getSynthSolution(nullTerm), CVC4ApiException); - ASSERT_THROW(d_solver.getSynthSolution(x), CVC4ApiException); + ASSERT_THROW(d_solver.getSynthSolution(nullTerm), CVC5ApiException); + ASSERT_THROW(d_solver.getSynthSolution(x), CVC5ApiException); Solver slv; - ASSERT_THROW(slv.getSynthSolution(f), CVC4ApiException); + ASSERT_THROW(slv.getSynthSolution(f), CVC5ApiException); } TEST_F(TestApiBlackSolver, getSynthSolutions) @@ -2268,20 +2268,20 @@ TEST_F(TestApiBlackSolver, getSynthSolutions) Term x = d_solver.mkBoolean(false); Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort()); - ASSERT_THROW(d_solver.getSynthSolutions({}), CVC4ApiException); - ASSERT_THROW(d_solver.getSynthSolutions({f}), CVC4ApiException); + ASSERT_THROW(d_solver.getSynthSolutions({}), CVC5ApiException); + ASSERT_THROW(d_solver.getSynthSolutions({f}), CVC5ApiException); d_solver.checkSynth(); ASSERT_NO_THROW(d_solver.getSynthSolutions({f})); ASSERT_NO_THROW(d_solver.getSynthSolutions({f, f})); - ASSERT_THROW(d_solver.getSynthSolutions({}), CVC4ApiException); - ASSERT_THROW(d_solver.getSynthSolutions({nullTerm}), CVC4ApiException); - ASSERT_THROW(d_solver.getSynthSolutions({x}), CVC4ApiException); + ASSERT_THROW(d_solver.getSynthSolutions({}), CVC5ApiException); + ASSERT_THROW(d_solver.getSynthSolutions({nullTerm}), CVC5ApiException); + ASSERT_THROW(d_solver.getSynthSolutions({x}), CVC5ApiException); Solver slv; - ASSERT_THROW(slv.getSynthSolutions({x}), CVC4ApiException); + ASSERT_THROW(slv.getSynthSolutions({x}), CVC5ApiException); } TEST_F(TestApiBlackSolver, tupleProject) @@ -2315,9 +2315,9 @@ TEST_F(TestApiBlackSolver, tupleProject) d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices4), tuple)); ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices5), tuple), - CVC4ApiException); + CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices6), tuple), - CVC4ApiException); + CVC5ApiException); std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2}; diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index 8338ffa2c..c2b924bfa 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -282,7 +282,7 @@ TEST_F(TestApiBlackSort, getDatatype) ASSERT_NO_THROW(dtypeSort.getDatatype()); // create bv sort, check should fail Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getDatatype(), CVC4ApiException); + ASSERT_THROW(bvSort.getDatatype(), CVC5ApiException); } TEST_F(TestApiBlackSort, datatypeSorts) @@ -291,9 +291,9 @@ TEST_F(TestApiBlackSort, datatypeSorts) Sort dtypeSort = create_datatype_sort(); Datatype dt = dtypeSort.getDatatype(); ASSERT_FALSE(dtypeSort.isConstructor()); - ASSERT_THROW(dtypeSort.getConstructorCodomainSort(), CVC4ApiException); - ASSERT_THROW(dtypeSort.getConstructorDomainSorts(), CVC4ApiException); - ASSERT_THROW(dtypeSort.getConstructorArity(), CVC4ApiException); + ASSERT_THROW(dtypeSort.getConstructorCodomainSort(), CVC5ApiException); + ASSERT_THROW(dtypeSort.getConstructorDomainSorts(), CVC5ApiException); + ASSERT_THROW(dtypeSort.getConstructorArity(), CVC5ApiException); // get constructor DatatypeConstructor dcons = dt[0]; @@ -314,8 +314,8 @@ TEST_F(TestApiBlackSort, datatypeSorts) ASSERT_EQ(isConsTerm.getSort().getTesterDomainSort(), dtypeSort); Sort booleanSort = d_solver.getBooleanSort(); ASSERT_EQ(isConsTerm.getSort().getTesterCodomainSort(), booleanSort); - ASSERT_THROW(booleanSort.getTesterDomainSort(), CVC4ApiException); - ASSERT_THROW(booleanSort.getTesterCodomainSort(), CVC4ApiException); + ASSERT_THROW(booleanSort.getTesterDomainSort(), CVC5ApiException); + ASSERT_THROW(booleanSort.getTesterCodomainSort(), CVC5ApiException); // get selector DatatypeSelector dselTail = dcons[1]; @@ -323,8 +323,8 @@ TEST_F(TestApiBlackSort, datatypeSorts) ASSERT_TRUE(tailTerm.getSort().isSelector()); ASSERT_EQ(tailTerm.getSort().getSelectorDomainSort(), dtypeSort); ASSERT_EQ(tailTerm.getSort().getSelectorCodomainSort(), dtypeSort); - ASSERT_THROW(booleanSort.getSelectorDomainSort(), CVC4ApiException); - ASSERT_THROW(booleanSort.getSelectorCodomainSort(), CVC4ApiException); + ASSERT_THROW(booleanSort.getSelectorDomainSort(), CVC5ApiException); + ASSERT_THROW(booleanSort.getSelectorCodomainSort(), CVC5ApiException); } TEST_F(TestApiBlackSort, instantiate) @@ -343,7 +343,7 @@ TEST_F(TestApiBlackSort, instantiate) Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); ASSERT_THROW( dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}), - CVC4ApiException); + CVC5ApiException); } TEST_F(TestApiBlackSort, getFunctionArity) @@ -352,7 +352,7 @@ TEST_F(TestApiBlackSort, getFunctionArity) d_solver.getIntegerSort()); ASSERT_NO_THROW(funSort.getFunctionArity()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getFunctionArity(), CVC4ApiException); + ASSERT_THROW(bvSort.getFunctionArity(), CVC5ApiException); } TEST_F(TestApiBlackSort, getFunctionDomainSorts) @@ -361,7 +361,7 @@ TEST_F(TestApiBlackSort, getFunctionDomainSorts) d_solver.getIntegerSort()); ASSERT_NO_THROW(funSort.getFunctionDomainSorts()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getFunctionDomainSorts(), CVC4ApiException); + ASSERT_THROW(bvSort.getFunctionDomainSorts(), CVC5ApiException); } TEST_F(TestApiBlackSort, getFunctionCodomainSort) @@ -370,7 +370,7 @@ TEST_F(TestApiBlackSort, getFunctionCodomainSort) d_solver.getIntegerSort()); ASSERT_NO_THROW(funSort.getFunctionCodomainSort()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getFunctionCodomainSort(), CVC4ApiException); + ASSERT_THROW(bvSort.getFunctionCodomainSort(), CVC5ApiException); } TEST_F(TestApiBlackSort, getArrayIndexSort) @@ -379,7 +379,7 @@ TEST_F(TestApiBlackSort, getArrayIndexSort) Sort indexSort = d_solver.mkBitVectorSort(32); Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); ASSERT_NO_THROW(arraySort.getArrayIndexSort()); - ASSERT_THROW(indexSort.getArrayIndexSort(), CVC4ApiException); + ASSERT_THROW(indexSort.getArrayIndexSort(), CVC5ApiException); } TEST_F(TestApiBlackSort, getArrayElementSort) @@ -388,7 +388,7 @@ TEST_F(TestApiBlackSort, getArrayElementSort) Sort indexSort = d_solver.mkBitVectorSort(32); Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); ASSERT_NO_THROW(arraySort.getArrayElementSort()); - ASSERT_THROW(indexSort.getArrayElementSort(), CVC4ApiException); + ASSERT_THROW(indexSort.getArrayElementSort(), CVC5ApiException); } TEST_F(TestApiBlackSort, getSetElementSort) @@ -398,7 +398,7 @@ TEST_F(TestApiBlackSort, getSetElementSort) Sort elementSort = setSort.getSetElementSort(); ASSERT_EQ(elementSort, d_solver.getIntegerSort()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getSetElementSort(), CVC4ApiException); + ASSERT_THROW(bvSort.getSetElementSort(), CVC5ApiException); } TEST_F(TestApiBlackSort, getBagElementSort) @@ -408,7 +408,7 @@ TEST_F(TestApiBlackSort, getBagElementSort) Sort elementSort = bagSort.getBagElementSort(); ASSERT_EQ(elementSort, d_solver.getIntegerSort()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getBagElementSort(), CVC4ApiException); + ASSERT_THROW(bvSort.getBagElementSort(), CVC5ApiException); } TEST_F(TestApiBlackSort, getSequenceElementSort) @@ -418,7 +418,7 @@ TEST_F(TestApiBlackSort, getSequenceElementSort) ASSERT_NO_THROW(seqSort.getSequenceElementSort()); Sort bvSort = d_solver.mkBitVectorSort(32); ASSERT_FALSE(bvSort.isSequence()); - ASSERT_THROW(bvSort.getSequenceElementSort(), CVC4ApiException); + ASSERT_THROW(bvSort.getSequenceElementSort(), CVC5ApiException); } TEST_F(TestApiBlackSort, getUninterpretedSortName) @@ -426,7 +426,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortName) Sort uSort = d_solver.mkUninterpretedSort("u"); ASSERT_NO_THROW(uSort.getUninterpretedSortName()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getUninterpretedSortName(), CVC4ApiException); + ASSERT_THROW(bvSort.getUninterpretedSortName(), CVC5ApiException); } TEST_F(TestApiBlackSort, isUninterpretedSortParameterized) @@ -437,7 +437,7 @@ TEST_F(TestApiBlackSort, isUninterpretedSortParameterized) Sort siSort = sSort.instantiate({uSort}); ASSERT_TRUE(siSort.isUninterpretedSortParameterized()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.isUninterpretedSortParameterized(), CVC4ApiException); + ASSERT_THROW(bvSort.isUninterpretedSortParameterized(), CVC5ApiException); } TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts) @@ -448,7 +448,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts) Sort siSort = sSort.instantiate({uSort, uSort}); ASSERT_EQ(siSort.getUninterpretedSortParamSorts().size(), 2); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException); + ASSERT_THROW(bvSort.getUninterpretedSortParamSorts(), CVC5ApiException); } TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName) @@ -456,7 +456,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName) Sort sSort = d_solver.mkSortConstructorSort("s", 2); ASSERT_NO_THROW(sSort.getSortConstructorName()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getSortConstructorName(), CVC4ApiException); + ASSERT_THROW(bvSort.getSortConstructorName(), CVC5ApiException); } TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity) @@ -464,7 +464,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity) Sort sSort = d_solver.mkSortConstructorSort("s", 2); ASSERT_NO_THROW(sSort.getSortConstructorArity()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getSortConstructorArity(), CVC4ApiException); + ASSERT_THROW(bvSort.getSortConstructorArity(), CVC5ApiException); } TEST_F(TestApiBlackSort, getBVSize) @@ -472,7 +472,7 @@ TEST_F(TestApiBlackSort, getBVSize) Sort bvSort = d_solver.mkBitVectorSort(32); ASSERT_NO_THROW(bvSort.getBVSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getBVSize(), CVC4ApiException); + ASSERT_THROW(setSort.getBVSize(), CVC5ApiException); } TEST_F(TestApiBlackSort, getFPExponentSize) @@ -482,7 +482,7 @@ TEST_F(TestApiBlackSort, getFPExponentSize) Sort fpSort = d_solver.mkFloatingPointSort(4, 8); ASSERT_NO_THROW(fpSort.getFPExponentSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPExponentSize(), CVC4ApiException); + ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException); } } @@ -493,7 +493,7 @@ TEST_F(TestApiBlackSort, getFPSignificandSize) Sort fpSort = d_solver.mkFloatingPointSort(4, 8); ASSERT_NO_THROW(fpSort.getFPSignificandSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPSignificandSize(), CVC4ApiException); + ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException); } } @@ -518,7 +518,7 @@ TEST_F(TestApiBlackSort, getDatatypeParamSorts) DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - ASSERT_THROW(dtypeSort.getDatatypeParamSorts(), CVC4ApiException); + ASSERT_THROW(dtypeSort.getDatatypeParamSorts(), CVC5ApiException); } TEST_F(TestApiBlackSort, getDatatypeArity) @@ -534,7 +534,7 @@ TEST_F(TestApiBlackSort, getDatatypeArity) ASSERT_NO_THROW(dtypeSort.getDatatypeArity()); // create bv sort, check should fail Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getDatatypeArity(), CVC4ApiException); + ASSERT_THROW(bvSort.getDatatypeArity(), CVC5ApiException); } TEST_F(TestApiBlackSort, getTupleLength) @@ -543,7 +543,7 @@ TEST_F(TestApiBlackSort, getTupleLength) {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); ASSERT_NO_THROW(tupleSort.getTupleLength()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getTupleLength(), CVC4ApiException); + ASSERT_THROW(bvSort.getTupleLength(), CVC5ApiException); } TEST_F(TestApiBlackSort, getTupleSorts) @@ -552,7 +552,7 @@ TEST_F(TestApiBlackSort, getTupleSorts) {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); ASSERT_NO_THROW(tupleSort.getTupleSorts()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getTupleSorts(), CVC4ApiException); + ASSERT_THROW(bvSort.getTupleSorts(), CVC5ApiException); } TEST_F(TestApiBlackSort, sortCompare) diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index d894f9720..9dd803c93 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -43,7 +43,7 @@ TEST_F(TestApiBlackTerm, eq) TEST_F(TestApiBlackTerm, getId) { Term n; - ASSERT_THROW(n.getId(), CVC4ApiException); + ASSERT_THROW(n.getId(), CVC5ApiException); Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x"); ASSERT_NO_THROW(x.getId()); Term y = x; @@ -62,7 +62,7 @@ TEST_F(TestApiBlackTerm, getKind) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term n; - ASSERT_THROW(n.getKind(), CVC4ApiException); + ASSERT_THROW(n.getKind(), CVC5ApiException); Term x = d_solver.mkVar(uSort, "x"); ASSERT_NO_THROW(x.getKind()); Term y = d_solver.mkVar(uSort, "y"); @@ -104,7 +104,7 @@ TEST_F(TestApiBlackTerm, getSort) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term n; - ASSERT_THROW(n.getSort(), CVC4ApiException); + ASSERT_THROW(n.getSort(), CVC5ApiException); Term x = d_solver.mkVar(bvSort, "x"); ASSERT_NO_THROW(x.getSort()); ASSERT_EQ(x.getSort(), bvSort); @@ -152,7 +152,7 @@ TEST_F(TestApiBlackTerm, getOp) Term b = d_solver.mkConst(bvsort, "b"); ASSERT_FALSE(x.hasOp()); - ASSERT_THROW(x.getOp(), CVC4ApiException); + ASSERT_THROW(x.getOp(), CVC5ApiException); Term ab = d_solver.mkTerm(SELECT, a, b); Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); @@ -169,7 +169,7 @@ TEST_F(TestApiBlackTerm, getOp) Term fx = d_solver.mkTerm(APPLY_UF, f, x); ASSERT_FALSE(f.hasOp()); - ASSERT_THROW(f.getOp(), CVC4ApiException); + ASSERT_THROW(f.getOp(), CVC5ApiException); ASSERT_TRUE(fx.hasOp()); std::vector<Term> children(fx.begin(), fx.end()); // testing rebuild from op and children @@ -228,21 +228,21 @@ TEST_F(TestApiBlackTerm, notTerm) Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); - ASSERT_THROW(Term().notTerm(), CVC4ApiException); + ASSERT_THROW(Term().notTerm(), CVC5ApiException); Term b = d_solver.mkTrue(); ASSERT_NO_THROW(b.notTerm()); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); - ASSERT_THROW(x.notTerm(), CVC4ApiException); + ASSERT_THROW(x.notTerm(), CVC5ApiException); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.notTerm(), CVC4ApiException); + ASSERT_THROW(f.notTerm(), CVC5ApiException); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.notTerm(), CVC4ApiException); + ASSERT_THROW(p.notTerm(), CVC5ApiException); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.notTerm(), CVC4ApiException); + ASSERT_THROW(zero.notTerm(), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.notTerm(), CVC4ApiException); + ASSERT_THROW(f_x.notTerm(), CVC5ApiException); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.notTerm(), CVC4ApiException); + ASSERT_THROW(sum.notTerm(), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.notTerm()); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); @@ -258,59 +258,59 @@ TEST_F(TestApiBlackTerm, andTerm) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); - ASSERT_THROW(Term().andTerm(b), CVC4ApiException); - ASSERT_THROW(b.andTerm(Term()), CVC4ApiException); + ASSERT_THROW(Term().andTerm(b), CVC5ApiException); + ASSERT_THROW(b.andTerm(Term()), CVC5ApiException); ASSERT_NO_THROW(b.andTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); - ASSERT_THROW(x.andTerm(b), CVC4ApiException); - ASSERT_THROW(x.andTerm(x), CVC4ApiException); + ASSERT_THROW(x.andTerm(b), CVC5ApiException); + ASSERT_THROW(x.andTerm(x), CVC5ApiException); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.andTerm(b), CVC4ApiException); - ASSERT_THROW(f.andTerm(x), CVC4ApiException); - ASSERT_THROW(f.andTerm(f), CVC4ApiException); + ASSERT_THROW(f.andTerm(b), CVC5ApiException); + ASSERT_THROW(f.andTerm(x), CVC5ApiException); + ASSERT_THROW(f.andTerm(f), CVC5ApiException); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.andTerm(b), CVC4ApiException); - ASSERT_THROW(p.andTerm(x), CVC4ApiException); - ASSERT_THROW(p.andTerm(f), CVC4ApiException); - ASSERT_THROW(p.andTerm(p), CVC4ApiException); + ASSERT_THROW(p.andTerm(b), CVC5ApiException); + ASSERT_THROW(p.andTerm(x), CVC5ApiException); + ASSERT_THROW(p.andTerm(f), CVC5ApiException); + ASSERT_THROW(p.andTerm(p), CVC5ApiException); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.andTerm(b), CVC4ApiException); - ASSERT_THROW(zero.andTerm(x), CVC4ApiException); - ASSERT_THROW(zero.andTerm(f), CVC4ApiException); - ASSERT_THROW(zero.andTerm(p), CVC4ApiException); - ASSERT_THROW(zero.andTerm(zero), CVC4ApiException); + ASSERT_THROW(zero.andTerm(b), CVC5ApiException); + ASSERT_THROW(zero.andTerm(x), CVC5ApiException); + ASSERT_THROW(zero.andTerm(f), CVC5ApiException); + ASSERT_THROW(zero.andTerm(p), CVC5ApiException); + ASSERT_THROW(zero.andTerm(zero), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.andTerm(b), CVC4ApiException); - ASSERT_THROW(f_x.andTerm(x), CVC4ApiException); - ASSERT_THROW(f_x.andTerm(f), CVC4ApiException); - ASSERT_THROW(f_x.andTerm(p), CVC4ApiException); - ASSERT_THROW(f_x.andTerm(zero), CVC4ApiException); - ASSERT_THROW(f_x.andTerm(f_x), CVC4ApiException); + ASSERT_THROW(f_x.andTerm(b), CVC5ApiException); + ASSERT_THROW(f_x.andTerm(x), CVC5ApiException); + ASSERT_THROW(f_x.andTerm(f), CVC5ApiException); + ASSERT_THROW(f_x.andTerm(p), CVC5ApiException); + ASSERT_THROW(f_x.andTerm(zero), CVC5ApiException); + ASSERT_THROW(f_x.andTerm(f_x), CVC5ApiException); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.andTerm(b), CVC4ApiException); - ASSERT_THROW(sum.andTerm(x), CVC4ApiException); - ASSERT_THROW(sum.andTerm(f), CVC4ApiException); - ASSERT_THROW(sum.andTerm(p), CVC4ApiException); - ASSERT_THROW(sum.andTerm(zero), CVC4ApiException); - ASSERT_THROW(sum.andTerm(f_x), CVC4ApiException); - ASSERT_THROW(sum.andTerm(sum), CVC4ApiException); + ASSERT_THROW(sum.andTerm(b), CVC5ApiException); + ASSERT_THROW(sum.andTerm(x), CVC5ApiException); + ASSERT_THROW(sum.andTerm(f), CVC5ApiException); + ASSERT_THROW(sum.andTerm(p), CVC5ApiException); + ASSERT_THROW(sum.andTerm(zero), CVC5ApiException); + ASSERT_THROW(sum.andTerm(f_x), CVC5ApiException); + ASSERT_THROW(sum.andTerm(sum), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.andTerm(b)); - ASSERT_THROW(p_0.andTerm(x), CVC4ApiException); - ASSERT_THROW(p_0.andTerm(f), CVC4ApiException); - ASSERT_THROW(p_0.andTerm(p), CVC4ApiException); - ASSERT_THROW(p_0.andTerm(zero), CVC4ApiException); - ASSERT_THROW(p_0.andTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_0.andTerm(sum), CVC4ApiException); + ASSERT_THROW(p_0.andTerm(x), CVC5ApiException); + ASSERT_THROW(p_0.andTerm(f), CVC5ApiException); + ASSERT_THROW(p_0.andTerm(p), CVC5ApiException); + ASSERT_THROW(p_0.andTerm(zero), CVC5ApiException); + ASSERT_THROW(p_0.andTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_0.andTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.andTerm(p_0)); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); ASSERT_NO_THROW(p_f_x.andTerm(b)); - ASSERT_THROW(p_f_x.andTerm(x), CVC4ApiException); - ASSERT_THROW(p_f_x.andTerm(f), CVC4ApiException); - ASSERT_THROW(p_f_x.andTerm(p), CVC4ApiException); - ASSERT_THROW(p_f_x.andTerm(zero), CVC4ApiException); - ASSERT_THROW(p_f_x.andTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_f_x.andTerm(sum), CVC4ApiException); + ASSERT_THROW(p_f_x.andTerm(x), CVC5ApiException); + ASSERT_THROW(p_f_x.andTerm(f), CVC5ApiException); + ASSERT_THROW(p_f_x.andTerm(p), CVC5ApiException); + ASSERT_THROW(p_f_x.andTerm(zero), CVC5ApiException); + ASSERT_THROW(p_f_x.andTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_f_x.andTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_f_x.andTerm(p_0)); ASSERT_NO_THROW(p_f_x.andTerm(p_f_x)); } @@ -324,59 +324,59 @@ TEST_F(TestApiBlackTerm, orTerm) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); - ASSERT_THROW(Term().orTerm(b), CVC4ApiException); - ASSERT_THROW(b.orTerm(Term()), CVC4ApiException); + ASSERT_THROW(Term().orTerm(b), CVC5ApiException); + ASSERT_THROW(b.orTerm(Term()), CVC5ApiException); ASSERT_NO_THROW(b.orTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); - ASSERT_THROW(x.orTerm(b), CVC4ApiException); - ASSERT_THROW(x.orTerm(x), CVC4ApiException); + ASSERT_THROW(x.orTerm(b), CVC5ApiException); + ASSERT_THROW(x.orTerm(x), CVC5ApiException); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.orTerm(b), CVC4ApiException); - ASSERT_THROW(f.orTerm(x), CVC4ApiException); - ASSERT_THROW(f.orTerm(f), CVC4ApiException); + ASSERT_THROW(f.orTerm(b), CVC5ApiException); + ASSERT_THROW(f.orTerm(x), CVC5ApiException); + ASSERT_THROW(f.orTerm(f), CVC5ApiException); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.orTerm(b), CVC4ApiException); - ASSERT_THROW(p.orTerm(x), CVC4ApiException); - ASSERT_THROW(p.orTerm(f), CVC4ApiException); - ASSERT_THROW(p.orTerm(p), CVC4ApiException); + ASSERT_THROW(p.orTerm(b), CVC5ApiException); + ASSERT_THROW(p.orTerm(x), CVC5ApiException); + ASSERT_THROW(p.orTerm(f), CVC5ApiException); + ASSERT_THROW(p.orTerm(p), CVC5ApiException); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.orTerm(b), CVC4ApiException); - ASSERT_THROW(zero.orTerm(x), CVC4ApiException); - ASSERT_THROW(zero.orTerm(f), CVC4ApiException); - ASSERT_THROW(zero.orTerm(p), CVC4ApiException); - ASSERT_THROW(zero.orTerm(zero), CVC4ApiException); + ASSERT_THROW(zero.orTerm(b), CVC5ApiException); + ASSERT_THROW(zero.orTerm(x), CVC5ApiException); + ASSERT_THROW(zero.orTerm(f), CVC5ApiException); + ASSERT_THROW(zero.orTerm(p), CVC5ApiException); + ASSERT_THROW(zero.orTerm(zero), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.orTerm(b), CVC4ApiException); - ASSERT_THROW(f_x.orTerm(x), CVC4ApiException); - ASSERT_THROW(f_x.orTerm(f), CVC4ApiException); - ASSERT_THROW(f_x.orTerm(p), CVC4ApiException); - ASSERT_THROW(f_x.orTerm(zero), CVC4ApiException); - ASSERT_THROW(f_x.orTerm(f_x), CVC4ApiException); + ASSERT_THROW(f_x.orTerm(b), CVC5ApiException); + ASSERT_THROW(f_x.orTerm(x), CVC5ApiException); + ASSERT_THROW(f_x.orTerm(f), CVC5ApiException); + ASSERT_THROW(f_x.orTerm(p), CVC5ApiException); + ASSERT_THROW(f_x.orTerm(zero), CVC5ApiException); + ASSERT_THROW(f_x.orTerm(f_x), CVC5ApiException); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.orTerm(b), CVC4ApiException); - ASSERT_THROW(sum.orTerm(x), CVC4ApiException); - ASSERT_THROW(sum.orTerm(f), CVC4ApiException); - ASSERT_THROW(sum.orTerm(p), CVC4ApiException); - ASSERT_THROW(sum.orTerm(zero), CVC4ApiException); - ASSERT_THROW(sum.orTerm(f_x), CVC4ApiException); - ASSERT_THROW(sum.orTerm(sum), CVC4ApiException); + ASSERT_THROW(sum.orTerm(b), CVC5ApiException); + ASSERT_THROW(sum.orTerm(x), CVC5ApiException); + ASSERT_THROW(sum.orTerm(f), CVC5ApiException); + ASSERT_THROW(sum.orTerm(p), CVC5ApiException); + ASSERT_THROW(sum.orTerm(zero), CVC5ApiException); + ASSERT_THROW(sum.orTerm(f_x), CVC5ApiException); + ASSERT_THROW(sum.orTerm(sum), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.orTerm(b)); - ASSERT_THROW(p_0.orTerm(x), CVC4ApiException); - ASSERT_THROW(p_0.orTerm(f), CVC4ApiException); - ASSERT_THROW(p_0.orTerm(p), CVC4ApiException); - ASSERT_THROW(p_0.orTerm(zero), CVC4ApiException); - ASSERT_THROW(p_0.orTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_0.orTerm(sum), CVC4ApiException); + ASSERT_THROW(p_0.orTerm(x), CVC5ApiException); + ASSERT_THROW(p_0.orTerm(f), CVC5ApiException); + ASSERT_THROW(p_0.orTerm(p), CVC5ApiException); + ASSERT_THROW(p_0.orTerm(zero), CVC5ApiException); + ASSERT_THROW(p_0.orTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_0.orTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.orTerm(p_0)); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); ASSERT_NO_THROW(p_f_x.orTerm(b)); - ASSERT_THROW(p_f_x.orTerm(x), CVC4ApiException); - ASSERT_THROW(p_f_x.orTerm(f), CVC4ApiException); - ASSERT_THROW(p_f_x.orTerm(p), CVC4ApiException); - ASSERT_THROW(p_f_x.orTerm(zero), CVC4ApiException); - ASSERT_THROW(p_f_x.orTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_f_x.orTerm(sum), CVC4ApiException); + ASSERT_THROW(p_f_x.orTerm(x), CVC5ApiException); + ASSERT_THROW(p_f_x.orTerm(f), CVC5ApiException); + ASSERT_THROW(p_f_x.orTerm(p), CVC5ApiException); + ASSERT_THROW(p_f_x.orTerm(zero), CVC5ApiException); + ASSERT_THROW(p_f_x.orTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_f_x.orTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_f_x.orTerm(p_0)); ASSERT_NO_THROW(p_f_x.orTerm(p_f_x)); } @@ -390,59 +390,59 @@ TEST_F(TestApiBlackTerm, xorTerm) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); - ASSERT_THROW(Term().xorTerm(b), CVC4ApiException); - ASSERT_THROW(b.xorTerm(Term()), CVC4ApiException); + ASSERT_THROW(Term().xorTerm(b), CVC5ApiException); + ASSERT_THROW(b.xorTerm(Term()), CVC5ApiException); ASSERT_NO_THROW(b.xorTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); - ASSERT_THROW(x.xorTerm(b), CVC4ApiException); - ASSERT_THROW(x.xorTerm(x), CVC4ApiException); + ASSERT_THROW(x.xorTerm(b), CVC5ApiException); + ASSERT_THROW(x.xorTerm(x), CVC5ApiException); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.xorTerm(b), CVC4ApiException); - ASSERT_THROW(f.xorTerm(x), CVC4ApiException); - ASSERT_THROW(f.xorTerm(f), CVC4ApiException); + ASSERT_THROW(f.xorTerm(b), CVC5ApiException); + ASSERT_THROW(f.xorTerm(x), CVC5ApiException); + ASSERT_THROW(f.xorTerm(f), CVC5ApiException); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.xorTerm(b), CVC4ApiException); - ASSERT_THROW(p.xorTerm(x), CVC4ApiException); - ASSERT_THROW(p.xorTerm(f), CVC4ApiException); - ASSERT_THROW(p.xorTerm(p), CVC4ApiException); + ASSERT_THROW(p.xorTerm(b), CVC5ApiException); + ASSERT_THROW(p.xorTerm(x), CVC5ApiException); + ASSERT_THROW(p.xorTerm(f), CVC5ApiException); + ASSERT_THROW(p.xorTerm(p), CVC5ApiException); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.xorTerm(b), CVC4ApiException); - ASSERT_THROW(zero.xorTerm(x), CVC4ApiException); - ASSERT_THROW(zero.xorTerm(f), CVC4ApiException); - ASSERT_THROW(zero.xorTerm(p), CVC4ApiException); - ASSERT_THROW(zero.xorTerm(zero), CVC4ApiException); + ASSERT_THROW(zero.xorTerm(b), CVC5ApiException); + ASSERT_THROW(zero.xorTerm(x), CVC5ApiException); + ASSERT_THROW(zero.xorTerm(f), CVC5ApiException); + ASSERT_THROW(zero.xorTerm(p), CVC5ApiException); + ASSERT_THROW(zero.xorTerm(zero), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.xorTerm(b), CVC4ApiException); - ASSERT_THROW(f_x.xorTerm(x), CVC4ApiException); - ASSERT_THROW(f_x.xorTerm(f), CVC4ApiException); - ASSERT_THROW(f_x.xorTerm(p), CVC4ApiException); - ASSERT_THROW(f_x.xorTerm(zero), CVC4ApiException); - ASSERT_THROW(f_x.xorTerm(f_x), CVC4ApiException); + ASSERT_THROW(f_x.xorTerm(b), CVC5ApiException); + ASSERT_THROW(f_x.xorTerm(x), CVC5ApiException); + ASSERT_THROW(f_x.xorTerm(f), CVC5ApiException); + ASSERT_THROW(f_x.xorTerm(p), CVC5ApiException); + ASSERT_THROW(f_x.xorTerm(zero), CVC5ApiException); + ASSERT_THROW(f_x.xorTerm(f_x), CVC5ApiException); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.xorTerm(b), CVC4ApiException); - ASSERT_THROW(sum.xorTerm(x), CVC4ApiException); - ASSERT_THROW(sum.xorTerm(f), CVC4ApiException); - ASSERT_THROW(sum.xorTerm(p), CVC4ApiException); - ASSERT_THROW(sum.xorTerm(zero), CVC4ApiException); - ASSERT_THROW(sum.xorTerm(f_x), CVC4ApiException); - ASSERT_THROW(sum.xorTerm(sum), CVC4ApiException); + ASSERT_THROW(sum.xorTerm(b), CVC5ApiException); + ASSERT_THROW(sum.xorTerm(x), CVC5ApiException); + ASSERT_THROW(sum.xorTerm(f), CVC5ApiException); + ASSERT_THROW(sum.xorTerm(p), CVC5ApiException); + ASSERT_THROW(sum.xorTerm(zero), CVC5ApiException); + ASSERT_THROW(sum.xorTerm(f_x), CVC5ApiException); + ASSERT_THROW(sum.xorTerm(sum), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.xorTerm(b)); - ASSERT_THROW(p_0.xorTerm(x), CVC4ApiException); - ASSERT_THROW(p_0.xorTerm(f), CVC4ApiException); - ASSERT_THROW(p_0.xorTerm(p), CVC4ApiException); - ASSERT_THROW(p_0.xorTerm(zero), CVC4ApiException); - ASSERT_THROW(p_0.xorTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_0.xorTerm(sum), CVC4ApiException); + ASSERT_THROW(p_0.xorTerm(x), CVC5ApiException); + ASSERT_THROW(p_0.xorTerm(f), CVC5ApiException); + ASSERT_THROW(p_0.xorTerm(p), CVC5ApiException); + ASSERT_THROW(p_0.xorTerm(zero), CVC5ApiException); + ASSERT_THROW(p_0.xorTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_0.xorTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.xorTerm(p_0)); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); ASSERT_NO_THROW(p_f_x.xorTerm(b)); - ASSERT_THROW(p_f_x.xorTerm(x), CVC4ApiException); - ASSERT_THROW(p_f_x.xorTerm(f), CVC4ApiException); - ASSERT_THROW(p_f_x.xorTerm(p), CVC4ApiException); - ASSERT_THROW(p_f_x.xorTerm(zero), CVC4ApiException); - ASSERT_THROW(p_f_x.xorTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_f_x.xorTerm(sum), CVC4ApiException); + ASSERT_THROW(p_f_x.xorTerm(x), CVC5ApiException); + ASSERT_THROW(p_f_x.xorTerm(f), CVC5ApiException); + ASSERT_THROW(p_f_x.xorTerm(p), CVC5ApiException); + ASSERT_THROW(p_f_x.xorTerm(zero), CVC5ApiException); + ASSERT_THROW(p_f_x.xorTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_f_x.xorTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_f_x.xorTerm(p_0)); ASSERT_NO_THROW(p_f_x.xorTerm(p_f_x)); } @@ -456,59 +456,59 @@ TEST_F(TestApiBlackTerm, eqTerm) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); - ASSERT_THROW(Term().eqTerm(b), CVC4ApiException); - ASSERT_THROW(b.eqTerm(Term()), CVC4ApiException); + ASSERT_THROW(Term().eqTerm(b), CVC5ApiException); + ASSERT_THROW(b.eqTerm(Term()), CVC5ApiException); ASSERT_NO_THROW(b.eqTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); - ASSERT_THROW(x.eqTerm(b), CVC4ApiException); + ASSERT_THROW(x.eqTerm(b), CVC5ApiException); ASSERT_NO_THROW(x.eqTerm(x)); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.eqTerm(b), CVC4ApiException); - ASSERT_THROW(f.eqTerm(x), CVC4ApiException); + ASSERT_THROW(f.eqTerm(b), CVC5ApiException); + ASSERT_THROW(f.eqTerm(x), CVC5ApiException); ASSERT_NO_THROW(f.eqTerm(f)); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.eqTerm(b), CVC4ApiException); - ASSERT_THROW(p.eqTerm(x), CVC4ApiException); - ASSERT_THROW(p.eqTerm(f), CVC4ApiException); + ASSERT_THROW(p.eqTerm(b), CVC5ApiException); + ASSERT_THROW(p.eqTerm(x), CVC5ApiException); + ASSERT_THROW(p.eqTerm(f), CVC5ApiException); ASSERT_NO_THROW(p.eqTerm(p)); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.eqTerm(b), CVC4ApiException); - ASSERT_THROW(zero.eqTerm(x), CVC4ApiException); - ASSERT_THROW(zero.eqTerm(f), CVC4ApiException); - ASSERT_THROW(zero.eqTerm(p), CVC4ApiException); + ASSERT_THROW(zero.eqTerm(b), CVC5ApiException); + ASSERT_THROW(zero.eqTerm(x), CVC5ApiException); + ASSERT_THROW(zero.eqTerm(f), CVC5ApiException); + ASSERT_THROW(zero.eqTerm(p), CVC5ApiException); ASSERT_NO_THROW(zero.eqTerm(zero)); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.eqTerm(b), CVC4ApiException); - ASSERT_THROW(f_x.eqTerm(x), CVC4ApiException); - ASSERT_THROW(f_x.eqTerm(f), CVC4ApiException); - ASSERT_THROW(f_x.eqTerm(p), CVC4ApiException); + ASSERT_THROW(f_x.eqTerm(b), CVC5ApiException); + ASSERT_THROW(f_x.eqTerm(x), CVC5ApiException); + ASSERT_THROW(f_x.eqTerm(f), CVC5ApiException); + ASSERT_THROW(f_x.eqTerm(p), CVC5ApiException); ASSERT_NO_THROW(f_x.eqTerm(zero)); ASSERT_NO_THROW(f_x.eqTerm(f_x)); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.eqTerm(b), CVC4ApiException); - ASSERT_THROW(sum.eqTerm(x), CVC4ApiException); - ASSERT_THROW(sum.eqTerm(f), CVC4ApiException); - ASSERT_THROW(sum.eqTerm(p), CVC4ApiException); + ASSERT_THROW(sum.eqTerm(b), CVC5ApiException); + ASSERT_THROW(sum.eqTerm(x), CVC5ApiException); + ASSERT_THROW(sum.eqTerm(f), CVC5ApiException); + ASSERT_THROW(sum.eqTerm(p), CVC5ApiException); ASSERT_NO_THROW(sum.eqTerm(zero)); ASSERT_NO_THROW(sum.eqTerm(f_x)); ASSERT_NO_THROW(sum.eqTerm(sum)); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.eqTerm(b)); - ASSERT_THROW(p_0.eqTerm(x), CVC4ApiException); - ASSERT_THROW(p_0.eqTerm(f), CVC4ApiException); - ASSERT_THROW(p_0.eqTerm(p), CVC4ApiException); - ASSERT_THROW(p_0.eqTerm(zero), CVC4ApiException); - ASSERT_THROW(p_0.eqTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_0.eqTerm(sum), CVC4ApiException); + ASSERT_THROW(p_0.eqTerm(x), CVC5ApiException); + ASSERT_THROW(p_0.eqTerm(f), CVC5ApiException); + ASSERT_THROW(p_0.eqTerm(p), CVC5ApiException); + ASSERT_THROW(p_0.eqTerm(zero), CVC5ApiException); + ASSERT_THROW(p_0.eqTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_0.eqTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.eqTerm(p_0)); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); ASSERT_NO_THROW(p_f_x.eqTerm(b)); - ASSERT_THROW(p_f_x.eqTerm(x), CVC4ApiException); - ASSERT_THROW(p_f_x.eqTerm(f), CVC4ApiException); - ASSERT_THROW(p_f_x.eqTerm(p), CVC4ApiException); - ASSERT_THROW(p_f_x.eqTerm(zero), CVC4ApiException); - ASSERT_THROW(p_f_x.eqTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_f_x.eqTerm(sum), CVC4ApiException); + ASSERT_THROW(p_f_x.eqTerm(x), CVC5ApiException); + ASSERT_THROW(p_f_x.eqTerm(f), CVC5ApiException); + ASSERT_THROW(p_f_x.eqTerm(p), CVC5ApiException); + ASSERT_THROW(p_f_x.eqTerm(zero), CVC5ApiException); + ASSERT_THROW(p_f_x.eqTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_f_x.eqTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_f_x.eqTerm(p_0)); ASSERT_NO_THROW(p_f_x.eqTerm(p_f_x)); } @@ -522,59 +522,59 @@ TEST_F(TestApiBlackTerm, impTerm) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); - ASSERT_THROW(Term().impTerm(b), CVC4ApiException); - ASSERT_THROW(b.impTerm(Term()), CVC4ApiException); + ASSERT_THROW(Term().impTerm(b), CVC5ApiException); + ASSERT_THROW(b.impTerm(Term()), CVC5ApiException); ASSERT_NO_THROW(b.impTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); - ASSERT_THROW(x.impTerm(b), CVC4ApiException); - ASSERT_THROW(x.impTerm(x), CVC4ApiException); + ASSERT_THROW(x.impTerm(b), CVC5ApiException); + ASSERT_THROW(x.impTerm(x), CVC5ApiException); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.impTerm(b), CVC4ApiException); - ASSERT_THROW(f.impTerm(x), CVC4ApiException); - ASSERT_THROW(f.impTerm(f), CVC4ApiException); + ASSERT_THROW(f.impTerm(b), CVC5ApiException); + ASSERT_THROW(f.impTerm(x), CVC5ApiException); + ASSERT_THROW(f.impTerm(f), CVC5ApiException); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.impTerm(b), CVC4ApiException); - ASSERT_THROW(p.impTerm(x), CVC4ApiException); - ASSERT_THROW(p.impTerm(f), CVC4ApiException); - ASSERT_THROW(p.impTerm(p), CVC4ApiException); + ASSERT_THROW(p.impTerm(b), CVC5ApiException); + ASSERT_THROW(p.impTerm(x), CVC5ApiException); + ASSERT_THROW(p.impTerm(f), CVC5ApiException); + ASSERT_THROW(p.impTerm(p), CVC5ApiException); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.impTerm(b), CVC4ApiException); - ASSERT_THROW(zero.impTerm(x), CVC4ApiException); - ASSERT_THROW(zero.impTerm(f), CVC4ApiException); - ASSERT_THROW(zero.impTerm(p), CVC4ApiException); - ASSERT_THROW(zero.impTerm(zero), CVC4ApiException); + ASSERT_THROW(zero.impTerm(b), CVC5ApiException); + ASSERT_THROW(zero.impTerm(x), CVC5ApiException); + ASSERT_THROW(zero.impTerm(f), CVC5ApiException); + ASSERT_THROW(zero.impTerm(p), CVC5ApiException); + ASSERT_THROW(zero.impTerm(zero), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.impTerm(b), CVC4ApiException); - ASSERT_THROW(f_x.impTerm(x), CVC4ApiException); - ASSERT_THROW(f_x.impTerm(f), CVC4ApiException); - ASSERT_THROW(f_x.impTerm(p), CVC4ApiException); - ASSERT_THROW(f_x.impTerm(zero), CVC4ApiException); - ASSERT_THROW(f_x.impTerm(f_x), CVC4ApiException); + ASSERT_THROW(f_x.impTerm(b), CVC5ApiException); + ASSERT_THROW(f_x.impTerm(x), CVC5ApiException); + ASSERT_THROW(f_x.impTerm(f), CVC5ApiException); + ASSERT_THROW(f_x.impTerm(p), CVC5ApiException); + ASSERT_THROW(f_x.impTerm(zero), CVC5ApiException); + ASSERT_THROW(f_x.impTerm(f_x), CVC5ApiException); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.impTerm(b), CVC4ApiException); - ASSERT_THROW(sum.impTerm(x), CVC4ApiException); - ASSERT_THROW(sum.impTerm(f), CVC4ApiException); - ASSERT_THROW(sum.impTerm(p), CVC4ApiException); - ASSERT_THROW(sum.impTerm(zero), CVC4ApiException); - ASSERT_THROW(sum.impTerm(f_x), CVC4ApiException); - ASSERT_THROW(sum.impTerm(sum), CVC4ApiException); + ASSERT_THROW(sum.impTerm(b), CVC5ApiException); + ASSERT_THROW(sum.impTerm(x), CVC5ApiException); + ASSERT_THROW(sum.impTerm(f), CVC5ApiException); + ASSERT_THROW(sum.impTerm(p), CVC5ApiException); + ASSERT_THROW(sum.impTerm(zero), CVC5ApiException); + ASSERT_THROW(sum.impTerm(f_x), CVC5ApiException); + ASSERT_THROW(sum.impTerm(sum), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.impTerm(b)); - ASSERT_THROW(p_0.impTerm(x), CVC4ApiException); - ASSERT_THROW(p_0.impTerm(f), CVC4ApiException); - ASSERT_THROW(p_0.impTerm(p), CVC4ApiException); - ASSERT_THROW(p_0.impTerm(zero), CVC4ApiException); - ASSERT_THROW(p_0.impTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_0.impTerm(sum), CVC4ApiException); + ASSERT_THROW(p_0.impTerm(x), CVC5ApiException); + ASSERT_THROW(p_0.impTerm(f), CVC5ApiException); + ASSERT_THROW(p_0.impTerm(p), CVC5ApiException); + ASSERT_THROW(p_0.impTerm(zero), CVC5ApiException); + ASSERT_THROW(p_0.impTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_0.impTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_0.impTerm(p_0)); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); ASSERT_NO_THROW(p_f_x.impTerm(b)); - ASSERT_THROW(p_f_x.impTerm(x), CVC4ApiException); - ASSERT_THROW(p_f_x.impTerm(f), CVC4ApiException); - ASSERT_THROW(p_f_x.impTerm(p), CVC4ApiException); - ASSERT_THROW(p_f_x.impTerm(zero), CVC4ApiException); - ASSERT_THROW(p_f_x.impTerm(f_x), CVC4ApiException); - ASSERT_THROW(p_f_x.impTerm(sum), CVC4ApiException); + ASSERT_THROW(p_f_x.impTerm(x), CVC5ApiException); + ASSERT_THROW(p_f_x.impTerm(f), CVC5ApiException); + ASSERT_THROW(p_f_x.impTerm(p), CVC5ApiException); + ASSERT_THROW(p_f_x.impTerm(zero), CVC5ApiException); + ASSERT_THROW(p_f_x.impTerm(f_x), CVC5ApiException); + ASSERT_THROW(p_f_x.impTerm(sum), CVC5ApiException); ASSERT_NO_THROW(p_f_x.impTerm(p_0)); ASSERT_NO_THROW(p_f_x.impTerm(p_f_x)); } @@ -588,39 +588,39 @@ TEST_F(TestApiBlackTerm, iteTerm) Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); - ASSERT_THROW(Term().iteTerm(b, b), CVC4ApiException); - ASSERT_THROW(b.iteTerm(Term(), b), CVC4ApiException); - ASSERT_THROW(b.iteTerm(b, Term()), CVC4ApiException); + ASSERT_THROW(Term().iteTerm(b, b), CVC5ApiException); + ASSERT_THROW(b.iteTerm(Term(), b), CVC5ApiException); + ASSERT_THROW(b.iteTerm(b, Term()), CVC5ApiException); ASSERT_NO_THROW(b.iteTerm(b, b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); ASSERT_NO_THROW(b.iteTerm(x, x)); ASSERT_NO_THROW(b.iteTerm(b, b)); - ASSERT_THROW(b.iteTerm(x, b), CVC4ApiException); - ASSERT_THROW(x.iteTerm(x, x), CVC4ApiException); - ASSERT_THROW(x.iteTerm(x, b), CVC4ApiException); + ASSERT_THROW(b.iteTerm(x, b), CVC5ApiException); + ASSERT_THROW(x.iteTerm(x, x), CVC5ApiException); + ASSERT_THROW(x.iteTerm(x, b), CVC5ApiException); Term f = d_solver.mkVar(funSort1, "f"); - ASSERT_THROW(f.iteTerm(b, b), CVC4ApiException); - ASSERT_THROW(x.iteTerm(b, x), CVC4ApiException); + ASSERT_THROW(f.iteTerm(b, b), CVC5ApiException); + ASSERT_THROW(x.iteTerm(b, x), CVC5ApiException); Term p = d_solver.mkVar(funSort2, "p"); - ASSERT_THROW(p.iteTerm(b, b), CVC4ApiException); - ASSERT_THROW(p.iteTerm(x, b), CVC4ApiException); + ASSERT_THROW(p.iteTerm(b, b), CVC5ApiException); + ASSERT_THROW(p.iteTerm(x, b), CVC5ApiException); Term zero = d_solver.mkInteger(0); - ASSERT_THROW(zero.iteTerm(x, x), CVC4ApiException); - ASSERT_THROW(zero.iteTerm(x, b), CVC4ApiException); + ASSERT_THROW(zero.iteTerm(x, x), CVC5ApiException); + ASSERT_THROW(zero.iteTerm(x, b), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); - ASSERT_THROW(f_x.iteTerm(b, b), CVC4ApiException); - ASSERT_THROW(f_x.iteTerm(b, x), CVC4ApiException); + ASSERT_THROW(f_x.iteTerm(b, b), CVC5ApiException); + ASSERT_THROW(f_x.iteTerm(b, x), CVC5ApiException); Term sum = d_solver.mkTerm(PLUS, f_x, f_x); - ASSERT_THROW(sum.iteTerm(x, x), CVC4ApiException); - ASSERT_THROW(sum.iteTerm(b, x), CVC4ApiException); + ASSERT_THROW(sum.iteTerm(x, x), CVC5ApiException); + ASSERT_THROW(sum.iteTerm(b, x), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.iteTerm(b, b)); ASSERT_NO_THROW(p_0.iteTerm(x, x)); - ASSERT_THROW(p_0.iteTerm(x, b), CVC4ApiException); + ASSERT_THROW(p_0.iteTerm(x, b), CVC5ApiException); Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x); ASSERT_NO_THROW(p_f_x.iteTerm(b, b)); ASSERT_NO_THROW(p_f_x.iteTerm(x, x)); - ASSERT_THROW(p_f_x.iteTerm(x, b), CVC4ApiException); + ASSERT_THROW(p_f_x.iteTerm(x, b), CVC5ApiException); } TEST_F(TestApiBlackTerm, termAssignment) @@ -650,7 +650,7 @@ TEST_F(TestApiBlackTerm, termChildren) ASSERT_EQ(t1[0], two); ASSERT_EQ(t1.getNumChildren(), 2); Term tnull; - ASSERT_THROW(tnull.getNumChildren(), CVC4ApiException); + ASSERT_THROW(tnull.getNumChildren(), CVC5ApiException); // apply term f(2) Sort intSort = d_solver.getIntegerSort(); @@ -661,7 +661,7 @@ TEST_F(TestApiBlackTerm, termChildren) ASSERT_EQ(t2.getNumChildren(), 2); ASSERT_EQ(t2[0], f); ASSERT_EQ(t2[1], two); - ASSERT_THROW(tnull[0], CVC4ApiException); + ASSERT_THROW(tnull[0], CVC5ApiException); } TEST_F(TestApiBlackTerm, getInteger) @@ -679,15 +679,15 @@ TEST_F(TestApiBlackTerm, getInteger) Term int11 = d_solver.mkInteger("18446744073709551616"); Term int12 = d_solver.mkInteger("-0"); - ASSERT_THROW(d_solver.mkInteger(""), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("-"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("-1-"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("0.0"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("-0.1"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("012"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("0000"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("-01"), CVC4ApiException); - ASSERT_THROW(d_solver.mkInteger("-00"), CVC4ApiException); + ASSERT_THROW(d_solver.mkInteger(""), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("-"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("-1-"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("0.0"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("-0.1"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("012"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("0000"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("-01"), CVC5ApiException); + ASSERT_THROW(d_solver.mkInteger("-00"), CVC5ApiException); ASSERT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64() && !int1.isUInt64() && int1.isInteger()); @@ -760,7 +760,7 @@ TEST_F(TestApiBlackTerm, substitute) ASSERT_EQ(xpx.substitute(x, one), onepone); ASSERT_EQ(onepone.substitute(one, x), xpx); // incorrect due to type - ASSERT_THROW(xpx.substitute(one, ttrue), CVC4ApiException); + ASSERT_THROW(xpx.substitute(one, ttrue), CVC5ApiException); // simultaneous substitution Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y"); @@ -776,28 +776,28 @@ TEST_F(TestApiBlackTerm, substitute) // incorrect substitution due to arity rs.pop_back(); - ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException); + ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException); // incorrect substitution due to types rs.push_back(ttrue); - ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException); + ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException); // null cannot substitute Term tnull; - ASSERT_THROW(tnull.substitute(one, x), CVC4ApiException); - ASSERT_THROW(xpx.substitute(tnull, x), CVC4ApiException); - ASSERT_THROW(xpx.substitute(x, tnull), CVC4ApiException); + ASSERT_THROW(tnull.substitute(one, x), CVC5ApiException); + ASSERT_THROW(xpx.substitute(tnull, x), CVC5ApiException); + ASSERT_THROW(xpx.substitute(x, tnull), CVC5ApiException); rs.pop_back(); rs.push_back(tnull); - ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException); + ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException); es.clear(); rs.clear(); es.push_back(x); rs.push_back(y); - ASSERT_THROW(tnull.substitute(es, rs), CVC4ApiException); + ASSERT_THROW(tnull.substitute(es, rs), CVC5ApiException); es.push_back(tnull); rs.push_back(one); - ASSERT_THROW(xpx.substitute(es, rs), CVC4ApiException); + ASSERT_THROW(xpx.substitute(es, rs), CVC5ApiException); } TEST_F(TestApiBlackTerm, constArray) @@ -810,7 +810,7 @@ TEST_F(TestApiBlackTerm, constArray) ASSERT_EQ(constarr.getKind(), CONST_ARRAY); ASSERT_EQ(constarr.getConstArrayBase(), one); - ASSERT_THROW(a.getConstArrayBase(), CVC4ApiException); + ASSERT_THROW(a.getConstArrayBase(), CVC5ApiException); arrsort = d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort()); @@ -837,7 +837,7 @@ TEST_F(TestApiBlackTerm, constSequenceElements) // A seq.unit app is not a constant sequence (regardless of whether it is // applied to a constant). Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1)); - ASSERT_THROW(su.getConstSequenceElements(), CVC4ApiException); + ASSERT_THROW(su.getConstSequenceElements(), CVC5ApiException); } TEST_F(TestApiBlackTerm, termScopedToString) diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp index 71ad2b1f4..8af29a8e4 100644 --- a/test/unit/main/interactive_shell_black.cpp +++ b/test/unit/main/interactive_shell_black.cpp @@ -39,7 +39,7 @@ class TestMainBlackInteractiveShell : public TestInternal d_sout.reset(new std::stringstream); d_options.set(options::in, d_sin.get()); d_options.set(options::out, d_sout.get()); - d_options.set(options::inputLanguage, language::input::LANG_CVC4); + d_options.set(options::inputLanguage, language::input::LANG_CVC); d_solver.reset(new cvc5::api::Solver(&d_options)); d_symman.reset(new SymbolManager(d_solver.get())); } diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 94eb3ae83..2309c0ac7 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -623,7 +623,7 @@ TEST_F(TestNodeBlackNode, dagifier) OR, fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy); std::stringstream sstr; - sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4); + sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC); sstr << Node::dag(false) << n; // never dagify ASSERT_EQ(sstr.str(), "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = " diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index 1e8e210ca..b6c433663 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -193,7 +193,7 @@ class TestParserBlackParser : public TestInternal class TestParserBlackCvCParser : public TestParserBlackParser { protected: - TestParserBlackCvCParser() : TestParserBlackParser(LANG_CVC4) {} + TestParserBlackCvCParser() : TestParserBlackParser(LANG_CVC) {} }; TEST_F(TestParserBlackCvCParser, good_inputs) diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp index b8c12eee2..4ed036202 100644 --- a/test/unit/parser/parser_builder_black.cpp +++ b/test/unit/parser/parser_builder_black.cpp @@ -81,7 +81,7 @@ TEST_F(TestParseBlackParserBuilder, empty_file_input) ASSERT_NE(filename, nullptr); checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), filename) - .withInputLanguage(LANG_CVC4)); + .withInputLanguage(LANG_CVC)); remove(filename); free(filename); @@ -96,7 +96,7 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input) fs.close(); checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), filename) - .withInputLanguage(LANG_CVC4)); + .withInputLanguage(LANG_CVC)); remove(filename); free(filename); @@ -105,14 +105,14 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input) TEST_F(TestParseBlackParserBuilder, empty_string_input) { checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), "foo") - .withInputLanguage(LANG_CVC4) + .withInputLanguage(LANG_CVC) .withStringInput("")); } TEST_F(TestParseBlackParserBuilder, true_string_input) { checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), "foo") - .withInputLanguage(LANG_CVC4) + .withInputLanguage(LANG_CVC) .withStringInput("TRUE")); } @@ -120,7 +120,7 @@ TEST_F(TestParseBlackParserBuilder, empty_stream_input) { std::stringstream ss("", std::ios_base::in); checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), "foo") - .withInputLanguage(LANG_CVC4) + .withInputLanguage(LANG_CVC) .withStreamInput(ss)); } @@ -128,7 +128,7 @@ TEST_F(TestParseBlackParserBuilder, true_stream_input) { std::stringstream ss("TRUE", std::ios_base::in); checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), "foo") - .withInputLanguage(LANG_CVC4) + .withInputLanguage(LANG_CVC) .withStreamInput(ss)); } diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp index d75e5881d..ccf26cbbd 100644 --- a/test/unit/theory/theory_sets_type_rules_white.cpp +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -53,7 +53,7 @@ TEST_F(TestTheoryWhiteSetsTypeRuleApi, singleton_term) // (singleton (singleton_op Int) 1) // (as emptyset (Set Real))) ASSERT_THROW(d_solver.mkTerm(UNION, singletonInt, emptyReal), - CVC4ApiException); + CVC5ApiException); // (union // (singleton (singleton_op Real) 1) // (as emptyset (Set Real))) diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp index 4a3afb281..1078a0e4e 100644 --- a/test/unit/util/boolean_simplification_black.cpp +++ b/test/unit/util/boolean_simplification_black.cpp @@ -72,7 +72,7 @@ class TestUtilBlackBooleanSimplification : public TestNode Assert(BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD >= 10); std::cout << expr::ExprSetDepth(-1) - << language::SetLanguage(language::output::LANG_CVC4); + << language::SetLanguage(language::output::LANG_CVC); } // assert equality up to commuting children diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp index 8e9595009..37937769c 100644 --- a/test/unit/util/output_black.cpp +++ b/test/unit/util/output_black.cpp @@ -69,7 +69,7 @@ TEST_F(TestUtilBlackOutput, output) Debug.on("foo"); Debug("foo") << "testing3"; - CVC4Message() << "a message"; + CVC5Message() << "a message"; Warning() << "bad warning!"; Chat() << "chatty"; Notice() << "note"; @@ -136,7 +136,7 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be) ASSERT_FALSE(Debug.isOn("foo")); ASSERT_FALSE(Trace.isOn("foo")); ASSERT_FALSE(Warning.isOn()); - ASSERT_FALSE(CVC4Message.isOn()); + ASSERT_FALSE(CVC5Message.isOn()); ASSERT_FALSE(Notice.isOn()); ASSERT_FALSE(Chat.isOn()); @@ -147,7 +147,7 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be) cout << "warning" << std::endl; Warning() << failure() << std::endl; cout << "message" << std::endl; - CVC4Message() << failure() << std::endl; + CVC5Message() << failure() << std::endl; cout << "notice" << std::endl; Notice() << failure() << std::endl; cout << "chat" << std::endl; @@ -185,7 +185,7 @@ TEST_F(TestUtilBlackOutput, simple_print) ASSERT_EQ(d_chatStream.str(), std::string()); d_chatStream.str(""); - CVC4Message() << "baz foo"; + CVC5Message() << "baz foo"; ASSERT_EQ(d_messageStream.str(), std::string()); d_messageStream.str(""); @@ -229,7 +229,7 @@ TEST_F(TestUtilBlackOutput, simple_print) ASSERT_EQ(d_chatStream.str(), std::string("baz foo")); d_chatStream.str(""); - CVC4Message() << "baz foo"; + CVC5Message() << "baz foo"; ASSERT_EQ(d_messageStream.str(), std::string("baz foo")); d_messageStream.str(""); |