ksmt-core
0.5.23
ksmt-core
/
io.ksmt.expr.rewrite.simplify
/
simplifyArrayStore
simplify
Array
Store
fun
<
D
:
KSort
,
R
:
KSort
>
KContext
.
simplifyArrayStore
(
array
:
KExpr
<
KArraySort
<
D
,
R
>
>
,
index
:
KExpr
<
D
>
,
value
:
KExpr
<
R
>
)
:
KExpr
<
KArraySort
<
D
,
R
>
>
fun
<
D0
:
KSort
,
D1
:
KSort
,
R
:
KSort
>
KContext
.
simplifyArrayStore
(
array
:
KExpr
<
KArray2Sort
<
D0
,
D1
,
R
>
>
,
index0
:
KExpr
<
D0
>
,
index1
:
KExpr
<
D1
>
,
value
:
KExpr
<
R
>
)
:
KExpr
<
KArray2Sort
<
D0
,
D1
,
R
>
>
fun
<
D0
:
KSort
,
D1
:
KSort
,
D2
:
KSort
,
R
:
KSort
>
KContext
.
simplifyArrayStore
(
array
:
KExpr
<
KArray3Sort
<
D0
,
D1
,
D2
,
R
>
>
,
index0
:
KExpr
<
D0
>
,
index1
:
KExpr
<
D1
>
,
index2
:
KExpr
<
D2
>
,
value
:
KExpr
<
R
>
)
:
KExpr
<
KArray3Sort
<
D0
,
D1
,
D2
,
R
>
>