ksmt-core
0.5.23
ksmt-core
io.
ksmt
KAst
KContext
Ast
Management
Mode
GC
NO_GC
Operation
Mode
SINGLE_THREAD
CONCURRENT
Simplification
Mode
SIMPLIFY
NO_SIMPLIFY
io.
ksmt.
cache
Ast
Cache
Ast
Interner
Cache
Remove
Handler
Concurrent
Gc
Ast
Cache
Concurrent
Gc
Ast
Interner
Concurrent
No
Gc
Ast
Cache
Concurrent
No
Gc
Ast
Interner
hash()
KInterned
Object
mk
Ast
Cache()
mk
Ast
Interner()
mk
Cache()
Single
Thread
Gc
Ast
Cache
Single
Thread
Gc
Ast
Interner
Single
Thread
No
Gc
Ast
Cache
Single
Thread
No
Gc
Ast
Interner
structurally
Equal()
io.
ksmt.
cache.
weak
Concurrent
Weak
Cache
Concurrent
Weak
Hash
Map
Cache
Companion
Key
Ref
Node
Companion
Concurrent
Weak
Interner
Companion
Weak
Cache
Weak
Hash
Map
Cache
Companion
Key
Ref
Node
Weak
Interner
Companion
io.
ksmt.
decl
KAnd
Decl
KArith
Add
Decl
KArith
Div
Decl
KArith
Ge
Decl
KArith
Gt
Decl
KArith
Le
Decl
KArith
Lt
Decl
KArith
Mul
Decl
KArith
Power
Decl
KArith
Sub
Decl
KArith
Unary
Minus
Decl
KArray2Select
Decl
KArray2Store
Decl
KArray3Select
Decl
KArray3Store
Decl
KArray
Const
Decl
KArray
NSelect
Decl
KArray
NStore
Decl
KArray
Select
Decl
KArray
Select
Decl
Base
KArray
Store
Decl
KArray
Store
Decl
Base
KBit
Vec16Value
Decl
KBit
Vec1Value
Decl
KBit
Vec32Value
Decl
KBit
Vec64Value
Decl
KBit
Vec8Value
Decl
KBit
Vec
Custom
Size
Value
Decl
KBit
Vec
Value
Decl
Companion
KBv2Int
Decl
KBv
Add
Decl
KBv
Add
No
Overflow
Decl
KBv
Add
No
Underflow
Decl
KBv
And
Decl
KBv
Arith
Shift
Right
Decl
KBv
Concat
Decl
KBv
Div
No
Overflow
Decl
KBv
Extract
Decl
KBv
Logical
Shift
Right
Decl
KBv
Mul
Decl
KBv
Mul
No
Overflow
Decl
KBv
Mul
No
Underflow
Decl
KBv
NAnd
Decl
KBv
Negation
Decl
KBv
Neg
No
Overflow
Decl
KBv
Nor
Decl
KBv
Not
Decl
KBv
Or
Decl
KBv
Reduction
And
Decl
KBv
Reduction
Or
Decl
KBv
Repeat
Decl
KBv
Rotate
Left
Decl
KBv
Rotate
Left
Indexed
Decl
KBv
Rotate
Right
Decl
KBv
Rotate
Right
Indexed
Decl
KBv
Shift
Left
Decl
KBv
Signed
Div
Decl
KBv
Signed
Greater
Decl
KBv
Signed
Greater
Or
Equal
Decl
KBv
Signed
Less
Decl
KBv
Signed
Less
Or
Equal
Decl
KBv
Signed
Mod
Decl
KBv
Signed
Rem
Decl
KBv
Sub
Decl
KBv
Sub
No
Overflow
Decl
KBv
Sub
No
Underflow
Decl
KBv
To
Fp
Decl
KBv
Unsigned
Div
Decl
KBv
Unsigned
Greater
Decl
KBv
Unsigned
Greater
Or
Equal
Decl
KBv
Unsigned
Less
Decl
KBv
Unsigned
Less
Or
Equal
Decl
KBv
Unsigned
Rem
Decl
KBv
XNor
Decl
KBv
Xor
Decl
KConst
Decl
KDecl
KDecl
Visitor
KDistinct
Decl
KEq
Decl
KFalse
Decl
KFp128Decl
KFp16Decl
KFp32Decl
KFp64Decl
KFp
Abs
Decl
KFp
Add
Decl
KFp
Custom
Size
Decl
KFp
Decl
Companion
KFp
Div
Decl
KFp
Equal
Decl
KFp
From
Bv
Decl
KFp
Fused
Mul
Add
Decl
KFp
Greater
Decl
KFp
Greater
Or
Equal
Decl
KFp
Is
Infinite
Decl
KFp
Is
Na
NDecl
KFp
Is
Negative
Decl
KFp
Is
Normal
Decl
KFp
Is
Positive
Decl
KFp
Is
Subnormal
Decl
KFp
Is
Zero
Decl
KFp
Less
Decl
KFp
Less
Or
Equal
Decl
KFp
Max
Decl
KFp
Min
Decl
KFp
Mul
Decl
KFp
Negation
Decl
KFp
Rem
Decl
KFp
Rounding
Mode
Decl
KFp
Round
To
Integral
Decl
KFp
Sqrt
Decl
KFp
Sub
Decl
KFp
To
Bv
Decl
KFp
To
Fp
Decl
KFp
To
IEEEBv
Decl
KFp
To
Real
Decl
KFunc
Decl
KFunc
Decl1
KFunc
Decl2
KFunc
Decl3
KFunc
Decl4
KFunc
Decl
Chain
KImplies
Decl
KInt
Mod
Decl
KInt
Num
Decl
KInt
Rem
Decl
KInt
To
Real
Decl
KIte
Decl
KNot
Decl
KOr
Decl
KParameterized
Func
Decl
KReal
Is
Int
Decl
KReal
Num
Decl
KReal
To
Fp
Decl
KReal
To
Int
Decl
KSign
Ext
Decl
KTo
Fp
Decl
KTrue
Decl
KUninterpreted
Const
Decl
KUninterpreted
Func
Decl
KUninterpreted
Sort
Value
Decl
KXor
Decl
KZero
Ext
Decl
io.
ksmt.
expr
KAdd
Arith
Expr
KAnd
Binary
Expr
KAnd
Expr
KAnd
Nary
Expr
KApp
KArray2Lambda
KArray2Select
KArray2Store
KArray3Lambda
KArray3Select
KArray3Store
KArray
Const
KArray
Lambda
KArray
Lambda
Base
KArray
NLambda
KArray
NSelect
KArray
NStore
KArray
Select
KArray
Select
Base
KArray
Store
KArray
Store
Base
Companion
KBit
Vec16Value
KBit
Vec1Value
KBit
Vec32Value
KBit
Vec64Value
KBit
Vec8Value
KBit
Vec
Custom
Value
KBit
Vec
Number
Value
KBit
Vec
Value
KBv2Int
Expr
KBv
Add
Expr
KBv
Add
No
Overflow
Expr
KBv
Add
No
Underflow
Expr
KBv
And
Expr
KBv
Arith
Shift
Right
Expr
KBv
Concat
Expr
KBv
Div
No
Overflow
Expr
KBv
Extract
Expr
KBv
Logical
Shift
Right
Expr
KBv
Mul
Expr
KBv
Mul
No
Overflow
Expr
KBv
Mul
No
Underflow
Expr
KBv
NAnd
Expr
KBv
Negation
Expr
KBv
Neg
No
Overflow
Expr
KBv
Nor
Expr
KBv
Not
Expr
KBv
Or
Expr
KBv
Reduction
And
Expr
KBv
Reduction
Or
Expr
KBv
Repeat
Expr
KBv
Rotate
Left
Expr
KBv
Rotate
Left
Indexed
Expr
KBv
Rotate
Right
Expr
KBv
Rotate
Right
Indexed
Expr
KBv
Shift
Left
Expr
KBv
Signed
Div
Expr
KBv
Signed
Greater
Expr
KBv
Signed
Greater
Or
Equal
Expr
KBv
Signed
Less
Expr
KBv
Signed
Less
Or
Equal
Expr
KBv
Signed
Mod
Expr
KBv
Signed
Rem
Expr
KBv
Sign
Extension
Expr
KBv
Sub
Expr
KBv
Sub
No
Overflow
Expr
KBv
Sub
No
Underflow
Expr
KBv
To
Fp
Expr
KBv
Unsigned
Div
Expr
KBv
Unsigned
Greater
Expr
KBv
Unsigned
Greater
Or
Equal
Expr
KBv
Unsigned
Less
Expr
KBv
Unsigned
Less
Or
Equal
Expr
KBv
Unsigned
Rem
Expr
KBv
XNor
Expr
KBv
Xor
Expr
KBv
Zero
Extension
Expr
KConst
KDistinct
Expr
KDiv
Arith
Expr
KEq
Expr
KExistential
Quantifier
KExpr
KFalse
KFp128Value
KFp16Value
KFp32Value
KFp64Value
KFp
Abs
Expr
KFp
Add
Expr
KFp
Custom
Size
Value
KFp
Div
Expr
KFp
Equal
Expr
KFp
From
Bv
Expr
KFp
Fused
Mul
Add
Expr
KFp
Greater
Expr
KFp
Greater
Or
Equal
Expr
KFp
Is
Infinite
Expr
KFp
Is
Na
NExpr
KFp
Is
Negative
Expr
KFp
Is
Normal
Expr
KFp
Is
Positive
Expr
KFp
Is
Subnormal
Expr
KFp
Is
Zero
Expr
KFp
Less
Expr
KFp
Less
Or
Equal
Expr
KFp
Max
Expr
KFp
Min
Expr
KFp
Mul
Expr
KFp
Negation
Expr
KFp
Rem
Expr
KFp
Rounding
Mode
Round
Nearest
Ties
To
Even
Round
Nearest
Ties
To
Away
Round
Toward
Positive
Round
Toward
Negative
Round
Toward
Zero
KFp
Rounding
Mode
Expr
KFp
Round
To
Integral
Expr
KFp
Sqrt
Expr
KFp
Sub
Expr
KFp
To
Bv
Expr
KFp
To
Fp
Expr
KFp
To
IEEEBv
Expr
KFp
To
Real
Expr
KFp
Value
KFunction
App
KFunction
As
Array
KGe
Arith
Expr
KGt
Arith
Expr
KImplies
Expr
KInt32Num
Expr
KInt64Num
Expr
KInt
Big
Num
Expr
KInterpreted
Value
KInt
Num
Expr
KIs
Int
Real
Expr
KIte
Expr
KLe
Arith
Expr
KLt
Arith
Expr
KMod
Int
Expr
KMul
Arith
Expr
KNot
Expr
KOr
Binary
Expr
KOr
Expr
KOr
Nary
Expr
KPower
Arith
Expr
KQuantifier
KReal
Num
Expr
KReal
To
Fp
Expr
KRem
Int
Expr
KSub
Arith
Expr
KTo
Int
Real
Expr
KTo
Real
Int
Expr
KTrue
KUnary
Minus
Arith
Expr
KUninterpreted
Sort
Value
KUniversal
Quantifier
KXor
Expr
io.
ksmt.
expr.
printer
Bv
Value
Print
Mode
BINARY
HEX
Expression
Printer
Expression
Printer
With
Let
Bindings
Printer
Params
io.
ksmt.
expr.
rewrite
KExpr
Substitutor
KExpr
Uninterpreted
Decl
Collector
Companion
io.
ksmt.
expr.
rewrite.
simplify
add
Arith
Term()
are
Definitely
Distinct()
bv
Less
Or
Equal()
cast
Real
Value()
distribute
Extract
Over
Concat()
distribute
Operation
Over
Concat()
ensure
Expressions
Order()
eval
Binary
Op()
eval
Bv
Operation()
eval
Bv
Signed
Mul
No
Overflow()
eval
Fp
Predicate
Or()
eval
Int
Div()
eval
Int
Mod()
eval
Int
Rem()
execute
If
Value()
Expression
Ordering
flat
Binary
Bv
Expr()
flat
Concat
Args()
is
Complement()
is
Max
Value()
is
Min
Value()
KArith
Expr
Simplifier
KArray
Expr
Simplifier
KBool
Expr
Simplifier
KBv
Expr
Simplifier
KExpr
Simplifier
Companion
KExpr
Simplifier
Base
KFp
Expr
Simplifier
mul
Arith
Term()
rewrite
Arith
Ge()
rewrite
Arith
Gt()
rewrite
Arith
Sub()
rewrite
Bv
Add
No
Overflow
Expr()
rewrite
Bv
Add
No
Underflow
Expr()
rewrite
Bv
Concat
Eq()
rewrite
Bv
Div
No
Overflow
Expr()
rewrite
Bv
Mul
No
Overflow
Expr()
rewrite
Bv
Mul
No
Underflow
Expr()
rewrite
Bv
NAnd
Expr()
rewrite
Bv
Neg
No
Overflow
Expr()
rewrite
Bv
Nor
Expr()
rewrite
Bv
Repeat
Expr()
rewrite
Bv
Rotate
Left
Indexed
Expr()
rewrite
Bv
Rotate
Right
Indexed
Expr()
rewrite
Bv
Signed
Greater
Expr()
rewrite
Bv
Signed
Greater
Or
Equal
Expr()
rewrite
Bv
Signed
Less
Expr()
rewrite
Bv
Sub
Expr()
rewrite
Bv
Sub
No
Overflow
Expr()
rewrite
Bv
Sub
No
Underflow
Expr()
rewrite
Bv
Unsigned
Greater
Expr()
rewrite
Bv
Unsigned
Greater
Or
Equal
Expr()
rewrite
Bv
Unsigned
Less
Expr()
rewrite
Bv
Unsigned
Less
Or
Equal
Expr
Light()
rewrite
Bv
XNor
Expr()
rewrite
Bv
Zero
Extension
Expr()
rewrite
Fp
Greater
Expr()
rewrite
Fp
Greater
Or
Equal
Expr()
rewrite
Fp
Sub
Expr()
rewrite
Implies()
rewrite
Xor()
rotate
Left()
SIMPLIFIER_DEFAULT_BOUNDED_REWRITE_DEPTH
simplify
And()
simplify
And
Or()
simplify
Arith
Add()
simplify
Arith
Add
Light()
simplify
Arith
Div()
simplify
Arith
Div
Light()
simplify
Arith
Ge()
simplify
Arith
Gt()
simplify
Arith
Le()
simplify
Arith
Le
Light()
simplify
Arith
Lt()
simplify
Arith
Lt
Light()
simplify
Arith
Mul()
simplify
Arith
Mul
Light()
simplify
Arith
Power()
simplify
Arith
Power
Light()
simplify
Arith
Sub()
simplify
Arith
Unary
Minus()
simplify
Arith
Unary
Minus
Light()
simplify
Array
NSelect()
simplify
Array
NSelect
From
Array
Store()
simplify
Array
NSelect
Lambda()
simplify
Array
NStore()
simplify
Array
NStore
Light()
simplify
Array
Select()
simplify
Array
Select
Lambda()
simplify
Array
Store()
simplify
Array
Store
Light()
simplify
Bool
Ite
Const
Branches()
simplify
Bool
Ite
Same
Condition
Branch()
simplify
Bv2Int
Expr()
simplify
Bv2Int
Expr
Light()
simplify
Bv
Add
Expr()
simplify
Bv
Add
Expr
Light()
simplify
Bv
Add
Expr
Nested
Add()
simplify
Bv
Add
No
Overflow
Expr()
simplify
Bv
Add
No
Underflow
Expr()
simplify
Bv
And
Expr()
simplify
Bv
And
Expr
Light()
simplify
Bv
And
Expr
Nested
And()
simplify
Bv
And
Or()
simplify
Bv
Arith
Shift
Right
Expr()
simplify
Bv
Arith
Shift
Right
Expr
Light()
simplify
Bv
Concat
Expr()
simplify
Bv
Concat
Expr
Light()
simplify
Bv
Concat
Expr
Nested
Concat()
simplify
Bv
Div
No
Overflow
Expr()
simplify
Bv
Extract
Expr()
simplify
Bv
Extract
Expr
Light()
simplify
Bv
Extract
Expr
Nested
Extract()
simplify
Bv
Extract
Expr
Try
Rewrite()
simplify
Bv
Logical
Shift
Right
Expr()
simplify
Bv
Logical
Shift
Right
Expr
Const
Shift()
simplify
Bv
Logical
Shift
Right
Expr
Light()
simplify
Bv
Mul
Expr()
simplify
Bv
Mul
Expr
Light()
simplify
Bv
Mul
Expr
Minus
One
Const()
simplify
Bv
Mul
Expr
Nested
Mul()
simplify
Bv
Mul
No
Overflow
Expr()
simplify
Bv
Mul
No
Underflow
Expr()
simplify
Bv
NAnd
Expr()
simplify
Bv
Negation
Expr()
simplify
Bv
Negation
Expr
Add()
simplify
Bv
Negation
Expr
Light()
simplify
Bv
Negation
No
Overflow
Expr()
simplify
Bv
Nor
Expr()
simplify
Bv
Not
Expr()
simplify
Bv
Not
Expr
Concat()
simplify
Bv
Not
Expr
Ite()
simplify
Bv
Not
Expr
Light()
simplify
Bv
Or
Expr()
simplify
Bv
Or
Expr
Light()
simplify
Bv
Or
Expr
Nested
Or()
simplify
Bv
Reduction
And
Expr()
simplify
Bv
Reduction
And
Expr
Light()
simplify
Bv
Reduction
Or
Expr()
simplify
Bv
Reduction
Or
Expr
Light()
simplify
Bv
Repeat
Expr()
simplify
Bv
Repeat
Expr
Light()
simplify
Bv
Rotate
Left
Expr()
simplify
Bv
Rotate
Left
Expr
Const
Rotation()
simplify
Bv
Rotate
Left
Indexed
Expr()
simplify
Bv
Rotate
Right
Expr()
simplify
Bv
Rotate
Right
Expr
Const
Rotation()
simplify
Bv
Rotate
Right
Indexed
Expr()
simplify
Bv
Shift
Left
Expr()
simplify
Bv
Shift
Left
Expr
Const
Shift()
simplify
Bv
Shift
Left
Expr
Light()
simplify
Bv
Shift
Left
Expr
Nested
Shift
Left()
simplify
Bv
Signed
Div
Expr()
simplify
Bv
Signed
Div
Expr
Light()
simplify
Bv
Signed
Greater
Expr()
simplify
Bv
Signed
Greater
Or
Equal
Expr()
simplify
Bv
Signed
Less
Expr()
simplify
Bv
Signed
Less
Or
Equal
Expr()
simplify
Bv
Signed
Less
Or
Equal
Expr
Light()
simplify
Bv
Signed
Mod
Expr()
simplify
Bv
Signed
Mod
Expr
Light()
simplify
Bv
Signed
Rem
Expr()
simplify
Bv
Signed
Rem
Expr
Light()
simplify
Bv
Sign
Extension
Expr()
simplify
Bv
Sign
Extension
Expr
Light()
simplify
Bv
Sub
Expr()
simplify
Bv
Sub
No
Overflow
Expr()
simplify
Bv
Sub
No
Underflow
Expr()
simplify
Bv
To
Fp
Expr()
simplify
Bv
To
Fp
Expr
Light()
simplify
Bv
Unsigned
Div
Expr()
simplify
Bv
Unsigned
Div
Expr
Light()
simplify
Bv
Unsigned
Div
Expr
Power
Of
Two
Divisor()
simplify
Bv
Unsigned
Greater
Expr()
simplify
Bv
Unsigned
Greater
Or
Equal
Expr()
simplify
Bv
Unsigned
Less
Expr()
simplify
Bv
Unsigned
Less
Or
Equal
Expr()
simplify
Bv
Unsigned
Rem
Expr()
simplify
Bv
Unsigned
Rem
Expr
Light()
simplify
Bv
Unsigned
Rem
Expr
Power
Of
Two
Divisor()
simplify
Bv
XNor
Expr()
simplify
Bv
Xor
Expr()
simplify
Bv
Xor
Expr
Light()
simplify
Bv
Xor
Expr
Max
Const()
simplify
Bv
Xor
Expr
Nested
Xor()
simplify
Bv
Zero
Extension
Expr()
simplify
Bv
Zero
Extension
Expr
Light()
simplify
Distinct()
simplify
Distinct
Light()
simplify
Eq()
simplify
Eq
Bool()
simplify
Eq
Bool
Light()
simplify
Eq
Bool
Not()
simplify
Eq
Bv
Concat()
simplify
Eq
Bv
Light()
simplify
Eq
Fp
Light()
simplify
Eq
Int
Light()
simplify
Eq
Light()
simplify
Eq
Real
Light()
simplify
Expr()
simplify
Expr
Base()
simplify
Flat
Bv
Add
Expr()
simplify
Flat
Bv
And
Expr()
simplify
Flat
Bv
And
Expr
Distribute
Over
Concat()
simplify
Flat
Bv
Concat
Expr()
simplify
Flat
Bv
Mul
Expr()
simplify
Flat
Bv
Or
Expr()
simplify
Flat
Bv
Or
Expr
Distribute
Over
Concat()
simplify
Flat
Bv
Xor
Expr()
simplify
Flat
Bv
Xor
Expr
Distribute
Over
Concat()
simplify
Fp
Abs
Expr()
simplify
Fp
Abs
Expr
Light()
simplify
Fp
Add
Expr()
simplify
Fp
Add
Expr
Light()
simplify
Fp
Div
Expr()
simplify
Fp
Div
Expr
Light()
simplify
Fp
Equal
Expr()
simplify
Fp
Equal
Expr
Light()
simplify
Fp
From
Bv
Expr()
simplify
Fp
From
Bv
Expr
Light()
simplify
Fp
Fused
Mul
Add
Expr()
simplify
Fp
Fused
Mul
Add
Expr
Light()
simplify
Fp
Greater
Expr()
simplify
Fp
Greater
Or
Equal
Expr()
simplify
Fp
Is
Infinite
Expr()
simplify
Fp
Is
Infinite
Expr
Light()
simplify
Fp
Is
Na
NExpr()
simplify
Fp
Is
Na
NExpr
Light()
simplify
Fp
Is
Negative
Expr()
simplify
Fp
Is
Negative
Expr
Light()
simplify
Fp
Is
Normal
Expr()
simplify
Fp
Is
Normal
Expr
Light()
simplify
Fp
Is
Positive
Expr()
simplify
Fp
Is
Positive
Expr
Light()
simplify
Fp
Is
Subnormal
Expr()
simplify
Fp
Is
Subnormal
Expr
Light()
simplify
Fp
Is
Zero
Expr()
simplify
Fp
Is
Zero
Expr
Light()
simplify
Fp
Less
Expr()
simplify
Fp
Less
Expr
Light()
simplify
Fp
Less
Or
Equal
Expr()
simplify
Fp
Less
Or
Equal
Expr
Light()
simplify
Fp
Max
Expr()
simplify
Fp
Max
Expr
Light()
simplify
Fp
Min
Expr()
simplify
Fp
Min
Expr
Light()
simplify
Fp
Mul
Expr()
simplify
Fp
Mul
Expr
Light()
simplify
Fp
Negation
Expr()
simplify
Fp
Negation
Expr
Light()
simplify
Fp
Rem
Expr()
simplify
Fp
Rem
Expr
Light()
simplify
Fp
Round
To
Integral
Expr()
simplify
Fp
Round
To
Integral
Expr
Light()
simplify
Fp
Sqrt
Expr()
simplify
Fp
Sqrt
Expr
Light()
simplify
Fp
Sub
Expr()
simplify
Fp
To
Bv
Expr()
simplify
Fp
To
Bv
Expr
Light()
simplify
Fp
To
Fp
Expr()
simplify
Fp
To
Fp
Expr
Light()
simplify
Fp
To
IEEEBv
Expr()
simplify
Fp
To
IEEEBv
Expr
Light()
simplify
Fp
To
Real
Expr()
simplify
Fp
To
Real
Expr
Light()
simplify
Implies()
simplify
Int
Mod()
simplify
Int
Mod
Light()
simplify
Int
Rem()
simplify
Int
Rem
Light()
simplify
Int
To
Real()
simplify
Int
To
Real
Light()
simplify
Ite()
simplify
Ite
Bool()
simplify
Ite
Light()
simplify
Ite
Not
Condition()
simplify
Ite
Same
Branches()
simplify
Not()
simplify
Not
Light()
simplify
Or()
simplify
Real
Is
Int()
simplify
Real
Is
Int
Light()
simplify
Real
To
Fp
Expr()
simplify
Real
To
Fp
Expr
Light()
simplify
Real
To
Int()
simplify
Real
To
Int
Light()
simplify
Select
From
Array
Store()
simplify
Xor()
to
Real
Value()
try
Eval
Arith
Power()
try
Merge
Bv
Concat
Extract()
try
Simplify
And
Or
Element()
try
Simplify
Bv
Signed
Mul
No
Overflow()
try
Simplify
Bv
Unsigned
Mul
No
Overflow()
with
Expressions
Ordered()
io.
ksmt.
expr.
transformer
KExpr
Visit
Result
Companion
KNon
Recursive
Transformer
KNon
Recursive
Transformer
Base
KNon
Recursive
Visitor
KNon
Recursive
Visitor
Base
KTransformer
KTransformer
Base
KVisitor
visit
Expr()
io.
ksmt.
parser
KSMTLib
Parse
Exception
KSMTLib
Parser
io.
ksmt.
solver
KModel
KSolver
KSolver
Configuration
KSolver
Exception
KSolver
Status
SAT
UNSAT
UNKNOWN
KSolver
Universal
Configuration
Builder
KSolver
Unsupported
Feature
Exception
KSolver
Unsupported
Parameter
Exception
io.
ksmt.
solver.
model
KFunc
Interp
Companion
KFunc
Interp
Entry
Companion
KFunc
Interp
Entry
NAry
KFunc
Interp
Entry
One
Ary
Companion
KFunc
Interp
Entry
Three
Ary
Companion
KFunc
Interp
Entry
Two
Ary
Companion
KFunc
Interp
Entry
Vars
Free
Companion
KFunc
Interp
Entry
Vars
Free
NAry
KFunc
Interp
Entry
Vars
Free
One
Ary
KFunc
Interp
Entry
Vars
Free
Three
Ary
KFunc
Interp
Entry
Vars
Free
Two
Ary
KFunc
Interp
Entry
With
Vars
Companion
KFunc
Interp
Entry
With
Vars
NAry
KFunc
Interp
Entry
With
Vars
One
Ary
KFunc
Interp
Entry
With
Vars
Three
Ary
KFunc
Interp
Entry
With
Vars
Two
Ary
KFunc
Interp
Vars
Free
KFunc
Interp
With
Vars
KModel
Evaluator
KModel
Impl
KNative
Solver
Model
io.
ksmt.
solver.
util
conversion
Loop()
ensure
Args
Converted
And
Convert()
Expr
Conversion
Result
internalization
Loop()
KExpr
Converter
Base
KExpr
Converter
Utils
KExpr
Internalizer
Base
KExpr
Int
Internalizer
Base
Companion
KExpr
Long
Converter
Base
KExpr
Long
Internalizer
Base
Companion
transform()
transform
List()
io.
ksmt.
sort
KArith
Sort
KArray2Sort
Companion
KArray3Sort
Companion
KArray
NSort
KArray
Sort
Companion
KArray
Sort
Base
KBool
Sort
KBv16Sort
KBv1Sort
KBv32Sort
KBv64Sort
KBv8Sort
KBv
Custom
Size
Sort
KBv
Sort
KFp128Sort
Companion
KFp16Sort
Companion
KFp32Sort
Companion
KFp64Sort
Companion
KFp
Custom
Size
Sort
KFp
Rounding
Mode
Sort
KFp
Sort
KInt
Sort
KReal
Sort
KSort
KSort
Visitor
KUninterpreted
Sort
io.
ksmt.
utils
Arith
Utils
Real
Value
Companion
as
Expr()
boolean
Sign
Bit
Bv
Utils
cast()
Default
Value
Sampler
extend
With
Leading
Zeros()
extract
Exponent()
extract
Significand()
Fp
Utils
get
Exponent()
get
Half
Precision
Exponent()
get
Value()
half
Precision
Significand
mk
Const()
mk
Const
Decl()
mk
Fresh
Const()
mk
Fresh
Const
Decl()
normalize
Value()
power
Of
Two()
sample
Value()
sign
Bit
significand
to
Big
Integer()
to
Binary()
to
ULong
Value()
to
Unsigned
Big
Integer()
unchecked
Cast()
io.
ksmt.
utils.
library
Native
Library
Loader
Native
Library
Loader
Arm
Native
Library
Loader
Linux
Native
Library
Loader
Mac
Native
Library
Loader
Utils
Native
Library
Loader
Windows
Native
Library
Loader
X64
ksmt-core
/
io.ksmt.solver.model
/
KModelImpl
/
KModelImpl
KModel
Impl
fun
KModelImpl
(
ctx
:
KContext
,
interpretations
:
Map
<
KDecl
<
*
>
,
KFuncInterp
<
*
>
>
,
uninterpretedSortsUniverses
:
Map
<
KUninterpretedSort
,
Set
<
KUninterpretedSortValue
>
>
)