我是使用 Z3 的新人。
想知道如何计算一组和两个不同组的最大值。
例如：
[1, 6, 5]- 较大的是 6
[1, 6, 5]e [10, 7, 2]- 较大的是 6
我使用以下代码进行设置：
(declare-sort Set 0)
(declare-fun contains (Set Int) bool)
( declare-const set Set )
( declare-const distinct_set Set )
( declare-const A Int )
( declare-const B Int )
( declare-const C Int )
( assert ( = A 0 ) )
( assert ( = B 1 ) )
( assert ( = C 2 ) )
( …我在Z3中得到以下统计信息.
(:added-eqs 24529
:binary-propagations 43837
:bv-bit2core 7115
:bv-conflicts 156
:bv-diseqs 10395
:bv-dynamic-diseqs 10028
:bv->core-eq 10401
:conflicts 409
:decisions 4840
:del-clause 84926
:final-checks 2
:max-generation 4
:memory 5.69
:minimized-lits 467
:mk-clause 88358
:propagations 90195
:quant-instantiations 3388
:restarts 3
:time 0.83)
我想知道每个结果行使用的指标.
你能帮助我吗？