Решение для х = 2 не удается при использовании Z3.Monad в Haskell - PullRequest
Новая
       7

Решение для х = 2 не удается при использовании Z3.Monad в Haskell

0 голосов
/ 25 августа 2018

Я пытаюсь сделать действительно простой пример с использованием интерфейса Z3.Monad в Haskell. К сожалению, в пакете нет простого рабочего примера, поэтому я начинаю с нуля. Я также проверил, и примеры, перечисленные в пакете, работают для меня, поэтому не должно быть никаких проблем с моей установкой Z3.

Что я делаю

Эта функция не работает при запуске: 

import Z3.Monad

computeTwo = evalZ3 $ do
    x <- mkFreshIntVar "x"
    _2 <- mkInteger 2
    assert =<< mkEq x _2
    fmap snd $ withModel $ \m -> fromJust <$> evalInt m x

Я получаю следующую ошибку: 

uncaught exception: ErrorCall
Z3.Base.toBool: illegal `Z3_bool' value
CallStack (from HasCallStack):
  error, called at src/Z3/Base.hs:3197:23 in z3-4.3.1- 
JxhFvE2Tmnm1VKrfgyob6s:Z3.Base

Какой ответ ожидался

Модель должна проверить с x = 2.

Что еще я пробовал

Эквивалентный пример работает в онлайн-контролере Z3 

(declare-const x Int)
(assert (= x 2))
(check-sat)
(get-model)

Предоставление ответа: 

sat
(model 
  (define-fun x () Int
    2)
)

1 Ответ

0 голосов
/ 26 августа 2018

Исправлено:

1) Обновление XCode

Использование App Store.

2) Переустановка z3 

 brew uninstall z3
 brew install z3
 echo 'export PATH="/usr/local/opt/openssl/bin:$PATH"' >> ~/.bash_profile
 echo 'export LDFLAGS="-L/usr/local/opt/openssl/lib"' >> ~/.bash_profile
 echo 'export CPPFLAGS="-I/usr/local/opt/openssl/include"' >> ~/.bash_profile

Последние три были конкретными инструкциями из процесса brew install.

Спасибо всем за помощь.

...