Adding interpolation and abduction to the python API (#7868)

This PR adds getAbduct, getAbductNext, getInterpol, and getInterpolNext to the python API.
Tests and documentation are added as well.

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 552fe6399f7085de28bb3df8ce91db9f8086afb9..43108d2426b9e38cfda3a862ea7baffa40549fba 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -296,6 +296,12 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         void setInfo(string& keyword, const string& value) except +
         void setLogic(const string& logic) except +
         void setOption(const string& option, const string& value) except +
+        bint getInterpolant(const Term& conj, Term& output) except +
+        bint getInterpolant(const Term& conj, Grammar& grammar, Term& output) except +
+        bint getInterpolantNext(const Term& conj) except +
+        bint getAbduct(const Term& conj, Term& output) except +
+        bint getAbduct(const Term& conj, Grammar& grammar, Term& output) except +
+        bint getAbductNext(const Term& conj) except +
 
     cdef cppclass Grammar:
         Grammar() except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 63e21bf7ec862aedbd26e6f860727da3aa777d50..ce9e98e6fedbea0a3d1fa9f9a95cd7d1502fd046 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2235,6 +2235,117 @@ cdef class Solver:
         """
         self.csolver.setOption(option.encode(), value.encode())
 
+    def getInterpolant(self, Term conj, *args):
+        """Get an interpolant.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( get-interpol <conj> )
+            ( get-interpol <conj> <grammar> )
+
+        Requires option :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a mode different from `none`.
+
+        Supports the following variants:
+
+        - ``bool getInteprolant(Term conj, Term output)``
+        - ``bool getInteprolant(Term conj, Grammar grammar, Term output)``
+        
+        :param conj: the conjecture term
+        :param output: the term where the result will be stored
+        :param grammar: a grammar for the inteprolant
+        :return: True iff an interpolant was found
+        """
+        result = False
+        if len(args) == 1:
+            assert isinstance(args[0], Term)
+            result = self.csolver.getInterpolant(conj.cterm, (<Term ?> args[0]).cterm)
+        else:
+            assert len(args) == 2
+            assert isinstance(args[0], Grammar)
+            assert isinstance(args[1], Term)
+            result = self.csolver.getInterpolant(conj.cterm, (<Grammar ?> args[0]).cgrammar, (<Term ?> args[1]).cterm)
+        return result
+
+
+    def getInterpolantNext(self, Term output):
+        """
+        Get the next interpolant. Can only be called immediately after
+        a succesful call to get-interpol or get-interpol-next. 
+        Is guaranteed to produce a syntactically different interpolant wrt the
+        last returned interpolant if successful.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( get-interpol-next )
+
+        Requires to enable incremental mode, and 
+        option :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a mode different from `none`.
+
+        :param output: the term where the result will be stored
+        :return: True iff an interpolant was found
+        """
+        result = self.csolver.getInterpolantNext(output.cterm)
+        return result
+        
+    def getAbduct(self, Term conj, *args):
+        """Get an abduct.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( get-abduct <conj> )
+            ( get-abduct <conj> <grammar> )
+
+        Requires to enable option :ref:`produce-abducts <lbl-option-produce-abducts>`.
+
+        Supports the following variants:
+
+        - ``bool getAbduct(Term conj, Term output)``
+        - ``bool getAbduct(Term conj, Grammar grammar, Term output)``
+        
+        :param conj: the conjecture term
+        :param output: the term where the result will be stored
+        :param grammar: a grammar for the abduct 
+        :return: True iff an abduct was found
+        """
+        result = False
+        if len(args) == 1:
+            assert isinstance(args[0], Term)
+            result = self.csolver.getAbduct(conj.cterm, (<Term ?> args[0]).cterm)
+        else:
+            assert len(args) == 2
+            assert isinstance(args[0], Grammar)
+            assert isinstance(args[1], Term)
+            result = self.csolver.getAbduct(conj.cterm, (<Grammar ?> args[0]).cgrammar, (<Term ?> args[1]).cterm)
+        return result
+
+    def getAbductNext(self, Term output):
+        """
+        Get the next abduct. Can only be called immediately after
+        a succesful call to get-abduct or get-abduct-next. 
+        Is guaranteed to produce a syntactically different abduct wrt the 
+        last returned abduct if successful.
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+
+            ( get-abduct-next )
+
+        Requires to enable incremental mode, and 
+        option :ref:`produce-abducts <lbl-option-produce-abducts>`.
+        :param output: the term where the result will be stored
+        :return: True iff an abduct was found
+        """
+        result = self.csolver.getAbductNext(output.cterm)
+        return result
+
+
 
 cdef class Sort:
     """

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 0fe0d465ece0b7574c36ffa92a5dcc1dbaef1cce..90e6610d85daa1b373ab784e530f348c00a2cf82 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -1987,6 +1987,104 @@ def test_check_synth_next3(solver):
     with pytest.raises(RuntimeError):
         solver.checkSynthNext()
 
+def test_get_abduct(solver):
+    solver.setLogic("QF_LIA")
+    solver.setOption("produce-abducts", "true")
+    solver.setOption("incremental", "false")
+
+    intSort = solver.getIntegerSort()
+    zero = solver.mkInteger(0)
+    x = solver.mkConst(intSort, "x")
+    y = solver.mkConst(intSort, "y")
+
+    solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero))
+    conj = solver.mkTerm(Kind.Gt, y, zero)
+    output = pycvc5.Term(solver)
+    assert solver.getAbduct(conj, output)
+    assert not output.isNull() and output.getSort().isBoolean()
+
+    boolean = solver.getBooleanSort()
+    truen = solver.mkBoolean(True)
+    start = solver.mkVar(boolean)
+    output2 = pycvc5.Term(solver)
+    g = solver.mkSygusGrammar([], [start])
+    conj2 = solver.mkTerm(Kind.Gt, x, zero)
+    g.addRule(start, truen)
+    assert solver.getAbduct(conj2, g, output2)
+    assert output2 == truen
+
+def test_get_abduct2(solver):
+    solver.setLogic("QF_LIA")
+    solver.setOption("incremental", "false")
+    intSort = solver.getIntegerSort()
+    zero = solver.mkInteger(0)
+    x = solver.mkConst(intSort, "x")
+    y = solver.mkConst(intSort, "y")
+    solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero))
+    conj = solver.mkTerm(Kind.Gt, y, zero)
+    output = pycvc5.Term(solver)
+    with pytest.raises(RuntimeError):
+        solver.getAbduct(conj, output)
+
+def test_get_abduct_next(solver):
+    solver.setLogic("QF_LIA")
+    solver.setOption("produce-abducts", "true")
+    solver.setOption("incremental", "true")
+
+    intSort = solver.getIntegerSort()
+    zero = solver.mkInteger(0)
+    x = solver.mkConst(intSort, "x")
+    y = solver.mkConst(intSort, "y")
+
+    solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero))
+    conj = solver.mkTerm(Kind.Gt, y, zero)
+    output = pycvc5.Term(solver)
+    assert solver.getAbduct(conj, output)
+    output2 = pycvc5.Term(solver)
+    assert solver.getAbductNext(output2)
+    assert output != output2
+
+
+def test_get_interpolant(solver):
+    solver.setLogic("QF_LIA")
+    solver.setOption("produce-interpols", "default")
+    solver.setOption("incremental", "false")
+
+    intSort = solver.getIntegerSort()
+    zero = solver.mkInteger(0)
+    x = solver.mkConst(intSort, "x")
+    y = solver.mkConst(intSort, "y")
+    z = solver.mkConst(intSort, "z")
+
+    solver.assertFormula(solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, x, y), zero))
+    solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero))
+    conj = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, y, z), zero), solver.mkTerm(Kind.Lt, z, zero))
+    output = pycvc5.Term(solver)
+    solver.getInterpolant(conj, output)
+    assert output.getSort().isBoolean()
+
+def test_get_interpolant_next(solver):
+    solver.setLogic("QF_LIA")
+    solver.setOption("produce-interpols", "default")
+    solver.setOption("incremental", "true")
+
+    intSort = solver.getIntegerSort()
+    zero = solver.mkInteger(0)
+    x = solver.mkConst(intSort, "x")
+    y = solver.mkConst(intSort, "y")
+    z = solver.mkConst(intSort, "z")
+
+    solver.assertFormula(solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, x, y), zero))
+    solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero))
+    conj = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, y, z), zero), solver.mkTerm(Kind.Lt, z, zero))
+    output = pycvc5.Term(solver)
+    solver.getInterpolant(conj, output)
+    output2 = pycvc5.Term(solver)
+    solver.getInterpolantNext(output2)
+
+    assert output != output2
+
+
 def test_declare_pool(solver):
     intSort = solver.getIntegerSort()
     setSort = solver.mkSetSort(intSort)