playbooks

home / skills / a5c-ai / babysitter / smt-solver-interface

smt-solver-interface skill

/plugins/babysitter/skills/babysit/process/specializations/domains/science/computer-science/skills/smt-solver-interface

This skill helps you reason about SMT solvers for automated verification and synthesis, generating queries, selecting theories, and extracting models.

npx playbooks add skill a5c-ai/babysitter --skill smt-solver-interface

Review the files below or copy the command above to add this skill to your agents.

Files (1)
SKILL.md
892 B
---
name: smt-solver-interface
description: Interface with SMT solvers for verification and synthesis
allowed-tools:
  - Bash
  - Read
  - Write
  - Edit
  - Glob
  - Grep
metadata:
  specialization: computer-science
  domain: science
  category: formal-verification
  phase: 6
---

# SMT Solver Interface

## Purpose

Provides expert guidance on using SMT solvers for automated reasoning, verification, and program synthesis.

## Capabilities

- Z3 query generation
- CVC5 interface
- Theory selection guidance
- Model extraction
- Unsat core analysis
- Incremental solving

## Usage Guidelines

1. **Encoding**: Encode problem in SMT-LIB format
2. **Theory Selection**: Choose appropriate theories
3. **Solving**: Run SMT solver
4. **Model Extraction**: Extract satisfying assignments
5. **Debugging**: Analyze unsat cores for debugging

## Tools/Libraries

- Z3
- CVC5
- Boolector
- Yices

Overview

This skill provides a practical interface to SMT solvers for verification, automated reasoning, and program synthesis workflows. It exposes capabilities for generating solver queries, selecting theories, running incremental checks, extracting models, and retrieving unsat cores. The goal is to make SMT tools like Z3 and CVC5 accessible as deterministic, resumable steps inside larger agentic workflows.

How this skill works

The skill encodes problems into SMT-LIB or solver-native queries, chooses appropriate background theories (bitvectors, arithmetic, arrays, etc.), and dispatches queries to Z3, CVC5 or other supported backends. It supports incremental solving, model extraction for satisfying instances, and unsat core analysis for debugging infeasible constraints. The interface returns structured solver responses that can be consumed by orchestration logic for verification or synthesis tasks.

When to use it

  • Formal verification of program properties, invariants, or contracts.
  • Synthesis of small programs, functions, or parameter values satisfying constraints.
  • Debugging complex constraint sets using unsat cores and minimal failing subsets.
  • Automated test-case generation from path constraints.
  • Integrating SMT checks into deterministic, resumable agent workflows.

Best practices

  • Encode constraints in SMT-LIB or the solver's native API for clarity and portability.
  • Select the lightest expressive theory set required; avoid mixing heavy theories unless necessary.
  • Use incremental solving for sequences of related queries to reuse solver state and improve performance.
  • Request models only when queries are satisfiable; request unsat cores or proofs for infeasible cases.
  • Limit domain sizes or add bounds for synthesis tasks to keep search tractable.

Example use cases

  • Verify that a refactored function preserves pre/post-conditions by translating properties to SMT queries.
  • Synthesize configuration parameters that satisfy a set of resource and policy constraints.
  • Find a counterexample execution path for a safety property using path constraints from symbolic execution.
  • Diagnose conflicting constraints in a specification by extracting and analyzing an unsat core.
  • Drive automated planning or scheduling agents with constraint checks to validate candidate plans.

FAQ

Which solvers are supported?

The interface targets Z3 and CVC5 primarily, with compatibility layers for other solvers such as Boolector and Yices when needed.

How do I get useful debugging information for failing checks?

Enable unsat core generation and proof logging where supported, and use incremental solving to isolate the smallest conflicting subset of constraints.