Module: Z3

Extended by:
Z3
Included in:
Z3
Defined in:
lib/z3/interface.rb,
lib/z3.rb,
lib/z3/ast.rb,
lib/z3/goal.rb,
lib/z3/model.rb,
lib/z3/probe.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/low_level.rb,
lib/z3/sort/sort.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/very_low_level_auto.rb,
lib/z3/expr/rounding_mode_expr.rb,
lib/z3/sort/rounding_mode_sort.rb

Overview

Seriously do not use this directly in your code They unwrap inputs, but don’t wrap returns yet

Defined Under Namespace

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

Instance Method Summary collapse

Instance Method Details

#Add(*args) ⇒ Object 



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

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

#And(*args) ⇒ Object 



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

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

#Bitvec(v, n) ⇒ Object 



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

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

#Bool(v) ⇒ Object 



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

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

#Const(v) ⇒ Object 



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

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

#Distinct(*args) ⇒ Object

Multiargument constructors



34
35
36
 
# File 'lib/z3/interface.rb', line 34

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

#Eq(*args) ⇒ Object 



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

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

#False ⇒ Object 



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

def False
  BoolSort.new.False
end

#IfThenElse(a, b, c) ⇒ Object 



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

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

#Implies(a, b) ⇒ Object 



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

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

#Int(v) ⇒ Object

Variables



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

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

#Mul(*args) ⇒ Object 



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

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

#Or(*args) ⇒ Object 



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

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

#Real(v) ⇒ Object 



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

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

#set_param(k, v) ⇒ Object 



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

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

#True ⇒ Object

Constants



21
22
23
 
# File 'lib/z3/interface.rb', line 21

def True
  BoolSort.new.True
end

#version ⇒ Object

Global functions



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

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

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

Returns:

  • (Boolean) 


75
76
77
 
# 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

#Xor(*args) ⇒ Object 



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

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