diff options
| author | Ying Sheng <sqy1415@gmail.com> | 2021-01-14 03:19:45 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-13 13:19:45 -0600 |
| commit | 4ddbf7c13d2ce344e46a57bdef5af44922ca2552 (patch) | |
| tree | 42e56583787ba4cc47efbd1b63462ae5b9d73219 | |
| parent | acbe543869918eb2d88779f0f98bfd18b82282d3 (diff) | |
Add unit test for api getInterpolant() -- issue #5593 (#5772)
The pull request addressed issue #5593 for adding an unit test.
| -rw-r--r-- | test/unit/api/solver_black.cpp | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 5592c7d3d..e89d31e7d 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -1251,7 +1251,30 @@ TEST_F(TestApiSolverBlack, getInfo) TEST_F(TestApiSolverBlack, getInterpolant) { - // TODO issue #5593 + d_solver.setOption("produce-interpols", "default"); + 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"); + Term z = d_solver.mkConst(intSort, "z"); + + // Assumptions for interpolation: x + y > 0 /\ x < 0 + d_solver.assertFormula( + d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero)); + d_solver.assertFormula(d_solver.mkTerm(LT, x, zero)); + // Conjecture for interpolation: y + z > 0 /\ z < 0 + Term conj = + d_solver.mkTerm(OR, + d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero), + d_solver.mkTerm(LT, z, zero)); + Term output; + // Call the interpolation api, while the resulting interpolant is the output + d_solver.getInterpolant(conj, output); + + // We expect the resulting output to be a boolean formula + ASSERT_TRUE(output.getSort().isBoolean()); } TEST_F(TestApiSolverBlack, getOp) |