Описание тега cvc4
CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
1
ответ
Кодировка возвращает "неизвестно"
Для этого примера: http://pastebin.com/QyebfD1p z3 и cvc4 возвращают "unknown" в результате проверки-сата. Оба не слишком многословны в отношении причины, есть ли способ сделать z3 более многословным в отношении его выполнения?
11 фев '13 в 22:00
1
ответ
Как выполнить следующий код SMT-LIB, используя Alt-Ergo
Следующий код SMT-LIB работает без проблем в Z3, MathSat и CVC4, но не работает в Alt-Ergo, пожалуйста, дайте мне знать, что происходит, большое спасибо: (set-logic QF_UF) (set-option :incremental true) (set-option :produce-models true) (declare-fun…
01 июн '13 в 15:10
1
ответ
Моделирование логической головоломки
Я пытаюсь смоделировать логическую головоломку из " Перемешать пересмешника". Я изо всех сил пытаюсь перевести его в SMT-LIB. Головоломка выглядит примерно так: Есть сад, в котором все цветы красного, желтого или синего цветов и представлены все цве…
10 дек '18 в 17:59
1
ответ
Разница в кодировании одной и той же аксиомы
Мне интересно, в чем разница между этими двумя кодировками одной и той же аксиомы списка: (define-sort T1 () Int) (declare-fun list_length ( (List T1) ) Int) (assert (forall ( (i T1) (l (List T1)) ) (ite (= l (as nil (List T1))) (= (list_length l) 0…
04 янв '19 в 21:20
0
ответов
Ошибка синтаксиса плагина frama-c wp при использовании средства проверки CVC4
С примером файла find.c я могу без проблем доказать это, используя alt-ergo по умолчанию. Но при переходе на cvc4 выдается предупреждение и синтаксическая ошибка. Вот код: /*@ requires 0 <= n && \valid(a+(0..n-1)); assigns \nothing; ensur…
01 ноя '18 в 23:51
1
ответ
LibGMP не найден при установке CVC4 на FreeBSD
Я пытаюсь скомпилировать CVC4 из исходного кода на FreeBSD, но я сталкиваюсь с ошибкой во время настройки - GMP не может быть найден, даже если общий объект явно находится на общем пути: $> ls /usr/local/lib | grep gmp libgmp.a libgmp.la libgmp.s…
10 сен '14 в 02:17
1
ответ
Логарифм / Экспонента вещественных чисел в cvc4
Я ищу решателя, который может предоставить модели формул на действительные числа, включающие логарифмы или экспоненты. Может ли cvc4 обрабатывать функции, которые содержат логарифмы или экспоненты действительных чисел? Точно так же может cvc4 вырази…
20 ноя '17 в 13:35
1
ответ
Поддерживает ли z3 рациональную арифметику для своих входных ограничений?
На самом деле, стандарт SMT-LIB имеет рациональную (а не только реальную) сортировку? Судя по его сайту, это не так.Если x рационально и у нас есть ограничение x^2 = 2, то мы должны получить обратно "неудовлетворительно". Самое близкое, что я мог по…
29 июн '15 в 16:06
1
ответ
cvc4 mkconst из std::string в C++ API
Мне нужно изменить "123" в const в C++, что я закодировал как ExprManager em; Rational i = Rational("123",10); Expr expri = em.mkConst(i); или же Integer i = Integer("123", 10); Expr epri = em.mkConst(Rational(i,1)); но я получил ошибку Неопределенн…
23 янв '18 в 22:00
0
ответов
CVC4: использование квантификаторов в интерфейсе C++
Я пытаюсь понять, как кодировать квантификаторы в CVC4, используя интерфейс C++. Вот пример, который я пытаюсь запустить, но не могу. int main() { SmtEngine smt(&em); smt.setLogic("AUFLIRA"); // Set the logic Expr three = em.mkConst(Rational(3))…
29 ноя '14 в 02:15
1
ответ
Сообщение "Неизвестный логический символ map.Map.const" в Why3
Я экспериментирую с Why3, следуя их руководству, но я получаю сообщение Unknown logical symbol map.Map.const для нескольких пруверов. Вот содержание теории, которую я пытаюсь доказать: theory List type list 'a = Nil | Cons 'a (list 'a) predicate mem…
08 мар '17 в 16:39
1
ответ
Утверждения об индуктивных типах данных в CVC4
Я пытаюсь немного поэкспериментировать с CVC4. (set-option :produce-models true) (set-option :produce-assignments true) (set-logic QF_UFDT) (declare-datatypes () (Color (Red) (Black)) ) (declare-const x C) (declare-const y C) (assert (not (= x y))) …
22 апр '17 в 10:21
2
ответа
Внедрение дробеструйной обработки для арифметики с плавающей точкой в SMT
Мне было интересно, как люди реализуют дробеструйные арифметические конструкции с плавающей точкой в решателях SMT. Существуют ли какие-либо библиотеки или средства для этого (VHDL, ...) или они реализованы с нуля? Это представляет сколько строк к…
03 янв '17 в 14:23
1
ответ
Значение (_ bv0 32), (_ bv1 16) ... в тестах SMT2
Я заметил, что это некоторые тесты SMT2, обозначения, такие как (_ bv0 32), (_ bv16 32),... используются как, например, в: QF_FP / Schanda / искровым / zeros_consistent_2.smt2 http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_smal…
23 сен '16 в 08:56
0
ответов
Разве нельзя использовать массив пользовательских типов данных с CVC4?
Используя последнюю версию cvc4 по состоянию на 2018-07-10, этот код: (set-info :smt-lib-version 2.6) (set-logic ALL) (declare-datatypes ( (Type 0) ) ( ((bool) (number) (tuple (tuple-type (Array Int Type)))) )) производит этот вывод из cvc4: (error …
10 июл '18 в 14:35
1
ответ
Ошибка разбора CVC4 (та же формула пропускает Z3)
Следующие разделы SMT проходят решение по ограничению Z3, а CVC4 отмечает ошибку синтаксического анализа: "Символ" None ", ранее объявленный как переменная". Я протестировал с использованием CVC4 1.4 и CVC 1.5 на Windows. Есть предложения или мысли?…
22 авг '17 в 13:52
1
ответ
Дискретные временные шаги в Z3 / CVC4 / SMT-LIB
Я определяю временные шаги, используя Int в SMT-LIB, что заставляет меня утверждать, что ничего не происходит в негативах: (declare-sort Pkg) ; A package (define-sort Time () Int) ; The installation step ; ... (assert (forall ((t Time) (p Pkg)) (=&g…
02 мар '18 в 18:17
1
ответ
Как повернуть битвектор в cvc4 с помощью API C++
Я пытаюсь повернуть битовый вектор в cvc4, используя C++ API, но API немного сбивает с толку, когда дело доходит до выражений операторов. Используя следующий код (выдержка): #include <iostream> #include <cvc4/cvc4.h> using namespace std;…
23 дек '16 в 11:27
1
ответ
Z3 может быть несовместимым при решении этой проблемы со строками?
Я только что столкнулся с проблемой SMTLIB в теории струн, что Z3 мог ответить непоследовательно. При вызове Z3 для решения проблемы: с аргументом smt.string_solver=z3str3 это возвращается unsat; без каких-либо аргументов возвращает sat, Я также исп…
01 окт '18 в 07:53
2
ответа
Каковы пределы рассуждений в количественной арифметике в SMT?
Я попробовал несколько решателей SMT (CVC3, CVC4 и Z3) на следующем, казалось бы, тривиальном тесте: (set-logic LIA) (set-info :smt-lib-version 2.0) (assert (forall (( x Int)) (forall ((y Int)) (= y x)))) (check-sat) (exit) Все решатели возвращаются…
20 фев '13 в 19:27