diff options
Diffstat (limited to 'test/unit/api/solver_black.cpp')
-rw-r--r-- | test/unit/api/solver_black.cpp | 55 |
1 files changed, 46 insertions, 9 deletions
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 19113ae13..8dcb0fde6 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -376,15 +376,6 @@ TEST_F(TestApiBlackSolver, mkRoundingMode) ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); } -TEST_F(TestApiBlackSolver, mkUninterpretedConst) -{ - ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC5ApiException); - Solver slv; - ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1), - CVC5ApiException); -} - TEST_F(TestApiBlackSolver, mkAbstractValue) { ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1"))); @@ -419,6 +410,17 @@ TEST_F(TestApiBlackSolver, mkFloatingPoint) ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC5ApiException); } +TEST_F(TestApiBlackSolver, mkCardinalityConstraint) +{ + Sort su = d_solver.mkUninterpretedSort("u"); + Sort si = d_solver.getIntegerSort(); + ASSERT_NO_THROW(d_solver.mkCardinalityConstraint(su, 3)); + ASSERT_THROW(d_solver.mkCardinalityConstraint(si, 3), CVC5ApiException); + ASSERT_THROW(d_solver.mkCardinalityConstraint(su, 0), CVC5ApiException); + Solver slv; + ASSERT_THROW(slv.mkCardinalityConstraint(su, 3), CVC5ApiException); +} + TEST_F(TestApiBlackSolver, mkEmptySet) { Solver slv; @@ -606,6 +608,8 @@ TEST_F(TestApiBlackSolver, mkRegexpSigma) d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); } +TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); } + TEST_F(TestApiBlackSolver, mkSepNil) { ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort())); @@ -1234,6 +1238,23 @@ TEST_F(TestApiBlackSolver, getAbduct) ASSERT_EQ(output2, truen); } +TEST_F(TestApiBlackSolver, getAbduct2) +{ + d_solver.setLogic("QF_LIA"); + d_solver.setOption("incremental", "false"); + Sort intSort = d_solver.getIntegerSort(); + Term zero = d_solver.mkInteger(0); + Term x = d_solver.mkConst(intSort, "x"); + Term y = d_solver.mkConst(intSort, "y"); + // Assumptions for abduction: x > 0 + d_solver.assertFormula(d_solver.mkTerm(GT, x, zero)); + // Conjecture for abduction: y > 0 + Term conj = d_solver.mkTerm(GT, y, zero); + Term output; + // Fails due to option not set + ASSERT_THROW(d_solver.getAbduct(conj, output), CVC5ApiException); +} + TEST_F(TestApiBlackSolver, getInterpolant) { d_solver.setLogic("QF_LIA"); @@ -2536,5 +2557,21 @@ TEST_F(TestApiBlackSolver, Output) ASSERT_NE(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf()); } + +TEST_F(TestApiBlackSolver, issue7000) +{ + Sort s1 = d_solver.getIntegerSort(); + Sort s2 = d_solver.mkFunctionSort(s1, s1); + Sort s3 = d_solver.getRealSort(); + Term t4 = d_solver.mkPi(); + Term t7 = d_solver.mkConst(s3, "_x5"); + Term t37 = d_solver.mkConst(s2, "_x32"); + Term t59 = d_solver.mkConst(s2, "_x51"); + Term t72 = d_solver.mkTerm(EQUAL, t37, t59); + Term t74 = d_solver.mkTerm(GT, t4, t7); + // throws logic exception since logic is not higher order by default + ASSERT_THROW(d_solver.checkEntailed({t72, t74, t72, t72}), CVC5ApiException); +} + } // namespace test } // namespace cvc5 |