@isl-lang/isl-smt

SMT (Satisfiability Modulo Theories) solver integration for ISL verification.

Features

• Real SMT Solving: Integration with Z3 and CVC5 solvers
• Built-in Solver: Bounded solver for simple cases without external dependencies
• Cross-Platform: Automatic solver detection on Windows, Linux, and macOS
• Strict Timeouts: No hanging processes - every solve has a hard timeout with process kill
• Deterministic: Same query always produces same result (via caching)
• Proof Bundles: Solver evidence attached to verification results

Installation

npm install @isl-lang/isl-smt

For real SMT solving (recommended for production), install Z3:

# macOS
brew install z3

# Ubuntu/Debian
apt-get install z3

# Windows (with chocolatey)
choco install z3

# Or download from: https://github.com/Z3Prover/z3/releases

Quick Start

import { solve, Expr, Sort } from '@isl-lang/isl-smt';

// Check if x > 0 AND x < 10 is satisfiable
const result = await solve(
  Expr.and(
    Expr.gt(Expr.var('x', Sort.Int()), Expr.int(0)),
    Expr.lt(Expr.var('x', Sort.Int()), Expr.int(10))
  ),
  { timeout: 5000 }
);

if (result.verdict === 'disproved') {
  console.log('Satisfiable with model:', result.model);
  // { x: 5 } (or any value 1-9)
}

Solver Modes

Builtin Solver (Default)

The builtin solver handles common cases without requiring external solvers:

import { solve } from '@isl-lang/isl-smt';

const result = await solve(formula, {
  solver: 'builtin', // default
  timeout: 5000,
});

Capabilities:

• Boolean SAT solving (up to ~20 variables)
• Linear integer arithmetic (bounded)
• Simple constraint analysis

Use when:

• Quick verification without Z3 installation
• Development and testing
• Simple constraints

Z3 Solver (Recommended for Production)

Full SMT solving with Z3:

import { solve, isZ3Available } from '@isl-lang/isl-smt';

if (await isZ3Available()) {
  const result = await solve(formula, {
    solver: 'z3',
    timeout: 10000,
  });
}

Capabilities:

• All SMT-LIB 2 theories
• Unlimited variable count
• Quantifier support
• Model generation

CVC5 Solver

Alternative solver with CVC5:

import { solve, isCVC5Available } from '@isl-lang/isl-smt';

if (await isCVC5Available()) {
  const result = await solve(formula, {
    solver: 'cvc5',
    timeout: 10000,
  });
}

Auto-Detection

Let the library choose the best available solver:

import { getSolverAvailability, solve } from '@isl-lang/isl-smt';

const availability = await getSolverAvailability();
console.log('Best available:', availability.bestAvailable);
// 'z3', 'cvc5', or 'builtin'

Supported Theories

| Theory | Builtin | Z3 | CVC5 | |--------|---------|-----|------| | Booleans | Yes | Yes | Yes | | Integers (bounded) | Yes | Yes | Yes | | Integers (unbounded) | No | Yes | Yes | | Reals | Limited | Yes | Yes | | Strings | No | Yes | Yes | | Arrays | No | Yes | Yes | | Bitvectors | No | Yes | Yes | | Quantifiers | No | Yes | Yes |

Supported Operations

Boolean:

• and, or, not, implies, iff

Arithmetic:

• +, -, *, div, mod
• =, !=, <, <=, >, >=
• abs, min, max

Quantifiers (Z3/CVC5 only):

• forall, exists

Arrays (Z3/CVC5 only):

• select, store

Timeout Handling

Every solve operation has a hard timeout to prevent hanging:

const result = await solve(formula, { timeout: 5000 }); // 5 seconds

// Result can be:
// - { verdict: 'proved' }           // Formula is valid
// - { verdict: 'disproved', model } // Found counterexample
// - { verdict: 'unknown', reason }  // Could not determine (timeout, etc.)

Guarantees:

• Process killed if timeout exceeded
• No memory leaks from zombie processes
• Output truncated if too large (1MB default)

Proof Bundles

For formal verification, attach solver evidence to results:

import { verifyFormal } from '@isl-lang/isl-smt';

const { batchResult, proofBundle } = await verifyFormal(domain, {
  solver: 'z3',
  timeout: 10000,
  generateEvidence: true,
});

// Each entry has solver evidence
for (const entry of proofBundle) {
  console.log(`${entry.name}: ${entry.verdict}`);
  if (entry.solverEvidence) {
    console.log(`  Solver: ${entry.solverEvidence.solver}`);
    console.log(`  Status: ${entry.solverEvidence.status}`);
    console.log(`  Duration: ${entry.solverEvidence.durationMs}ms`);
    console.log(`  Query hash: ${entry.solverEvidence.queryHash}`);
  }
}

