Вопросы по теме 'z3py'
Найдите логические условия эквивалентности двух формул?
Я опубликовал связанный с этим вопрос , но тогда я думаю, что это было не очень Чисто. Я хотел бы перефразировать проблему следующим образом:
Две формулы a1 == a + b (1) и a1 == b (2) эквивалентны, если a == 0 . Учитывая эти формулы (1) и...
155 просмотров
schedule
27.08.2023
Почему этот код возвращает Unsat (формула с использованием ForAll и подразумевает)?
Даны 2 уравнения c == a + 4 и t == c + b , если a == -4 , то t == b . Я пытаюсь сделать наоборот, то есть с учетом двух приведенных выше уравнений и t == b я пытаюсь найти значение a .
У меня есть код ниже, чтобы сделать это с помощью...
194 просмотров
schedule
08.12.2022
Как решить экземпляр 2-SAT с 60 булевыми переменными и 99 предложениями с помощью Z3Py
Я использую следующий код:
X = BoolVector('x', 60)
M = [[21, 34],[-49, -12],[7, 18],
[-5, -1],[28, 17],
[3, 55],[36, 33],
[-6, -50],[44, -41],
[-55, 3],[14, -54],[-30, 13],
[-13, 60],[54, -16],[-48, 41],
[3, 6],[49,...
286 просмотров
schedule
18.08.2022
Z3Py Вычисление с фиксированной точкой слишком слабое
Я использую API-интерфейсы z3py для вычисления набора индуктивных аннотаций. Я сопоставляю свои ограничения с конъюнкцией обобщенных предложений Хорна. Среди ограничений есть пара отношений (l6 и iwc1), которые необходимо вывести. Все вовлеченные...
90 просмотров
schedule
16.11.2022
z3py на rise4fun недоступен несколько недель
Я много использовал сайт rise4fun z3py, и он мне очень понравился.
Однако, поскольку несколько недель при попытке доступа
http://rise4fun.com/z3py
Меня перенаправляют на
http://rise4fun.com
Сайт http://rise4fun.com/z3 работает, но...
315 просмотров
schedule
04.05.2022
Как эффективно решать комбинации теорий в Z3
Я пытаюсь решить проблему, связанную с пропозициональной выполнимостью (с кванторами) и линейной арифметикой.
Я сформулировал задачу, и Z3 в состоянии ее решить, но это занимает неоправданно много времени.
Я пытался помочь Z3, указав тактику, но...
252 просмотров
schedule
10.04.2022
Как определить матрицу?
Похоже, что Microsoft полностью испортила свой веб-сайт «rise4fun», и руководство по Z3 Python больше не загружается.
Как я могу определить матрицу в Z3 для Python и наложить на нее некоторые ограничения?
214 просмотров
schedule
02.07.2022
z3python: использование математической библиотеки
Я пытался использовать математическую библиотеку Python с z3python, что я сделал:
import z3
import math
a,b = z3.Reals('a b')
solve(b == math.factorial(a), b == 6)
Он возвращает сообщение об ошибке AttributeError: экземпляр ArithRef не имеет...
286 просмотров
schedule
15.02.2023
z3py выдает ошибку парсера для действительного файла SMT2
1 (set-logic UFLIA)
2 (set-info :source | Simple list theorem |)
3 (set-info :smt-lib-version 2.0)
4 (set-info :category "crafted")
5 (set-info :status unsat)
6 (declare-sort List 0)
7 (declare-sort Elem 0)
8 (declare-fun cons (Elem...
768 просмотров
schedule
29.12.2022
Это ошибка в Z3? Неправильный ответ на применение Real и ForAll
Я пытаюсь найти минимальное значение Параболы y=(x+2)**2-3, видимо, ответ должен быть y==-3, когда x ==-2. Но z3 дает ответ [x = 0, y = 1], который не соответствует утверждению ForAll.
Я что-то неправильно предполагаю?
Вот код питона:
from...
280 просмотров
schedule
13.04.2022
z3py: Как правильно утверждать, что ограничение чего-то не существует?
Я хочу установить ограничение «что-то не должно существовать» в z3py. Я попытался использовать «Не (существует (...))». Простой пример таков. Я хочу найти задание для a и b, чтобы такого c не существовало.
from z3 import *
s = Solver()
a =...
377 просмотров
schedule
26.05.2022
z3, z3py: Могу ли я определить сортировку, включающую набор целых чисел?
Это дополнительный вопрос к моему предыдущему вопросу of-function">"Возможно ли существенно уменьшить пространство поиска Function" .
Я думаю, возможно ли определить сортировку, содержащую набор целых чисел, например, целые числа 1-10.
Моя...
772 просмотров
schedule
21.08.2022
Простое упражнение Z3, возвращающее неизвестное значение
Я начинаю использовать решатели SMT, и я практиковался с этой простой проблемой:
Exercise 5. Using Z3 at the restaurant:
(a) Encode the following menu choices into Z3 and determine what a customer could buy using exactly
$15.05
• Mixed fruit...
219 просмотров
schedule
15.09.2022
Может ли z3py добавить новое утверждение после чтения модели?
Мы можем использовать следующий код, чтобы решить головоломку Dog, Cat, Mouse в учебнике.
dog, cat, mouse = Ints('dog cat mouse')
s = Solver();
s.add(dog>=1)
s.add(cat>=1)
s.add(mouse>=1)
s.add(dog+cat+mouse==100)
s.add(1500 * dog + 100...
63 просмотров
schedule
20.03.2023
Python Оптимизировать систему неравенств
Я работаю над программой на Python, в которой небольшая часть связана с оптимизацией системы уравнений/неравенств. В идеале я хотел бы сделать то, что можно сделать в Modelica, написать уравнения и позволить решателю позаботиться об этом.
Работа с...
3019 просмотров
schedule
26.06.2022
Может ли Z3 эффективно решать ограничения с максимальной операцией?
Предположим, я хочу решить следующее ограничение: y == max(x, 0) . Что я мог придумать, так это закодировать следующее (в интерфейсе z3py): If(x > 0, y == x, y == 0) . Мои вопросы были:
Будет ли Z3 внутренне преобразовывать приведенное...
605 просмотров
schedule
07.04.2022
Будет ли Z3 адаптивно менять стратегию решения линейных вещественных арифметических ограничений?
У меня есть огромный набор линейных вещественных арифметических ограничений, которые нужно решить, и я постепенно передаю их решателю. Z3 всегда, кажется, застревает через некоторое время. Собирается ли Z3 изменить свою стратегию при разрешении...
68 просмотров
schedule
09.12.2022
Подсчет количества переменных в количественной формуле Z3
Я пытаюсь собрать все переменные в формулу (количественная формула в Z3py). Небольшой пример
w, x, y, z = Bools('w x y z')
fml = And( ForAll(x, ForAll(y, And(x, y))), ForAll(z, ForAll(w, And(z, w))) )
varSet = traverse( fml )
Код, который...
167 просмотров
schedule
21.12.2022
z3py BitVector, смешанный с целочисленными операциями
Имея ( lst_v ) список BitVectors и ( lst_b ) список значений логических выражений. Как вы выполняете следующие операции с помощью z3py:
используйте lst_b для маскировки элементов в lst_v . Маскирование необходимо для использования функции...
149 просмотров
schedule
26.08.2022
Как добавить ограничение, которое требует, чтобы целочисленная переменная принадлежала массиву?
Предположим, у меня есть z3py целочисленная переменная x = Int('x') и целочисленный массив a = [1, 2, 3] . Затем я добавляю ограничение через s.add (x in a).
Я думаю, что это приемлемо, потому что x может быть 1 or 2 or 3 . Но на самом...
790 просмотров
schedule
10.08.2022
