fmrisc.ProofNavigator.Proving

Class ProverReasoning

java.lang.Object

fmrisc.ProofNavigator.Proving.ProverReasoning

public final class ProverReasoning
extends java.lang.Object

Reasoning with the help of an external prover.

Constructor Summary

Constructors

Constructor and Description
ProverReasoning()

Method Summary

Modifier and Type	Method and Description
static boolean	simplify(ProofState state, boolean hard, boolean generate) Simplify the current proof state and potentially close it.
static boolean	simplify(ProofState state, Formula formula, boolean hard) Simplify a single formula in some proof state.

Methods inherited from class java.lang.Object

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

Constructor Detail

ProverReasoning

public ProverReasoning()

Method Detail

simplify

public static boolean simplify(ProofState state,
                               Formula formula,
                               boolean hard)

Simplify a single formula in some proof state.

Parameters:

state - a proof state.

formula - a formula of this proof state to be simplified.

hard - true iff simplification is attempted hard.

Returns:

true iff everything went okay.

simplify

public static boolean simplify(ProofState state,
                               boolean hard,
                               boolean generate)

Simplify the current proof state and potentially close it.

Parameters:

state - the proof state.

hard - true if hard (and time-consuming) simplification is tried.

generate - true if counterexample is to be generated, if state could not be closed.

Returns:

true iff everything went okay.