module Z3

# File lib/z3/interface.rb, line 47
def Add(*args)
  Expr.Add(*args)
end

# File lib/z3/interface.rb, line 59
def And(*args)
  BoolExpr.And(*args)
end

# File lib/z3/interface.rb, line 17
def Bitvec(v, n)
  BitvecSort.new(n).var(v)
end

# File lib/z3/interface.rb, line 13
def Bool(v)
  BoolSort.new.var(v)
end

# File lib/z3/interface.rb, line 32
def Const(v)
  Expr.sort_for_const(v).from_const(v)
end

# File lib/z3/interface.rb, line 39
def Distinct(*args)
  Expr.Distinct(*args)
end

# File lib/z3/interface.rb, line 43
def Eq(*args)
  Expr.Eq(*args)
end

# File lib/z3/interface.rb, line 28
def False
  BoolSort.new.False
end

# File lib/z3/interface.rb, line 71
def IfThenElse(a,b,c)
  BoolExpr.IfThenElse(a,b,c)
end

# File lib/z3/interface.rb, line 67
def Implies(a,b)
  BoolExpr.Implies(a,b)
end

# File lib/z3/interface.rb, line 5
def Int(v)
  IntSort.new.var(v)
end

# File lib/z3/interface.rb, line 51
def Mul(*args)
  Expr.Mul(*args)
end

# File lib/z3/interface.rb, line 55
def Or(*args)
  BoolExpr.Or(*args)
end

# File lib/z3/interface.rb, line 9
def Real(v)
  RealSort.new.var(v)
end

# File lib/z3/interface.rb, line 24
def True
  BoolSort.new.True
end

# File lib/z3/interface.rb, line 63
def Xor(*args)
  Expr.Xor(*args)
end

# File lib/z3/interface.rb, line 86
def set_param(k,v)
  LowLevel.global_param_set(k,v)
end

# File lib/z3/interface.rb, line 78
def version
  LowLevel.get_version.join(".")
end

# File lib/z3/interface.rb, line 82
def version_at_least?(a, b=0, c=0, d=0)
  (LowLevel.get_version <=> [a, b, c, d]) >= 0
end