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