diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-05-21 13:01:14 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-21 13:01:14 -0500 |
commit | 2c78f3bf696e7eb4b04f687e15b9569b9e1b8f23 (patch) | |
tree | ff490ec9c28be25ca7de7b201349b93935371027 /examples/api/sygus-grammar.cpp | |
parent | 3dc56426a37bf85f82ed6dc8cf15e4eb81498110 (diff) |
Make Grammar reusable. (#4506)
This PR modifies the Grammar implementation to make it reusable (i.e., can be copied or passed multiple times to synthFun/synthInv) with the catch that it becomes read-only after the first use.
Diffstat (limited to 'examples/api/sygus-grammar.cpp')
-rw-r--r-- | examples/api/sygus-grammar.cpp | 121 |
1 files changed, 121 insertions, 0 deletions
diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp new file mode 100644 index 000000000..c2e624c1f --- /dev/null +++ b/examples/api/sygus-grammar.cpp @@ -0,0 +1,121 @@ +/********************* */ +/*! \file sygus-grammar.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 id1 ((x Int)) Int + ** ((Start Int)) ((Start Int ((- x) (+ x Start))))) + ** + ** (synth-fun id2 ((x Int)) Int + ** ((Start Int)) ((Start Int ((Variable Int) (- x) (+ x Start))))) + ** + ** (synth-fun id3 ((x Int)) Int + ** ((Start Int)) ((Start Int (0 (- x) (+ x Start))))) + ** + ** (synth-fun id4 ((x Int)) Int + ** ((Start Int)) ((Start Int ((- x) (+ x Start))))) + ** + ** (declare-var x Int) + ** + ** (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) + ** + ** (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 <cvc4/api/cvc4cpp.h> + +#include <iostream> + +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"); + + // declare the grammar non-terminals + Term start = slv.mkVar(integer, "Start"); + + // define the rules + Term zero = slv.mkReal(0); + Term neg_x = slv.mkTerm(UMINUS, x); + Term plus = slv.mkTerm(PLUS, x, start); + + // create the grammar object + Grammar g1 = slv.mkSygusGrammar({x}, {start}); + + // bind each non-terminal to its rules + g1.addRules(start, {neg_x, plus}); + + // copy the first grammar with all of its non-termainals and their rules + Grammar g2 = g1; + Grammar g3 = g1; + + // add parameters as rules to the start symbol. Similar to "(Variable Int)" + g2.addAnyVariable(start); + + // declare the function-to-synthesizse + Term id1 = slv.synthFun("id1", {x}, integer, g1); + Term id2 = slv.synthFun("id2", {x}, integer, g2); + + g3.addRule(start, zero); + + Term id3 = slv.synthFun("id3", {x}, integer, g3); + + // g1 is reusable as long as it remains unmodified after first use + Term id4 = slv.synthFun("id4", {x}, integer, g1); + + // declare universal variables. + Term varX = slv.mkSygusVar(integer, "x"); + + Term id1_x = slv.mkTerm(APPLY_UF, id1, varX); + Term id2_x = slv.mkTerm(APPLY_UF, id2, varX); + Term id3_x = slv.mkTerm(APPLY_UF, id3, varX); + Term id4_x = slv.mkTerm(APPLY_UF, id4, varX); + + // add logical constraints + // (constraint (= (id1 x) (id2 x) x)) + slv.addSygusConstraint(slv.mkTerm(EQUAL, {id1_x, id2_x, id3_x, id4_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(std::cout); + } + + return 0; +} |