diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-05-14 11:24:54 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-14 16:24:54 +0000 |
commit | a4d56aed6874b4f074f5eb96c4a5d688988cba98 (patch) | |
tree | 9c5a66819c38a2a1ae8aa777c4a3798275fe97d7 /examples/api | |
parent | bcd2e8e2fd28e30cddac35a466bf6ca797e2aa51 (diff) |
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.
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/CMakeLists.txt | 11 | ||||
-rw-r--r-- | examples/api/sygus-fun.cpp | 19 | ||||
-rw-r--r-- | examples/api/sygus-grammar.cpp | 27 | ||||
-rw-r--r-- | examples/api/sygus-inv.cpp | 15 | ||||
-rw-r--r-- | examples/api/utils.cpp | 69 | ||||
-rw-r--r-- | examples/api/utils.h | 29 |
6 files changed, 148 insertions, 22 deletions
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 <cvc5/cvc5.h> #include <iostream> +#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<Term> 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 <cvc5/cvc5.h> #include <iostream> +#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<Term> 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 <cvc5/cvc5.h> #include <iostream> +#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<Term> 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 <iostream> + +/** + * 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<cvc5::api::Term> 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<cvc5::api::Term>& terms, + const std::vector<cvc5::api::Term>& sols) +{ + std::cout << '(' << std::endl; + + for (size_t i = 0, n = terms.size(); i < n; ++i) + { + std::vector<cvc5::api::Term> 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 <cvc5/cvc5.h> + +/** + * 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<cvc5::api::Term>& terms, + const std::vector<cvc5::api::Term>& sols); + +#endif // CVC5__UTILS_H |