code: package wprover;
  
  import gprover.cndg;
  import gprover.cons;
  import gprover.gterm;
  import maths.PolyBasic;
  import maths.TDono;
  import maths.TMono;
  import maths.TPoly;
  
  import javax.swing.*;
  import java.awt.event.ActionEvent;
  import java.awt.event.ActionListener;
  import java.awt.event.MouseListener;
  import java.awt.event.MouseEvent;
  import java.util.Vector;
  import java.io.File;
  import java.io.FileOutputStream;
  import java.io.IOException;
  
  public class panelGB extends panelAlgebric implements MouseListener {
  
      private Vector vndgs;
      private boolean prs = false;
      private static long TIME = 1000000;
      private JPopupMenu menu;
  
      public panelGB(drawProcess dp, wuTextPane tpane) {
          super(dp, tpane);
          menu = new JPopupMenu();
          JMenuItem it = new JMenuItem("Save as Maple Format");
          menu.add(it);
          it.addActionListener(new ActionListener() {
              public void actionPerformed(ActionEvent e) {
                  saveAsMaple();
              }
          });
          tpane.addMouseListener(this);
      }
  
  
      public void stopRunning() {
          running = false;
          PolyBasic.setbbStop(true);
          this.addString("\n");
          this.addString("icon4", "icon4");
          this.addString("The Process Is Stopped By The User.");
  
      }
  
  
      public void prove(gterm tm, drawProcess dp) {
          if (running)
              return;
  
          tpane.setText("");
          _mremainder = null;
          gt = tm;
          main = new Thread(this, "GbProver");
          running = true;
          main.start();
          startTimer();
      }
  
      public void startTimer() {
          if (gxInstance != null) {
              Timer t = new Timer(1000, new ActionListener() {
                  public void actionPerformed(ActionEvent e) {
                      if (running) {
                          rund = RunningDialog.startTimer(gxInstance, "GBasis is Running");
                          rund.setPanelGB(panelGB.this);
                      }
                      Timer t = (Timer) e.getSource();
                      t.stop();
                  }
              });
  
              t.start();
          }
  
      }
  
  
      protected int div(TMono m1, TPoly p1) {
          if (poly.pzerop(m1))
              return 0;
          Vector vt = new Vector();
  
          while (p1 != null) {
              TMono t = p1.poly;
              vt.add(0, t);
              if (t.x == m1.x)
                  break;
              p1 = p1.next;
          }
  
          int index = vt.size();
  
          long time = System.currentTimeMillis();
          int i = 0;
          while (true) {
              if (i >= vt.size())
                  break;
  
              TMono m = (TMono) vt.get(i++);
              TMono md = poly.pcopy(m);
              m1 = poly.prem(m1, md);
              if (m1 != null && m1.x == 9) {
                  int k = 0;
              }
              long t1 = System.currentTimeMillis();
  //            addDiv(--index, m1, m.x, t1 - time);
              time = t1;
              if (poly.pzerop(m1))
                  return 0;
              if (!running)
                  return 1;
          }
          String s = poly.printSPoly(m1);
          addString("Remainder:  " + s);
  
          return 1;
      }
  
      protected TMono getTMono(cons c) {
          return dp.getTMono(c);
      }
  
      public int addMM(TMono m, Vector v, int param) {
          GeoPoly gp = GeoPoly.getPoly();
  
          if (gp.plength(m) == 1) {
              while (m != null && m.deg > 0 && m.x > 0) {
                  TMono m1 = gp.pth(m.x, 1, 1);
                  m1 = gp.n_ndg(m1, param--);
                  v.add(m1);
                  m = m.coef;
              }
          } else {
              m = gp.n_ndg(m, param--);
              v.add(m);
          }
  
          return param;
  
      }
  
      private boolean is_ndg_set() {
          return gt != null && gt.getNcons().size() > 0;
      }
  
      public void getNDGS(Vector v3) {
          int t = 3;
          int param = -1;
          GeoPoly gp = GeoPoly.getPoly();
  
          if (t == 3) {
              vndgs = gt.getNcons();
          }
  
  
          if (t == 0 || t == 3) {     // from FULL
              for (int i = 0; i < vndgs.size(); i++) {
                  cndg nd = (cndg) vndgs.get(i);
                  TMono m = gp.mm_poly(nd, dp);
                  addString1(nd.toString() + "\n");
                  if (m != null) {
                      param = addMM(m, v3, param);
  
  
                  }
              }
          } else if (t == 1) { // from DB
              Vector v = dp.getNDGS();
              for (int i = 0; i < v.size(); i++) {
                  TMono m = (TMono) v.get(i);
                  if (m != null) {
                      param = addMM(m, v3, param);
                  }
              }
          }
      }
  
  
      public void run() {
  
          if (gt == null) {
              running = false;
              if (rund != null)
                  rund.stopTimer();
              return;
          }
  
  //        /if (is_ndg_set())
  //            this.gbasis1();
  //        else
          gbasis();
  
          PolyBasic.setbbStop(false);
          running = false;
          if (rund != null)
              rund.stopTimer();
      }
  
      public void gbasis1() {
  
          String sc = gt.getConcText();
          cons cc = gt.getConclution();
  
          TMono mc = getTMono(cc);
          if (mc == null) {
              running = false;
              return;
          }
  
  
          addAlgebraicForm();
          addString2("The equational hypotheses:");
  
          Vector vc = dp.getAllConstraint();
          int n = 1;
          Vector pp = new Vector();
  
  
          for (int i = 0; i < vc.size(); i++) {
              constraint c = (constraint) vc.get(i);
              if (c.is_poly_genereate) {
                  c.PolyGenerate();
                  TPoly p1 = constraint.getPolyListAndSetNull();
                  if (p1 != null)
                      addString1(n++ + ": " + c.toString() + "\n");
                  while (p1 != null) {
                      TMono m = p1.getPoly();
                      if (m != null) {
                          poly.ppush(m, pp);
                          addString("  " + poly.printSPoly(m));
                      }
                      p1 = p1.next;
                  }
              }
          }
  
  
          addString2("Nondegenerate Conditions");
          Vector v3 = new Vector();
          this.getNDGS(v3);
          Vector p = v3;
          printTP(p);
  
  
          for (int i = 0; i < p.size(); i++) {
              TMono m = (TMono) p.get(i);
              poly.ppush(m, pp);
          }
  
          if (prs) {
              addString2("Poly set before gbasis");
              printTP(pp);
          }
  
          int dx = p.size() + 2;
          poly.upValueTM(pp, dx);
  
          int index = 1;
          long t = System.currentTimeMillis();
  
          boolean r1 = false;
  //        if (true) {
  //            sbasis();
  //            return;
  //        }
  
          while (true) {
              if (index == 2) {
                  int k = 0;
              }
  
              if (!prs) {
                  addString2(index + ": Poly set before bb-reduce");
                  printTP(pp);
              }
              r1 = true;
  
  
              pp = poly.bb_reduce(pp, t);
              //           if (System.currentTimeMillis() - t > 10000)
              //             break;
  
              if (!prs) {
                  addString2(index++ + ": Poly set after bb-reduce");
                  printTP(pp);
              }
  //            }
              if (gb_finished(pp))
                  break;
              //       if (pp.size() > 30)
              //            break;
  
              Vector tp = poly.s_polys(pp);
              if (tp.size() != 0) {
                  tp = poly.bb_reduce(tp, t);
                  if (!prs) {
                      addString2("S - Polynomials");
                      printTP(tp);
                  }
  //                }
                  for (int i = 0; i < tp.size(); i++)
                      poly.ppush((TMono) tp.get(i), pp);
              } else {
                  break;
              }
              if (!running)
                  return;
          }
  
  
          String s1 = poly.printSPoly(mc);
          poly.upValueTM(mc, dx);
          mc = poly.b_reduce(mc, pp);
          poly.upValueTM(mc, -dx);
          poly.upValueTM(pp, -dx);
          String s2 = poly.printSPoly(mc);
  
          if (prs) {
              addString2("Poly set after gbasis");
              printTP(pp);
          }
  
  
          addString2("The conclution: ");
          addString1(sc + "\n");
  
          addString(s1);
          addString2("The conclution after reduce:");
          addString(s2);
  
          if (mc == null) {
              addString("icon1", "icon1");
              addString1("The conclution is true");
          } else {
              addString("icon2", "icon2");
              addString1("The conclution is false");
          }
          running = false;
      }
  
      public void printTP(Vector v) {
          for (int i = 0; i < v.size(); i++) {
              TMono m = (TMono) v.get(i);
              if (m != null)
                  addString(poly.printSPoly(m));
          }
      }
  
      public boolean gb_finished(Vector v) {
          for (int i = 0; i < v.size(); i++) {
              TMono m = (TMono) v.get(i);
              if (poly.plength(m) == 1 && m.x == 0)
                  return true;
          }
          return false;
      }
  
      public void test(Vector pp, int dx) {
          int size = pp.size();
  
  
          if (size < 2) return;
  
          int index = size - 3;
          Vector vp = new Vector();
          for (int i = size - 2; i < size; i++)
              vp.add(pp.get(i));
  
  
          for (int i = index; i >= 0; i--) {
              addString2(i + "GBASIS");
              printTP(vp);
  
              vp.add(0, pp.get(i));
              gbasis(vp);
          }
  
          addString2(-1 + "GBASIS");
          poly.upValueTM(vp, -dx);
          printTP(vp);
  
  
      }
  
  
      public void gbasis(Vector pp) {
  //        long t = System.currentTimeMillis();
  
          while (true) {
              pp = poly.bb_reduce(pp, 10000);
              if (!isRunning())
                  break;
  
              if (gb_finished(pp))
                  break;
  
  
              Vector tp = poly.s_polys(pp);
  
              if (tp.size() != 0) {
                  for (int i = 0; i < tp.size(); i++)
                      poly.ppush((TMono) tp.get(i), pp);
  
              } else {
                  break;
              }
          }
      }
  
      public void dbasis(Vector pp) {
  
          GeoPoly basic = GeoPoly.getPoly();
  
          Vector v = new Vector();
          int size = pp.size();
          for (int i = 0; i < size - 1; i++) {
              TMono m1 = (TMono) pp.get(i);
              for (int j = i + 1; j < size; j++) {
                  TMono m2 = (TMono) pp.get(j);
                  v.clear();
                  v.add(basic.p_copy(m1));
                  v.add(basic.p_copy(m2));
  
                  basic.printVpoly(v);
                  while (true) {
                      v = poly.bb_reduce(v, -1);
  
                      if (gb_finished(v))
                          break;
  
  
                      Vector tp = poly.s_polys(v);
  
                      if (v.size() >= 1) {
                          basic.printVpoly(v);
                          basic.printVpoly(tp);
                      }
                      tp = poly.bb_reduce(tp, -1);
  
  
                      if (tp.size() != 0) {
                          for (int k = 0; k < tp.size(); k++)
                              poly.ppush((TMono) tp.get(k), v);
                      } else {
                          break;
                      }
                  }
                  basic.printVpoly(v);
              }
          }
      }
  
  
      public TMono sbasis(int x, Vector v, TMono mc) {
  
          Vector vg = new Vector();
          if (v.size() == 0) return mc;
          GeoPoly basic = GeoPoly.getPoly();
  
          int nn = x;
          int dx = nn / 2 + 2;
          TMono m1, m2;
          int param = 0;
          Vector vrs = new Vector();
  
  
          for (int n = 1; n < nn / 2 + 1; n++) {
              m1 = m2 = null;
  
              for (int i = 0; i < v.size(); i++) {
                  TMono m = (TMono) v.get(i);
                  if (m.x == 2 * n || m.x == 2 * n - 1) {
                      if (m1 == null)
                          m1 = m;
                      else m2 = m;
                  }
              }
  
              if (m1 != null)
                  v.remove(m1);
              if (m2 != null)
                  v.remove(m2);
  
              if (m1 != null || m2 != null) {
                  TMono t = basic.ll_delta(2 * n, m1, m2);
                  if (basic.plength(t) == 1 && t.x == 0 && t.val.intValue() != 0)
                      t = null;
                  --param;
                  int dd = -param + 3;
                  t = basic.n_ndg(t, param);
  
                  vg.clear();
  
                  basic.ppush(m2, vg);
                  basic.ppush(m1, vg);
                  basic.ppush(t, vg);
  //                System.out.println(basic.getAllPrinted(m1));
  //                System.out.println(basic.getAllPrinted(m2));
  
                  basic.upValueTM(vg, dd);
  //
  //                if(false)
  //                {
  //                    Vector vtp = basic.specialTreatment(m1, m2, param + dd);
  //                    if (vtp.size() != 0) {
  //                        vg.clear();
  //                        for (int i = 0; i < vtp.size(); i++)
  //                            basic.ppush((TMono) vtp.get(i), vg);
  //                        basic.ppush(t, vg);
  //                    }
  //                }
  
                  this.gbasis(vg);
                  basic.upValueTM(vg, -dd);
                  for (int i = 0; i < vg.size(); i++) {
                      TMono tt = (TMono) vg.get(i);
                      basic.ppush(tt, vrs);
                  }
              }
          }
  
          basic.upValueTM(vrs, dx);
  
          Vector vnds = basic.getcnds(vrs, dx);
          basic.bb_reduce(vrs, 10000, true);
          if (!running)
              return null;
  
          Vector vnn = new Vector();
          for (int i = 0; i < vnds.size(); i++) {
  
              TMono m = (TMono) vnds.get(i);
              m = basic.b_reduce(basic.p_copy(m), vrs);
              if (!running)
                  return null;
              TDono d = basic.splitDono(m, dx);
  
              if (d != null)
                  vnn.add(d);
          }
  
          Vector vco = basic.parseCommonDono(vnn, dx);
          for (int i = 0; i < vnds.size(); i++) {
              TMono d = (TMono) vnds.get(i);
              basic.ppush(d, vrs);
          }
  
          if (vco.size() != 0) {
              for (int i = 0; i < vco.size(); i++) {
                  TMono m = (TMono) vco.get(i);
                  basic.ppush(m, vrs);
              }
  
          }
  
          basic.bb_reduce(vrs, 10000, true);
          mc = basic.b_reduce(mc, vrs);
  
          while (basic.ctLessdx(mc, dx)) {
              mc = basic.reduceMDono(mc, vnn, dx); // reduced all u parameters.
              mc = basic.b_reduce(mc, vrs);
              if (!running)
                  return null;
          }
  
          TMono mcr = basic.p_copy(mc);
          basic.eraseCommonDono(vnn);
  
  
          Vector vnn1 = new Vector();
          for (int i = 0; i < vnn.size(); i++) {
              TDono d = (TDono) vnn.get(i);
              TMono m = basic.p_copy(d.p2);
              m = basic.reduceMDono(m, vnn, dx);
              if (!running)
                  return null;
              m = basic.b_reduce(m, vrs);
              if (!running)
                  return null;
              vnn1.add(m);
          }
  
          basic.upValueTM(vrs, -dx);
          basic.upValueDM(vnn, -dx);
          basic.upValueTM(mc, -dx);
          basic.upValueTM(mcr, -dx);
          basic.upValueTM(vnn1, -dx);
  
          this.printTP(vrs);
  //        this.printVectorExpanded(vrs, 0);
  
          addSVdd(vnn1);
          v.clear();
          v.addAll(vrs);
          return mc;
      }
  
      public void printVectorExpanded(Vector vrs, int dx) {
          GeoPoly basic = GeoPoly.getPoly();
  
          basic.upValueTM(vrs, -dx);
          for (int i = 0; i < vrs.size(); i++) {
              TMono ma = (TMono) vrs.get(i);
              String st = basic.getExpandedPrint(ma);
              if (st.endsWith("*"))
                  st = st.substring(0, st.length() - 1);
              else if (st.endsWith("-") || st.endsWith("+"))
                  st += "1";
              System.out.println(st);
          }
          basic.upValueTM(vrs, dx);
      }
  
      public void addSVdd(Vector v) {
          GeoPoly basic = GeoPoly.getPoly();
  
          addString2(getLanguage(1116, "The Nondegenerate Conditions"));
          for (int i = 0; i < v.size(); i++) {
  //            TDono d = (TDono) v.get(i);
              TMono m = (TMono) v.get(i);
              basic.coefgcd(m);
              TMono mf = basic.get_factor1(m);
              if (mf == null) {
                  basic.factor1(m);
                  String s = basic.printNPoly(m);
                  this.addString(s);
              } else {
                  TMono ff = mf;
                  while (mf != null) {
                      basic.div_factor1(m, mf.x, mf.deg);
                      mf = mf.coef;
                  }
                  String s = basic.printNPoly(ff, m);
                  this.addString(s);
  
              }
          }
  
      }
  
      public void printVDD(Vector v) {
          GeoPoly basic = GeoPoly.getPoly();
  
          for (int i = 0; i < v.size(); i++) {
  
              TDono d = (TDono) v.get(i);
              basic.sprint(d.p1);
              System.out.print("*( ");
              basic.sprint(d.p2);
              System.out.print(" )");
              if (d.c.value() > 0)
                  System.out.print(" + ");
              basic.sprint(d.c);
              System.out.print("\n");
  
  
          }
  
      }
  
      public void gbasis() {
          GeoPoly basic = GeoPoly.getPoly();
          String sc = gt.getConcText();
          cons cc = gt.getConclution();
          TMono mc = getTMono(cc);
          if (mc == null) {
              running = false;
              return;
          }
  
  
          addAlgebraicForm();
          addString2(getLanguage(1103, "The Equational Hypotheses:"));
  
          Vector vc = dp.getAllConstraint();
          int n = 1;
          Vector pp = new Vector();
  
  
          for (int i = 0; i < vc.size(); i++) {
              constraint c = (constraint) vc.get(i);
              if (c.is_poly_genereate) {
                  c.PolyGenerate();
                  TPoly p1 = constraint.getPolyListAndSetNull();
                  if (p1 != null)
                      addString1(n++ + ": " + c.toString() + "\n");
                  while (p1 != null) {
                      TMono m = p1.getPoly();
                      if (m != null) {
                          poly.ppush(m, pp);
                          addString("  " + poly.printSPoly(m));
                      }
                      p1 = p1.next;
                  }
              }
          }
  
          addString2(getLanguage(1114, "The Initial Polynomial Set"));
          printTP(pp);
  
          String s1 = poly.printSPoly(mc);
  
          addString2(getLanguage(1115, "The Groebner Basis: ") + "GB = ");
  //        addString2("GB = ");
          Vector v = dp.getPBMono();
  
          int x = basic.getMaxX(v);
          int dx = x / 2 + 2;
          basic.upValueTM(mc, dx);
  
          mc = sbasis(x, v, mc);
          if (!running)
              return;
          pp = v;
  
          String s2 = poly.printSPoly(mc);
          addString2(getLanguage(1105, "The Conclution: "));
          addString1(sc + "\n");
          addString(s1);
          addString2(getLanguage(1117, "The Conclution After Reduce:"));
          addString(s2);
  
          if (mc == null) {
              addString("icon1", "icon1");
              addString1(getLanguage(1108, "The conclution is true"));
          } else {
              addString("icon2", "icon2");
              addString1(getLanguage(1109, "The conclution is false"));
              if (poly.plength(mc) > 2) {
                  _mremainder = mc;
                  addString("\n");
                  addButton();
              }
          }
  
          running = false;
      }
  
  
      ////////////////////////////////////////////////////////////
      public void mouseClicked(MouseEvent e) {
          menu.show((JComponent) e.getSource(), e.getX(), e.getY());
      }
  
      public void mousePressed(MouseEvent e) {
      }
  
      public void mouseReleased(MouseEvent e) {
      }
  
      public void mouseEntered(MouseEvent e) {
      }
  
      public void mouseExited(MouseEvent e) {
      }
  
      public void saveAsMaple() {
          JFileChooser filechooser1 = new JFileChooser();
          String dr = GExpert.getUserDir();
          filechooser1.setCurrentDirectory(new File(dr));
          int result = filechooser1.showDialog(this, "Save");
          if (result == JFileChooser.APPROVE_OPTION) {
              File f = filechooser1.getSelectedFile();
              FileOutputStream fp;
              try {
                  if (f.exists()) {
                      f.delete();
                      fp = new FileOutputStream(f, true);
                  } else {
                      f.createNewFile();
                      fp = new FileOutputStream(f, false);
                  }
                  if (fp == null) {
                      return;
                  }
                  writeMaple(fp);
                  fp.close();
              } catch (IOException ee) {
                  JOptionPane.showMessageDialog(this, ee.getMessage(),
                          "Save Failed", JOptionPane.ERROR_MESSAGE);
              }
  
          }
      }
  
      public void writeMaple(FileOutputStream out) throws IOException {
          GeoPoly basic = GeoPoly.getPoly();
          cons cc = gt.getConclution();
          TMono mc = getTMono(cc);
  
          // Part 1: Order for the variables.
          boolean fr = true;
          out.write("vars := [".getBytes());
  
          Vector vp = dp.getPointList();
          for (int i = vp.size() - 1; i >= 0; i--) {
              CPoint pt = (CPoint) vp.get(i);
              String s1 = pt.x1.getString();
              String s2 = pt.y1.getString();
              if (GeoPoly.vzero(pt.x1.xindex))
                  continue;
              if (GeoPoly.vzero(pt.y1.xindex))
                  continue;
              if (fr) {
                  fr = false;
              } else out.write(", ".getBytes());
              out.write((s2 + ", " + s1).getBytes());
          }
  
  
          Vector v = dp.getPBMono();
          int x = basic.getMaxX(v);
  
          Vector vg = new Vector();
          int nn = x;
          TMono m1, m2;
          int param = 0;
  
          for (int n = 1; n < nn / 2 + 1; n++) {
              m1 = m2 = null;
  
              for (int i = 0; i < v.size(); i++) {
                  TMono m = (TMono) v.get(i);
                  if (m.x == 2 * n || m.x == 2 * n - 1) {
                      if (m1 == null)
                          m1 = m;
                      else m2 = m;
                  }
              }
  
              if (m1 != null)
                  v.remove(m1);
              if (m2 != null)
                  v.remove(m2);
  
              if (m1 != null || m2 != null) {
                  TMono t = basic.ll_delta(2 * n, m1, m2);
                  if (basic.plength(t) == 1 && t.x == 0 && t.val.intValue() != 0)
                      t = null;
                  --param;
                  t = basic.n_ndg(t, param);
                  if (t != null)
                      out.write((", u" + (-param)).getBytes());
  
                  basic.ppush(m2, vg);
                  basic.ppush(m1, vg);
                  basic.ppush(t, vg);
              }
          }
          out.write("];".getBytes());
  
  // Part 2: All polynomials.
  //        out.write(("\n" + vg.size()).getBytes());
          for (int i = 0; i < vg.size(); i++) {
              TMono m = (TMono) vg.get(i);
              out.write("\n".getBytes());
              out.write(("P" + i + " := " + poly.getExpandedPrint(m) +" ;").getBytes());
          }
          String st = poly.getExpandedPrint(mc);
          out.write(("\n C := " + st +" ;").getBytes());
  
      }
  }