Wie variabel verstecken mit Z3

t1<x and x<t2

ist es möglich, Variablen x, so dass t1<t2 in Z3 zu verbergen?

2012-07-24 william007

Sie können dafür die Quantifier-Eliminierung verwenden. Hier ein Beispiel:

(declare-const t1 Int) 
(declare-const t2 Int) 

(elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))

Sie dieses Beispiel ausprobieren können online unter: http://rise4fun.com/Z3/kp0X

2012-07-24 11:27:12

Danke, aber warum das Ergebnis ist T1-T2 < = -2? und nicht t1-t2 <0? – william007

Weil 't1',' t2' und 'x' ganze Zahlen sind. Für ganze Zahlen haben wir das, wenn 'a

Diese Antwort scheint veraltet zu sein, da sie als Ergebnis "nicht unterstützt" ergibt (auch auf rise4fun) – DCTLib

Mögliche Lösung mit Redlog von Reduce:

enter image description here

2013-07-28 20:31:05

Antwort