Warum kann Z3 nicht beweisen/zugeben, dass `is_int` bei einigen Operationen geschlossen ist?

Question

Zum Beispiel der folgenden Abfrage mal aus:

(declare-const x Real) 
(declare-const y Real) 
(assert (is_int x)) 
(assert (is_int y)) 
(assert (not (is_int (+ x y)))) 
(check-sat) 

Soweit ich, die Z3 gelesen habe Real mathematische reelle Zahlen sind und nicht die Maschine diejenigen mit subtiler Semantik. Gibt es ein Problem bei der Annahme, dass einige Operationen is_int beibehalten?

Answer 1

Z3 reduziert dies auf die Lösung eines gemischt-ganzzahligen linearen Problems, das einer der schwächeren Bereiche ist. Es endet in diesem Fall mit endlosen Verzweigungen und Schnitten.