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.

3 files changed, 225 insertions, 0 deletions

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 <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");
+  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 <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();
+
+  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;
+}