2
엄격한 제한 조건 (예 : max x s.t. x < 4)에 따라 실제 값을 최적화하면 Z3_optimize_get_upper을 호출 할 때 epsilon 값이 생성됩니다.Z3에서 최적화 : 엡실론 제거
위 예제에서 반환 값은 4 - epsilon입니다.
엡실론 제거 방법이 있습니까? 특정 값으로 인스턴스화 할 수 있습니까? 예 : 0 또는 1 또는 0.1으로 설정 하시겠습니까?
감사합니다.
편집 : opt_context.cpp의 코드에서
, 나는 epsilon라는 상수가 생성 된 것을 볼 : 사실
if (!eps.is_zero()) { expr* ep = m.mk_const(symbol("epsilon"), m_arith.mk_int());