diff options
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/api/solver_black.cpp | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 99a60aa76..312d57319 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -1473,6 +1473,57 @@ TEST_F(TestApiBlackSolver, getValue3) ASSERT_THROW(slv.getValue(x), CVC5ApiException); } +TEST_F(TestApiBlackSolver, getModelDomainElements) +{ + d_solver.setOption("produce-models", "true"); + Sort uSort = d_solver.mkUninterpretedSort("u"); + Sort intSort = d_solver.getIntegerSort(); + Term x = d_solver.mkConst(uSort, "x"); + Term y = d_solver.mkConst(uSort, "y"); + Term z = d_solver.mkConst(uSort, "z"); + Term f = d_solver.mkTerm(DISTINCT, x, y, z); + d_solver.assertFormula(f); + d_solver.checkSat(); + ASSERT_NO_THROW(d_solver.getModelDomainElements(uSort)); + ASSERT_TRUE(d_solver.getModelDomainElements(uSort).size() >= 3); + ASSERT_THROW(d_solver.getModelDomainElements(intSort), CVC5ApiException); +} + +TEST_F(TestApiBlackSolver, getModelDomainElements2) +{ + d_solver.setOption("produce-models", "true"); + d_solver.setOption("finite-model-find", "true"); + Sort uSort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(uSort, "x"); + Term y = d_solver.mkVar(uSort, "y"); + Term eq = d_solver.mkTerm(EQUAL, x, y); + Term bvl = d_solver.mkTerm(BOUND_VAR_LIST, x, y); + Term f = d_solver.mkTerm(FORALL, bvl, eq); + d_solver.assertFormula(f); + d_solver.checkSat(); + ASSERT_NO_THROW(d_solver.getModelDomainElements(uSort)); + // a model for the above must interpret u as size 1 + ASSERT_TRUE(d_solver.getModelDomainElements(uSort).size() == 1); +} + +TEST_F(TestApiBlackSolver, isModelCoreSymbol) +{ + d_solver.setOption("produce-models", "true"); + d_solver.setOption("model-cores", "simple"); + Sort uSort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkConst(uSort, "x"); + Term y = d_solver.mkConst(uSort, "y"); + Term z = d_solver.mkConst(uSort, "z"); + Term zero = d_solver.mkInteger(0); + Term f = d_solver.mkTerm(NOT, d_solver.mkTerm(EQUAL, x, y)); + d_solver.assertFormula(f); + d_solver.checkSat(); + ASSERT_TRUE(d_solver.isModelCoreSymbol(x)); + ASSERT_TRUE(d_solver.isModelCoreSymbol(y)); + ASSERT_FALSE(d_solver.isModelCoreSymbol(z)); + ASSERT_THROW(d_solver.isModelCoreSymbol(zero), CVC5ApiException); +} + TEST_F(TestApiBlackSolver, getQuantifierElimination) { Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x"); |