search

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
186 stars 46 forks source link

Cloud-based Solver #11

Closed PhilippWendler closed 7 years ago

PhilippWendler commented 8 years ago

A solver package that implements the usual interface and delegates solving to a cloud-based webservice could be added (like in this paper).

It is questionable whether this would be useful, given that many queries are faster than the typical internet latency, and supporting push/pop etc. would be difficult.

cheshire commented 8 years ago

Some people do this -- eg Isabelle exposes http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP through the "sledgehammer" tactics. However, their problems are usually much larger (I would think)

cheshire commented 8 years ago

TPTP has machines with Z3 and CVC4 installed; maybe it would be even possible to query their infrastructure.

cheshire commented 8 years ago

Wow, there is even a translator to TPTP format from SMT-LIB! https://bitbucket.org/peba123/smttotptp Thus all we need to do is to dump a query in SMT-LIB and perform a query to the cloud solver.

cheshire commented 8 years ago

We would need to construct formulas though, as currently we are relying on solvers datastructures entirely.

PhilippWendler commented 8 years ago

Instead of our own formula representation, we could also use for example SmtInterpol for this task.

dbeyer commented 8 years ago

But will the TPTP people let us send many queries and produce significant load? It looks like a web interface just for humans, not for machines.

cheshire commented 7 years ago

Doesn't look like this is coming anytime soon :P