diff options
Diffstat (limited to 'test')
35 files changed, 70 insertions, 261 deletions
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/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index 44ce684dd..1255bf270 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): @@ -60,11 +56,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 +71,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 +87,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): @@ -313,11 +300,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): @@ -333,11 +316,7 @@ 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 +329,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): @@ -382,43 +360,23 @@ 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_pi(solver): 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/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/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/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/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/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/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/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/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) |