Inheritance diagram for RealSort:

Package Functions
	RealSort (Context ctx, long obj) throws Z3Exception
	RealSort (Context ctx) throws Z3Exception

Detailed Description

A real sort

Definition at line 23 of file RealSort.java.

Constructor & Destructor Documentation

RealSort	(	Context	ctx,
		long	obj
	)		throws Z3Exception `[inline, package]`

Definition at line 25 of file RealSort.java.

    {
        super(ctx, obj);
    }

RealSort ( Context ctx ) throws Z3Exception [inline, package]

Definition at line 30 of file RealSort.java.

    {
        super(ctx, Native.mkRealSort(ctx.nCtx()));
    }