Module: Z3

Extended by:
Z3
Included in:
Z3
Defined in:
lib/z3.rb,
lib/z3/ast.rb,
lib/z3/goal.rb,
lib/z3/model.rb,
lib/z3/probe.rb,
lib/z3/params.rb,
lib/z3/solver.rb,
lib/z3/tactic.rb,
lib/z3/context.rb,
lib/z3/printer.rb,
lib/z3/optimize.rb,
lib/z3/exception.rb,
lib/z3/expr/expr.rb,
lib/z3/func_decl.rb,
lib/z3/interface.rb,
lib/z3/low_level.rb,
lib/z3/sort/sort.rb,
lib/z3/param_descrs.rb,
lib/z3/expr/int_expr.rb,
lib/z3/expr/set_expr.rb,
lib/z3/sort/int_sort.rb,
lib/z3/sort/set_sort.rb,
lib/z3/expr/bool_expr.rb,
lib/z3/expr/real_expr.rb,
lib/z3/low_level_auto.rb,
lib/z3/sort/bool_sort.rb,
lib/z3/sort/real_sort.rb,
lib/z3/very_low_level.rb,
lib/z3/expr/arith_expr.rb,
lib/z3/expr/array_expr.rb,
lib/z3/expr/float_expr.rb,
lib/z3/sort/array_sort.rb,
lib/z3/sort/float_sort.rb,
lib/z3/expr/bitvec_expr.rb,
lib/z3/sort/bitvec_sort.rb,
lib/z3/reference_counted.rb,
lib/z3/very_low_level_auto.rb,
lib/z3/expr/rounding_mode_expr.rb,
lib/z3/sort/rounding_mode_sort.rb

Defined Under Namespace

Modules: LowLevel, ReferenceCounted, VeryLowLevel Classes: AST, ArithExpr, ArrayExpr, ArraySort, BitvecExpr, BitvecSort, BoolExpr, BoolSort, Context, Exception, Expr, FloatExpr, FloatSort, FuncDecl, Goal, IntExpr, IntSort, Model, Optimize, ParamDescrs, Params, Printer, Probe, RealExpr, RealSort, RoundingModeExpr, RoundingModeSort, SetExpr, SetSort, Solver, Sort, Tactic

Instance Method Summary collapse

Instance Method Details

#Add(*args) ⇒ Object 



47
48
49
 
# File 'lib/z3/interface.rb', line 47

def Add(*args)
  Expr.Add(*args)
end

#And(*args) ⇒ Object 



59
60
61
 
# File 'lib/z3/interface.rb', line 59

def And(*args)
  BoolExpr.And(*args)
end

#AtLeast(args, k) ⇒ Object 



79
80
81
 
# File 'lib/z3/interface.rb', line 79

def AtLeast(args, k)
  BoolExpr.AtLeast(args, k)
end

#AtMost(args, k) ⇒ Object 



75
76
77
 
# File 'lib/z3/interface.rb', line 75

def AtMost(args, k)
  BoolExpr.AtMost(args, k)
end

#Bitvec(v, n) ⇒ Object 



17
18
19
 
# File 'lib/z3/interface.rb', line 17

def Bitvec(v, n)
  BitvecSort.new(n).var(v)
end

#Bool(v) ⇒ Object 



13
14
15
 
# File 'lib/z3/interface.rb', line 13

def Bool(v)
  BoolSort.new.var(v)
end

#Const(v) ⇒ Object 



32
33
34
 
# File 'lib/z3/interface.rb', line 32

def Const(v)
  Expr.sort_for_const(v).from_const(v)
end

#Distinct(*args) ⇒ Object

-- Multiargument constructors ++



39
40
41
 
# File 'lib/z3/interface.rb', line 39

def Distinct(*args)
  Expr.Distinct(*args)
end

#Eq(*args) ⇒ Object 



43
44
45
 
# File 'lib/z3/interface.rb', line 43

def Eq(*args)
  Expr.Eq(*args)
end

#Exactly(args, k) ⇒ Object 



83
84
85
 
# File 'lib/z3/interface.rb', line 83

def Exactly(args, k)
  BoolExpr.Exactly(args, k)
end

#False ⇒ Object 



28
29
30
 
# File 'lib/z3/interface.rb', line 28

def False
  BoolSort.new.False
end

#IfThenElse(a, b, c) ⇒ Object 



71
72
73
 
# File 'lib/z3/interface.rb', line 71

def IfThenElse(a,b,c)
  BoolExpr.IfThenElse(a,b,c)
end

#Implies(a, b) ⇒ Object 



67
68
69
 
# File 'lib/z3/interface.rb', line 67

def Implies(a,b)
  BoolExpr.Implies(a,b)
end

#Int(v) ⇒ Object

-- Variables ++



5
6
7
 
# File 'lib/z3/interface.rb', line 5

def Int(v)
  IntSort.new.var(v)
end

#Mul(*args) ⇒ Object 



51
52
53
 
# File 'lib/z3/interface.rb', line 51

def Mul(*args)
  Expr.Mul(*args)
end

#Or(*args) ⇒ Object 



55
56
57
 
# File 'lib/z3/interface.rb', line 55

def Or(*args)
  BoolExpr.Or(*args)
end

#Real(v) ⇒ Object 



9
10
11
 
# File 'lib/z3/interface.rb', line 9

def Real(v)
  RealSort.new.var(v)
end

#set_param(k, v) ⇒ Object 



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

def set_param(k,v)
  LowLevel.global_param_set(k,v)
end

#True ⇒ Object

-- Constants ++



24
25
26
 
# File 'lib/z3/interface.rb', line 24

def True
  BoolSort.new.True
end

#version ⇒ Object

-- Global functions ++



90
91
92
 
# File 'lib/z3/interface.rb', line 90

def version
  LowLevel.get_version.join(".")
end

#version_at_least?(a, b = 0, c = 0, d = 0) ⇒ Boolean

Returns:

  • (Boolean) 


94
95
96
 
# File 'lib/z3/interface.rb', line 94

def version_at_least?(a, b=0, c=0, d=0)
  (LowLevel.get_version <=> [a, b, c, d]) >= 0
end

#Xor(*args) ⇒ Object 



63
64
65
 
# File 'lib/z3/interface.rb', line 63

def Xor(*args)
  Expr.Xor(*args)
end