что означает ключевое слово at-most в языке SMT-LIB (расширенная версия Z3 FixedPoint)

как в этом файле, самое большее ключевое слово в правиле:

horn1.smt2(из примеров репозитория Z3 github/python/data)

(declare-rel Goal (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
(declare-rel Invariant (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
(declare-var A Bool)
(declare-var B Bool)
(declare-var C Bool)
(declare-var D Bool)
(declare-var E Bool)
(declare-var F Bool)
(declare-var G Bool)
(declare-var H Bool)
(declare-var I Bool)
(declare-var J Bool)
(declare-var K Bool)
(declare-var L Bool)
(declare-var M Bool)
(declare-var N Bool)
(declare-var O Bool)
(declare-var P Bool)
(declare-var Q Bool)
(declare-var R Bool)
(declare-var S Bool)
(declare-var T Bool)
(declare-var U Bool)
(declare-var V Bool)
(declare-var W Bool)
(declare-var X Bool)
(rule (=> (not (or L K J I H G F E D C B A)) (Invariant L K J I H G F E D C B A)))
(rule (let ((a!1 (and (Invariant X W V U T S R Q P O N M)
                (=> (not (and true)) (not F))
                (=> (not (and true)) (not E))
                (=> (not (and W)) (not D))
                (=> (not (and W)) (not C))
                (=> (not (and U)) (not B))
                (=> (not (and U)) (not A))
                (= L (xor F X))
                (= K (xor E W))
                (= J (xor D V))
                (= I (xor C U))
                (= H (xor B T))
                (= G (xor A S))
                (=> D (not E))
                (=> C (not E))
                (=> B (not C))
                (=> A (not C))
                ((_ at-most 5) L K J I H G))))
  (=> a!1 (Invariant L K J I H G F E D C B A))))
(rule (=> (and (Invariant L K J I H G F E D C B A) L (not K) J (not I) H G)
    (Goal L K J I H G F E D C B A)))
(query Goal)

Похоже, что значение ключевого слова at-most в том, что только пять букв из шести букв (L K J I H G) могут быть истинными одновременно, или оно означает что-то еще, я не могу понять. Я очень признателен, если есть какой-нибудь хороший парень, который может мне помочь.


smt horn
person howareyouimfinethanks    schedule 15.11.2020    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Это псевдобулевы функции, подробности см. в этом ответе: K-out-of -N ограничение в Z3Py

В основном:

  • at-most: В лучшем случае это много правды
  • at-least: По крайней мере, это правда
  • pble: Максимум это количество, взвешенное
  • pbge: По крайней мере, это количество, взвешенное
  • pbeq: Ровно столько, взвешенное

Взвешенные версии, по сути, являются множителями логического значения и принимают постоянный список целых чисел.

Обратите внимание, что они специфичны для z3 и фактически не определены в SMTLib. Конечно, могут быть и другие решатели, которые его поддерживают.

person alias    schedule 15.11.2020