//https://leetcode.com/problems/path-sum\r

/**\r

function hasPathSum(root: TreeNode | null, targetSum: number): boolean {\r

    if(root == null) {\r

        return false;\r

    }\r

    if(root.val-targetSum == 0 && root.left == null && root.right == null) {\r

        return true;\r

    }\r

    return hasPathSum(root.left, targetSum-root.val) || hasPathSum(root.right, targetSum-root.val);\r

};\r

 */\r

\r

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

\r

function TreeSeq(root: TreeNode): seq<TreeNode> {\r

    match root {\r

        case Nil => [Nil]\r

        case Cons(val, left, right) => [root]+TreeSeq(left)+TreeSeq(right)\r

    }\r

}\r

\r

function TreeSet(root: TreeNode): set<TreeNode> {\r

    match root {\r

        case Nil => {Nil}\r

        case Cons(val, left, right) => TreeSet(left)+{root}+TreeSet(right)\r

    }\r

}\r

\r

predicate isPath(paths: seq<TreeNode>, root: TreeNode) {\r

    if |paths| == 0 then false else match paths[0] {\r

        case Nil => false\r

        case Cons(val, left, right) => if |paths| == 1 then root == paths[0] else root == paths[0] && (isPath(paths[1..], left) || isPath(paths[1..], right))\r

    }\r

}\r

\r

function pathSum(paths: seq<TreeNode>): nat {\r

    if |paths| == 0 then 0 else match paths[0] {\r

        case Nil => 0\r

        case Cons(val, left, right) => val + pathSum(paths[1..])\r

    }\r

}\r

\r

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) \r

    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum\r

{\r

    if root == Nil {\r

        return false;\r

    }\r

\r

    if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {\r

        assert isPath([root], root) && pathSum([root]) == targetSum;\r

        return true;\r

    }\r

    var leftPath := hasPathSum(root.left, targetSum-root.val);\r

    var rightPath := hasPathSum(root.right, targetSum-root.val);\r

\r

    if leftPath {\r

        ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;\r

        assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;\r

    }\r

    if rightPath {\r

        ghost var p: seq<TreeNode> :| isPath(p, root.right) && pathSum(p) == targetSum-root.val;\r

        assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;\r

    }\r

    return leftPath || rightPath;\r

}\r

\r

method Test() {\r

    var c := Cons(3, Nil, Nil);\r

    var b := Cons(2, c, Nil);\r

    var a := Cons(1, b, Nil);\r

    assert isPath([a], a);\r

    assert a.left == b;\r

    assert isPath([a,b], a);\r

    assert isPath([a,b,c], a);\r

}\r

\r

\r

\r