From: yoni206 Date: Tue, 4 Jan 2022 15:18:41 +0000 (+0200) Subject: Adding interpolation and abduction to the python API (#7868) X-Git-Tag: cvc5-1.0.0~611 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a0bd75c53fe2c647368f5419c28cd7494ece748d;p=cvc5.git 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 552fe6399..43108d242 100644 --- 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 63e21bf7e..ce9e98e6f 100644 --- 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 ) + ( get-interpol ) + + Requires option :ref:`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, ( args[0]).cterm) + else: + assert len(args) == 2 + assert isinstance(args[0], Grammar) + assert isinstance(args[1], Term) + result = self.csolver.getInterpolant(conj.cterm, ( args[0]).cgrammar, ( 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 ` 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 ) + ( get-abduct ) + + Requires to enable option :ref:`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, ( args[0]).cterm) + else: + assert len(args) == 2 + assert isinstance(args[0], Grammar) + assert isinstance(args[1], Term) + result = self.csolver.getAbduct(conj.cterm, ( args[0]).cgrammar, ( 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 `. + :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 0fe0d465e..90e6610d8 100644 --- 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)