Theory of Sequences
examples/api/cpp/sequences.cpp
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of reasoning about sequences via the C++ API.
11 */
12
13#include <cvc5/cvc5.h>
14
15#include <iostream>
16
17using namespace cvc5;
18
19int main()
20{
21 TermManager tm;
22 Solver slv(tm);
23
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
31 // Sequence sort
32 Sort intSeq = tm.mkSequenceSort(tm.getIntegerSort());
33
34 // Sequence variables
35 Term x = tm.mkConst(intSeq, "x");
36 Term y = tm.mkConst(intSeq, "y");
37
38 // Empty sequence
39 Term empty = tm.mkEmptySequence(tm.getIntegerSort());
40 // Sequence concatenation: x.y.empty
41 Term concat = tm.mkTerm(Kind::SEQ_CONCAT, {x, y, empty});
42 // Sequence length: |x.y.empty|
43 Term concat_len = tm.mkTerm(Kind::SEQ_LENGTH, {concat});
44 // |x.y.empty| > 1
45 Term formula1 = tm.mkTerm(Kind::GT, {concat_len, tm.mkInteger(1)});
46 // Sequence unit: seq(1)
47 Term unit = tm.mkTerm(Kind::SEQ_UNIT, {tm.mkInteger(1)});
48 // x = seq(1)
49 Term formula2 = tm.mkTerm(Kind::EQUAL, {x, unit});
50
51 // Make a query
52 Term q = tm.mkTerm(Kind::AND, {formula1, formula2});
53
54 // check sat
55 Result result = slv.checkSatAssuming(q);
56 std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl;
57
58 if (result.isSat())
59 {
60 std::cout << " x = " << slv.getValue(x) << std::endl;
61 std::cout << " y = " << slv.getValue(y) << std::endl;
62 }
63}
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of reasoning about sequences via the C API.
11 */
12
13#include <cvc5/c/cvc5.h>
14#include <stdio.h>
15
16int main()
17{
18 Cvc5TermManager* tm = cvc5_term_manager_new();
19 Cvc5* slv = cvc5_new(tm);
20
21 // Set the logic
22 cvc5_set_logic(slv, "QF_SLIA");
23 // Produce models
24 cvc5_set_option(slv, "produce-models", "true");
25 // The option strings-exp is needed
26 cvc5_set_option(slv, "strings-exp", "true");
27
28 // Sequence sort
29 Cvc5Sort int_seq = cvc5_mk_sequence_sort(tm, cvc5_get_integer_sort(tm));
30
31 // Sequence variables
32 Cvc5Term x = cvc5_mk_const(tm, int_seq, "x");
33 Cvc5Term y = cvc5_mk_const(tm, int_seq, "y");
34
35 // Empty sequence
36 Cvc5Term empty = cvc5_mk_empty_sequence(tm, cvc5_get_integer_sort(tm));
37 // Sequence concatenation: x.y.empty
38 Cvc5Term args3[3] = {x, y, empty};
39 Cvc5Term concat = cvc5_mk_term(tm, CVC5_KIND_SEQ_CONCAT, 3, args3);
40 // Sequence length: |x.y.empty|
41 Cvc5Term args1[1] = {concat};
42 Cvc5Term concat_len = cvc5_mk_term(tm, CVC5_KIND_SEQ_LENGTH, 1, args1);
43 // |x.y.empty| > 1
44 Cvc5Term args2[2] = {concat_len, cvc5_mk_integer_int64(tm, 1)};
45 Cvc5Term formula1 = cvc5_mk_term(tm, CVC5_KIND_GT, 2, args2);
46 // Sequence unit: seq(1)
47 args1[0] = cvc5_mk_integer_int64(tm, 1);
48 Cvc5Term unit = cvc5_mk_term(tm, CVC5_KIND_SEQ_UNIT, 1, args1);
49 // x = seq(1)
50 args2[0] = x;
51 args2[1] = unit;
52 Cvc5Term formula2 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
53
54 // Make a query
55 args2[0] = formula1;
56 args2[1] = formula2;
57 Cvc5Term q = cvc5_mk_term(tm, CVC5_KIND_AND, 2, args2);
58
59 // check sat
60 Cvc5Term assumptions[1] = {q};
61 Cvc5Result result = cvc5_check_sat_assuming(slv, 1, assumptions);
62 printf("cvc5 reports: %s is %s.\n",
63 cvc5_term_to_string(q),
64 cvc5_result_to_string(result));
65
66 if (cvc5_result_is_sat(result))
67 {
68 printf(" x = %s\n", cvc5_term_to_string(cvc5_get_value(slv, x)));
69 printf(" y = %s\n", cvc5_term_to_string(cvc5_get_value(slv, y)));
70 }
71
72 cvc5_delete(slv);
73 cvc5_term_manager_delete(tm);
74}
examples/api/java/Sequences.java
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of reasoning about sequences with cvc5 via C++ API.
11 */
12
13import static io.github.cvc5.Kind.*;
14
15import io.github.cvc5.*;
16
17public class Sequences
18{
19 public static void main(String args[]) throws CVC5ApiException
20 {
21 TermManager tm = new TermManager();
22 Solver slv = new Solver(tm);
23 {
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 // Sequence sort
34 Sort intSeq = tm.mkSequenceSort(tm.getIntegerSort());
35
36 // Sequence variables
37 Term x = tm.mkConst(intSeq, "x");
38 Term y = tm.mkConst(intSeq, "y");
39
40 // Empty sequence
41 Term empty = tm.mkEmptySequence(tm.getIntegerSort());
42 // Sequence concatenation: x.y.empty
43 Term concat = tm.mkTerm(SEQ_CONCAT, x, y, empty);
44 // Sequence length: |x.y.empty|
45 Term concat_len = tm.mkTerm(SEQ_LENGTH, concat);
46 // |x.y.empty| > 1
47 Term formula1 = tm.mkTerm(GT, concat_len, tm.mkInteger(1));
48 // Sequence unit: seq(1)
49 Term unit = tm.mkTerm(SEQ_UNIT, tm.mkInteger(1));
50 // x = seq(1)
51 Term formula2 = tm.mkTerm(EQUAL, x, unit);
52
53 // Make a query
54 Term q = tm.mkTerm(AND, formula1, formula2);
55
56 // check sat
57 Result result = slv.checkSatAssuming(q);
58 System.out.println("cvc5 reports: " + q + " is " + result + ".");
59
60 if (result.isSat())
61 {
62 System.out.println(" x = " + slv.getValue(x));
63 System.out.println(" y = " + slv.getValue(y));
64 }
65 }
66 Context.deletePointers();
67 }
68}
examples/api/python/pythonic/sequences.py
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# A simple demonstration of the solving capabilities of the cvc5 strings
12# solver. A simple translation of the base python API example.
13##
14
15from cvc5.pythonic import *
16
17if __name__ == "__main__":
18 x = Const("x", SeqSort(IntSort()))
19 y = Const("y", SeqSort(IntSort()))
20
21 # Empty sequence
22 empty = Empty(SeqSort(IntSort()))
23 # Sequence concatenation: x.y.empty
24 concat = Concat( x, y, empty)
25 # Sequence length: |x.y.empty|
26 concat_len = Length(concat)
27 # |x.y.empty| > 1
28 formula1 = (concat_len > 1)
29 # Sequence unit: seq(1)
30 unit = Unit(IntVal(1))
31 # x = seq(1)
32 formula2 = (x == unit)
33
34 # Make a query
35 q = And(formula1, formula2)
36
37 # Check satisfiability
38 s = Solver()
39 result = s.check([q])
40 assert result == sat
41 m = s.model()
42 print("x = {}".format(m[x]))
43 print("y = {}".format(m[y]))
examples/api/python/sequences.py
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# A simple demonstration of the solving capabilities of the cvc5 strings solver
12# through the Python API. This is a direct translation of sequences.cpp.
13##
14
15import cvc5
16from cvc5 import Kind
17
18if __name__ == "__main__":
19 tm = cvc5.TermManager()
20 slv = cvc5.Solver(tm)
21 # Set the logic
22 slv.setLogic("QF_SLIA")
23 # Produce models
24 slv.setOption("produce-models", "true")
25 # The option strings-exp is needed
26 slv.setOption("strings-exp", "true")
27 # Set output language to SMTLIB2
28 slv.setOption("output-language", "smt2")
29
30 # Sequence sort
31 int_seq = tm.mkSequenceSort(tm.getIntegerSort())
32
33 # Sequence variables
34 x = tm.mkConst(int_seq, "x")
35 y = tm.mkConst(int_seq, "y")
36
37 # Empty sequence
38 empty = tm.mkEmptySequence(tm.getIntegerSort())
39 # Sequence concatenation: x.y.empty
40 concat = tm.mkTerm(Kind.SEQ_CONCAT, x, y, empty)
41 # Sequence length: |x.y.empty|
42 concat_len = tm.mkTerm(Kind.SEQ_LENGTH, concat)
43 # |x.y.empty| > 1
44 formula1 = tm.mkTerm(Kind.GT, concat_len, tm.mkInteger(1))
45 # Sequence unit: seq(1)
46 unit = tm.mkTerm(Kind.SEQ_UNIT, tm.mkInteger(1))
47 # x = seq(1)
48 formula2 = tm.mkTerm(Kind.EQUAL, x, unit)
49
50 # Make a query
51 q = tm.mkTerm(Kind.AND, formula1, formula2)
52
53 # Check satisfiability
54 result = slv.checkSatAssuming(q)
55 print("cvc5 reports:", q, "is", result)
56
57 if result:
58 print("x = {}".format(slv.getValue(x)))
59 print("y = {}".format(slv.getValue(y)))
examples/api/smtlib/sequences.smt2
1(set-logic QF_SLIA)
2(set-option :produce-models true)
3
4; create integer sequence constants
5(declare-const x (Seq Int))
6(declare-const y (Seq Int))
7
8; |x.y.empty| > 1
9(assert (> (seq.len (seq.++ x y (as seq.empty (Seq Int)))) 1))
10; x = seq(1)
11(assert (= x (seq.unit 1)))
12
13(check-sat)
14(get-value (x y))