RCFNum.cs

Go to the documentation of this file.

/*++
Copyright (c) 2024 Microsoft Corporation
 
Module Name:
 
    RCFNum.cs
 
Abstract:
 
    Z3 Managed API: Real Closed Field (RCF) Numerals
 
Author:
 
    GitHub Copilot 2024-01-12
 
Notes:
    
--*/
using System.Diagnostics;
using System;
 
namespace Microsoft.Z3
{
    public class RCFNum : Z3Object
    {
        public RCFNum(Context ctx, string value)
            : base(ctx, Native.Z3_rcf_mk_rational(ctx.nCtx, value))
        {
            Debug.Assert(ctx != null);
        }
 
        public RCFNum(Context ctx, int value)
            : base(ctx, Native.Z3_rcf_mk_small_int(ctx.nCtx, value))
        {
            Debug.Assert(ctx != null);
        }
 
        internal RCFNum(Context ctx, IntPtr obj)
            : base(ctx, obj)
        {
            Debug.Assert(ctx != null);
        }
 
        public static RCFNum MkPi(Context ctx)
        {
            return new RCFNum(ctx, Native.Z3_rcf_mk_pi(ctx.nCtx));
        }
 
        public static RCFNum MkE(Context ctx)
        {
            return new RCFNum(ctx, Native.Z3_rcf_mk_e(ctx.nCtx));
        }
 
        public static RCFNum MkInfinitesimal(Context ctx)
        {
            return new RCFNum(ctx, Native.Z3_rcf_mk_infinitesimal(ctx.nCtx));
        }
 
        public static RCFNum[] MkRoots(Context ctx, RCFNum[] coefficients)
        {
            if (coefficients == null || coefficients.Length == 0)
            {
                throw new Z3Exception("Polynomial coefficients cannot be empty");
            }
 
            uint n = (uint)coefficients.Length;
            IntPtr[] a = new IntPtr[n];
            IntPtr[] roots = new IntPtr[n];
 
            for (uint i = 0; i < n; i++)
            {
                a[i] = coefficients[i].NativeObject;
            }
 
            uint numRoots = Native.Z3_rcf_mk_roots(ctx.nCtx, n, a, roots);
 
            RCFNum[] result = new RCFNum[numRoots];
            for (uint i = 0; i < numRoots; i++)
            {
                result[i] = new RCFNum(ctx, roots[i]);
            }
 
            return result;
        }
 
        public RCFNum Add(RCFNum other)
        {
            CheckContext(other);
            return new RCFNum(Context, Native.Z3_rcf_add(Context.nCtx, NativeObject, other.NativeObject));
        }
 
        public RCFNum Sub(RCFNum other)
        {
            CheckContext(other);
            return new RCFNum(Context, Native.Z3_rcf_sub(Context.nCtx, NativeObject, other.NativeObject));
        }
 
        public RCFNum Mul(RCFNum other)
        {
            CheckContext(other);
            return new RCFNum(Context, Native.Z3_rcf_mul(Context.nCtx, NativeObject, other.NativeObject));
        }
 
        public RCFNum Div(RCFNum other)
        {
            CheckContext(other);
            return new RCFNum(Context, Native.Z3_rcf_div(Context.nCtx, NativeObject, other.NativeObject));
        }
 
        public RCFNum Neg()
        {
            return new RCFNum(Context, Native.Z3_rcf_neg(Context.nCtx, NativeObject));
        }
 
        public RCFNum Inv()
        {
            return new RCFNum(Context, Native.Z3_rcf_inv(Context.nCtx, NativeObject));
        }
 
        public RCFNum Power(uint k)
        {
            return new RCFNum(Context, Native.Z3_rcf_power(Context.nCtx, NativeObject, k));
        }
 
        public static RCFNum operator +(RCFNum a, RCFNum b)
        {
            return a.Add(b);
        }
 
        public static RCFNum operator -(RCFNum a, RCFNum b)
        {
            return a.Sub(b);
        }
 
