Class: Udb::Z3FiniteArray

Inherits:
Object
  • Object
show all
Extended by:
T::Sig
Defined in:
lib/udb/z3.rb

Overview

Arrays in Z3 are unbounded, but we need to occasionally represent the length of an array therefore, we use this class to model a finite-sized array as a size plus constiuent scalars

Instance Method Summary collapse

Constructor Details

#initialize(solver, name, sort, max_n, bitvec_width: nil)

Parameters:

  • solver (Z3Solver)
  • name (String)
  • sort (T.class_of(Z3::IntSort), T.class_of(Z3::BoolSort), T.class_of(Z3::BitvecSort))
  • max_n (Integer)
  • bitvec_width (Integer, nil) (defaults to: nil) 


21
22
23
24
25
26
27
28
 
# File 'lib/udb/z3.rb', line 21

def initialize(solver, name, sort, max_n, bitvec_width: nil)
  @subtype_sort = sort
  @solver = solver
  @items = T.let([], T::Array[T.nilable(T.any(Z3::BitvecExpr, Z3::IntExpr, Z3::BoolExpr))])
  @size = Z3.Int("#{@name}_size")
  @max_size = max_n
  @bitvec_width = bitvec_width
end

Instance Method Details

#[](idx) ⇒ Z3::BitvecExpr, ...

Parameters:

  • idx (Integer)

Returns:

  • (Z3::BitvecExpr, Z3::IntExpr, Z3::BoolExpr) 


31
32
33
34
35
36
37
38
39
40
41
42
43
 
# File 'lib/udb/z3.rb', line 31

def [](idx)
  T.must(
    @items[idx] ||=
      begin
        @solver.assert @size >= idx
        if @subtype_sort == Z3::BitvecSort
          @subtype_sort.new(T.must(@bitvec_width)).var("#{@name}_i#{idx}")
        else
          @subtype_sort.new.var("#{@name}_i#{idx}")
        end
      end
  )
end

#max_size ⇒ Object 



47
 
# File 'lib/udb/z3.rb', line 47

def max_size = @max_size

#size_term ⇒ Object 



45
 
# File 'lib/udb/z3.rb', line 45

def size_term = @size