From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Sat, 6 Dec 2014 21:28:52 +0000 (-0600)
Subject: Added string constant in java api example.
X-Git-Tag: cvc5-1.0.0~6468
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3bb096fbdbf7ac1e24a6a5935c591aa84d50af89;p=cvc5.git

Added string constant in java api example.
---

diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java
index 293118d62..9437115a9 100644
--- a/examples/api/java/Strings.java
+++ b/examples/api/java/Strings.java
@@ -36,32 +36,56 @@ public class Strings {
     // String type
     Type string = em.stringType();
 
+    // String constants
+    Expr ab  = em.mkConst(new CVC4String("ab"));
+    Expr abc = em.mkConst(new CVC4String("abc"));
     // 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
+    // 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| >= 1
-    Expr formula2 = em.mkExpr(Kind.GEQ, leny, em.mkConst(new Rational(1)));
+    // |y| >= 0
+    Expr formula2 = em.mkExpr(Kind.GEQ, leny, em.mkConst(new Rational(0)));
 
-    // Make a query
+    // 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(new CVC4String("ab"))),
+        em.mkExpr(Kind.REGEXP_STAR,
+          em.mkExpr(Kind.REGEXP_RANGE, em.mkConst(new CVC4String("c")), em.mkConst(new CVC4String("e")))),
+        em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("f")))),
+      em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("g"))),
+      em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("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);
+      formula2,
+      formula3);
 
      // check sat
      Result result = smt.checkSat(q);
      System.out.println("CVC4 reports: " + q + " is " + result + ".");
 
      System.out.println("  x  = " + smt.getValue(x));
+     System.out.println("  s1.s2 = " + smt.getValue(s));
   }
 }