В SAT-решателе можно найти быстрые, но неполные способы проверки неявности / неудовлетворенности. Например, применяя только единичное распространение без разделения, или ограничение на количество разделений или длину возврата. Это позволяет нам, например, при заданном наборе 'A' и некотором предложении единицы 'c' очень быстро проверить, подразумевает ли A * c, просто добавив последнее и выполнив распространение единицы.
Есть ли эквивалентный способ сделать «быструю проверку неполного следствия» в Z3? Допустим, например, что вызывается только теоретический решатель, но не SAT-расщепление + возвратный компонент? Если я прав, я верю, что могу достичь чего-то подобного, используя тактику. В текущей версии Z3 их 110, некоторые из которых не применимы к моей проблеме (на данный момент, скажем, у меня есть только функции равенства + неинтерпретируемые функции), а некоторые из них я не совсем уверен, что они делают, или если они соответствуют моему счету.
Есть ли подходящая функция для этой цели?
PS: Я также должен добавить, что инкрементальность по-прежнему необходима.