Skip to main content
Glama
theTyster

smt-mcp

by theTyster
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Local

check_satisfiability

Verify if SMT-LIB constraints are jointly satisfiable, cross-checking Z3 and cvc5 to return verdicts, witnesses, and caveats.

Instructions

Check whether a set of constraints is jointly satisfiable, cross-checked in both Z3 and cvc5.

YOU (the calling model) are responsible for translating the user's prose question into declarations and constraints. This server does NOT interpret English — it only runs the SMT-LIB you hand it. Pass the user's original wording in prose so the English and the formalization travel together in the evidence trail.

Before presenting the verdict to the user as an answer about their original English question, SHOW THEM THE FORMALIZATION (the declarations and constraints, or the assembled smtlib_script) and get their agreement that it captures what they meant. A verdict from this tool is a fact about the formalization, not directly about the user's English.

Report exactly what the solvers returned. An UNSATISFIABLE verdict is bounded-unsat relative to the constraints and declarations as written, not an unbounded proof about the world — do not upgrade it into a stronger claim. Read the caveats list and pass its contents along (quantifiers, nonlinear arithmetic, uninterpreted sorts, or bounded checks each get their own caveat). If status comes back DISAGREEMENT, that is the headline: the two solvers returned different verdicts and the result must not be trusted.

declarations are full SMT-LIB forms, e.g. (declare-const x Int). constraints are bare boolean terms, e.g. (> x 5) — this tool wraps each in (assert ...) for you (a constraint that already starts with (assert is accepted as-is).

Example: declarations = ["(declare-const x Int)"] constraints = ["(> x 5)", "(< x 8)"] -> satisfiable (both solvers find a witness, e.g. x = 6).

Input Schema

TableJSON Schema
NameRequiredDescriptionDefault
logicNo
proseNo
timeout_msNo
constraintsYes
declarationsYes

Schema Changelog

Changes observed during successful MCP inspections.

  1. First observedv0.1.0

TDQS

A3.9/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations, the description carries the full behavioral burden and does so extensively. It discloses the cross-solver design, that the server does not interpret English, that UNSATISFIABLE is bounded relative to the formalization, that caveats must be surfaced, and that DISAGREEMENT is a headline untrustworthy result.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The definition is long but front-loaded with purpose and then organized into operational guidance. Most sentences carry useful constraints or warnings, though some procedural repetition could be tightened without losing meaning.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

No output schema exists, so the description must cover returns, and it does: verdicts, caveats, and DISAGREEMENT are all explained. It is nearly complete for a complex solver tool, with the main omission being parameter details for logic and timeout_ms.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 0%, so the description must compensate. It clearly explains declarations, constraints, and prose usage with an example, but it says nothing about the logic or timeout_ms parameters, leaving part of the five-parameter surface undocumented.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

The first sentence names a specific operation and resource: checking joint satisfiability of constraints with cross-checking in Z3 and cvc5. That distinguishes it from a generic SMT runner, but no sibling tool is named, so an agent must infer the boundary with check_entailment or run_smtlib.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description gives clear procedural context: the caller must translate prose into declarations/constraints, show the formalization for user agreement, and report solver output exactly. However, it never says when to choose this tool over check_entailment or run_smtlib, so the when-vs-alternative guidance remains implicit.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Deploy Server

Other Tools