tools

feasibility_checker

heuristic_feasibility_check(constraints, variable_name, variable_type, variable_bounds, samples=10000)

A tool for checking feasibility of the constraints.

Parameters:

Name	Type	Description	Default
constraints	Annotated[List[str], "List of strings like 'x0+x1<=5'"]	list of strings like 'x0 + x1 <= 5', etc.	required
variable_name	Annotated[List[str], "List of strings like 'x0', 'x1', etc."]	list of strings containing variable names used in constraint expressions.	required
variable_type	Annotated[List[str], "List of strings like 'real', 'integer', 'boolean', etc."]	list of strings like 'real', 'integer', 'boolean', etc.	required
variable_bounds	Annotated[List[List[float]], "List of (lower bound, upper bound) tuples for x0, x1, ...'"]	list of (lower, upper) tuples for x0, x1, etc.	required
samples	Annotated[int, 'Number of random sample. Default 10000']	number of random samples, default value 10000	10000

Returns:

Type	Description
Tuple[str]	A string indicating whether a feasible solution was found.

Source code in src/ursa/tools/feasibility_checker.py

@tool(parse_docstring=True)
def heuristic_feasibility_check(
    constraints: Annotated[List[str], "List of strings like 'x0+x1<=5'"],
    variable_name: Annotated[
        List[str], "List of strings like 'x0', 'x1', etc."
    ],
    variable_type: Annotated[
        List[str], "List of strings like 'real', 'integer', 'boolean', etc."
    ],
    variable_bounds: Annotated[
        List[List[float]],
        "List of (lower bound, upper bound) tuples for x0, x1, ...'",
    ],
    samples: Annotated[int, "Number of random sample. Default 10000"] = 10000,
) -> Tuple[str]:
    """
    A tool for checking feasibility of the constraints.

    Args:
        constraints: list of strings like 'x0 + x1 <= 5', etc.
        variable_name: list of strings containing variable names used in constraint expressions.
        variable_type: list of strings like 'real', 'integer', 'boolean', etc.
        variable_bounds: list of (lower, upper) tuples for x0, x1, etc.
        samples: number of random samples, default value 10000

    Returns:
        A string indicating whether a feasible solution was found.
    """

    symbols = sp.symbols(variable_name)

    # Build a dict mapping each name to its Symbol, for parsing
    locals_map = {name: sym for name, sym in zip(variable_name, symbols)}

    # Parse constraints into Sympy Boolean expressions
    parsed_constraints = []
    try:
        for expr in constraints:
            parsed = parse_expr(
                expr,
                local_dict=locals_map,
                transformations=standard_transformations,
                evaluate=False,
            )
            parsed_constraints.append(parsed)
    except Exception as e:
        return f"Error parsing constraints: {e}"

    # Sampling loop
    n = len(parsed_constraints)
    funcs = [
        sp.lambdify(symbols, c, modules=["math", "numpy"])
        for c in parsed_constraints
    ]
    constraint_satisfied = np.zeros(n, dtype=int)
    for _ in range(samples):
        point = {}
        for i, sym in enumerate(symbols):
            typ = variable_type[i].lower()
            low, high = variable_bounds[i]
            if typ == "integer":
                value = random.randint(int(low), int(high))
            elif typ in ("real", "continuous"):
                value = random.uniform(low, high)
            elif typ in ("boolean", "logical"):
                value = random.choice([False, True])
            else:
                raise ValueError(
                    f"Unknown type {variable_type[i]} for variable {variable_name[i]}"
                )
            point[sym] = value

        # Evaluate all constraints at this point
        try:
            vals = [point[s] for s in symbols]
            cons_satisfaction = [
                bool(np.asarray(f(*vals)).all()) for f in funcs
            ]
            if all(cons_satisfaction):
                # Found a feasible point
                readable = {str(k): round(v, 3) for k, v in point.items()}
                return f"Feasible solution found: {readable}"
            else:
                constraint_satisfied += np.array(cons_satisfaction)
        except Exception as e:
            return f"Error evaluating constraint at point {point}: {e}"

    rates = constraint_satisfied / samples  # fraction satisfied per constraint
    order = np.argsort(rates)  # lowest (most violated) first

    lines = []
    for rank, idx in enumerate(order, start=1):
        expr_text = constraints[
            idx
        ]  # use the original string; easier to read than str(sympy_expr)
        sat = constraint_satisfied[idx]
        lines.append(
            f"[C{idx + 1}] {expr_text} — satisfied {sat:,}/{samples:,} ({sat / samples:.1%}), "
            f"violated {1 - sat / samples:.1%}"
        )

    return (
        f"No feasible solution found after {samples:,} samples. Most violated constraints (low→high satisfaction):\n "
        + "\n  ".join(lines)
    )

