Ich habe ein Programm, das eine Reihe von Nebenbedingungen in nichtlinearer reeller Arithmetik erzeugt. Berücksichtigen Sie die folgenden zwei Einschränkungen:

(<(- (- (- (+ (* (- v0_x v3_x) (- v1_y v3_y) (+ (* (- v2_x v3_x)) (- v2_x v3_x)) (- 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))) (- 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)) )) (* (- 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))) (- 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)

Wenn ich sie auf Z3 setze, heißt es, dass sie erfüllbar sind, aber sobald ich die zweite Einschränkung auf (<... 0) anstelle von (> ... 0) ändere, die jetzt unerfüllbar sein sollte, wird z3 für immer ausgeführt. Ich wundere mich über die Einschränkungen von z3 für die Übergabe nichtlinearer reeller Arithmetik. Gibt es eine Chance, dass Z3 mit den oben genannten Einschränkungen umgehen kann (z. B. durch Ändern der Formulierung oder auf andere Weise)?