SMT Solving

SMT (Satisfiability Modulo Theories) solving usually means installing binaries and learning solver-specific flags. Here you send the problem over HTTP and get back a verdict — with models and unsat cores when you need them. Looking for plain propositional logic? That's the SAT endpoint.

Quickstart

Submit an SMT-LIB 2.0 problem:

curl -X POST https://api.mcpte.ch/v1/smt \
  -H 'Content-Type: application/json' \
  -d '{"problem":"(declare-const x Int) (assert (= x 5)) (check-sat)"}'

Returns a job id:

{ "job_id": "0191cc2e-...+", "status": "queued" }

Poll for the result:

curl https://api.mcpte.ch/v1/jobs/{job_id}

{ "status": "completed", "result": { "sat": true } }

Endpoints

Models & debugging

Request a model with (get-model) in your SMT-LIB script (or list specific assignments with (get-value ...)) and the result includes a model object with each assignment as a string:

{
  "status": "completed",
  "result": { "sat": true, "model": { "x": "5", "on": "true" } }
}

Unsat results return "sat": false and — when requested — an unsat_core array naming the conflicting assertions to help you debug. If the solver cannot decide, "sat": null with an error message: that is not the same as unsat.

Authentication

MCP

A native Model Context Protocol server is available at https://api.mcpte.ch/v1/mcp using the Streamable HTTP transport. Use it from Claude Desktop, Cursor, and other MCP clients — it handles JSON parsing and result polling for you, and this endpoint is available as a tool.