Sabit boyutlu bir dizi oluşturun ve onu

Question

başlatabilirsiniz Sabit boyutlu bir dizi oluşturacağım ve bazı değerlerle başlatacağım.

Örneğin, aşağıdaki C++ kod:

a[0] = 10; 
a[1] = 23; 
a[2] = 27; 
a[3] = 12; 
a[4] = 19; 
a[5] = 31; 
a[6] = 41; 
a[7] = 7; 

o model Z3 bazı araçları var mı?

Answer 1

Z3 dizi teorisini destekler, ancak genellikle sınırsız dizileri veya çok büyük dizileri kodlamak için kullanılır. Büyük, demek istediğim, formülünüzdeki dizi erişim sayısı (yani, seçimler) dizinin gerçek boyutundan çok daha küçüktür. Kendimize şunu sormalıyız: “X problemini modellemek/çözmek için dizilere gerçekten ihtiyacımız var mı?”. Örneğinizdeki gibi sabit boyutlu diziler için, her dizi konumu için farklı bir değişken kullanabiliriz. Örnek: a[0] için a0, a[1] için a1 vb Elbette, o zaman gibi a[i] büyük if-then-else terim gibi

(ite (= i 0) a0 (ite (= i 1) a1 ...))

olarak kodlanmış gereken bir dizi erişimi kodlayan, teorileri kullanmıyorsanız

Dizi boyutu biliniyor ve küçükse, bu genellikle bir sorunu kodlamak için en verimli yaklaşımdır. Öte yandan

, dizinin teorisini kullanmaya karar sanki senin soru başlatma kodlayabilir:

: Burada

(declare-const a (Array Int Int)) 
(assert (= (select a 0) 10)) 
... 
(assert (= (select a 7) 7)) 

SMT 2.0 biçiminde kodlanmış bütün örnektir http://rise4fun.com/Z3/iwo

Bu dizide bir güncelleştirmeyi kodlamak için not edin. Örneğin, C ifadesi a[3] = 5, bu ödevden sonra diziyi temsil eden yeni bir dizi değişkeni oluşturmamız gerekir. İşte

(declare-const a1 (Array Int Int)) 
(assert (= a1 (store a 3 5))) 

güncelleme ile tam örnektir: en kompakt yolu store ifadesini kullanır.

http://rise4fun.com/Z3/Kpln

Ayrıca Python/C++ /. Net API'ler düşünebilir. Sizinki gibi örnekleri daha kompakt bir şekilde kodlamamıza izin veriyorlar. Fikir, dizi başlatma gibi yaygın olarak kullanılan kalıpları kodlayan işlevleri uygulamaktır.

http://rise4fun.com/Z3Py/AAD