Quantifier Vs Non-Quantifier

Question

У меня вопрос о квантификаторах.

Предположим, что у меня есть массив, и я хочу, чтобы вычислить индекс массива 0, 1 и 2 для этого массива -

(declare-const cpuA (Array Int Int)) 
(assert (or (= (select cpuA 0) 0) (= (select cpuA 0) 1))) 
(assert (or (= (select cpuA 1) 0) (= (select cpuA 1) 1))) 
(assert (or (= (select cpuA 2) 0) (= (select cpuA 2) 1))) 

Или иначе я могу указать тот же используя FORALL построить, как -

(assert (forall ((x Int)) (=> (and (>= x 0) (<= x 2)) (or (= (select cpuA x) 0) (= (select cpuA x) 1))))) 

Теперь я хотел бы понять разницу между двумя из них. Первый метод выполняется быстро и дает простую и читаемую модель. Напротив, размер кода со второй опцией очень мал, но для выполнения программы требуется время. А также решение является сложным.

Я бы хотел использовать второй метод, так как мой код станет меньше. Тем не менее, я хочу найти читаемую простую модель.

Answer 1

Квантификатор, как правило, очень дорог. В вашем примере количественная формула эквивалентна трем утверждениям, которые вы предоставили. Однако это не так, как Z3 решает/решает вашу формулу. Z3 решает вашу формулу с помощью метода, называемого Instantiation Quantifier Instantiation (MBQI). Этот метод может решить многие фрагменты (см. http://rise4fun.com/Z3/tutorial/guide). Он в основном эффективен на фрагментах, описанных в этом руководстве. Он поддерживает неинтерпретируемые функции, арифметические и битово-векторные теории. Он также имеет ограниченную поддержку массивов и типов данных. Этого достаточно для решения вашего примера. Модель, созданная Z3, кажется более сложной, потому что один и тот же движок используется для определения более сложных фрагментов. Модель должна выглядеть как небольшая функциональная программа. Вы можете найти более подробную информацию о том, как этот подход работает в следующих статьях:

• Complete instantiation for quantified SMT formulas

• Efficiently Solving Quantified Bit-Vector Formula

Заметим, что теория массива в основном полезен для представления/моделирования неограниченная или большие массивы. То есть фактический размер массива неизвестен или слишком велик. Большим я имею в виду, что количество обращений к массиву (т. Е. selects) в вашей формуле намного меньше фактического размера массива. Мы должны спросить себя: «Нам действительно нужны массивы для моделирования/решения проблемы X?». Вы можете рассмотреть следующие альтернативы:

• (Неинтерпретированные) функции вместо массивов. Ваш пример может быть закодирована также как:

  (объявить-забавным cpuA (Int) Int)

  (утверждают (или (= (cpuA 0) 0) (= (cpuA 0) 1)))
  (утверждают (или (= (cpuA 1) 0) (= (cpuA 1) 1)))
  (утверждают (или (= (cpuA 2) 0) (= (cpuA 2) 1)))

• Программный API. Мы видели множество примеров, где массивы (и функции) используются для обеспечения компактного кодирования. Компактная и элегантная кодировка не всегда проще решить. На самом деле, это обычно наоборот.Вы можете достичь наилучшего из обоих миров (производительность и компактность), используя программный API для Z3. В следующей ссылке я закодировал ваш пример, используя одну «переменную» для каждой позиции «массива». Макросы/функции используются для кодирования ограничений, таких как: выражение: 0 или 1. http://rise4fun.com/Z3Py/JF