From bfa34c539319746dd3c247851cbbb8db86625fd0 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 20 May 2021 08:29:27 -0700 Subject: [PATCH] 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. --- examples/api/python/CMakeLists.txt | 2 +- examples/api/python/__init__.py | 0 examples/api/python/sygus-fun.py | 5 ++- examples/api/python/sygus-grammar.py | 4 +- examples/api/python/sygus-inv.py | 5 ++- examples/api/python/utils.py | 55 ++++++++++++++++++++++++++++ examples/api/utils.cpp | 14 +++---- src/api/python/cvc5.pxd | 1 - src/api/python/cvc5.pxi | 16 ++++++-- 9 files changed, 85 insertions(+), 17 deletions(-) create mode 100644 examples/api/python/__init__.py create mode 100644 examples/api/python/utils.py 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 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 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& 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(( 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(), v, grammar.cgrammar) return term - def printSynthSolution(self): - self.csolver.printSynthSolution(cout) - @expand_list_arg(num_req_args=0) def checkSatAssuming(self, *assumptions): ''' -- 2.30.2