Есть ли способ анализа выходных данных модели Z3 с привязками Java? - PullRequest
Новая
       71

Есть ли способ анализа выходных данных модели Z3 с привязками Java?

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

У меня есть файл .smt, и я пытаюсь проанализировать его с помощью Java привязок, используя context.parseSMTLIB2File(). Моя проблема в том, что Z3 CLI и привязки дают разные модели в качестве результатов. Я согласен, что результаты отличаются, за исключением того, что в некоторых случаях выражения ite имеют 2 различных значения при использовании CLI и 3 различных значения при использовании solver.getModel() из привязок Java; см. следующий пример:

С Z3 CLI я получаю 

sat
((O_STUDENT (lambda ((x!1 Int))
  (ite (<= 2 x!1)
       (STUDENT_TupleType _ID__00128 _NAME__Snow NULL_DEPT_NAME_1 94)
       (STUDENT_TupleType _ID__12345 _NAME__Snow NULL_DEPT_NAME_1 94)))))

Но с привязками Java я получаю следующую интерпретацию для того же массива O_STUDENT (I ' ve System.out.println редактировал объявление и возвращенное значение solver.getConstInterp в объявлении): 

(declare-fun O_STUDENT () (Array Int STUDENT_TupleType))
(lambda ((x!1 Int))
  (let ((a!1 (ite (= (ite (<= 2 x!1) 2 1) 2)
                  (STUDENT_TupleType
                    _ID__12345
                    _NAME__Bourikas
                    NULL_DEPT_NAME_1
                    94)
                  (STUDENT_TupleType
                    _ID__19991
                    _NAME__Bourikas
                    _DEPT_uNAME__Music
                    2))))
    (ite (= (ite (<= 2 x!1) 2 1) 1)
         (STUDENT_TupleType _ID__00128 _NAME__Bourikas NULL_DEPT_NAME_1 94)
         a!1)))

То, что я хотел бы иметь, - это одинаковое количество различных значений (однако они могут отличаться) , Поскольку я пытался получить те же результаты, что и интерфейс командной строки с привязками Java, напрасно, я хотел бы использовать CLI Z3 для моего файла, а затем проанализировать его вывод обратно с привязками Z3 Java (ie, Я намерен проанализировать интерпретацию модели из CLI Z3, используя привязки Java.

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

PS: вместо этого использовать solver.fromFile() context.parseSMTLIB2File() для разбора файла дал те же результаты.

...