Evet, aslında iki aşamalı mod vardır.
Yığın tabanlı: push(), pop() kullanarak yığın bir disiplini izleyen yerel bir bağlam yaratırsınız. Bir push() öğesinin altına eklenen onaylar, eşleşen bir pop() öğesinden sonra kaldırılır. Ayrıca, bir itme altında türetilen herhangi bir lemmas kaldırılır. Bir durumu dondurmayı taklit etmek ve donmuş duruma ek kısıtlamalar eklemek için push()/pop() öğesini kullanın ve ardından donmuş duruma geri dönün. Bir itme() kapsamı dahilinde oluşturulan herhangi bir ek bellek yükünün (örneğin öğrenilmiş lemmalar) serbest bırakılması avantajına sahiptir. Çalışma varsayımı, bir itme altında öğrenilen lemmaların artık yararlı olmayacağıdır.
Varsayım tabanlı: ek varsayımların kullanılması için, check()/check_sat() 'a geçildiğinde, (1) kabul edilemez çekirdekleri varsayımlar üzerine çıkarabilir, (2) varsayımlardan bağımsız olarak elde edilen lemmaları toplayan yerel artışlar elde edebilirsiniz. . Başka bir deyişle, eğer Z3, varsayımsal değişmezleri içermeyen bir lemma öğrenirse, bunları toplayıp çöp toplamayacağını umar. Varsayım değişmezlerini etkili bir şekilde kullanmak için bunları formüllerinize de eklemelisiniz. Dolayısıyla, varsayım, varsayımlarla kullanılan cümlelerin bir miktar bloğu içermesidir. Örneğin, yerel olarak bir formül (< = x y) varsa, bir yan tümce (=> p (< = x y)) ekleyin ve check_sat() öğesini çağırırken p değerini atarsınız. Orijinal varsayımın bir birim olduğunu unutmayın. Z3 üniteleri verimli bir şekilde yaymaktadır. Varsayım değişmezlerini kullanan formülasyon ile artık temel arama düzeyinde bir birim değildir. Bu ek bir ek yüke neden olur. Birimler ikili ifadeler haline gelir, ikili maddeler üçüncül bir deyim haline gelir, vb.
Z3'ün varsayılan SMT motoru için push/pop işlevi arasındaki fark aynıdır. Bu, çoğu formülün kullanacağı motordur. Z3 bazı motor portföyleri içerir. Örneğin, saf bit-vektör problemleri için Z3, sat tabanlı motoru kullanarak sonuçlanabilir. Sat tabanlı motordaki artış, varsayılan motordan farklı şekilde uygulanır. Burada artış, varsayımsal değişmezler kullanılarak uygulanır. Bir itme kapsamında eklediğiniz herhangi bir iddia, bir implikasyon olarak belirtilir (=> scope_literals formülü). Böyle bir kapsamdaki check_sat() varsayımsal değişmezlerle uğraşmak zorunda kalacaktır. Kapak tarafında, geçerli kapsama bağlı olmayan herhangi bir sonuç (lemma), pop() üzerinde toplanan çöp değil olur.
En iyileştirme modunda, optimizasyon hedeflerini belirlediğinizde veya API üzerinden optimizasyon nesnelerini kullandığınızda, itme/popu da çağırabilirsiniz. Aynı şekilde sabit noktaları ile. Bu iki özellik için, push/pop temel olarak kullanıcı kolaylığı içindir. İçsel bir artış yok. Bunun nedeni, bu iki modun, süper olmayan-artımsal olmayan büyük ön-işlemeleri kullanmasıdır.