ExMaude.Result.Search (ExMaude v0.2.0)

View Source

Result of a Maude search operation.

A search result contains all solutions found, along with statistics about the search process like states explored and execution time.

Structure

  • :solutions - List of ExMaude.Result.Solution structs
  • :states_explored - Total number of states visited during search
  • :time_ms - Time taken in milliseconds

Search Arrow Types

Maude supports different search strategies via arrow operators:

ArrowDescription
=>1One-step rewriting (exactly one rule application)
=>+One or more steps (at least one rule application)
=>*Zero or more steps (default, includes initial state)
=>!Normal form (only states with no applicable rules)

Maude Output Format

The parser handles Maude's search output format:

search [1, 100] in MOD : init =>* goal .

Solution 1 (state 5)
states: 42  rewrites: 156 in 10ms cpu
X:Nat --> 42
Y:Bool --> true

No more solutions.

State Space Concepts

  • State number - Unique identifier for each state in the search graph
  • Solution number - 1-indexed order in which solutions were found
  • Substitution - Variable bindings that make the pattern match

Examples

{:ok, output} = ExMaude.execute("search [3] in MOD : init =>* goal .")
{:ok, result} = ExMaude.Result.Search.parse(output)
length(result.solutions)  #=> 3
result.states_explored    #=> 42

ExMaude.Result.Search.found?(result)  #=> true

first = ExMaude.Result.Search.first(result)
first.substitution["X:Nat"]  #=> "42"

See Also

Summary

Types

t()

Functions

all_bindings(search, var_name)

Returns all variable bindings from all solutions.

first(search)

Returns the first solution, or nil if none found.

found?(search)

Checks if any solutions were found.

new(solutions, opts \\ [])

Creates a new Search result.

parse(output)

Parses Maude search output into a Search result.

solution_count(search)

Returns the number of solutions found.

Types

t()

@type t() :: %ExMaude.Result.Search{
  solutions: [ExMaude.Result.Solution.t()],
  states_explored: non_neg_integer() | nil,
  time_ms: non_neg_integer() | nil
}

Functions

all_bindings(search, var_name)

@spec all_bindings(t(), String.t()) :: [String.t()]

Returns all variable bindings from all solutions.

Useful when you want to see all possible values for a variable across all solutions.

Examples

result = %ExMaude.Result.Search{solutions: [
  %Solution{substitution: %{"X" => "1"}},
  %Solution{substitution: %{"X" => "2"}}
]}
ExMaude.Result.Search.all_bindings(result, "X")  #=> ["1", "2"]

first(search)

@spec first(t()) :: ExMaude.Result.Solution.t() | nil

Returns the first solution, or nil if none found.

found?(search)

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

Checks if any solutions were found.

new(solutions, opts \\ [])

@spec new(
  [ExMaude.Result.Solution.t()],
  keyword()
) :: t()

Creates a new Search result.

Examples

solutions = [ExMaude.Result.Solution.new(1, state_num: 5)]
result = ExMaude.Result.Search.new(solutions, states_explored: 10)

parse(output)

@spec parse(String.t()) :: {:ok, t()}

Parses Maude search output into a Search result.

Uses ExMaude.Parser.parse_search_results/1 to extract solutions, then enriches with statistics.

solution_count(search)

@spec solution_count(t()) :: non_neg_integer()

Returns the number of solutions found.