Объявите внешние функции в z3py - PullRequest
Новая
       9

Объявите внешние функции в z3py

0 голосов
/ 06 июня 2018

Сценарий

В мире математической оптимизации возникает необходимость смоделировать ограничения g_k(...).g_k(...) иногда может быть вызовом функции внешней программы, которая, по сути, является черным ящиком.Простой поиск удовлетворительных ответов может быть полезен для определенного технического анализа.

Пример

Пример применения приведенного выше сценария для вещественных чисел, но также может быть целыми числами или логическими значениями:

мин f (х, у)
г 1 (х, у) <= 25 <br>г 2 (х, у)> = 7,7
x, y ε Real
x> = 0
x <= 50.0 <br>y> = 0
y <= 5.0 </p>

g 1 и g 2 - это функции Python, которые вызывают внешнюю программу.Функции возвращают действительное число.После этого формата Z3, чтобы найти модель, которая просто удовлетворяет ограничениям, будет представлен как: 

from z3 import *
from ExternalCodes import Code1, Code2 #For example, these could be Python wrappers to C++ codes

def g_1(x, y):
    return Code1(x, y) #isinstance(Code1(x,y), float) == True

def g_2(x, y):
    return Code2(x, y) #isinstance(Code2(x,y), float) == True

s = Solver()

x, y = Reals('x y')
s.add(g_1(x, y) <= 25.0)
s.add(g_2(x, y) >= 7.7)
s.add(x <= 0)
s.add(50.0 <= x)
s.add(y <= 0)
s.add(5.0 <= y)

m = s.model()
print(m)

Вопросы

  1. Я понимаю, что тип, возвращаемыйCode1 и Code2 должны быть типами данных Z3.Как преобразовать типы Python в типы Z3, как упомянуто в 1-м комментарии
  2. Как Z3 используется для поиска спутниковой модели, когда может потребоваться оценка ограничений во внешнем коде, т.е. объявлять функции?Я понимаю, что это может быть неэффективно, я бы потерял эвристику и т. Д., Потому что это неразрешимо, но для некоторых инженерных приложений перечисление спутникового решения, если оно существует, более выгодно, чем использование оптимизатора с самого начала.

Соответствующие ответы

1 Ответ

0 голосов
/ 06 июня 2018

Вы ищете неинтерпретированные функции.

Поиск термина "неинтерпретированные функции" в http://ericpony.github.io/z3py-tutorial/advanced-examples.htm

Ваш вопрос, кажется, делает некоторые предположения о том, как можно использовать решатели SMT;которые не совсем отражают текущее состояние дел.Хороший ресурс, чтобы прочитать об использовании решателей SMT: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-smt-application-chapter.pdf Было бы неплохо потратить время на то, чтобы ознакомиться с его применением на практике.

Некоторые общие замечания:

Z3py

Z3py - это , а не система рассуждений о программах на Python.Z3py - это коллекция библиотек, поэтому вы можете писать сценарии для Z3 гораздо более понятным и простым способом.Есть много таких привязок из многих языков: C / C ++ / Java / Haskell / Scala, вы называете это.Преимущество Z3py в том, что его легче изучать и использовать.Но вы не должны думать об этом как о системе, которая рассуждает о самом Python.Это всего лишь способ написания сценариев Z3 в упрощенной форме.

Логики решателя

Решатели SMT по существу работают над разрешимыми фрагментами (в основном без квантификаторов) многих сортированных логик различных теорий.Вы можете найти их подробно по адресу: http://smtlib.cs.uiowa.edu/logics.shtml

SMTLib

Большинство решателей принимают ввод в так называемом формате SMT-Lib, подробно здесь: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

Обратите внимание, что любое «связывание» на уровне C / Python / Java и т. Д. - просто удобство для программистов.Хотя многие решатели также предоставляют расширенные возможности, вам следует подумать о языке SMTLib.В вашем конкретном случае неинтерпретированные функции хорошо описаны в приведенном выше документе.

Типы

SMTLib понимает набор типов: целые числа, вещественные числа, бит-векторы (целые числа машин), числа с плавающей запятойи т. д. Он также допускает составные типы, такие как алгебраические типы данных, которые могут быть даже рекурсивными.(Хотя поддержка решателей различается.) Вам необходимо «сопоставить» типы внешних функций с этими типами: Надеюсь, что-то достаточно близко.Если нет, не стесняйтесь задавать конкретные вопросы о типах, которые вас интересуют.

«Импорт» функций

невозможно импортировать функции, написанные на других языках (Python/ C / C ++ и т. Д.) В SMTLib и рассуждать о них.Механизма для этого нет, и никогда не будет.Это не цель решения SMT.Если вы хотите рассуждать о программах, написанных на определенном языке, вам следует искать инструменты, специально предназначенные для работы на этих языках.(Например, Dafny для общих императивных программ, программы Klee / CBMC для C, программы LiquidHaskell для Haskell и т. Д.) Эти инструменты различаются по своим возможностям и тому, что они позволяют вам указывать и доказывать.Обратите внимание, что сами эти инструменты могут использовать SMT-решатели внизу для выполнения своих задач - и они часто делают это, а не наоборот.

Придерживаясь SMTLib

Если других инструментов нетдоступны (и, к сожалению, это, вероятно, имеет место для большинства языков, особенно устаревших), вы по сути застряли с тем, что обеспечивает язык SMTLib.В вашем случае, лучший способ моделирования таких «внешних» функций с использованием SMTLib - это использовать неинтерпретированные функции вместе с аксиомами.В общем, вам нужны аксиомы, чтобы ограничить поведение самих неинтерпретированных функций, моделировать ваши внешние функции.С другой стороны, если аксиомы определены количественно (как правило, они будут), решатель может вернуть unknown.

Сводка

Хотя решатели SMT являются отличными инструментами, вы должны всегдаимейте в виду, что язык, на котором они работают, это SMTLib, а не Python / C или что-то еще.Эти привязки являются просто средством доступа к решателю, поскольку вы можете включить его в более крупный проект.Я надеюсь, что это очищает ожидаемый вариант использования.

Задавать конкретные вопросы о том, что вы пытались и чего пытаетесь достичь (примеры кода), - это лучший способ получить выгоду от этого форума!

...