Hedefler oluşturabildiğimi, bunları bir taktik ekleyebileceğimi ve taktikten bir çözücü yaratabildiğimi görüyorum.z3 :: tactic ve z3 :: 'in amacı
Bu yaklaşımın basitçe bir z3 :: çözücü örneği oluşturup ifadelerimi eklemeye yönelik avantajı nedir?
Taktikleri farklı bir amacı vardır. İddialarınızı/kısıtlamalarınızı içeren bir hedef oluşturabilir ve daha sonra hedefiniz üzerinde bir taktik çalıştırabilirsiniz. Bunun sonucu, yeni bir dizi (alt) hedef, yani yeni iddialar/kısıtlamalar olacaktır. Çözücüler tatmin edilebilirliği belirler ve yeni (alt) hedefler üretmez.
Taktikler çözücüye dönüştürülebilir, sonuçta ortaya çıkan çözücü taktiği çalıştıracak ve sonuç kesin ise (önemsiz sat/unsat) bu sonucu döndürecektir. Taktik tarafından üretilen alt hedefler kesin değilse, "bilinmeyen" dönecektir.