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, #func_decl, #sexpr, #simplify, #to_s

Constructor Details

#initialize(_ast, sort) ⇒ Expr

Returns a new instance of Expr.

Raises:



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

def initialize(_ast, sort)
  super(_ast)
  @sort = sort
  raise Z3::Exception, "Values must have AST kind numeral or app" unless [:numeral, :app].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:



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

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 



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

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 #{a.sort} exprs, only Bool and Bitvec"
  end
end

.coerce_to_same_sort(*args) ⇒ Object 



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

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 



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

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

.Eq(a, b) ⇒ Object 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 #{a.sort} exprs, only Bool and Bitvec"
  end
end

.sort_for_const(a) ⇒ Object 



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

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 



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

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 



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

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 #{a.sort} exprs, only Bool and Bitvec"
  end
end

Instance Method Details

#!=(other) ⇒ Object 



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

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

#==(other) ⇒ Object 



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

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

#inspect ⇒ Object 



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

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