1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
#!/usr/bin/env python
#####################
## sequences.py
## Top contributors (to current version):
## Andres Noetzli, Makai Mann, Mudathir Mohamed
## This file is part of the CVC4 project.
## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
## in the top-level source directory and their institutional affiliations.
## All rights reserved. See the file COPYING in the top-level source
## directory for licensing information.
##
## A simple demonstration of the solving capabilities of the CVC4
## strings solver through the Python API. This is a direct translation
## of sequences.cpp.
##
import pycvc4
from pycvc4 import kinds
if __name__ == "__main__":
slv = pycvc4.Solver()
# Set the logic
slv.setLogic("QF_SLIA")
# Produce models
slv.setOption("produce-models", "true")
# The option strings-exp is needed
slv.setOption("strings-exp", "true")
# Set output language to SMTLIB2
slv.setOption("output-language", "smt2")
# Sequence sort
int_seq = slv.mkSequenceSort(slv.getIntegerSort())
# Sequence variables
x = slv.mkConst(int_seq, "x")
y = slv.mkConst(int_seq, "y")
# Empty sequence
empty = slv.mkEmptySequence(slv.getIntegerSort())
# Sequence concatenation: x.y.empty
concat = slv.mkTerm(kinds.SeqConcat, x, y, empty)
# Sequence length: |x.y.empty|
concat_len = slv.mkTerm(kinds.SeqLength, concat)
# |x.y.empty| > 1
formula1 = slv.mkTerm(kinds.Gt, concat_len, slv.mkInteger(1))
# Sequence unit: seq(1)
unit = slv.mkTerm(kinds.SeqUnit, slv.mkInteger(1))
# x = seq(1)
formula2 = slv.mkTerm(kinds.Equal, x, unit)
# Make a query
q = slv.mkTerm(kinds.And, formula1, formula2)
# Check satisfiability
result = slv.checkSatAssuming(q)
print("CVC4 reports:", q, "is", result)
if result:
print("x = {}".format(slv.getValue(x)))
print("y = {}".format(slv.getValue(y)))
|
