Class: Udb::Z3FiniteArray

Inherits:

Object

• Object
• Udb::Z3FiniteArray

Extended by:

T::Sig

Defined in:

lib/udb/z3.rb

Overview

Models a finite-sized array in Z3 using explicit scalar variables

Z3 arrays are normally unbounded, but we need finite arrays with explicit size for parameter validation. This class models an array as:

• A size variable (Z3::IntExpr)

• Individual scalar variables for each potential element

Limitations:

• Cannot truly represent unbounded arrays (would require ForAll/Exists quantifiers not available in the Z3 Ruby bindings)

• Maximum practical size is 64 elements (hardcoded limit)

• Arrays larger than 64 are capped at 64 with an error if more are needed

Instance Method Summary

• #!=(ary) ⇒ Object
• #==(ary) ⇒ Object
• #[](idx) ⇒ Object
• #constrain_element(i, v) ⇒ Object
• #has_value?(val) ⇒ Boolean
• #initialize(solver, name, sort, constraints, bitvec_width: nil) ⇒ Z3FiniteArray constructor

  A new instance of Z3FiniteArray.

• #max_size ⇒ Object
• #size_term ⇒ Object

Constructor Details

#initialize(solver, name, sort, constraints, bitvec_width: nil) ⇒ Z3FiniteArray

Returns a new instance of Z3FiniteArray.

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

def initialize(solver, name, sort, constraints, bitvec_width: nil)
  @name = name
  @solver = solver
  @subtype_sort =
    T.let(
      if sort == Z3::BitvecSort
        sort.new(T.must(bitvec_width))
      else
        sort.new
      end,
      Z3::Sort
    )
  @constraints = constraints
  # Determine array size: use max_size if specified, otherwise cap at 64
  # The 64-element limit is a practical constraint to keep the solver tractable
  @num_items =
    T.let(
      if @constraints.max_size.nil?
        64
      else
        if T.must(@constraints.max_size) > 64
          64
        else
          T.must(@constraints.max_size)
        end
      end,
      Integer
    )
  # Create Z3 variables for each array element and apply constraints
  @items = T.let(
    Array.new(@num_items) { |index|
      v = @subtype_sort.var("#{@name}_idx#{index}")
      constrain_element(index, v)
    },
    T::Array[T.any(Z3::BitvecExpr, Z3::IntExpr, Z3::BoolExpr)]
  )
  # Create a size variable to track the logical array length
  @size = T.let(Z3.Int("#{@name}_size"), Z3::IntExpr)
  unless @constraints.min_size.nil?
    solver.assert_as @size >= @constraints.min_size, "#{@name}_size_lower_bound"
  end
  unless @constraints.max_size.nil?
    solver.assert_as @size <= @constraints.max_size, "#{@name}_size_upper_bound"
  end
  # Handle "contains" constraint: at least one element must match the schema
  unless @constraints.contains.nil?
    target_value = @subtype_sort.var("#{@name}_contain_value")
    T.must(@constraints.contains).mthd.call(@solver, target_value, T.must(@constraints.contains).schema, assert: true)
    exprs = @items.map do |item|
      item == target_value
    end
    solver.assert T.unsafe(Z3).Or(*exprs)
  end
  # Handle uniqueness constraint: all elements must be distinct
  if @constraints.unique
    solver.assert T.unsafe(Z3).Distinct(*@items)
  end
end

Instance Method Details

#!=(ary) ⇒ Object

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

def !=(ary)
  ~(self == ary)
end

#==(ary) ⇒ Object

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

def ==(ary)
  if ary.empty?
    @size == 0
  elsif ary.size > @num_items
    # Check if this is a real constraint violation or just our 64-element limit
    if @constraints.max_size.nil?
      # This is an artificial limit from our 64-element cap
      raise "Comparison of array larger than proof model can handle. May need to increase the 64-entry limit"
    elsif T.must(@constraints.max_size) > @num_items
      raise "Comparison of array larger than proof model can handle. May need to increase the 64-entry limit"
    else
      # Array can't be equal because it exceeds the schema's max_size
      return Z3.False
    end
  elsif !@constraints.min_size.nil? && (ary.size < T.must(@constraints.min_size))
    # Array is too small to satisfy min_size constraint
    return Z3.False
  else
    # Build equality expression: size matches and all elements match
    exprs = ary.each_index.map do |i|
      # Use hash for strings since Z3 doesn't have native string support
      @items.fetch(i) == (ary[i].is_a?(String) ? ary[i].hash : ary[i])
    end
    T.unsafe(Z3).And(@size == ary.size, *exprs)
  end
end

#[](idx) ⇒ Object

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

def [](idx)
  if idx >= @num_items
    raise "array index (#{idx}) is out of bounds (#{@num_items}). May need to increase the upper limit of Z3FiniteArray from 64"
  end
  @items.fetch(idx)
end

#constrain_element(i, v) ⇒ Object

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

def constrain_element(i, v)
  if !@constraints.item_by_idx.empty?
    already_constrained = T.let(false, T::Boolean)
    @constraints.item_by_idx.each do |idx, typ_constr|
      if idx == i
        already_constrained = true
        assertions =
          typ_constr.mthd.call(@solver, v, typ_constr.schema, assert: false)
        assertions.each { |a| @solver.assert a }
      end
    end
    # Apply general schema if no position-specific schema was found
    if !already_constrained && !@constraints.item_rest.nil?
      assertions =
        T.must(@constraints.item_rest).mthd.call(@solver, v, T.must(@constraints.item_rest).schema, assert: false)
      assertions.each { |a| @solver.assert a }
    end
  elsif !@constraints.item_rest.nil?
    T.must(@constraints.item_rest).mthd.call(@solver, v, T.must(@constraints.item_rest).schema)
  end
  v
end

#has_value?(val) ⇒ Boolean

Returns:

• (Boolean)

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

def has_value?(val)
  exprs = @items.each_with_index.map do |i, idx|
    # Use hash for strings since Z3 doesn't have native string support
    (i == (val.is_a?(String) ? val.hash : val)) & (@size > idx)
  end
  T.unsafe(Z3).Or(*exprs)
end

#max_size ⇒ Object

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

def max_size = @constraints.max_size

#size_term ⇒ Object

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

def size_term = @size