microsoft
/
ivy
зеркало из https://github.com/microsoft/ivy.git
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность

trying to get sht to work again

This commit is contained in:
Ken McMillan 2017-11-30 18:33:53 -08:00
Родитель 37d3f3a577
Коммит 572cfe59a9
4 изменённых файлов: 101 добавлений и 42 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

57
doc/examples/sht/shard.ivy
Просмотреть файл

@ -24,11 +24,62 @@ module table_shard(key,data) = {
pairs : arr.t
}
function key_at(S,I) = p_key(arr.value(pairs(S),I))
function value_at(S,I) = p_value(arr.value(pairs(S),I))
function at(S,X,I) = (0 <= I & I < arr.end(pairs(S)) & key_at(S,I) = X & value_at(S,I) ~= 0)
relation key_at(A:arr.t, X:key.t,I:index.t)
relation at(S:t,X:key.t,I:index.t) = key_at(pairs(S),X,I)
function value_at(S:t,I:index.t) : data
action empty returns (s:t)
action get_key(s:t, i:index.t) returns (k:key.t)
action get_value(s:t, i:index.t) returns (d:data)
action append_pair(s:t, k:key.t, d:data) returns (s:t)
object spec = {
after empty {
assert s.pairs.end = 0 & ~at(s,X,I)
}
before get_key {
assert 0 <= i & i < s.pairs.end
}
after get_key {
assert at(s,k,i)
}
before get_value {
assert 0 <= i & i < s.pairs.end
}
after get_value {
assert value_at(s,i) = d
}
after append_pair {
assert at(s,X,I) <-> at(old s,X,I) | I = pairs(old s).end & X = k;
assert at(old s,X,I) -> value_at(s,I) = value_at(old s,I);
assert value_at(s,pairs(old s).end) = d
}
}
object impl = {
definition value_at(S,I) = p_value(arr.value(pairs(S),I))
definition key_at(A,X,I) = (0 <= I & I < arr.end(A) & arr.value(A,I).p_key = X)
implement empty {
s.pairs := arr.empty
}
implement get_key {
k := pairs(s).get(i).p_key
}
implement get_value {
d := pairs(s).get(i).p_value
}
implement append_pair {
var p : pair;
p.p_key := k;
p.p_value := d;
s.pairs := s.pairs.append(p)
}
}
function value(S:t,X:key.t) = some Y. at(S,X,Y) in value_at(S,Y) else 0
function valid(s:t) = forall X,Y,Z. at(s,X,Y) & at(s,X,Z) -> Y = Z
isolate iso = this with key
}

61
doc/examples/sht/table.ivy
Просмотреть файл

