Próbuję zrozumieć, w jaki sposób indeksowane zmienne są indeksowanez3. Oto fragment wz3py i odpowiednie wyjście. (http://rise4fun.com/Z3Py/plVw1 )

x, y = Ints('x y')
f1 = ForAll(x, And(x == 0, Exists(y, x == y)))
f2 = ForAll(x, Exists(y, And(x == 0, x == y)))
print f1.body()
print f2.body()

Wydajność:

ν0 = 0 ∧ (∃y : ν1 = y)
y : ν1 = 0 ∧ ν1 = y

Wf1, dlaczego ta sama zmienna związanax ma inny indeks. (0 i1). Jeśli zmodyfikujęf1 i wydobądźExists, następniex ma ten sam indeks (0).

Powód Chcę zrozumieć mechanizm indeksowania:

Mam formułę FOL reprezentowaną w DSL w scali, którą chcę wysłaćz3. TerazScalaZ3 mamkBound api do tworzenia zmiennych zmiennych, które trwaindex isort jako argumenty. Nie jestem pewien, jaką wartość powinienem przekazaćindex argument. Chciałbym więc wiedzieć, co następuje:

Jeśli mam dwie formułyphi1 iphi2 z maksymalnymi indeksami zmiennych związanychn1 in2, jaki byłby indeksx wForAll(x, And(phi1, phi2))

Czy istnieje sposób na pokazanie wszystkich zmiennych w formie indeksowanej?f1.body() po prostu mnie pokazujex w formie indeksowanej, a niey. (Myślę, że powodem jest toy jest nadal związanyf1.body())