From 4ddbf7c13d2ce344e46a57bdef5af44922ca2552 Mon Sep 17 00:00:00 2001 From: Ying Sheng Date: Thu, 14 Jan 2021 03:19:45 +0800 Subject: [PATCH] Add unit test for api getInterpolant() -- issue #5593 (#5772) The pull request addressed issue #5593 for adding an unit test. --- test/unit/api/solver_black.cpp | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) 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) -- 2.30.2