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 <abdalrhman-mohamed@uiowa.edu>
'lang': 'c++',
'group': 'c++'
},
+ '\.h$': {
+ 'title': 'C++ (header)',
+ 'lang': 'c++',
+ 'group': 'c++'
+ },
'\.java$': {
'title': 'Java',
'lang': 'java',
<examples>/api/java/SygusFun.java
<examples>/api/python/sygus-fun.py
<examples>/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::
+ <examples>/api/cpp/utils.h
+ <examples>/api/cpp/utils.cpp
+ <examples>/api/java/Utils.java
+ <examples>/api/python/utils.py
<examples>/api/java/SygusGrammar.java
<examples>/api/python/sygus-grammar.py
<examples>/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::
+ <examples>/api/cpp/utils.h
+ <examples>/api/cpp/utils.cpp
+ <examples>/api/java/Utils.java
+ <examples>/api/python/utils.py
<examples>/api/java/SygusInv.java
<examples>/api/python/sygus-inv.py
<examples>/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::
+ <examples>/api/cpp/utils.h
+ <examples>/api/cpp/utils.cpp
+ <examples>/api/java/Utils.java
+ <examples>/api/python/utils.py
)
foreach(example ${CVC5_EXAMPLES_API})
- cvc5_add_example(${example} "" "api")
+ cvc5_add_example(${example} "" "api/cpp")
endforeach()
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()
* 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 <cvc5/cvc5.h>
// (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
// )
std::vector<Term> terms = {max, min};
- printSynthSolutions(terms, slv.getSynthSolutions(terms));
+ utils::printSynthSolutions(terms, slv.getSynthSolutions(terms));
}
return 0;
* 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 <cvc5/cvc5.h>
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");
// (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
// )
std::vector<Term> terms = {id1, id2, id3, id4};
- printSynthSolutions(terms, slv.getSynthSolutions(terms));
+ utils::printSynthSolutions(terms, slv.getSynthSolutions(terms));
}
return 0;
* 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 <cvc5/cvc5.h>
// (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
// )
std::vector<Term> terms = {inv_f};
- printSynthSolutions(terms, slv.getSynthSolutions(terms));
+ utils::printSynthSolutions(terms, slv.getSynthSolutions(terms));
}
return 0;
#include <iostream>
+namespace utils {
+
+using namespace cvc5;
+
/**
* Get the string version of define-fun command.
* @param f the function to print
* @return a string version of define-fun
*/
std::string defineFunToString(const cvc5::Term& f,
- const std::vector<cvc5::Term> params,
- const cvc5::Term body)
+ const std::vector<cvc5::Term>& params,
+ const cvc5::Term& body)
{
cvc5::Sort sort = f.getSort();
if (sort.isFunction())
const std::vector<cvc5::Term>& sols)
{
std::cout << '(' << std::endl;
-
for (size_t i = 0, n = terms.size(); i < n; ++i)
{
std::vector<cvc5::Term> 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
#include <cvc5/cvc5.h>
+namespace utils {
+
/**
* Print solutions for synthesis conjecture to the standard output stream.
* @param terms the terms for which the synthesis solutions were retrieved
void printSynthSolutions(const std::vector<cvc5::Term>& terms,
const std::vector<cvc5::Term>& sols);
+} // namespace utils
+
#endif // CVC5__UTILS_H
* 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.*;
* 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.*;
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");
* 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.*;
--- /dev/null
+/******************************************************************************
+ * 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<Term> 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(')');
+ }
+}
slv.setLogic("LIA")
integer = slv.getIntegerSort()
- boolean = slv.getBooleanSort()
# declare input variable for the function-to-synthesize
x = slv.mkVar(integer, "x")
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 += " "
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)
{
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<Term> 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(')');
- }
}
projects / cvc5.git / commitdiff