1 /*********************                                                        */
2 /*! \file Strings.java
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Tianyi Liang
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8  ** in the top-level source directory) and their institutional affiliations.
9  ** All rights reserved.  See the file COPYING in the top-level source
10  ** directory for licensing information.\endverbatim
11  **
12  ** \brief Reasoning about strings with CVC4 via Java API.
13  **
14  ** A simple demonstration of reasoning about strings with CVC4 via Jave API.
15  **/
16 
17 import edu.nyu.acsys.CVC4.*;
18 
19 public class Strings {
main(String[] args)20   public static void main(String[] args) {
21     System.loadLibrary("cvc4jni");
22 
23     ExprManager em = new ExprManager();
24     SmtEngine smt = new SmtEngine(em);
25 
26     // Set the logic
27     smt.setLogic("S");
28 
29     // Produce models
30     smt.setOption("produce-models", new SExpr(true));
31     // The option strings-exp is needed
32     smt.setOption("strings-exp", new SExpr(true));
33 	// output-language
34     smt.setOption("output-language", new SExpr("smt2"));
35 
36     // String type
37     Type string = em.stringType();
38 
39     // String constants
40     Expr ab  = em.mkConst(new CVC4String("ab"));
41     Expr abc = em.mkConst(new CVC4String("abc"));
42     // Variables
43     Expr x = em.mkVar("x", string);
44     Expr y = em.mkVar("y", string);
45     Expr z = em.mkVar("z", string);
46 
47     // String concatenation: x.ab.y
48     Expr lhs = em.mkExpr(Kind.STRING_CONCAT, x, ab, y);
49     // String concatenation: abc.z
50     Expr rhs = em.mkExpr(Kind.STRING_CONCAT, abc, z);;
51     // x.ab.y = abc.z
52     Expr formula1 = em.mkExpr(Kind.EQUAL, lhs, rhs);
53 
54     // Length of y: |y|
55     Expr leny = em.mkExpr(Kind.STRING_LENGTH, y);
56     // |y| >= 0
57     Expr formula2 = em.mkExpr(Kind.GEQ, leny, em.mkConst(new Rational(0)));
58 
59     // Regular expression: (ab[c-e]*f)|g|h
60     Expr r = em.mkExpr(Kind.REGEXP_UNION,
61       em.mkExpr(Kind.REGEXP_CONCAT,
62         em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("ab"))),
63         em.mkExpr(Kind.REGEXP_STAR,
64           em.mkExpr(Kind.REGEXP_RANGE, em.mkConst(new CVC4String("c")), em.mkConst(new CVC4String("e")))),
65         em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("f")))),
66       em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("g"))),
67       em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("h"))));
68 
69     // String variables
70     Expr s1 = em.mkVar("s1", string);
71     Expr s2 = em.mkVar("s2", string);
72     // String concatenation: s1.s2
73     Expr s = em.mkExpr(Kind.STRING_CONCAT, s1, s2);
74 
75     // s1.s2 in (ab[c-e]*f)|g|h
76     Expr formula3 = em.mkExpr(Kind.STRING_IN_REGEXP, s, r);
77 
78 	// Make a query
79     Expr q = em.mkExpr(Kind.AND,
80       formula1,
81       formula2,
82       formula3);
83 
84      // check sat
85      Result result = smt.checkSat(q);
86      System.out.println("CVC4 reports: " + q + " is " + result + ".");
87 
88      System.out.println("  x  = " + smt.getValue(x));
89      System.out.println("  s1.s2 = " + smt.getValue(s));
90   }
91 }
92