В версиях до 1.2 языка SMT-LIB была разрешена перегрузка определяемых пользователем символов. Начиная с версии 2.0 стандарта, перегрузка ограничена теоретическим символом.
Тем не менее, некоторые SMT-решатели по-прежнему допускают перегрузку пользовательских символов, и это оказывается удобным для моего варианта использования: обязательства по доказательствам легко генерируются автоматически с перегрузкой, не так уж и без... Я хотел бы добавить cvc4 в свой портфель. среди решателей SMT, но я обнаружил, что он выдает ошибку синтаксического анализа на перегруженных пользовательских символах.
Я знаю, что это правильный способ обеспечить соответствие стандарту SMT-LIB, но мне хотелось бы знать следующее: Есть ли в CVC4 параметр, отключающий такую проверку, и где синтаксический анализатор может устранить неоднозначность при перегрузке? пользовательские символы?
