From f6bd42406897e165f2c9faffd69ab8db0204004f Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Mon, 20 Apr 2020 22:07:42 -0500 Subject: Introduce a public interface for Sygus commands. (#4204) This commit addresses issue #38 in cvc4-projects by introducing public API for Sygus commands. It also includes two simple examples of how to use the API. --- examples/api/CMakeLists.txt | 2 + examples/api/sygus-fun.cpp | 134 ++++++++++++++++++++++++++++++++++++++++++++ examples/api/sygus-inv.cpp | 89 +++++++++++++++++++++++++++++ 3 files changed, 225 insertions(+) create mode 100644 examples/api/sygus-fun.cpp create mode 100644 examples/api/sygus-inv.cpp (limited to 'examples/api') diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt index b121c8833..e4ef4ee78 100644 --- a/examples/api/CMakeLists.txt +++ b/examples/api/CMakeLists.txt @@ -17,6 +17,8 @@ set(CVC4_EXAMPLES_API sets-new strings strings-new + sygus-fun + sygus-inv ) foreach(example ${CVC4_EXAMPLES_API}) diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp new file mode 100644 index 000000000..d6437afa3 --- /dev/null +++ b/examples/api/sygus-fun.cpp @@ -0,0 +1,134 @@ +/********************* */ +/*! \file sygus-fun.cpp + ** \verbatim + ** Top contributors (to current version): + ** Abdalrhman Mohamed, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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.\endverbatim + ** + ** \brief 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 to 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 + +#include + +using namespace CVC4::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 function-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.mkReal(0); + Term one = slv.mkReal(1); + + Term plus = slv.mkTerm(PLUS, start, start); + Term minus = slv.mkTerm(PLUS, 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 function-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 logical 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)) + slv.printSynthSolution(std::cout); + } + + return 0; +} diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp new file mode 100644 index 000000000..061ad8c1f --- /dev/null +++ b/examples/api/sygus-inv.cpp @@ -0,0 +1,89 @@ +/********************* */ +/*! \file sygus-inv.cpp + ** \verbatim + ** Top contributors (to current version): + ** Abdalrhman Mohamed, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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.\endverbatim + ** + ** \brief 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 to this example should be equivalent to: + ** (define-fun inv-f ((x Int)) Bool (not (>= x 11))) + **/ + +#include + +#include + +using namespace CVC4::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(); + + Term zero = slv.mkReal(0); + Term one = slv.mkReal(1); + Term ten = slv.mkReal(10); + + // declare input variables for functions + Term x = slv.mkVar(integer, "x"); + Term xp = slv.mkVar(integer, "xp"); + + // (ite (< x 10) (= xp (+ x 1)) (= xp x)) + Term ite = slv.mkTerm(ITE, + slv.mkTerm(LT, x, ten), + slv.mkTerm(EQUAL, xp, slv.mkTerm(PLUS, x, one)), + slv.mkTerm(EQUAL, xp, x)); + + // define the pre-conditions, transition relations, and post-conditions + Term pre_f = slv.defineFun("pre-f", {x}, boolean, slv.mkTerm(EQUAL, x, zero)); + Term trans_f = slv.defineFun("trans-f", {x, xp}, boolean, ite); + Term post_f = slv.defineFun("post-f", {x}, boolean, slv.mkTerm(LEQ, x, ten)); + + // declare the invariant-to-synthesize. + Term inv_f = slv.synthInv("inv-f", {x}); + + slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f); + + // print solutions if available + if (slv.checkSynth().isUnsat()) + { + // Output should be equivalent to: + // (define-fun inv-f ((x Int)) Bool (not (>= x 11))) + slv.printSynthSolution(std::cout); + } + + return 0; +} -- cgit v1.2.3