No recent searches
Z3
AST
ApplyResult
ArithExpr
ArrayExpr
ArraySort
BitvecExpr
BitvecSort
BoolExpr
BoolSort
CharExpr
CharSort
Context
EnumExpr
EnumSort
Exception
Expr
FiniteDomainExpr
FiniteDomainSort
FloatExpr
FloatSort
FuncDecl
Goal
IntExpr
IntSort
LowLevel
Model
Optimize
ParamDescrs
Params
Printer
PrintedExpr
Probe
Re
ReExpr
ReSort
RealExpr
RealSort
ReferenceCounted
RoundingModeExpr
RoundingModeSort
SeqExpr
SeqSort
SetExpr
SetSort
Simplifier
Solver
Sort
StringExpr
StringSort
Tactic
TypeVariableExpr
TypeVariableSort
UninterpretedExpr
UninterpretedSort
# File lib/z3/context.rb, line 8 def self.instance @instance ||= new end
# File lib/z3/context.rb, line 4 def initialize @_context = LowLevel.mk_context end