Nano Hash - криптовалюты, майнинг, программирование

извлечение десятичного значения из символа в строке Z3

Пусть s1 — произвольная строка из Z3Str. Я могу проверить, является ли третий символ строчной буквой:

(declare-const s1 String)
(assert (= s1 "74b\x00!!###$$"))
(assert (str.in.re (str.at s1 2) (re.range "a" "z")))
(check-sat)
(get-value (s1))

Теперь предположим, что это действительно так, и я хочу заменить эту третью букву заглавной (новая строка s2 будет содержать замененную версию). Вдохновленный стандартными языками программирования, у меня может возникнуть соблазн сделать что-то вроде этого:

(declare-const s1 String)
(declare-const s2 String)
(declare-const b1 Bool)
(assert (= s1 "74b\x00!!###$$"))
(assert (= b1 (str.in.re (str.at s1 2) (re.range "a" "z"))))
(assert (= (str.substr s2 0 2) (str.substr s1 0 2)))
(assert (= (str.substr s2 3 8) (str.substr s1 3 8)))
(assert (= (str.len s2) (str.len s1)))
(assert (= (str.at s2 2) (ite b1 (- (str.at s1 2) 32) (str.at s1 2))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 32 = 'a'-'A'
(check-sat)
(get-value (s1 s2 b1))

Но, конечно, это не работает из-за типов:

(error "line 9 column 52: Sort mismatch at argument #1 for function 
(declare-fun - (Int Int) Int) supplied sort is String")

Существует ли прямой способ манипулирования десятичным значением символа в строке Z3? Я имею в виду, кроме гигантского переключателя для всех строчных букв ... Кажется, есть некоторая надежда, потому что API поддерживает «\ x61» в качестве альтернативного представления «a». Любая помощь очень ценится, спасибо!!

string z3 smt
02.10.2017

Ответы:


1

Следующие работы:

(declare-const s1 String)
(declare-const s2 String)
(declare-const b1 Bool)
(assert (= s1 "74b\x00!!###$$"))
(assert (= b1 (str.in.re (str.at s1 2) (re.range "a" "z"))))
(assert (= (str.substr s2 0 2) (str.substr s1 0 2)))
(assert (= (str.substr s2 3 8) (str.substr s1 3 8)))
(assert (= (str.len s2) (str.len s1)))

(declare-const subSecElt (_ BitVec 8))
(declare-const eltUpCase (_ BitVec 8))
(assert (= (bvsub subSecElt #x20) eltUpCase))
(assert (= (seq.unit subSecElt) (str.at s1 2)))
(assert (= (str.at s2 2) (ite b1 (seq.unit eltUpCase) (str.at s1 2))))

(check-sat)
(get-value (s1 s2 b1))

Было бы действительно неплохо, если бы это можно было еще больше упростить, хотя я не вижу простого способа сделать это, поскольку API, похоже, не позволяет получить доступ к элементам непосредственно из последовательности. Он позволяет вам получать подпоследовательности, но не элементы, что вам действительно нужно здесь: обратите внимание, что подпоследовательность длины 1 отличается от базового элемента в этой позиции, что объясняет правильную ошибку типа, которую вы получили.

Вот ответ, который я получаю на этот запрос:

sat
((s1 "74b\x00!!###$$")
 (s2 "74B\x00!!###$$")
 (b1 true))
02.10.2017
  • Используя Z3 4.5.1, я получил неправильное значение для s2 (нижний регистр g): ((s1...) (s2 74g\x00!!###$$) (b1...)) 03.10.2017
  • Я обновил ответ полученным ответом, который кажется правильным. Строковый решатель претерпел множество изменений, поэтому вы можете получить более свежую копию Z3 отсюда: github.com/Z3Prover/bin/tree/master/nightly 03.10.2017
  • Все еще не идет даже с ночной сборкой. Я добавил наблюдение за вспомогательными переменными subSecElt и eltUpCase, и они действительно имеют ожидаемые значения... Однако я продолжаю получать неправильное значение для s2 (нижний регистр o): sat ((s1 ...) (s2 74o\x00!!###$$) (b1 ...) (subSecElt #x62) (eltUpCase #x42)) 08.10.2017
  • Я только что сделал новую сборку Z3, и она отлично работает для меня. Я не думаю, что это имеет значение, но я на Mac. Какую ОС вы используете? 08.10.2017
  • Я использую UBUNTU 14.04.5 ... Вот командная строка, которую я запускаю из z3/build: ./z3 smt.string_solver=z3str3 -smt2 example.txt 09.10.2017
  • Командная строка, которую я запускал из z3/build, была неправильной: ./z3 smt.string_solver=z3str3 -smt2 example.txt ... Я изменил ее на: ./z3 -smt2 example.txt и теперь все работает! 09.10.2017
  • Похоже, это ошибка решателя z3str. Вы должны сообщить об этом в системе отслеживания ошибок z3, чтобы они могли устранить ее при необходимости: github.com/Z3Prover/z3. /вопросы 09.10.2017
  • О проблеме было сообщено на GitHub/Z3Prover/z3/issues. 31.10.2017
    • Новые материалы
    Кластеризация: более глубокий взгляд
    Кластеризация — это метод обучения без учителя, в котором мы пытаемся найти группы в наборе данных на основе некоторых известных или неизвестных свойств, которые могут существовать. Независимо от..
    Как написать эффективное резюме
    Предложения по дизайну и макету, чтобы представить себя профессионально Вам не позвонили на собеседование после того, как вы несколько раз подали заявку на работу своей мечты? У вас может..
    Частный метод Python: улучшение инкапсуляции и безопасности
    Введение Python — универсальный и мощный язык программирования, известный своей простотой и удобством использования. Одной из ключевых особенностей, отличающих Python от других языков, является..
    Как я автоматизирую тестирование с помощью Jest
    Шутка для победы, когда дело касается автоматизации тестирования Одной очень важной частью разработки программного обеспечения является автоматизация тестирования, поскольку она создает..
    Работа с векторными символическими архитектурами, часть 4 (искусственный интеллект)
    Hyperseed: неконтролируемое обучение с векторными символическими архитектурами (arXiv) Автор: Евгений Осипов , Сачин Кахавала , Диланта Хапутантри , Тимал Кемпития , Дасвин Де Сильва ,..
    Понимание расстояния Вассерштейна: мощная метрика в машинном обучении
    В обширной области машинного обучения часто возникает необходимость сравнивать и измерять различия между распределениями вероятностей. Традиционные метрики расстояния, такие как евклидово..
    Обеспечение масштабируемости LLM: облачный анализ с помощью AWS Fargate и Copilot
    В динамичной области искусственного интеллекта все большее распространение получают модели больших языков (LLM). Они жизненно важны для различных приложений, таких как интеллектуальные..