Z3 получает FuncInterp как ноль - PullRequest
Новая
       11

Z3 получает FuncInterp как ноль

0 голосов
/ 07 июля 2019

Я использую Java API Z3 для разбора файла SMT; когда я звоню s.getModel(), где s - решатель, я могу правильно напечатать модель следующим образом: 

(define-fun O_STUDENT () (Array Int STUDENT_TupleType)
  ((as const (Array Int STUDENT_TupleType))
  (STUDENT_TupleType _ID__12345 _NAME__Bourikas _DEPT_uNAME__Music 29)))
(define-fun O_DEPARTMENT () (Array Int DEPARTMENT_TupleType)
  ((as const (Array Int DEPARTMENT_TupleType))
  (DEPARTMENT_TupleType _DEPT_uNAME__Music _BUILDING__BUILDING_u5 50000.0)))

Однако, когда я пытаюсь получить массив FuncInterp для O_STUDENT, я получаю null. Я использую следующее для извлечения этого значения: 

if (s.check() == Status.SATISFIABLE) {
            Model m = s.getModel();
            FuncDecl arrayDep = m.getConstDecls()[0];
            System.out.println(m.getFuncInterp(arrayDep));
        }

1 Ответ

0 голосов
/ 08 июля 2019

На всякий случай: массивы немного особенные, потому что есть константы, но их модели являются функциями (см., Например, https://github.com/Z3Prover/z3/blob/master/src/api/java/Model.java#L88).

Модели могут не содержать назначения для всех переменных - если одна отсутствует, это означает, чточто вы можете выбрать любое значение, которое вам нравится. Если вам не нравится это, вы можете включить завершение модели, и Z3 выберет для вас.

...