Полностью ли поддерживает Z3 квантификатор-исключение для NRA? Если нет, предположим, что я хотел использовать для этой цели реализацию САПР в Z3; Имеет ли она явную функцию для удаления переменной и доступна ли она API?