ExMaude.Result.Solution (ExMaude v0.2.0)

View Source

A single solution from a Maude search operation.

Each solution represents a state that matches the search pattern, along with the state number in the search graph and any variable substitutions that make the pattern match.

Structure

  • :number - The solution number (1-indexed)
  • :state_num - The state number in the search graph
  • :term - The matching term (optional)
  • :substitution - Map of variable names to their bound values

Variable Naming Conventions

Maude variables include their sort in the name for disambiguation:

VariableDescription
X:NatA natural number variable named X
S:StateA state variable named S
L:List{Nat}A list of naturals variable named L

When accessing substitutions, use the full variable name including sort:

solution.substitution["X:Nat"]  # Correct
solution.substitution["X"]      # Won't match

Substitution Format

The substitution map contains variable bindings parsed from Maude output:

Solution 1 (state 5)
X:Nat --> 42
Y:Bool --> true

Becomes:

%{"X:Nat" => "42", "Y:Bool" => "true"}

Examples

solution = %ExMaude.Result.Solution{
  number: 1,
  state_num: 5,
  substitution: %{"S:State" => "active"}
}

# Access bindings
ExMaude.Result.Solution.get_binding(solution, "S:State")  #=> "active"

# Check if has bindings
ExMaude.Result.Solution.has_bindings?(solution)  #=> true

See Also

Summary

Types

t()

Functions

get_binding(solution, var_name)

Gets a substitution value by variable name.

has_bindings?(solution)

Checks if the solution has any variable bindings.

new(number, opts \\ [])

Creates a new Solution struct.

Types

t()

@type t() :: %ExMaude.Result.Solution{
  number: pos_integer(),
  state_num: non_neg_integer() | nil,
  substitution: %{required(String.t()) => String.t()},
  term: ExMaude.Term.t() | nil
}

Functions

get_binding(solution, var_name)

@spec get_binding(t(), String.t()) :: String.t() | nil

Gets a substitution value by variable name.

Examples

solution = ExMaude.Result.Solution.new(1, substitution: %{"X:Nat" => "42"})
ExMaude.Result.Solution.get_binding(solution, "X:Nat")  #=> "42"
ExMaude.Result.Solution.get_binding(solution, "Y:Nat")  #=> nil

has_bindings?(solution)

@spec has_bindings?(t()) :: boolean()

Checks if the solution has any variable bindings.

new(number, opts \\ [])

@spec new(
  pos_integer(),
  keyword()
) :: t()

Creates a new Solution struct.

Examples

solution = ExMaude.Result.Solution.new(1, state_num: 5, substitution: %{"X" => "42"})