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