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.
)
set_tests_properties(${example_test} PROPERTIES
LABELS "example"
- ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH})
+ ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH}:${CMAKE_SOURCE_DIR}/api/python)
endforeach()
import copy
import pycvc5
+import utils
from pycvc5 import kinds
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))
##
import copy
+import utils
import pycvc5
from pycvc5 import kinds
# (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))
# translation of sygus-inv.cpp .
##
+import utils
import pycvc5
from pycvc5 import kinds
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))
--- /dev/null
+#!/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)
*/
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)
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;
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 +
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
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):
'''
projects / cvc5.git / commitdiff