Theory of Sequences
examples/api/cpp/sequences.cpp
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Andres Noetzli, Tianyi Liang
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 sequences via the 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
34 // Sequence sort
35 Sort intSeq = tm.mkSequenceSort(tm.getIntegerSort());
36
37 // Sequence variables
38 Term x = tm.mkConst(intSeq, "x");
39 Term y = tm.mkConst(intSeq, "y");
40
41 // Empty sequence
42 Term empty = tm.mkEmptySequence(tm.getIntegerSort());
43 // Sequence concatenation: x.y.empty
44 Term concat = tm.mkTerm(Kind::SEQ_CONCAT, {x, y, empty});
45 // Sequence length: |x.y.empty|
46 Term concat_len = tm.mkTerm(Kind::SEQ_LENGTH, {concat});
47 // |x.y.empty| > 1
48 Term formula1 = tm.mkTerm(Kind::GT, {concat_len, tm.mkInteger(1)});
49 // Sequence unit: seq(1)
50 Term unit = tm.mkTerm(Kind::SEQ_UNIT, {tm.mkInteger(1)});
51 // x = seq(1)
52 Term formula2 = tm.mkTerm(Kind::EQUAL, {x, unit});
53
54 // Make a query
55 Term q = tm.mkTerm(Kind::AND, {formula1, formula2});
56
57 // check sat
58 Result result = slv.checkSatAssuming(q);
59 std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl;
60
61 if (result.isSat())
62 {
63 std::cout << " x = " << slv.getValue(x) << std::endl;
64 std::cout << " y = " << slv.getValue(y) << std::endl;
65 }
66}
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz
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 sequences via the C API.
14 */
15
16#include <cvc5/c/cvc5.h>
17#include <stdio.h>
18
19int main()
20{
21 Cvc5TermManager* tm = cvc5_term_manager_new();
22 Cvc5* slv = cvc5_new(tm);
23
24 // Set the logic
25 cvc5_set_logic(slv, "QF_SLIA");
26 // Produce models
27 cvc5_set_option(slv, "produce-models", "true");
28 // The option strings-exp is needed
29 cvc5_set_option(slv, "strings-exp", "true");
30
31 // Sequence sort
32 Cvc5Sort int_seq = cvc5_mk_sequence_sort(tm, cvc5_get_integer_sort(tm));
33
34 // Sequence variables
35 Cvc5Term x = cvc5_mk_const(tm, int_seq, "x");
36 Cvc5Term y = cvc5_mk_const(tm, int_seq, "y");
37
38 // Empty sequence
39 Cvc5Term empty = cvc5_mk_empty_sequence(tm, cvc5_get_integer_sort(tm));
40 // Sequence concatenation: x.y.empty
41 Cvc5Term args3[3] = {x, y, empty};
42 Cvc5Term concat = cvc5_mk_term(tm, CVC5_KIND_SEQ_CONCAT, 3, args3);
43 // Sequence length: |x.y.empty|
44 Cvc5Term args1[1] = {concat};
45 Cvc5Term concat_len = cvc5_mk_term(tm, CVC5_KIND_SEQ_LENGTH, 1, args1);
46 // |x.y.empty| > 1
47 Cvc5Term args2[2] = {concat_len, cvc5_mk_integer_int64(tm, 1)};
48 Cvc5Term formula1 = cvc5_mk_term(tm, CVC5_KIND_GT, 2, args2);
49 // Sequence unit: seq(1)
50 args1[0] = cvc5_mk_integer_int64(tm, 1);
51 Cvc5Term unit = cvc5_mk_term(tm, CVC5_KIND_SEQ_UNIT, 1, args1);
52 // x = seq(1)
53 args2[0] = x;
54 args2[1] = unit;
55 Cvc5Term formula2 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
56
57 // Make a query
58 args2[0] = formula1;
59 args2[1] = formula2;
60 Cvc5Term q = cvc5_mk_term(tm, CVC5_KIND_AND, 2, args2);
61
62 // check sat
63 Cvc5Term assumptions[1] = {q};
64 Cvc5Result result = cvc5_check_sat_assuming(slv, 1, assumptions);
65 printf("cvc5 reports: %s is %s.\n",
66 cvc5_term_to_string(q),
67 cvc5_result_to_string(result));
68
69 if (cvc5_result_is_sat(result))
70 {
71 printf(" x = %s\n", cvc5_term_to_string(cvc5_get_value(slv, x)));
72 printf(" y = %s\n", cvc5_term_to_string(cvc5_get_value(slv, y)));
73 }
74
75 cvc5_delete(slv);
76 cvc5_term_manager_delete(tm);
77}
examples/api/java/Sequences.java
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, 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 sequences with cvc5 via C++ API.
14 */
15
16import static io.github.cvc5.Kind.*;
17
18import io.github.cvc5.*;
19
20public class Sequences
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 // Sequence sort
36 Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort());
37
38 // Sequence variables
39 Term x = slv.mkConst(intSeq, "x");
40 Term y = slv.mkConst(intSeq, "y");
41
42 // Empty sequence
43 Term empty = slv.mkEmptySequence(slv.getIntegerSort());
44 // Sequence concatenation: x.y.empty
45 Term concat = slv.mkTerm(SEQ_CONCAT, x, y, empty);
46 // Sequence length: |x.y.empty|
47 Term concat_len = slv.mkTerm(SEQ_LENGTH, concat);
48 // |x.y.empty| > 1
49 Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1));
50 // Sequence unit: seq(1)
51 Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1));
52 // x = seq(1)
53 Term formula2 = slv.mkTerm(EQUAL, x, unit);
54
55 // Make a query
56 Term q = slv.mkTerm(AND, formula1, formula2);
57
58 // check sat
59 Result result = slv.checkSatAssuming(q);
60 System.out.println("cvc5 reports: " + q + " is " + result + ".");
61
62 if (result.isSat())
63 {
64 System.out.println(" x = " + slv.getValue(x));
65 System.out.println(" y = " + slv.getValue(y));
66 }
67 }
68 Context.deletePointers();
69 }
70}
examples/api/python/pythonic/sequences.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 x = Const("x", SeqSort(IntSort()))
22 y = Const("y", SeqSort(IntSort()))
23
24 # Empty sequence
25 empty = Empty(SeqSort(IntSort()))
26 # Sequence concatenation: x.y.empty
27 concat = Concat( x, y, empty)
28 # Sequence length: |x.y.empty|
29 concat_len = Length(concat)
30 # |x.y.empty| > 1
31 formula1 = (concat_len > 1)
32 # Sequence unit: seq(1)
33 unit = Unit(IntVal(1))
34 # x = seq(1)
35 formula2 = (x == unit)
36
37 # Make a query
38 q = And(formula1, formula2)
39
40 # Check satisfiability
41 s = Solver()
42 result = s.check([q])
43 assert result == sat
44 m = s.model()
45 print("x = {}".format(m[x]))
46 print("y = {}".format(m[y]))
examples/api/python/sequences.py
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Andres Noetzli, Makai Mann, Aina Niemetz
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 sequences.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 # Sequence sort
34 int_seq = tm.mkSequenceSort(tm.getIntegerSort())
35
36 # Sequence variables
37 x = tm.mkConst(int_seq, "x")
38 y = tm.mkConst(int_seq, "y")
39
40 # Empty sequence
41 empty = tm.mkEmptySequence(tm.getIntegerSort())
42 # Sequence concatenation: x.y.empty
43 concat = tm.mkTerm(Kind.SEQ_CONCAT, x, y, empty)
44 # Sequence length: |x.y.empty|
45 concat_len = tm.mkTerm(Kind.SEQ_LENGTH, concat)
46 # |x.y.empty| > 1
47 formula1 = tm.mkTerm(Kind.GT, concat_len, tm.mkInteger(1))
48 # Sequence unit: seq(1)
49 unit = tm.mkTerm(Kind.SEQ_UNIT, tm.mkInteger(1))
50 # x = seq(1)
51 formula2 = tm.mkTerm(Kind.EQUAL, x, unit)
52
53 # Make a query
54 q = tm.mkTerm(Kind.AND, formula1, formula2)
55
56 # Check satisfiability
57 result = slv.checkSatAssuming(q)
58 print("cvc5 reports:", q, "is", result)
59
60 if result:
61 print("x = {}".format(slv.getValue(x)))
62 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))