class Z3::Sort

Public Class Methods

Source

# File lib/z3/sort/sort.rb, line 120
def self.from_pointer(_sort)
  kind = VeryLowLevel.Z3_get_sort_kind(LowLevel._ctx_pointer, _sort)
  case kind
  when 0
    UninterpretedSort.new(name_from_pointer(_sort))
  when 1
    BoolSort.new
  when 2
    IntSort.new
  when 3
    RealSort.new
  when 4
    n = VeryLowLevel.Z3_get_bv_sort_size(LowLevel._ctx_pointer, _sort)
    BitvecSort.new(n)
  when 5
    domain = from_pointer(VeryLowLevel.Z3_get_array_sort_domain(LowLevel._ctx_pointer, _sort))
    range = from_pointer(VeryLowLevel.Z3_get_array_sort_range(LowLevel._ctx_pointer, _sort))
    if range == BoolSort.new
      SetSort.new(domain)
    else
      ArraySort.new(domain, range)
    end
  when 6
    # Rebuilt rather than redeclared - see EnumSort.from_pointer
    EnumSort.from_pointer(_sort)
  when 8
    FiniteDomainSort.new(
      name_from_pointer(_sort),
      LowLevel.get_finite_domain_sort_size(_sort),
    )
  when 9
    e = VeryLowLevel.Z3_fpa_get_ebits(LowLevel._ctx_pointer, _sort)
    s = VeryLowLevel.Z3_fpa_get_sbits(LowLevel._ctx_pointer, _sort)
    FloatSort.new(e, s)
  when 10
    RoundingModeSort.new
  when 11
    # SeqSort.new turns Seq(Char) back into a StringSort, just like Set(X) is really Array(X, Bool)
    SeqSort.new(from_pointer(VeryLowLevel.Z3_get_seq_sort_basis(LowLevel._ctx_pointer, _sort)))
  when 12
    seq_sort = from_pointer(VeryLowLevel.Z3_get_re_sort_basis(LowLevel._ctx_pointer, _sort))
    ReSort.new(seq_sort)
  when 13
    CharSort.new
  when 14
    TypeVariableSort.new(name_from_pointer(_sort))
  else
    raise Z3::Exception, "Unknown sort kind #{kind}"
  end
end

name_from_pointer (_sort)

Source

# File lib/z3/sort/sort.rb, line 173
def self.name_from_pointer(_sort)
  LowLevel.symbol_value(VeryLowLevel.Z3_get_sort_name(LowLevel._ctx_pointer, _sort))
end

Sorts with a name (uninterpreted, finite domain, enum, type variable) need it to be rebuilt. Takes a raw pointer, as from_pointer needs it before there’s a Sort.

new (_ast)

Source

# File lib/z3/sort/sort.rb, line 3
def initialize(_ast)
  super(_ast)
  raise Z3::Exception, "Sorts must have AST kind sort" unless ast_kind == :sort
end

Calls superclass method

Public Instance Methods

< (other)

Source

# File lib/z3/sort/sort.rb, line 20
def <(other)
  raise ArgumentError unless other.is_a?(Sort)
  other > self
end

Reimplementing Comparable Check if it can handle partial orders OK

<= (other)

Source

# File lib/z3/sort/sort.rb, line 30
def <=(other)
  raise ArgumentError unless other.is_a?(Sort)
  other >= self
end

<=> (other)

Source

# File lib/z3/sort/sort.rb, line 35
def <=>(other)
  raise ArgumentError unless other.is_a?(Sort)
  return 0 if self == other
  return 1 if self > other
  return -1 if other > self
  nil
end

== (other)

Source

# File lib/z3/sort/sort.rb, line 9
def ==(other)
  other.is_a?(Sort) and @_ast == other._ast
end

> (other)

Source

# File lib/z3/sort/sort.rb, line 13
def >(other)
  raise ArgumentError unless other.is_a?(Sort)
  false
end

>= (other)

Source

# File lib/z3/sort/sort.rb, line 25
def >=(other)
  raise ArgumentError unless other.is_a?(Sort)
  self == other or self > other
end

cant_convert (value)

Source

# File lib/z3/sort/sort.rb, line 116
def cant_convert(value)
  Z3::Exception.new("Can't convert #{AST.describe(value)} into #{self}")
end

Every failed conversion into a sort goes through here, so they’re all worded the way Ruby words its own: ‘Integer(nil)` says “can’t convert nil into Integer”

cast (a)

Source

# File lib/z3/sort/sort.rb, line 102
def cast(a)
  if a.is_a?(Expr)
    if  a.sort == self
      a
    else
      from_value(a)
    end
  else
    from_const(a)
  end
end

eql? (other)

Source

# File lib/z3/sort/sort.rb, line 47
def eql?(other)
  self == other
end

fresh_var (prefix)

Source

# File lib/z3/sort/sort.rb, line 84
def fresh_var(prefix)
  new(LowLevel.mk_fresh_const(prefix.to_s, self))
end

A variable Z3 names for you, by appending a number to ‘prefix` - for the ones you need but don’t want to have to name, and which mustn’t collide with anything the caller has named.

‘Z3.Const` is a different thing entirely: that’s a literal built from a Ruby value, where this is a variable, which is what Z3 calls a const.

The number comes from a counter shared by the whole context, and by FuncDecl.declare_fresh too, so don’t count on getting any particular one.

from_value (v)

Source

# File lib/z3/sort/sort.rb, line 97
def from_value(v)
  return v if v.sort == self
  raise cant_convert(v)
end

hash ()

Source

# File lib/z3/sort/sort.rb, line 54
def hash
  _ast.address
end

Z3 hash-conses sorts, and Set(X) is really Array(X, Bool), so two sorts can be

while their Ruby classes differ. hash has to follow the pointer like eql? does,

or sorts which are eql? would end up in different Hash buckets.

inspect ()

Source

# File lib/z3/sort/sort.rb, line 58
def inspect
  "#{self}Sort"
end

new (_ast)

Source

# File lib/z3/sort/sort.rb, line 89
def new(_ast)
  expr_class.new(_ast, self)
end

We pretend to be a class, sort of

to_s ()

Source

# File lib/z3/sort/sort.rb, line 43
def to_s
  LowLevel.ast_to_string(self)
end

value_class ()

Source

# File lib/z3/sort/sort.rb, line 93
def value_class
  raise "SubclassResponsibility"
end

var (name)

Source

# File lib/z3/sort/sort.rb, line 62
def var(name)
  if name.is_a?(Enumerable)
    name.map{|v| var(v)}
  else
    new(
      LowLevel.mk_const(
        LowLevel.mk_string_symbol(name),
        self,
      )
    )
  end
end