cvc4

1зной

1ответ

Как выполнить следующий код SMT-LIB с помощью Alt-Ergo

Следующий код SMT-LIB работает без проблем в Z3, MathSat и CVC4, но он не работает в Alt-Ergo, пожалуйста, дайте мне знать, что происходит, много спасибо : (set-logic QF_UF) (set-option :incremental

2зной

1ответ

Решение экземпляров dimacs с решателем SMT кажется медленным (формат SMT2)

Я преобразовываю свою проблему в SMT, и я заметил, что решатели SMT (MathSat5 и CVC4) медленны при решении сильных экземпляров. Моя приостановка заключается в том, что в моем переводе есть что-то, что

1зной

2ответ

Есть ли какая-либо функция, которая легко доступна для вычисления логарифма на базе 2 в Z3/cvc4?

Я хочу доказать упрощение, которое включает в себя вычисление журнала на базу 2. Есть ли какая-либо функция, доступная в z3/cvc4 для ее вычисления?

1зной

2ответ

Как использовать Z3 и CVC4 с SMT-LIB для доказательства теорем для диэдральной группы D3

В предыдущей post была доказана одна теорема для диэдральной группы D3 с использованием Z3 SMT-LIB. В этом посте мы попытаемся доказать такую теорему, используя как Z3 и CVC4 с помощью следующей SMT

0зной

1ответ

Как запустить следующий код SMT-LIB с помощью Alt-Ergo

Следующий код SMT-LIB работает без проблем в Z3, MathSat и CVC4, но он не работает в Alt-Ergo, пожалуйста, дайте мне знать, что происходит, много спасибо : (set-logic QF_LIA) (set-option :interactive