From a9b0e87897b95871916368d0dae780f53efcadd8 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Mon, 3 Aug 2020 14:02:35 -0700 Subject: [PATCH] Examples for using sygus python api (#4822) This PR adds examples for using the sygus python api. The examples are obtained from the examples of the cpp sygus api. --- examples/api/python/sygus-fun.py | 97 ++++++++++++++++++++++++++++ examples/api/python/sygus-grammar.py | 87 +++++++++++++++++++++++++ examples/api/python/sygus-inv.py | 66 +++++++++++++++++++ 3 files changed, 250 insertions(+) create mode 100644 examples/api/python/sygus-fun.py create mode 100644 examples/api/python/sygus-grammar.py create mode 100644 examples/api/python/sygus-inv.py diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py new file mode 100644 index 000000000..0f53bd343 --- /dev/null +++ b/examples/api/python/sygus-fun.py @@ -0,0 +1,97 @@ +#!/usr/bin/env python +##################### +#! \file sygus-fun.py +## \verbatim +## Top contributors (to current version): +## Yoni Zohar +## This file is part of the CVC4 project. +## Copyright (c) 2009-2018 by the authors listed in the file AUTHkinds.OrS +## 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 solving capabilities of the CVC4 +## sygus solver through the Python API. This is a direct +## translation of sygus-fun.cpp. +##################### + +import copy +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + + # required options + slv.setOption("lang", "sygus2") + slv.setOption("incremental", "false") + + # set the logic + slv.setLogic("LIA") + + integer = slv.getIntegerSort() + boolean = slv.getBooleanSort() + + # declare input variables for the functions-to-synthesize + x = slv.mkVar(integer, "x") + y = slv.mkVar(integer, "y") + + # declare the grammar non-terminals + start = slv.mkVar(integer, "Start") + start_bool = slv.mkVar(boolean, "StartBool") + + # define the rules + zero = slv.mkReal(0) + one = slv.mkReal(1) + + plus = slv.mkTerm(kinds.Plus, start, start) + minus = slv.mkTerm(kinds.Minus, start, start) + ite = slv.mkTerm(kinds.Ite, start_bool, start, start) + + And = slv.mkTerm(kinds.And, start_bool, start_bool) + Not = slv.mkTerm(kinds.Not, start_bool) + leq = slv.mkTerm(kinds.Leq, start, start) + + # create the grammar object + 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 + max = slv.synthFun("max", {x, y}, integer, g) + min = slv.synthFun("min", {x, y}, integer) + + # declare universal variables. + varX = slv.mkSygusVar(integer, "x") + varY = slv.mkSygusVar(integer, "y") + + max_x_y = slv.mkTerm(kinds.ApplyUf, max, varX, varY) + min_x_y = slv.mkTerm(kinds.ApplyUf, min, varX, varY) + + # add semantic constraints + # (constraint (>= (max x y) x)) + slv.addSygusConstraint(slv.mkTerm(kinds.Geq, max_x_y, varX)) + + # (constraint (>= (max x y) y)) + slv.addSygusConstraint(slv.mkTerm(kinds.Geq, max_x_y, varY)) + + # (constraint (or (= x (max x y)) + # (= y (max x y)))) + slv.addSygusConstraint(slv.mkTerm( + kinds.Or, slv.mkTerm(kinds.Equal, max_x_y, varX), slv.mkTerm(kinds.Equal, max_x_y, varY))) + + # (constraint (= (+ (max x y) (min x y)) + # (+ x y))) + slv.addSygusConstraint(slv.mkTerm( + kinds.Equal, slv.mkTerm(kinds.Plus, max_x_y, min_x_y), slv.mkTerm(kinds.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() + diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py new file mode 100644 index 000000000..efba88286 --- /dev/null +++ b/examples/api/python/sygus-grammar.py @@ -0,0 +1,87 @@ +#!/usr/bin/env python +##################### +#! \file sygus-grammar.py +## \verbatim +## Top contributors (to current version): +## Yoni Zohar +## This file is part of the CVC4 project. +## Copyright (c) 2009-2018 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 solving capabilities of the CVC4 +## sygus solver through the Python API. This is a direct +## translation of sygus-grammar.cpp. +import copy +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + + # required options + slv.setOption("lang", "sygus2") + slv.setOption("incremental", "false") + + # set the logic + slv.setLogic("LIA") + + integer = slv.getIntegerSort() + boolean = slv.getBooleanSort() + + # declare input variable for the function-to-synthesize + x = slv.mkVar(integer, "x") + + # declare the grammar non-terminal + start = slv.mkVar(integer, "Start") + + # define the rules + zero = slv.mkReal(0) + neg_x = slv.mkTerm(kinds.Uminus, x) + plus = slv.mkTerm(kinds.Plus, x, start) + + # create the grammar object + g1 = slv.mkSygusGrammar({x}, {start}) + g2 = slv.mkSygusGrammar({x}, {start}) + g3 = slv.mkSygusGrammar({x}, {start}) + + # bind each non-terminal to its rules + g1.addRules(start, {neg_x, plus}) + g2.addRules(start, {neg_x, plus}) + g3.addRules(start, {neg_x, plus}) + + # add parameters as rules for the start symbol. Similar to "(Variable Int)" + g2.addAnyVariable(start) + + # declare the functions-to-synthesize + id1 = slv.synthFun("id1", {x}, integer, g1) + id2 = slv.synthFun("id2", {x}, integer, g2) + + g3.addRule(start, zero) + + id3 = slv.synthFun("id3", {x}, integer, g3) + + # g1 is reusable as long as it remains unmodified after first use + id4 = slv.synthFun("id4", {x}, integer, g1) + + # declare universal variables. + varX = slv.mkSygusVar(integer, "x") + + id1_x = slv.mkTerm(kinds.ApplyUf, id1, varX) + id2_x = slv.mkTerm(kinds.ApplyUf, id2, varX) + id3_x = slv.mkTerm(kinds.ApplyUf, id3, varX) + id4_x = slv.mkTerm(kinds.ApplyUf, id4, varX) + + # add semantic constraints + # (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) + slv.addSygusConstraint(slv.mkTerm(kinds.And, [slv.mkTerm(kinds.Equal, id1_x, id2_x), slv.mkTerm(kinds.Equal, id1_x, id3_x), slv.mkTerm(kinds.Equal, id1_x, id4_x), slv.mkTerm(kinds.Equal, id1_x, varX)])) + + # print solutions if available + if (slv.checkSynth().isUnsat()): + # Output should be equivalent to: + # (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) + # (define-fun id2 ((x Int)) Int x) + # (define-fun id3 ((x Int)) Int (+ x 0)) + # (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) + slv.printSynthSolution() diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py new file mode 100644 index 000000000..cb21e1849 --- /dev/null +++ b/examples/api/python/sygus-inv.py @@ -0,0 +1,66 @@ +#!/usr/bin/env python + +##################### +#! \file sygus-inv.py +## \verbatim +## Top contributors (to current version): +## Yoni Zohar +## This file is part of the CVC4 project. +## Copyright (c) 2009-2018 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 solving capabilities of the CVC4 +## sygus solver through the Python API. This is a direct +## translation of sygus-inv.cpp . +##################### + +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + + # required options + slv.setOption("lang", "sygus2") + slv.setOption("incremental", "false") + + # set the logic + slv.setLogic("LIA") + + integer = slv.getIntegerSort() + boolean = slv.getBooleanSort() + + zero = slv.mkReal(0) + one = slv.mkReal(1) + ten = slv.mkReal(10) + + # declare input variables for functions + x = slv.mkVar(integer, "x") + xp = slv.mkVar(integer, "xp") + + # (ite (< x 10) (= xp (+ x 1)) (= xp x)) + ite = slv.mkTerm(kinds.Ite, + slv.mkTerm(kinds.Lt, x, ten), + slv.mkTerm(kinds.Equal, xp, slv.mkTerm(kinds.Plus, x, one)), + slv.mkTerm(kinds.Equal, xp, x)) + + # define the pre-conditions, transition relations, and post-conditions + pre_f = slv.defineFun("pre-f", {x}, boolean, slv.mkTerm(kinds.Equal, x, zero)) + trans_f = slv.defineFun("trans-f", {x, xp}, boolean, ite) + post_f = slv.defineFun("post-f", {x}, boolean, slv.mkTerm(kinds.Leq, x, ten)) + + # declare the invariant-to-synthesize + 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() + + + -- 2.30.2