-
Notifications
You must be signed in to change notification settings - Fork 23
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
added benchmarks in both heap theory and array theory
- Loading branch information
1 parent
42b948d
commit 0598b26
Showing
223 changed files
with
24,513 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,91 @@ | ||
| (set-logic HORN) | ||
| (set-info :source | | ||
| Benchmark: C_VC | ||
| Output by Princess (http://www.philipp.ruemmer.org/princess.shtml) | ||
| |) | ||
| (set-info :status sat) | ||
| ;=============================================================================== | ||
| ; Encoding of Heap sorts and operations | ||
| ;------------------------------------------------------------------------------- | ||
| (define-sort Addr() Int) | ||
| (declare-datatypes ((HeapObject 0) (node 0)) | ||
| (((O_Int (getInt Int)) (O_Addr (getAddr Addr)) (O_node (getnode node)) (defObj)) | ||
| ((node (h Int) (n Addr))))) | ||
| (declare-datatypes ((AllocResHeap 0) (Heap 0)) | ||
| (((AllocResHeap (newHeap Heap) (newAddr Addr))) | ||
| ((HeapCtor (HeapSize Int) | ||
| (HeapContents (Array Addr HeapObject)))))) | ||
| (define-fun nullAddr () Addr 0) | ||
| (define-fun defHeapObject () HeapObject defObj) | ||
| (define-fun valid ((h Heap) (p Addr)) Bool | ||
| (and (>= (HeapSize h) p) (> p 0))) | ||
| (define-fun emptyHeap () Heap ( | ||
| HeapCtor 0 (( as const (Array Addr HeapObject)) defHeapObject))) | ||
| (define-fun read ((h Heap) (p Addr)) HeapObject | ||
| (ite (valid h p) | ||
| (select (HeapContents h) p) | ||
| defHeapObject)) | ||
| (define-fun write ((h Heap) (p Addr) (o HeapObject)) Heap | ||
| (ite (valid h p) | ||
| (HeapCtor (HeapSize h) (store (HeapContents h) p o)) | ||
| h)) | ||
| (define-fun alloc ((h Heap) (o HeapObject)) AllocResHeap | ||
| (AllocResHeap (HeapCtor (+ 1 (HeapSize h)) | ||
| (store (HeapContents h) (+ 1 (HeapSize h)) o)) | ||
| (+ 1 (HeapSize h)))) | ||
|
|
||
| ;=============================================================================== | ||
| (declare-fun inv_main12 (Heap Int Addr Addr Addr) Bool) | ||
| (declare-fun inv_main13 (Heap Int Addr Addr Addr) Bool) | ||
| (declare-fun inv_main17 (Heap Int Addr Addr Addr) Bool) | ||
| (declare-fun inv_main18 (Heap Int Addr Addr Addr) Bool) | ||
| (declare-fun inv_main23 (Heap Int Addr Addr Addr) Bool) | ||
| (declare-fun inv_main26 (Heap Int Addr Addr Addr Int) Bool) | ||
| (declare-fun inv_main29 (Heap Int Addr Addr Addr) Bool) | ||
| (declare-fun inv_main3 (Heap Int) Bool) | ||
| (declare-fun inv_main33 (Heap Int Addr Addr Addr) Bool) | ||
| (declare-fun inv_main37 (Heap Int Addr Addr Addr) Bool) | ||
| (declare-fun inv_main40 (Heap Int Addr Addr Addr) Bool) | ||
| (declare-fun inv_main44 (Heap Int Addr Addr Addr) Bool) | ||
| (declare-fun inv_main49 (Heap Int Addr Addr Addr) Bool) | ||
| (declare-fun inv_main53 (Heap Int Addr Addr Addr Addr) Bool) | ||
| (declare-fun inv_main57 (Heap Int Addr Addr Addr) Bool) | ||
| (declare-fun inv_main8 (Heap Int Addr Int) Bool) | ||
| (assert (forall ((var0 Heap)) (or (not (= var0 emptyHeap)) (inv_main3 var0 1)))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Addr) (var4 Addr) (var5 Addr) (var6 Heap) (var7 Heap) (var8 Addr) (var9 node) (var10 Addr) (var11 Int) (var12 Addr) (var13 Int) (var14 Addr) (var15 Heap) (var16 Addr)) (or (not (and (inv_main17 var15 var11 var8 var14 var16) (and (and (not (= var0 nullAddr)) (and (and (and (and (and (= var7 (newHeap (alloc var6 (O_node var9)))) (= var13 0)) (= var10 var3)) (= var4 var2)) (= var5 var12)) (= var0 (newAddr (alloc var6 (O_node var9)))))) (and (and (and (and (= var6 (write var15 var16 (O_node (node 1 (n (getnode (read var15 var16))))))) (= var1 var11)) (= var3 var8)) (= var2 var14)) (= var12 var16))))) (inv_main23 var7 var13 var10 var0 var5)))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 node) (var4 Addr) (var5 Addr) (var6 Int) (var7 Addr) (var8 Heap) (var9 Int) (var10 Addr) (var11 Heap) (var12 Heap) (var13 Addr) (var14 Addr) (var15 Addr) (var16 Addr)) (or (not (and (inv_main18 var11 var9 var7 var10 var14) (and (and (not (= var15 nullAddr)) (and (and (and (and (and (= var12 (newHeap (alloc var8 (O_node var3)))) (= var1 1)) (= var0 var2)) (= var4 var16)) (= var5 var13)) (= var15 (newAddr (alloc var8 (O_node var3)))))) (and (and (and (and (= var8 (write var11 var14 (O_node (node 2 (n (getnode (read var11 var14))))))) (= var6 var9)) (= var2 var7)) (= var16 var10)) (= var13 var14))))) (inv_main23 var12 var1 var0 var15 var5)))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Heap) (var3 Int)) (or (not (inv_main8 var2 var1 var0 var3)) (inv_main8 var2 var1 var0 var3)))) | ||
| (assert (forall ((var0 Addr) (var1 node) (var2 Heap) (var3 Int) (var4 Heap) (var5 Int)) (or (not (and (inv_main3 var4 var3) (and (= var0 nullAddr) (and (and (= var2 (newHeap (alloc var4 (O_node var1)))) (= var5 var3)) (= var0 (newAddr (alloc var4 (O_node var1)))))))) (inv_main8 var2 var5 var0 1)))) | ||
| (assert (forall ((var0 Addr) (var1 Addr) (var2 Addr) (var3 Int) (var4 Int) (var5 Int) (var6 Addr) (var7 Heap) (var8 Heap) (var9 Addr) (var10 Addr)) (or (not (and (inv_main49 var7 var3 var0 var6 var9) (and (not (= var5 3)) (and (and (and (and (and (= var8 var7) (= var4 var3)) (= var2 var0)) (= var1 var6)) (= var10 var9)) (= var5 (h (getnode (read var7 var9)))))))) (inv_main53 var8 var4 var2 var1 var10 var10)))) | ||
| (assert (forall ((var0 Addr) (var1 Heap) (var2 Addr) (var3 Int) (var4 Int) (var5 Addr) (var6 Addr) (var7 Heap) (var8 Addr) (var9 Addr) (var10 Addr)) (or (not (and (inv_main29 var7 var4 var0 var6 var9) (and (and (and (and (and (= var1 var7) (= var3 var4)) (= var8 var0)) (= var10 var6)) (= var5 var9)) (= var2 (n (getnode (read var7 var9))))))) (inv_main12 var1 var3 var8 var10 var2)))) | ||
| (assert (forall ((var0 node) (var1 Addr) (var2 Int) (var3 Heap) (var4 Addr) (var5 Heap) (var6 Int)) (or (not (and (inv_main3 var5 var2) (and (not (= var1 nullAddr)) (and (and (= var3 (newHeap (alloc var5 (O_node var0)))) (= var6 var2)) (= var1 (newAddr (alloc var5 (O_node var0)))))))) (inv_main12 var3 var6 var1 var4 var1)))) | ||
| (assert (forall ((var0 Addr) (var1 Addr) (var2 Addr) (var3 Heap) (var4 Addr) (var5 Int) (var6 Addr) (var7 Heap) (var8 Addr) (var9 Addr) (var10 Int)) (or (not (and (inv_main37 var7 var5 var0 var6 var8) (and (and (and (and (and (= var3 var7) (= var10 var5)) (= var1 var0)) (= var9 var6)) (= var4 var8)) (= var2 (n (getnode (read var7 var8))))))) (inv_main33 var3 var10 var1 var9 var2)))) | ||
| (assert (forall ((var0 Int) (var1 Addr) (var2 Addr) (var3 Addr) (var4 Int) (var5 Addr) (var6 Heap) (var7 Addr) (var8 Heap) (var9 Addr)) (or (not (and (inv_main13 var8 var4 var1 var7 var9) (and (and (and (and (= var6 (write var8 var9 (O_node (node 3 (n (getnode (read var8 var9))))))) (= var0 var4)) (= var3 var1)) (= var2 var7)) (= var5 var9)))) (inv_main33 var6 1 var3 var2 var3)))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Int) (var3 Int) (var4 Addr) (var5 Addr) (var6 Addr) (var7 Addr) (var8 Heap) (var9 Addr) (var10 Heap)) (or (not (and (inv_main33 var8 var3 var0 var7 var9) (and (not (= var1 0)) (and (not (= var2 3)) (and (and (and (and (and (= var10 var8) (= var1 var3)) (= var6 var0)) (= var5 var7)) (= var4 var9)) (= var2 (h (getnode (read var8 var9))))))))) (inv_main40 var10 0 var6 var5 var4)))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Int) (var5 Addr)) (or (not (inv_main26 var3 var1 var0 var2 var5 var4)) (inv_main26 var3 var1 var0 var2 var5 var4)))) | ||
| (assert (forall ((var0 node) (var1 Int) (var2 Int) (var3 Addr) (var4 Addr) (var5 Heap) (var6 Heap) (var7 Addr) (var8 Addr) (var9 Addr) (var10 Int) (var11 Addr) (var12 Addr) (var13 Addr) (var14 Heap) (var15 Addr) (var16 Addr)) (or (not (and (inv_main17 var14 var10 var8 var13 var15) (and (and (= var11 nullAddr) (and (and (and (and (and (= var6 (newHeap (alloc var5 (O_node var0)))) (= var1 0)) (= var9 var4)) (= var16 var3)) (= var7 var12)) (= var11 (newAddr (alloc var5 (O_node var0)))))) (and (and (and (and (= var5 (write var14 var15 (O_node (node 1 (n (getnode (read var14 var15))))))) (= var2 var10)) (= var4 var8)) (= var3 var13)) (= var12 var15))))) (inv_main26 var6 var1 var9 var11 var7 1)))) | ||
| (assert (forall ((var0 Int) (var1 Addr) (var2 Addr) (var3 Int) (var4 node) (var5 Addr) (var6 Addr) (var7 Heap) (var8 Int) (var9 Heap) (var10 Addr) (var11 Heap) (var12 Addr) (var13 Addr) (var14 Addr) (var15 Addr) (var16 Addr)) (or (not (and (inv_main18 var11 var8 var5 var10 var13) (and (and (= var15 nullAddr) (and (and (and (and (and (= var9 (newHeap (alloc var7 (O_node var4)))) (= var0 1)) (= var1 var2)) (= var14 var16)) (= var6 var12)) (= var15 (newAddr (alloc var7 (O_node var4)))))) (and (and (and (and (= var7 (write var11 var13 (O_node (node 2 (n (getnode (read var11 var13))))))) (= var3 var8)) (= var2 var5)) (= var16 var10)) (= var12 var13))))) (inv_main26 var9 var0 var1 var15 var6 1)))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Addr)) (or (not (inv_main23 var3 var1 var0 var2 var4)) (inv_main29 (write var3 var4 (O_node (node (h (getnode (read var3 var4))) var2))) var1 var0 var2 var4)))) | ||
| (assert (forall ((var0 Addr) (var1 Addr) (var2 Addr) (var3 Heap) (var4 Int) (var5 Int) (var6 Addr) (var7 Heap) (var8 Addr) (var9 Int) (var10 Addr)) (or (not (and (inv_main40 var7 var4 var0 var6 var8) (and (= var9 1) (and (and (and (and (and (= var3 var7) (= var5 var4)) (= var10 var0)) (= var2 var6)) (= var1 var8)) (= var9 (h (getnode (read var7 var8)))))))) (inv_main37 var3 var5 var10 var2 var1)))) | ||
| (assert (forall ((var0 Addr) (var1 Addr) (var2 Addr) (var3 Addr) (var4 Int) (var5 Addr) (var6 Heap) (var7 Int) (var8 Addr) (var9 Heap) (var10 Int)) (or (not (and (inv_main44 var6 var4 var0 var5 var8) (and (= var7 2) (and (and (and (and (and (= var9 var6) (= var10 var4)) (= var1 var0)) (= var2 var5)) (= var3 var8)) (= var7 (h (getnode (read var6 var8)))))))) (inv_main37 var9 var10 var1 var2 var3)))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Int) (var3 Int) (var4 Addr) (var5 Addr) (var6 Addr) (var7 Addr) (var8 Heap) (var9 Addr) (var10 Heap)) (or (not (and (inv_main33 var8 var3 var0 var7 var9) (and (= var1 0) (and (not (= var2 3)) (and (and (and (and (and (= var10 var8) (= var1 var3)) (= var6 var0)) (= var5 var7)) (= var4 var9)) (= var2 (h (getnode (read var8 var9))))))))) (inv_main44 var10 1 var6 var5 var4)))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Int) (var3 Addr) (var4 Heap) (var5 Addr)) (or (not (and (inv_main12 var4 var2 var0 var3 var5) (and (not (= var2 0)) (not (= var1 0))))) (inv_main17 var4 var2 var0 var3 var5)))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Int) (var5 Addr)) (or (not (and (inv_main12 var3 var1 var0 var2 var5) (= var4 0))) (inv_main13 var3 var1 var0 var2 var5)))) | ||
| (assert (forall ((var0 Addr) (var1 Heap) (var2 Addr) (var3 Addr) (var4 Int) (var5 Int) (var6 Addr) (var7 Addr) (var8 Addr) (var9 Heap) (var10 Addr) (var11 Addr) (var12 Addr)) (or (not (and (inv_main53 var9 var4 var0 var8 var11 var7) (and (and (and (and (and (and (= var1 var9) (= var5 var4)) (= var10 var0)) (= var2 var8)) (= var12 var11)) (= var6 var7)) (= var3 (n (getnode (read var9 var11))))))) (inv_main49 (write var1 var6 defObj) var5 var10 var2 var3)))) | ||
| (assert (forall ((var0 Addr) (var1 Heap) (var2 Int) (var3 Int) (var4 Int) (var5 Addr) (var6 Heap) (var7 Addr) (var8 Addr) (var9 Addr) (var10 Addr)) (or (not (and (inv_main33 var6 var3 var0 var5 var9) (and (= var4 3) (and (and (and (and (and (= var1 var6) (= var2 var3)) (= var8 var0)) (= var7 var5)) (= var10 var9)) (= var4 (h (getnode (read var6 var9)))))))) (inv_main49 var1 var2 var8 var7 var8)))) | ||
| (assert (forall ((var0 Addr) (var1 Addr) (var2 Int) (var3 Int) (var4 Addr) (var5 Heap) (var6 Int) (var7 Addr) (var8 Heap) (var9 Addr) (var10 Addr)) (or (not (and (inv_main40 var8 var6 var1 var7 var9) (and (not (= var3 1)) (and (and (and (and (and (= var5 var8) (= var2 var6)) (= var4 var1)) (= var10 var7)) (= var0 var9)) (= var3 (h (getnode (read var8 var9)))))))) (inv_main57 var5 var2 var4 var10 var0)))) | ||
| (assert (forall ((var0 Int) (var1 Addr) (var2 Int) (var3 Int) (var4 Heap) (var5 Addr) (var6 Heap) (var7 Addr) (var8 Addr) (var9 Addr) (var10 Addr)) (or (not (and (inv_main44 var6 var3 var1 var5 var8) (and (not (= var0 2)) (and (and (and (and (and (= var4 var6) (= var2 var3)) (= var10 var1)) (= var9 var5)) (= var7 var8)) (= var0 (h (getnode (read var6 var8)))))))) (inv_main57 var4 var2 var10 var9 var7)))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Int) (var3 Addr) (var4 Heap) (var5 Addr)) (or (not (and (inv_main12 var4 var2 var0 var3 var5) (and (= var2 0) (not (= var1 0))))) (inv_main18 var4 var2 var0 var3 var5)))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Addr)) (not (and (inv_main17 var3 var1 var0 var2 var4) (not (is-O_node (read var3 var4))))))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Addr)) (not (and (inv_main18 var3 var1 var0 var2 var4) (not (is-O_node (read var3 var4))))))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Addr)) (not (and (inv_main23 var3 var1 var0 var2 var4) (not (is-O_node (read var3 var4))))))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Addr)) (not (and (inv_main29 var3 var1 var0 var2 var4) (not (is-O_node (read var3 var4))))))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Addr)) (not (and (inv_main13 var3 var1 var0 var2 var4) (not (is-O_node (read var3 var4))))))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Addr)) (not (and (inv_main33 var3 var1 var0 var2 var4) (not (is-O_node (read var3 var4))))))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Addr)) (not (and (inv_main40 var3 var1 var0 var2 var4) (not (is-O_node (read var3 var4))))))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Addr)) (not (and (inv_main44 var3 var1 var0 var2 var4) (not (is-O_node (read var3 var4))))))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Addr)) (not (and (inv_main37 var3 var1 var0 var2 var4) (not (is-O_node (read var3 var4))))))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Addr)) (not (and (inv_main49 var3 var1 var0 var2 var4) (not (is-O_node (read var3 var4))))))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Addr) (var4 Heap) (var5 Addr)) (not (and (inv_main53 var4 var1 var0 var3 var5 var2) (not (is-O_node (read var4 var5))))))) | ||
| (assert (forall ((var0 Addr) (var1 Int) (var2 Addr) (var3 Heap) (var4 Addr)) (not (inv_main57 var3 var1 var0 var2 var4)))) | ||
| (check-sat) |
Oops, something went wrong.