fmrisc.ProgramExplorer.Proving

Class ProofNavigator

java.lang.Object

fmrisc.ProgramExplorer.Proving.ProofNavigator

public final class ProofNavigator
extends java.lang.Object

Translate theories into the RISC ProofNavigator.

Method Summary

Modifier and Type	Method and Description
static ProofNavigatorProblem	translate(ClassicalProblem task, java.io.File dir, ErrorStream out) Translate classical problem to RISC ProofNavigator Problem
ValueDeclaration[]	translateValueDefs(ValueDefinition[] defs) Translate value definitions.

Methods inherited from class java.lang.Object

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

Method Detail

translate

public static ProofNavigatorProblem translate(ClassicalProblem task,
                                              java.io.File dir,
                                              ErrorStream out)

Translate classical problem to RISC ProofNavigator Problem

Parameters:

task - the problem to be translated.

dir - the directory to which information may be written

out - stream for printing messages

Returns:

the translation.

translateValueDefs

public ValueDeclaration[] translateValueDefs(ValueDefinition[] defs)

Translate value definitions.

Parameters:

defs - the value definitions.

Returns:

the translation