From: Ying Sheng <sqy1415@gmail.com>
Date: Tue, 17 May 2022 13:40:32 +0000 (-0700)
Subject: Add getInterpolant with a grammar in the unit test for all language bindings (#8775)
X-Git-Tag: cvc5-1.0.1~125
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3690b354b40923fadbaad148fc93ea281feaafbc;p=cvc5.git

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