Package org.sosy_lab.java_smt.basicimpl

Enum Class AbstractFormulaManager.SMTLIB2ProgramState

java.lang.Object

java.lang.Enum<AbstractFormulaManager.SMTLIB2ProgramState>

org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.SMTLIB2ProgramState

All Implemented Interfaces:

Serializable, Comparable<AbstractFormulaManager.SMTLIB2ProgramState>, Constable

Enclosing class:

AbstractFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>

public static enum AbstractFormulaManager.SMTLIB2ProgramState
extends Enum<AbstractFormulaManager.SMTLIB2ProgramState>

Nested Class Summary

Nested classes/interfaces inherited from class java.lang.Enum

Enum.EnumDesc<E extends Enum<E>>

Enum Constant Summary

Enum Constants

Enum Constant	Description
ASSERT_MODE	Mode entered after the initial setup is done by executing the 'set-logic' command.
EXITED_STATE	State after 'exit' has been called.
RESULT_MODE	Joined alternative to SAT_MODE and UNSAT_MODE.
SAT_MODE	Mode entered after SAT has been returned after calling 'check-set'.
START_MODE	Initial state.
UNSAT_MODE	Mode entered after UNSAT has been returned after calling 'check-set'.

Method Summary

Modifier and Type	Method	Description
static AbstractFormulaManager.SMTLIB2ProgramState	valueOf(String name)	Returns the enum constant of this class with the specified name.
static AbstractFormulaManager.SMTLIB2ProgramState[]	values()	Returns an array containing the constants of this enum class, in the order they are declared.

Methods inherited from class java.lang.Enum

clone, compareTo, describeConstable, equals, finalize, getDeclaringClass, hashCode, name, ordinal, toString, valueOf

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Enum Constant Details

START_MODE

public static final AbstractFormulaManager.SMTLIB2ProgramState START_MODE

Initial state. Can be re-entered using the 'reset' command.

ASSERT_MODE

public static final AbstractFormulaManager.SMTLIB2ProgramState ASSERT_MODE

Mode entered after the initial setup is done by executing the 'set-logic' command. In this state, formulas can be defined/asserted etc.

SAT_MODE

public static final AbstractFormulaManager.SMTLIB2ProgramState SAT_MODE

Mode entered after SAT has been returned after calling 'check-set'.

UNSAT_MODE

public static final AbstractFormulaManager.SMTLIB2ProgramState UNSAT_MODE

Mode entered after UNSAT has been returned after calling 'check-set'.

RESULT_MODE

public static final AbstractFormulaManager.SMTLIB2ProgramState RESULT_MODE

Joined alternative to SAT_MODE and UNSAT_MODE. Used if we don't solve, i.e. don't know whether we are in a SAT/UNSAT state after 'check-sat'.

EXITED_STATE

public static final AbstractFormulaManager.SMTLIB2ProgramState EXITED_STATE

State after 'exit' has been called. No operations are possible anymore and everything ends in an error.

Method Details

values

public static AbstractFormulaManager.SMTLIB2ProgramState[] values()

Returns an array containing the constants of this enum class, in the order they are declared.

Returns:

an array containing the constants of this enum class, in the order they are declared

valueOf

public static AbstractFormulaManager.SMTLIB2ProgramState valueOf(String name)

Returns the enum constant of this class with the specified name. The string must match exactly an identifier used to declare an enum constant in this class. (Extraneous whitespace characters are not permitted.)

Parameters:

name - the name of the enum constant to be returned.

Returns:

the enum constant with the specified name

Throws:

IllegalArgumentException - if this enum class has no constant with the specified name

NullPointerException - if the argument is null