SyGuS: Functions

examples/api/cpp/sygus-fun.cpp

  1/******************************************************************************
  2 * Top contributors (to current version):
  3 *   Abdalrhman Mohamed, Mathias Preiner, Andrew Reynolds
  4 *
  5 * This file is part of the cvc5 project.
  6 *
  7 * Copyright (c) 2009-2022 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 max and min
 16 * functions.
 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  Solver slv;
 30
 31  // required options
 32  slv.setOption("sygus", "true");
 33  slv.setOption("incremental", "false");
 34
 35  // set the logic
 36  slv.setLogic("LIA");
 37
 38  Sort integer = slv.getIntegerSort();
 39  Sort boolean = slv.getBooleanSort();
 40
 41  // declare input variables for the functions-to-synthesize
 42  Term x = slv.mkVar(integer, "x");
 43  Term y = slv.mkVar(integer, "y");
 44
 45  // declare the grammar non-terminals
 46  Term start = slv.mkVar(integer, "Start");
 47  Term start_bool = slv.mkVar(boolean, "StartBool");
 48
 49  // define the rules
 50  Term zero = slv.mkInteger(0);
 51  Term one = slv.mkInteger(1);
 52
 53  Term plus = slv.mkTerm(Kind::ADD, {start, start});
 54  Term minus = slv.mkTerm(Kind::SUB, {start, start});
 55  Term ite = slv.mkTerm(Kind::ITE, {start_bool, start, start});
 56
 57  Term And = slv.mkTerm(Kind::AND, {start_bool, start_bool});
 58  Term Not = slv.mkTerm(Kind::NOT, {start_bool});
 59  Term leq = slv.mkTerm(Kind::LEQ, {start, start});
 60
 61  // create the grammar object
 62  Grammar g = slv.mkGrammar({x, y}, {start, start_bool});
 63
 64  // bind each non-terminal to its rules
 65  g.addRules(start, {zero, one, x, y, plus, minus, ite});
 66  g.addRules(start_bool, {And, Not, leq});
 67
 68  // declare the functions-to-synthesize. Optionally, provide the grammar
 69  // constraints
 70  Term max = slv.synthFun("max", {x, y}, integer, g);
 71  Term min = slv.synthFun("min", {x, y}, integer);
 72
 73  // declare universal variables.
 74  Term varX = slv.declareSygusVar("x", integer);
 75  Term varY = slv.declareSygusVar("y", integer);
 76
 77  Term max_x_y = slv.mkTerm(Kind::APPLY_UF, {max, varX, varY});
 78  Term min_x_y = slv.mkTerm(Kind::APPLY_UF, {min, varX, varY});
 79
 80  // add semantic constraints
 81  // (constraint (>= (max x y) x))
 82  slv.addSygusConstraint(slv.mkTerm(Kind::GEQ, {max_x_y, varX}));
 83
 84  // (constraint (>= (max x y) y))
 85  slv.addSygusConstraint(slv.mkTerm(Kind::GEQ, {max_x_y, varY}));
 86
 87  // (constraint (or (= x (max x y))
 88  //                 (= y (max x y))))
 89  slv.addSygusConstraint(
 90      slv.mkTerm(Kind::OR,
 91                 {slv.mkTerm(Kind::EQUAL, {max_x_y, varX}),
 92                  slv.mkTerm(Kind::EQUAL, {max_x_y, varY})}));
 93
 94  // (constraint (= (+ (max x y) (min x y))
 95  //                (+ x y)))
 96  slv.addSygusConstraint(slv.mkTerm(Kind::EQUAL,
 97                                    {slv.mkTerm(Kind::ADD, {max_x_y, min_x_y}),
 98                                     slv.mkTerm(Kind::ADD, {varX, varY})}));
 99
100  // print solutions if available
101  if (slv.checkSynth().hasSolution())
102  {
103    // Output should be equivalent to:
104    // (
105    //   (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
106    //   (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
107    // )
108    std::vector<Term> terms = {max, min};
109    utils::printSynthSolutions(terms, slv.getSynthSolutions(terms));
110  }
111
112  return 0;
113}

The utility method used for printing the synthesis solutions in the examples above is defined separately in the utils module:

examples/api/cpp/utils.h

 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-2022 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