Added C++/Java api examples;

Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.

4 files changed, 179 insertions, 3 deletions

diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am
index a1455d168..1b3e0b086 100644
--- a/examples/api/Makefile.am
+++ b/examples/api/Makefile.am
@@ -12,7 +12,8 @@ noinst_PROGRAMS = \
 	datatypes \
 	helloworld \
 	linear_arith \
-	sets
+	sets \
+	strings
 
 noinst_DATA =
 
@@ -53,6 +54,11 @@ sets_SOURCES = \
 sets_LDADD = \
 	@builddir@/../../src/libcvc4.la
 
+strings_SOURCES = \
+	strings.cpp
+strings_LDADD = \
+	@builddir@/../../src/libcvc4.la
+
 # for installation
 examplesdir = $(docdir)/$(subdir)
 examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST)
diff --git a/examples/api/java/Makefile.am b/examples/api/java/Makefile.am
index 7216d758e..d12f2877e 100644
--- a/examples/api/java/Makefile.am
+++ b/examples/api/java/Makefile.am
@@ -9,7 +9,8 @@ noinst_DATA += \
 	HelloWorld.class \
 	LinearArith.class \
 	Datatypes.class \
-	PipedInput.class
+	PipedInput.class \
+	Strings.class
 endif
 
 %.class: %.java
@@ -23,7 +24,8 @@ EXTRA_DIST = \
 	HelloWorld.java \
 	LinearArith.java \
 	Datatypes.java \
-	PipedInput.java
+	PipedInput.java \
+	Strings.java
 
 # for installation
 examplesdir = $(docdir)/$(subdir)
diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java
new file mode 100644
index 000000000..293118d62
--- /dev/null
+++ b/examples/api/java/Strings.java
@@ -0,0 +1,67 @@
+/*********************                                                        */

+/*! \file Strings.java

+ ** \verbatim

+ ** Original author: Tianyi Liang

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 project.

+ ** Copyright (c) 2009-2014  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Reasoning about strings with CVC4 via Java API.

+ **

+ ** A simple demonstration of reasoning about strings with CVC4 via Jave API.

+ **/

+

+import edu.nyu.acsys.CVC4.*;

+

+public class Strings {

+  public static void main(String[] args) {

+    System.loadLibrary("cvc4jni");

+

+    ExprManager em = new ExprManager();

+    SmtEngine smt = new SmtEngine(em);

+

+    // Set the logic

+    smt.setLogic("S");

+

+    // Produce models

+    smt.setOption("produce-models", new SExpr(true));

+    // The option strings-exp is needed

+    smt.setOption("strings-exp", new SExpr(true));

+	// output-language

+    smt.setOption("output-language", new SExpr("smt2"));

+

+    // String type

+    Type string = em.stringType();

+

+    // Variables

+    Expr x = em.mkVar("x", string);

+    Expr y = em.mkVar("y", string);

+    Expr z = em.mkVar("z", string);

+

+    // String concatenation: x.y

+    Expr lhs = em.mkExpr(Kind.STRING_CONCAT, x, y);

+    // String concatenation: z.z

+    Expr rhs = em.mkExpr(Kind.STRING_CONCAT, z, z);;

+    // x.y = z.z

+    Expr formula1 = em.mkExpr(Kind.EQUAL, lhs, rhs);

+

+    // Length of y: |y|

+    Expr leny = em.mkExpr(Kind.STRING_LENGTH, y);

+    // |y| >= 1

+    Expr formula2 = em.mkExpr(Kind.GEQ, leny, em.mkConst(new Rational(1)));

+

+    // Make a query

+    Expr q = em.mkExpr(Kind.AND,

+      formula1,

+      formula2);

+

+     // check sat

+     Result result = smt.checkSat(q);

+     System.out.println("CVC4 reports: " + q + " is " + result + ".");

+

+     System.out.println("  x  = " + smt.getValue(x));

+  }

+}

diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp
new file mode 100644
index 000000000..a424c654a
--- /dev/null
+++ b/examples/api/strings.cpp
@@ -0,0 +1,101 @@
+/*********************                                                        */

+/*! \file sets.cpp

+ ** \verbatim

+ ** Original author: Tianyi Liang

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 project.

+ ** Copyright (c) 2009-2014  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Reasoning about strings with CVC4 via C++ API.

+ **

+ ** A simple demonstration of reasoning about strings with CVC4 via C++ API.

+ **/

+

+#include <iostream>

+

+//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed

+#include "smt/smt_engine.h"

+

+using namespace CVC4;

+

+int main() {

+  ExprManager em;

+  SmtEngine smt(&em);

+

+  // Set the logic

+  smt.setLogic("S");

+

+  // Produce models

+  smt.setOption("produce-models", true);

+

+  // The option strings-exp is needed

+  smt.setOption("strings-exp", true);

+

+  // Set output language to SMTLIB2

+  std::cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);

+  

+  // String type

+  Type string = em.stringType();

+

+  // std::string

+  std::string std_str_ab("ab");

+  // CVC4::String

+  CVC4::String cvc4_str_ab(std_str_ab);

+  CVC4::String cvc4_str_abc("abc");

+  // String constants

+  Expr ab  = em.mkConst(cvc4_str_ab);

+  Expr abc = em.mkConst(CVC4::String("abc"));

+  // String variables

+  Expr x = em.mkVar("x", string);

+  Expr y = em.mkVar("y", string);

+  Expr z = em.mkVar("z", string);

+

+  // String concatenation: x.ab.y

+  Expr lhs = em.mkExpr(kind::STRING_CONCAT, x, ab, y);

+  // String concatenation: abc.z

+  Expr rhs = em.mkExpr(kind::STRING_CONCAT, abc, z);

+  // x.ab.y = abc.z

+  Expr formula1 = em.mkExpr(kind::EQUAL, lhs, rhs);

+

+  // Length of y: |y|

+  Expr leny = em.mkExpr(kind::STRING_LENGTH, y);

+  // |y| >= 0

+  Expr formula2 = em.mkExpr(kind::GEQ, leny, em.mkConst(Rational(0)));

+

+  // Regular expression: (ab[c-e]*f)|g|h

+  Expr r = em.mkExpr(kind::REGEXP_UNION,

+    em.mkExpr(kind::REGEXP_CONCAT,

+      em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("ab"))),

+      em.mkExpr(kind::REGEXP_STAR,

+        em.mkExpr(kind::REGEXP_RANGE, em.mkConst(String("c")), em.mkConst(String("e")))),

+      em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("f")))),

+    em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("g"))),

+    em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("h"))));

+

+  // String variables

+  Expr s1 = em.mkVar("s1", string);

+  Expr s2 = em.mkVar("s2", string);

+  // String concatenation: s1.s2

+  Expr s = em.mkExpr(kind::STRING_CONCAT, s1, s2);

+

+  // s1.s2 in (ab[c-e]*f)|g|h

+  Expr formula3 = em.mkExpr(kind::STRING_IN_REGEXP, s, r);

+

+  // Make a query

+  Expr q = em.mkExpr(kind::AND,

+    formula1,

+    formula2,

+    formula3);

+

+  // check sat

+  Result result = smt.checkSat(q);

+  std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl;

+

+  if(result == Result::SAT) {

+    std::cout << "  x  = " << smt.getValue(x) << std::endl;

+    std::cout << "  s1.s2 = " << smt.getValue(s) << std::endl;

+  }

+}