Class: Z3::Expr

Inherits:
AST
  • Object
show all
Defined in:
lib/z3/expr/expr.rb

Instance Attribute Summary collapse

Attributes inherited from AST

#_ast

Class Method Summary collapse

Instance Method Summary collapse

Methods inherited from AST

#arguments, #ast_kind, #eql?, #func_decl, #hash, #sexpr, #simplify, #to_s

Constructor Details

#initialize(_ast, sort) ⇒ Expr

Returns a new instance of Expr.

Raises:



5
6
7
8
9
 
# File 'lib/z3/expr/expr.rb', line 5

def initialize(_ast, sort)
  super(_ast)
  @sort = sort
  raise Z3::Exception, "Values must have AST kind numeral, app, or quantifier" unless [:numeral, :app, :quantifier].include?(ast_kind)
end

Instance Attribute Details

#sort ⇒ Object (readonly)

Returns the value of attribute sort.



3
4
5
 
# File 'lib/z3/expr/expr.rb', line 3

def sort
  @sort
end

Class Method Details

.Add(*args) ⇒ Object

Raises:



152
153
154
155
156
157
158
159
160
161
162
163
164
165
 
# File 'lib/z3/expr/expr.rb', line 152

def Add(*args)
  raise Z3::Exception if args.empty?
  args = coerce_to_same_sort(*args)
  case args[0]
  when ArithExpr
    args[0].sort.new(LowLevel.mk_add(args))
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(LowLevel.mk_bvadd(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} exprs, only Int/Real/Bitvec"
  end
end

.And(*args) ⇒ Object 



108
109
110
111
112
113
114
115
116
117
118
119
120
 
# File 'lib/z3/expr/expr.rb', line 108

def And(*args)
  args = coerce_to_same_sort(*args)
  case args[0]
  when BoolExpr
    BoolSort.new.new(Z3::LowLevel.mk_and(args))
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(Z3::LowLevel.mk_bvand(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} exprs, only Bool and Bitvec"
  end
end

.coerce_to_same_sort(*args) ⇒ Object 



24
25
26
27
28
29
30
 
# File 'lib/z3/expr/expr.rb', line 24

def coerce_to_same_sort(*args)
  # This will raise exception unless one of the sorts is highest
  max_sort = args.map { |a| a.is_a?(Expr) ? a.sort : Expr.sort_for_const(a) }.max
  args.map do |a|
    max_sort.cast(a)
  end
end

.Distinct(*args) ⇒ Object 



103
104
105
106
 
# File 'lib/z3/expr/expr.rb', line 103

def Distinct(*args)
  args = coerce_to_same_sort(*args)
  BoolSort.new.new(LowLevel.mk_distinct(args))
end

.Eq(a, b) ⇒ Object 



98
99
100
101
 
# File 'lib/z3/expr/expr.rb', line 98

def Eq(a, b)
  a, b = coerce_to_same_sort(a, b)
  BoolSort.new.new(LowLevel.mk_eq(a, b))
end

.Ge(a, b) ⇒ Object 



62
63
64
65
66
67
68
69
70
71
72
 
# File 'lib/z3/expr/expr.rb', line 62

def Ge(a, b)
  a, b = coerce_to_same_sort(a, b)
  case a
  when ArithExpr
    BoolSort.new.new(LowLevel.mk_ge(a, b))
  when BitvecExpr
    raise Z3::Exception, "Use #signed_ge or #unsigned_ge for Bitvec, not >="
  else
    raise Z3::Exception, "Can't compare #{a.sort} values"
  end
end

.Gt(a, b) ⇒ Object 



50
51
52
53
54
55
56
57
58
59
60
 
# File 'lib/z3/expr/expr.rb', line 50

def Gt(a, b)
  a, b = coerce_to_same_sort(a, b)
  case a
  when ArithExpr
    BoolSort.new.new(LowLevel.mk_gt(a, b))
  when BitvecExpr
    raise Z3::Exception, "Use #signed_gt or #unsigned_gt for Bitvec, not >"
  else
    raise Z3::Exception, "Can't compare #{a.sort} values"
  end
end

.Le(a, b) ⇒ Object 



86
87
88
89
90
91
92
93
94
95
96
 
# File 'lib/z3/expr/expr.rb', line 86

def Le(a, b)
  a, b = coerce_to_same_sort(a, b)
  case a
  when ArithExpr
    BoolSort.new.new(LowLevel.mk_le(a, b))
  when BitvecExpr
    raise Z3::Exception, "Use #signed_le or #unsigned_le for Bitvec, not <="
  else
    raise Z3::Exception, "Can't compare #{a.sort} values"
  end
end

.Lt(a, b) ⇒ Object 



74
75
76
77
78
79
80
81
82
83
84
 
# File 'lib/z3/expr/expr.rb', line 74

def Lt(a, b)
  a, b = coerce_to_same_sort(a, b)
  case a
  when ArithExpr
    BoolSort.new.new(LowLevel.mk_lt(a, b))
  when BitvecExpr
    raise Z3::Exception, "Use #signed_lt or #unsigned_lt for Bitvec, not <"
  else
    raise Z3::Exception, "Can't compare #{a.sort} values"
  end
end

.Mul(*args) ⇒ Object 



181
182
183
184
185
186
187
188
189
190
191
192
193
 
# File 'lib/z3/expr/expr.rb', line 181

def Mul(*args)
  args = coerce_to_same_sort(*args)
  case args[0]
  when ArithExpr
    args[0].sort.new(LowLevel.mk_mul(args))
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(LowLevel.mk_bvmul(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} values, only Int/Real/Bitvec"
  end
end

.new_from_pointer(_ast) ⇒ Object 



45
46
47
48
 
# File 'lib/z3/expr/expr.rb', line 45

def new_from_pointer(_ast)
  _sort = Z3::VeryLowLevel.Z3_get_sort(Z3::LowLevel._ctx_pointer, _ast)
  Sort.from_pointer(_sort).new(_ast)
end

.Or(*args) ⇒ Object 



122
123
124
125
126
127
128
129
130
131
132
133
134
 
# File 'lib/z3/expr/expr.rb', line 122

def Or(*args)
  args = coerce_to_same_sort(*args)
  case args[0]
  when BoolExpr
    BoolSort.new.new(Z3::LowLevel.mk_or(args))
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(Z3::LowLevel.mk_bvor(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} exprs, only Bool and Bitvec"
  end
end

.sort_for_const(a) ⇒ Object 



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

def sort_for_const(a)
  case a
  when TrueClass, FalseClass
    BoolSort.new
  when Integer
    IntSort.new
  when Float, Rational
    RealSort.new
  else
    raise Z3::Exception, "No idea how to autoconvert `#{a.class}': `#{a.inspect}'"
  end
end

.Sub(*args) ⇒ Object 



167
168
169
170
171
172
173
174
175
176
177
178
179
 
# File 'lib/z3/expr/expr.rb', line 167

def Sub(*args)
  args = coerce_to_same_sort(*args)
  case args[0]
  when ArithExpr
    args[0].sort.new(LowLevel.mk_sub(args))
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(LowLevel.mk_bvsub(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} values, only Int/Real/Bitvec"
  end
end

.Xor(*args) ⇒ Object 



136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
 
# File 'lib/z3/expr/expr.rb', line 136

def Xor(*args)
  args = coerce_to_same_sort(*args)
  case args[0]
  when BoolExpr
    args.inject do |a, b|
      BoolSort.new.new(Z3::LowLevel.mk_xor(a, b))
    end
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(Z3::LowLevel.mk_bvxor(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} exprs, only Bool and Bitvec"
  end
end

Instance Method Details

#!=(other) ⇒ Object 



19
20
21
 
# File 'lib/z3/expr/expr.rb', line 19

def !=(other)
  Expr.Distinct(self, other)
end

#==(other) ⇒ Object 



15
16
17
 
# File 'lib/z3/expr/expr.rb', line 15

def ==(other)
  Expr.Eq(self, other)
end

#inspect ⇒ Object 



11
12
13
 
# File 'lib/z3/expr/expr.rb', line 11

def inspect
  "#{sort.to_s}<#{to_s}>"
end