forge.solve
Class ForgeSolution

java.lang.Object
  forge.solve.ForgeSolution

public final class ForgeSolution
extends java.lang.Object

A solution that includes coverage information when it is unsatisfiable.

Author:

Greg Dennis (gdennis@mit.edu)

Method Summary

ForgeCFG	code()
Coverage	coverage() Return the statements covered by the analysis if unsatisfiable; otherwise null.
java.lang.Object	kkFormula() Returns set of Kodkod formula solved.
ForgeProgram	program()
boolean	satisfiable() Returns true iff the solver found a satisfying trace.
ForgeCFG.Spec	spec()
java.lang.String	toString()
Trace	trace() Returns the satisfying trace if unsatisfiable; otherwise null.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Method Detail

program

public ForgeProgram program()

code

public ForgeCFG code()

spec

public ForgeCFG.Spec spec()

kkFormula

public java.lang.Object kkFormula()

Returns set of Kodkod formula solved.

satisfiable

public boolean satisfiable()

Returns true iff the solver found a satisfying trace.

trace

public Trace trace()

Returns the satisfying trace if unsatisfiable; otherwise null.

coverage

public Coverage coverage()

Return the statements covered by the analysis if unsatisfiable; otherwise null.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object