1
Могу ли я создать новый решатель из старого в Z3? В Z3 стандартный процесс создания решателя выглядит следующим образом:Могу ли я создать новый решатель из старого в Z3?
ctx; решатель sv (ctx);
После процесса вставки утверждений и проверки, я хочу создать новый решатель, скажем sv2, что эквивалентно sv. Но я не могу найти вспомогательную функцию или API. Решение дорого, поэтому я не хочу создавать sv2 с нуля.
Ting Chen
Что именно вы подразумеваете под «эквивалентом»? Вы можете создать столько решателей, сколько захотите, но они не будут содержать утверждений первого. Вы можете, конечно, скопировать их на новый решатель, но я не вижу, как это может сделать что-нибудь дешевле. –
Да, как вы говорите, скопируйте все утверждения от старого решателя на новый, не сделайте ничего дешевле. Я верю в это, я должен решить утверждения, которые я уже решил в старом решателе. Так есть дешевый способ. Я имею в виду создание нового решателя из старого, сохраняя при этом статус, чтобы поэтапно решать проблему. –