Theory of Sequences
examples/api/cpp/sequences.cpp
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andres Noetzli, Mathias Preiner, Aina Niemetz
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 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
16 #include <cvc5/cvc5.h>
17
18 #include <iostream>
19
20 using namespace cvc5;
21
22 int main()
23 {
24 Solver slv;
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 std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl;
61
62 if (result.isSat())
63 {
64 std::cout << " x = " << slv.getValue(x) << std::endl;
65 std::cout << " y = " << slv.getValue(y) << std::endl;
66 }
67 }
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-2022 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
16 import static io.github.cvc5.Kind.*;
17
18 import io.github.cvc5.*;
19
20 public class Sequences
21 {
22 public static void main(String args[]) throws CVC5ApiException
23 {
24 try (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 }
69 }
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-2022 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
18 import cvc5
19 from cvc5 import Kind
20
21 if __name__ == "__main__":
22 slv = cvc5.Solver()
23 # Set the logic
24 slv.setLogic("QF_SLIA")
25 # Produce models
26 slv.setOption("produce-models", "true")
27 # The option strings-exp is needed
28 slv.setOption("strings-exp", "true")
29 # Set output language to SMTLIB2
30 slv.setOption("output-language", "smt2")
31
32 # Sequence sort
33 int_seq = slv.mkSequenceSort(slv.getIntegerSort())
34
35 # Sequence variables
36 x = slv.mkConst(int_seq, "x")
37 y = slv.mkConst(int_seq, "y")
38
39 # Empty sequence
40 empty = slv.mkEmptySequence(slv.getIntegerSort())
41 # Sequence concatenation: x.y.empty
42 concat = slv.mkTerm(Kind.SEQ_CONCAT, x, y, empty)
43 # Sequence length: |x.y.empty|
44 concat_len = slv.mkTerm(Kind.SEQ_LENGTH, concat)
45 # |x.y.empty| > 1
46 formula1 = slv.mkTerm(Kind.GT, concat_len, slv.mkInteger(1))
47 # Sequence unit: seq(1)
48 unit = slv.mkTerm(Kind.SEQ_UNIT, slv.mkInteger(1))
49 # x = seq(1)
50 formula2 = slv.mkTerm(Kind.EQUAL, x, unit)
51
52 # Make a query
53 q = slv.mkTerm(Kind.AND, formula1, formula2)
54
55 # Check satisfiability
56 result = slv.checkSatAssuming(q)
57 print("cvc5 reports:", q, "is", result)
58
59 if result:
60 print("x = {}".format(slv.getValue(x)))
61 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))