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

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 7ad259fdb6848b554de781b01375de44f449a65c..b9627073c5bd7caf1bd5aefb66aa29adff9ac67a 100644 (file)
--- 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 f9384c288bdeeff7035c00324323530bb4fd42c7..b52514a283f7bd3976e5437557d28a529e727320 100644 (file)
--- 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 4e0c4bbb012e5338d63ab0afe908fbe583c2c3ca..dc2bfef75da006bc5ac937c602715acb5353133e 100644 (file)
--- 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")