diff options
Diffstat (limited to 'examples/api/cpp/sygus-fun.cpp')
-rw-r--r-- | examples/api/cpp/sygus-fun.cpp | 142 |
1 files changed, 142 insertions, 0 deletions
diff --git a/examples/api/cpp/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp new file mode 100644 index 000000000..0f96e72a7 --- /dev/null +++ b/examples/api/cpp/sygus-fun.cpp @@ -0,0 +1,142 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * 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)) + * ) + */ + +#include <cvc5/cvc5.h> + +#include <iostream> + +#include "utils.h" + +using namespace cvc5::api; + +int main() +{ + Solver slv; + + // required options + slv.setOption("lang", "sygus2"); + slv.setOption("incremental", "false"); + + // set the logic + slv.setLogic("LIA"); + + Sort integer = slv.getIntegerSort(); + Sort boolean = slv.getBooleanSort(); + + // declare input variables for the functions-to-synthesize + Term x = slv.mkVar(integer, "x"); + Term y = slv.mkVar(integer, "y"); + + // declare the grammar non-terminals + Term start = slv.mkVar(integer, "Start"); + Term start_bool = slv.mkVar(boolean, "StartBool"); + + // define the rules + Term zero = slv.mkInteger(0); + Term one = slv.mkInteger(1); + + Term plus = slv.mkTerm(PLUS, start, start); + Term minus = slv.mkTerm(MINUS, start, start); + Term ite = slv.mkTerm(ITE, start_bool, start, start); + + Term And = slv.mkTerm(AND, start_bool, start_bool); + Term Not = slv.mkTerm(NOT, start_bool); + Term leq = slv.mkTerm(LEQ, start, start); + + // create the grammar object + Grammar g = slv.mkSygusGrammar({x, y}, {start, start_bool}); + + // bind each non-terminal to its rules + g.addRules(start, {zero, one, x, y, plus, minus, ite}); + g.addRules(start_bool, {And, Not, leq}); + + // declare the functions-to-synthesize. Optionally, provide the grammar + // constraints + Term max = slv.synthFun("max", {x, y}, integer, g); + Term min = slv.synthFun("min", {x, y}, integer); + + // declare universal variables. + Term varX = slv.mkSygusVar(integer, "x"); + Term varY = slv.mkSygusVar(integer, "y"); + + Term max_x_y = slv.mkTerm(APPLY_UF, max, varX, varY); + Term min_x_y = slv.mkTerm(APPLY_UF, min, varX, varY); + + // add semantic constraints + // (constraint (>= (max x y) x)) + slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varX)); + + // (constraint (>= (max x y) y)) + slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varY)); + + // (constraint (or (= x (max x y)) + // (= y (max x y)))) + slv.addSygusConstraint(slv.mkTerm( + OR, slv.mkTerm(EQUAL, max_x_y, varX), slv.mkTerm(EQUAL, max_x_y, varY))); + + // (constraint (= (+ (max x y) (min x y)) + // (+ x y))) + slv.addSygusConstraint(slv.mkTerm( + EQUAL, slv.mkTerm(PLUS, max_x_y, min_x_y), slv.mkTerm(PLUS, varX, varY))); + + // print solutions if available + if (slv.checkSynth().isUnsat()) + { + // Output 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)) + // ) + std::vector<Term> terms = {max, min}; + printSynthSolutions(terms, slv.getSynthSolutions(terms)); + } + + return 0; +} |