feasibility_tools

Unified feasibility checker with heuristic pre-check and exact auto-routing.

Backends (imported lazily and used only if available): - PySMT (cvc5/msat/yices/z3) for SMT-style logic, disjunctions, and nonlinear constructs. - OR-Tools CP-SAT for strictly linear integer/boolean instances with integer coefficients. - OR-Tools CBC (pywraplp) for linear MILP/LP (mixed real + integer, or pure LP). - SciPy HiGHS (linprog) for pure continuous LP feasibility.

Install any subset you need

pip install pysmt && pysmt-install --cvc5 # or --z3/--msat/--yices pip install ortools pip install scipy pip install numpy

This file exposes a single LangChain tool: feasibility_check_auto.

feasibility_check_auto(constraints, variable_name, variable_type, variable_bounds, prefer_smt_solver='cvc5', heuristic_enabled=True, heuristic_first=True, heuristic_samples=2000, heuristic_seed=None, heuristic_unbounded_radius_real=1000.0, heuristic_unbounded_radius_int=10 ** 6, numeric_tolerance=1e-08)

Unified feasibility checker with heuristic pre-check and exact auto-routing.

Performs an optional randomized feasibility search. If no witness is found (or the heuristic is disabled), the function auto-routes to an exact backend based on the detected problem structure (PySMT for SMT/logic/nonlinear, OR-Tools CP-SAT for linear integer/boolean, OR-Tools CBC for MILP/LP, or SciPy HiGHS for pure LP).

Parameters:

Name	Type	Description	Default
constraints	Annotated[List[str], "Constraint strings like 'x0 + 2*x1 <= 5' or '(x0<=3) | (x1>=2)'"]	Constraint strings such as "x0 + 2*x1 <= 5" or "(x0<=3) | (x1>=2)".	required
variable_name	Annotated[List[str], ['x0', 'x1', ...]]	Variable names, e.g., ["x0", "x1"].	required
variable_type	Annotated[List[str], ['real' | 'integer' | 'boolean', ...]]	Variable types aligned with variable_name. Each must be one of "real", "integer", or "boolean".	required
variable_bounds	Annotated[List[List[Optional[float]]], '[(low, high), ...] (use None for unbounded)']	Per-variable [low, high] bounds aligned with variable_name. Use None to denote an unbounded side.	required
prefer_smt_solver	Annotated[str, "SMT backend if needed: 'cvc5'|'msat'|'yices'|'z3'"]	SMT backend name used by PySMT ("cvc5", "msat", "yices", or "z3").	'cvc5'
heuristic_enabled	Annotated[bool, 'Run a fast randomized search first?']	Whether to run the heuristic sampler.	True
heuristic_first	Annotated[bool, 'Try heuristic before exact routing']	If True, run the heuristic before exact routing; if False, run it after.	True
heuristic_samples	Annotated[int, 'Samples for heuristic search']	Number of heuristic samples.	2000
heuristic_seed	Annotated[Optional[int], 'Seed for reproducibility']	Random seed for reproducibility.	None
heuristic_unbounded_radius_real	Annotated[float, 'Sampling range for unbounded real vars']	Sampling radius for unbounded real variables.	1000.0
heuristic_unbounded_radius_int	Annotated[int, 'Sampling range for unbounded integer vars']	Sampling radius for unbounded integer variables.	10 ** 6
numeric_tolerance	Annotated[float, 'Tolerance for relational checks (Eq/Lt/Le/etc.)']	Tolerance used in relational checks (e.g., Eq, Lt, Le).	1e-08

Returns:

Type	Description
str	A message indicating the chosen backend and the feasibility result. On success,
str	includes an example model (assignment). On infeasibility, includes a short
str	diagnostic or solver status.

Raises:

Type	Description
ValueError	If constraints cannot be parsed or an unsupported variable type is provided.

Source code in src/ursa/tools/feasibility_tools.py

