remove API

[MichaelRawson]

See #157. The API currently doesn't build and doesn't look like it will be revived any time soon. Remove it to improve greppability of the current codebase, can be restored later if/when desired.

I tried to remove the relevant stuff from the Makefile build, hopefully I didn't break anything.

[MichaelRawson]

Ah - @selig I remember that I opened #183 a while back, but then closed it. I don't remember why exactly. Feel free to say you still want this in the tree.

[selig]

I don't have a lot of love for the current API code. I've never touched it. @ibnyusuf spent some time trying to bring it back.

BUT I do think it's very important that we have a programmatic API. We often see people calling Vampire by writing to file and reading the result, which adds unnecessary overhead to the integration and a general barrier to integration.

There are other SMT general API libraries we could/should integrate with as well.

Perhaps this code isn't helpful and we should start again on an API, I don't know.

[MichaelRawson]

BUT I do think it's very important that we have a programmatic API. We often see people calling Vampire by writing to file and reading the result, which adds unnecessary overhead to the integration and a general barrier to integration.

Agreed. If at the very least we had some way to invoke Vampire in a black-box fashion it would be nice, others have asked for the same thing recently. I'll think about it.

[quickbeam123]

This is rooted in "Tue Nov 17 10:44:11 2020". Will it survive merge with the current master?

[ibnyusuf]

I did implement a working API on this branch.

The main difficulty faced, was that I never managed to wrangle the input via API to be exactly the same as input via a file. Symbol order or some other subtle thing would differ. As we know, this can have a major impact on the shape of proof search making it very difficult to debug API calls that don't behave as expected.

In any case, if we ever want to revive the API in the future we have the option of going back to my branch, the original, or just starting from scratch.

So no objections to removing the code.

[selig]

My guess is that to solve the problem of via file vs via API we would want to make the parser use the API to construct the problem. That would require some decoupling in the parsers that should be possible but a little bit of work.