RatNum 표현식을 점 넷 십진수로 변환하고 싶습니다. RatNum에는 ToDecimalString 메서드가 있지만 ToDecimal 메서드는 없습니다. 이것에 대한 이유가 있습니까? RatNum을 Decimal.Parse (ratnum.ToDecimalString (2)) 이외의 소수로 변환하는 다른 방법이 있습니까? 감사.RatNum에 ToDecimal() 메서드가없는 이유는 무엇입니까?
이 질문에 대한 간단한 대답은 System.Decimal 형식이 (IEEE-754가 아닌) 부동 소수점 형식 인 반면 Z3의 RatNum은 rationals에 대한 무한 정밀도 형식이라는 것입니다. 이것은 유리수의 십진법 확장이 반드시 유한 한 것은 아니기 때문에 필요합니다 (예 : 1/3).
정밀도 p를 취하여 최대 p 자리수의 합리적인 10 진수 문자열 표현을 생성하는 ToStringDecimal을 사용할 수 있습니다. 이것은 Int64 나 Single/Double/Decimal보다 더 많은 자릿수가 될 수 있습니다.
또는 ToString을 사용하여 정확한 표현을 생성 할 수 있습니다. '1/3'.
다른 형식의 소수를 생성하는 데 사용할 수있는 합리적인 분자와 분모를 구하는 함수도 있습니다.
Z3은 무한 정밀도이며 솔루션을 근사해야하는 경우 Z3 외부에서 문자열과의 변환 방법이나 다른 변환을 통해 수행해야합니다. 예컨대
x.Numerator.Int/x.Denominator.Int
애플리케이션이 결과를 부동 소수점 근사 겪지 않으면 그 정수는 INT 타입의 최대 값을 초과하지 않을 것으로 알려지면.
누구에게 물어보고 있으며, 어떤 대답을 원하십니까? 문자열에'ToWhatShouldICallIt()'메서드가없는 이유를 묻는 것과 비슷합니다. 프레임 워크를 만든 프로그래머에게 물어보아야합니다. – Patrick
Patrick :이 질문은 Microsoft Research의 Z3 theorem 증명 도구에 대한 관리 API에 대한 것입니다. 질문은 올바르게 태그가 지정되었고 실제로 프레임 워크의 개발자에게 전달되었습니다. –