forge.solve
Class ForgeSolver

java.lang.Object
  forge.solve.ForgeSolver

public final class ForgeSolver
extends java.lang.Object

Binds instance literals to atoms. All bindings belong to a ConstantScene.

Author:

Greg Dennis (gdennis@mit.edu)

Constructor Summary

ForgeSolver(ForgeCFG cfg, int unrolls)
Constructs a solver for analyzing the given code, where loops and recursion are unrolled the specified number of times.

ForgeSolver(ForgeCFG code, SolveOptions options)
Constructs a solver for analyzing the given code with the given options.

Method Summary

ForgeSolution	check(ForgeCFG.Spec spec, ForgeBounds bounds) Finds a trace of the procedure within the given bounds that does not refine the given specification statement, determining coverage information in the case where no trace can be found if coverage flag is set to true.
java.util.Iterator<ForgeSolution>	checkAll(ForgeCFG.Spec spec, ForgeBounds bounds)
ForgeCFG	code()
SolveOptions	options()
ForgeProgram	program()
ForgeSolution	run(ForgeBounds bounds) Finds a trace of the procedure within the given bounds.
ForgeSolution	run(ForgeCFG.Spec spec, ForgeBounds bounds) Finds a trace of the procedure within the given bounds that refines the given specification statement, determining coverage information in the case where no trace can be found if coverage flag is set to true.
java.util.Iterator<ForgeSolution>	runAll(ForgeCFG.Spec spec, ForgeBounds bounds)

Methods inherited from class java.lang.Object

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

Constructor Detail

ForgeSolver

public ForgeSolver(ForgeCFG cfg,
                   int unrolls)

Constructs a solver for analyzing the given code, where loops and recursion are unrolled the specified number of times.

ForgeSolver

public ForgeSolver(ForgeCFG code,
                   SolveOptions options)

Constructs a solver for analyzing the given code with the given options.

Method Detail

program

public ForgeProgram program()

code

public ForgeCFG code()

options

public SolveOptions options()

run

public ForgeSolution run(ForgeBounds bounds)

Finds a trace of the procedure within the given bounds.

run

public ForgeSolution run(ForgeCFG.Spec spec,
                         ForgeBounds bounds)

Finds a trace of the procedure within the given bounds that refines the given specification statement, determining coverage information in the case where no trace can be found if coverage flag is set to true. The selected solver must have proving capability if coverage is true.

check

public ForgeSolution check(ForgeCFG.Spec spec,
                           ForgeBounds bounds)

Finds a trace of the procedure within the given bounds that does not refine the given specification statement, determining coverage information in the case where no trace can be found if coverage flag is set to true. The selected solver must have proving capability if coverage is true.

runAll

public java.util.Iterator<ForgeSolution> runAll(ForgeCFG.Spec spec,
                                                ForgeBounds bounds)

checkAll

public java.util.Iterator<ForgeSolution> checkAll(ForgeCFG.Spec spec,
                                                  ForgeBounds bounds)