Added string constant in java api example.

diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java
index 293118d62af4fd04e7a76ccbce1155d7c5e9d33f..9437115a9c32fc5a64a4199e1d79098a91aa7ba1 100644 (file)
--- a/examples/api/java/Strings.java
+++ b/examples/api/java/Strings.java
@@ -36,32 +36,56 @@ public class Strings {
     // String type\r
     Type string = em.stringType();\r
 \r
+    // String constants\r
+    Expr ab  = em.mkConst(new CVC4String("ab"));\r
+    Expr abc = em.mkConst(new CVC4String("abc"));\r
     // Variables\r
     Expr x = em.mkVar("x", string);\r
     Expr y = em.mkVar("y", string);\r
     Expr z = em.mkVar("z", string);\r
 \r
-    // String concatenation: x.y\r
-    Expr lhs = em.mkExpr(Kind.STRING_CONCAT, x, y);\r
-    // String concatenation: z.z\r
-    Expr rhs = em.mkExpr(Kind.STRING_CONCAT, z, z);;\r
-    // x.y = z.z\r
+    // String concatenation: x.ab.y\r
+    Expr lhs = em.mkExpr(Kind.STRING_CONCAT, x, ab, y);\r
+    // String concatenation: abc.z\r
+    Expr rhs = em.mkExpr(Kind.STRING_CONCAT, abc, z);;\r
+    // x.ab.y = abc.z\r
     Expr formula1 = em.mkExpr(Kind.EQUAL, lhs, rhs);\r
 \r
     // Length of y: |y|\r
     Expr leny = em.mkExpr(Kind.STRING_LENGTH, y);\r
-    // |y| >= 1\r
-    Expr formula2 = em.mkExpr(Kind.GEQ, leny, em.mkConst(new Rational(1)));\r
+    // |y| >= 0\r
+    Expr formula2 = em.mkExpr(Kind.GEQ, leny, em.mkConst(new Rational(0)));\r
 \r
-    // Make a query\r
+    // Regular expression: (ab[c-e]*f)|g|h\r
+    Expr r = em.mkExpr(Kind.REGEXP_UNION,\r
+      em.mkExpr(Kind.REGEXP_CONCAT,\r
+        em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("ab"))),\r
+        em.mkExpr(Kind.REGEXP_STAR,\r
+          em.mkExpr(Kind.REGEXP_RANGE, em.mkConst(new CVC4String("c")), em.mkConst(new CVC4String("e")))),\r
+        em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("f")))),\r
+      em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("g"))),\r
+      em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("h"))));\r
+\r
+    // String variables\r
+    Expr s1 = em.mkVar("s1", string);\r
+    Expr s2 = em.mkVar("s2", string);\r
+    // String concatenation: s1.s2\r
+    Expr s = em.mkExpr(Kind.STRING_CONCAT, s1, s2);\r
+\r
+    // s1.s2 in (ab[c-e]*f)|g|h\r
+    Expr formula3 = em.mkExpr(Kind.STRING_IN_REGEXP, s, r);\r
+\r
+       // Make a query\r
     Expr q = em.mkExpr(Kind.AND,\r
       formula1,\r
-      formula2);\r
+      formula2,\r
+      formula3);\r
 \r
      // check sat\r
      Result result = smt.checkSat(q);\r
      System.out.println("CVC4 reports: " + q + " is " + result + ".");\r
 \r
      System.out.println("  x  = " + smt.getValue(x));\r
+     System.out.println("  s1.s2 = " + smt.getValue(s));\r
   }\r
 }\r