Add SyGuS Python API (#4812)

This commit extends the Python API with support for SyGuS functionality.
This required the addition of a nullary constructor for `Grammar` in the C++ API.
A unit test is also included, and is a translation of the corresponding C++ API unit test.

Examples are not added yet, but are ready and planned for a next PR (in order to keep this one shorter).

5 files changed, 234 insertions, 0 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 2da791da0..1c15466a1 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2446,6 +2446,18 @@ bool Datatype::const_iterator::operator!=(
 /* -------------------------------------------------------------------------- */
 /* Grammar                                                                    */
 /* -------------------------------------------------------------------------- */
+
+Grammar::Grammar()
+    : d_solver(nullptr),
+      d_sygusVars(),
+      d_ntSyms(),
+      d_ntsToTerms(0),
+      d_allowConst(),
+      d_allowVars(),
+      d_isResolved(false)
+{
+}
+
 Grammar::Grammar(const Solver* slv,
                  const std::vector<Term>& sygusVars,
                  const std::vector<Term>& ntSymbols)
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 997616ae3..edd74280a 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1954,6 +1954,11 @@ class CVC4_PUBLIC Grammar
    */
   void addRules(Term ntSymbol, std::vector<Term> rules);
 
+  /**
+   * Nullary constructor. Needed for the Cython API.
+   */
+  Grammar();
+
  private:
   /**
    * Constructor.
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index eea263a96..16d64b85e 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -143,6 +143,22 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         Op mkOp(Kind kind, const string& arg) except +
         Op mkOp(Kind kind, uint32_t arg) except +
         Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) except +
+        # Sygus related functions
+        Grammar mkSygusGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except +
+        Term mkSygusVar(Sort sort, const string& symbol) except +
+        Term mkSygusVar(Sort sort) except +
+        void addSygusConstraint(Term term) except +
+        void addSygusInvConstraint(Term inv_f, Term pre_f, Term trans_f, Term post_f) except +
+        Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort) except +
+        Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort, Grammar grammar) except +
+        Result checkSynth() except +
+        Term getSynthSolution(Term t) except +
+        vector[Term] getSynthSolutions(const vector[Term]& terms) except +
+        Term synthInv(const string& symbol, const vector[Term]& bound_vars) except +
+        Term synthInv(const string& symbol, const vector[Term]& bound_vars, Grammar grammar) except +
+        void printSynthSolution(ostream& out) except +
+        # End of sygus related functions
+
         Term mkTrue() except +
         Term mkFalse() except +
         Term mkBoolean(bint val) except +
@@ -220,6 +236,13 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         void setLogic(const string& logic) except +
         void setOption(const string& option, const string& value) except +
 
+    cdef cppclass Grammar:
+        Grammar() except +
+        Grammar(Solver* solver, vector[Term] boundVars, vector[Term] ntSymbols) except +
+        void addRule(Term ntSymbol, Term rule) except +
+        void addAnyConstant(Term ntSymbol) except +
+        void addAnyVariable(Term ntSymbol) except +
+        void addRules(Term ntSymbol, vector[Term] rules) except +
 
     cdef cppclass Sort:
         Sort() except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 133bd4660..b6e4616da 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -17,6 +17,7 @@ from cvc4 cimport RoundingMode as c_RoundingMode
 from cvc4 cimport Op as c_Op
 from cvc4 cimport OpHashFunction as c_OpHashFunction
 from cvc4 cimport Solver as c_Solver
+from cvc4 cimport Grammar as c_Grammar
 from cvc4 cimport Sort as c_Sort
 from cvc4 cimport SortHashFunction as c_SortHashFunction
 from cvc4 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
@@ -271,6 +272,25 @@ cdef class Op:
 
         return indices
 
+cdef class Grammar:
+    cdef c_Grammar  cgrammar
+    def __cinit__(self):
+        self.cgrammar = c_Grammar()
+
+    def addRule(self, Term ntSymbol, Term rule):
+        self.cgrammar.addRule(ntSymbol.cterm, rule.cterm)
+
+    def addAnyConstant(self, Term ntSymbol):
+        self.cgrammar.addAnyConstant(ntSymbol.cterm)
+
+    def addAnyVariable(self, Term ntSymbol):
+        self.cgrammar.addAnyVariable(ntSymbol.cterm)
+
+    def addRules(self, Term ntSymbol, rules):
+        cdef vector[c_Term] crules
+        for r in rules:
+            crules.push_back((<Term?> r).cterm)
+        self.cgrammar.addRules(ntSymbol.cterm, crules)
 
 cdef class Result:
     cdef c_Result cr
@@ -783,6 +803,63 @@ cdef class Solver:
         r.cr = self.csolver.checkSat()
         return r
 
+    def mkSygusGrammar(self, boundVars, ntSymbols):
+        cdef Grammar grammar = Grammar()
+        cdef vector[c_Term] bvc
+        cdef vector[c_Term] ntc
+        for bv in boundVars:
+            bvc.push_back((<Term?> bv).cterm)
+        for nt in ntSymbols:
+            ntc.push_back((<Term?> nt).cterm)
+        grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
+        return grammar
+
+    def mkSygusVar(self, Sort sort, str symbol=""):
+        cdef Term term = Term()
+        term.cterm = self.csolver.mkSygusVar(sort.csort, symbol.encode())
+        return term
+
+    def addSygusConstraint(self, Term t):
+        self.csolver.addSygusConstraint(t.cterm)
+
+    def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f):
+        self.csolver.addSygusInvConstraint(inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
+
+    def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
+        cdef Term term = Term()
+        cdef vector[c_Term] v
+        for bv in bound_vars:
+            v.push_back((<Term?> bv).cterm)
+        if grammar is None:
+          term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort)
+        else:
+          term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort, grammar.cgrammar)
+        return term
+
+    def checkSynth(self):
+        cdef Result r = Result()
+        r.cr = self.csolver.checkSynth()
+        return r
+
+    def getSynthSolution(self, Term term):
+        cdef Term t = Term()
+        t.cterm = self.csolver.getSynthSolution(term.cterm)
+        return t
+
+    def synthInv(self, symbol, bound_vars, Grammar grammar=None):
+        cdef Term term = Term()
+        cdef vector[c_Term] v
+        for bv in bound_vars:
+            v.push_back((<Term?> bv).cterm)
+        if grammar is None:
+            term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v)
+        else:
+            term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v, grammar.cgrammar)
+        return term
+
+    def printSynthSolution(self):
+        self.csolver.printSynthSolution(cout)
+
     @expand_list_arg(num_req_args=0)
     def checkSatAssuming(self, *assumptions):
         '''
diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py
new file mode 100644
index 000000000..3a703017f
--- /dev/null
+++ b/test/unit/api/python/test_grammar.py
@@ -0,0 +1,117 @@
+# translated from test/unit/api/grammar_black.h
+
+import pytest
+
+import pycvc4
+from pycvc4 import kinds
+
+def test_add_rule():
+  solver = pycvc4.Solver()
+  boolean = solver.getBooleanSort()
+  integer = solver.getIntegerSort()
+
+  nullTerm = pycvc4.Term()
+  start = solver.mkVar(boolean)
+  nts = solver.mkVar(boolean)
+
+  # expecting no error
+  g = solver.mkSygusGrammar([], [start])
+
+  g.addRule(start, solver.mkBoolean(False))
+
+  # expecting errors
+  with pytest.raises(Exception):
+    g.addRule(nullTerm, solver.mkBoolean(false))
+  with pytest.raises(Exception):
+    g.addRule(start, nullTerm)
+  with pytest.raises(Exception):
+    g.addRule(nts, solver.mkBoolean(false))
+  with pytest.raises(Exception):
+    g.addRule(start, solver.mkReal(0))
+
+  # expecting no errors
+  solver.synthFun("f", {}, boolean, g)
+
+  # expecting an error
+  with pytest.raises(Exception):
+    g.addRule(start, solver.mkBoolean(false))
+
+def test_add_rules():
+  solver = pycvc4.Solver()
+  boolean = solver.getBooleanSort()
+  integer = solver.getIntegerSort()
+
+  nullTerm = pycvc4.Term()
+  start = solver.mkVar(boolean)
+  nts = solver.mkVar(boolean)
+
+  g = solver.mkSygusGrammar([], [start])
+
+  g.addRules(start, {solver.mkBoolean(False)})
+
+  #Expecting errors
+  with pytest.raises(Exception):
+    g.addRules(nullTerm, solver.mkBoolean(False))
+  with pytest.raises(Exception):
+    g.addRules(start, {nullTerm})
+  with pytest.raises(Exception):
+    g.addRules(nts, {solver.mkBoolean(False)})
+  with pytest.raises(Exception):
+    g.addRules(start, {solver.mkReal(0)})
+  #Expecting no errors
+  solver.synthFun("f", {}, boolean, g)
+
+  #Expecting an error
+  with pytest.raises(Exception):
+    g.addRules(start, solver.mkBoolean(False))
+
+def testAddAnyConstant():
+  solver = pycvc4.Solver()
+  boolean = solver.getBooleanSort()
+
+  nullTerm = pycvc4.Term()
+  start = solver.mkVar(boolean)
+  nts = solver.mkVar(boolean)
+
+  g = solver.mkSygusGrammar({}, {start})
+
+  g.addAnyConstant(start)
+  g.addAnyConstant(start)
+
+  with pytest.raises(Exception):
+    g.addAnyConstant(nullTerm)
+  with pytest.raises(Exception):
+    g.addAnyConstant(nts)
+
+  solver.synthFun("f", {}, boolean, g)
+
+  with pytest.raises(Exception):
+    g.addAnyConstant(start)
+
+
+def testAddAnyVariable():
+  solver = pycvc4.Solver()
+  boolean = solver.getBooleanSort()
+
+  nullTerm = pycvc4.Term()
+  x = solver.mkVar(boolean)
+  start = solver.mkVar(boolean)
+  nts = solver.mkVar(boolean)
+
+  g1 = solver.mkSygusGrammar({x}, {start})
+  g2 = solver.mkSygusGrammar({}, {start})
+
+  g1.addAnyVariable(start)
+  g1.addAnyVariable(start)
+  g2.addAnyVariable(start)
+
+  with pytest.raises(Exception):
+    g1.addAnyVariable(nullTerm)
+  with pytest.raises(Exception):
+    g1.addAnyVariable(nts)
+
+  solver.synthFun("f", {}, boolean, g1)
+
+  with pytest.raises(Exception):
+    g1.addAnyVariable(start)
+