From f1ba9b8542b8cd7424b6dfc679c834593c7b8f01 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 29 Mar 2022 21:11:08 -0500 Subject: [PATCH] Show the code for utilities in the docs. (#8387) This PR adds the code for printing synthesis solutions to the docs. Various other changes are made to increase the consistency between the different bindings. Signed-off-by: Abdalrhman M Mohamed --- docs/conf.py.in | 5 ++ docs/examples/sygus-fun.rst | 9 +++ docs/examples/sygus-grammar.rst | 9 +++ docs/examples/sygus-inv.rst | 9 +++ examples/api/cpp/CMakeLists.txt | 4 +- examples/api/cpp/sygus-fun.cpp | 36 +--------- examples/api/cpp/sygus-grammar.cpp | 34 +-------- examples/api/cpp/sygus-inv.cpp | 24 +------ examples/api/cpp/utils.cpp | 16 +++-- examples/api/cpp/utils.h | 4 ++ examples/api/java/SygusFun.java | 34 +-------- examples/api/java/SygusGrammar.java | 33 +-------- examples/api/java/SygusInv.java | 22 +----- examples/api/java/Utils.java | 83 ++++++++++++++++++++++ examples/api/python/sygus-grammar.py | 1 - examples/api/python/utils.py | 7 +- src/api/java/io/github/cvc5/api/Utils.java | 57 --------------- 17 files changed, 145 insertions(+), 242 deletions(-) create mode 100644 examples/api/java/Utils.java diff --git a/docs/conf.py.in b/docs/conf.py.in index 1b09f152a..4d54a49d8 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -150,6 +150,11 @@ examples_types = { 'lang': 'c++', 'group': 'c++' }, + '\.h$': { + 'title': 'C++ (header)', + 'lang': 'c++', + 'group': 'c++' + }, '\.java$': { 'title': 'Java', 'lang': 'java', diff --git a/docs/examples/sygus-fun.rst b/docs/examples/sygus-fun.rst index 164a8f65b..d2470c6d8 100644 --- a/docs/examples/sygus-fun.rst +++ b/docs/examples/sygus-fun.rst @@ -7,3 +7,12 @@ SyGuS: Functions /api/java/SygusFun.java /api/python/sygus-fun.py /api/smtlib/sygus-fun.sy + +The utility method used for printing the synthesis solutions in the examples +above is defined separately in the ``utils`` module: + +.. api-examples:: + /api/cpp/utils.h + /api/cpp/utils.cpp + /api/java/Utils.java + /api/python/utils.py diff --git a/docs/examples/sygus-grammar.rst b/docs/examples/sygus-grammar.rst index 4d416b5f8..c659be6ae 100644 --- a/docs/examples/sygus-grammar.rst +++ b/docs/examples/sygus-grammar.rst @@ -7,3 +7,12 @@ SyGuS: Grammars /api/java/SygusGrammar.java /api/python/sygus-grammar.py /api/smtlib/sygus-grammar.sy + +The utility method used for printing the synthesis solutions in the examples +above is defined separately in the ``utils`` module: + +.. api-examples:: + /api/cpp/utils.h + /api/cpp/utils.cpp + /api/java/Utils.java + /api/python/utils.py diff --git a/docs/examples/sygus-inv.rst b/docs/examples/sygus-inv.rst index b2addf8c1..80f89ccc1 100644 --- a/docs/examples/sygus-inv.rst +++ b/docs/examples/sygus-inv.rst @@ -7,3 +7,12 @@ SyGuS: Invariants /api/java/SygusInv.java /api/python/sygus-inv.py /api/smtlib/sygus-inv.sy + +The utility method used for printing the synthesis solutions in the examples +above is defined separately in the ``utils`` module: + +.. api-examples:: + /api/cpp/utils.h + /api/cpp/utils.cpp + /api/java/Utils.java + /api/python/utils.py diff --git a/examples/api/cpp/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt index defb716c3..6d462da5d 100644 --- a/examples/api/cpp/CMakeLists.txt +++ b/examples/api/cpp/CMakeLists.txt @@ -31,7 +31,7 @@ set(CVC5_EXAMPLES_API ) foreach(example ${CVC5_EXAMPLES_API}) - cvc5_add_example(${example} "" "api") + cvc5_add_example(${example} "" "api/cpp") endforeach() set(SYGUS_EXAMPLES_API @@ -41,5 +41,5 @@ set(SYGUS_EXAMPLES_API ) foreach(example ${SYGUS_EXAMPLES_API}) - cvc5_add_example(${example} "${example}.cpp utils.h utils.cpp" "api") + cvc5_add_example(${example} "${example}.cpp utils.h utils.cpp" "api/cpp") endforeach() diff --git a/examples/api/cpp/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp index 895a791d6..864ab6a11 100644 --- a/examples/api/cpp/sygus-fun.cpp +++ b/examples/api/cpp/sygus-fun.cpp @@ -13,39 +13,7 @@ * A simple demonstration of the Sygus API. * * A simple demonstration of how to use the Sygus API to synthesize max and min - * functions. Here is the same problem written in Sygus V2 format: - * - * (set-logic LIA) - * - * (synth-fun max ((x Int) (y Int)) Int - * ((Start Int) (StartBool Bool)) - * ((Start Int (0 1 x y - * (+ Start Start) - * (- Start Start) - * (ite StartBool Start Start))) - * (StartBool Bool ((and StartBool StartBool) - * (not StartBool) - * (<= Start Start))))) - * - * (synth-fun min ((x Int) (y Int)) Int) - * - * (declare-var x Int) - * (declare-var y Int) - * - * (constraint (>= (max x y) x)) - * (constraint (>= (max x y) y)) - * (constraint (or (= x (max x y)) - * (= y (max x y)))) - * (constraint (= (+ (max x y) (min x y)) - * (+ x y))) - * - * (check-synth) - * - * 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)) - * ) + * functions. */ #include @@ -137,7 +105,7 @@ int main() // (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) // ) std::vector terms = {max, min}; - printSynthSolutions(terms, slv.getSynthSolutions(terms)); + utils::printSynthSolutions(terms, slv.getSynthSolutions(terms)); } return 0; diff --git a/examples/api/cpp/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp index a6a1dfede..cca30d301 100644 --- a/examples/api/cpp/sygus-grammar.cpp +++ b/examples/api/cpp/sygus-grammar.cpp @@ -13,36 +13,7 @@ * A simple demonstration of the Sygus API. * * A simple demonstration of how to use Grammar to add syntax constraints to - * the Sygus solution for the identity function. Here is the same problem - * written in Sygus V2 format: - * - * (set-logic LIA) - * - * (synth-fun id1 ((x Int)) Int - * ((Start Int)) ((Start Int ((- x) (+ x Start))))) - * - * (synth-fun id2 ((x Int)) Int - * ((Start Int)) ((Start Int ((Variable Int) (- x) (+ x Start))))) - * - * (synth-fun id3 ((x Int)) Int - * ((Start Int)) ((Start Int (0 (- x) (+ x Start))))) - * - * (synth-fun id4 ((x Int)) Int - * ((Start Int)) ((Start Int ((- x) (+ x Start))))) - * - * (declare-var x Int) - * - * (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) - * - * (check-synth) - * - * 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)))) - * ) + * the Sygus solution for the identity function. */ #include @@ -65,7 +36,6 @@ int main() slv.setLogic("LIA"); Sort integer = slv.getIntegerSort(); - Sort boolean = slv.getBooleanSort(); // declare input variable for the function-to-synthesize Term x = slv.mkVar(integer, "x"); @@ -126,7 +96,7 @@ int main() // (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) // ) std::vector terms = {id1, id2, id3, id4}; - printSynthSolutions(terms, slv.getSynthSolutions(terms)); + utils::printSynthSolutions(terms, slv.getSynthSolutions(terms)); } return 0; diff --git a/examples/api/cpp/sygus-inv.cpp b/examples/api/cpp/sygus-inv.cpp index d872ca5fd..5d517d03d 100644 --- a/examples/api/cpp/sygus-inv.cpp +++ b/examples/api/cpp/sygus-inv.cpp @@ -13,27 +13,7 @@ * A simple demonstration of the Sygus API. * * A simple demonstration of how to use the Sygus API to synthesize a simple - * invariant. Here is the same problem written in Sygus V2 format: - * - * (set-logic LIA) - * - * (synth-inv inv-f ((x Int))) - * - * (define-fun pre-f ((x Int)) Bool - * (= x 0)) - * (define-fun trans-f ((x Int) (xp Int)) Bool - * (ite (< x 10) (= xp (+ x 1)) (= xp x))) - * (define-fun post-f ((x Int)) Bool - * (<= x 10)) - * - * (inv-constraint inv-f pre-f trans-f post-f) - * - * (check-synth) - * - * The printed output for this example should be equivalent to: - * ( - * (define-fun inv-f ((x Int)) Bool (not (>= x 11))) - * ) + * invariant. */ #include @@ -92,7 +72,7 @@ int main() // (define-fun inv-f ((x Int)) Bool (not (>= x 11))) // ) std::vector terms = {inv_f}; - printSynthSolutions(terms, slv.getSynthSolutions(terms)); + utils::printSynthSolutions(terms, slv.getSynthSolutions(terms)); } return 0; diff --git a/examples/api/cpp/utils.cpp b/examples/api/cpp/utils.cpp index bb2573843..788f509f2 100644 --- a/examples/api/cpp/utils.cpp +++ b/examples/api/cpp/utils.cpp @@ -17,6 +17,10 @@ #include +namespace utils { + +using namespace cvc5; + /** * Get the string version of define-fun command. * @param f the function to print @@ -25,8 +29,8 @@ * @return a string version of define-fun */ std::string defineFunToString(const cvc5::Term& f, - const std::vector params, - const cvc5::Term body) + const std::vector& params, + const cvc5::Term& body) { cvc5::Sort sort = f.getSort(); if (sort.isFunction()) @@ -51,18 +55,18 @@ 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::Term body; + cvc5::Term body = sols[i]; if (sols[i].getKind() == cvc5::LAMBDA) { params.insert(params.end(), sols[i][0].begin(), sols[i][0].end()); body = sols[i][1]; } - std::cout << " " << defineFunToString(terms[i], params, body) - << std::endl; + std::cout << " " << defineFunToString(terms[i], params, body) << std::endl; } std::cout << ')' << std::endl; } + +} // namespace utils diff --git a/examples/api/cpp/utils.h b/examples/api/cpp/utils.h index c6393427f..ec22e4fa8 100644 --- a/examples/api/cpp/utils.h +++ b/examples/api/cpp/utils.h @@ -18,6 +18,8 @@ #include +namespace utils { + /** * Print solutions for synthesis conjecture to the standard output stream. * @param terms the terms for which the synthesis solutions were retrieved @@ -26,4 +28,6 @@ void printSynthSolutions(const std::vector& terms, const std::vector& sols); +} // namespace utils + #endif // CVC5__UTILS_H diff --git a/examples/api/java/SygusFun.java b/examples/api/java/SygusFun.java index 42a93e4f7..6063a8239 100644 --- a/examples/api/java/SygusFun.java +++ b/examples/api/java/SygusFun.java @@ -13,39 +13,7 @@ * A simple demonstration of the Sygus API. * * A simple demonstration of how to use the Sygus API to synthesize max and min - * functions. Here is the same problem written in Sygus V2 format: - * - * (set-logic LIA) - * - * (synth-fun max ((x Int) (y Int)) Int - * ((Start Int) (StartBool Bool)) - * ((Start Int (0 1 x y - * (+ Start Start) - * (- Start Start) - * (ite StartBool Start Start))) - * (StartBool Bool ((and StartBool StartBool) - * (not StartBool) - * (<= Start Start))))) - * - * (synth-fun min ((x Int) (y Int)) Int) - * - * (declare-var x Int) - * (declare-var y Int) - * - * (constraint (>= (max x y) x)) - * (constraint (>= (max x y) y)) - * (constraint (or (= x (max x y)) - * (= y (max x y)))) - * (constraint (= (+ (max x y) (min x y)) - * (+ x y))) - * - * (check-synth) - * - * 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)) - * ) + * functions. This is a direct translation of sygus-fun.cpp. */ import static io.github.cvc5.api.Kind.*; diff --git a/examples/api/java/SygusGrammar.java b/examples/api/java/SygusGrammar.java index ce59ab9c5..cb8a5106a 100644 --- a/examples/api/java/SygusGrammar.java +++ b/examples/api/java/SygusGrammar.java @@ -13,36 +13,8 @@ * A simple demonstration of the Sygus API. * * A simple demonstration of how to use Grammar to add syntax constraints to - * the Sygus solution for the identity function. Here is the same problem - * written in Sygus V2 format: - * - * (set-logic LIA) - * - * (synth-fun id1 ((x Int)) Int - * ((Start Int)) ((Start Int ((- x) (+ x Start))))) - * - * (synth-fun id2 ((x Int)) Int - * ((Start Int)) ((Start Int ((Variable Int) (- x) (+ x Start))))) - * - * (synth-fun id3 ((x Int)) Int - * ((Start Int)) ((Start Int (0 (- x) (+ x Start))))) - * - * (synth-fun id4 ((x Int)) Int - * ((Start Int)) ((Start Int ((- x) (+ x Start))))) - * - * (declare-var x Int) - * - * (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) - * - * (check-synth) - * - * 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)))) - * ) + * the Sygus solution for the identity function. This is a direct translation + * of sygus-grammar.cpp. */ import static io.github.cvc5.api.Kind.*; @@ -63,7 +35,6 @@ public class SygusGrammar slv.setLogic("LIA"); Sort integer = slv.getIntegerSort(); - Sort bool = slv.getBooleanSort(); // declare input variable for the function-to-synthesize Term x = slv.mkVar(integer, "x"); diff --git a/examples/api/java/SygusInv.java b/examples/api/java/SygusInv.java index f1d611b2e..8e9f79eac 100644 --- a/examples/api/java/SygusInv.java +++ b/examples/api/java/SygusInv.java @@ -13,27 +13,7 @@ * A simple demonstration of the Sygus API. * * A simple demonstration of how to use the Sygus API to synthesize a simple - * invariant. Here is the same problem written in Sygus V2 format: - * - * (set-logic LIA) - * - * (synth-inv inv-f ((x Int))) - * - * (define-fun pre-f ((x Int)) Bool - * (= x 0)) - * (define-fun trans-f ((x Int) (xp Int)) Bool - * (ite (< x 10) (= xp (+ x 1)) (= xp x))) - * (define-fun post-f ((x Int)) Bool - * (<= x 10)) - * - * (inv-constraint inv-f pre-f trans-f post-f) - * - * (check-synth) - * - * The printed output for this example should be equivalent to: - * ( - * (define-fun inv-f ((x Int)) Bool (not (>= x 11))) - * ) + * invariant. This is a direct translation of sygus-inv.cpp. */ import static io.github.cvc5.api.Kind.*; diff --git a/examples/api/java/Utils.java b/examples/api/java/Utils.java new file mode 100644 index 000000000..6cfd6c766 --- /dev/null +++ b/examples/api/java/Utils.java @@ -0,0 +1,83 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 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. + */ + +import java.util.ArrayList; +import java.util.List; + +import io.github.cvc5.api.CVC5ApiException; +import io.github.cvc5.api.Kind; +import io.github.cvc5.api.Sort; +import io.github.cvc5.api.Term; + +public class Utils +{ + /** + * 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 + */ + private static String defineFunToString(Term f, Term[] params, Term body) + { + Sort sort = f.getSort(); + if (sort.isFunction()) + { + sort = sort.getFunctionCodomainSort(); + } + StringBuilder ss = new StringBuilder(); + ss.append("(define-fun ").append(f).append(" ("); + for (int i = 0; i < params.length; ++i) + { + if (i > 0) + { + ss.append(' '); + } + ss.append('(').append(params[i]).append(' ').append(params[i].getSort()) + .append(')'); + } + ss.append(") ").append(sort).append(' ').append(body).append(')'); + return ss.toString(); + } + + /** + * 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 + */ + public static void printSynthSolutions(Term[] terms, Term[] sols) + throws CVC5ApiException + { + System.out.println('('); + for (int i = 0; i < terms.length; ++i) + { + List params = new ArrayList<>(); + Term body = sols[i]; + if (sols[i].getKind() == Kind.LAMBDA) + { + for (Term t : sols[i].getChild(0)) + { + params.add(t); + } + body = sols[i].getChild(1); + } + System.out.println(" " + + defineFunToString(terms[i], params.toArray(new Term[0]), body)); + } + System.out.println(')'); + } +} diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py index 7c020e39d..1613f6595 100644 --- a/examples/api/python/sygus-grammar.py +++ b/examples/api/python/sygus-grammar.py @@ -32,7 +32,6 @@ if __name__ == "__main__": slv.setLogic("LIA") integer = slv.getIntegerSort() - boolean = slv.getBooleanSort() # declare input variable for the function-to-synthesize x = slv.mkVar(integer, "x") diff --git a/examples/api/python/utils.py b/examples/api/python/utils.py index e367a743d..765327eb4 100644 --- a/examples/api/python/utils.py +++ b/examples/api/python/utils.py @@ -28,8 +28,7 @@ def define_fun_to_string(f, params, body): sort = f.getSort() if sort.isFunction(): sort = f.getSort().getFunctionCodomainSort() - result = "" - result += "(define-fun " + str(f) + " (" + result = "(define-fun " + str(f) + " (" for i in range(0, len(params)): if i > 0: result += " " @@ -44,11 +43,13 @@ def define_fun_to_string(f, params, body): def print_synth_solutions(terms, sols): - result = "" + result = "(\n" for i in range(0, len(terms)): params = [] + body = sols[i] if sols[i].getKind() == Kind.Lambda: params += sols[i][0] body = sols[i][1] result += " " + define_fun_to_string(terms[i], params, body) + "\n" + result += ")" print(result) diff --git a/src/api/java/io/github/cvc5/api/Utils.java b/src/api/java/io/github/cvc5/api/Utils.java index 54e0c9ced..6254d43ba 100644 --- a/src/api/java/io/github/cvc5/api/Utils.java +++ b/src/api/java/io/github/cvc5/api/Utils.java @@ -161,61 +161,4 @@ public class Utils { return pair.first.toString() + "/" + pair.second.toString(); } - - /** - * 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 - */ - private static String defineFunToString(Term f, Term[] params, Term body) - { - Sort sort = f.getSort(); - if (sort.isFunction()) - { - sort = sort.getFunctionCodomainSort(); - } - StringBuilder ss = new StringBuilder(); - ss.append("(define-fun ").append(f).append(" ("); - for (int i = 0; i < params.length; ++i) - { - if (i > 0) - { - ss.append(' '); - } - ss.append('(').append(params[i]).append(' ').append(params[i].getSort()).append(')'); - } - ss.append(") ").append(sort).append(' ').append(body).append(')'); - return ss.toString(); - } - - /** - * 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 - */ - public static void printSynthSolutions(Term[] terms, Term[] sols) throws CVC5ApiException - { - System.out.println('('); - - for (int i = 0; i < terms.length; ++i) - { - List params = new ArrayList<>(); - Term body = null; - if (sols[i].getKind() == Kind.LAMBDA) - { - for (Term t : sols[i].getChild(0)) - { - params.add(t); - } - body = sols[i].getChild(1); - } - if (body != null) - { - System.out.println(" " + defineFunToString(terms[i], params.toArray(new Term[0]), body)); - } - } - System.out.println(')'); - } } -- 2.30.2