1. Grep for relevant patterns
2. Glob for similar files
3. Read existing implementations
4. Understand existing patterns before proposing new ones

1. WebSearch "z3 python {concept}"
2. WebFetch Z3 documentation
3. Check existing z3_helpers.py
4. Test patterns with Bash(python -c "...")

1. Read existing theories (logos, exclusion, imposition, bimodal)
2. Identify common patterns
3. Check theory_lib/__init__.py for registration
4. Review theory-specific tests

1. Receive task context (description, focus)
2. Extract key concepts (Z3 features, theory patterns, testing)
3. Search local codebase for related code
4. Search web for Z3/Python documentation if needed
5. Validate patterns with quick Python tests
6. Analyze implementation approaches
7. Create research report
8. Return results

# Python Research Report: Task #{N}

**Task**: {title}
**Date**: {date}
**Focus**: {focus}

## Summary

{Overview of findings}

## Codebase Findings

### Related Files
- `path/to/file.py` - {description}

### Existing Patterns
```python
# Pattern name
def example():
    ...

# Proposed implementation approach
class NewFeature:
    ...

## Return Format

```json
{
  "status": "completed",
  "summary": "Found N relevant patterns for implementation",
  "artifacts": [
    {
      "path": ".claude/specs/{N}_{SLUG}/reports/research-001.md",
      "type": "research",
      "description": "Python/Z3 research report"
    }
  ],
  "patterns_found": [
    {"name": "Pattern.name", "location": "file.py", "relevance": "high"}
  ],
  "z3_apis_needed": [
    "z3.Solver", "z3.Bool"
  ],
  "recommended_approach": "Description of recommended approach"
}

# Test Z3 pattern
PYTHONPATH=Code/src python -c "
import z3
s = z3.Solver()
x = z3.Bool('x')
s.add(x)
print(s.check())
"

# Test import
PYTHONPATH=Code/src python -c "from model_checker import ..."

# Check theory structure
ls Code/src/model_checker/theory_lib/logos/