Z3
Public Member Functions | Static Public Member Functions | Data Fields
Z3_lbool Enum Reference

Public Member Functions

 Z3_lbool (int v)
 
final int toInt ()
 

Static Public Member Functions

static final Z3_lbool fromInt (int v)
 

Data Fields

 Z3_L_TRUE =(1)
 
 Z3_L_UNDEF =(0)
 
 Z3_L_FALSE =(-1)
 

Detailed Description

Z3_lbool

Definition at line 10 of file Z3_lbool.java.

Constructor & Destructor Documentation

Z3_lbool ( int  v)
inline

Definition at line 17 of file Z3_lbool.java.

17  {
18  this.intValue = v;
19  }

Member Function Documentation

static final Z3_lbool fromInt ( int  v)
inlinestatic

Definition at line 21 of file Z3_lbool.java.

Referenced by Optimize.Check(), Solver.check(), InterpolationContext.ComputeInterpolant(), Expr.getBoolValue(), and Fixedpoint.query().

21  {
22  for (Z3_lbool k: values())
23  if (k.intValue == v) return k;
24  return values()[0];
25  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:143
final int toInt ( )
inline

Definition at line 27 of file Z3_lbool.java.

27 { return this.intValue; }

Field Documentation

Z3_L_FALSE =(-1)

Definition at line 13 of file Z3_lbool.java.

Referenced by InterpolationContext.ComputeInterpolant().

Z3_L_TRUE =(1)

Definition at line 11 of file Z3_lbool.java.

Referenced by InterpolationContext.ComputeInterpolant().

Z3_L_UNDEF =(0)

Definition at line 12 of file Z3_lbool.java.