class Z3::Expr
Attributes
sort[R]
Public Class Methods
Add(*args)
click to toggle source
# 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)
click to toggle source
# 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
Distinct(*args)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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
Or(*args)
click to toggle source
# 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
Sub(*args)
click to toggle source
# 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)
click to toggle source
# 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
coerce_to_same_sort(*args)
click to toggle source
# 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
new(_ast, sort)
click to toggle source
Calls superclass method
Z3::AST::new
# 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
new_from_pointer(_ast)
click to toggle source
# 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
sort_for_const(a)
click to toggle source
# 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
Public Instance Methods
!=(other)
click to toggle source
# File lib/z3/expr/expr.rb, line 19 def !=(other) Expr.Distinct(self, other) end
==(other)
click to toggle source
# File lib/z3/expr/expr.rb, line 15 def ==(other) Expr.Eq(self, other) end
inspect()
click to toggle source
# File lib/z3/expr/expr.rb, line 11 def inspect "#{sort.to_s}<#{to_s}>" end