Я бы хотел использовать Z3 для моделирования статистики персонажей в игре. Для простоты мы сосредоточимся на одном стате: класс брони (A C).
В этой игре персонажи могут носить различные типы брони, каждый из которых имеет свой базовый класс брони. Кроме того, есть много других бонусов, которые можно добавить к броне. Для простоты давайте рассмотрим следующие
Armor Type | Base armor class
-----------|-----------------
Chain Mail | 16
Plate Mail | 18
Shield Type | Armor Bonus
------------------------
Kite Shield | +2
Magic Shield | +4
Defense Training | Bonus
-------------------------
Without | +0
With | +1
Персонажи могут получать выгоду только от одного бонуса каждого вида, например, персонаж может иметь только один экипированный щит за раз.
Персонаж должен иметь щит, чтобы экипировать его, поэтому набор щитов, которые они могут экипировать, может динамически меняться.
Кроме того, персонаж может приобрести защитную подготовку в какой-то момент во время игры (например, при повышении уровня), поэтому набор типов бонусов также может динамически меняться.
Игроки обычно хотят получить наибольшее A C, которое они могут получить за своих персонажей, поэтому персонажи A C являются лучшей базой A C, которую они могут получить плюс лучший бонус в каждой категории для всех категорий, к которым они имеют доступ.
На языке программирования императив / OO я мог бы смоделировать систему следующим образом
class Character():
base_armor_bonuses = [16, 18]
shield_armor_bonuses = [2, 4]
armor_class_bonuses: List[List[Int]] = [base_armor_bonuses, shield_armor_bonuses]
def armor_class(armor_class_bonus_options):
sum([max(bonus_kind) for bonus_kind in armor_class bonuses])
def add_bonus_kind(new_bonus_options):
armor_class_bonuses.append(new_bonus_options)
def add_new_armor_type(new_armor_bonus):
base_armor_bonuses.append(new_armor_bonus)
Императивный подход прекрасно работает для кодирования этих простых правила, однако я заинтересован в быстрой итерации изменений правил и новых эффектов, поэтому я надеюсь, что Z3 включит или гибкий способ кодирования этих правил.
Кроме того, я хотел бы использовать Z3, чтобы немного изучить пространство разработки, например, найти сборку персонажа, которая максимизирует класс брони, что трудно сделать с императивным подходом. .
Редактировать:
Я хотел бы иметь возможность использовать систему в режиме реального времени для ответа на запросы типа "что это за классы нынешних символов?". Затем в ответ на события, которые происходят в игре, например, когда персонаж получает новый щит, идет за стеной или снимает броню, обновите состояние мира, чтобы класс его брони обновился в следующий раз, когда я произвожу запрос "что это за класс доспехов персонажей?".
Я также хотел бы ответить, не обязательно в режиме реального времени. Какой персонаж из всех возможных персонажей имеет самый высокий класс брони. Это легко сделать в упрощенном примере, но перечисление всех возможных персонажей для поиска персонажа с наивысшим классом брони становится невозможным, когда вы вводите множество видов персонажей, каждый из которых имеет доступ к различным видам бонусов к классу брони из различных возможных вариантов. выберите из.
В качестве альтернативы я провел некоторое исследование по прологу, которое также могло бы отвечать на запросы, хотя я не уверен, какие могут быть различия в производительности. Я также рассмотрел типичную императивную программу, такую как фрагмент python, который я включил ниже. Это будет хорошо обрабатывать запросы в реальном времени. Однако это будет связано с поддержанием императивной программы, которая правильно поддерживает все различные параметры. Кроме того, было бы трудно или невозможно определить персонажа с максимальным классом брони или чего-либо еще из этой программы. Я надеюсь, что декларативный язык логики c, такой как z3, может преодолеть оба эти ограничения.
На данный момент это хобби-проект для моих друзей и меня, который я использую при игре в существующие игры (запросы в реальном времени ) и разработку новых игр (запросы не в реальном времени).
Edit 2
Для базовой версии c свободных переменных не существует, по сути, это просто расчет класса брони и других статистика для определенного c символа. Причина, по которой я хочу это сделать, заключается в том, что я не хочу поддерживать две отдельные системы с кодированными правилами игры, одну для игры и одну для проектирования.
Для более сложного примера свободными переменными являются: выбор, который вы делаете при создании персонажа. Вот простой пример.
У персонажей есть базовый класс Fighter, Archer или Wizard. Каждый раз, когда вы повышаете уровень, вы можете пройти уровень в любом из классов, получая способности самого низкого уровня класса, которого у вас еще нет. Например, Fighter 2 / Archer 1 будет иметь способности первого и второго уровня бойца и способности первого уровня лучника. Вот несколько примеров способностей
level | fighter ability
----------------------
1 | Proficiency with Chain mail and the Kite Shield
2 | Defense Training or Proficiency with plate (players choice, i.e. a free variable)
3 | Defense Training or Proficiency with plate (whichever one they didn't get before)
level | wizard ability
-----------------------
1 | proficiency with Magic Shields
2 | proficiency with chain
Итак, я хотел бы определить бонусы / опции, доступные каждому персонажу декларативным способом, а затем спросить Z3, какая сборка имеет самый высокий класс брони на уровне 3. Fighter 2 (для планшета) / Wizard 1 - лучшее, что я могу придумать для этого небольшого примера с общей броней 18 + 4 = 22.
Теперь, если, например, было 12 классов персонажей и каждый имел уровни от 1 до 20, как 5-е издание D & D. было бы 12 ^ 20 или примерно 2 ^ 71 возможных сборок персонажей уровня 20. Отвечая на вопрос, какой персонаж 20-го уровня имеет самый высокий класс брони, перечислив все варианты, вероятно, потребуется больше времени, чем я буду жив. Здесь я надеюсь, что Z3 сможет помочь.
Edit 3
Я не уверен, какую структуру / тип данных мне следует использовать для представления брони, доступной для определенного персонажа. Я думал об использовании массивов, но я не знаю, как сделать express утверждение типа «массив типа брони содержит табличку», когда я определяю опцию класса истребителя, а затем также express, что в массиве нет других неопределенных элементов .
Другими словами, я не знаю, как определить содержимое массива таким образом, чтобы оно зависело от назначения свободных переменных (выбор уровня класса символов), а потом сказать, что больше ничего нет в массиве.
Кроме того, я недостаточно знаком с Z3, чтобы даже знать, является ли это хорошим способом моделирования системы.