Arrays

Basic Array Term Builders

cvc5.pythonic.Array(name, dom, rng)

Return an array constant named name with the given domain and range sorts.

>>> a = Array('a', IntSort(), IntSort())
>>> a.sort()
Array(Int, Int)
>>> a[0]
a[0]

cvc5.pythonic.ConstArray(dom, v)

Return an SMT constant array expression.

>>> a = ConstArray(IntSort(), 10)
>>> a
ConstArray(Int, 10)
>>> a.sort()
Array(Int, Int)
>>> i = Int('i')
>>> a[i]
ConstArray(Int, 10)[i]
>>> simplify(a[i])
10

cvc5.pythonic.K(dom, v)

Return an SMT constant array expression. An alias for ConstArray.

>>> a = K(IntSort(), 10)
>>> a
ConstArray(Int, 10)
>>> a.sort()
Array(Int, Int)
>>> i = Int('i')
>>> a[i]
ConstArray(Int, 10)[i]
>>> simplify(a[i])
10

cvc5.pythonic.ArraySort(*sig)

Return the SMT array sort with the given domain and range sorts.

>>> A = ArraySort(IntSort(), BoolSort())
>>> A
Array(Int, Bool)
>>> A.domain()
Int
>>> A.range()
Bool
>>> AA = ArraySort(IntSort(), A)
>>> AA
Array(Int, Array(Int, Bool))
>>> try:
...  ArraySort(IntSort(), IntSort(), BoolSort())
... except SMTException as e:
...  print("failed: %s" % e)
failed: Unimplemented: multi-domain array

Array Operators

cvc5.pythonic.Select(a, i)

Return an SMT select array expression.

>>> a = Array('a', IntSort(), IntSort())
>>> i = Int('i')
>>> Select(a, i)
a[i]
>>> eq(Select(a, i), a[i])
True

cvc5.pythonic.Store(a, i, v)

Return an SMT store array expression.

>>> a    = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s    = Store(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j    = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved

cvc5.pythonic.Update(a, i, v)

Return an SMT store array expression. An alias for Store.

>>> a    = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s    = Update(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j    = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved

See the following operator overloads for building other kinds of array terms:

• select: cvc5.pythonic.ArrayRef.__getitem__()

Testers

cvc5.pythonic.is_array_sort(a)

Is this an array sort?

>>> is_array_sort(ArraySort(BoolSort(), BoolSort()))
True
>>> is_array_sort(BoolSort())
False

cvc5.pythonic.is_array(a)

Return True if a is an SMT array expression.

>>> a = Array('a', IntSort(), IntSort())
>>> is_array(a)
True
>>> is_array(Store(a, 0, 1))
True
>>> is_array(a[0])
False

cvc5.pythonic.is_const_array(a)

Return True if a is an SMT constant array.

>>> a = ConstArray(IntSort(), 10)
>>> is_const_array(a)
True
>>> a = Array('a', IntSort(), IntSort())
>>> is_const_array(a)
False

cvc5.pythonic.is_K(a)

Return True if a is an SMT constant array. An alias for is_const_array.

>>> a = ConstArray(IntSort(), 10)
>>> is_K(a)
True
>>> a = Array('a', IntSort(), IntSort())
>>> is_K(a)
False

cvc5.pythonic.is_select(a)

Return True if a is an SMT array select application.

>>> a = Array('a', IntSort(), IntSort())
>>> is_select(a)
False
>>> i = Int('i')
>>> is_select(a[i])
True

cvc5.pythonic.is_store(a)

Return True if a is an SMT array store application.

>>> a = Array('a', IntSort(), IntSort())
>>> is_store(a)
False
>>> is_store(Store(a, 0, 1))
True

cvc5.pythonic.is_update(a)

Return True if a is an SMT array store application. An alias for is_store.

>>> a = Array('a', IntSort(), IntSort())
>>> is_update(a)
False
>>> is_update(Update(a, 0, 1))
True

Classes (with overloads)

class cvc5.pythonic.ArraySortRef(ast, ctx=None)

Array sorts.

domain()

Return the domain of the array sort self.

>>> A = ArraySort(IntSort(), BoolSort())
>>> A.domain()
Int

range()

Return the range of the array sort self.

>>> A = ArraySort(IntSort(), BoolSort())
>>> A.range()
Bool

class cvc5.pythonic.ArrayRef(ast, ctx=None, reverse_children=False)

Array expressions.

__getitem__(arg)

Return the SMT expression self[arg].

>>> a = Array('a', IntSort(), BoolSort())
>>> i = Int('i')
>>> a[i]
a[i]
>>> a[i].sexpr()
'(select a i)'

arg(idx)

Get the “argument” (base element) of this constant array.

>>> b = ConstArray(IntSort(), 1)
>>> b.arg(0)
1

default()

Get the constant element of this (constant) array >>> b = ConstArray(IntSort(), 1) >>> b.default() 1

domain()

Shorthand for self.sort().domain().

>>> a = Array('a', IntSort(), BoolSort())
>>> a.domain()
Int

range()

Shorthand for self.sort().range().

>>> a = Array('a', IntSort(), BoolSort())
>>> a.range()
Bool

sort()

Return the array sort of the array expression self.

>>> a = Array('a', IntSort(), BoolSort())
>>> a.sort()
Array(Int, Bool)