|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
public interface Prover
Method Summary | |
---|---|
boolean |
abort()
Abort current prover activity. |
void |
addDeclaration(Declaration decl)
add declaration |
void |
assertAxiom(Expression axiom)
assert axiom about previously asserted declarations. |
void |
assertFormula(Expression formula)
assert truth of formula. |
void |
generateCounterExamples(boolean generate)
generate counterexamples, if possible. |
java.lang.String |
getError()
error message, if last command signalled a problem |
boolean |
isOkay()
true iff prover is okay after creation |
void |
popContext()
End subcontext for formula assertions. |
void |
pushContext()
Start a new subcontext for formula assertions. |
Answer |
queryFormula(Expression formula)
query truth of formula. |
Expression |
simplifyExpression(Expression exp)
simplify expression |
void |
terminate()
Terminate prover instance. |
void |
tryHard(boolean hard)
Try hard to simplify (potentially timeconsuming). |
Method Detail |
---|
boolean isOkay()
java.lang.String getError()
void generateCounterExamples(boolean generate)
generate
- true iff counterexamples are to be generatedvoid tryHard(boolean hard)
hard
- true iff prover is to try hard.void addDeclaration(Declaration decl)
decl
- declaration that is added to prover statevoid assertAxiom(Expression axiom)
axiom
- formula whose truth is asserted;
declaration symbols must be only used in context of axiom.void pushContext()
void popContext()
void assertFormula(Expression formula)
formula
- formula whose truth is asserted.Answer queryFormula(Expression formula)
formula
- formula whose truth is queried.
Expression simplifyExpression(Expression exp)
exp
- expression to be simplified
void terminate()
boolean abort()
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |