RCFNum.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
public class RCFNum extends Z3Object {
    
    public RCFNum(Context ctx, String value) {
        super(ctx, Native.rcfMkRational(ctx.nCtx(), value));
    }
    
    public RCFNum(Context ctx, int value) {
        super(ctx, Native.rcfMkSmallInt(ctx.nCtx(), value));
    }
    
    RCFNum(Context ctx, long obj) {
        super(ctx, obj);
    }
    
    public static RCFNum mkPi(Context ctx) {
        return new RCFNum(ctx, Native.rcfMkPi(ctx.nCtx()));
    }
    
    public static RCFNum mkE(Context ctx) {
        return new RCFNum(ctx, Native.rcfMkE(ctx.nCtx()));
    }
    
    public static RCFNum mkInfinitesimal(Context ctx) {
        return new RCFNum(ctx, Native.rcfMkInfinitesimal(ctx.nCtx()));
    }
    
    public static RCFNum[] mkRoots(Context ctx, RCFNum[] coefficients) {
        if (coefficients == null || coefficients.length == 0) {
            throw new Z3Exception("Polynomial coefficients cannot be empty");
        }
        
        int n = coefficients.length;
        long[] a = new long[n];
        long[] roots = new long[n];
        
        for (int i = 0; i < n; i++) {
            a[i] = coefficients[i].getNativeObject();
        }
        
        int numRoots = Native.rcfMkRoots(ctx.nCtx(), n, a, roots);
        
        RCFNum[] result = new RCFNum[numRoots];
        for (int i = 0; i < numRoots; i++) {
            result[i] = new RCFNum(ctx, roots[i]);
        }
        
        return result;
    }
    
    public RCFNum add(RCFNum other) {
        checkContext(other);
        return new RCFNum(getContext(), Native.rcfAdd(getContext().nCtx(), 
                                                       getNativeObject(), 
                                                       other.getNativeObject()));
    }
    
    public RCFNum sub(RCFNum other) {
        checkContext(other);
        return new RCFNum(getContext(), Native.rcfSub(getContext().nCtx(), 
                                                       getNativeObject(), 
                                                       other.getNativeObject()));
    }
    
    public RCFNum mul(RCFNum other) {
        checkContext(other);
        return new RCFNum(getContext(), Native.rcfMul(getContext().nCtx(), 
                                                       getNativeObject(), 
                                                       other.getNativeObject()));
    }
    
    public RCFNum div(RCFNum other) {
        checkContext(other);
        return new RCFNum(getContext(), Native.rcfDiv(getContext().nCtx(), 
                                                       getNativeObject(), 
                                                       other.getNativeObject()));
    }
    
    public RCFNum neg() {
        return new RCFNum(getContext(), Native.rcfNeg(getContext().nCtx(), 
                                                       getNativeObject()));
    }
    
    public RCFNum inv() {
        return new RCFNum(getContext(), Native.rcfInv(getContext().nCtx(), 
                                                       getNativeObject()));
    }
    
    public RCFNum power(int k) {
        return new RCFNum(getContext(), Native.rcfPower(getContext().nCtx(), 
                                                         getNativeObject(), k));
    }
    
    public boolean lt(RCFNum other) {
        checkContext(other);
        return Native.rcfLt(getContext().nCtx(), getNativeObject(), 
                           other.getNativeObject());
    }
    
    public boolean gt(RCFNum other) {
        checkContext(other);
        return Native.rcfGt(getContext().nCtx(), getNativeObject(), 
                           other.getNativeObject());
    }
    
    public boolean le(RCFNum other) {
        checkContext(other);
        return Native.rcfLe(getContext().nCtx(), getNativeObject(), 
                           other.getNativeObject());
    }
    
    public boolean ge(RCFNum other) {
        checkContext(other);
        return Native.rcfGe(getContext().nCtx(), getNativeObject(), 
                           other.getNativeObject());
    }
    
    public boolean eq(RCFNum other) {
        checkContext(other);
        return Native.rcfEq(getContext().nCtx(), getNativeObject(), 
                           other.getNativeObject());
    }
    
    public boolean neq(RCFNum other) {
        checkContext(other);
        return Native.rcfNeq(getContext().nCtx(), getNativeObject(), 
                            other.getNativeObject());
    }
    
    public boolean isRational() {
        return Native.rcfIsRational(getContext().nCtx(), getNativeObject());
    }
    
    public boolean isAlgebraic() {
        return Native.rcfIsAlgebraic(getContext().nCtx(), getNativeObject());
    }
    
    public boolean isInfinitesimal() {
        return Native.rcfIsInfinitesimal(getContext().nCtx(), getNativeObject());
    }
    
    public boolean isTranscendental() {
        return Native.rcfIsTranscendental(getContext().nCtx(), getNativeObject());
    }
    
    public String toString(boolean compact) {
        return Native.rcfNumToString(getContext().nCtx(), getNativeObject(), 
                                     compact, false);
    }
    
    @Override
    public String toString() {
        return toString(false);
    }
    
    public String toDecimal(int precision) {
        return Native.rcfNumToDecimalString(getContext().nCtx(), 
                                            getNativeObject(), precision);
    }
    
    @Override
    void incRef() {
        // RCF numerals don't use standard reference counting
        // They are managed through Z3_rcf_del
    }
    
    @Override
    void addToReferenceQueue() {
        getContext().getReferenceQueue().storeReference(this, RCFNumRef::new);
    }
    
    private static class RCFNumRef extends Z3ReferenceQueue.Reference<RCFNum> {
        
        private RCFNumRef(RCFNum referent, java.lang.ref.ReferenceQueue<Z3Object> q) {
            super(referent, q);
        }
        
        @Override
        void decRef(Context ctx, long z3Obj) {
            Native.rcfDel(ctx.nCtx(), z3Obj);
        }
    }
    
    private void checkContext(RCFNum other) {
        if (getContext() != other.getContext()) {
            throw new Z3Exception("RCF numerals from different contexts");
        }
    }
}