A small utility to strip leading/trailing whitespace around a parser

Parse a search configuration from a string. This will parse the new options from the string and update the search configuration.

Is the query empty, i.e. does it have no goals left to prove?

Get the variables used in the environment.

Borrow the name of the symbol as a string

Merge the goals of this query with the goals of another query, returning a new query with all the goals

Substitute all occurrences of variables in this term with the given bindings. This will modify this term in place, replacing all occurrences of varia

Get an iterator over all the goals in the query

Attempt to find a solution for the query using the search configuration. If a solution is found, it will be returned. If no solution is found, an err

Apply all the rules in the environment to all the goals query, adding the new goals to the query. If the search configuration requires a head match,

Find solutions for the query using the given search configuration.

Return a new, reduced term. This will apply the environment's variable bindings to this term, performing variable substitution and simplification. C

Remove all the complemented goals that cannot be simplified by any of the rules in the environment. These are inherently negative goals that cannot b

Add a positive goal to the query. This means that the goal must be proven true for the query to be true.

Get a variable from the environment.

Is this query a ground truth query, meaning it is a query that is always true? A query is ground truth if all the goals are either true or the comple

Prune the environment, removing unused variables. It takes the full, original query supplied by the user, and the current query that is being searche

Clear the environment, removing all rules and variable bindings.

Substitute all the variables in the rule with the given bindings.

Get the variable bindings for the environment.

Supply a new search configuration for the environment.

Apply a rule to a term in an environment. The `original_term` is the term that the rule is being applied to. The query is passed to allow the rule t

Apply a rule to a query, adding the new goals to the query. If the search configuration requires a head match, the rule will be applied to the first

Check if the search configuration allows pruning.

Evaluate a string of rules, queries, and search configuration settings in an environment with a given solver

Does this term contain an application of the given application term? If the term contains an application of a function with the same name as the give

Does the query contain any complements?

Reduce this term in place. This will apply the environment's variable bindings to this term, performing variable substitution and simplification. Co

Remove a goal from the query

Set a variable in the environment.

Convert the bindings in this environment to a solution. This will take all the variables in the query, and return the reduced bindings for those vari

Apply a function that inspects this term, and all subterms recursively. When the function returns false, the traversal stops. When the function retur

Unify this term with another term. This will attempt to bind the variable terms in this term to the corresponding terms in the other term. If the st

Create a new search configuration with the given depth limit.

Create a new search configuration with the given require head match setting.

Create a new search configuration with the given maximum search depth.

Apply a rule to a goal term, adding the new goals to the query.

Get mutable references to the arguments of the application term as an iterator

Check if the search configuration allows deeper searches.

Check if the search configuration allows wider searches.

Does this query contain contradictory goals? If false is in the query, then the query is contradictory. If a goal is in the query, and its complement