add data type dataflow and minor fixes

Author: llalexandru00

.idea/codeStyles/Project.xml

@@ -1,40 +1,43 @@
-vertex_cover(e)
-@requires e : array< array<int> >
-@ensures \result : array<boolean>
-@ensures forall i : int :: 0 <= i && i < e.size() && !\result[i] ==> (forall j : int :: 0 <= j && j < e[i].size() ==> \result[e[i][j]])
+partition(out a, l, r)
+@requires a: array<int>
+@requires l: int
+@requires r: int
+@requires 0 <= l && l+2 <= r && r <= a.size()
+@ensures \result: int
+@ensures l <= \result && \result < r
 {
-    @havoc S : array<boolean>;
-    @assume S.size() == e.size();
-
-    for (i = 0; i < e.size(); i++)
-    @invariant 0 <= i && i <= e.size()
-    @modifies i, S
+    pv = a[l];
+    i = l;
+    j = r-1;
+    tmp = a[l];
+    a[l] = a[j];
+    a[j] = tmp;
+    print(a);
+    while (i < j)
+    @invariant l <= i && i <= j && j < r 
     {
-        choose b from {true, false};
-        S[i] = b;
-    }
-
-    @assert S.size() == e.size();
-
-    for (i = 0; i < e.size(); i++)
-    @invariant 0 <= i && i <= e.size()
-    @invariant forall k : int :: 0 <= k && k < i && !S[k] ==> (forall l : int :: 0 <= l && l < e[k].size() ==> S[e[k][l]])
-    @modifies i
-    {
-        if (!S[i])
-        {
-            for (j = 0; j < e[i].size(); j++)
-            @invariant 0 <= j && j <= e[i].size()
-            @invariant forall l : int :: 0 <= l && l < j ==> S[e[i][l]]
-            @modifies j
-            {
-                if (!S[e[i][j]])
-                {
-                    failure;
-                }
-            }
+        if (a[i] <= pv) {
+            i = i+1;
+        } 
+        else if (pv <= a[j-1]) {
+            j = j-1;
+        }
+        else {
+            tmp = a[i];
+            a[i] = a[j-1];
+            a[j-1] = tmp;
+            i = i+1;
+            j = j-1;
         }
-    }
+        print(a);
+    }  
+    tmp = a[i];
+    a[i] = a[r-1];
+    a[r-1] = tmp;
+    return i;
+}
 
-    return S;
-}
+/*
+a = [5,3,7,2,6,4];
+k = partition(a, 1, 6);
+*/

.idea/java-semantics.iml

@@ -1,27 +1,19 @@
-@havoc n : int;
-@havoc a : array<int>, b : array<int>, c : array<int>, cb : array<int>;
-@assume 1 <= n;
-
-@assume a.size() == n;
-@assume forall i : int :: 0 <= i && i < n ==> a[i] == 0;
-@assume b.size() == 2 * n;
-@assume forall i : int :: 0 <= i && i < 2 * n ==> b[i] == 0;
-@assume c.size() == 2 * n;
-@assume forall i : int :: 0 <= i && i < 2 * n ==> c[i] == 0;
-@assume cb.size() == 0;
-
-for (col = 0; col < n; col++)
-@invariant 0 <= col && col <= n
-@invariant cb.size() == col;
-@invariant forall i : int :: 0 <= i && i < n ==> a[i] <= 1
-@invariant forall i : int :: 0 <= i && i < 2 * n ==> b[i] <= 1
-@invariant forall i : int :: 0 <= i && i < 2 * n ==> c[i] <= 1
-@invariant forall i : int, j : int :: 0 <= i && i < j && j < col ==> cb[i] != cb[j]
-@modifies col, a, b, c, cb
+swap(out a, i, j)
+@requires a: array<int>
+@requires i: int
+@requires j: int
+@requires 0 <= i && i < a.size()
+@requires 0 <= j && j < a.size()
+@ensures a[i] == \old(a)[j]  
+@ensures a[j] == \old(a)[i]
 {
-    choose row from {0 .. n-1} s.t. a[row] == 0 && b[row + col] == 0 && c[n + (row-col)] == 0;
-    a[row]++;
-    b[row + col]++;
-    c[n + (row-col)]++;
-    cb[col] = row;
-}
+  temp = a[i];
+  a[i] = a[j];
+  a[j] = temp;
+}
+
+@havoc a : array<int>;
+@assume a.size() == 2;
+b = a;
+swap(a, 0, 1);
+@assert a[1] == b[0] && a[0] == b[1];

bin/alk.jar

@@ -1,28 +1,15 @@
-queens(n)
-@requires n : int
-@requires 1 <= n
-@ensures \result : array<int>
-@ensures \result.size() == n
-@ensures forall i : int :: 0 <= i && i < n ==> a[i] <= 1
+f(a)
 {
-    @havoc a : array<int>, b : array<int>, c : array<int>, cb : array<int>;
+    return f(a);
+}
 
-    @assume a.size() == n;
-    @assume forall i : int :: 0 <= i && i < n ==> a[i] == 0;
-    @assume cb.size() == 0;
-
-    for (col = 0; col < n; col++)
-    @invariant 0 <= col && col <= n
-    @invariant cb.size() == col;
-    @invariant forall i : int :: 0 <= i && i < n ==> a[i] <= 1
-    @modifies col, a, cb, cb.size
+g(a)
+{
+    if (a == 0)
     {
-        choose row from {0 .. n-1} s.t. a[row] == 0 && b[row + col] == 0 && c[n + (row-col)] == 0;
-        a[row]++;
-        b[row + col]++;
-        c[n + (row-col)]++;
-        cb[col] = row;
+        \result = 1;
+        return;
     }
-
-    return cb;
+    \result = f(a - 1);
+    return;
 }

bin/liblibz3.dylib

@@ -53,6 +53,7 @@ public <T> T accept(VisitorIface<T> visitor)
     @Override
     public DataTypeAST getDataType(DataTypeProvider dtp)
     {
-        throw new InternalException("Can't detect data type for id: " + getId());
+        return dtp.getDataType(text != null ? text : getAttribute(IdASTAttr.class).getId());
+//        throw new InternalException("Can't detect data type for id: " + getId());
     }
 }

bin/liblibz3java.dylib

@@ -23,11 +23,16 @@ public DataTypeAST(ParserRuleContext ctx)
     @Override
     public boolean equals(Object o)
     {
-        if (!(o instanceof DataTypeAST))
-            return false;
+        if (!(o instanceof DataTypeAST)) return false;
         return this.toString().equals(o.toString());
     }
 
+    @Override
+    public int hashCode()
+    {
+        return this.toString().hashCode();
+    }
+
     @Override
     public <T> T accept(VisitorIface<T> visitor)
     {