dafny how to bound set comprehension resolver?

user_821989 0
Viewed 69

Trying to write an algorithm involving paths from a root of a binary tree to a leaf. I ran into the following error for the ghost var I was trying to define. I had intended to try to show that some other path was in this set. How do I resolve this error?

the result of a set comprehension must be finite, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'px'Resolver

datatype TreeNode = Nil | Cons(val: nat, left: TreeNode, right: TreeNode)

predicate isPath(paths: seq<TreeNode>, root: TreeNode) 
    requires root != Nil && root == paths[0] ==> root !in paths[1..]
{
    if |paths| == 0 then false else match paths[0] {
        case Nil => false
        case Cons(val, left, right) => if |paths| == 1 then root == paths[0] else root == paths[0] && (isPath(paths[1..], left) || isPath(paths[1..], right))
    }
}

method Test(root: TreeNode) {
   ghost var ps := set px: seq<TreeNode> | isPath(px, root) ;
}

I thought that perhaps Dafny implied that there could be a loop in the tree which would result in infinite paths, so I wrote the following to try to assert it was not possible. However, it still did not resolve the issue. I believe there should be a finite albeit large number of paths.

function TreeSet(root: TreeNode): set<TreeNode> {
    match root {
        case Nil => {}
        case Cons(val, left, right) => TreeSet(left)+{root}+TreeSet(right)
    }
}

function ChildSet(root: TreeNode): set<TreeNode> {
    match root {
        case Nil => {}
        case Cons(val, left, right) => {left}+ChildSet(left)+{right}+ChildSet(right)
    }
}

method Test(root: TreeNode) 
    requires forall node :: node in TreeSet(root) ==> node !in ChildSet(node)
{
   ghost var ps := set px: seq<TreeNode> | isPath(px, root) ;
}
dafny set
2 Answers

Dafny enforces finiteness of set using syntactic scan and fixed set of heuristics, as a result it is not exhaustive. Following example give same error

predicate test(i: int)
{
   i >= 10 && i <= 20
}

method Test(){
  ghost var s := set i | test(i);
}

Also no language construct exists to convince dafny that set constructed using set comprehension is finite set.

[1] https://github.com/dafny-lang/dafny/issues/13#issuecomment-286909795

[2] https://github.com/dafny-lang/dafny/issues/1366#issuecomment-906785889

user_144130690

This is not the end of the story.

You can definitely use iset that don't have the constraint to check that they are finite.

The following code snippet works, modulo the fact that there are still unsatisfied preconditions in the recursive calls to isPath:

datatype TreeNode = Nil | Cons(val: nat, left: TreeNode, right: TreeNode)

predicate isPath(paths: seq<TreeNode>, root: TreeNode) 
    requires root != Nil && root == paths[0] ==> root !in paths[1..]
{
    if |paths| == 0 then false else match paths[0] {
        case Nil => false
        case Cons(val, left, right) => if |paths| == 1 then root == paths[0] else root == paths[0] && (isPath(paths[1..], left) || isPath(paths[1..], right))
    }
}

method Test(root: TreeNode) {
   ghost var ps := iset px: seq<TreeNode> | |px| > 0 && root != Nil && root == px[0] ==> root !in px[1..] && isPath(px, root) ;
}
user_12878560
Related