Avoid using printSynthSolution in the python API and examples (#6564)

The function printSynthSolution declared here is going to be removed in #6521.

This PR removes it from the python API.
Following #6530, this PR also replaces its usages in the examples by a utility function.
For this, we also add support for getSynthSolutions in the python API.

9 files changed, 85 insertions, 17 deletions

diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
index 95e5fb80e..ec4154f4f 100644
--- a/examples/api/python/CMakeLists.txt
+++ b/examples/api/python/CMakeLists.txt
@@ -53,5 +53,5 @@ foreach(example ${EXAMPLES_API_PYTHON})
   )
   set_tests_properties(${example_test} PROPERTIES
     LABELS "example"
-    ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH})
+    ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH}:${CMAKE_SOURCE_DIR}/api/python)
 endforeach()
diff --git a/examples/api/python/__init__.py b/examples/api/python/__init__.py
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/examples/api/python/__init__.py
diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py
index 6e1440d66..d2ad1feb4 100644
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -17,6 +17,7 @@
 
 import copy
 import pycvc5
+import utils
 from pycvc5 import kinds
 
 if __name__ == "__main__":
@@ -93,5 +94,5 @@ if __name__ == "__main__":
     # Output should be equivalent to:
     # (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
     # (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
-    slv.printSynthSolution()
-
+    terms = [max, min]
+    utils.print_synth_solutions(terms, slv.getSynthSolutions(terms))
diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py
index 406646f9f..02a7dff48 100644
--- a/examples/api/python/sygus-grammar.py
+++ b/examples/api/python/sygus-grammar.py
@@ -17,6 +17,7 @@
 ##
 
 import copy
+import utils 
 import pycvc5
 from pycvc5 import kinds
 
@@ -87,4 +88,5 @@ if __name__ == "__main__":
     # (define-fun id2 ((x Int)) Int x)
     # (define-fun id3 ((x Int)) Int (+ x 0))
     # (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
-    slv.printSynthSolution()
+    terms = [id1, id2, id3, id4]
+    utils.print_synth_solutions(terms, slv.getSynthSolutions(terms))
diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py
index 0fa752b1e..8273aa298 100644
--- a/examples/api/python/sygus-inv.py
+++ b/examples/api/python/sygus-inv.py
@@ -16,6 +16,7 @@
 # translation of sygus-inv.cpp .
 ##
 
+import utils
 import pycvc5
 from pycvc5 import kinds
 
@@ -60,7 +61,7 @@ if __name__ == "__main__":
   if slv.checkSynth().isUnsat():
     # Output should be equivalent to:
     # (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
-    slv.printSynthSolution()
-
+    terms = [inv_f]
+    utils.print_synth_solutions(terms, slv.getSynthSolutions(terms))
 
 
diff --git a/examples/api/python/utils.py b/examples/api/python/utils.py
new file mode 100644
index 000000000..23b41d50d
--- /dev/null
+++ b/examples/api/python/utils.py
@@ -0,0 +1,55 @@
+#!/usr/bin/env python
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# Utility Methods, translated from examples/api/utils.h
+##
+
+import pycvc5
+from pycvc5 import kinds
+
+# Get the string version of define-fun command.
+# @param f the function to print
+# @param params the function parameters
+# @param body the function body
+# @return a string version of define-fun
+
+
+def define_fun_to_string(f, params, body):
+    sort = f.getSort()
+    if sort.isFunction():
+        sort = f.getSort().getFunctionCodomainSort()
+    result = ""
+    result += "(define-fun " + str(f) + " ("
+    for i in range(0, len(params)):
+        if i > 0:
+            result += " "
+        else:
+            result += "(" + str(params[i]) + " " + str(params[i].getSort()) + ")"
+    result += ") " + str(sort) + " " + str(body) + ")"
+    return result
+
+
+# Print solutions for synthesis conjecture to the standard output stream.
+# @param terms the terms for which the synthesis solutions were retrieved
+# @param sols the synthesis solutions of the given terms
+
+
+def print_synth_solutions(terms, sols):
+    result = ""
+    for i in range(0, len(terms)):
+        params = []
+        if sols[i].getKind() == kinds.Lambda:
+            params += sols[i][0]
+            body = sols[i][1]
+        result += "  " + define_fun_to_string(terms[i], params, body) + "\n"
+    print(result)
diff --git a/examples/api/utils.cpp b/examples/api/utils.cpp
index b7385d688..69676819a 100644
--- a/examples/api/utils.cpp
+++ b/examples/api/utils.cpp
@@ -26,9 +26,14 @@
  */
 std::string defineFunToString(const cvc5::api::Term& f,
                               const std::vector<cvc5::api::Term> params,
-                              const cvc5::api::Sort& sort,
                               const cvc5::api::Term body)
 {
+
+  cvc5::api::Sort sort = f.getSort();
+  if (sort.isFunction())
+  {
+    sort = sort.getFunctionCodomainSort();
+  }
   std::stringstream ss;
   ss << "(define-fun " << f << " (";
   for (size_t i = 0, n = params.size(); i < n; ++i)
@@ -57,12 +62,7 @@ void printSynthSolutions(const std::vector<cvc5::api::Term>& terms,
       params.insert(params.end(), sols[i][0].begin(), sols[i][0].end());
       body = sols[i][1];
     }
-    cvc5::api::Sort rangeSort = terms[i].getSort();
-    if (rangeSort.isFunction())
-    {
-      rangeSort = rangeSort.getFunctionCodomainSort();
-    }
-    std::cout << "  " << defineFunToString(terms[i], params, rangeSort, body)
+    std::cout << "  " << defineFunToString(terms[i], params, body)
               << std::endl;
   }
   std::cout << ')' << std::endl;
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 6fbc5ab57..205b82918 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -180,7 +180,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         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 +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index cd643d3f3..2fac78552 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -958,6 +958,19 @@ cdef class Solver:
         t.cterm = self.csolver.getSynthSolution(term.cterm)
         return t
 
+    def getSynthSolutions(self, list terms):
+        result = []
+        cdef vector[c_Term] vec
+        for t in terms:
+            vec.push_back((<Term?> t).cterm)
+        cresult = self.csolver.getSynthSolutions(vec)
+        for s in cresult:
+            term = Term(self)
+            term.cterm = s
+            result.append(term)
+        return result
+
+
     def synthInv(self, symbol, bound_vars, Grammar grammar=None):
         cdef Term term = Term(self)
         cdef vector[c_Term] v
@@ -969,9 +982,6 @@ cdef class Solver:
             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):
         '''