톤> = 1, t> = 2 => t> = 1

Z3을 사용하여, 어떻게 든톤> = 1, t> = 2 => t> = 1

t>=1

에

t>=2 or t>=1

정수 t를 여기서 간단히/병합 가능?

가능한 한 간단하게 t에 대한 제약 조건을 유지하기를 바랍니다.

출처

2012-07-16 william007

Z3은 전술 번호 ctx-solver-simplify을 사용하여 수행 할 수 있습니다. 이 전략은 상당히 비쌉니다. 전술 ctx-simplify은 동등성 만 "전파"합니다. http://rise4fun.com/Z3/F7Q

출처

2012-07-16 16:32:11

감사 : 여기

이 전술을 사용하는 스크립트에 대한 링크입니다! 내게 보입니다. (t> = 0이고 t <=1) or (t> = 0이고 t <=1) => (t> = 0이고 t <= 1) 하지만 왜 링크가 false일까요? http://rise4fun.com/Z3/aZFY – william007

죄송합니다. 버그입니다. 다음 릴리스에서 수정 해 드리겠습니다. –

감사합니다. 또한 저에게 (t> = 2이고 t <=2) => t == 2이지만 http://rise4fun.com/Z3에 링크되어 있습니다./NHlx는 이것을 간소화하지 않는 것입니까? – william007

톤> = 1, t> = 2 => t> = 1

답변

관련 문제