solve_logic_program
Check satisfiability of a structured logic program defined with sorts, functions, and constraints using Z3.
Instructions
Solve a structured logic program (Logic-LLM format).
The program should have sections:
Declarations
EnumSort, IntSort, Function declarations
Constraints
Logical constraints
Example:
# Declarations
Color = EnumSort([red, green, blue])
assign = Function(Object -> Color)
# Constraints
assign(obj1) != assign(obj2)Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| logic_program | Yes | Structured logic program | |
| timeout_ms | No | Timeout in milliseconds (default: 30000) |