From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Fri, 14 May 2021 16:24:54 +0000 (-0500) Subject: Stop using the solver for printing sygus synthesis solutions. (#6530) X-Git-Tag: cvc5-1.0.0~1760 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a4d56aed6874b4f074f5eb96c4a5d688988cba98;p=cvc5.git Stop using the solver for printing sygus synthesis solutions. (#6530) This PR uses custom methods for printing the synthesis solutions instead of Solver::printSynthSolution, which is going to be removed by #6521. --- diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt index 7b713e6e7..bff7caa4d 100644 --- a/examples/api/CMakeLists.txt +++ b/examples/api/CMakeLists.txt @@ -24,11 +24,18 @@ set(CVC5_EXAMPLES_API sets sequences strings +) + +foreach(example ${CVC5_EXAMPLES_API}) + cvc5_add_example(${example} "" "api") +endforeach() + +set(SYGUS_EXAMPLES_API sygus-fun sygus-grammar sygus-inv ) -foreach(example ${CVC5_EXAMPLES_API}) - cvc5_add_example(${example} "" "api") +foreach(example ${SYGUS_EXAMPLES_API}) + cvc5_add_example(${example} "${example}.cpp utils.h utils.cpp" "api") endforeach() diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp index 6eeffff1c..0f96e72a7 100644 --- a/examples/api/sygus-fun.cpp +++ b/examples/api/sygus-fun.cpp @@ -41,15 +41,19 @@ * * (check-synth) * - * The printed output to this example 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)) + * The printed output for this example 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)) + * ) */ #include #include +#include "utils.h" + using namespace cvc5::api; int main() @@ -126,9 +130,12 @@ int main() if (slv.checkSynth().isUnsat()) { // 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(std::cout); + // ( + // (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)) + // ) + std::vector terms = {max, min}; + printSynthSolutions(terms, slv.getSynthSolutions(terms)); } return 0; diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp index 095f15889..ce5a1bc8b 100644 --- a/examples/api/sygus-grammar.cpp +++ b/examples/api/sygus-grammar.cpp @@ -36,17 +36,21 @@ * * (check-synth) * - * The printed output to this example should look like: - * (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) - * (define-fun id2 ((x Int)) Int x) - * (define-fun id3 ((x Int)) Int (+ x 0)) - * (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) + * The printed output for this example should look like: + * ( + * (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) + * (define-fun id2 ((x Int)) Int x) + * (define-fun id3 ((x Int)) Int (+ x 0)) + * (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) + * ) */ #include #include +#include "utils.h" + using namespace cvc5::api; int main() @@ -114,11 +118,14 @@ int main() if (slv.checkSynth().isUnsat()) { // Output should be equivalent to: - // (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) - // (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(std::cout); + // ( + // (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) + // (define-fun id2 ((x Int)) Int x) + // (define-fun id3 ((x Int)) Int (+ x 0)) + // (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) + // ) + std::vector terms = {id1, id2, id3, id4}; + printSynthSolutions(terms, slv.getSynthSolutions(terms)); } return 0; diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp index 820fe8630..f658fa33a 100644 --- a/examples/api/sygus-inv.cpp +++ b/examples/api/sygus-inv.cpp @@ -30,14 +30,18 @@ * * (check-synth) * - * The printed output to this example should be equivalent to: - * (define-fun inv-f ((x Int)) Bool (not (>= x 11))) + * The printed output for this example should be equivalent to: + * ( + * (define-fun inv-f ((x Int)) Bool (not (>= x 11))) + * ) */ #include #include +#include "utils.h" + using namespace cvc5::api; int main() @@ -82,8 +86,11 @@ int main() if (slv.checkSynth().isUnsat()) { // Output should be equivalent to: - // (define-fun inv-f ((x Int)) Bool (not (>= x 11))) - slv.printSynthSolution(std::cout); + // ( + // (define-fun inv-f ((x Int)) Bool (not (>= x 11))) + // ) + std::vector terms = {inv_f}; + printSynthSolutions(terms, slv.getSynthSolutions(terms)); } return 0; diff --git a/examples/api/utils.cpp b/examples/api/utils.cpp new file mode 100644 index 000000000..b7385d688 --- /dev/null +++ b/examples/api/utils.cpp @@ -0,0 +1,69 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed + * + * 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. + * **************************************************************************** + * + * Implementations of utility methods. + */ + +#include "utils.h" + +#include + +/** + * 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 + */ +std::string defineFunToString(const cvc5::api::Term& f, + const std::vector params, + const cvc5::api::Sort& sort, + const cvc5::api::Term body) +{ + std::stringstream ss; + ss << "(define-fun " << f << " ("; + for (size_t i = 0, n = params.size(); i < n; ++i) + { + if (i > 0) + { + ss << ' '; + } + ss << '(' << params[i] << ' ' << params[i].getSort() << ')'; + } + ss << ") " << sort << ' ' << body << ')'; + return ss.str(); +} + +void printSynthSolutions(const std::vector& terms, + const std::vector& sols) +{ + std::cout << '(' << std::endl; + + for (size_t i = 0, n = terms.size(); i < n; ++i) + { + std::vector params; + cvc5::api::Term body; + if (sols[i].getKind() == cvc5::api::LAMBDA) + { + 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::endl; + } + std::cout << ')' << std::endl; +} diff --git a/examples/api/utils.h b/examples/api/utils.h new file mode 100644 index 000000000..69cddee26 --- /dev/null +++ b/examples/api/utils.h @@ -0,0 +1,29 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed + * + * 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. + */ + +#ifndef CVC5__UTILS_H +#define CVC5__UTILS_H + +#include + +/** + * 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 + */ +void printSynthSolutions(const std::vector& terms, + const std::vector& sols); + +#endif // CVC5__UTILS_H