@ -66,19 +66,19 @@ module hash_table(key,value,shard) = {
}
implement extract_ {
shard.pairs(res) := shard.arr.empty;
res := shard.empty;
local idx : key.iter.t, pos : shard.index.t {
idx := tab.lub(lo);
while idx < hi
invariant lo <= idx
invariant shard.value(res,X) = hash(X) if key.iter.between(lo,X,idx) else 0
invariant lo <= idx & (idx < hi -> tab.contains(idx.val))
invariant key.iter.between(lo,X,idx) & tab.contains(X) ->
exists I. (shard.at(res,X,I) & tab.maps(X,shard.value_at(res,I)))
invariant shard.at(res,X,I) -> key.iter.between(lo,X,idx) & tab.contains(X)
invariant shard.valid(res)
{
local pair : shard.pair, k:key.t {
k := key.iter.val(idx);
shard.p_key(pair) := k;
shard.p_value(pair) := tab.get(k,0);
shard.pairs(res) := shard.arr.append(shard.pairs(res),pair);
res := res.append_pair(k,tab.get(k,0));
idx := tab.next(idx)
}
};
@ -88,32 +88,26 @@ module hash_table(key,value,shard) = {
}
implement incorporate(s:shard.t) {
local lo:key.iter.t, hi:key.iter.t, pairs:shard.arr.t {
lo := shard.lo(s);
hi := shard.hi(s);
pairs := shard.pairs(s);
call tab.erase(lo,hi);
local idx : key.iter.t, pos : shard.index.t {
pos := 0;
while pos < shard.arr.end(pairs)
invariant 0 <= pos & pos <= shard.arr.end(pairs)
invariant key.iter.between(lo,X,hi) & shard.value(s,X) = 0 -> ~tab.contains(X)
invariant key.iter.between(lo,X,hi) & Y < pos & shard.at(s,X,Y) & shard.value(s,X) ~= 0
-> tab.contains(X) & tab.maps(X,shard.value(s,X))
invariant ~key.iter.between(lo,X,hi) -> spec.tab_invar(X,Y)
# following are object invariants of tab and shouldn't be needed here
invariant tab.maps(X,Y) & tab.maps(X,Z) -> Y = Z & tab.contains(X)
{
local pair:shard.pair {
pair := shard.arr.get(pairs,pos);
if key.iter.between(lo,shard.p_key(pair),hi) & shard.p_value(pair) ~= 0{
call tab.set(shard.p_key(pair),shard.p_value(pair))
}
};
pos := shard.index.next(pos)
}
}
}
var lo := shard.lo(s);
var hi := shard.hi(s);
call tab.erase(lo,hi);
var pos:shard.index.t := 0;
while pos < s.pairs.end
invariant 0 <= pos & pos <= s.pairs.end
invariant key.iter.between(lo,X,hi) & shard.value(s,X) = 0 -> ~tab.contains(X)
invariant key.iter.between(lo,X,hi) & Y < pos & shard.at(s,X,Y) & shard.value(s,X) ~= 0
-> tab.contains(X) & tab.maps(X,shard.value(s,X))
invariant ~key.iter.between(lo,X,hi) -> spec.tab_invar(X,Y)
# following are object invariants of tab and shouldn't be needed here
invariant tab.maps(X,Y) & tab.maps(X,Z) -> Y = Z & tab.contains(X)
{
var k := s.get_key(pos);
var d := s.get_value(pos);
if key.iter.between(lo,k,hi) & d ~= 0{
call tab.set(k,d)
};
pos := pos.next
}
}
object spec = {
@ -123,7 +117,8 @@ module hash_table(key,value,shard) = {
& (tab.contains(X) -> tab.maps(X,hash(X)))
}
conjecture shard.value(S,X)=Z -> spec.tab_invar(X,Y)
# conjecture shard.value(S,X)=Z -> spec.tab_invar(X,Y)
conjecture spec.tab_invar(X,Y)
}

6
doc/examples/sht/table_test.ivy
Просмотреть файл

@ -14,10 +14,10 @@ object impl = {
interpret key.t -> bv[4]
}
export tab.set
export tab.get
#export tab.set
#export tab.get
export tab.extract_
export tab.incorporate
#export tab.incorporate
isolate iso_tab = tab with tab,shard,key
isolate iso_key = key

19
ivy/ivy_theory.py
Просмотреть файл

@ -96,6 +96,16 @@ def get_qa_arcs(fmla,ast,pol,univs,strat_map):
for arg in fmla.args:
for a in get_qa_arcs(arg,ast,pol,univs,strat_map):
yield a
if isinstance(fmla,il.Ite):
for a in get_qa_arcs(fmla.args[0],ast,not pol,univs,strat_map):
yield a
if isinstance(fmla,il.Iff) or (il.is_eq(fmla) and il.is_boolean(fmla.args[0])):
for a in get_qa_arcs(fmla.args[0],ast,not pol,univs,strat_map):
yield a
for a in get_qa_arcs(fmla.args[1],ast,not pol,univs,strat_map):
yield a
def get_sort_arcs(assumes,asserts,strat_map):
# for sym in il.all_symbols():
@ -107,7 +117,7 @@ def get_sort_arcs(assumes,asserts,strat_map):
# if il.is_uninterpreted_sort(ds):
# yield (ds,rng,sym)
# show_strat_map(strat_map)
show_strat_map(strat_map)
for func,node in list(strat_map.iteritems()):
if isinstance(func,tuple) and not il.is_interpreted_symbol(func[0]):
yield (find(node),find(strat_map[func[0]]),func[0])
@ -151,7 +161,7 @@ def map_fmla(fmla,strat_map):
return nodes[1]
if il.is_app(fmla):
func = fmla.rep
if func in symbols_over_universals:
if func in symbols_over_universals or True:
for idx,node in enumerate(nodes):
if node is not None:
unify(strat_map[(func,idx)],node)
@ -167,7 +177,7 @@ def create_strat_map(assumes,asserts,macros):
# for f in all_fmlas:
# print f
symbols_over_universals = il.symbols_over_universals(all_fmlas)
# iu.dbg('[str(x) for x in symbols_over_universals]')
iu.dbg('[str(x) for x in symbols_over_universals]')
universally_quantified_variables = il.universal_variables(all_fmlas)
strat_map = defaultdict(UFNode)
@ -190,6 +200,9 @@ def get_unstratified_funs(assumes,asserts,macros):
macros = map(vupair,macros)
strat_map = create_strat_map(assumes,asserts,macros)
for f,g in macros:
print 'macro: {}'.format(f)
arcs = list(get_sort_arcs(assumes+macros,asserts,strat_map))