fmrisc.ProgramExplorer.Tasks

Class FlattenDeclarations

java.lang.Object

fmrisc.ProgramExplorer.Tasks.FlattenDeclarations

public final class FlattenDeclarations
extends java.lang.Object

Flatten nested declarations of a task.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	FlattenDeclarations.Result The flattening result.

Method Summary

Modifier and Type	Method and Description
static FlattenDeclarations.Result	flatten(java.util.Vector<TheorySymbol> theories, Declaration[][] decls, Formula goal, TheorySymbol theory) Flatten a task with nested declarations.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

flatten

public static FlattenDeclarations.Result flatten(java.util.Vector<TheorySymbol> theories,
                                                 Declaration[][] decls,
                                                 Formula goal,
                                                 TheorySymbol theory)

Flatten a task with nested declarations.

Parameters:

theories - the theories that are referenced in dependence order.

decls - the nested declarations.

goal - the goal.

theory - the theory of the goal (may be null)

Returns:

a pair of translated declarations and goals.