search

tip-org / benchmarks

Tons of Inductive Problems: The Benchmarks
http://tip-org.github.io/
BSD 3-Clause "New" or "Revised" License
24 stars 6 forks source link

spurious `@` in some benchmarks? #5

Closed c-cube closed 8 years ago

c-cube commented 8 years ago

Some problems, e.g. benchmarks/isaplanner/prop_12.smt2, contain the symbol @, which is not declared. I am not very familiar with smtlib2 but I don't think it is a special keyword.

nick8325 commented 8 years ago

This is our extension for first-class functions - @ is the application operator. Unfortunately the documentation for the TIP language is rather sparse but you can find it described at http://www.cse.chalmers.se/~nicsma/papers/tip-tools.pdf.

If you run tip --lambda-lift --axiomatize-lambdas, all uses of @ will be axiomatised away. You can also look in the benchmarks-cvc4 directory for versions of the benchmarks which have been translated to more standard smtlib2.

c-cube commented 8 years ago

My bad, thanks.