Theory of Strings
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Tianyi Liang, Mathias Preiner
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 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.
11 * ****************************************************************************
12 *
13 * A simple demonstration of reasoning about strings with cvc5 via C++ API.
14 */
15
16#include <cvc5/cvc5.h>
17
18#include <iostream>
19
20using namespace cvc5;
21
22int main()
23{
24 TermManager tm;
25 Solver slv(tm);
26
27 // Set the logic
28 slv.setLogic("QF_SLIA");
29 // Produce models
30 slv.setOption("produce-models", "true");
31 // The option strings-exp is needed
32 slv.setOption("strings-exp", "true");
33 // Set output language to SMTLIB2
34 slv.setOption("output-language", "smt2");
35
36 // String type
37 Sort string = tm.getStringSort();
38
39 // std::string
40 std::string str_ab("ab");
41 // String constants
42 Term ab = tm.mkString(str_ab);
43 Term abc = tm.mkString("abc");
44 // String variables
45 Term x = tm.mkConst(string, "x");
46 Term y = tm.mkConst(string, "y");
47 Term z = tm.mkConst(string, "z");
48
49 // String concatenation: x.ab.y
50 Term lhs = tm.mkTerm(Kind::STRING_CONCAT, {x, ab, y});
51 // String concatenation: abc.z
52 Term rhs = tm.mkTerm(Kind::STRING_CONCAT, {abc, z});
53 // x.ab.y = abc.z
54 Term formula1 = tm.mkTerm(Kind::EQUAL, {lhs, rhs});
55
56 // Length of y: |y|
57 Term leny = tm.mkTerm(Kind::STRING_LENGTH, {y});
58 // |y| >= 0
59 Term formula2 = tm.mkTerm(Kind::GEQ, {leny, tm.mkInteger(0)});
60
61 // Regular expression: (ab[c-e]*f)|g|h
62 Term r = tm.mkTerm(
63 Kind::REGEXP_UNION,
64
65 {tm.mkTerm(Kind::REGEXP_CONCAT,
66 {tm.mkTerm(Kind::STRING_TO_REGEXP, {tm.mkString("ab")}),
67 tm.mkTerm(Kind::REGEXP_STAR,
68 {tm.mkTerm(Kind::REGEXP_RANGE,
69 {tm.mkString("c"), tm.mkString("e")})}),
70 tm.mkTerm(Kind::STRING_TO_REGEXP, {tm.mkString("f")})}),
71 tm.mkTerm(Kind::STRING_TO_REGEXP, {tm.mkString("g")}),
72 tm.mkTerm(Kind::STRING_TO_REGEXP, {tm.mkString("h")})});
73
74 // String variables
75 Term s1 = tm.mkConst(string, "s1");
76 Term s2 = tm.mkConst(string, "s2");
77 // String concatenation: s1.s2
78 Term s = tm.mkTerm(Kind::STRING_CONCAT, {s1, s2});
79
80 // s1.s2 in (ab[c-e]*f)|g|h
81 Term formula3 = tm.mkTerm(Kind::STRING_IN_REGEXP, {s, r});
82
83 // Make a query
84 Term q = tm.mkTerm(Kind::AND, {formula1, formula2, formula3});
85
86 // check sat
87 Result result = slv.checkSatAssuming(q);
88 std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl;
89
90 if(result.isSat())
91 {
92 std::cout << " x = " << slv.getValue(x) << std::endl;
93 std::cout << " s1.s2 = " << slv.getValue(s) << std::endl;
94 }
95}
examples/api/java/Strings.java
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Tianyi Liang, Andres Noetzli
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 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.
11 * ****************************************************************************
12 *
13 * A simple demonstration of reasoning about strings with cvc5 via C++ API.
14 */
15
16import static io.github.cvc5.Kind.*;
17
18import io.github.cvc5.*;
19
20public class Strings
21{
22 public static void main(String args[]) throws CVC5ApiException
23 {
24 Solver slv = new Solver();
25 {
26 // Set the logic
27 slv.setLogic("QF_SLIA");
28 // Produce models
29 slv.setOption("produce-models", "true");
30 // The option strings-exp is needed
31 slv.setOption("strings-exp", "true");
32 // Set output language to SMTLIB2
33 slv.setOption("output-language", "smt2");
34
35 // String type
36 Sort string = slv.getStringSort();
37
38 // std::string
39 String str_ab = "ab";
40 // String constants
41 Term ab = slv.mkString(str_ab);
42 Term abc = slv.mkString("abc");
43 // String variables
44 Term x = slv.mkConst(string, "x");
45 Term y = slv.mkConst(string, "y");
46 Term z = slv.mkConst(string, "z");
47
48 // String concatenation: x.ab.y
49 Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y);
50 // String concatenation: abc.z
51 Term rhs = slv.mkTerm(STRING_CONCAT, abc, z);
52 // x.ab.y = abc.z
53 Term formula1 = slv.mkTerm(EQUAL, lhs, rhs);
54
55 // Length of y: |y|
56 Term leny = slv.mkTerm(STRING_LENGTH, y);
57 // |y| >= 0
58 Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0));
59
60 // Regular expression: (ab[c-e]*f)|g|h
61 Term r = slv.mkTerm(REGEXP_UNION,
62 slv.mkTerm(REGEXP_CONCAT,
63 slv.mkTerm(STRING_TO_REGEXP, slv.mkString("ab")),
64 slv.mkTerm(
65 REGEXP_STAR, slv.mkTerm(REGEXP_RANGE, slv.mkString("c"), slv.mkString("e"))),
66 slv.mkTerm(STRING_TO_REGEXP, slv.mkString("f"))),
67 slv.mkTerm(STRING_TO_REGEXP, slv.mkString("g")),
68 slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h")));
69
70 // String variables
71 Term s1 = slv.mkConst(string, "s1");
72 Term s2 = slv.mkConst(string, "s2");
73 // String concatenation: s1.s2
74 Term s = slv.mkTerm(STRING_CONCAT, s1, s2);
75
76 // s1.s2 in (ab[c-e]*f)|g|h
77 Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r);
78
79 // Make a query
80 Term q = slv.mkTerm(AND, formula1, formula2, formula3);
81
82 // check sat
83 Result result = slv.checkSatAssuming(q);
84 System.out.println("cvc5 reports: " + q + " is " + result + ".");
85
86 if (result.isSat())
87 {
88 System.out.println(" x = " + slv.getValue(x));
89 System.out.println(" s1.s2 = " + slv.getValue(s));
90 }
91 }
92 Context.deletePointers();
93 }
94}
examples/api/python/pythonic/strings.py
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Yoni Zohar
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
9# in the top-level source directory and their institutional affiliations.
10# All rights reserved. See the file COPYING in the top-level source
11# directory for licensing information.
12# ############################################################################
13#
14# A simple demonstration of the solving capabilities of the cvc5 strings solver. A simple translation of the base python API
15# example.
16##
17
18from cvc5.pythonic import *
19
20if __name__ == "__main__":
21
22 str_ab = "ab"
23 # String constants
24 ab = StringVal(str_ab)
25 abc = StringVal("abc")
26 # String variables
27 x = String("x")
28 y = String("y")
29 z = String("z")
30
31 # String concatenation: x.ab.y
32 lhs = Concat(x, ab, y)
33 # String concatenation: abc.z
34 rhs = Concat(abc, z)
35 # x.ab.y = abc.z
36 formula1 = (lhs == rhs)
37
38 # Length of y: |y|
39 leny = Length(y)
40 # |y| >= 0
41 formula2 = leny >= 0
42
43 # Regular expression: (ab[c-e]*f)|g|h
44 r = Union(Concat(Re("ab"), Star(Range("c", "e")), Re("f")), Re("g"), Re("h"))
45
46
47 # String variables
48 s1 = String("s1")
49 s2 = String("s2")
50 # String concatenation: s1.s2
51 s = Concat(s1, s2)
52
53 # s1.s2 in (ab[c-e]*f)|g|h
54 formula3 = InRe(s,r)
55
56 # Make a query
57 q = And(formula1, formula2, formula3)
58
59 # check sat
60 s = Solver()
61 s.add(q)
62 assert sat == s.check()
63 m = s.model()
64 print("x = ", m[x])
65 print(" s1.s2 =", m[Concat(s1, s2)])
examples/api/python/strings.py
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Makai Mann, Aina Niemetz, Alex Ozdemir
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
9# in the top-level source directory and their institutional affiliations.
10# All rights reserved. See the file COPYING in the top-level source
11# directory for licensing information.
12# #############################################################################
13#
14# A simple demonstration of the solving capabilities of the cvc5 strings solver
15# through the Python API. This is a direct translation of strings-new.cpp.
16##
17
18import cvc5
19from cvc5 import Kind
20
21if __name__ == "__main__":
22 tm = cvc5.TermManager()
23 slv = cvc5.Solver(tm)
24 # Set the logic
25 slv.setLogic("QF_SLIA")
26 # Produce models
27 slv.setOption("produce-models", "true")
28 # The option strings-exp is needed
29 slv.setOption("strings-exp", "true")
30 # Set output language to SMTLIB2
31 slv.setOption("output-language", "smt2")
32
33 # String type
34 string = tm.getStringSort()
35
36 # std::string
37 str_ab = "ab"
38 # String constants
39 ab = tm.mkString(str_ab)
40 abc = tm.mkString("abc")
41 # String variables
42 x = tm.mkConst(string, "x")
43 y = tm.mkConst(string, "y")
44 z = tm.mkConst(string, "z")
45
46 # String concatenation: x.ab.y
47 lhs = tm.mkTerm(Kind.STRING_CONCAT, x, ab, y)
48 # String concatenation: abc.z
49 rhs = tm.mkTerm(Kind.STRING_CONCAT, abc, z)
50 # x.ab.y = abc.z
51 formula1 = tm.mkTerm(Kind.EQUAL, lhs, rhs)
52
53 # Length of y: |y|
54 leny = tm.mkTerm(Kind.STRING_LENGTH, y)
55 # |y| >= 0
56 formula2 = tm.mkTerm(Kind.GEQ, leny, tm.mkInteger(0))
57
58 # Regular expression: (ab[c-e]*f)|g|h
59 r = tm.mkTerm(Kind.REGEXP_UNION,
60 tm.mkTerm(Kind.REGEXP_CONCAT,
61 tm.mkTerm(Kind.STRING_TO_REGEXP,
62 tm.mkString("ab")),
63 tm.mkTerm(Kind.REGEXP_STAR,
64 tm.mkTerm(Kind.REGEXP_RANGE,
65 tm.mkString("c"),
66 tm.mkString("e"))),
67 tm.mkTerm(Kind.STRING_TO_REGEXP,
68 tm.mkString("f"))),
69 tm.mkTerm(Kind.STRING_TO_REGEXP, tm.mkString("g")),
70 tm.mkTerm(Kind.STRING_TO_REGEXP, tm.mkString("h")))
71
72 # String variables
73 s1 = tm.mkConst(string, "s1")
74 s2 = tm.mkConst(string, "s2")
75 # String concatenation: s1.s2
76 s = tm.mkTerm(Kind.STRING_CONCAT, s1, s2)
77
78 # s1.s2 in (ab[c-e]*f)|g|h
79 formula3 = tm.mkTerm(Kind.STRING_IN_REGEXP, s, r)
80
81 # Make a query
82 q = tm.mkTerm(Kind.AND, formula1, formula2, formula3)
83
84 # check sat
85 result = slv.checkSatAssuming(q)
86 print("cvc5 reports:", q, "is", result)
87
88 if result:
89 print("x = ", slv.getValue(x))
90 print(" s1.s2 =", slv.getValue(s))
examples/api/smtlib/strings.smt2
1(set-logic QF_SLIA)
2(set-option :produce-models true)
3
4(define-const ab String "ab")
5(define-const abc String "abc")
6
7(declare-const x String)
8(declare-const y String)
9(declare-const z String)
10
11; x.ab.y = abc.z
12(assert (= (str.++ x ab y) (str.++ abc z)))
13; |y| >= 0
14(assert (>= (str.len y) 0))
15
16; Regular expression: (ab[c-e]*f)|g|h
17(define-const r RegLan
18 (re.union
19 (re.++ (str.to_re "ab") (re.* (re.range "c" "e")) (str.to_re "f"))
20 (str.to_re "f")
21 (str.to_re "h")
22 )
23 )
24
25; s1.s2 in (ab[c-e]*f)|g|h
26(assert (str.in_re (str.++ "s1" "s2") r))
27
28(check-sat)