        public static RCFNum operator *(RCFNum a, RCFNum b)
        {
            return a.Mul(b);
        }
 
        public static RCFNum operator /(RCFNum a, RCFNum b)
        {
            return a.Div(b);
        }
 
        public static RCFNum operator -(RCFNum a)
        {
            return a.Neg();
        }
 
        public bool Lt(RCFNum other)
        {
            CheckContext(other);
            return 0 != Native.Z3_rcf_lt(Context.nCtx, NativeObject, other.NativeObject);
        }
 
        public bool Gt(RCFNum other)
        {
            CheckContext(other);
            return 0 != Native.Z3_rcf_gt(Context.nCtx, NativeObject, other.NativeObject);
        }
 
        public bool Le(RCFNum other)
        {
            CheckContext(other);
            return 0 != Native.Z3_rcf_le(Context.nCtx, NativeObject, other.NativeObject);
        }
 
        public bool Ge(RCFNum other)
        {
            CheckContext(other);
            return 0 != Native.Z3_rcf_ge(Context.nCtx, NativeObject, other.NativeObject);
        }
 
        public bool Eq(RCFNum other)
        {
            CheckContext(other);
            return 0 != Native.Z3_rcf_eq(Context.nCtx, NativeObject, other.NativeObject);
        }
 
        public bool Neq(RCFNum other)
        {
            CheckContext(other);
            return 0 != Native.Z3_rcf_neq(Context.nCtx, NativeObject, other.NativeObject);
        }
 
        public static bool operator <(RCFNum a, RCFNum b)
        {
            return a.Lt(b);
        }
 
        public static bool operator >(RCFNum a, RCFNum b)
        {
            return a.Gt(b);
        }
 
        public static bool operator <=(RCFNum a, RCFNum b)
        {
            return a.Le(b);
        }
 
        public static bool operator >=(RCFNum a, RCFNum b)
        {
            return a.Ge(b);
        }
 
        public static bool operator ==(RCFNum a, RCFNum b)
        {
            if (ReferenceEquals(a, b)) return true;
            if (ReferenceEquals(a, null) || ReferenceEquals(b, null)) return false;
            return a.Eq(b);
        }
 
        public static bool operator !=(RCFNum a, RCFNum b)
        {
            return !(a == b);
        }
 
        public bool IsRational()
        {
            return 0 != Native.Z3_rcf_is_rational(Context.nCtx, NativeObject);
        }
 
        public bool IsAlgebraic()
        {
            return 0 != Native.Z3_rcf_is_algebraic(Context.nCtx, NativeObject);
        }
 
        public bool IsInfinitesimal()
        {
            return 0 != Native.Z3_rcf_is_infinitesimal(Context.nCtx, NativeObject);
        }
 
        public bool IsTranscendental()
        {
            return 0 != Native.Z3_rcf_is_transcendental(Context.nCtx, NativeObject);
        }
 
        public string ToString(bool compact)
        {
            return Native.Z3_rcf_num_to_string(Context.nCtx, NativeObject, compact ? (byte)1 : (byte)0, 0);
        }
 
        public override string ToString()
        {
            return ToString(false);
        }
 
        public string ToDecimal(uint precision)
        {
            return Native.Z3_rcf_num_to_decimal_string(Context.nCtx, NativeObject, precision);
        }
 
        public override bool Equals(object obj)
        {
            if (obj is RCFNum other)
            {
                return this == other;
            }
            return false;
        }
 
        public override int GetHashCode()
        {
            return NativeObject.GetHashCode();
        }
 
        #region Internal
        internal override void DecRef(IntPtr o)
        {
            Native.Z3_rcf_del(Context.nCtx, o);
        }
 
        private void CheckContext(RCFNum other)
        {
            if (Context != other.Context)
            {
                throw new Z3Exception("RCF numerals from different contexts");
            }
        }
        #endregion
    }
}