From: Ying Sheng <sqy1415@gmail.com>
Date: Wed, 13 Jan 2021 19:19:45 +0000 (+0800)
Subject: Add unit test for api getInterpolant() -- issue #5593 (#5772)
X-Git-Tag: cvc5-1.0.0~2380
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4ddbf7c13d2ce344e46a57bdef5af44922ca2552;p=cvc5.git

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 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)