Z3 Java API - получить ядро ​​unsat

Я пытаюсь понять, как получить ядро ​​unsat с помощью Java API для Z3. Наш сценарий выглядит следующим образом (внизу код, который работает в rise4fun):

  1. Создаем вход SMT2 программно
  2. Входные данные содержат определения функций, объявления типов данных и утверждения.
  3. Мы разбираем это с помощью API parseSMTLIB2String.
  4. Мы гарантируем, что контекст и решатель имеют unsat_core -> true
  5. Z3 возвращает UNSAT для предоставленного ввода, что является правильным
  6. Однако ядро ​​UNSAT всегда пусто.
  7. Тот же самый ввод правильно производит ядро ​​UNSAT на rise4fun (x1 x3)

Я предполагаю, что как-то неправильно использую API ... но не совсем уверен, как / почему.

Я заметил, что я не могу установить опцию unsat core в строке SMT, которую я передаю parseSMTLIB2String, потому что это недопустимо. Я предполагаю, что это ожидается.

Кто-нибудь может указать мне правильное направление, пожалуйста?

Спасибо!!

(set-option :smt.macro-finder true)

;; The following is only for rise4fun, i cannot get it 
;; to work with the parse SMT Java API
(set-option :produce-unsat-cores true)

(define-sort Ref () Int)

(declare-datatypes (T1 T2) ((Tuple2 (mk-Tuple2 (_1 T1)(_2 T2)))))
(declare-datatypes (T1 T2 T3) ((Tuple3 (mk-Tuple3 (_1 T1)(_2 T2)(_3 T3)))))

(define-sort Set (T) (Array T Bool))
(define-sort Bag (T) (Array T Int))

(declare-const emptySetOf_Int (Set Int))
(assert (!(forall ((x Int)) (= (select emptySetOf_Int x) false)) :named AXIOM1))

(declare-sort TopLevelDeclarations) (declare-const mk-TopLevelDeclarations TopLevelDeclarations)
(declare-datatypes () ((A (mk-A (x Int)(y Int)))))

(declare-datatypes () ((Any
  (lift-TopLevelDeclarations (sel-TopLevelDeclarations TopLevelDeclarations))
  (lift-A (sel-A A))
  null))
)

(declare-const heap (Array Ref Any))

(define-fun deref ((ref Ref)) Any
  (select heap ref)
)

(define-fun deref-is-TopLevelDeclarations ((this Ref)) Bool
  (is-lift-TopLevelDeclarations (deref this))
)

(define-fun deref-TopLevelDeclarations ((this Ref)) TopLevelDeclarations
  (sel-TopLevelDeclarations (deref this))
)

(define-fun deref-is-A ((this Ref)) Bool
  (is-lift-A (deref this))
)

(define-fun deref-A ((this Ref)) A
  (sel-A (deref this))
)

(define-fun deref-isa-TopLevelDeclarations ((this Ref)) Bool
  (deref-is-TopLevelDeclarations this)
)

(define-fun deref-isa-A ((this Ref)) Bool
  (deref-is-A this)
)

(define-fun A!x ((this Ref)) Int
  (x (deref-A this))
)

(define-fun A!y ((this Ref)) Int
  (y (deref-A this))
)

(define-fun TopLevelDeclarations.inv ((this Ref)) Bool
  true
)

(assert (! (forall ((this Ref))
  (=> (deref-is-TopLevelDeclarations this) (TopLevelDeclarations.inv this))
) :named x0))

(define-fun A.inv ((this Ref)) Bool
  (and
    (> (A!x this)  0)
    (> (A!y this)  0)
    (< (A!x this)  0)
  )
)

(assert (! (forall ((this Ref))
  (=> (deref-is-A this) (A.inv this))
) :named x1))

(assert (!(deref-is-TopLevelDeclarations 0) :named TOP))
(assert (!(exists ((instanceOfA Ref)) (deref-is-A instanceOfA)) :named x3))

(check-sat)
(get-unsat-core)

z3 smt theorem-proving
person r-k    schedule 15.09.2015    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Вы не используете Java API, за исключением вызова parseSMTLIB2String. Эта функция не выполняет никаких SMT-команд, и нет функции, которая могла бы сделать это за вас. parseSMTLIB2String существует исключительно для анализа утверждений, все остальное игнорируется. Для этой конкретной проблемы я рекомендую просто передать файл проблемы z3.exe либо в качестве аргумента командной строки, либо через стандартный ввод (используйте параметр -in). Это производит

unsat
(x1 x3)

Если позже планируется использовать Java API для других целей, см. Пример ненадежного ядра Java API.

person Christoph Wintersteiger    schedule 16.09.2015
comment
Спасибо, Кристоф. Я просто пропустил это, но мы добавляем возвращенный BoolExpr в решатель, созданный из контекста, а затем используем API для проверки. Передача его в Z3.exe - это нормально, но на самом деле нас также интересуют случаи, когда модель является SAT, а затем анализируется модель, возвращенная Z3, что, на мой взгляд, сложно при простом вызове z3.exe. Или это не так? - person r-k; 16.09.2015
comment
Это вопрос перспективы ... модели также относительно легко анализировать (просто добавьте (get-model) после (check-sat), чтобы выгрузить их), но это немного сложнее, чем анализ вывода ядра unsat. Лично я предпочитаю делать это через API. - person Christoph Wintersteiger; 16.09.2015
comment
Да, мы используем API, чтобы получить модель, а затем проанализировать ее. Итак, мой вопрос все еще остается: почему я не вижу ядра UNSAT при использовании Java API getUnsatCore ... - person r-k; 16.09.2015
comment
Дело в том, что я на самом деле никогда не создаю константы типа bool с помощью API - я просто использую возвращенный BoolExp и передаю его решателю ...? - person r-k; 16.09.2015
comment
Я подтвердил, что, поскольку я не создаю логические константы и выражения (поэтому у меня нет символов), ядро ​​unsat не работает. Немного неинтуитивно, потому что я мог подумать, что API синтаксического анализа втянет имена ... Итак, в этом случае я переключился на использование исполняемого файла Z3. Спасибо, Кристоф. - person r-k; 16.09.2015
comment
Да, это правильно. Парсер действительно нужен только для удобства разбора простых выражений. Я думаю, что он анализирует имена, но есть несколько других параметров, которые необходимо включить, чтобы ядра unsat работали (например, unsat_core = true в контексте и / или целях, потому что синтаксический анализатор не будет выполнять команды set-option ). - person Christoph Wintersteiger; 17.09.2015

arrow_upward
0
arrow_downward

У меня была такая же проблема, и я обнаружил, что это зависит от того, как вы передаете проанализированный ввод в решатель.

В то время как следующий подход создает пустое ядро ​​unsat-core ...:

BoolExpr[] program = context.parseSMTLIB2File(input_file, null, null, null, null);
solver.add(program);
solver.check();
solver.getUnsatCore();

... ядро ​​unsat-core создается правильно, если вы передаете проанализированный входной файл решателю следующим образом:

BoolExpr[] program = context.parseSMTLIB2File(input_file, null, null, null, null);
solver.check(program);
solver.getUnsatCore();

Поэтому я предполагаю, что все, что передается через solver.add(), принадлежит предположениям и, следовательно, предположительно не принадлежит ненадежному ядру согласно Z3.

person Pascal    schedule 01.07.2021