Вопросы по теме 'z3'
Статистика Z3: что измеряет время?
Я получаю странные результаты статистики при запуске Z3 3.1 с опцией -st. Если вы нажмете Ctrl-C, Z3 сообщит общее время ‹ время. В противном случае, если вы дождетесь завершения Z3: total_time > time.
Что измеряют «общее время» и «время»?...
546 просмотров
schedule
24.10.2023
Поддержка AUFBV?
Будет ли Z3 поддерживать AUFBV?
Для следующего скрипта:
(set-logic AUFBV)
(declare-fun x () (_ BitVec 16))
(declare-const t (Array (_ BitVec 16) (_ BitVec 16)))
(assert (= (select t #x0000) #x0000))
Онлайн-демонстрация Z3, кажется,...
520 просмотров
schedule
24.02.2024
Используемые предпосылки/аксиомы в доказательствах Z3 TPTP
При использовании Z3 в файлах TPTP (например, http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=SYN&File=SYN054+1.p ) есть ли способ узнать, какие аксиомы использовались доказать предположение? В качестве альтернативы, может ли...
224 просмотров
schedule
06.03.2024
Исключение квантификатора - дополнительные вопросы
Большое спасибо Джошу и Леонардо за ответы на предыдущий вопрос.
У меня еще несколько вопросов.
‹1> Рассмотрим другой пример.
(exists k) i * k > = 4 and k > 1.
У этого есть простое решение i> 0. (как для Int, так и для Real...
2212 просмотров
schedule
15.12.2023
Преобразовать формулу в CNF
Есть ли способ использовать z3 для преобразования формулы в CNF (с использованием кодирования в стиле Цейцина)? Я ищу что-то вроде команды simplify , но гарантирую, что возвращаемая формула является CNF.
2941 просмотров
schedule
24.10.2022
(Z3Py) проверка всех решений уравнения
Как в Z3Py проверить, имеет ли уравнение для заданных ограничений только одно решение?
Если решений несколько, как их перечислить?
8072 просмотров
schedule
09.06.2024
О теории массивов в Z3
Я хочу знать, могу ли я заставить Z3 «запомнить» обновление массива.
Например, следующий ввод допустим:
(declare-const x Int)
(declare-const a1 (Array Int Int))
(assert (= (select (store a1 x 2) x) 2))
(assert (not (= (select a1 x) 2)))...
960 просмотров
schedule
20.01.2024
Поддержка многомерных массивов в QF_AUFBV?
В настоящее время я работаю над кодом, который переводит «путь» через программу C в соответствующий запрос SMT, чтобы проверить возможность этого пути. У меня есть рабочий код, который создает запрос SMT-LIB v1.2 и использует Z3 2.11 и логику...
616 просмотров
schedule
06.06.2024
У меня проблемы с DLL с F# Interactive в Visual Studio 2012
Я запускаю VS 2012 на 64-битной машине, но я установил для параметра «F # 64-битный интерактивный» значение False, что означает, что по умолчанию должен использоваться 32-битный процесс.
Я вызываю 32-битную DLL, и моя программа компилируется...
173 просмотров
schedule
18.04.2024
содержит для двух наборов в Z3
Если я хочу проверить, есть ли в наборе элементы другого набора, это также возможно?
Например (содержит Set1 Set2):
contains [1,2] [3,5] -> is false
contains [1] [2,3, 1] -> is true
Множества конечны. И максимальное значение наборов...
461 просмотров
schedule
30.10.2023
Использование Z3Py с Python 3.3
Моя ситуация
Я установил Microsoft Z3 ( Z3 [version 4.3.0 - 64 bit]. (C) 2006 ) и pyc исполняемых файлов для Python2.
Я написал пакет Python3, которому нужен доступ к функциям z3 .
Чтобы иметь возможность использовать pyc двоичные файлы...
2938 просмотров
schedule
11.02.2024
Опция bv-enable-int2bv-propagation
(set-option :bv-enable-int2bv-propagation true) работает онлайн. Но моя локальная версия жалуется на это, говоря:
(ошибка «строка 1, столбец 43: неизвестный параметр« bv_enable_int2bv_propagation », это старое имя параметра, вызовите« z3 -p...
321 просмотров
schedule
08.05.2024
рассказывая о разнице между слабыми переменными и исходными переменными в Z3
Я пытаюсь создать новый вид нарезки, чтобы заменить нарезки gomory, реализованные в Z3. Я разработал свой разрез для работы с исходным ограничением, введенным пользователем. К сожалению, я обнаружил, что предварительная обработка Z3 ограничений...
175 просмотров
schedule
27.09.2022
получение неизвестного результата с тривиальным forall
Я использую API z3 C++. если я создам это простое ложное выражение:
z3::expr x = C->int_const("x");
z3::expr p = z3::forall(x, x==0);
и пытаюсь решить, я получаю неизвестный результат. Я не специалист по стратегиям и тактикам, но уверен,...
256 просмотров
schedule
25.01.2024
Утверждения именования Microsoft Z3
Мне нужно назвать некоторые утверждения в моей модели z3, чтобы она могла генерировать ненасыщенные ядра.
Я могу сделать это вручную следующим образом:
(assert (! (assertion) :named x))
Мне просто нужно сделать это напрямую с помощью .NET...
716 просмотров
schedule
18.11.2022
Ускорение использования Z3py для проверки выполнимости формулы
Меня зовут Вэй-Фан. Я попытался использовать Z3py для проверки выполнимости конкретной формулы, которая показана следующим образом:
from z3 import *
import time
import sys
import signal
UNIT_TIMEOUT = 300
# ==== time out exception class and...
142 просмотров
schedule
10.02.2024
Ускорьте z3-solver с правильной тактикой
Я создаю около 20 тысяч ограничений, и на моем компьютере их решение занимает около 3 минут. У меня разные ограничения, и ниже я привожу примеры и объясняю их. Я загрузил утверждения на http://filebin.ca/vKcV1gvuGG3 .
Я заинтересован в решении...
601 просмотров
schedule
18.12.2023
Есть ли способ использовать Z3 для получения моделей ограничений, включающих последовательности и карты?
Некоторое время назад я спросил, как я могу использовать Z3 для получения моделей для ограничений, включающих наборы ( Есть ли способ использовать Z3 для получения моделей ограничений, включающих наборы? ). Для этого в моем случае хорошо работает...
265 просмотров
schedule
08.01.2024
Процедурное вложение в Z3
Я использую z3py. У меня есть предикат над двумя целыми числами, которые необходимо оценить с использованием пользовательского алгоритма. Я пытался реализовать его, но без особого успеха. По-видимому, мне нужно процедурное вложение, которое сейчас...
121 просмотров
schedule
09.12.2022
Как я могу проверить, является ли логическое выражение буквально TRUE или FALSE?
Я создал следующую программу:
context c;
expr x = c.int_val(1);
expr y = c.int_val(2);
expr b = (x > y).simplify();
std::cout << "b = " << b << "\n";
Вывод сказал, что b = false. Но как я могу проверить, является ли b...
52 просмотров
schedule
14.01.2024
