Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Static Public Member Functions | Data Fields
Status Enum Reference

Public Member Functions

 Status (int v)
final int toInt ()

Static Public Member Functions

static final Status fromInt (int v)

Data Fields

 UNSATISFIABLE = (-1)
 UNKNOWN = (0)
 SATISFIABLE = (1)

Detailed Description

Status values.

Definition at line 23 of file Status.java.


Constructor & Destructor Documentation

Status ( int  v) [inline]

Definition at line 36 of file Status.java.

    {
        this.intValue = v;
    }

Member Function Documentation

static final Status fromInt ( int  v) [inline, static]

Definition at line 41 of file Status.java.

    {
        for (Status k : values())
            if (k.intValue == v)
                return k;
        return values()[0];
    }
final int toInt ( ) [inline]

Definition at line 49 of file Status.java.

    {
        return this.intValue;
    }

Field Documentation

SATISFIABLE = (1)

Definition at line 32 of file Status.java.

Referenced by Solver.check(), and Fixedpoint.query().

UNKNOWN = (0)

Definition at line 29 of file Status.java.

Referenced by Solver.check(), and Fixedpoint.query().

UNSATISFIABLE = (-1)

Definition at line 26 of file Status.java.

Referenced by Solver.check(), and Fixedpoint.query().

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines