Skip to content

Instantly share code, notes, and snippets.

@ranjitjhala

ranjitjhala/ple.rkt

Last active July 30, 2020 23:11
Show Gist options
  • Save ranjitjhala/8083d19e874b12c0b7c2f769f8882665 to your computer and use it in GitHub Desktop.
Save ranjitjhala/8083d19e874b12c0b7c2f769f8882665 to your computer and use it in GitHub Desktop.
Download ZIP
PLE formula for `foo 3 == 0`
Raw
ple.rkt
(assert
(and (and (= (= (- (- 3 1) 1) 7) false)
(= (= (- 3 1) 4) false)
(=
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0)))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0)))
(= (= (- (- (- 3 1) 1) 1) 4) false)
(= (foo 3) 0)
(=
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0))
(=
(ite
(= (- (- (- 3 1) 1) 1) 6)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 5)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0))))))
(ite
(= (- (- (- 3 1) 1) 1) 5)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0))))))
(= (= (- (- (- 3 1) 1) 1) 7) false)
(=
(ite
(= (- 3 1) 6)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 5)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0))))))
(ite
(= (- 3 1) 5)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0))))))
(= (= (- 3 1) 7) false)
(= (= (- (- (- 3 1) 1) 1) 6) false)
(=
(apply$35$$35$1
(as is$36$GHC.Types.$58$ Int)
(as GHC.Types.$91$$93$ Int))
false)
(= (= (- 3 1) 6) false)
(= (= (- (- (- 3 1) 1) 1) 9) false)
(= (= (- 3 1) 9) false)
(= (= (- (- 3 1) 1) 3) false)
(= (= (- (- 3 1) 1) 10) false)
(=
(ite
(= (- 3 1) 9)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 8)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 7)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 6)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 5)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0)))))))))
(ite
(= (- 3 1) 8)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 7)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 6)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 5)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0)))))))))
(=
(ite
(= (- 3 1) 7)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 6)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 5)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0)))))))
(ite
(= (- 3 1) 6)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 5)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0)))))))
(=
(ite
(= (- (- 3 1) 1) 9)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 8)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 7)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 6)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 5)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 1)
(foo (- (- (- 3 1) 1) 1))
0)))))))))
(ite
(= (- (- 3 1) 1) 8)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 7)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 6)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 5)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 1)
(foo (- (- (- 3 1) 1) 1))
0)))))))))
(=
(ite
(= (- (- (- 3 1) 1) 1) 9)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 8)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 7)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 6)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 5)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0)))))))))
(ite
(= (- (- (- 3 1) 1) 1) 8)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 7)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 6)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 5)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0)))))))))
(=
(ite
(= (- 3 1) 5)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0)))))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0)))))
(=
(ite
(= (- (- (- 3 1) 1) 1) 5)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0)))))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0)))))
(=
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0)))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0)))
(=
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite (= (- (- (- 3 1) 1) 1) 1) (foo (- (- (- (- 3 1) 1) 1) 1)) 0))
(ite (= (- (- (- 3 1) 1) 1) 1) (foo (- (- (- (- 3 1) 1) 1) 1)) 0))
(= (= (- (- (- 3 1) 1) 1) 3) false)
(= (= (- 3 1) 3) false)
(= (= (- (- 3 1) 1) 9) false)
(= (= (- (- 3 1) 1) 8) false)
(=
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 10)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 9)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 8)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 7)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 6)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 5)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0)))))))))))
(= (= (- (- 3 1) 1) 1) true)
(= (= (- (- (- 3 1) 1) 1) 2) false)
(= (= (- (- (- 3 1) 1) 1) 5) false)
(= (= (- 3 1) 5) false)
(=
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0)))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0)))
(=
(ite
(= (- (- 3 1) 1) 7)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 6)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 5)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0)))))))
(ite
(= (- (- 3 1) 1) 6)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 5)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0)))))))
(=
(foo (- (- 3 1) 1))
(ite
(= (- (- 3 1) 1) 10)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 9)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 8)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 7)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 6)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 5)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 1)
(foo (- (- (- 3 1) 1) 1))
0)))))))))))
(= (= (- (- 3 1) 1) 6) false)
(= (= (- (- 3 1) 1) 5) false)
(=
(ite
(= (- (- 3 1) 1) 10)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 9)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 8)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 7)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 6)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 5)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 1)
(foo (- (- (- 3 1) 1) 1))
0))))))))))
(ite
(= (- (- 3 1) 1) 9)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 8)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 7)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 6)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 5)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 1)
(foo (- (- (- 3 1) 1) 1))
0))))))))))
(=
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0)
(foo (- (- (- 3 1) 1) 1)))
(= (= (- (- 3 1) 1) 4) false)
(=
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0))))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0))))
(= (foo 3) (foo (- 3 1)))
(= (= (- (- (- 3 1) 1) 1) 1) false)
(=
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0))))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0))))
(=
(ite
(= (- (- (- 3 1) 1) 1) 8)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 7)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 6)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 5)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0))))))))
(ite
(= (- (- (- 3 1) 1) 1) 7)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 6)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 5)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0))))))))
(=
(ite
(= (- 3 1) 8)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 7)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 6)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 5)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0))))))))
(ite
(= (- 3 1) 7)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 6)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 5)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0))))))))
(=
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0))))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0))))
(=
(ite
(= (- (- 3 1) 1) 8)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 7)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 6)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 5)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0))))))))
(ite
(= (- (- 3 1) 1) 7)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 6)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 5)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0))))))))
(= (= (- (- 3 1) 1) 2) false)
(= (= (- (- (- 3 1) 1) 1) 8) false)
(=
(ite
(= (- (- 3 1) 1) 5)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0)))))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0)))))
(= (= (- 3 1) 8) false)
(=
(ite
(= (- (- (- 3 1) 1) 1) 7)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 6)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 5)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0)))))))
(ite
(= (- (- (- 3 1) 1) 1) 6)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 5)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0)))))))
(=
(ite (= (- (- (- 3 1) 1) 1) 1) (foo (- (- (- (- 3 1) 1) 1) 1)) 0)
0)
(= (= (- 3 1) 2) true)
(=
(ite
(= (- 3 1) 10)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 9)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 8)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 7)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 6)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 5)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0))))))))))
(ite
(= (- 3 1) 9)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 8)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 7)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 6)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 5)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0))))))))))
(=
(ite
(= (- (- (- 3 1) 1) 1) 10)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 9)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 8)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 7)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 6)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 5)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0))))))))))
(ite
(= (- (- (- 3 1) 1) 1) 9)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 8)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 7)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 6)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 5)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 4)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 1)
(foo (- (- (- (- 3 1) 1) 1) 1))
0))))))))))
(=
(ite
(= (- (- 3 1) 1) 6)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 5)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0))))))
(ite
(= (- (- 3 1) 1) 5)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 4)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 3)
(foo (- (- (- 3 1) 1) 1))
(ite
(= (- (- 3 1) 1) 2)
(foo (- (- (- 3 1) 1) 1))
(ite (= (- (- 3 1) 1) 1) (foo (- (- (- 3 1) 1) 1)) 0))))))
(= (= (- (- (- 3 1) 1) 1) 10) false)
(= (= (- 3 1) 10) false)
(=
(foo (- 3 1))
(ite
(= (- 3 1) 10)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 9)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 8)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 7)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 6)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 5)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 4)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 3)
(foo (- (- 3 1) 1))
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0)))))))))))
(=
(ite
(= (- 3 1) 2)
(foo (- (- 3 1) 1))
(ite (= (- 3 1) 1) (foo (- (- 3 1) 1)) 0))
(foo (- (- 3 1) 1))))))
@ranjitjhala
Copy link
Author

ranjitjhala commented Jul 30, 2020 •
edited
Loading

The above is the PLE generated invariant (with all equalities) for the below code, namely foo 3 == 0.

{-@ reflect foo @-}
foo :: Int -> Int
foo n
  | n == 10 = foo (n-1)
  | n == 9 = foo (n-1)
  | n == 8 = foo (n-1)
  | n == 7 = foo (n-1)
  | n == 6 = foo (n-1)
  | n == 5 = foo (n-1)
  | n == 4 = foo (n-1)
  | n == 3 = foo (n-1)
  | n == 2 = foo (n-1)
  | n == 1 = foo (n-1)
  | otherwise = 0

{-@ thm3 :: () -> { foo 3 == 0 } @-}
thm3 :: () -> ()
thm3 () = ()

Yes, the SMT solver can handle it fast, but I'm pretty sure there's lots of overhead just generating and manipulating the data structures
that create the above. If instead we could produce something like:

(and 
  (= (foo 3) (foo (3 - 1)))
  (= (foo (3 - 1)) (foo (3 - 1 - 1))) 
  (= (foo (3 - 1 - 1)) (foo (3 - 1 - 1 - 1)))
  (= (foo (3 - 1 - 1 - 1)) 0))

then I'm sure it would be a nice performance boost.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment