SyGuS: Invariants
examples/api/cpp/sygus-inv.cpp
1/******************************************************************************
2 * Top contributors (to current version):
3 * Abdalrhman Mohamed, Aina Niemetz, Mathias Preiner
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of the Sygus API.
14 *
15 * A simple demonstration of how to use the Sygus API to synthesize a simple
16 * invariant.
17 */
18
19#include <cvc5/cvc5.h>
20
21#include <iostream>
22
23#include "utils.h"
24
25using namespace cvc5;
26
27int main()
28{
29 TermManager tm;
30 Solver slv(tm);
31
32 // required options
33 slv.setOption("sygus", "true");
34 slv.setOption("incremental", "false");
35
36 // set the logic
37 slv.setLogic("LIA");
38
39 Sort integer = tm.getIntegerSort();
40 Sort boolean = tm.getBooleanSort();
41
42 Term zero = tm.mkInteger(0);
43 Term one = tm.mkInteger(1);
44 Term ten = tm.mkInteger(10);
45
46 // declare input variables for functions
47 Term x = tm.mkVar(integer, "x");
48 Term xp = tm.mkVar(integer, "xp");
49
50 // (ite (< x 10) (= xp (+ x 1)) (= xp x))
51 Term ite =
52 tm.mkTerm(Kind::ITE,
53 {tm.mkTerm(Kind::LT, {x, ten}),
54 tm.mkTerm(Kind::EQUAL, {xp, tm.mkTerm(Kind::ADD, {x, one})}),
55 tm.mkTerm(Kind::EQUAL, {xp, x})});
56
57 // define the pre-conditions, transition relations, and post-conditions
58 Term pre_f =
59 slv.defineFun("pre-f", {x}, boolean, tm.mkTerm(Kind::EQUAL, {x, zero}));
60 Term trans_f = slv.defineFun("trans-f", {x, xp}, boolean, ite);
61 Term post_f =
62 slv.defineFun("post-f", {x}, boolean, tm.mkTerm(Kind::LEQ, {x, ten}));
63
64 // declare the invariant-to-synthesize
65 Term inv_f = slv.synthFun("inv-f", {x}, boolean);
66
67 slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f);
68
69 // print solutions if available
70 if (slv.checkSynth().hasSolution())
71 {
72 // Output should be equivalent to:
73 // (
74 // (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
75 // )
76 std::vector<Term> terms = {inv_f};
77 utils::printSynthSolutions(terms, slv.getSynthSolutions(terms));
78 }
79
80 return 0;
81}
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of the Sygus API.
14 *
15 * A simple demonstration of how to use the Sygus API to synthesize a simple
16 * invariant.
17 */
18
19#include <cvc5/c/cvc5.h>
20#include <stdio.h>
21
22#include "utils.h"
23
24int main()
25{
26 Cvc5TermManager* tm = cvc5_term_manager_new();
27 Cvc5* slv = cvc5_new(tm);
28
29 // required options
30 cvc5_set_option(slv, "sygus", "true");
31 cvc5_set_option(slv, "incremental", "false");
32
33 // set the logic
34 cvc5_set_logic(slv, "LIA");
35
36 Cvc5Sort int_sort = cvc5_get_integer_sort(tm);
37 Cvc5Sort bool_sort = cvc5_get_boolean_sort(tm);
38
39 Cvc5Term zero = cvc5_mk_integer_int64(tm, 0);
40 Cvc5Term one = cvc5_mk_integer_int64(tm, 1);
41 Cvc5Term ten = cvc5_mk_integer_int64(tm, 10);
42
43 // declare input variables for functions
44 Cvc5Term x = cvc5_mk_var(tm, int_sort, "x");
45 Cvc5Term xp = cvc5_mk_var(tm, int_sort, "xp");
46
47 // (ite (< x 10) (= xp (+ x 1)) (= xp x))
48 Cvc5Term args2[2] = {x, ten};
49 Cvc5Term cond = cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2);
50 args2[0] = x;
51 args2[1] = one;
52 Cvc5Term add = cvc5_mk_term(tm, CVC5_KIND_ADD, 2, args2);
53 args2[0] = xp;
54 args2[1] = add;
55 Cvc5Term els = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
56 args2[0] = xp;
57 args2[1] = x;
58 Cvc5Term the = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
59 Cvc5Term args3[3] = {cond, els, the};
60 Cvc5Term ite = cvc5_mk_term(tm, CVC5_KIND_ITE, 3, args3);
61
62 // define the pre-conditions, transition relations, and post-conditions
63 Cvc5Term vars1[1] = {x};
64 args2[0] = x;
65 args2[1] = zero;
66 Cvc5Term pre_f = cvc5_define_fun(slv,
67 "pre-f",
68 1,
69 vars1,
70 bool_sort,
71 cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2),
72 false);
73 Cvc5Term vars2[2] = {x, xp};
74 Cvc5Term trans_f =
75 cvc5_define_fun(slv, "trans-f", 2, vars2, bool_sort, ite, false);
76 args2[0] = x;
77 args2[1] = ten;
78 Cvc5Term post_f = cvc5_define_fun(slv,
79 "post-f",
80 1,
81 vars1,
82 bool_sort,
83 cvc5_mk_term(tm, CVC5_KIND_LEQ, 2, args2),
84 false);
85
86 // declare the invariant-to-synthesize
87 Cvc5Term inv_f = cvc5_synth_fun(slv, "inv-f", 1, vars1, bool_sort);
88
89 cvc5_add_sygus_inv_constraint(slv, inv_f, pre_f, trans_f, post_f);
90
91 // print solutions if available
92 if (cvc5_synth_result_has_solution(cvc5_check_synth(slv)))
93 {
94 // Output should be equivalent to:
95 // (
96 // (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
97 // )
98 Cvc5Term args1[1] = {inv_f};
99 const Cvc5Term* sols = cvc5_get_synth_solutions(slv, 1, args1);
100 print_synth_solutions(1, args1, sols);
101 }
102
103 cvc5_delete(slv);
104 cvc5_term_manager_delete(tm);
105 return 0;
106}
examples/api/java/SygusInv.java
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Andrew Reynolds, Andres Noetzli
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of the Sygus API.
14 *
15 * A simple demonstration of how to use the Sygus API to synthesize a simple
16 * invariant. This is a direct translation of sygus-inv.cpp.
17 */
18
19import static io.github.cvc5.Kind.*;
20
21import io.github.cvc5.*;
22
23public class SygusInv
24{
25 public static void main(String args[]) throws CVC5ApiException
26 {
27 TermManager tm = new TermManager();
28 Solver slv = new Solver(tm);
29 {
30 // required options
31 slv.setOption("sygus", "true");
32 slv.setOption("incremental", "false");
33
34 // set the logic
35 slv.setLogic("LIA");
36
37 Sort integer = tm.getIntegerSort();
38 Sort bool = tm.getBooleanSort();
39
40 Term zero = tm.mkInteger(0);
41 Term one = tm.mkInteger(1);
42 Term ten = tm.mkInteger(10);
43
44 // declare input variables for functions
45 Term x = tm.mkVar(integer, "x");
46 Term xp = tm.mkVar(integer, "xp");
47
48 // (ite (< x 10) (= xp (+ x 1)) (= xp x))
49 Term ite = tm.mkTerm(ITE,
50 tm.mkTerm(LT, x, ten),
51 tm.mkTerm(EQUAL, xp, tm.mkTerm(ADD, x, one)),
52 tm.mkTerm(EQUAL, xp, x));
53
54 // define the pre-conditions, transition relations, and post-conditions
55 Term pre_f = slv.defineFun("pre-f", new Term[] {x}, bool, tm.mkTerm(EQUAL, x, zero));
56 Term trans_f = slv.defineFun("trans-f", new Term[] {x, xp}, bool, ite);
57 Term post_f = slv.defineFun("post-f", new Term[] {x}, bool, tm.mkTerm(LEQ, x, ten));
58
59 // declare the invariant-to-synthesize
60 Term inv_f = slv.synthFun("inv-f", new Term[] {x}, bool);
61
62 slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f);
63
64 // print solutions if available
65 if (slv.checkSynth().hasSolution())
66 {
67 // Output should be equivalent to:
68 // (
69 // (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
70 // )
71 Term[] terms = new Term[] {inv_f};
72 Utils.printSynthSolutions(terms, slv.getSynthSolutions(terms));
73 }
74 }
75 Context.deletePointers();
76 }
77}
examples/api/python/sygus-inv.py
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Yoni Zohar, Aina Niemetz, Mudathir Mohamed
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
9# in the top-level source directory and their institutional affiliations.
10# All rights reserved. See the file COPYING in the top-level source
11# directory for licensing information.
12# #############################################################################
13#
14# A simple demonstration of the solving capabilities of the cvc5
15# sygus solver through the Python API. This is a direct
16# translation of sygus-inv.cpp .
17##
18
19import utils
20import cvc5
21from cvc5 import Kind
22
23if __name__ == "__main__":
24 tm = cvc5.TermManager()
25 slv = cvc5.Solver(tm)
26
27 # required options
28 slv.setOption("sygus", "true")
29 slv.setOption("incremental", "false")
30
31 # set the logic
32 slv.setLogic("LIA")
33
34 integer = tm.getIntegerSort()
35 boolean = tm.getBooleanSort()
36
37 zero = tm.mkInteger(0)
38 one = tm.mkInteger(1)
39 ten = tm.mkInteger(10)
40
41 # declare input variables for functions
42 x = tm.mkVar(integer, "x")
43 xp = tm.mkVar(integer, "xp")
44
45 # (ite (< x 10) (= xp (+ x 1)) (= xp x))
46 ite = tm.mkTerm(Kind.ITE,
47 tm.mkTerm(Kind.LT, x, ten),
48 tm.mkTerm(Kind.EQUAL, xp, tm.mkTerm(Kind.ADD, x, one)),
49 tm.mkTerm(Kind.EQUAL, xp, x))
50
51 # define the pre-conditions, transition relations, and post-conditions
52 pre_f = slv.defineFun("pre-f", [x], boolean, tm.mkTerm(Kind.EQUAL, x, zero))
53 trans_f = slv.defineFun("trans-f", [x, xp], boolean, ite)
54 post_f = slv.defineFun("post-f", [x], boolean, tm.mkTerm(Kind.LEQ, x, ten))
55
56 # declare the invariant-to-synthesize
57 inv_f = slv.synthFun("inv-f", [x], boolean)
58
59 slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f)
60
61 # print solutions if available
62 if slv.checkSynth().hasSolution():
63 # Output should be equivalent to:
64 # (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
65 terms = [inv_f]
66 utils.print_synth_solutions(terms, slv.getSynthSolutions(terms))
67
68
examples/api/smtlib/sygus-inv.sy
1; The printed output for this example should be equivalent to:
2; (
3; (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
4; )
5
6(set-logic LIA)
7(synth-fun inv-f ((x Int)) Bool)
8(define-fun pre-f ((x Int)) Bool (= x 0))
9(define-fun trans-f ((x Int) (xp Int)) Bool (ite (< x 10) (= xp (+ x 1)) (= xp x)))
10(define-fun post-f ((x Int)) Bool (<= x 10))
11(inv-constraint inv-f pre-f trans-f post-f)
12(check-synth)
The utility method used for printing the synthesis solutions in the examples
above is defined separately in the utils module:
1/******************************************************************************
2 * Top contributors (to current version):
3 * Abdalrhman Mohamed, Mathias Preiner
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * Utility methods.
14 */
15
16#ifndef CVC5__UTILS_H
17#define CVC5__UTILS_H
18
19#include <cvc5/cvc5.h>
20
21namespace utils {
22
23/**
24 * Print solutions for synthesis conjecture to the standard output stream.
25 * @param terms the terms for which the synthesis solutions were retrieved
26 * @param sols the synthesis solutions of the given terms
27 */
28void printSynthSolutions(const std::vector<cvc5::Term>& terms,
29 const std::vector<cvc5::Term>& sols);
30
31} // namespace utils
32
33#endif // CVC5__UTILS_H
1/******************************************************************************
2 * Top contributors (to current version):
3 * Abdalrhman Mohamed, Mathias Preiner, Yoni Zohar
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * Implementations of utility methods.
14 */
15
16#include "utils.h"
17
18#include <iostream>
19
20namespace utils {
21
22using namespace cvc5;
23
24/**
25 * Get the string version of define-fun command.
26 * @param f the function to print
27 * @param params the function parameters
28 * @param body the function body
29 * @return a string version of define-fun
30 */
31std::string defineFunToString(const cvc5::Term& f,
32 const std::vector<cvc5::Term>& params,
33 const cvc5::Term& body)
34{
35 cvc5::Sort sort = f.getSort();
36 if (sort.isFunction())
37 {
38 sort = sort.getFunctionCodomainSort();
39 }
40 std::stringstream ss;
41 ss << "(define-fun " << f << " (";
42 for (size_t i = 0, n = params.size(); i < n; ++i)
43 {
44 if (i > 0)
45 {
46 ss << ' ';
47 }
48 ss << '(' << params[i] << ' ' << params[i].getSort() << ')';
49 }
50 ss << ") " << sort << ' ' << body << ')';
51 return ss.str();
52}
53
54void printSynthSolutions(const std::vector<cvc5::Term>& terms,
55 const std::vector<cvc5::Term>& sols)
56{
57 std::cout << '(' << std::endl;
58 for (size_t i = 0, n = terms.size(); i < n; ++i)
59 {
60 std::vector<cvc5::Term> params;
61 cvc5::Term body = sols[i];
62 if (sols[i].getKind() == cvc5::Kind::LAMBDA)
63 {
64 params.insert(params.end(), sols[i][0].begin(), sols[i][0].end());
65 body = sols[i][1];
66 }
67 std::cout << " " << defineFunToString(terms[i], params, body) << std::endl;
68 }
69 std::cout << ')' << std::endl;
70}
71
72} // namespace utils
1/******************************************************************************
2 * Top contributors (to current version):
3 * Abdalrhman Mohamed, Mathias Preiner
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * Utility methods.
14 */
15
16#ifndef CVC5__C_UTILS_H
17#define CVC5__C_UTILS_H
18
19#include <cvc5/c/cvc5.h>
20
21/**
22 * Print solutions for synthesis conjecture to the stdout.
23 * @param nterms The number of terms.
24 * @param terms The terms for which the synthesis solutions were retrieved.
25 * @param sols The synthesis solutions of the given terms.
26 */
27void print_synth_solutions(size_t nterms,
28 const Cvc5Term terms[],
29 const Cvc5Term sols[]);
30
31#endif
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * Implementations of utility methods.
14 */
15
16#include "utils.h"
17
18#include <stdio.h>
19#include <stdlib.h>
20
21/**
22 * Get the string version of define-fun command.
23 * @param f The function to print.
24 * @param nparams The number of function parameters.
25 * @param params The function parameters.
26 * @param body The function body.
27 * @return A string version of define-fun.
28 */
29void print_define_fun(const Cvc5Term f,
30 size_t nparams,
31 const Cvc5Term params[],
32 const Cvc5Term body)
33{
34 Cvc5Sort sort = cvc5_term_get_sort(f);
35 if (cvc5_sort_is_fun(sort))
36 {
37 sort = cvc5_sort_fun_get_codomain(sort);
38 }
39 printf("(define-fun %s (", cvc5_term_to_string(f));
40 for (size_t i = 0; i < nparams; i++)
41 {
42 printf("%s", i > 0 ? " " : "");
43 printf("(%s %s)",
44 cvc5_term_to_string(params[i]),
45 cvc5_sort_to_string(cvc5_term_get_sort(params[i])));
46 }
47 printf(") %s %s)", cvc5_sort_to_string(sort), cvc5_term_to_string(body));
48}
49
50void print_synth_solutions(size_t nterms,
51 const Cvc5Term terms[],
52 const Cvc5Term sols[])
53{
54 printf("(\n");
55 for (size_t i = 0; i < nterms; i++)
56 {
57 size_t nparams = 0;
58 Cvc5Term* params = NULL;
59 Cvc5Term body = sols[i];
60 if (cvc5_term_get_kind(sols[i]) == CVC5_KIND_LAMBDA)
61 {
62 Cvc5Term psols = cvc5_term_get_child(sols[i], 0);
63 nparams = cvc5_term_get_num_children(psols);
64 params = (Cvc5Term*)malloc(nparams * sizeof(Cvc5Term));
65 for (size_t k = 0; k < nparams; k++)
66 {
67 params[k] = cvc5_term_get_child(psols, k);
68 }
69 body = cvc5_term_get_child(sols[i], 1);
70 }
71 printf(" ");
72 print_define_fun(terms[i], nterms, params, body);
73 if (params)
74 {
75 free(params);
76 }
77 printf("\n");
78 }
79 printf(")\n");
80}
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Abdalrhman Mohamed, Andres Noetzli
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * Utility methods.
14 */
15
16import io.github.cvc5.CVC5ApiException;
17import io.github.cvc5.Kind;
18import io.github.cvc5.Sort;
19import io.github.cvc5.Term;
20import java.util.ArrayList;
21import java.util.List;
22
23public class Utils
24{
25 /**
26 * Get the string version of define-fun command.
27 *
28 * @param f the function to print
29 * @param params the function parameters
30 * @param body the function body
31 * @return a string version of define-fun
32 */
33 private static String defineFunToString(Term f, Term[] params, Term body)
34 {
35 Sort sort = f.getSort();
36 if (sort.isFunction())
37 {
38 sort = sort.getFunctionCodomainSort();
39 }
40 StringBuilder ss = new StringBuilder();
41 ss.append("(define-fun ").append(f).append(" (");
42 for (int i = 0; i < params.length; ++i)
43 {
44 if (i > 0)
45 {
46 ss.append(' ');
47 }
48 ss.append('(').append(params[i]).append(' ').append(params[i].getSort()).append(')');
49 }
50 ss.append(") ").append(sort).append(' ').append(body).append(')');
51 return ss.toString();
52 }
53
54 /**
55 * Print solutions for synthesis conjecture to the standard output stream.
56 *
57 * @param terms the terms for which the synthesis solutions were retrieved
58 * @param sols the synthesis solutions of the given terms
59 */
60 public static void printSynthSolutions(Term[] terms, Term[] sols) throws CVC5ApiException
61 {
62 System.out.println('(');
63 for (int i = 0; i < terms.length; ++i)
64 {
65 List<Term> params = new ArrayList<>();
66 Term body = sols[i];
67 if (sols[i].getKind() == Kind.LAMBDA)
68 {
69 for (Term t : sols[i].getChild(0))
70 {
71 params.add(t);
72 }
73 body = sols[i].getChild(1);
74 }
75 System.out.println(" " + defineFunToString(terms[i], params.toArray(new Term[0]), body));
76 }
77 System.out.println(')');
78 }
79}
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Yoni Zohar, Abdalrhman Mohamed, Alex Ozdemir
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
9# in the top-level source directory and their institutional affiliations.
10# All rights reserved. See the file COPYING in the top-level source
11# directory for licensing information.
12# #############################################################################
13#
14# Utility Methods, translated from examples/api/utils.h
15##
16
17import cvc5
18from cvc5 import Kind
19
20# Get the string version of define-fun command.
21# @param f the function to print
22# @param params the function parameters
23# @param body the function body
24# @return a string version of define-fun
25
26
27def define_fun_to_string(f, params, body):
28 sort = f.getSort()
29 if sort.isFunction():
30 sort = f.getSort().getFunctionCodomainSort()
31 result = "(define-fun " + str(f) + " ("
32 for i in range(0, len(params)):
33 if i > 0:
34 result += " "
35 result += "(" + str(params[i]) + " " + str(params[i].getSort()) + ")"
36 result += ") " + str(sort) + " " + str(body) + ")"
37 return result
38
39
40# Print solutions for synthesis conjecture to the standard output stream.
41# @param terms the terms for which the synthesis solutions were retrieved
42# @param sols the synthesis solutions of the given terms
43
44
45def print_synth_solutions(terms, sols):
46 result = "(\n"
47 for i in range(0, len(terms)):
48 params = []
49 body = sols[i]
50 if sols[i].getKind() == Kind.LAMBDA:
51 params += sols[i][0]
52 body = sols[i][1]
53 result += " " + define_fun_to_string(terms[i], params, body) + "\n"
54 result += ")"
55 print(result)