diff --git a/CHANGELOG.md b/CHANGELOG.md index cf132d9..68a18c9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,9 @@ # Changelog +### [3.4.0] - 2024-07-02 + +- **New Feature:** Full integration of Answer Set Programming (ASP) via clingo API + ### [3.3.0] - 2025-06-10 - **New Feature:** Added MaxSAT as a 4th mode for weighted optimization problems using RC2 solver @@ -17,7 +21,6 @@ - **Update:** Enhanced documentation for model code formats in README.md and INSTALL.md - **Update:** Added support for LM Studio local models - --- ### [3.1.0] - 2025-04-03 diff --git a/INSTALL.md b/INSTALL.md index 454a639..0b39eed 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -129,7 +129,7 @@ python -m venv .venv ### Install dependencies ```bash -uv pip install -e ."[all]" +uv pip install -e ".[all]" ``` This installs the MCP Solver in editable mode. @@ -182,6 +182,7 @@ uv run test-setup-z3 uv run test-setup-pysat uv run test-setup-maxsat uv run test-setup-client +uv run test-setup-asp ``` ## Step 6: Test Client Setup diff --git a/README.md b/README.md index 21140a4..3f12f8d 100644 --- a/README.md +++ b/README.md @@ -132,6 +132,23 @@ Z3 mode provides access to Z3 SMT (Satisfiability Modulo Theories) solving capab mcp-solver-z3 ``` +### ASP Mode + +ASP (Answer Set Programming) mode provides integration with ASP solvers (e.g., Clingo) for declarative problem solving with logic programs. Features include: + +- Expressive logic programming for combinatorial and knowledge representation problems +- Support for constraints, choice rules, aggregates, and optimization statements +- Integration with the Clingo solver for efficient answer set computation +- Access to answer sets and model inspection + +**Dependencies**: Requires the `clingo` package (`uv pip install -e ".[asp]"` or included in `[all]`) + +**Configuration**: To run in ASP mode, use: + +``` +mcp-solver-asp +``` + ## MCP Test Client The MCP Solver includes an MCP client for development, experimentation, and diagnostic purposes, based on the *ReAct* agent framework. This client serves as an intermediary between an LLM and the MCP server, facilitating the translation of natural language problem statements into formal constraint programming solutions. @@ -148,7 +165,7 @@ uv run test-setup-client The client requires an **API key** from an LLM provider. For Anthropic (the default LLM is Claude Sonnet 3.7), set the `ANTHROPIC_API_KEY` environment variable. This can be set in your environment or included in a `.env` file in the project root. -The client also supports other LLM providers including OpenAI, Google (Gemini), OpenRouter, and even local models via LM Studio. You can specify which model to use with the `--mc` command line flag. See [INSTALL.md](INSTALL.md) for details on model code formats. +The client also supports other LLM providers including OpenAI, Google (Gemini), OpenRouter and even local models via LM Studio. You can specify which model to use with the `--mc` command line flag. See [INSTALL.md](INSTALL.md) for details on model code formats. ### Usage @@ -166,6 +183,9 @@ uv run run-test maxsat --problem # Z3 mode uv run run-test z3 --problem + +# ASP mode +uv run run-test asp --problem ``` ------ diff --git a/prompts/asp/instructions.md b/prompts/asp/instructions.md new file mode 100644 index 0000000..29f5ed4 --- /dev/null +++ b/prompts/asp/instructions.md @@ -0,0 +1,253 @@ +# MCP Solver – ASP (clingo) Quick Start Guide + +Welcome to the MCP Solver. This document provides detailed guidelines for building and solving Answer Set Programming (ASP) models using the clingo Python API. + +## Overview + +The MCP Solver integrates ASP solving with the Model Context Protocol, allowing you to create, modify, and solve logic programs incrementally. The following tools are available: + +- **clear_model** +- **add_item** +- **replace_item** +- **delete_item** +- **solve_model** + +These tools let you construct your model item by item and solve it using clingo. + +## ASP Model Items and Structure + +- **ASP Item:** + An ASP item is a complete fact, rule, or constraint (ending with a period). Inline comments are considered part of the same item. + +- **No Output Statements:** + Do not include output formatting in your model. The solver handles only facts, rules, and constraints. + +- **Indices Start at 0:** + Items are added one by one, starting with index 0 (i.e., index=0, index=1, etc.). + +## List Semantics for Model Operations + +The model items behave like a standard programming list with these exact semantics: + +- **add_item(index, content)**: Inserts the item at the specified position, shifting all items at that index and after to the right. + - Example: If model has items [A, B, C] and you call add_item(1, X), result is [A, X, B, C] + - Valid index range: 0 to length (inclusive) + +- **delete_item(index)**: Removes the item at the specified index, shifting all subsequent items to the left. + - Example: If model has items [A, B, C, D] and you call delete_item(1), result is [A, C, D] + - Valid index range: 0 to length-1 (inclusive) + +- **replace_item(index, content)**: Replaces the item at the specified index in-place. No shifting occurs. + - Example: If model has items [A, B, C] and you call replace_item(1, X), result is [A, X, C] + - Valid index range: 0 to length-1 (inclusive) + +**Important**: All indices are 0-based. The first item is at index 0, the second at index 1, etc. + +**Critical: Index stability on errors** + +- Indices only change when an operation succeeds. If `add_item`, `replace_item`, or `delete_item` returns an error, the model is unchanged and item indices remain exactly the same. +- Specifically for `add_item`: do not advance your intended insertion index after a failed call. Try again with the same index once the cause of the error is fixed. + +## Tool Input and Output Details + +1. **clear_model** + - **Input:** No arguments. + - **Output:** Confirmation that the model has been cleared. + +2. **add_item** + - **Input:** + - `index` (integer): Position to insert the new ASP statement. + - `content` (string): The complete ASP statement to add. + - **Output:** Confirmation and the current (truncated) model. + - **Index behavior on error:** If the call fails (e.g., invalid index, malformed content), the model is not modified and no indices shift. Do not increment your next `index` based on a failed attempt. + +3. **replace_item** + - **Input:** + - `index` (integer): Index of the item to replace. + - `content` (string): The new ASP statement. + - **Output:** Confirmation and the updated (truncated) model. + +4. **delete_item** + - **Input:** + - `index` (integer): Index of the item to delete. + - **Output:** Confirmation and the updated (truncated) model. + +5. **solve_model** + - **Input:** + - `timeout` (number): Time in seconds allowed for solving (between 1 and 30 seconds). + - **Output:** + - A JSON object with: + - **status:** `"SAT"`, `"UNSAT"`, or `"TIMEOUT"`. + - **solution:** (If applicable) The solution object when the model is satisfiable. + +## Model Solving and Verification + +- **Solution Verification:** + After solving, verify that the returned solution satisfies all specified constraints. If the model is satisfiable (`SAT`), you will receive both the status and the solution; otherwise, only the status is provided. + +## Model Modification Guidelines + +- **Comments:** + A comment is not an item by itself. Always combine a comment with the fact, rule, or constraint it belongs to. + +- **Combining similar parts:** + If you have a long list of similar facts or rules, you can put them into the same item. + +- **Incremental Changes:** + Use `add_item`, `replace_item`, and `delete_item` to modify your model incrementally. This allows you to maintain consistency in item numbering without needing to clear the entire model. + +- **Making Small Changes:** + When a user requests a small change to the model (like changing a parameter value or modifying a rule), use `replace_item` to update just the relevant item rather than rebuilding the entire model. This maintains the model structure and is more efficient. + +- **When to Clear the Model:** + Use `clear_model` only when extensive changes are required and starting over is necessary. + +## Important: Model Item Indexing + +ASP mode uses **0-based indexing** for all model operations: +- First item is at index 0 +- Used with add_item, replace_item, delete_item +- Example: `add_item(0, "color(red).")` adds at the beginning +- Example: `replace_item(2, "edge(a,b).")` replaces the third item + +## Blueprint: Recommended ASP Model Structure + +A typical ASP model for MCP Solver should follow this structure: + +1. **Facts and Data**: All problem-specific facts and data. +2. **Domain Declarations**: Define domains, constants, and sets. +3. **Rules**: Logical rules that define relationships and constraints. +4. **Integrity Constraints**: Constraints that must be satisfied (e.g., `:- condition.`). +5. **Optimization Statements** (if any): Use `#minimize` or `#maximize` as needed. + +**Example:** +```asp +% Item 0: Facts +graph_node(a). graph_node(b). graph_node(c). +edge(a,b). edge(b,c). + +% Item 1: Domain +domain_color(red). +domain_color(green). +domain_color(blue). + +% Item 2: Rules +1 { color(N,C) : domain_color(C) } 1 :- graph_node(N). + +% Item 3: Integrity Constraints +:- edge(N,M), color(N,C), color(M,C). + +% Item 4: Optimization (optional) +#minimize { 1,N,C : color(N,C) }. +``` + +## Best Practices + +- **Use clear, descriptive names** for predicates and variables. +- **Comment complex rules** for clarity. +- **Group related facts and rules** together. +- **Avoid redundant rules** and facts. +- **Test incrementally**: Add and solve small parts before building the full model. +- **Use integrity constraints** to enforce requirements. +- **Use optimization statements** only when required by the problem. + +## Common Pitfalls + +- **Forgetting periods** at the end of facts/rules. +- **Incorrect variable usage** (e.g., ungrounded variables). +- **Redundant or conflicting rules**. +- **Missing or incorrect integrity constraints**. +- **Improper use of optimization statements**. +- **Not checking for unsatisfiable models**. + +## Minimal Working Example + +Suppose you want to color a simple graph: + +```asp +% Item 0: Facts +graph_node(a). graph_node(b). graph_node(c). +edge(a,b). edge(b,c). + +% Item 1: Domain +domain_color(red). +domain_color(green). +domain_color(blue). + +% Item 2: Rules +1 { color(N,C) : domain_color(C) } 1 :- graph_node(N). + +% Item 3: Integrity Constraints +:- edge(N,M), color(N,C), color(M,C). + +% Item 4: Optimization (optional) +#minimize { 1,N,C : color(N,C) }. +``` + +## Advanced ASP Constructs and Patterns + +### Defaults and Exceptions (Negation-as-Failure) + +- Encode defaults using `not` and override with explicit exceptions. +- Pattern: +```asp +flies(X) :- bird(X), not abnormal(X). +abnormal(X) :- penguin(X). +:- penguin(X), flies(X). +``` +- Tips: + - Place taxonomy rules first (e.g., `bird(X) :- penguin(X).`). + - Keep defaults separate from integrity constraints that enforce exceptions. + +### Negation-as-Failure for Eligibility Policies + +- Derive permissive defaults, then constrain with explicit facts. +```asp +eligible(C) :- customer(C), not excluded(C). +eligible(C) :- vip(C), not blacklisted(C). +excluded(C) :- blacklisted(C). +:- eligible(C), excluded(C). +``` +- Use integrity constraints to prevent contradictory conclusions. + +### Recursive Aggregates (#sum) + +- Aggregate over a recursively defined relation to compute thresholds. +```asp +controls(X,X) :- company(X). +contrib(A,B,A,P) :- owns(A,B,P). +contrib(A,B,C,P) :- controls(A,C), owns(C,B,P), A != C. +sum(A,B,S) :- S = #sum { P,C : contrib(A,B,C,P) }. +controls(A,B) :- sum(A,B,S), S > 50, A != B. +``` +- Use helper predicates like `contrib/4` to keep aggregates readable. + +### Weak Constraints (Optimization with :~) + +- Prefer solutions that minimize penalties using weak constraints. +```asp +1 { assign(T,S) : slot(S) } 1 :- task(T). +:- assign(T,S), conflict(T,S). +:~ prefer(T,S,W), not assign(T,S). [W@1,T,S] +``` +- Alternatively, use `#minimize` with weighted literals. +- Keep all hard constraints as `:- ...` and only preferences in weak constraints. + +### Modeling UNSAT for Testing + +- To intentionally create UNSAT, introduce contradictory defaults with integrity constraints. +```asp +p :- not not_p. +not_p :- not p. +:- p. +:- not p. +``` +- Useful for verifying solver correctly reports `UNSAT`. + +## Final Notes + +- **Review return information** after each tool call. +- **Maintain a consistent structure** for easier debugging and review. +- **Verify solutions** after solving to ensure all constraints are met. + +Happy modeling with MCP Solver and ASP (clingo)! diff --git a/prompts/asp/review.md b/prompts/asp/review.md new file mode 100644 index 0000000..ab257e8 --- /dev/null +++ b/prompts/asp/review.md @@ -0,0 +1,106 @@ +# ASP (clingo) Solution Review Template + +Your task is to review an Answer Set Programming (ASP) solution for structural correctness, adherence to the problem statement, and best practices. + +## Problem Statement + +${PROBLEM} + +## Model Implementation + +${MODEL} + +## Solution Results + +${SOLUTION} + +## Review Guidelines + +⚠️ **IMPORTANT**: Do NOT try to verify that the logic of every rule is mathematically correct. However, DO verify that the solution satisfies the hard constraints and requirements stated in the problem. + +Focus on these checks: + +1. **Structural Correctness** + - Are all facts, rules, and constraints properly terminated with periods? + - Are variables properly grounded (no unsafe variables)? + - Are integrity constraints (`:- ... .`) used for hard requirements? + - Are optimization statements (`#minimize`, `#maximize`) used only if required? + - Is the model divided into clear sections (facts, domains, rules, constraints, optimization)? + +2. **Hard Constraint Satisfaction** + - Based on the solution, check if all integrity constraints are satisfied. + - For example: If the problem says "no two adjacent nodes have the same color", verify this in the solution. + - Focus on constraints you can easily verify from the problem statement and solution. + - If unsure about complex encodings, skip them. + +3. **Solution Format & Completeness** + - Does the solution include all required outputs from the problem statement? + - Are all relevant variables/atoms present in the solution? + - Does the solution format match what the problem asks for? + +4. **For Unsatisfiable Solutions** + - **IMPORTANT**: You do NOT need to explain WHY the problem is unsatisfiable. + - Simply verify that all integrity constraints in the model are justified by the problem statement. + - Note that "unsatisfiable" is a perfectly valid result—if all constraints are justified by the problem, mark it as correct. + - Trust the solver's determination of unsatisfiability. + +5. **Basic Sanity Checks** + - Are all atoms/variables in the solution properly grounded? + - Are there any obvious contradictions or missing assignments? + +6. **Optimality Verification** + - If the solution claims to be optimal (e.g., with a cost value), check if this makes sense given the problem and constraints. + - For optimization problems, verify that the reported cost matches the solution's assignments. + +7. **DO NOT Check** + - ❌ Whether the logic of each rule is mathematically correct (trust the encoding for non-obvious cases) + - ❌ Whether the solution is globally optimal (trust the solver) + - ❌ Complex Boolean formula transformations + - ❌ Whether soft constraint polarities match your interpretation + +## Output Format + +After your detailed analysis, provide your verdict using simple XML tags. + +**Your answer MUST follow this structure:** +1. First provide a detailed explanation of your reasoning +2. Analyze each constraint in detail +3. End with a clear conclusion statement: "The solution is correct." or "The solution is incorrect." +4. Finally, add exactly ONE of these verdict tags on a new line: + correct + incorrect + unknown + +For example: +``` +[Your detailed analysis here] + +After checking all constraints, I can confirm that each one is satisfied by the provided solution values. + +The solution is correct. + +correct +``` + +The verdict must be EXACTLY one of: "correct", "incorrect", or "unknown" nothing else. + +**Before finalizing your response, always check that:** +1. Your explanation ends with a clear conclusion statement +2. The verdict tag matches your conclusion exactly +3. If your explanation concludes "The solution is correct", then use correct +4. If your explanation concludes "The solution is incorrect", then use incorrect +5. If you cannot determine correctness or establish incorrectness, use unknown + +## Data + +### Problem Statement + +$PROBLEM + +### ASP Model + +$MODEL + +### Solution + +$SOLUTION diff --git a/pyproject.toml b/pyproject.toml index 5d860fb..3adfcb3 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -7,7 +7,7 @@ packages = ["src/mcp_solver", "tests"] [project] name = "mcp-solver" -version = "3.3.0" +version = "3.4.0" description = "MCP server for Constraint, SAT, and SMT solving" authors = [ {name = "Stefan Szeider", email = "stefan@szeider.net"}, @@ -42,8 +42,12 @@ client = [ "rich>=13.9.4", "uuid>=1.30", ] +asp = [ + "clingo>=5.8.0", + "dumbo-asp>=0.3.16", +] all = [ - "mcp-solver[mzn,z3,pysat,client,dev]", + "mcp-solver[mzn,z3,pysat,asp,client,dev]", ] dev = [ "coverage>=7.7.1", @@ -52,6 +56,7 @@ dev = [ ] [project.scripts] +test-setup-asp = "mcp_solver.asp.test_setup:main" test-setup-mzn = "mcp_solver.mzn.test_setup:main" test-setup-z3 = "mcp_solver.z3.test_setup:main" test-setup-pysat = "mcp_solver.pysat.test_setup:main" @@ -62,6 +67,7 @@ mcp-solver-mzn = "mcp_solver.core.__main__:main_mzn" mcp-solver-z3 = "mcp_solver.core.__main__:main_z3" mcp-solver-pysat = "mcp_solver.core.__main__:main_pysat" mcp-solver-maxsat = "mcp_solver.core.__main__:main_maxsat" +mcp-solver-asp = "mcp_solver.core.__main__:main_asp" test-client = "mcp_solver.client.client:main_cli" run-test = "tests.run_test:main" @@ -146,4 +152,4 @@ warn_return_any = true warn_unused_configs = true [tool.test_client] -recursion_limit = 200 \ No newline at end of file +recursion_limit = 200 diff --git a/src/mcp_solver/asp/__init__.py b/src/mcp_solver/asp/__init__.py new file mode 100644 index 0000000..ab87d34 --- /dev/null +++ b/src/mcp_solver/asp/__init__.py @@ -0,0 +1,8 @@ +""" +Clingo integration for MCP Solver. +""" + +from .model_manager import ASPModelManager + + +__all__ = ["ASPModelManager"] diff --git a/src/mcp_solver/asp/environment.py b/src/mcp_solver/asp/environment.py new file mode 100644 index 0000000..c313cc3 --- /dev/null +++ b/src/mcp_solver/asp/environment.py @@ -0,0 +1,2 @@ +# environment.py +# Handles ASP environment setup and clingo configuration diff --git a/src/mcp_solver/asp/error_handling.py b/src/mcp_solver/asp/error_handling.py new file mode 100644 index 0000000..fe0526d --- /dev/null +++ b/src/mcp_solver/asp/error_handling.py @@ -0,0 +1,132 @@ +""" +ASP error handling module using dumbo_asp Parser. + +This module provides enhanced error handling for ASP operations, including: +- Function wrappers that capture and translate ASP exceptions +- Context-aware error messages using dumbo_asp.primitives.parsers.Parser +- Structured error reporting for better user experience +""" + +import functools +import logging +import traceback +from collections.abc import Callable +from typing import Any, TypeVar + + +# Try to import dumbo_asp Parser +try: + from dumbo_asp.primitives.parsers import Parser + + DUMBO_ASP_AVAILABLE = True +except ImportError: + DUMBO_ASP_AVAILABLE = False + +logger = logging.getLogger(__name__) +T = TypeVar("T") + +# Map of common ASP exceptions to user-friendly messages +EXCEPTION_MESSAGES = { + "SyntaxError": { + "unexpected token": "Syntax error in ASP code: unexpected token.", + "unexpected character": "Syntax error in ASP code: unexpected character.", + "unexpected end of input": "Syntax error: unexpected end of input.", + }, + "RuntimeError": { + "clingo": "Clingo runtime error. Check your ASP code for semantic issues.", + }, +} + + +class ASPError(Exception): + """Custom exception class for enhanced ASP errors.""" + + def __init__( + self, + message: str, + original_error: Exception | None = None, + context: str | None = None, + ): + self.original_error = original_error + self.original_traceback = traceback.format_exc() + enhanced_message = message + if context: + enhanced_message += f"\nHere are more error details:\n{context}" + if original_error: + error_type = type(original_error).__name__ + error_msg = str(original_error) + enhanced_message += f"\n\nOriginal error ({error_type}): {error_msg}" + super().__init__(enhanced_message) + + +def asp_error_handler(func: Callable[..., T]) -> Callable[..., T]: + """ + Decorator to handle ASP exceptions with enhanced error messages. + """ + + @functools.wraps(func) + def wrapper(*args: Any, **kwargs: Any) -> T: + try: + return func(*args, **kwargs) + except Exception as e: + error_type = type(e).__name__ + error_msg = str(e) + # Try to find a matching error message pattern + friendly_message = None + if error_type in EXCEPTION_MESSAGES: + for pattern, message in EXCEPTION_MESSAGES[error_type].items(): + if pattern in error_msg: + friendly_message = message + break + if not friendly_message: + friendly_message = f"Error in ASP operation: {error_msg}" + # Gather context information (could include code snippet, etc.) + context = "" + # Log the error with full traceback for debugging + logger.error( + f"ASP error in {func.__name__}: {error_type}: {error_msg}", + exc_info=True, + ) + raise ASPError(friendly_message, original_error=e, context=context) from e + + return wrapper + + +def validate_asp_code(asp_code: str) -> list[str]: + """ + Validate ASP code using dumbo_asp Parser if available. + Returns a list of error messages (empty if no errors). + """ + + errors = [] + if not asp_code.strip(): + return errors + if DUMBO_ASP_AVAILABLE: + try: + Parser.parse_program(asp_code) + except Exception as e: + # Handle different error types appropriately + if hasattr(e, "llm_message"): + errors.append(e.llm_message) + else: + errors.append(str(e)) # Use string representation of the error + else: + # Fallback: try basic syntax check (e.g., unmatched parentheses) + if asp_code.count("(") != asp_code.count(")"): + errors.append("Unmatched parentheses in ASP code.") + return errors + + +def format_solution_error(error: Exception) -> dict[str, Any]: + """ + Format an error for inclusion in the solution. + """ + error_type = type(error).__name__ + error_msg = str(error) + return { + "satisfiable": False, + "status": "error", + "success": True, # Keep server connection logic satisfied + "error_type": error_type, + "error_message": error_msg, + } diff --git a/src/mcp_solver/asp/model_manager.py b/src/mcp_solver/asp/model_manager.py new file mode 100644 index 0000000..65f2dcd --- /dev/null +++ b/src/mcp_solver/asp/model_manager.py @@ -0,0 +1,289 @@ +# model_manager.py +# Manages ASP models, runs clingo, and parses results + +from datetime import timedelta + +import clingo + +from ..core.base_model_manager import BaseModelManager + +# --- Integration: Import new error handling and solution modules --- +from . import error_handling, solution + + +class ModelError(Exception): + """Custom exception for model-related errors""" + + pass + + +class ASPModelManager(BaseModelManager): + """ + ASP model manager implementation using clingo. + Manages ASP models, runs clingo, and parses answer sets. + """ + + def __init__(self): + super().__init__() + self.initialized = True + self.last_solution = None + self._last_raw_result = None + + async def _validate_model( + self, items: list[str], validate_grounding: bool = True + ) -> tuple[str, clingo.Control | None]: + """ + Validates the full model through syntax and optionally grounding checks. + + Args: + items: List of ASP code fragments to validate + validate_grounding: If True, also checks for grounding errors + + Returns: + Tuple of (list of error messages, Control object if grounding successful) + The Control object is only returned if validate_grounding is True and grounding succeeds + """ + asp_code = "\n".join(items) + if not asp_code.strip(): + return "", None # Empty model is valid + + # First check syntax using dumbo_asp + syntax_errors = error_handling.validate_asp_code(asp_code) + if syntax_errors: + return "\n".join(syntax_errors), None + + if not validate_grounding: + return "", None + + # Now check grounding if requested + messages = [] + + def logger(_, message): + messages.append(message) + + try: + ctl = clingo.Control(logger=logger) + ctl.add("base", [], asp_code) + ctl.ground([("base", [])]) + except Exception as e: + # If grounding fails, return the error messages + if messages: + return "Grounding error:\n" + "\n".join(messages), None + if messages: + return "Grounding error:\n" + "\n".join(messages), None + return "", ctl + + async def add_item(self, index: int, content: str) -> dict: + """ + Attempt to add an item (ASP code fragment) at the specified index. + + This method implements the MCP editing protocol's incremental validation: + 1. It creates a hypothetical model with the new item inserted. + 2. It validates the entire model using clingo to ensure it is syntactically correct and groundable. + 3. If validation succeeds, the item is added to the model. + 4. If validation fails, the change is rejected and an error is returned. + + Args: + index: The position at which to insert the new item (0-based). + content: The ASP code fragment to add. + + Returns: + A dictionary indicating success or failure, and an error message if rejected. + """ + if not (0 <= index <= len(self.code_items)): + return { + "success": False, + "error": f"Invalid index {index}. Valid range: 0 to {len(self.code_items)}", + } + + hypothetical_items = self.code_items[:] + hypothetical_items.insert(index, content) + + validation_errors, _ = await self._validate_model(hypothetical_items) + if validation_errors: + return { + "success": False, + "error": f"Validation failed: {validation_errors}", + } + + return await super().add_item(index, content) + + async def delete_item(self, index: int) -> dict: + """ + Attempt to delete an item (ASP code fragment) at the specified index. + + This method implements incremental validation: + 1. It creates a hypothetical model with the item at the given index removed. + 2. It validates the entire model using clingo to ensure it remains groundable. + 3. If validation succeeds, the item is deleted from the model. + 4. If validation fails, the change is rejected and an error is returned. + + Args: + index: The position of the item to delete (0-based). + + Returns: + A dictionary indicating success or failure, and an error message if rejected. + """ + if not (0 <= index < len(self.code_items)): + return { + "success": False, + "error": f"Invalid index {index}. Valid range: 0 to {len(self.code_items) - 1}", + } + + hypothetical_items = self.code_items[:] + del hypothetical_items[index] + + validation_errors, _ = await self._validate_model(hypothetical_items) + if validation_errors: + return { + "success": False, + "error": f"Validation failed after deletion: {validation_errors}", + } + + return await super().delete_item(index) + + async def replace_item(self, index: int, content: str) -> dict: + """ + Attempt to replace an item (ASP code fragment) at the specified index. + + This method implements the MCP editing protocol's incremental validation: + 1. It creates a hypothetical model with the item at the given index replaced. + 2. It validates the entire model using clingo to ensure it is syntactically correct and groundable. + 3. If validation succeeds, the replacement is committed to the model. + 4. If validation fails, the change is rejected and an error is returned. + + Args: + index: The position of the item to replace (0-based). + content: The new ASP code fragment to use as replacement. + + Returns: + A dictionary indicating success or failure, and an error message if rejected. + """ + if not (0 <= index < len(self.code_items)): + return { + "success": False, + "error": f"Invalid index {index}. Valid range: 0 to {len(self.code_items) - 1}", + } + + hypothetical_items = self.code_items[:] + hypothetical_items[index] = content + + validation_errors, _ = await self._validate_model(hypothetical_items) + if validation_errors: + return { + "success": False, + "error": f"Validation failed: {validation_errors}", + } + + return await super().replace_item(index, content) + + async def solve_model(self, timeout: timedelta) -> dict: + """ + Solve the current ASP model using clingo, with enhanced error handling and solution formatting. + Args: + timeout: Maximum time to spend on solving + Returns: + A dictionary with the solving result and answer sets, or a structured error solution + """ + if not self.code_items: + error_sol = solution.export_solution( + error_handling.ASPError( + "No model items to solve", context="Empty model" + ) + ) + self.last_solution = error_sol + return error_sol + + # Validate and get pre-grounded control object if successful + validation_errors, ctl = await self._validate_model(self.code_items) + if validation_errors: + err = error_handling.ASPError( + "Model validation failed", context=validation_errors + ) + error_sol = solution.export_solution(err) + self.last_solution = error_sol + return error_sol + + answer_sets = [] + try: + + def on_model(model): + atoms = [str(atom) for atom in model.symbols(shown=True)] + answer_sets.append(atoms) + + with ctl.solve(on_model=on_model, async_=True) as handle: + handle.wait(timeout.total_seconds()) + handle.cancel() + handle.get() + stats = ctl.statistics + self.last_solve_time = ( + stats.get("summary", {}).get("times", {}).get("solve", 0.0) + ) + # --- Integration: Use solution.export_solution for standardized output --- + sol = solution.export_solution(answer_sets) + self.last_solution = sol + self._last_raw_result = ctl + return sol + except Exception as e: + # --- Integration: Use solution.export_solution for error reporting --- + error_sol = solution.export_solution(e) + self.last_solution = error_sol + return error_sol + + def get_solution(self) -> dict: + """ + Get the last computed answer sets. + Returns: + A dictionary with the answer sets + """ + if not self.last_solution: + return {"success": False, "message": "No solution available"} + return {"success": True, "solution": self.last_solution} + + def get_variable_value(self, variable_name: str) -> dict: + """ + Get the value of a variable (atom) from the last answer set. + This searches for atoms starting with the given variable_name in all answer sets. + + Args: + variable_name: The atom name to search for + Returns: + A dictionary with the value(s) of the atom + """ + if not self.last_solution: + return {"success": False, "message": "No solution available"} + # Search for the atom in all answer sets + results = [] + for answer_set in self.last_solution: + values = [atom for atom in answer_set if atom.startswith(variable_name)] + results.append(values) + + if not any(results): + return { + "success": False, + "message": f"Atom starting with '{variable_name}' not found in any answer set.", + } + + return {"success": True, "variable": variable_name, "values": results} + + def get_solve_time(self) -> dict: + """ + Get the time taken for the last solve operation. + + Returns: + A dictionary with the solve time information + """ + if self.last_solve_time is None: + return { + "success": False, + "message": "No solve operation has been performed", + } + return {"success": True, "solve_time": self.last_solve_time, "unit": "seconds"} + + async def clear_model(self) -> dict: + """Clears the model and resets the solver's internal state.""" + result = await super().clear_model() + self.last_solution = None + self._last_raw_result = None + result["message"] = "ASP model cleared" + return result diff --git a/src/mcp_solver/asp/solution.py b/src/mcp_solver/asp/solution.py new file mode 100644 index 0000000..641de28 --- /dev/null +++ b/src/mcp_solver/asp/solution.py @@ -0,0 +1,126 @@ +""" +ASP solution module for extracting and formatting solutions from ASP solvers. + +This module provides functions for extracting solution data from ASP solvers +and converting it to a standardized format. +""" + +import logging +from typing import Any + +from .error_handling import ASPError, format_solution_error + + +logger = logging.getLogger(__name__) + +_LAST_SOLUTION = None + +RESERVED_KEYS = { + "satisfiable", + "answer_sets", + "values", + "status", + "error_type", + "error_message", + "warnings", +} + + +def export_solution( + data: Any = None, + status: str | None = None, + warnings: list[str] | None = None, +) -> dict[str, Any]: + """ + Extract and format solutions from an ASP solver or answer set data. + + Args: + data: List of answer sets, or dictionary containing solution data + status: Optional status string ("sat", "unsat", "error") + warnings: Optional list of warning messages + + Returns: + Dictionary with structured solution data, including: + - satisfiable: Boolean indicating if at least one answer set was found + - status: String status ("sat", "unsat", or "error") + - answer_sets: List of answer sets (each a list of atoms) + - values: Flattened dictionary of all atoms (True if present in any answer set) + - warnings: List of warning messages (if any) + + If an error occurs, the returned dictionary will include: + - satisfiable: False + - error_type: Type of the error + - error_message: Detailed error message + - status: "error" + """ + global _LAST_SOLUTION + try: + # If data is an exception, format as error immediately + if isinstance(data, Exception): + error_solution = format_solution_error(data) + _LAST_SOLUTION = error_solution + return error_solution + solution_data = _process_input_data(data, status, warnings) + solution_data = _extract_values_from_answer_sets(solution_data) + # Ensure success flag for normal results to prevent server from overriding status + solution_data["success"] = True + logger.debug(f"Setting _LAST_SOLUTION: {solution_data}") + _LAST_SOLUTION = solution_data + return solution_data + except Exception as e: + error_solution = format_solution_error(e) + _LAST_SOLUTION = error_solution + logger.error(f"Error in export_solution: {e!s}", exc_info=True) + return error_solution + + +def _process_input_data( + data: Any, + status: str | None = None, + warnings: list[str] | None = None, +) -> dict[str, Any]: + """ + Process input data from various sources into a standardized solution dictionary. + """ + solution_data: dict[str, Any] = {} + # Case 1: Direct dictionary data + if isinstance(data, dict): + solution_data = data.copy() + # Case 2: List of answer sets (each a list of atoms) + elif isinstance(data, list) and (not data or isinstance(data[0], list)): + solution_data["answer_sets"] = data + solution_data["satisfiable"] = bool(data) + # Case 3: None or unknown type + elif data is None: + solution_data["answer_sets"] = [] + solution_data["satisfiable"] = False + else: + raise ASPError(f"Unsupported data type for ASP solution: {type(data).__name__}") + # Set the status field + if status: + solution_data["status"] = status + else: + solution_data["status"] = ( + "sat" if solution_data.get("satisfiable", False) else "unsat" + ) + # Add warnings if provided + if warnings: + solution_data["warnings"] = warnings + # Ensure values dictionary exists (may be populated later) + solution_data["values"] = solution_data.get("values", {}) + return solution_data + + +def _extract_values_from_answer_sets(solution_data: dict[str, Any]) -> dict[str, Any]: + """ + Extract values from answer sets into a flat values dictionary. + """ + answer_sets = solution_data.get("answer_sets", []) + values: dict[str, Any] = {} + # For each atom in any answer set, set True + for answer_set in answer_sets: + for atom in answer_set: + if atom not in values: + values[atom] = True + solution_data["values"] = values + return solution_data diff --git a/src/mcp_solver/asp/templates/__init__.py b/src/mcp_solver/asp/templates/__init__.py new file mode 100644 index 0000000..bc2acd5 --- /dev/null +++ b/src/mcp_solver/asp/templates/__init__.py @@ -0,0 +1,2 @@ +# templates/__init__.py +# Initializes ASP templates module diff --git a/src/mcp_solver/asp/templates/basic_templates.py b/src/mcp_solver/asp/templates/basic_templates.py new file mode 100644 index 0000000..aa92ba2 --- /dev/null +++ b/src/mcp_solver/asp/templates/basic_templates.py @@ -0,0 +1,36 @@ +""" +Basic templates for ASP (clingo). + +This module provides template functions for common ASP patterns. +""" + + +def facts(atoms: list[str]) -> str: + """ + Generate a string of ASP facts from a list of atoms. + + Args: + atoms: List of atoms (strings) + + Returns: + A string containing the ASP facts. + Example: ['a', 'b'] -> 'a.\nb.' + """ + return "\n".join([f"{atom}." for atom in atoms]) + + +def rule(head: str, body: list[str]) -> str: + """ + Generate a simple ASP rule. + Args: + head: The head of the rule. + body: A list of atoms in the body of the rule. + + Returns: + A string containing the ASP rule. + Example: rule('c', ['a', 'b']) -> 'c :- a, b.' + """ + if not body: + return f"{head}." + body_str = ", ".join(body) + return f"{head} :- {body_str}." diff --git a/src/mcp_solver/asp/test_setup.py b/src/mcp_solver/asp/test_setup.py new file mode 100644 index 0000000..d741328 --- /dev/null +++ b/src/mcp_solver/asp/test_setup.py @@ -0,0 +1,258 @@ +#!/usr/bin/env python3 +""" +Test script for verifying the ASP mode installation of MCP-Solver. +This script checks: + 1. Required configuration files for ASP mode + 2. Clingo dependencies + 3. Basic ASP solver functionality +""" + +import asyncio +import sys +from datetime import timedelta +from pathlib import Path + +# Import our centralized prompt loader +from mcp_solver.core.prompt_loader import load_prompt + +from .model_manager import ASPModelManager + + +class ASPSetupTest: + def __init__(self): + self.successes: list[tuple[str, str]] = [] # (test_name, details) + self.failures: list[tuple[str, str]] = [] # (test_name, error_details) + self.base_dir = Path(__file__).resolve().parents[3] + self.GREEN = "\033[92m" + self.RED = "\033[91m" + self.RESET = "\033[0m" + self.BOLD = "\033[1m" + + def print_result(self, test_name: str, success: bool, details: str | None = None): + """Print a test result with color and proper formatting.""" + mark = "✓" if success else "✗" + color = self.GREEN if success else self.RED + print(f"{color}{mark} {test_name}{self.RESET}") + if details: + print(f" └─ {details}") + + def record_test(self, test_name: str, success: bool, details: str | None = None): + """Record a test result and print it.""" + if success: + self.successes.append((test_name, details if details else "")) + else: + self.failures.append((test_name, details if details else "Test failed")) + self.print_result(test_name, success, None if success else details) + + def test_configuration_files(self): + """Test for the presence of required configuration files.""" + print(f"\n{self.BOLD}Configuration Files:{self.RESET}") + + prompts_to_test = [("asp", "instructions"), ("asp", "review")] + + for mode, prompt_type in prompts_to_test: + try: + content = load_prompt(mode, prompt_type) + self.record_test( + f"Prompt file: {mode}/{prompt_type}.md", + True, + f"Successfully loaded ({len(content)} characters)", + ) + except Exception as e: + self.record_test( + f"Prompt file: {mode}/{prompt_type}.md", + False, + f"Error loading prompt: {e!s}", + ) + + def test_asp_dependencies(self): + """Test clingo and dumbo_asp installation and dependencies.""" + print(f"\n{self.BOLD}ASP (clingo) Dependencies:{self.RESET}") + # Check clingo + try: + import clingo + + self.record_test( + "clingo package", True, f"Found version {clingo.__version__}" + ) + except ImportError as e: + self.record_test( + "clingo package", + False, + f"Error importing clingo: {e!s}\nPlease install with: pip install clingo", + ) + return + # Check dumbo_asp + try: + import dumbo_asp + + self.record_test( + "dumbo_asp package", + True, + f"Found version {getattr(dumbo_asp, '__version__', 'unknown')}", + ) + except ImportError as e: + self.record_test( + "dumbo_asp package", + False, + f"Error importing dumbo_asp: {e!s}\nPlease install with: pip install dumbo-asp", + ) + return + + def test_error_handling(self): + """Test ASP error handling functionality including validation and solution export.""" + from mcp_solver.asp import error_handling, solution + + print(f"\n{self.BOLD}ASP Error Handling:{self.RESET}") + + # Test syntax validation + test_cases = [ + ("a. b :- a.", True, "Valid ASP code"), + ("a b :- .", False, "Invalid ASP syntax"), + ( + "result(X) :- undefined_predicate(X).", + True, + "Valid syntax with undefined predicate", + ), + ] + + for code, should_be_valid, desc in test_cases: + print(f"\nValidating {desc}: {code!r}") + errors = error_handling.validate_asp_code(code) + self.record_test( + f"ASP validation ({desc})", + (errors == []) == should_be_valid, + f"Errors: {errors}", + ) + + # Test solution export + print(f"\n{self.BOLD}Solution Export:{self.RESET}") + + # Test successful case + answer_sets = [["a"], ["b", "a"]] + sol = solution.export_solution(answer_sets) + self.record_test( + "Solution export (valid answer sets)", + sol.get("satisfiable") is True, + f"Solution: {sol}", + ) + + # Test error case + try: + raise error_handling.ASPError( + "Simulated ASP error", context='"line: 1", "code": "a b :- ."' + ) + except Exception as e: + err_sol = solution.export_solution(e) + self.record_test( + "Solution export (error case)", + err_sol.get("satisfiable") is False, + f"Error solution: {err_sol}", + ) + + def test_model_manager(self): + """Test ASPModelManager functionality including item management and solving.""" + print(f"\n{self.BOLD}Model Manager Tests:{self.RESET}") + mgr = ASPModelManager() + timeout = timedelta(seconds=5) + + async def run_tests(): + # Test group 1: Model item management + print(f"\n{self.BOLD}1. Model Item Management:{self.RESET}") + + test_cases = [ + (0, "a.", True, "Add initial valid item"), + (1, "b :- a.", True, "Add dependent valid item"), + (2, "a b :- .", False, "Add item with syntax error"), + (10, "c.", False, "Add item at invalid index"), + ( + 2, + "result(X) :- undefined_predicate(X).", + False, + "Add item with grounding error", + ), + ] + + for index, content, should_succeed, desc in test_cases: + print(f"\nTesting: {desc}") + result = await mgr.add_item(index, content) + print(f"Result: {result}") + self.record_test( + f"Model item management - {desc}", + result.get("success") == should_succeed, + str(result), + ) + + # Test group 2: Model solving + print(f"\n{self.BOLD}2. Model Solving:{self.RESET}") + + solve_test_cases = [ + (["a.", "b :- a."], True, "Valid model"), + (["a.", "b :- a.", "a b :- ."], False, "Model with syntax error"), + ( + ["result(X) :- undefined_predicate(X)."], + False, + "Model with grounding error", + ), + ([], False, "Empty model"), + ] + + for items, should_be_satisfiable, desc in solve_test_cases: + print(f"\nTesting: {desc}") + mgr.code_items = items + result = await mgr.solve_model(timeout) + print(f"Result: {result}") + self.record_test( + f"Model solving - {desc}", + result.get("satisfiable") == should_be_satisfiable, + str(result), + ) + + asyncio.run(run_tests()) + + def run_all_tests(self): + """Run all setup tests and display results.""" + print(f"{self.BOLD}=== MCP-Solver ASP Mode Setup Test ==={self.RESET}") + print("Running test suite for ASP mode components...\n") + + test_groups = [ + ("Configuration", self.test_configuration_files), + ("Dependencies", self.test_asp_dependencies), + ("Error Handling", self.test_error_handling), + ("Model Manager", self.test_model_manager), + ] + + for group_name, test_func in test_groups: + print(f"\n{self.BOLD}Testing {group_name}...{self.RESET}") + print("=" * (9 + len(group_name))) + test_func() + + print(f"\n{self.BOLD}=== Test Summary ==={self.RESET}") + print(f"Total tests: {len(self.successes) + len(self.failures)}") + print(f"Passed: {len(self.successes)}") + print(f"Failed: {len(self.failures)}") + + if self.failures: + print(f"\n{self.BOLD}Failed Tests:{self.RESET}") + for test, details in self.failures: + print(f"\n{self.RED}✗ {test}{self.RESET}") + print(f" └─ {details}") + print( + "\nASP mode setup incomplete. Please fix the issues above before proceeding." + ) + sys.exit(1) + else: + print( + f"\n{self.GREEN}✓ All ASP mode tests passed successfully!{self.RESET}" + ) + print("\nSystem is ready to use MCP-Solver in ASP mode.") + sys.exit(0) + + +def main(): + test = ASPSetupTest() + test.run_all_tests() + + +if __name__ == "__main__": + main() diff --git a/src/mcp_solver/client/client.py b/src/mcp_solver/client/client.py index fabe903..c40f36c 100644 --- a/src/mcp_solver/client/client.py +++ b/src/mcp_solver/client/client.py @@ -76,6 +76,7 @@ def format_token_count(count): "z3": ["run", "mcp-solver-z3"], "pysat": ["run", "mcp-solver-pysat"], "maxsat": ["run", "mcp-solver-maxsat"], + "asp": ["run", "mcp-solver-asp"], } # Global Rich Console instance with color support @@ -353,7 +354,7 @@ def parse_arguments(): parser.add_argument( "--mode", type=str, - choices=["mzn", "z3", "pysat", "maxsat"], + choices=["mzn", "z3", "pysat", "maxsat", "asp"], help="Solver mode to use (overrides automatic detection)", ) parser.add_argument( @@ -1101,6 +1102,8 @@ async def main(): mode = "maxsat" elif "pysat" in server_cmd: mode = "pysat" + elif "asp" in server_cmd: + mode = "asp" else: # Default to MiniZinc if no mode or server specified mode = "mzn" diff --git a/src/mcp_solver/client/test_setup.py b/src/mcp_solver/client/test_setup.py index a2f4138..c8a629b 100644 --- a/src/mcp_solver/client/test_setup.py +++ b/src/mcp_solver/client/test_setup.py @@ -86,6 +86,8 @@ def test_configuration_files(self): ("pysat", "review"), ("z3", "instructions"), ("z3", "review"), + ("asp", "instructions"), + ("asp", "review"), ] for mode, prompt_type in prompts_to_test: diff --git a/src/mcp_solver/core/__main__.py b/src/mcp_solver/core/__main__.py index 2cc2529..4c920e2 100644 --- a/src/mcp_solver/core/__main__.py +++ b/src/mcp_solver/core/__main__.py @@ -59,6 +59,15 @@ def main_maxsat(): return server_main() +def main_asp(): + """Entry point for ASP mode""" + from .server import main as server_main + + # Set command line arguments for ASP mode + sys.argv = [sys.argv[0], "--asp"] + return server_main() + + if __name__ == "__main__": try: sys.exit(main()) diff --git a/src/mcp_solver/core/prompt_loader.py b/src/mcp_solver/core/prompt_loader.py index 400dc49..dbf99e7 100644 --- a/src/mcp_solver/core/prompt_loader.py +++ b/src/mcp_solver/core/prompt_loader.py @@ -4,7 +4,7 @@ # Type definitions for better type checking -PromptMode = Literal["mzn", "pysat", "z3", "maxsat"] +PromptMode = Literal["mzn", "pysat", "z3", "maxsat", "asp"] PromptType = Literal["instructions", "review"] logger = logging.getLogger(__name__) @@ -15,7 +15,7 @@ def get_prompt_path(mode: PromptMode, prompt_type: PromptType = "instructions") Get the path to a prompt file based on mode and type, without loading its content. Args: - mode: The solver mode ("mzn", "pysat", "z3", or "maxsat") + mode: The solver mode ("mzn", "pysat", "z3", "maxsat", or "asp") prompt_type: The type of prompt ("instructions" or "review"), defaults to "instructions" Returns: @@ -25,9 +25,9 @@ def get_prompt_path(mode: PromptMode, prompt_type: PromptType = "instructions") ValueError: If invalid mode or prompt type is provided """ # Validate inputs - if mode not in ("mzn", "pysat", "z3", "maxsat"): + if mode not in ("mzn", "pysat", "z3", "maxsat", "asp"): raise ValueError( - f"Invalid mode: {mode}. Must be one of: mzn, pysat, z3, maxsat" + f"Invalid mode: {mode}. Must be one of: mzn, pysat, z3, maxsat, asp" ) if prompt_type not in ("instructions", "review"): @@ -50,7 +50,7 @@ def load_prompt(mode: PromptMode, prompt_type: PromptType) -> str: Load a prompt file based on mode and type. Args: - mode: The solver mode ("mzn", "pysat", "z3", or "maxsat") + mode: The solver mode ("mzn", "pysat", "z3", "maxsat" or "asp") prompt_type: The type of prompt ("instructions" or "review") Returns: diff --git a/src/mcp_solver/core/server.py b/src/mcp_solver/core/server.py index 26fda99..276eb1f 100644 --- a/src/mcp_solver/core/server.py +++ b/src/mcp_solver/core/server.py @@ -24,6 +24,7 @@ Z3_MODE = False PYSAT_MODE = False MAXSAT_MODE = False +ASP_MODE = False try: version_str = version("mcp-solver") @@ -70,6 +71,11 @@ async def serve() -> None: model_mgr = MaxSATModelManager() logging.getLogger(__name__).info("Using MaxSAT model manager") + elif ASP_MODE: + from ..asp.model_manager import ASPModelManager + + model_mgr = ASPModelManager() + logging.getLogger(__name__).info("Using ASP model manager") else: from ..mzn.model_manager import MiniZincModelManager @@ -82,7 +88,7 @@ def get_description(descriptions: dict) -> str: Get the appropriate description based on the current mode. Args: - descriptions: A dictionary of descriptions keyed by mode ('z3', 'pysat', 'maxsat', 'mzn') + descriptions: A dictionary of descriptions keyed by mode ('z3', 'pysat', 'maxsat', 'mzn', 'asp') or a string for a common description across all modes Returns: @@ -97,8 +103,14 @@ def get_description(descriptions: dict) -> str: return descriptions["pysat"] elif MAXSAT_MODE and "maxsat" in descriptions: return descriptions["maxsat"] + elif ASP_MODE and "asp" in descriptions: + return descriptions["asp"] elif ( - not Z3_MODE and not PYSAT_MODE and not MAXSAT_MODE and "mzn" in descriptions + not Z3_MODE + and not PYSAT_MODE + and not MAXSAT_MODE + and not ASP_MODE + and "mzn" in descriptions ): return descriptions["mzn"] elif "default" in descriptions: @@ -130,6 +142,8 @@ async def handle_get_prompt( mode_folder = "pysat" elif MAXSAT_MODE: mode_folder = "maxsat" + elif ASP_MODE: + mode_folder = "asp" else: mode_folder = "mzn" @@ -202,6 +216,7 @@ async def list_tools() -> list[types.Tool]: "z3": "Remove all items from the Z3 Python model, effectively resetting it.", "pysat": "Remove all items from the PySAT Python model, effectively resetting it.", "maxsat": "Remove all items from the MaxSAT optimization model, effectively resetting it.", + "asp": "Remove all items from the ASP model, effectively resetting it.", } ), inputSchema={"type": "object", "properties": {}}, @@ -214,6 +229,7 @@ async def list_tools() -> list[types.Tool]: "z3": "Add new Python code to the Z3 model at a specific index (indices start at 0). Required parameters: 'index' and 'content'.", "pysat": "Add new Python code to the PySAT model at a specific index (indices start at 0). Required parameters: 'index' and 'content'.", "maxsat": "Add new Python code to the MaxSAT optimization model at a specific index (indices start at 0). Required parameters: 'index' and 'content'.", + "asp": "Add new ASP item to the model at a specific index (indices start at 0). Required parameters: 'index' and 'content'.", } ), inputSchema={ @@ -233,6 +249,7 @@ async def list_tools() -> list[types.Tool]: "z3": "Replace an existing item in the Z3 Python model at a specified index with new content. Required parameters: 'index' and 'content'.", "pysat": "Replace an existing item in the PySAT Python model at a specified index with new content. Required parameters: 'index' and 'content'.", "maxsat": "Replace an existing item in the MaxSAT optimization model at a specified index with new content. Required parameters: 'index' and 'content'.", + "asp": "Replace an existing item in the ASP model at a specified index with new content. Required parameters: 'index' and 'content'.", } ), inputSchema={ @@ -252,6 +269,7 @@ async def list_tools() -> list[types.Tool]: "z3": "Delete an item from the Z3 Python model at the specified index. Required parameter: 'index'.", "pysat": "Delete an item from the PySAT Python model at the specified index. Required parameter: 'index'.", "maxsat": "Delete an item from the MaxSAT optimization model at the specified index. Required parameter: 'index'.", + "asp": "Delete an item from the ASP model at the specified index. Required parameter: 'index'.", } ), inputSchema={ @@ -268,6 +286,7 @@ async def list_tools() -> list[types.Tool]: "z3": "Fetch the current content of the Z3 Python model, listing each item with its index.", "pysat": "Fetch the current content of the PySAT Python model, listing each item with its index.", "maxsat": "Fetch the current content of the MaxSAT optimization model, listing each item with its index.", + "asp": "Fetch the current content of the ASP model, listing each item with its index.", } ), inputSchema={"type": "object", "properties": {}}, @@ -280,6 +299,7 @@ async def list_tools() -> list[types.Tool]: "z3": "Solve the current Z3 Python model with a timeout parameter. Required parameter: 'timeout'.", "pysat": "Solve the current PySAT Python model with a timeout parameter. Required parameter: 'timeout'.", "maxsat": "Solve the current MaxSAT optimization model with a timeout parameter. Required parameter: 'timeout'.", + "asp": "Solve the current ASP model with a timeout parameter. Required parameter: 'timeout'.", } ), inputSchema={ @@ -627,17 +647,19 @@ def main() -> int: parser.add_argument( "--maxsat", action="store_true", help="Use MaxSAT optimization solver" ) + parser.add_argument("--asp", action="store_true", help="Use ASP solver") parser.add_argument("--port", type=int, help="Port to listen on (debug)") args = parser.parse_args() # Set global flags based on arguments - global Z3_MODE, PYSAT_MODE, MAXSAT_MODE + global Z3_MODE, PYSAT_MODE, MAXSAT_MODE, ASP_MODE Z3_MODE = args.z3 PYSAT_MODE = args.pysat MAXSAT_MODE = args.maxsat + ASP_MODE = args.asp # Check for incompatible flags - if sum([Z3_MODE, PYSAT_MODE, MAXSAT_MODE]) > 1: + if sum([Z3_MODE, PYSAT_MODE, MAXSAT_MODE, ASP_MODE]) > 1: print("Error: Cannot use multiple solver mode flags at the same time") return 1 @@ -650,6 +672,8 @@ def main() -> int: logging.getLogger(__name__).info( "Server running with MaxSAT optimization solver" ) + elif ASP_MODE: + logging.getLogger(__name__).info("Server running with ASP solver") else: logging.getLogger(__name__).info("Server running with MiniZinc solver") diff --git a/src/mcp_solver/core/test_setup.py b/src/mcp_solver/core/test_setup.py index 104d1c9..a08fc83 100644 --- a/src/mcp_solver/core/test_setup.py +++ b/src/mcp_solver/core/test_setup.py @@ -62,6 +62,8 @@ def test_configuration_files(self): ("pysat", "review"), ("z3", "instructions"), ("z3", "review"), + ("asp", "instructions"), + ("asp", "review"), ] for mode, prompt_type in prompts_to_test: diff --git a/src/mcp_solver/core/validation.py b/src/mcp_solver/core/validation.py index 8496373..8088364 100644 --- a/src/mcp_solver/core/validation.py +++ b/src/mcp_solver/core/validation.py @@ -342,7 +342,6 @@ def get_standardized_response( # Log this with a stack trace to identify the source logger.error( f"CRITICAL INCONSISTENCY DETECTED: success=True with error='{error}'", - exc_info=True, ) # Always override success to be False if there's an error diff --git a/tests/problems/asp/birds_fly.md b/tests/problems/asp/birds_fly.md new file mode 100644 index 0000000..aba4feb --- /dev/null +++ b/tests/problems/asp/birds_fly.md @@ -0,0 +1,29 @@ + +We have a knowledge base that describes different entities and their characteristics, specifically, whether or not they can fly. Model the problem using Answer Set Programming. + +### Here’s what we know: + +- Tweety is a bird and is yellow. +- Opus is a bird and is a penguin. +- Woody is a bird and is a woodpecker. +- Penguins and woodpeckers are both types of birds. +- Later, we find out that Woody is injured due to a broken wing. +- There is also an airplane named Polly, and Polly can fly. + +### General Rules + +- By default, birds can fly. +- Penguins cannot fly (this is an exception). +- Injured birds cannot fly (another exception). +- Anything that can fly is considered mobile. +- All birds have feathers. + +### Task + +For each of the following entities — Tweety, Opus, Woody, and Polly — determine: + +1. Can it fly? +2. Is it mobile? +3. Does it have feathers? +4. For each conclusion, specify the type of reasoning used: + - Was it based on a default rule, an exception, or a direct fact? diff --git a/tests/problems/asp/company_controls.md b/tests/problems/asp/company_controls.md new file mode 100644 index 0000000..62f8c13 --- /dev/null +++ b/tests/problems/asp/company_controls.md @@ -0,0 +1,10 @@ +Solve the following problem using answer set programming (ASP): + +### There are four companies: c1, c2, c3, and c4 + +- Company c1 owns 60% of company c2, giving it direct control over c2. +- Company c1 also owns 20% of company c3. +- Company c2 owns 40% of company c3. +- Company c3 owns 51% of company c4, giving it direct control over c4. + +I want to know all the pair of companies X, Y where X is different than Y such that X controls Y, given the previous information on stock possessions of companies. diff --git a/tests/problems/asp/package_status_unsat.md b/tests/problems/asp/package_status_unsat.md new file mode 100644 index 0000000..33b4782 --- /dev/null +++ b/tests/problems/asp/package_status_unsat.md @@ -0,0 +1,3 @@ +Solve the following problem with answer set programming: + +A package has been marked both as lost and delivered. A package is considered lost if it is not delivered. A package is considered delivered if it is not lost. Consider that a package cannot be lost and delivered at the same time. diff --git a/tests/problems/asp/party_invitation.md b/tests/problems/asp/party_invitation.md new file mode 100644 index 0000000..a0350f1 --- /dev/null +++ b/tests/problems/asp/party_invitation.md @@ -0,0 +1,7 @@ +Solve the following problem using answer set programming (ASP): + +#### Suppose you are organizing a party and you want to invite people under the following rules + +- You will invite Alice unless you know she is not coming. +- You will invite Bob if Alice is not invited. +- You will invite Carol only if both Alice and Bob are invited. diff --git a/tests/problems/asp/shift_assignment.md b/tests/problems/asp/shift_assignment.md new file mode 100644 index 0000000..c7446d2 --- /dev/null +++ b/tests/problems/asp/shift_assignment.md @@ -0,0 +1,11 @@ +## Problem: Assigning Shifts to Employees + +We need to assign 2 employees to work 3 shifts (morning, afternoon, evening). Each shift must be covered by exactly one employee. However, employees have preferences about which shifts they like or dislike. + +The goal is to: + +- Ensure each shift is covered by exactly one employee. +- Assign at most 2 shifts to any employee. +- Prefer assigning employees to their preferred shifts. + +Model and solve the previous problem using answer set programming (ASP) diff --git a/tests/problems/asp/test.md b/tests/problems/asp/test.md new file mode 100644 index 0000000..5d8774c --- /dev/null +++ b/tests/problems/asp/test.md @@ -0,0 +1,10 @@ +# ASP Trivial Test + +## Problem Description +Create a model to verify end-to-end plumbing: choose exactly one of two options. + +## Given +- Two options: a, b + +## Constraints +- Exactly one option must be selected. diff --git a/tests/run_test.py b/tests/run_test.py index 6e31f7c..6acf2fb 100644 --- a/tests/run_test.py +++ b/tests/run_test.py @@ -1,6 +1,6 @@ #!/usr/bin/env python3 """ -Unified Test Runner for MCP Solvers (MiniZinc, PySAT, Z3) +Unified Test Runner for MCP Solvers (MiniZinc, PySAT, Z3, ASP) Runs problems through the appropriate test-client. """ @@ -31,6 +31,7 @@ # Import test configuration constants (excluding prompt files) from tests.test_config import ( + ASP_PROBLEMS_DIR, DEFAULT_TIMEOUT, MAXSAT_PROBLEMS_DIR, MCP_CLIENT_DIR, @@ -259,6 +260,14 @@ def track_tool_usage(line): "results_subdir": "maxsat", "needs_server_arg": True, }, + "asp": { + "solver_mode": "asp", + "problems_dir": ASP_PROBLEMS_DIR, + "command_template": 'cd {mcp_client_dir} && uv run test-client --query {query_path} --server "uv run mcp-solver-asp"', + "model_ext": ".lp", + "results_subdir": "asp", + "needs_server_arg": True, + }, } @@ -696,7 +705,7 @@ def main(): parser.add_argument( "solver", choices=SOLVER_CONFIGS.keys(), - help="Specify the solver type to test (mzn, pysat, z3)", + help="Specify the solver type to test (mzn, pysat, z3, asp)", ) parser.add_argument("--problem", help="Path to specific problem file (.md)") parser.add_argument( diff --git a/tests/test_config.py b/tests/test_config.py index 2d20b42..a454b8b 100644 --- a/tests/test_config.py +++ b/tests/test_config.py @@ -19,6 +19,7 @@ PYSAT_PROBLEMS_DIR = os.path.join(PROBLEMS_DIR, "pysat") Z3_PROBLEMS_DIR = os.path.join(PROBLEMS_DIR, "z3") MAXSAT_PROBLEMS_DIR = os.path.join(PROBLEMS_DIR, "maxsat") +ASP_PROBLEMS_DIR = os.path.join(PROBLEMS_DIR, "asp") RESULTS_DIR = os.path.join(ROOT_DIR, "test_results")