package gprover;


public class ndgcs {
    ndgcs parent = null;
    cndg nd = null;
    int ntype = 0; // 0. Normal,  1. exists.
    boolean leaf = false;
    boolean valid = true;

    int no = -1;
    ndgcs[] child = new ndgcs[3];
    cons[] allcns = new cons[100];


    public void add(cons c) {
        if (c != null) {
            allcns[++no] = c;
        }
    }


    public int getMaxCnsInt() {
        int n = 0;

        for (int i = 0; i <= no; i++) {
            if (allcns[i] == null)
                continue;
            int k = allcns[i].getLastPt();
            if (k > n)
                n = k;
        }
        return n;
    }

    public void add(int i, cons c) {
        if (c != null) {
            allcns[i] = c;
        }
    }

    public int getNotNullNum() {
        int k = 0;
        for (int i = 0; i <= no; i++) {
            if (allcns[i] != null)
                k++;
        }
        return k;
    }

    public void addChild(ndgcs c) {
        for (int i = 0; i < child.length; i++) {
            if (child[i] == null) {
                child[i] = c;
                break;
            }
        }
    }

    public void replace(int m, int n) {
        for (int i = 0; i <= no; i++) {
            cons c1 = allcns[i];
            if (c1 != null)
                c1.replace(m, n);
        }
    }

    public void sort() {

        for (int i = 0; i <= no; i++) {
            cons c1 = allcns[i];
            for (int j = 0; j < i; j++) {
                cons c2 = allcns[j];
                if (c1 != null && c2 != null && compare(c1, c2) < 0) {
                    for (int k = i - 1; k >= j; k--)
                        allcns[k + 1] = allcns[k];
                    allcns[j] = c1;
                    break;
                }
            }
        }

    }

    public static int compare(cons c1, cons c2) {
        int n1 = c1.getLastPt();
        int n2 = c2.getLastPt();
        if (n1 == n2) {
            if (c1.type > c2.type)
                return 1;
            if (c1.type < c2.type)
                return -1;
            return compare1(c1, c2, n1);
        }

        if (n1 > n2)
            return 1;

        return 0;
    }

    private static int compare1(cons c1, cons c2, int n)  // euql type;
    {
        while (n > 0) {
            int n1 = c1.getLessPt(n);
            int n2 = c2.getLessPt(n);
            if (n1 == n2) {
                n = n1;
            } else if (n1 > n2)
                return 1;
            else return -1;
        }
        return 0;
    }

    public void rm_common() {
        for (int i = 0; i <= no; i++) {
            cons c = allcns[i];
            if (c == null)
                continue;
            for (int j = 0; j < i; j++) {
                cons c1 = allcns[j];
                if (c1 != null && c1.isEqual(c)) {
                    allcns[i] = null;
                    break;
                }
            }
        }
    }

    public void reduce() {
        if (nd == null)
            return;
        int a = nd.p[0];
        int b = nd.p[1];

        if (nd.type == gib.NDG_NEQ || nd.type == gib.NDG_NON_ISOTROPIC) {
            for (int i = 0; i <= no; i++) {
                cons c = allcns[i];
                if (c == null)
                    continue;
                c.replace(b, a);   // replace b with a.
                c.reorder();
            }
        }
    }

    public void reorder() {
        for (int i = 0; i <= no; i++) {
            cons c = allcns[i];
            if (c == null)
                continue;
            c.reorder();
        }
    }

    public ndgcs() {
    }

    public ndgcs(ndgcs c) {
        parent = c.parent;
        nd = c.nd;
        no = c.no;
        for (int i = 0; i <= no; i++) {
            if (c.allcns[i] != null)
                allcns[i] = new cons(c.allcns[i]);
        }
    }

    public int getCSindex() {
        int a = -1;
        for (int d = 0; d < child.length; d++) {
            if (child[d] != null)
                a = d;
        }
        return a;
    }
}