@tool(parse_docstring=True)
def feasibility_check_auto(
    constraints: Annotated[
        List[str],
        "Constraint strings like 'x0 + 2*x1 <= 5' or '(x0<=3) | (x1>=2)'",
    ],
    variable_name: Annotated[List[str], "['x0','x1',...]"],
    variable_type: Annotated[List[str], "['real'|'integer'|'boolean', ...]"],
    variable_bounds: Annotated[
        List[List[Optional[float]]],
        "[(low, high), ...] (use None for unbounded)",
    ],
    prefer_smt_solver: Annotated[
        str, "SMT backend if needed: 'cvc5'|'msat'|'yices'|'z3'"
    ] = "cvc5",
    heuristic_enabled: Annotated[
        bool, "Run a fast randomized search first?"
    ] = True,
    heuristic_first: Annotated[
        bool, "Try heuristic before exact routing"
    ] = True,
    heuristic_samples: Annotated[int, "Samples for heuristic search"] = 2000,
    heuristic_seed: Annotated[Optional[int], "Seed for reproducibility"] = None,
    heuristic_unbounded_radius_real: Annotated[
        float, "Sampling range for unbounded real vars"
    ] = 1e3,
    heuristic_unbounded_radius_int: Annotated[
        int, "Sampling range for unbounded integer vars"
    ] = 10**6,
    numeric_tolerance: Annotated[
        float, "Tolerance for relational checks (Eq/Lt/Le/etc.)"
    ] = 1e-8,
) -> str:
    """Unified feasibility checker with heuristic pre-check and exact auto-routing.

    Performs an optional randomized feasibility search. If no witness is found (or the
    heuristic is disabled), the function auto-routes to an exact backend based on the
    detected problem structure (PySMT for SMT/logic/nonlinear, OR-Tools CP-SAT for
    linear integer/boolean, OR-Tools CBC for MILP/LP, or SciPy HiGHS for pure LP).

    Args:
        constraints: Constraint strings such as "x0 + 2*x1 <= 5" or "(x0<=3) | (x1>=2)".
        variable_name: Variable names, e.g., ["x0", "x1"].
        variable_type: Variable types aligned with `variable_name`. Each must be one of
            "real", "integer", or "boolean".
        variable_bounds: Per-variable [low, high] bounds aligned with `variable_name`.
            Use None to denote an unbounded side.
        prefer_smt_solver: SMT backend name used by PySMT ("cvc5", "msat", "yices", or "z3").
        heuristic_enabled: Whether to run the heuristic sampler.
        heuristic_first: If True, run the heuristic before exact routing; if False, run it after.
        heuristic_samples: Number of heuristic samples.
        heuristic_seed: Random seed for reproducibility.
        heuristic_unbounded_radius_real: Sampling radius for unbounded real variables.
        heuristic_unbounded_radius_int: Sampling radius for unbounded integer variables.
        numeric_tolerance: Tolerance used in relational checks (e.g., Eq, Lt, Le).

    Returns:
        A message indicating the chosen backend and the feasibility result. On success,
        includes an example model (assignment). On infeasibility, includes a short
        diagnostic or solver status.

    Raises:
        ValueError: If constraints cannot be parsed or an unsupported variable type is provided.
    """
    # 1) Parse
    try:
        symbols, sympy_cons = _parse_constraints(constraints, variable_name)
    except Exception as e:
        return f"Parse error: {e}"

    # 2) Heuristic (optional)
    if heuristic_enabled and heuristic_first:
        try:
            h_model = _heuristic_feasible(
                sympy_cons,
                symbols,
                variable_name,
                variable_type,
                variable_bounds,
                samples=heuristic_samples,
                seed=heuristic_seed,
                tol=numeric_tolerance,
                unbounded_radius_real=heuristic_unbounded_radius_real,
                unbounded_radius_int=heuristic_unbounded_radius_int,
            )
            if h_model is not None:
                return f"[backend=heuristic] Feasible (sampled witness). Example solution: {h_model}"
        except Exception:
            # Ignore heuristic issues and continue to exact route
            pass

    # 3) Classify & route
    info = _classify(sympy_cons, symbols, variable_type)

    # SMT needed or nonlinear / non-conj
    if info["requires_smt"] or not info["all_linear"]:
        res = _solve_with_pysmt(
            sympy_cons,
            symbols,
            variable_name,
            variable_type,
            variable_bounds,
            solver_name=prefer_smt_solver,
        )
        # Optional heuristic after exact if requested
        if (
            heuristic_enabled
            and not heuristic_first
            and any(
                kw in res.lower()
                for kw in ("unknown", "not installed", "unsupported", "failed")
            )
        ):
            h_model = _heuristic_feasible(
                sympy_cons,
                symbols,
                variable_name,
                variable_type,
                variable_bounds,
                samples=heuristic_samples,
                seed=heuristic_seed,
                tol=numeric_tolerance,
                unbounded_radius_real=heuristic_unbounded_radius_real,
                unbounded_radius_int=heuristic_unbounded_radius_int,
            )
            if h_model is not None:
                return f"[backend=heuristic] Feasible (sampled witness). Example solution: {h_model}"
        return res

    # Linear-only path: collect atomic conjuncts
    conjuncts: List[sp.Expr] = []
    for c in sympy_cons:
        atoms, _ = _flatten_conjunction(c)
        conjuncts.extend(atoms)

    has_int, has_bool, has_real = (
        info["has_int"],
        info["has_bool"],
        info["has_real"],
    )

    # Pure LP (continuous only)
    if not has_int and not has_bool and has_real:
        res = _solve_with_highs_lp(
            conjuncts, symbols, variable_name, variable_bounds
        )
        if "not installed" in res.lower():
            res = _solve_with_cbc_milp(
                conjuncts,
                symbols,
                variable_name,
                variable_type,
                variable_bounds,
            )
        if (
            heuristic_enabled
            and not heuristic_first
            and any(kw in res.lower() for kw in ("failed", "unknown"))
        ):
            h_model = _heuristic_feasible(
                sympy_cons,
                symbols,
                variable_name,
                variable_type,
                variable_bounds,
                samples=heuristic_samples,
                seed=heuristic_seed,
                tol=numeric_tolerance,
                unbounded_radius_real=heuristic_unbounded_radius_real,
                unbounded_radius_int=heuristic_unbounded_radius_int,
            )
            if h_model is not None:
                return f"[backend=heuristic] Feasible (sampled witness). Example solution: {h_model}"
        return res

    # All integer/boolean → CP-SAT first (if integer coefficients), else CBC MILP
    if (has_int or has_bool) and not has_real:
        res = _solve_with_cpsat_integer_boolean(
            conjuncts, symbols, variable_name, variable_type, variable_bounds
        )
        if (
            any(
                kw in res
                for kw in (
                    "routing to MILP/LP",
                    "handles linear conjunctions only",
                )
            )
            or "not installed" in res.lower()
        ):
            res = _solve_with_cbc_milp(
                conjuncts,
                symbols,
                variable_name,
                variable_type,
                variable_bounds,
            )
        return res

    # Mixed reals + integers → CBC MILP
    res = _solve_with_cbc_milp(
        conjuncts, symbols, variable_name, variable_type, variable_bounds
    )

    # Optional heuristic after exact (if backend missing/failing)
    if (
        heuristic_enabled
        and not heuristic_first
        and any(
            kw in res.lower() for kw in ("not installed", "failed", "status:")
        )
    ):
        h_model = _heuristic_feasible(
            sympy_cons,
            symbols,
            variable_name,
            variable_type,
            variable_bounds,
            samples=heuristic_samples,
            seed=heuristic_seed,
            tol=numeric_tolerance,
            unbounded_radius_real=heuristic_unbounded_radius_real,
            unbounded_radius_int=heuristic_unbounded_radius_int,
        )
        if h_model is not None:
            return f"[backend=heuristic] Feasible (sampled witness). Example solution: {h_model}"

    return res

