public class SMTSolverResult
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
SMTSolverResult.ThreeValuedTruth
In the context of proving nodes/sequents these values mean the following:
TRUE iff negation of the sequent is unsatisfiable,
FALSIFIABLE iff negation of the sequent is satisfiable (i.e.
|
Modifier and Type | Field and Description |
---|---|
static SMTSolverResult |
NO_IDEA |
java.lang.String |
solverName
This is to identify where the result comes from.
|
Modifier and Type | Method and Description |
---|---|
static SMTSolverResult |
createInvalidResult(java.lang.String name) |
static SMTSolverResult |
createUnknownResult(java.lang.String name) |
static SMTSolverResult |
createValidResult(java.lang.String name) |
boolean |
equals(java.lang.Object o) |
int |
getID() |
SMTSolverResult.ThreeValuedTruth |
isValid() |
java.lang.String |
toString() |
public static final SMTSolverResult NO_IDEA
public final java.lang.String solverName
public int getID()
public static SMTSolverResult createValidResult(java.lang.String name)
public static SMTSolverResult createInvalidResult(java.lang.String name)
public static SMTSolverResult createUnknownResult(java.lang.String name)
public SMTSolverResult.ThreeValuedTruth isValid()
public java.lang.String toString()
toString
in class java.lang.Object
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.