У меня есть программа, которая генерирует набор ограничений в нелинейной вещественной арифметике. Рассмотрим следующие два ограничения: (<

 (- (- (- (+ (* (- v0_x v3_x) (- v1_y v3_y) (+ (* (- v2_x v3_x) (- v2_x v3_x)) (* (- v2_y v3_y) (- v2_y v3_y)))) (* (- v0_y v3_y) (- v2_x v3_x) (+ (* (- v1_x v3_x) (- v1_x v3_x)) (* (- v1_y v3_y) (- v1_y v3_y)))) (* (- v1_x v3_x) ( - v2_y v3_y) (+ (* (- v0_x v3_x) (- v0_x v3_x)) (* (- v0_y v3_y) (- v0_y v3_y))))) (* (- - v1_y v3_y) (- v2_x v3_x) (+ ( * (- v0_x v3_x) (- v0_x v3_x)) (* (- v0_y v3_y) (- v0_y v3_y))))) (* (- v0_y v3_y) (- v1_x v3_x) (+ (* (- v2_x v3_x) ( - v2_x v3_x)) (* (- v2_y v3_y) (- v2_y v3_y))))) (* (- v0_x v3_x) (- v2_y v3_y) (+ (* (- - v1_x v3_x) (- v1_x v3_x)) (* (- v1_y v3_y) (- v1_y v3_y))))) 0) (>

 (- (- (- (+ (* (- v0_x v2_x) (- v1_y v2_y) (+ (* (- v3_x v2_x) (- v3_x v2_x)) (* (- v3_y v2_y) (- v3_y v2_y)))) (* (- v0_y v2_y) (- v3_x v2_x) (+ (* (- v1_x v2_x) (- v1_x v2_x)) (* (- v1_y v2_y) (- v1_y v2_y)))) (* (- v1_x v2_x) ( - v3_y v2_y) (+ (* (- v0_x v2_x) (- v0_x v2_x)) (* (- v0_y v2_y) (- v0_y v2_y))))) (* (- - v1_y v2_y) (- v3_x v2_x) (+ ( * (- v0_x v2_x) (- v0_x v2_x)) (* (- v0_y v2_y) (- v0_y v2_y))))) (* (- v0_y v2_y) (- v1_x v2_x) (+ (* (- v3_x v2_x) ( - v3_x v2_x)) (* (- v3_y v2_y) (- v3_y v2_y))))) (* (- v0_x v2_x) (- v3_y v2_y) (+ (* (- - v1_x v2_x) (- v1_x v2_x)) (* (- v1_y v2_y) (- v1_y v2_y))))) 0)

когда я утверждаю их в Z3, он говорит, что это выполнимо, но как только я изменяю второе ограничение на (< ... 0) вместо (> ... 0) что теперь должно быть неудовлетворительно, z3 работает вечно. Я задаюсь вопросом об ограничениях z3 для передачи нелинейной вещественной арифметики. Есть ли вероятность того, что Z3 сможет справиться с вышеуказанными ограничениями (например, путем изменения их формулировки или любым другим способом)?