public class SMTSolverResult extends 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 |
---|---|
private int |
id |
private static int |
idCounter |
private SMTSolverResult.ThreeValuedTruth |
isValid |
static SMTSolverResult |
NO_IDEA |
String |
solverName
This is to identify where the result comes from.
|
Modifier | Constructor and Description |
---|---|
private |
SMTSolverResult(SMTSolverResult.ThreeValuedTruth isValid,
String solverName) |
Modifier and Type | Method and Description |
---|---|
static SMTSolverResult |
createInvalidResult(String name) |
static SMTSolverResult |
createUnknownResult(String name) |
static SMTSolverResult |
createValidResult(String name) |
boolean |
equals(Object o) |
int |
getID() |
SMTSolverResult.ThreeValuedTruth |
isValid() |
String |
toString() |
public static final SMTSolverResult NO_IDEA
private final SMTSolverResult.ThreeValuedTruth isValid
private static int idCounter
private final int id
public final String solverName
private SMTSolverResult(SMTSolverResult.ThreeValuedTruth isValid, String solverName)
public int getID()
public static SMTSolverResult createValidResult(String name)
public static SMTSolverResult createInvalidResult(String name)
public static SMTSolverResult createUnknownResult(String name)
public SMTSolverResult.ThreeValuedTruth isValid()