Я использую Z3Py для генерации относительно большого решателя, который содержит около 90000 ограничений. Как будто я инициализировал решатель s = solver(), а затем добавил множество ограничений, используя s.add(constraint). Предположим, я добавил 90000 ограничений, затем мне нужно выполнить проверку, используя s.check(). Но программа, кажется, застряла, я думаю, что действительно нужно много времени, чтобы решить эти ограничения (по крайней мере, более 1 дня).
Однако я также попытался преобразовать ограничения 90000 в файл SMT2 с помощью команды file.write(s.sexpr()). Затем я использую Z3 из командной строки, чтобы проверить сгенерированный файл smt2, используя z3 -smt2 file.smt2. В этом случае программа была решена с помощью (check-sat) в файле smt2 в течение часа.
У меня вопрос: есть ли разница между s.check() в Z3Py и (check-sat) в z3 -smt2 file.smt2?
Какая может быть возможная причина, которая вызывает эту огромную разницу во времени?