diff options
Diffstat (limited to 'test')
53 files changed, 945 insertions, 320 deletions
diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index e9fd47261..4811cca1b 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -51,6 +51,7 @@ cvc5_add_api_test(smt2_compliance) cvc5_add_api_test(two_solvers) cvc5_add_api_test(issue5074) cvc5_add_api_test(issue4889) +cvc5_add_api_test(issue6111) # if we've built using libedit, then we want the interactive shell tests if (USE_EDITLINE) diff --git a/test/api/issue4889.cpp b/test/api/issue4889.cpp index f84d99f42..8e0853682 100644 --- a/test/api/issue4889.cpp +++ b/test/api/issue4889.cpp @@ -19,7 +19,6 @@ using namespace cvc5::api; int main() { -#ifdef CVC5_USE_SYMFPU Solver slv; Sort sort_int = slv.getIntegerSort(); Sort sort_array = slv.mkArraySort(sort_int, sort_int); @@ -33,6 +32,5 @@ int main() Term rem = slv.mkTerm(FLOATINGPOINT_REM, ite, const1); Term isnan = slv.mkTerm(FLOATINGPOINT_ISNAN, rem); slv.checkSatAssuming(isnan); -#endif return 0; } diff --git a/test/api/issue6111.cpp b/test/api/issue6111.cpp new file mode 100644 index 000000000..bd7be2ad0 --- /dev/null +++ b/test/api/issue6111.cpp @@ -0,0 +1,58 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Test for issue #6111 + * + */ +#include <iostream> +#include <vector> + +#include "api/cpp/cvc5.h" + +using namespace cvc5::api; +using namespace std; + +int main() +{ + Solver solver; + solver.setLogic("QF_BV"); + Sort bvsort12979 = solver.mkBitVectorSort(12979); + Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1"); + Term zero = solver.mkBitVector(bvsort12979.getBVSize(), "0", 10); + + vector<Term> args1; + args1.push_back(zero); + args1.push_back(input2_1); + Term bvult_res = solver.mkTerm(BITVECTOR_ULT, args1); + solver.assertFormula(bvult_res); + + Sort bvsort4 = solver.mkBitVectorSort(4); + Term concat_result_42 = solver.mkConst(bvsort4, "concat_result_42"); + Sort bvsort8 = solver.mkBitVectorSort(8); + Term concat_result_43 = solver.mkConst(bvsort8, "concat_result_43"); + + vector<Term> args2; + args2.push_back(concat_result_42); + args2.push_back( + solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 7, 4), {concat_result_43})); + solver.assertFormula(solver.mkTerm(EQUAL, args2)); + + vector<Term> args3; + args3.push_back(concat_result_42); + args3.push_back( + solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 3, 0), {concat_result_43})); + solver.assertFormula(solver.mkTerm(EQUAL, args3)); + + cout << solver.checkSat() << endl; + + return 0; +} diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index 9794888b2..ee58b7ad4 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -18,6 +18,7 @@ #include <sstream> #include "api/cpp/cvc5.h" +#include "options/base_options.h" #include "options/options.h" #include "options/options_public.h" #include "options/set_language.h" @@ -35,8 +36,8 @@ void testGetInfo(api::Solver* solver, const char* s); int main() { Options opts; - options::setInputLanguage(language::input::LANG_SMTLIB_V2, opts); - options::setOutputLanguage(language::output::LANG_SMTLIB_V2, opts); + opts.base.inputLanguage = language::input::LANG_SMTLIB_V2; + opts.base.outputLanguage = language::output::LANG_SMTLIB_V2; cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt index 54134b510..5b681ca36 100644 --- a/test/python/CMakeLists.txt +++ b/test/python/CMakeLists.txt @@ -33,3 +33,5 @@ cvc5_add_python_api_test(pytest_term unit/api/test_term.py) cvc5_add_python_api_test(pytest_datatype_api unit/api/test_datatype_api.py) cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py) cvc5_add_python_api_test(pytest_to_python_obj unit/api/test_to_python_obj.py) +cvc5_add_python_api_test(pytest_op unit/api/test_op.py) +cvc5_add_python_api_test(pytest_result unit/api/test_result.py) diff --git a/test/python/unit/api/test_op.py b/test/python/unit/api/test_op.py new file mode 100644 index 000000000..07a57a5c6 --- /dev/null +++ b/test/python/unit/api/test_op.py @@ -0,0 +1,178 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# Unit tests for op API. +# +# Obtained by translating test/unit/api/op_black.cpp +## + +import pytest +import pycvc5 +from pycvc5 import kinds +from pycvc5 import Sort +from pycvc5 import Op + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_get_kind(solver): + x = solver.mkOp(kinds.BVExtract, 31, 1) + x.getKind() + + +def test_is_null(solver): + x = Op(solver) + assert x.isNull() + x = solver.mkOp(kinds.BVExtract, 31, 1) + assert not x.isNull() + + +def test_op_from_kind(solver): + solver.mkOp(kinds.Plus) + with pytest.raises(RuntimeError): + solver.mkOp(kinds.BVExtract) + + +def test_get_num_indices(solver): + plus = solver.mkOp(kinds.Plus) + divisible = solver.mkOp(kinds.Divisible, 4) + bitvector_repeat = solver.mkOp(kinds.BVRepeat, 5) + bitvector_zero_extend = solver.mkOp(kinds.BVZeroExtend, 6) + bitvector_sign_extend = solver.mkOp(kinds.BVSignExtend, 7) + bitvector_rotate_left = solver.mkOp(kinds.BVRotateLeft, 8) + bitvector_rotate_right = solver.mkOp(kinds.BVRotateRight, 9) + int_to_bitvector = solver.mkOp(kinds.IntToBV, 10) + iand = solver.mkOp(kinds.Iand, 3) + floatingpoint_to_ubv = solver.mkOp(kinds.FPToUbv, 11) + floatingopint_to_sbv = solver.mkOp(kinds.FPToSbv, 13) + floatingpoint_to_fp_ieee_bitvector = solver.mkOp(kinds.FPToFpIeeeBV, 4, 25) + floatingpoint_to_fp_floatingpoint = solver.mkOp(kinds.FPToFpFP, 4, 25) + floatingpoint_to_fp_real = solver.mkOp(kinds.FPToFpReal, 4, 25) + floatingpoint_to_fp_signed_bitvector = solver.mkOp(kinds.FPToFpSignedBV, 4, + 25) + floatingpoint_to_fp_unsigned_bitvector = solver.mkOp( + kinds.FPToFpUnsignedBV, 4, 25) + floatingpoint_to_fp_generic = solver.mkOp(kinds.FPToFpGeneric, 4, 25) + regexp_loop = solver.mkOp(kinds.RegexpLoop, 2, 3) + + assert 0 == plus.getNumIndices() + assert 1 == divisible.getNumIndices() + assert 1 == bitvector_repeat.getNumIndices() + assert 1 == bitvector_zero_extend.getNumIndices() + assert 1 == bitvector_sign_extend.getNumIndices() + assert 1 == bitvector_rotate_left.getNumIndices() + assert 1 == bitvector_rotate_right.getNumIndices() + assert 1 == int_to_bitvector.getNumIndices() + assert 1 == iand.getNumIndices() + assert 1 == floatingpoint_to_ubv.getNumIndices() + assert 1 == floatingopint_to_sbv.getNumIndices() + assert 2 == floatingpoint_to_fp_ieee_bitvector.getNumIndices() + assert 2 == floatingpoint_to_fp_floatingpoint.getNumIndices() + assert 2 == floatingpoint_to_fp_real.getNumIndices() + assert 2 == floatingpoint_to_fp_signed_bitvector.getNumIndices() + assert 2 == floatingpoint_to_fp_unsigned_bitvector.getNumIndices() + assert 2 == floatingpoint_to_fp_generic.getNumIndices() + assert 2 == regexp_loop.getNumIndices() + + +def test_get_indices_string(solver): + x = Op(solver) + with pytest.raises(RuntimeError): + x.getIndices() + + divisible_ot = solver.mkOp(kinds.Divisible, 4) + assert divisible_ot.isIndexed() + divisible_idx = divisible_ot.getIndices() + assert divisible_idx == "4" + + +def test_get_indices_uint(solver): + bitvector_repeat_ot = solver.mkOp(kinds.BVRepeat, 5) + assert bitvector_repeat_ot.isIndexed() + bitvector_repeat_idx = bitvector_repeat_ot.getIndices() + assert bitvector_repeat_idx == 5 + + bitvector_zero_extend_ot = solver.mkOp(kinds.BVZeroExtend, 6) + bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIndices() + assert bitvector_zero_extend_idx == 6 + + bitvector_sign_extend_ot = solver.mkOp(kinds.BVSignExtend, 7) + bitvector_sign_extend_idx = bitvector_sign_extend_ot.getIndices() + assert bitvector_sign_extend_idx == 7 + + bitvector_rotate_left_ot = solver.mkOp(kinds.BVRotateLeft, 8) + bitvector_rotate_left_idx = bitvector_rotate_left_ot.getIndices() + assert bitvector_rotate_left_idx == 8 + + bitvector_rotate_right_ot = solver.mkOp(kinds.BVRotateRight, 9) + bitvector_rotate_right_idx = bitvector_rotate_right_ot.getIndices() + assert bitvector_rotate_right_idx == 9 + + int_to_bitvector_ot = solver.mkOp(kinds.IntToBV, 10) + int_to_bitvector_idx = int_to_bitvector_ot.getIndices() + assert int_to_bitvector_idx == 10 + + floatingpoint_to_ubv_ot = solver.mkOp(kinds.FPToUbv, 11) + floatingpoint_to_ubv_idx = floatingpoint_to_ubv_ot.getIndices() + assert floatingpoint_to_ubv_idx == 11 + + floatingpoint_to_sbv_ot = solver.mkOp(kinds.FPToSbv, 13) + floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIndices() + assert floatingpoint_to_sbv_idx == 13 + + +def test_get_indices_pair_uint(solver): + bitvector_extract_ot = solver.mkOp(kinds.BVExtract, 4, 0) + assert bitvector_extract_ot.isIndexed() + bitvector_extract_indices = bitvector_extract_ot.getIndices() + assert bitvector_extract_indices == (4, 0) + + floatingpoint_to_fp_ieee_bitvector_ot = solver.mkOp( + kinds.FPToFpIeeeBV, 4, 25) + floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot.getIndices( + ) + assert floatingpoint_to_fp_ieee_bitvector_indices == (4, 25) + + floatingpoint_to_fp_floatingpoint_ot = solver.mkOp(kinds.FPToFpFP, 4, 25) + floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot.getIndices( + ) + assert floatingpoint_to_fp_floatingpoint_indices == (4, 25) + + floatingpoint_to_fp_real_ot = solver.mkOp(kinds.FPToFpReal, 4, 25) + floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIndices() + assert floatingpoint_to_fp_real_indices == (4, 25) + + floatingpoint_to_fp_signed_bitvector_ot = solver.mkOp( + kinds.FPToFpSignedBV, 4, 25) + floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot.getIndices( + ) + assert floatingpoint_to_fp_signed_bitvector_indices == (4, 25) + + floatingpoint_to_fp_unsigned_bitvector_ot = solver.mkOp( + kinds.FPToFpUnsignedBV, 4, 25) + floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot.getIndices( + ) + assert floatingpoint_to_fp_unsigned_bitvector_indices == (4, 25) + + floatingpoint_to_fp_generic_ot = solver.mkOp(kinds.FPToFpGeneric, 4, 25) + floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot.getIndices( + ) + assert floatingpoint_to_fp_generic_indices == (4, 25) + + +def test_op_scoping_to_string(solver): + bitvector_repeat_ot = solver.mkOp(kinds.BVRepeat, 5) + op_repr = str(bitvector_repeat_ot) + assert str(bitvector_repeat_ot) == op_repr diff --git a/test/python/unit/api/test_result.py b/test/python/unit/api/test_result.py new file mode 100644 index 000000000..bd97646f9 --- /dev/null +++ b/test/python/unit/api/test_result.py @@ -0,0 +1,115 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# Unit tests for result API. +# +# Obtained by translating test/unit/api/result_black.cpp +## + +import pytest +import pycvc5 +from pycvc5 import kinds +from pycvc5 import Result +from pycvc5 import UnknownExplanation + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_is_null(solver): + res_null = Result(solver) + assert res_null.isNull() + assert not res_null.isSat() + assert not res_null.isUnsat() + assert not res_null.isSatUnknown() + assert not res_null.isEntailed() + assert not res_null.isNotEntailed() + assert not res_null.isEntailmentUnknown() + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkVar(u_sort, "x") + solver.assertFormula(x.eqTerm(x)) + res = solver.checkSat() + assert not res.isNull() + + +def test_eq(solver): + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkVar(u_sort, "x") + solver.assertFormula(x.eqTerm(x)) + res2 = solver.checkSat() + res3 = solver.checkSat() + res = res2 + assert res == res2 + assert res3 == res2 + + +def test_is_sat(solver): + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkVar(u_sort, "x") + solver.assertFormula(x.eqTerm(x)) + res = solver.checkSat() + assert res.isSat() + assert not res.isSatUnknown() + + +def test_is_unsat(solver): + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkVar(u_sort, "x") + solver.assertFormula(x.eqTerm(x).notTerm()) + res = solver.checkSat() + assert res.isUnsat() + assert not res.isSatUnknown() + + +def test_is_sat_unknown(solver): + solver.setLogic("QF_NIA") + solver.setOption("incremental", "false") + solver.setOption("solve-int-as-bv", "32") + int_sort = solver.getIntegerSort() + x = solver.mkVar(int_sort, "x") + solver.assertFormula(x.eqTerm(x).notTerm()) + res = solver.checkSat() + assert not res.isSat() + assert res.isSatUnknown() + + +def test_is_entailed(solver): + solver.setOption("incremental", "true") + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkConst(u_sort, "x") + y = solver.mkConst(u_sort, "y") + a = x.eqTerm(y).notTerm() + b = x.eqTerm(y) + solver.assertFormula(a) + entailed = solver.checkEntailed(a) + assert entailed.isEntailed() + assert not entailed.isEntailmentUnknown() + not_entailed = solver.checkEntailed(b) + assert not_entailed.isNotEntailed() + assert not not_entailed.isEntailmentUnknown() + + +def test_is_entailment_unknown(solver): + solver.setLogic("QF_NIA") + solver.setOption("incremental", "false") + solver.setOption("solve-int-as-bv", "32") + int_sort = solver.getIntegerSort() + x = solver.mkVar(int_sort, "x") + solver.assertFormula(x.eqTerm(x).notTerm()) + res = solver.checkEntailed(x.eqTerm(x)) + assert not res.isEntailed() + assert res.isEntailmentUnknown() + print(type(pycvc5.RoundTowardZero)) + print(type(pycvc5.UnknownReason)) + assert res.getUnknownExplanation() == pycvc5.UnknownReason diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index 44ce684dd..8b3ce944e 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -32,11 +32,7 @@ def test_recoverable_exception(solver): def test_supports_floating_point(solver): - if solver.supportsFloatingPoint(): - solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) - else: - with pytest.raises(RuntimeError): - solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) + solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) def test_get_boolean_sort(solver): @@ -47,6 +43,10 @@ def test_get_integer_sort(solver): solver.getIntegerSort() +def test_get_null_sort(solver): + solver.getNullSort() + + def test_get_real_sort(solver): solver.getRealSort() @@ -60,11 +60,7 @@ def test_get_string_sort(solver): def test_get_rounding_mode_sort(solver): - if solver.supportsFloatingPoint(): - solver.getRoundingModeSort() - else: - with pytest.raises(RuntimeError): - solver.getRoundingModeSort() + solver.getRoundingModeSort() def test_mk_array_sort(solver): @@ -79,10 +75,9 @@ def test_mk_array_sort(solver): solver.mkArraySort(boolSort, intSort) solver.mkArraySort(realSort, bvSort) - if (solver.supportsFloatingPoint()): - fpSort = solver.mkFloatingPointSort(3, 5) - solver.mkArraySort(fpSort, fpSort) - solver.mkArraySort(bvSort, fpSort) + fpSort = solver.mkFloatingPointSort(3, 5) + solver.mkArraySort(fpSort, fpSort) + solver.mkArraySort(bvSort, fpSort) slv = pycvc5.Solver() with pytest.raises(RuntimeError): @@ -96,15 +91,11 @@ def test_mk_bit_vector_sort(solver): def test_mk_floating_point_sort(solver): - if solver.supportsFloatingPoint(): - solver.mkFloatingPointSort(4, 8) - with pytest.raises(RuntimeError): - solver.mkFloatingPointSort(0, 8) - with pytest.raises(RuntimeError): - solver.mkFloatingPointSort(4, 0) - else: - with pytest.raises(RuntimeError): - solver.mkFloatingPointSort(4, 8) + solver.mkFloatingPointSort(4, 8) + with pytest.raises(RuntimeError): + solver.mkFloatingPointSort(0, 8) + with pytest.raises(RuntimeError): + solver.mkFloatingPointSort(4, 0) def test_mk_datatype_sort(solver): @@ -257,6 +248,15 @@ def test_mk_set_sort(solver): slv.mkSetSort(solver.mkBitVectorSort(4)) +def test_mk_bag_sort(solver): + solver.mkBagSort(solver.getBooleanSort()) + solver.mkBagSort(solver.getIntegerSort()) + solver.mkBagSort(solver.mkBitVectorSort(4)) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkBagSort(solver.mkBitVectorSort(4)) + + def test_mk_sequence_sort(solver): solver.mkSequenceSort(solver.getBooleanSort()) solver.mkSequenceSort(\ @@ -290,6 +290,42 @@ def test_mk_tuple_sort(solver): slv.mkTupleSort([solver.getIntegerSort()]) +def test_mk_bit_vector(solver): + size0 = 0 + size1 = 8 + size2 = 32 + val1 = 2 + val2 = 2 + solver.mkBitVector(size1, val1) + solver.mkBitVector(size2, val2) + solver.mkBitVector("1010", 2) + solver.mkBitVector("1010", 10) + solver.mkBitVector("1234", 10) + solver.mkBitVector("1010", 16) + solver.mkBitVector("a09f", 16) + solver.mkBitVector(8, "-127", 10) + with pytest.raises(RuntimeError): + solver.mkBitVector(size0, val1) + with pytest.raises(RuntimeError): + solver.mkBitVector(size0, val2) + with pytest.raises(RuntimeError): + solver.mkBitVector("", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector("10", 3) + with pytest.raises(RuntimeError): + solver.mkBitVector("20", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "101010101", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "-256", 10) + assert solver.mkBitVector("1010", 2) == solver.mkBitVector("10", 10) + assert solver.mkBitVector("1010", 2) == solver.mkBitVector("a", 16) + assert str(solver.mkBitVector(8, "01010101", 2)) == "#b01010101" + assert str(solver.mkBitVector(8, "F", 16)) == "#b00001111" + assert solver.mkBitVector(8, "-1", 10) ==\ + solver.mkBitVector(8, "FF", 16) + + def test_mk_var(solver): boolSort = solver.getBooleanSort() intSort = solver.getIntegerSort() @@ -313,11 +349,7 @@ def test_mk_boolean(solver): def test_mk_rounding_mode(solver): - if solver.supportsFloatingPoint(): - solver.mkRoundingMode(pycvc5.RoundTowardZero) - else: - with pytest.raises(RuntimeError): - solver.mkRoundingMode(pycvc5.RoundTowardZero) + solver.mkRoundingMode(pycvc5.RoundTowardZero) def test_mk_uninterpreted_const(solver): @@ -329,15 +361,31 @@ def test_mk_uninterpreted_const(solver): slv.mkUninterpretedConst(solver.getBooleanSort(), 1) +def test_mk_abstract_value(solver): + solver.mkAbstractValue("1") + with pytest.raises(ValueError): + solver.mkAbstractValue("0") + with pytest.raises(ValueError): + solver.mkAbstractValue("-1") + with pytest.raises(ValueError): + solver.mkAbstractValue("1.2") + with pytest.raises(ValueError): + solver.mkAbstractValue("1/2") + with pytest.raises(ValueError): + solver.mkAbstractValue("asdf") + + solver.mkAbstractValue(1) + with pytest.raises(ValueError): + solver.mkAbstractValue(-1) + with pytest.raises(ValueError): + solver.mkAbstractValue(0) + + def test_mk_floating_point(solver): t1 = solver.mkBitVector(8) t2 = solver.mkBitVector(4) t3 = solver.mkInteger(2) - if (solver.supportsFloatingPoint()): - solver.mkFloatingPoint(3, 5, t1) - else: - with pytest.raises(RuntimeError): - solver.mkFloatingPoint(3, 5, t1) + solver.mkFloatingPoint(3, 5, t1) with pytest.raises(RuntimeError): solver.mkFloatingPoint(0, 5, pycvc5.Term(solver)) @@ -350,10 +398,9 @@ def test_mk_floating_point(solver): with pytest.raises(RuntimeError): solver.mkFloatingPoint(3, 5, t2) - if (solver.supportsFloatingPoint()): - slv = pycvc5.Solver() - with pytest.raises(RuntimeError): - slv.mkFloatingPoint(3, 5, t1) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkFloatingPoint(3, 5, t1) def test_mk_empty_set(solver): @@ -367,6 +414,17 @@ def test_mk_empty_set(solver): slv.mkEmptySet(s) +def test_mk_empty_bag(solver): + slv = pycvc5.Solver() + s = solver.mkBagSort(solver.getBooleanSort()) + solver.mkEmptyBag(pycvc5.Sort(solver)) + solver.mkEmptyBag(s) + with pytest.raises(RuntimeError): + solver.mkEmptyBag(solver.getBooleanSort()) + with pytest.raises(RuntimeError): + slv.mkEmptyBag(s) + + def test_mk_empty_sequence(solver): slv = pycvc5.Solver() s = solver.mkSequenceSort(solver.getBooleanSort()) @@ -382,43 +440,50 @@ def test_mk_false(solver): def test_mk_nan(solver): - if (solver.supportsFloatingPoint()): - solver.mkNaN(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkNaN(3, 5) + solver.mkNaN(3, 5) def test_mk_neg_zero(solver): - if (solver.supportsFloatingPoint()): - solver.mkNegZero(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkNegZero(3, 5) + solver.mkNegZero(3, 5) def test_mk_neg_inf(solver): - if (solver.supportsFloatingPoint()): - solver.mkNegInf(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkNegInf(3, 5) + solver.mkNegInf(3, 5) def test_mk_pos_inf(solver): - if (solver.supportsFloatingPoint()): - solver.mkPosInf(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkPosInf(3, 5) + solver.mkPosInf(3, 5) def test_mk_pos_zero(solver): - if (solver.supportsFloatingPoint()): - solver.mkPosZero(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkPosZero(3, 5) + solver.mkPosZero(3, 5) + + +def test_mk_op(solver): + # mkOp(Kind kind, Kind k) + with pytest.raises(ValueError): + solver.mkOp(kinds.BVExtract, kinds.Equal) + + # mkOp(Kind kind, const std::string& arg) + solver.mkOp(kinds.Divisible, "2147483648") + with pytest.raises(RuntimeError): + solver.mkOp(kinds.BVExtract, "asdf") + + # mkOp(Kind kind, uint32_t arg) + solver.mkOp(kinds.Divisible, 1) + solver.mkOp(kinds.BVRotateLeft, 1) + solver.mkOp(kinds.BVRotateRight, 1) + with pytest.raises(RuntimeError): + solver.mkOp(kinds.BVExtract, 1) + + # mkOp(Kind kind, uint32_t arg1, uint32_t arg2) + solver.mkOp(kinds.BVExtract, 1, 1) + with pytest.raises(RuntimeError): + solver.mkOp(kinds.Divisible, 1, 2) + + # mkOp(Kind kind, std::vector<uint32_t> args) + args = [1, 2, 2] + solver.mkOp(kinds.TupleProject, args) def test_mk_pi(solver): @@ -568,11 +633,210 @@ def test_mk_sep_nil(solver): slv.mkSepNil(solver.getIntegerSort()) +def test_mk_string(solver): + solver.mkString("") + solver.mkString("asdfasdf") + str(solver.mkString("asdf\\nasdf")) == "\"asdf\\u{5c}nasdf\"" + str(solver.mkString("asdf\\u{005c}nasdf", True)) ==\ + "\"asdf\\u{5c}nasdf\"" + + +def test_mk_term(solver): + bv32 = solver.mkBitVectorSort(32) + a = solver.mkConst(bv32, "a") + b = solver.mkConst(bv32, "b") + v1 = [a, b] + v2 = [a, pycvc5.Term(solver)] + v3 = [a, solver.mkTrue()] + v4 = [solver.mkInteger(1), solver.mkInteger(2)] + v5 = [solver.mkInteger(1), pycvc5.Term(solver)] + v6 = [] + slv = pycvc5.Solver() + + # mkTerm(Kind kind) const + solver.mkPi() + solver.mkTerm(kinds.RegexpEmpty) + solver.mkTerm(kinds.RegexpSigma) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ConstBV) + + # mkTerm(Kind kind, Term child) const + solver.mkTerm(kinds.Not, solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Not, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Not, a) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.Not, solver.mkTrue()) + + # mkTerm(Kind kind, Term child1, Term child2) const + solver.mkTerm(kinds.Equal, a, b) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, pycvc5.Term(solver), b) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, a, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, a, solver.mkTrue()) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.Equal, a, b) + + # mkTerm(Kind kind, Term child1, Term child2, Term child3) const + solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, pycvc5.Term(solver), solver.mkTrue(), + solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, solver.mkTrue(), pycvc5.Term(solver), + solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), + pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), b) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), + solver.mkTrue()) + + # mkTerm(Kind kind, const std::vector<Term>& children) const + solver.mkTerm(kinds.Equal, v1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, v2) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, v3) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Distinct, v6) + + +def test_mk_term_from_op(solver): + bv32 = solver.mkBitVectorSort(32) + a = solver.mkConst(bv32, "a") + b = solver.mkConst(bv32, "b") + v1 = [solver.mkInteger(1), solver.mkInteger(2)] + v2 = [solver.mkInteger(1), pycvc5.Term(solver)] + v3 = [] + v4 = [solver.mkInteger(5)] + slv = pycvc5.Solver() + + # simple operator terms + opterm1 = solver.mkOp(kinds.BVExtract, 2, 1) + opterm2 = solver.mkOp(kinds.Divisible, 1) + + # list datatype + sort = solver.mkParamSort("T") + listDecl = solver.mkDatatypeDecl("paramlist", sort) + cons = solver.mkDatatypeConstructorDecl("cons") + nil = solver.mkDatatypeConstructorDecl("nil") + cons.addSelector("head", sort) + cons.addSelectorSelf("tail") + listDecl.addConstructor(cons) + listDecl.addConstructor(nil) + listSort = solver.mkDatatypeSort(listDecl) + intListSort =\ + listSort.instantiate([solver.getIntegerSort()]) + c = solver.mkConst(intListSort, "c") + lis = listSort.getDatatype() + + # list datatype constructor and selector operator terms + consTerm1 = lis.getConstructorTerm("cons") + consTerm2 = lis.getConstructor("cons").getConstructorTerm() + nilTerm1 = lis.getConstructorTerm("nil") + nilTerm2 = lis.getConstructor("nil").getConstructorTerm() + headTerm1 = lis["cons"].getSelectorTerm("head") + headTerm2 = lis["cons"].getSelector("head").getSelectorTerm() + tailTerm1 = lis["cons"].getSelectorTerm("tail") + tailTerm2 = lis["cons"]["tail"].getSelectorTerm() + + # mkTerm(Op op, Term term) const + solver.mkTerm(kinds.ApplyConstructor, nilTerm1) + solver.mkTerm(kinds.ApplyConstructor, nilTerm2) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplySelector, nilTerm1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplySelector, consTerm1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplyConstructor, consTerm2) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplySelector, headTerm1) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.ApplyConstructor, nilTerm1) + + # mkTerm(Op op, Term child) const + solver.mkTerm(opterm1, a) + solver.mkTerm(opterm2, solver.mkInteger(1)) + solver.mkTerm(kinds.ApplySelector, headTerm1, c) + solver.mkTerm(kinds.ApplySelector, tailTerm2, c) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, a) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0)) + with pytest.raises(RuntimeError): + slv.mkTerm(opterm1, a) + + # mkTerm(Op op, Term child1, Term child2) const + solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0), + solver.mkTerm(kinds.ApplyConstructor, nilTerm1)) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2)) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1, a, b) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, solver.mkInteger(1), pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, pycvc5.Term(solver), solver.mkInteger(1)) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.ApplyConstructor,\ + consTerm1,\ + solver.mkInteger(0),\ + solver.mkTerm(kinds.ApplyConstructor, nilTerm1)) + + # mkTerm(Op op, Term child1, Term child2, Term child3) const + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1, a, b, a) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(1), + pycvc5.Term(solver)) + + # mkTerm(Op op, const std::vector<Term>& children) const + solver.mkTerm(opterm2, v4) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, v1) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, v2) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, v3) + with pytest.raises(RuntimeError): + slv.mkTerm(opterm2, v4) + + def test_mk_true(solver): solver.mkTrue() solver.mkTrue() +def test_mk_tuple(solver): + solver.mkTuple([solver.mkBitVectorSort(3)], [solver.mkBitVector("101", 2)]) + solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")]) + + with pytest.raises(RuntimeError): + solver.mkTuple([], [solver.mkBitVector("101", 2)]) + with pytest.raises(RuntimeError): + solver.mkTuple([solver.mkBitVectorSort(4)], + [solver.mkBitVector("101", 2)]) + with pytest.raises(RuntimeError): + solver.mkTuple([solver.getIntegerSort()], [solver.mkReal("5.3")]) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkTuple([solver.mkBitVectorSort(3)], [slv.mkBitVector("101", 2)]) + with pytest.raises(RuntimeError): + slv.mkTuple([slv.mkBitVectorSort(3)], [solver.mkBitVector("101", 2)]) + + def test_mk_universe_set(solver): solver.mkUniverseSet(solver.getBooleanSort()) with pytest.raises(RuntimeError): diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py index 5e86382ee..def539cf4 100644 --- a/test/python/unit/api/test_sort.py +++ b/test/python/unit/api/test_sort.py @@ -89,9 +89,8 @@ def test_is_reg_exp(solver): def test_is_rounding_mode(solver): - if solver.supportsFloatingPoint(): - assert solver.getRoundingModeSort().isRoundingMode() - Sort(solver).isRoundingMode() + assert solver.getRoundingModeSort().isRoundingMode() + Sort(solver).isRoundingMode() def test_is_bit_vector(solver): @@ -100,9 +99,8 @@ def test_is_bit_vector(solver): def test_is_floating_point(solver): - if solver.supportsFloatingPoint(): - assert solver.mkFloatingPointSort(8, 24).isFloatingPoint() - Sort(solver).isFloatingPoint() + assert solver.mkFloatingPointSort(8, 24).isFloatingPoint() + Sort(solver).isFloatingPoint() def test_is_datatype(solver): @@ -447,21 +445,19 @@ def test_get_bv_size(solver): def test_get_fp_exponent_size(solver): - if solver.supportsFloatingPoint(): - fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPExponentSize() - setSort = solver.mkSetSort(solver.getIntegerSort()) - with pytest.raises(RuntimeError): - setSort.getFPExponentSize() + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPExponentSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + with pytest.raises(RuntimeError): + setSort.getFPExponentSize() def test_get_fp_significand_size(solver): - if solver.supportsFloatingPoint(): - fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPSignificandSize() - setSort = solver.mkSetSort(solver.getIntegerSort()) - with pytest.raises(RuntimeError): - setSort.getFPSignificandSize() + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPSignificandSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + with pytest.raises(RuntimeError): + setSort.getFPSignificandSize() def test_get_datatype_paramsorts(solver): diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9ad4f7e8a..6706ed4f6 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -670,6 +670,7 @@ set(regress_0_tests regress0/issue5743.smt2 regress0/issue5947.smt2 regress0/issue6605-2-abd-triv.smt2 + regress0/issue6741.smt2 regress0/ite_arith.smt2 regress0/ite_real_int_type.smtv1.smt2 regress0/ite_real_valid.smtv1.smt2 @@ -1589,6 +1590,7 @@ set(regress_1_tests regress1/fmf/issue4068-si-qf.smt2 regress1/fmf/issue4225-univ-fun.smt2 regress1/fmf/issue5738-dt-interp-finite.smt2 + regress1/fmf/issue6690-re-enum.smt2 regress1/fmf/issue916-fmf-or.smt2 regress1/fmf/jasmin-cdt-crash.smt2 regress1/fmf/loopy_coda.smt2 @@ -1612,13 +1614,10 @@ set(regress_1_tests regress1/ho/issue4065-no-rep.smt2 regress1/ho/issue4092-sinf.smt2 regress1/ho/issue4134-sinf.smt2 - regress1/ho/nested_lambdas-AGT034^2.smt2 - regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 regress1/ho/NUM638^1.smt2 regress1/ho/NUM925^1.p regress1/ho/soundness_fmf_SYO362^5-delta.p regress1/ho/store-ax-min.p - regress1/ho/SYO056^1.p regress1/hole6.cvc regress1/ite5.smt2 regress1/issue3970-nl-ext-purify.smt2 @@ -1847,6 +1846,7 @@ set(regress_1_tests regress1/quantifiers/issue5658-qe.smt2 regress1/quantifiers/issue5766-wrong-sel-trigger.smt2 regress1/quantifiers/issue5899-qe.smt2 + regress1/quantifiers/issue6699-nc-shadow.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 @@ -2630,6 +2630,10 @@ set(regression_disabled_tests regress1/fmf/ko-bound-set.cvc # results in an assertion failure (see issue #1650). regress1/ho/hoa0102.smt2 + # after disallowing solving for terms with quantifiers + regress1/ho/nested_lambdas-AGT034^2.smt2 + regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 + regress1/ho/SYO056^1.p # slow on some builds after changes to tangent planes regress1/nl/approx-sqrt-unsat.smt2 # times out after update to circuit propagator diff --git a/test/regress/README.md b/test/regress/README.md index efd79472b..ca6fc30ab 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -115,11 +115,11 @@ configurations. The `REQUIRES` directive can be used to only run a given benchmark when a feature is supported. For example: ``` -; REQUIRES: symfpu +; REQUIRES: cryptominisat ``` -This benchmark is only run when symfpu has been configured. Multiple +This benchmark is only run when CryptoMiniSat has been configured. Multiple `REQUIRES` directives are supported. For a list of features that can be listed 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. +excluded by adding the `no-` prefix, e.g. `no-cryptominisat` means that the +test is not valid for builds that include CryptoMiniSat support. diff --git a/test/regress/regress0/bv/eager-inc-cadical.smt2 b/test/regress/regress0/bv/eager-inc-cadical.smt2 index 01840dffa..34007f6aa 100644 --- a/test/regress/regress0/bv/eager-inc-cadical.smt2 +++ b/test/regress/regress0/bv/eager-inc-cadical.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: cadical ; COMMAND-LINE: --incremental --bv-sat-solver=cadical --bitblast=eager (set-logic QF_BV) (set-option :incremental true) diff --git a/test/regress/regress0/define-fun-model.smt2 b/test/regress/regress0/define-fun-model.smt2 index c6ca206fc..8f197cd04 100644 --- a/test/regress/regress0/define-fun-model.smt2 +++ b/test/regress/regress0/define-fun-model.smt2 @@ -1,8 +1,8 @@ -; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/' +; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/V/; s/_arg_[0-9]*/V/' ; EXPECT: sat ; EXPECT: (((f 4) 7)) -; EXPECT: ((g (lambda ((BOUND_VARIABLE Int)) 7))) -; EXPECT: ((f (lambda ((BOUND_VARIABLE Int)) 7))) +; EXPECT: ((g (lambda ((V Int)) 7))) +; EXPECT: ((f (lambda ((V Int)) 7))) (set-logic UFLIA) (set-option :produce-models true) (define-fun f ((x Int)) Int 7) diff --git a/test/regress/regress0/fp/abs-unsound.smt2 b/test/regress/regress0/fp/abs-unsound.smt2 index b5aa0452e..ae7117047 100644 --- a/test/regress/regress0/fp/abs-unsound.smt2 +++ b/test/regress/regress0/fp/abs-unsound.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: sat (set-logic QF_FP) diff --git a/test/regress/regress0/fp/abs-unsound2.smt2 b/test/regress/regress0/fp/abs-unsound2.smt2 index ad603f8c9..3040f9ba9 100644 --- a/test/regress/regress0/fp/abs-unsound2.smt2 +++ b/test/regress/regress0/fp/abs-unsound2.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: unsat (set-logic QF_FP) diff --git a/test/regress/regress0/fp/down-cast-RNA.smt2 b/test/regress/regress0/fp/down-cast-RNA.smt2 index dc99ff144..62314f284 100644 --- a/test/regress/regress0/fp/down-cast-RNA.smt2 +++ b/test/regress/regress0/fp/down-cast-RNA.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: unsat diff --git a/test/regress/regress0/fp/ext-rew-test.smt2 b/test/regress/regress0/fp/ext-rew-test.smt2 index 726487e18..3fb3a9e53 100644 --- a/test/regress/regress0/fp/ext-rew-test.smt2 +++ b/test/regress/regress0/fp/ext-rew-test.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg ; EXPECT: unsat (set-info :smt-lib-version 2.6) diff --git a/test/regress/regress0/fp/from_sbv.smt2 b/test/regress/regress0/fp/from_sbv.smt2 index 3211339d6..226d6589c 100644 --- a/test/regress/regress0/fp/from_sbv.smt2 +++ b/test/regress/regress0/fp/from_sbv.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: unsat (set-logic QF_BVFP) diff --git a/test/regress/regress0/fp/from_ubv.smt2 b/test/regress/regress0/fp/from_ubv.smt2 index c02f8d304..6939e478a 100644 --- a/test/regress/regress0/fp/from_ubv.smt2 +++ b/test/regress/regress0/fp/from_ubv.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: unsat (set-logic QF_FP) (declare-const r RoundingMode) diff --git a/test/regress/regress0/fp/issue-5524.smt2 b/test/regress/regress0/fp/issue-5524.smt2 index 8c361163c..741d77a19 100644 --- a/test/regress/regress0/fp/issue-5524.smt2 +++ b/test/regress/regress0/fp/issue-5524.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: unsat (set-logic QF_FP) (declare-fun fpv5 () Float32) diff --git a/test/regress/regress0/fp/issue3536.smt2 b/test/regress/regress0/fp/issue3536.smt2 index 68a17347e..6a58b371f 100644 --- a/test/regress/regress0/fp/issue3536.smt2 +++ b/test/regress/regress0/fp/issue3536.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_FP) diff --git a/test/regress/regress0/fp/issue3582.smt2 b/test/regress/regress0/fp/issue3582.smt2 index 2de76b680..c06cdb110 100644 --- a/test/regress/regress0/fp/issue3582.smt2 +++ b/test/regress/regress0/fp/issue3582.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: unsat (set-logic QF_FP) (declare-fun bv () (_ BitVec 1)) diff --git a/test/regress/regress0/fp/issue3619.smt2 b/test/regress/regress0/fp/issue3619.smt2 index 3e0858035..ab3c781bb 100644 --- a/test/regress/regress0/fp/issue3619.smt2 +++ b/test/regress/regress0/fp/issue3619.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_FPLRA) diff --git a/test/regress/regress0/fp/issue4277-assign-func.smt2 b/test/regress/regress0/fp/issue4277-assign-func.smt2 index c42bad235..d1fbc73d2 100644 --- a/test/regress/regress0/fp/issue4277-assign-func.smt2 +++ b/test/regress/regress0/fp/issue4277-assign-func.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: -q ; EXPECT: sat -; REQUIRES: symfpu (set-logic HO_ALL) (set-option :assign-function-values false) (set-info :status sat) diff --git a/test/regress/regress0/fp/issue5511.smt2 b/test/regress/regress0/fp/issue5511.smt2 index d4393486c..911db54ee 100644 --- a/test/regress/regress0/fp/issue5511.smt2 +++ b/test/regress/regress0/fp/issue5511.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: sat (set-logic QF_FP) (declare-fun a () (_ FloatingPoint 53 11)) diff --git a/test/regress/regress0/fp/issue5734.smt2 b/test/regress/regress0/fp/issue5734.smt2 index 2ad9ac921..d66e6aec7 100644 --- a/test/regress/regress0/fp/issue5734.smt2 +++ b/test/regress/regress0/fp/issue5734.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: sat (set-logic QF_FP) (declare-fun a () RoundingMode) diff --git a/test/regress/regress0/fp/issue6164.smt2 b/test/regress/regress0/fp/issue6164.smt2 index 056a98afc..3ec9f1594 100644 --- a/test/regress/regress0/fp/issue6164.smt2 +++ b/test/regress/regress0/fp/issue6164.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: sat ; EXPECT: ((((_ to_fp 5 11) roundNearestTiesToAway (/ 1 10)) (fp #b0 #b01011 #b1001100110))) (set-logic ALL) diff --git a/test/regress/regress0/fp/rti_3_5_bug.smt2 b/test/regress/regress0/fp/rti_3_5_bug.smt2 index 2c837b415..724e08b8c 100644 --- a/test/regress/regress0/fp/rti_3_5_bug.smt2 +++ b/test/regress/regress0/fp/rti_3_5_bug.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu
; COMMAND-LINE: --fp-exp
; EXPECT: unsat
diff --git a/test/regress/regress0/fp/simple.smt2 b/test/regress/regress0/fp/simple.smt2 index 0b4a11f08..754186943 100644 --- a/test/regress/regress0/fp/simple.smt2 +++ b/test/regress/regress0/fp/simple.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: unsat (set-logic QF_FP) (declare-const x Float32) diff --git a/test/regress/regress0/fp/wrong-model.smt2 b/test/regress/regress0/fp/wrong-model.smt2 index 7694d8a35..298c21b18 100644 --- a/test/regress/regress0/fp/wrong-model.smt2 +++ b/test/regress/regress0/fp/wrong-model.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: sat diff --git a/test/regress/regress0/issue5370.smt2 b/test/regress/regress0/issue5370.smt2 index 848567e2c..971602e14 100644 --- a/test/regress/regress0/issue5370.smt2 +++ b/test/regress/regress0/issue5370.smt2 @@ -1,5 +1,4 @@ ; COMMAND-LINE: --bv-to-bool -; REQUIRES: symfpu (set-logic ALL) (set-info :status sat) (declare-fun c () (Array (_ BitVec 2) (_ BitVec 1))) diff --git a/test/regress/regress0/issue6741.smt2 b/test/regress/regress0/issue6741.smt2 new file mode 100644 index 000000000..0fbf4edeb --- /dev/null +++ b/test/regress/regress0/issue6741.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --bv-solver=bitblast --bitblast=eager --check-models +(set-logic QF_BV) +(set-info :status sat) +(declare-fun x () (_ BitVec 1)) +(declare-fun y () (_ BitVec 1)) +(assert (= y (ite (= x (_ bv1 1)) (_ bv1 1) (_ bv0 1)))) +(assert (= y (_ bv1 1))) +(check-sat) diff --git a/test/regress/regress0/nl/issue3003.smt2 b/test/regress/regress0/nl/issue3003.smt2 index f28a1fd77..3247a941a 100644 --- a/test/regress/regress0/nl/issue3003.smt2 +++ b/test/regress/regress0/nl/issue3003.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-ext=none +; COMMAND-LINE: --nl-ext=none --no-check-models ; EXPECT: sat (set-logic QF_NRA) (set-info :status sat) diff --git a/test/regress/regress0/parser/to_fp.smt2 b/test/regress/regress0/parser/to_fp.smt2 index 277209ff8..1cd83816a 100644 --- a/test/regress/regress0/parser/to_fp.smt2 +++ b/test/regress/regress0/parser/to_fp.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --strict-parsing -q ; EXPECT: sat (set-logic QF_FP) diff --git a/test/regress/regress1/fmf/issue6690-re-enum.smt2 b/test/regress/regress1/fmf/issue6690-re-enum.smt2 new file mode 100644 index 000000000..35c8eabc7 --- /dev/null +++ b/test/regress/regress1/fmf/issue6690-re-enum.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(set-option :finite-model-find true) +(assert (forall ((a String)) (forall ((b String)) (str.in_re a (re.++ re.allchar (str.to_re b)))))) +(check-sat) diff --git a/test/regress/regress1/fp/rti_3_5_bug_report.smt2 b/test/regress/regress1/fp/rti_3_5_bug_report.smt2 index 3e94e6e05..6c0b68c95 100644 --- a/test/regress/regress1/fp/rti_3_5_bug_report.smt2 +++ b/test/regress/regress1/fp/rti_3_5_bug_report.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: unsat diff --git a/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 b/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 index 1ee8e6c11..3ab7495ea 100644 --- a/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 +++ b/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu (set-info :smt-lib-version 2.6) (set-logic FP) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 index 796d7e753..d30bd563d 100644 --- a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 +++ b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 @@ -1,5 +1,4 @@ ; COMMAND-LINE: --no-jh-rlv-order -; REQUIRES: symfpu ; EXPECT: unsat (set-logic AUFBVFPDTNIRA) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/issue6699-nc-shadow.smt2 b/test/regress/regress1/quantifiers/issue6699-nc-shadow.smt2 new file mode 100644 index 000000000..e1e0cdbe8 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6699-nc-shadow.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: -i +; EXPECT: unsat +(set-logic ALL) +(declare-fun v1 () Bool) +(declare-fun v4 () Bool) +(declare-fun v7 () Bool) +(assert (distinct v7 v1 (and v4 (exists ((q1 Int)) (= (= 0 q1) (and v7 v1)))))) +(push) +(check-sat) diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy index 30828ca76..2970fd0de 100644 --- a/test/regress/regress1/rr-verify/fp-arith.sy +++ b/test/regress/regress1/rr-verify/fp-arith.sy @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)' diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy index 6704198c3..e4b3a0fac 100644 --- a/test/regress/regress1/rr-verify/fp-bool.sy +++ b/test/regress/regress1/rr-verify/fp-bool.sy @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)' diff --git a/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy index fa8bdc2d7..385ade07f 100644 --- a/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy +++ b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) diff --git a/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 index c674c4039..4648c327a 100644 --- a/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 +++ b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --decision=internal -q ; COMMAND-LINE: --decision=justification -q ; EXPECT: sat diff --git a/test/regress/regress2/sygus/min_IC_1.sy b/test/regress/regress2/sygus/min_IC_1.sy index c0cae0025..8c0e2d82b 100644 --- a/test/regress/regress2/sygus/min_IC_1.sy +++ b/test/regress/regress2/sygus/min_IC_1.sy @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --fp-exp (set-logic ALL) diff --git a/test/unit/api/java/cvc5/GrammarTest.java b/test/unit/api/java/cvc5/GrammarTest.java new file mode 100644 index 000000000..76a80f55e --- /dev/null +++ b/test/unit/api/java/cvc5/GrammarTest.java @@ -0,0 +1,137 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Abdalrhman Mohamed, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Black box testing of the guards of the Java API functions. + */ + +package cvc5; + +import static cvc5.Kind.*; +import static org.junit.jupiter.api.Assertions.*; + +import java.util.Arrays; +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +class GrammarTest { + private Solver d_solver; + + @BeforeEach + void setUp() { + d_solver = new Solver(); + } + + @Test + void addRule() { + Sort bool = d_solver.getBooleanSort(); + Sort integer = d_solver.getIntegerSort(); + + Term nullTerm = d_solver.getNullTerm(); + Term start = d_solver.mkVar(bool); + Term nts = d_solver.mkVar(bool); + + Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + + assertDoesNotThrow(() -> g.addRule(start, d_solver.mkBoolean(false))); + + assertThrows(CVC5ApiException.class, + () -> g.addRule(nullTerm, d_solver.mkBoolean(false))); + assertThrows(CVC5ApiException.class, () -> g.addRule(start, nullTerm)); + assertThrows(CVC5ApiException.class, + () -> g.addRule(nts, d_solver.mkBoolean(false))); + assertThrows( + CVC5ApiException.class, () -> g.addRule(start, d_solver.mkInteger(0))); + assertThrows(CVC5ApiException.class, () -> g.addRule(start, nts)); + + d_solver.synthFun("f", new Term[] {}, bool, g); + + assertThrows(CVC5ApiException.class, + () -> g.addRule(start, d_solver.mkBoolean(false))); + } + + @Test + void addRules() { + Sort bool = d_solver.getBooleanSort(); + Sort integer = d_solver.getIntegerSort(); + + Term nullTerm = d_solver.getNullTerm(); + Term start = d_solver.mkVar(bool); + Term nts = d_solver.mkVar(bool); + + Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + + assertDoesNotThrow( + () -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)})); + + assertThrows(CVC5ApiException.class, + () -> g.addRules(nullTerm, new Term[] {d_solver.mkBoolean(false)})); + assertThrows( + CVC5ApiException.class, () -> g.addRules(start, new Term[] {nullTerm})); + assertThrows(CVC5ApiException.class, + () -> g.addRules(nts, new Term[] {d_solver.mkBoolean(false)})); + assertThrows(CVC5ApiException.class, + () -> g.addRules(start, new Term[] {d_solver.mkInteger(0)})); + assertThrows( + CVC5ApiException.class, () -> g.addRules(start, new Term[] {nts})); + + d_solver.synthFun("f", new Term[] {}, bool, g); + + assertThrows(CVC5ApiException.class, + () -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)})); + } + + @Test + void addAnyConstant() { + Sort bool = d_solver.getBooleanSort(); + + Term nullTerm = d_solver.getNullTerm(); + Term start = d_solver.mkVar(bool); + Term nts = d_solver.mkVar(bool); + + Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + + assertDoesNotThrow(() -> g.addAnyConstant(start)); + assertDoesNotThrow(() -> g.addAnyConstant(start)); + + assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(nullTerm)); + assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(nts)); + + d_solver.synthFun("f", new Term[] {}, bool, g); + + assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(start)); + } + + @Test + void addAnyVariable() { + Sort bool = d_solver.getBooleanSort(); + + Term nullTerm = d_solver.getNullTerm(); + Term x = d_solver.mkVar(bool); + Term start = d_solver.mkVar(bool); + Term nts = d_solver.mkVar(bool); + + Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start}); + Grammar g2 = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + + assertDoesNotThrow(() -> g1.addAnyVariable(start)); + assertDoesNotThrow(() -> g1.addAnyVariable(start)); + assertDoesNotThrow(() -> g2.addAnyVariable(start)); + + assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(nullTerm)); + assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(nts)); + + d_solver.synthFun("f", new Term[] {}, bool, g1); + + assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(start)); + } +} diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 018207293..20e0977f8 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -35,15 +35,7 @@ TEST_F(TestApiBlackSolver, recoverableException) TEST_F(TestApiBlackSolver, supportsFloatingPoint) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN)); - } - else - { - ASSERT_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN), - CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN)); } TEST_F(TestApiBlackSolver, getBooleanSort) @@ -78,14 +70,7 @@ TEST_F(TestApiBlackSolver, getStringSort) TEST_F(TestApiBlackSolver, getRoundingModeSort) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.getRoundingModeSort()); - } - else - { - ASSERT_THROW(d_solver.getRoundingModeSort(), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.getRoundingModeSort()); } TEST_F(TestApiBlackSolver, mkArraySort) @@ -101,12 +86,9 @@ TEST_F(TestApiBlackSolver, mkArraySort) ASSERT_NO_THROW(d_solver.mkArraySort(boolSort, intSort)); ASSERT_NO_THROW(d_solver.mkArraySort(realSort, bvSort)); - if (d_solver.supportsFloatingPoint()) - { - Sort fpSort = d_solver.mkFloatingPointSort(3, 5); - ASSERT_NO_THROW(d_solver.mkArraySort(fpSort, fpSort)); - ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, fpSort)); - } + Sort fpSort = d_solver.mkFloatingPointSort(3, 5); + ASSERT_NO_THROW(d_solver.mkArraySort(fpSort, fpSort)); + ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, fpSort)); Solver slv; ASSERT_THROW(slv.mkArraySort(boolSort, boolSort), CVC5ApiException); @@ -120,16 +102,9 @@ TEST_F(TestApiBlackSolver, mkBitVectorSort) TEST_F(TestApiBlackSolver, mkFloatingPointSort) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8)); - ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC5ApiException); - ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC5ApiException); - } - else - { - ASSERT_THROW(d_solver.mkFloatingPointSort(4, 8), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8)); + ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC5ApiException); + ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkDatatypeSort) @@ -377,15 +352,7 @@ TEST_F(TestApiBlackSolver, mkBoolean) TEST_F(TestApiBlackSolver, mkRoundingMode) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); - } - else - { - ASSERT_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO), - CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); } TEST_F(TestApiBlackSolver, mkUninterpretedConst) @@ -420,25 +387,15 @@ TEST_F(TestApiBlackSolver, mkFloatingPoint) Term t1 = d_solver.mkBitVector(8); Term t2 = d_solver.mkBitVector(4); Term t3 = d_solver.mkInteger(2); - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkFloatingPoint(3, 5, t1)); - } - else - { - ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t1), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkFloatingPoint(3, 5, t1)); 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), CVC5ApiException); - } + Solver slv; + ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkEmptySet) @@ -478,64 +435,26 @@ TEST_F(TestApiBlackSolver, mkFalse) ASSERT_NO_THROW(d_solver.mkFalse()); } -TEST_F(TestApiBlackSolver, mkNaN) -{ - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkNaN(3, 5)); - } - else - { - ASSERT_THROW(d_solver.mkNaN(3, 5), CVC5ApiException); - } -} +TEST_F(TestApiBlackSolver, mkNaN) { ASSERT_NO_THROW(d_solver.mkNaN(3, 5)); } TEST_F(TestApiBlackSolver, mkNegZero) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkNegZero(3, 5)); - } - else - { - ASSERT_THROW(d_solver.mkNegZero(3, 5), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkNegZero(3, 5)); } TEST_F(TestApiBlackSolver, mkNegInf) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkNegInf(3, 5)); - } - else - { - ASSERT_THROW(d_solver.mkNegInf(3, 5), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkNegInf(3, 5)); } TEST_F(TestApiBlackSolver, mkPosInf) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkPosInf(3, 5)); - } - else - { - ASSERT_THROW(d_solver.mkPosInf(3, 5), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkPosInf(3, 5)); } TEST_F(TestApiBlackSolver, mkPosZero) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkPosZero(3, 5)); - } - else - { - ASSERT_THROW(d_solver.mkPosZero(3, 5), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkPosZero(3, 5)); } TEST_F(TestApiBlackSolver, mkOp) diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index d1b096bda..757bacad6 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -95,11 +95,8 @@ TEST_F(TestApiBlackSort, isRegExp) TEST_F(TestApiBlackSort, isRoundingMode) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_TRUE(d_solver.getRoundingModeSort().isRoundingMode()); - ASSERT_NO_THROW(Sort().isRoundingMode()); - } + ASSERT_TRUE(d_solver.getRoundingModeSort().isRoundingMode()); + ASSERT_NO_THROW(Sort().isRoundingMode()); } TEST_F(TestApiBlackSort, isBitVector) @@ -110,11 +107,8 @@ TEST_F(TestApiBlackSort, isBitVector) TEST_F(TestApiBlackSort, isFloatingPoint) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_TRUE(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint()); - ASSERT_NO_THROW(Sort().isFloatingPoint()); - } + ASSERT_TRUE(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint()); + ASSERT_NO_THROW(Sort().isFloatingPoint()); } TEST_F(TestApiBlackSort, isDatatype) @@ -486,24 +480,18 @@ TEST_F(TestApiBlackSort, getBVSize) TEST_F(TestApiBlackSort, getFPExponentSize) { - if (d_solver.supportsFloatingPoint()) - { - Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - ASSERT_NO_THROW(fpSort.getFPExponentSize()); - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException); - } + Sort fpSort = d_solver.mkFloatingPointSort(4, 8); + ASSERT_NO_THROW(fpSort.getFPExponentSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException); } TEST_F(TestApiBlackSort, getFPSignificandSize) { - if (d_solver.supportsFloatingPoint()) - { - Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - ASSERT_NO_THROW(fpSort.getFPSignificandSize()); - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException); - } + Sort fpSort = d_solver.mkFloatingPointSort(4, 8); + ASSERT_NO_THROW(fpSort.getFPSignificandSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException); } TEST_F(TestApiBlackSort, getDatatypeParamSorts) diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp index fe74130d1..4b0f1892f 100644 --- a/test/unit/node/attribute_white.cpp +++ b/test/unit/node/attribute_white.cpp @@ -78,7 +78,7 @@ TEST_F(TestNodeWhiteAttribute, attribute_ids) // and that the next ID to be assigned is strictly greater than // those that have already been assigned. - unsigned lastId = attr::LastAttributeId<std::string, false>::getId(); + unsigned lastId = attr::LastAttributeId<std::string>::getId(); ASSERT_LT(VarNameAttr::s_id, lastId); ASSERT_LT(TestStringAttr1::s_id, lastId); ASSERT_LT(TestStringAttr2::s_id, lastId); @@ -87,7 +87,7 @@ TEST_F(TestNodeWhiteAttribute, attribute_ids) ASSERT_NE(VarNameAttr::s_id, TestStringAttr2::s_id); ASSERT_NE(TestStringAttr1::s_id, TestStringAttr2::s_id); - lastId = attr::LastAttributeId<bool, false>::getId(); + lastId = attr::LastAttributeId<bool>::getId(); ASSERT_LT(TestFlag1::s_id, lastId); ASSERT_LT(TestFlag2::s_id, lastId); ASSERT_LT(TestFlag3::s_id, lastId); @@ -104,7 +104,7 @@ TEST_F(TestNodeWhiteAttribute, attribute_ids) ASSERT_NE(TestFlag3::s_id, TestFlag5::s_id); ASSERT_NE(TestFlag4::s_id, TestFlag5::s_id); - lastId = attr::LastAttributeId<TypeNode, false>::getId(); + lastId = attr::LastAttributeId<TypeNode>::getId(); ASSERT_LT(TypeAttr::s_id, lastId); } diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp index 7a6e34abb..e999297fd 100644 --- a/test/unit/theory/logic_info_white.cpp +++ b/test/unit/theory/logic_info_white.cpp @@ -616,28 +616,14 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) info.arithOnlyLinear(); info.disableIntegers(); info.lock(); - if (cvc5::Configuration::isBuiltWithSymFPU()) - { - ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA"); - } - else - { - ASSERT_EQ(info.getLogicString(), "SEP_AUFBVDTLRA"); - } + ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA"); info = info.getUnlockedCopy(); ASSERT_FALSE(info.isLocked()); info.disableQuantifiers(); info.disableTheory(THEORY_BAGS); info.lock(); - if (cvc5::Configuration::isBuiltWithSymFPU()) - { - ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA"); - } - else - { - ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVDTLRA"); - } + ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA"); info = info.getUnlockedCopy(); ASSERT_FALSE(info.isLocked()); @@ -647,14 +633,7 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) info.enableIntegers(); info.disableReals(); info.lock(); - if (cvc5::Configuration::isBuiltWithSymFPU()) - { - ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA"); - } - else - { - ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFLIA"); - } + ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA"); info = info.getUnlockedCopy(); ASSERT_FALSE(info.isLocked()); diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index c23ce79dd..5cd29878e 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -57,9 +57,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min) d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), BitVector(32u, (uint32_t)0x3FFFFFA1)); @@ -78,9 +78,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min) d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, true); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>(); std::cout << "opt value is: " << val << std::endl; @@ -105,9 +105,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max) d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>(); std::cout << "opt value is: " << val << std::endl; @@ -130,9 +130,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max) d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, true); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // expect the maxmum x = ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), @@ -154,9 +154,9 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // expect the maximum x = 18 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index cf0434ddc..583f908e7 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -62,9 +62,9 @@ TEST_F(TestTheoryWhiteIntOpt, max) // We activate our objective so the subsolver knows to optimize it d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // We expect max_cost == 99 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(), @@ -93,9 +93,9 @@ TEST_F(TestTheoryWhiteIntOpt, min) // We activate our objective so the subsolver knows to optimize it d_optslv->addObjective(max_cost, OptimizationObjective::MINIMIZE); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // We expect max_cost == 99 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(), @@ -125,10 +125,10 @@ TEST_F(TestTheoryWhiteIntOpt, result) d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE); // This should return OPT_UNSAT since 0 > x > 100 is impossible. - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); // We expect our check to have returned UNSAT - ASSERT_EQ(r, OptimizationResult::UNSAT); + ASSERT_EQ(r.isSat(), Result::UNSAT); d_smtEngine->resetAssertions(); } @@ -157,9 +157,9 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval) d_optslv->addObjective(cost3, OptimizationObjective::MINIMIZE); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(), diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp index 73c6d9e7e..9a091fb3b 100644 --- a/test/unit/theory/theory_opt_multigoal_white.cpp +++ b/test/unit/theory/theory_opt_multigoal_white.cpp @@ -54,11 +54,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, box) // y <= x d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); - // Box optimization OptimizationSolver optSolver(d_smtEngine.get()); - optSolver.setObjectiveCombination(OptimizationSolver::BOX); - // minimize x optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); // maximize y with `signed` comparison over bit-vectors. @@ -66,9 +63,10 @@ TEST_F(TestTheoryWhiteOptMultigoal, box) // maximize z optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = optSolver.checkOpt(); + // Box optimization + Result r = optSolver.checkOpt(OptimizationSolver::BOX); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); std::vector<OptimizationResult> results = optSolver.getValues(); @@ -100,8 +98,6 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex) OptimizationSolver optSolver(d_smtEngine.get()); - optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC); - // minimize x optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); // maximize y with `signed` comparison over bit-vectors. @@ -109,9 +105,9 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex) // maximize z optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = optSolver.checkOpt(); + Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); std::vector<OptimizationResult> results = optSolver.getValues(); @@ -180,18 +176,17 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) (maximize b) */ OptimizationSolver optSolver(d_smtEngine.get()); - optSolver.setObjectiveCombination(OptimizationSolver::PARETO); optSolver.addObjective(a, OptimizationObjective::MAXIMIZE); optSolver.addObjective(b, OptimizationObjective::MAXIMIZE); - OptimizationResult::ResultType r; + Result r; // all possible result pairs <a, b> std::set<std::pair<uint32_t, uint32_t>> possibleResults = { {1, 3}, {2, 2}, {3, 1}}; - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::PARETO); + ASSERT_EQ(r.isSat(), Result::SAT); std::vector<OptimizationResult> results = optSolver.getValues(); std::pair<uint32_t, uint32_t> res = { results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(), @@ -205,8 +200,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) ASSERT_EQ(possibleResults.count(res), 1); possibleResults.erase(res); - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::PARETO); + ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); res = { results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(), @@ -220,8 +215,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) ASSERT_EQ(possibleResults.count(res), 1); possibleResults.erase(res); - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::PARETO); + ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); res = { results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(), @@ -235,8 +230,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) ASSERT_EQ(possibleResults.count(res), 1); possibleResults.erase(res); - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::UNSAT); + r = optSolver.checkOpt(OptimizationSolver::PARETO); + ASSERT_EQ(r.isSat(), Result::UNSAT); ASSERT_EQ(possibleResults.size(), 0); } @@ -254,11 +249,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) // y <= x d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); - // Lexico optimization OptimizationSolver optSolver(d_smtEngine.get()); - optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC); - // minimize x optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); @@ -270,9 +262,10 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) // maximize z optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = optSolver.checkOpt(); + // Lexico optimization + Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); std::vector<OptimizationResult> results = optSolver.getValues(); @@ -290,16 +283,16 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) d_smtEngine->pop(); // now we only have one objective: (minimize x) - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); + ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); ASSERT_EQ(results.size(), 1); ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u)); // resetting the assertions also resets the optimization objectives d_smtEngine->resetAssertions(); - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); + ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); ASSERT_EQ(results.size(), 0); } diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 26ab40614..c1630a203 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -24,9 +24,7 @@ cvc5_add_unit_test_white(check_white util) cvc5_add_unit_test_black(configuration_black util) cvc5_add_unit_test_black(datatype_black util) cvc5_add_unit_test_black(exception_black util) -if(CVC5_USE_SYMFPU) cvc5_add_unit_test_black(floatingpoint_black util) -endif() cvc5_add_unit_test_black(integer_black util) cvc5_add_unit_test_white(integer_white util) cvc5_add_unit_test_black(output_black util) |