Разрешимые запросы в muZ

Question

Я хочу использовать z3 для BMC с помощью muZ. Может быть, я упустил что-то относительно определения выполнимости запроса. Однако в следующем случае у меня есть пример запроса, который не является выполнимым (т. Е. Возвращает «false»), но при добавлении дополнительного ограничения (которое эффективно дает удовлетворяющее присваивание) возвращается правильное присваивание.

Есть ли какая-либо документация, помогающая понять точную семантику расширения языка muZ z3?

Спасибо и с наилучшими пожеланиями !!

Выполнение следующей .smt2-файл с Z3 версии 4.3.2 приводит к следующему результату:

formula undetermined in model: (= (head query!0_0_n) (state c1 1)) 
sat 
false 
sat 
(let ((a!1 (insert (state c1 1) (insert (state c2 0) (insert (state c1 0) nil)))) 
     (a!2 (TransClosure (insert (state c2 0) (insert (state c1 0) nil))))) 
    (and (TransClosure a!1) a!2 (TransClosure (insert (state c1 0) nil)))) 

Соответствующий .smt2-файл является:

;; Application of z3Mu for BMC of EFSM 
;; Behavior of EFSM is defined recursively as a predicate over finite sequences (Lists) of states 

;; Declaration of state space 
(declare-datatypes() ((Control c1 c2))) 
(declare-datatypes() ((State (state (cstate Control) (var Int))))) 

;; Definition of transition relation and initial state 
(declare-rel Trans (State State)) 
(declare-var pre State) 
(declare-var post State) 
(rule (=> (and (= (cstate pre) c1) (= (cstate post) c2) (= (+ (var pre) 0) (var post))) (Trans post pre))) 
(rule (=> (and (= (cstate pre) c2) (= (cstate post) c1) (= (+ (var pre) 1) (var post))) (Trans post pre))) 

;; Definition of fixed-point closure 
(declare-var init State) 
(declare-var trace (List State)) 

(declare-rel Init (State)) 
(rule (Init (state c1 0))) 

(declare-rel TransClosure ((List State))) 
(rule (=> (and (Trans (head trace) (head (tail trace))) (TransClosure (tail trace))) 
     (TransClosure trace))) 
(rule (=> (Init init) (TransClosure (insert init nil)))) 


;; Query for a witness which is satifiable in three steps 
;; Query without explicit witness construction fails 
(query (and (= (head trace) (state c1 1)) 
      (TransClosure trace) 
      ) 
    :print-answer true) 
;; Same query with explicit witness succeeds 
(query (and (= (head trace) (state c1 1)) 
      (TransClosure trace) 
      (= trace (insert (state c1 1) (insert (state c2 0) (insert (state c1 0) nil)))) 
      ) 
:print-answer true)    

Answer 1

«формула не определены в model "указывает на ошибку в Z3. Ошибка в том, что Z3 принял вход как есть без жалоб. Он должен был отклонить этот пример при использовании брандмауэра PDR. Бэкэнд-модуль PDR поддерживает арифметику, логические и не оптимизированные для бит-векторов и некоторую поддержку алгебраических типов данных. Он не поддерживает accessors (head, tail) для алгебраических типов данных, и теперь я добавил проверку, которая сообщает об ошибке перед вызовом поиска и указывает на использование неподдерживаемых аксессуаров. Нестабильная ветвь Z3 содержит исправление.

Можно переписать свой пример, используя только «вставку» вместо «хвоста» головы. Например, замените (head t) на 's1' и замените 't' в другом месте на '(insert s t)'.

Вы можете использовать либо предложения из чистого урона в SMT-LIB2, либо команду set (логическая команда HORN) для вызова одного из доступных решателей предложения Horn или использовать синтаксис расширения фиксированной точки, который имеет некоторые удобства для объявления переменных. Есть несколько бэкэндов. Основными из них являются: - «datalog»: решатель Datalog на основе хэш-таблицы. Отношения должны быть связаны с конечными переменными домена. - 'pdr': отношения должны быть над булевыми, арифметическими, битовыми векторами и/или алгебраическими типами данных. - 'bmc': ограниченная проверка модели, разворачивающая предложения рога, соответствующие соотношению перехода. Другие двигатели также присутствуют, но это основные из них.

Семантика предложений HORN в SMT-LIB2 такая же, как семантика SMT-LIB2. Специальной семантики нет, но решатели Хорна будут иметь возможность обрабатывать конъюнкцию формул, которые соответствуют предложениям Хорна. Ваш пример может быть выражен с использованием только предложений Horn: каждое правило является импликацией, а запрос соответствует опровергнутому предложению (отрицает запрос и утверждает его вместе с другими предложениями. Когда результирующий набор предложений является ненасыщенным, тогда запрос возможно, когда результирующий набор условий является выполнимым, тогда запрос является необратимым).