Add unit test for api getInterpolant() -- issue #5593 (#5772)

The pull request addressed issue #5593 for adding an unit test.

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 5592c7d3dfe7f898ff353b9bf900d8b2813f66ae..e89d31e7de4d8ca4729fb72b921f7979e9663fb2 100644 (file)
--- 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)