Описание тега pysmt
PySMT - это API-интерфейс Python для взаимодействия с различными решателями SMT.
1
ответ
Как использовать массив в PySMT?
У меня проблема с PySMT. Я новичок в этой области и понятия не имею, как использовать массивы. Это я поняла: 1) Можно объявить массив как: a = Symbol("a", ArrayType(INT, INT)) 2) Затем, чтобы сохранить значения в массиве: k = Store(a, Int(0), int(5)…
21 июл '19 в 00:59
0
ответов
Python и angr: как подавить предупреждение об устаревании
Я использую angrframework и Python 3.8. Независимо от того, что я делаю, я получаю следующее предупреждение: /home/ruturaj/.local/lib/python3.8/site-packages/pysmt/walkers/generic.py:43: DeprecationWarning: Using or importing the ABCs from 'collecti…
21 мар '20 в 20:16
1
ответ
Вывести ограничения SMTLib на стандартный вывод в PySMT
У меня проблема с кодированием с использованием API-интерфейсов PySMT. На странице PySMT на GitHub показан пример использования любого SMTLib-совместимого решателя с PySMT. В нем говорится, что PySMT передаст проблему для решения в stdin. Но я не мо…
06 май '21 в 10:20
0
ответов
arm-linux-gnueabi-g++: файл .so не распознан
Я хотел бы скомпилировать MathSat на EV3 Mindstorm с ev3dev в качестве ОС. Для этого я использую установщик, предоставленный PySMT (PySMT успешно установлен): pysmt-install --msat Дополнительно я установил несколько необходимых пакетов: sudo apt-get…
15 май '21 в 22:50
0
ответов
Работа с битвек в pySmt
Я изучаю битвек с pysmt. Но я встречаю некоторую проблему. У меня есть три битвека, размер которых равен 1, называемых a,b,c. И я хочу закодировать (a<b)&c a = Symbol("a",BVType(1)) b = Symbol("b",BVType(1)) c = Symbol("c",BVType(1)) f = BVAn…
22 мар '22 в 05:20
0
ответов
Я не могу найти «сокращение или» в pySmt
Работа с битвеком находится в pysmt.shortcuts. Но я не могу найти операцию "сокращение или". import pysmt.shortcuts
22 мар '22 в 13:20
0
ответов
Представление формулы SMT
Создать логическую формулу в PySMT очень просто: from pysmt.shortcuts import * from pysmt.typing import INT x1 = Symbol("x1") x2 = Symbol("x2") formula = Or(x1, x2) model = get_model(formula) print(model) Более того, формула SMT имеет такой вид: x1 …
15 дек '22 в 11:05
2
ответа
pysmt: как равномерно и случайным образом извлечь модели?
В настоящее время я работаю над проектом, в котором мне нужно попробовать решения заданной формулы. Для этого я использую библиотеку pysmt , опираясь на решатель z3. В настоящее время я делаю, учитывая формулу (какpysmt.fnode.FNode), я используюget_…
11 окт '23 в 15:02
1
ответ
Z3 для pysmt не работает в MacOS с ошибкой «libz3.dylib не найден»
Я пытался использовать z3 в pysmt и установил z3 как через доморощенный, так и черезpysmt-install --z3команда. Однако, когда я пытаюсь проверить статус решателей черезpysmt-install --check, он возвращает следующее сообщение Could not find libz3.dyli…
14 ноя '23 в 06:35
0
ответов
Ошибка ImportError для pysmt-install --msat с pySMT на Python 3.11
У меня Python 3.11 в Windows 11 и установлен pySMT 0.9.5. Однако я не могу установить решатель SMT, например MathSAT. Раньше я делал это на каком-то более старом Python, и это работало хорошо, так что в принципе, похоже, это работает. Когда я бегуpy…
03 окт '23 в 12:21