SyGuS: Grammars ¶

  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 Grammar to add syntax constraints to
 16  * the Sygus solution for the identity function.
 17  */
 18 
 19 #include <cvc5/cvc5.h>
 20 
 21 #include <iostream>
 22 
 23 #include "utils.h"
 24 
 25 using namespace cvc5;
 26 
 27 int 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 
 40   // declare input variable for the function-to-synthesize
 41   Term x = slv.mkVar(integer, "x");
 42 
 43   // declare the grammar non-terminal
 44   Term start = slv.mkVar(integer, "Start");
 45 
 46   // define the rules
 47   Term zero = slv.mkInteger(0);
 48   Term neg_x = slv.mkTerm(NEG, {x});
 49   Term plus = slv.mkTerm(ADD, {x, start});
 50 
 51   // create the grammar object
 52   Grammar g1 = slv.mkGrammar({x}, {start});
 53 
 54   // bind each non-terminal to its rules
 55   g1.addRules(start, {neg_x, plus});
 56 
 57   // copy the first grammar with all of its non-termainals and their rules
 58   Grammar g2 = g1;
 59   Grammar g3 = g1;
 60 
 61   // add parameters as rules for the start symbol. Similar to "(Variable Int)"
 62   g2.addAnyVariable(start);
 63 
 64   // declare the functions-to-synthesize
 65   Term id1 = slv.synthFun("id1", {x}, integer, g1);
 66   Term id2 = slv.synthFun("id2", {x}, integer, g2);
 67 
 68   g3.addRule(start, zero);
 69 
 70   Term id3 = slv.synthFun("id3", {x}, integer, g3);
 71 
 72   // g1 is reusable as long as it remains unmodified after first use
 73   Term id4 = slv.synthFun("id4", {x}, integer, g1);
 74 
 75   // declare universal variables.
 76   Term varX = slv.declareSygusVar("x", integer);
 77 
 78   Term id1_x = slv.mkTerm(APPLY_UF, {id1, varX});
 79   Term id2_x = slv.mkTerm(APPLY_UF, {id2, varX});
 80   Term id3_x = slv.mkTerm(APPLY_UF, {id3, varX});
 81   Term id4_x = slv.mkTerm(APPLY_UF, {id4, varX});
 82 
 83   // add semantic constraints
 84   // (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x))
 85   slv.addSygusConstraint(
 86       slv.mkTerm(EQUAL, {{id1_x, id2_x, id3_x, id4_x, varX}}));
 87 
 88   // print solutions if available
 89   if (slv.checkSynth().hasSolution())
 90   {
 91     // Output should be equivalent to:
 92     // (
 93     //   (define-fun id1 ((x Int)) Int (+ x (+ x (- x))))
 94     //   (define-fun id2 ((x Int)) Int x)
 95     //   (define-fun id3 ((x Int)) Int (+ x 0))
 96     //   (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
 97     // )
 98     std::vector<Term> terms = {id1, id2, id3, id4};
 99     utils::printSynthSolutions(terms, slv.getSynthSolutions(terms));
100   }
101 
102   return 0;
103 }

 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 
21 namespace 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  */
28 void 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-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  * Implementations of utility methods.
14  */
15 
16 #include "utils.h"
17 
18 #include <iostream>
19 
20 namespace utils {
21 
22 using 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  */
31 std::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 
54 void 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::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