Proof Bundle Entry Format

interface ProofBundleEntry {
  id: string;                    // Unique identifier
  kind: 'precondition_satisfiability' | 'postcondition_implication' | 'refinement_constraint';
  name: string;                  // Name of verified item
  expression: string;            // SMT-LIB expression
  verdict: 'proved' | 'disproved' | 'unknown';
  verdictSource: 'runtime_only' | 'solver_only' | 'runtime_then_solver';
  
  // Solver evidence (if generateEvidence: true)
  solverEvidence?: {
    queryHash: string;           // SHA-256 hash for reproducibility
    solver: 'builtin' | 'z3' | 'cvc5';
    status: 'sat' | 'unsat' | 'unknown' | 'timeout' | 'error';
    model?: Record<string, unknown>;
    reason?: string;
    durationMs: number;
    smtLibQuery?: string;        // Raw SMT-LIB for debugging
    timestamp: string;
  };
}

Resolving Unknown Results

When runtime verification returns "unknown", use SMT to resolve:

import { resolveUnknown } from '@isl-lang/isl-smt';

// In your verifier, when you get an unknown result:
if (result.triState === 'unknown') {
  const resolution = await resolveUnknown(
    clause.expression,
    clause.inputValues,
    { solver: 'z3', timeout: 5000 }
  );
  
  if (resolution.resolved?.verdict === 'proved') {
    result.triState = true;
    result.reason = 'Proved by SMT solver';
  }
  
  // Attach evidence to proof bundle
  if (resolution.evidence) {
    proofBundle.solverEvidence = resolution.evidence;
  }
}

Caching

Results are cached by query hash for determinism:

import { getGlobalCache, resetGlobalCache } from '@isl-lang/isl-smt';

// Get cache statistics
const stats = getGlobalCache().getStats();
console.log('Cache hit rate:', stats.hitRate);

// Clear cache if needed
resetGlobalCache();

Cross-Platform Support

The library automatically detects solver binaries:

| Platform | Search Locations | |----------|------------------| | Windows | z3.exe in PATH, C:\Program Files\Z3\bin, C:\z3\bin | | macOS | z3 in PATH, /usr/local/bin, /opt/homebrew/bin | | Linux | z3 in PATH, /usr/bin, /usr/local/bin |

Custom path:

import { checkSolverAvailability } from '@isl-lang/isl-smt';

const availability = await checkSolverAvailability('z3', '/custom/path/to/z3');

API Reference

Solving

• solve(formula, options) - High-level solve with tri-state output
• createSolver(options) - Create solver instance
• translate(formula, declarations) - Generate SMT-LIB string

Availability

• isZ3Available() - Check Z3 availability
• isCVC5Available() - Check CVC5 availability
• getSolverAvailability() - Get all solver info
• getBestAvailableSolver() - Get best available solver

Verification

• verifySMT(domain, options) - Verify ISL domain
• verifyFormal(domain, options) - Formal mode with evidence
• resolveUnknown(expr, values, options) - Resolve unknown results

External Solver

• checkSatExternal(smtlib, config) - Run external solver directly
• runSolver(smtlib, config) - Low-level solver execution

Example: Full Verification Flow

import {
  verifySMT,
  resolveUnknown,
  getSolverAvailability,
} from '@isl-lang/isl-smt';

async function verifyWithSMT(domain) {
  // Check what's available
  const { bestAvailable } = await getSolverAvailability();
  console.log(`Using solver: ${bestAvailable}`);
  
  // Run verification
  const result = await verifySMT(domain, {
    solver: bestAvailable,
    timeout: 10000,
    verbose: true,
  });
  
  console.log('Summary:');
  console.log(`  Total: ${result.summary.total}`);
  console.log(`  SAT: ${result.summary.sat}`);
  console.log(`  UNSAT: ${result.summary.unsat}`);
  console.log(`  Unknown: ${result.summary.unknown}`);
  
  // Try to resolve unknowns
  for (const r of result.results) {
    if (r.result.status === 'unknown') {
      console.log(`Attempting to resolve: ${r.name}`);
      const resolution = await resolveUnknown(
        /* expression from clause */,
        /* input values */,
        { solver: 'z3', timeout: 30000 }
      );
      console.log(`  Result: ${resolution.resolved?.verdict}`);
    }
  }
  
  return result;
}

License

MIT