diff options
Diffstat (limited to 'examples/api/python/sequences.py')
| -rw-r--r-- | examples/api/python/sequences.py | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py index f9fd925fb..66a4c1353 100644 --- a/examples/api/python/sequences.py +++ b/examples/api/python/sequences.py @@ -16,7 +16,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": slv = pycvc5.Solver() @@ -39,18 +39,18 @@ if __name__ == "__main__": # Empty sequence empty = slv.mkEmptySequence(slv.getIntegerSort()) # Sequence concatenation: x.y.empty - concat = slv.mkTerm(kinds.SeqConcat, x, y, empty) + concat = slv.mkTerm(Kind.SeqConcat, x, y, empty) # Sequence length: |x.y.empty| - concat_len = slv.mkTerm(kinds.SeqLength, concat) + concat_len = slv.mkTerm(Kind.SeqLength, concat) # |x.y.empty| > 1 - formula1 = slv.mkTerm(kinds.Gt, concat_len, slv.mkInteger(1)) + formula1 = slv.mkTerm(Kind.Gt, concat_len, slv.mkInteger(1)) # Sequence unit: seq(1) - unit = slv.mkTerm(kinds.SeqUnit, slv.mkInteger(1)) + unit = slv.mkTerm(Kind.SeqUnit, slv.mkInteger(1)) # x = seq(1) - formula2 = slv.mkTerm(kinds.Equal, x, unit) + formula2 = slv.mkTerm(Kind.Equal, x, unit) # Make a query - q = slv.mkTerm(kinds.And, formula1, formula2) + q = slv.mkTerm(Kind.And, formula1, formula2) # Check satisfiability result = slv.checkSatAssuming(q) |