Проверка всех решений для массива (as-array) в Z3PY - PullRequest
Новая
       50

Проверка всех решений для массива (as-array) в Z3PY

0 голосов
/ 05 февраля 2020

Моя проблема в том, что я должен получить все возможные модели для массива вида as-array. Код, который я сделал для этого, следующий: 

s = Solver()
check = s.check()
while (str(check) == "sat"):
      mod = s.model()
      block = []
      for var in mod.decls():
         block.append(var() != mod[var])
      s.add(Or(block))
      check = s.check()

var может принимать значения типа as-array среди других, и когда я запускаю строку s.add(Or(block)), в следующий раз, когда я запускаю строку check = s.check возвращает неизвестное

Есть ли другой способ сделать это?

------- Редактировать -------

У меня есть нашел способ получить все возможные модели для массива вида as-array, который был предыдущей проблемой, способ, который я сделал, это создать переменную, которая представляет размер массива и от i = 0 до i = n (где n - размер), сделайте a[i]!= x массивом «a», а «x» - значением, которое принимает «a [i]».

Теперь моя проблема в том, что у меня есть тип данных Форма "mk-pair", первый аргумент которой представляет собой массив в форме as-array и целое число, указывающее размер массива.

Когда я получаю модель, она появляется в форме mk-pair(as-array, 30) ( например), размер массива равен 30.

Проблема в том, что я не могу найти способ получить все возможные модели, поскольку, если я откажу pe данных (a! = x, при условии, что «a» является типом данных, а «x» - его значением), он возвращает меня неизвестно, и если я сделаю первое (as-array [0]! = x), что я на самом деле отрицание - это as-array, а не переменная "a" (которая имеет форму mk-pair (as-array, Int)), и когда я несколько раз запрашиваю модели, я получаю повторяющиеся результаты.

Any способ сделать это?

1 Ответ

0 голосов
/ 05 февраля 2020

Это частый запрос. Ваше предложение о блокировке должно быть изменено, чтобы учесть возможность использования массивов. Следует также следить за типами данных, функциями, числами с плавающей точкой ... Определенно выполнимо, и код этого ответа поможет вам начать: (Z3Py) проверка всех решений для уравнения

Обратите внимание, что вы не можете вообще «блокировать» функции. Массивы также могут быть проблематичны c, так как вы не сможете «преобразовать» их в блокировщики, если они имеют бесконечную поддержку. (То есть, подумайте о массиве, который отображает i '-ый элемент на значение i. Нет конечного представления этого, которое вы можете легко написать в SMTLib без квантификаторов.) Помимо этих соображений, я считаю, что хитрость в Приведенный выше ответ поможет вам справиться с большинством дел.

...