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)

               