run_command

run_cmd(query, workspace_dir)

Run command from commandline in the directory workspace_dir

Source code in src/ursa/tools/run_command.py

@tool
def run_cmd(query: str, workspace_dir: str) -> str:
    """Run command from commandline in the directory workspace_dir"""

    print("RUNNING: ", query)
    print(
        "DANGER DANGER DANGER - THERE IS NO GUARDRAIL FOR SAFETY IN THIS IMPLEMENTATION - DANGER DANGER DANGER"
    )
    process = subprocess.Popen(
        query.split(" "),
        stdout=subprocess.PIPE,
        stderr=subprocess.PIPE,
        text=True,
        cwd=workspace_dir,
    )

    stdout, stderr = process.communicate(timeout=600)

    print("STDOUT: ", stdout)
    print("STDERR: ", stderr)

    return f"STDOUT: {stdout} and STDERR: {stderr}"

write_code

write_python(code, filename, workspace_dir)

Writes code to a file in the given workspace.

Parameters:

Name	Type	Description	Default
code	str	The code to write	required
filename	str	the filename to write	required

Returns:

Type	Description
str	File writing status: string

Source code in src/ursa/tools/write_code.py

@tool
def write_python(code: str, filename: str, workspace_dir: str) -> str:
    """
    Writes code to a file in the given workspace.

    Args:
        code: The code to write
        filename: the filename to write

    Returns:
        File writing status: string
    """
    print("Writing filename ", filename)
    try:
        # Extract code if wrapped in markdown code blocks
        if "```" in code:
            code_parts = code.split("```")
            if len(code_parts) >= 3:
                # Extract the actual code
                if "\n" in code_parts[1]:
                    code = "\n".join(code_parts[1].strip().split("\n")[1:])
                else:
                    code = code_parts[2].strip()

        # Write code to a file
        code_file = os.path.join(workspace_dir, filename)

        with open(code_file, "w") as f:
            f.write(code)
        print(f"Written code to file: {code_file}")

        return f"File {filename} written successfully."

    except Exception as e:
        print(f"Error generating code: {str(e)}")
        # Return minimal code that prints the error
        return f"Failed to write {filename} successfully."