fmrisc.ProofNavigator.Proving.CVCL

Class InvalidAnswerCVCL

java.lang.Object

fmrisc.ProofNavigator.Proving.AnswerBase

fmrisc.ProofNavigator.Proving.InvalidAnswer

fmrisc.ProofNavigator.Proving.CVCL.InvalidAnswerCVCL

All Implemented Interfaces:

Answer

public final class InvalidAnswerCVCL
extends InvalidAnswer

Answer that formula is invalid.

Constructor Summary

Constructors

Constructor and Description
InvalidAnswerCVCL(CVCL cvcl, java.lang.String justification) Create answer that formula is valid with denoted justification.

Method Summary

Modifier and Type	Method and Description
Expression[]	getCounterExample() Interpret justification as a counterexample.

Methods inherited from class fmrisc.ProofNavigator.Proving.AnswerBase

getJustification

Methods inherited from class java.lang.Object

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

Constructor Detail

InvalidAnswerCVCL

public InvalidAnswerCVCL(CVCL cvcl,
                         java.lang.String justification)

Create answer that formula is valid with denoted justification.

Parameters:

cvcl - CVCL instance that gave the answer

justification - why is formula invalid (may be null)

Method Detail

getCounterExample

public Expression[] getCounterExample()

Interpret justification as a counterexample.

Overrides:

getCounterExample in class InvalidAnswer

Returns:

sequence of formulas whose conjunction represents a refutation (null, if answer cannot be interpreted in this way)