В настоящее время я имею дело с ситуацией, когда утверждения Z3 содержат большое количество неравенств и равенств. Они зависят друг от друга таким образом, что наиболее эффективно начать решение формулы с присвоения значений переменным, используемым в равенствах.
Есть ли способ изменить эвристику Z3 таким образом, чтобы решатель всегда предпочитал «начинать» с этих формул?
Мое предположение состояло бы в том, чтобы использовать тактику, которая изначально обрабатывает цель, содержащую упомянутые равенства. Затем он продолжит работу с другими утверждениями, при необходимости перезапустив весь процесс.
Однако я не знаю, как это реализовать. Как создать собственные цели на основе наборов формул?
