Каррированные функции и их применение в Z3 - PullRequest
Новая
       53

Каррированные функции и их применение в Z3

0 голосов
/ 14 июля 2020

Я работаю над языком, очень похожим на STL C, который я конвертирую в предложения Z3, отсюда несколько (под) вопросов о том, как Z3 обрабатывает (неинтерпретированные) функции:

  1. Функции естественным образом каррированы на моем языке, и, поскольку я рекурсивно конвертирую термины своего языка, я хотел бы также иметь возможность рекурсивно строить соответствующий Z3 AST. То есть, когда у меня есть термин f x y, я хотел бы сначала применить f к x, а затем применить его к y. Есть ли способ сделать это? API, который я нашел до сих пор (Z3_mk_func_decl / Z3_mk_app), похоже, требует от меня сначала собрать все аргументы и применить их все сразу.
  2. Есть ли разумный способ представить что-то вроде (if b then f else g) x?

В обоих случаях меня совершенно устраивает неинтерпретация функций и ограничение аргументации такими вещами, как «b = True /\ f x = 0 => (if b then f else g) x = 0 держит».

1 Ответ

1 голос
/ 14 июля 2020

SMTLib (как описано в http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf) - это многосортированный лог-файл первого порядка c. Все функции (неинтерпретируемые или нет) должны применяться ко всем его аргументам, и у вас не может быть никакой формы каррирования. Кроме того, вы не можете выполнять if-then-else более высокого порядка, т. Е. Ветви if-then-else должны быть значениями первого порядка. (Однако они могут быть массивами, и вы можете представить себе «подделку» функций с помощью массивов. Но это помимо сути.)

Следует отметить, что следующая итерация SMTLib (v3) будет основана на logi c более высокого порядка, после чего могут стать доступными такие функции, как вы просите. См .: http://smtlib.cs.uiowa.edu/version3.shtml. Конечно, это все еще предложение, и пройдет некоторое время, прежде чем оно будет определено и решатели начнут его добросовестно реализовывать. В конце концов, это произойдет, но я бы не ожидал этого в ближайшем будущем.

Кроме того: поскольку вы упомянули STL C (простое типизированное лямбда-исчисление), я полагаю, вы могли быть знакомы с такими функциональными языками, как Haskell. Если это так, вы можете изучить использование SBV: https://hackage.haskell.org/package/sbv. Он обеспечивает основу для выполнения некоторых из этих вещей, тщательно переводя их за кулисами. Вот пример: 

Prelude Data.SBV> sat $ \b -> (ite b (uninterpret "f") (uninterpret "g")) (0::SInteger) .== (0::SInteger)
Satisfiable. Model:
  s0 = True :: Bool

  f :: Integer -> Integer
  f _ = 0

  g :: Integer -> Integer
  g _ = 2

Здесь мы создали две функции и использовали конструкцию ite для их «слияния»; и получил решатель, чтобы вернуть нам модель. За кулисами SBV полностью заполнит эти приложения и позволит вам «притвориться», что вы программируете в более высоком смысле, как в STL C или Haskell. Конечно, дьявол кроется в деталях, и у этого подхода есть ограничения, но моделирование STL C в Haskell - это классическое c времяпрепровождение для многих людей, и выполнение его символически с использованием SBV может быть забавным упражнением *. 1018 *

...