1
Я пытаюсь улучшить производительность моего z3py-кода для создания вывода. Считаете ли вы, что изменение последовательности, которую логическое ограничение добавляет к решателю, возможно, поможет?z3py: Может ли переключатель заказов ограничений влиять на производительность решателя Z3 SMT?
Спасибо. Знаете ли вы о каких-либо хороших учебниках, объясняющих, какой решатель выбрать и как написать индивидуальную тактику? Я старался искать, но не смог. –
Из Z3Py вы можете распечатать набор доступных тактик. Тогда вы можете захотеть составить то в некотором роде (например, с помощью AndThen()). полезных функций в Z3Py: tactics() - возвращает список тактик; tactic_description (name); describe_tactics() - объединяет другие 2 функции –