fmrisc.Proving
Class ProverReasoning

java.lang.Object
  fmrisc.Proving.ProverReasoning

public final class ProverReasoning
extends java.lang.Object

Reasoning with the help of an external prover.

Constructor Summary

ProverReasoning()

Method Summary

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:

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.