module Z3
Everything here might go away
Seriously do not use this directly in your code They unwrap inputs, but don’t wrap returns yet
Public Instance Methods
Add(*args)
click to toggle source
# File lib/z3/interface.rb, line 42 def Add(*args) Expr.Add(*args) end
And(*args)
click to toggle source
# File lib/z3/interface.rb, line 54 def And(*args) BoolExpr.And(*args) end
Bitvec(v, n)
click to toggle source
# File lib/z3/interface.rb, line 16 def Bitvec(v, n) BitvecSort.new(n).var(v) end
Bool(v)
click to toggle source
# File lib/z3/interface.rb, line 12 def Bool(v) BoolSort.new.var(v) end
Const(v)
click to toggle source
# File lib/z3/interface.rb, line 29 def Const(v) Expr.sort_for_const(v).from_const(v) end
Distinct(*args)
click to toggle source
Multiargument constructors
# File lib/z3/interface.rb, line 34 def Distinct(*args) Expr.Distinct(*args) end
Eq(*args)
click to toggle source
# File lib/z3/interface.rb, line 38 def Eq(*args) Expr.Eq(*args) end
False()
click to toggle source
# File lib/z3/interface.rb, line 25 def False BoolSort.new.False end
IfThenElse(a,b,c)
click to toggle source
# File lib/z3/interface.rb, line 66 def IfThenElse(a,b,c) BoolExpr.IfThenElse(a,b,c) end
Implies(a,b)
click to toggle source
# File lib/z3/interface.rb, line 62 def Implies(a,b) BoolExpr.Implies(a,b) end
Int(v)
click to toggle source
Variables
# File lib/z3/interface.rb, line 4 def Int(v) IntSort.new.var(v) end
Mul(*args)
click to toggle source
# File lib/z3/interface.rb, line 46 def Mul(*args) Expr.Mul(*args) end
Or(*args)
click to toggle source
# File lib/z3/interface.rb, line 50 def Or(*args) BoolExpr.Or(*args) end
Real(v)
click to toggle source
# File lib/z3/interface.rb, line 8 def Real(v) RealSort.new.var(v) end
True()
click to toggle source
Constants
# File lib/z3/interface.rb, line 21 def True BoolSort.new.True end
Xor(*args)
click to toggle source
# File lib/z3/interface.rb, line 58 def Xor(*args) Expr.Xor(*args) end
set_param(k,v)
click to toggle source
# File lib/z3/interface.rb, line 79 def set_param(k,v) LowLevel.global_param_set(k,v) end
version()
click to toggle source
Global functions
# File lib/z3/interface.rb, line 71 def version LowLevel.get_version.join(".") end
version_at_least?(a, b=0, c=0, d=0)
click to toggle source
# File lib/z3/interface.rb, line 75 def version_at_least?(a, b=0, c=0, d=0) (LowLevel.get_version <=> [a, b, c, d]) >= 0 end