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. it has a counterexample),
UNKNOWN otherwise (I'm not sure if this holds if an error occurs)
Note: Currently (1.12.'09) the SMT Solvers do not check if a node is FALSE.
|
Modifier and Type | Field and Description |
---|---|
private int |
id |
private static int |
idCounter |
private SMTSolverResult.ThreeValuedTruth |
isValid |
static SMTSolverResult |
NO_IDEA |
java.lang.String |
solverName
This is to identify where the result comes from.
|
Modifier | Constructor and Description |
---|---|
private |
SMTSolverResult(SMTSolverResult.ThreeValuedTruth isValid,
java.lang.String solverName) |
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
private final SMTSolverResult.ThreeValuedTruth isValid
private static int idCounter
private final int id
public final java.lang.String solverName
private SMTSolverResult(SMTSolverResult.ThreeValuedTruth isValid, 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