From 3690b354b40923fadbaad148fc93ea281feaafbc Mon Sep 17 00:00:00 2001 From: Ying Sheng Date: Tue, 17 May 2022 06:40:32 -0700 Subject: [PATCH] Add getInterpolant with a grammar in the unit test for all language bindings (#8775) Add getInterpolant with a grammar in the unit test for all language bindings --- test/unit/api/cpp/solver_black.cpp | 13 ++++++++++++- test/unit/api/java/SolverTest.java | 12 ++++++++++++ test/unit/api/python/test_solver.py | 10 ++++++++++ 3 files changed, 34 insertions(+), 1 deletion(-) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 7ad259fdb..b9627073c 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -1462,9 +1462,20 @@ TEST_F(TestApiBlackSolver, getInterpolant) d_solver.mkTerm(LT, {z, zero})}); // Call the interpolation api, while the resulting interpolant is the output Term output = d_solver.getInterpolant(conj); - // We expect the resulting output to be a boolean formula ASSERT_TRUE(output.getSort().isBoolean()); + + // try with a grammar, a simple grammar admitting true + Sort boolean = d_solver.getBooleanSort(); + Term truen = d_solver.mkBoolean(true); + Term start = d_solver.mkVar(boolean); + Grammar g = d_solver.mkGrammar({}, {start}); + Term conj2 = d_solver.mkTerm(EQUAL, {zero, zero}); + ASSERT_NO_THROW(g.addRule(start, truen)); + // Call the interpolation api, while the resulting interpolant is the output + Term output2 = d_solver.getInterpolant(conj2, g); + // interpolant must be true + ASSERT_EQ(output2, truen); } TEST_F(TestApiBlackSolver, getInterpolantNext) diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index f9384c288..b52514a28 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1504,6 +1504,18 @@ class SolverTest // We expect the resulting output to be a boolean formula assertTrue(output.getSort().isBoolean()); + + // try with a grammar, a simple grammar admitting true + Sort bsort = d_solver.getBooleanSort(); + Term truen = d_solver.mkBoolean(true); + Term start = d_solver.mkVar(bsort); + Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start}); + Term conj2 = d_solver.mkTerm(EQUAL, zero, zero); + assertDoesNotThrow(() -> g.addRule(start, truen)); + // Call the interpolation api, while the resulting interpolant is the output + Term output2 = d_solver.getInterpolant(conj2, g); + // interpolant must be true + assertEquals(output2, truen); } @Test diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 4e0c4bbb0..dc2bfef75 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -2346,6 +2346,16 @@ def test_get_interpolant(solver): output = solver.getInterpolant(conj) assert output.getSort().isBoolean() + boolean = solver.getBooleanSort() + truen = solver.mkBoolean(True) + start = solver.mkVar(boolean) + g = solver.mkGrammar([], [start]) + conj2 = solver.mkTerm(Kind.EQUAL, zero, zero) + g.addRule(start, truen) + output2 = solver.getInterpolant(conj2, g) + assert output2 == truen + + def test_get_interpolant_next(solver): solver.setLogic("QF_LIA") solver.setOption("produce-interpolants", "true") -- 2.30.2