public final class ProofNavigatorProblem
extends java.lang.Object
Constructor and Description |
---|
ProofNavigatorProblem(Declaration[] decls,
Expression goal,
java.io.File dir,
ErrorStream out)
Construct a proving problem from declarations and goal.
|
Modifier and Type | Method and Description |
---|---|
static void |
closeProof()
Closes any pending proof.
|
boolean |
existsProof()
Determine whether there exists a (possibly incomplete or invalidated)
proof for this problem in the store.
|
static boolean |
existsProof(java.io.File dir)
Determine whether there exists a (possibly incomplete or invalidated)
proof for this problem in the store denoted by dir.
|
Proof |
getProof()
Get current proof, possibly load it from file.
|
boolean |
isSolved()
Determine whether problem is solved.
|
boolean |
isUnsolvable()
Determine whether problem is not solvable.
|
void |
print(java.io.PrintWriter out)
Print the problem.
|
static void |
proofDone(Proof proof)
Called if a proof is completed by the ProofNavigator.
|
void |
proveAuto(Task task)
Attempt to prove goal automatically.
|
void |
proveManual(Task task)
Start/resume manual proof.
|
void |
proveStrategy(Task task)
Attempt pseudo-interactive proof with automatic strategy
|
public ProofNavigatorProblem(Declaration[] decls, Expression goal, java.io.File dir, ErrorStream out)
decls
- the declarations.goal
- the goal to be proved in the context of the declarations.out
- stream for printing messagesdir
- the directory to be used for persistent data.public static boolean existsProof(java.io.File dir)
dir
- the directory for the proof.public boolean existsProof()
public boolean isSolved()
public boolean isUnsolvable()
public void print(java.io.PrintWriter out)
out
- the stream on which the task is to be printed.public void proveAuto(Task task)
task
- the associated taskpublic void proveStrategy(Task task)
task
- the associated taskpublic void proveManual(Task task)
task
- the associated taskpublic static void proofDone(Proof proof)
proof
- the completed proof.public static void closeProof()
public Proof getProof()