Crash on example with "unknown symbol"
Closed this issue · 1 comments
marcoeilers commented
The following program crashes Silicon; Z3 complains that it does not now the symbol "result":
// fields of Node
field vari: Int // negative for leafs
field left: Ref
field right: Ref
field height: Int
field const: Bool
// field of BB
field map: Map[Ref, Ref]
function lookupKey(bdd: Ref, node: Ref): Ref
requires isBDD(bdd)
requires acc(isNode(node), wildcard)
ensures (result == null) == (unfolding isBDD(bdd) in (forall n: Ref :: n in domain(bdd.map) ==> !equal(n, node)))
ensures (result != null) == (unfolding isBDD(bdd) in result in domain(bdd.map) && equal(result, node))
predicate isNode(this: Ref) {
acc(this.vari) && acc(this.height) && 0 <= this.height &&
(0 <= this.vari ==>
acc(this.left) && isNode(this.left) && (unfolding isNode(this.left) in this.left.height < this.height) &&
acc(this.right) && isNode(this.right) && (unfolding isNode(this.right) in this.right.height < this.height)
) &&
(this.vari < 0 ==> acc(this.const))
}
predicate isBDD(this: Ref) {
acc(this.map) &&
(forall n: Ref :: n in domain(this.map) ==> acc(isNode(n), wildcard)) &&
(forall n: Ref :: n in range(this.map) ==> acc(isNode(n), wildcard))
}
function equal(n: Ref, m: Ref): Bool
requires acc(isNode(n), wildcard)
requires acc(isNode(m), wildcard)
{
unfolding acc(isNode(n), wildcard) in unfolding acc(isNode(m), wildcard) in
(n.vari < 0 && m.vari < 0 && n.const == m.const) ||
(0 <= n.vari && n.vari == m.vari && equal(n.left, m.left) && equal(n.right, m.right))
}
function isTrue(n: Ref): Bool
requires acc(isNode(n), wildcard)
{
unfolding acc(isNode(n), wildcard) in
n.vari < 0 && n.const
}
function isFalse(n: Ref): Bool
requires acc(isNode(n), wildcard)
{
unfolding acc(isNode(n), wildcard) in
n.vari < 0 && !n.const
}
method getNode(bdd: Ref, node: Ref) returns (res: Ref)
requires isBDD(bdd)
requires acc(isNode(node), wildcard)
ensures isBDD(bdd)
ensures acc(isNode(node), wildcard)
ensures acc(isNode(res), wildcard)
{
unfold acc(isNode(node), wildcard)
if(0 <= node.vari && node.left == node.right) {
unfold acc(isNode(node.left), wildcard)
res := node.left
fold acc(isNode(node.left), wildcard)
fold acc(isNode(res), wildcard)
} else {
var key: Ref
key := lookupKey(bdd, node)
unfold isBDD(bdd)
if(key == null) {
bdd.map := bdd.map[node := node]
res := node
} else {
res := bdd.map[key]
}
fold isBDD(bdd)
}
fold acc(isNode(node), wildcard)
}
method mkLeaf(bdd: Ref, val: Bool) returns (res: Ref)
requires isBDD(bdd)
ensures isBDD(bdd)
ensures acc(isNode(res), wildcard)
{
var n: Ref
n := new(vari, const)
n.vari := -1
n.const := val
fold isNode(n)
res := getNode(bdd, n)
}
method mkCompound(bdd: Ref, v: Int, l: Ref, r: Ref) returns (res: Ref)
requires isBDD(bdd)
requires 0 <= v
requires acc(isNode(l), wildcard)
requires acc(isNode(r), wildcard)
ensures isBDD(bdd)
ensures acc(isNode(res), wildcard)
{
var n: Ref
n := new(vari, left, right)
n.vari := v
n.left := l
n.right := r
fold acc(isNode(n), wildcard)
res := getNode(bdd, n)
}
method not(bdd: Ref, node: Ref) returns (res: Ref)
requires isBDD(bdd)
requires acc(isNode(node), wildcard)
ensures isBDD(bdd)
ensures acc(isNode(node), wildcard)
ensures acc(isNode(res), wildcard)
{
if(isTrue(node)) {
res := mkLeaf(bdd, false)
} else {
if(isFalse(node)) {
res := mkLeaf(bdd, true)
} else {
unfold acc(isNode(node), wildcard)
var l1: Ref
var r1: Ref
l1 := not(bdd,node.left)
r1 := not(bdd,node.right)
res := mkCompound(bdd, node.vari, l1, r1)
}
}
}
method and(bdd: Ref, node1: Ref, node2: Ref) returns (res: Ref)
requires isBDD(bdd)
requires acc(isNode(node1), wildcard)
requires acc(isNode(node2), wildcard)
ensures isBDD(bdd)
ensures acc(isNode(node1), wildcard)
ensures acc(isNode(node2), wildcard)
ensures acc(isNode(res), wildcard)
{
if(isTrue(node1)) {
res := node2
} else {
if(isTrue(node2)) {
res := node1
} else {
if(isFalse(node1) || isFalse(node2)) {
res := mkLeaf(bdd, false)
} else {
var l1: Ref
var r1: Ref
unfold acc(isNode(node1), wildcard)
unfold acc(isNode(node2), wildcard)
if (node1.vari < node2.vari) {
l1 := and(bdd, node1.left, node2)
r1 := and(bdd, node1.right, node2)
res := mkCompound(bdd, node1.vari, l1, r1)
} else {
if (node1.vari == node2.vari) {
l1 := and(bdd, node1.left, node2.left)
r1 := and(bdd, node1.right, node2.right)
res := mkCompound(bdd, node1.vari, l1, r1)
} else {
l1 := and(bdd,node1, node2.left)
r1 := and(bdd,node1, node2.right)
res := mkCompound(bdd, node2.vari, l1, r1)
}
}
}
}
}
}
marcoeilers commented
Fixed in PR #712