Signs.java Source File

00001 package edu.ksu.cis.bandera.abstraction.lib.real;
00002 
00003 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
00004  * Bandera, a Java(TM) analysis and transformation toolkit           *
00005  * Copyright (C) 1998-2001 SAnToS Laboratories (santos@cis.ksu.edu)  *
00006 
00007  * All rights reserved.                                              *
00008  *                                                                   *
00009  * This work was done as a project in the SAnToS Laboratory,         *
00010  * Department of Computing and Information Sciences, Kansas State    *
00011  * University, USA (http://www.cis.ksu.edu/santos).                  *
00012  * It is understood that any modification not identified as such is  *
00013  * not covered by the preceding statement.                           *
00014  *                                                                   *
00015  * This work is free software; you can redistribute it and/or        *
00016  * modify it under the terms of the GNU Library General Public       *
00017  * License as published by the Free Software Foundation; either      *
00018  * version 2 of the License, or (at your option) any later version.  *
00019  *                                                                   *
00020  * This work is distributed in the hope that it will be useful,      *
00021  * but WITHOUT ANY WARRANTY; without even the implied warranty of    *
00022  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *
00023  * Library General Public License for more details.                  *
00024  *                                                                   *
00025  * You should have received a copy of the GNU Library General Public *
00026  * License along with this toolkit; if not, write to the             *
00027  * Free Software Foundation, Inc., 59 Temple Place - Suite 330,      *
00028  * Boston, MA  02111-1307, USA.                                      *
00029  *                                                                   *
00030  * Java is a trademark of Sun Microsystems, Inc.                     *
00031  *                                                                   *
00032  * To submit a bug report, send a comment, or get the latest news on *
00033  * this project and other SAnToS projects, please visit the web-site *
00034  *                http://www.cis.ksu.edu/santos                      *
00035  * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
00036 // This file was generated by Bandera (http://www.cis.ksu.edu/santos/bandera).
00037 import edu.ksu.cis.bandera.abstraction.*;
00038 public class Signs extends RealAbstraction {
00039   private static final Signs v = new Signs();
00040   public static final int ZERO = 0;
00041   public static final int NEG = 1;
00042   public static final int POS = 2;
00043   private Signs() {
00044   }  
00045   public static int abs(double n) {
00046     if (n < 0) return NEG;
00047     if (n == 0) return ZERO;
00048     if (n > 0) return POS;
00049     throw new RuntimeException("Signs cannot abstract value '" + n + "'");
00050   }  
00051   public static int add(int left$, int right$) {
00052     if (left$ == NEG && right$ == NEG) return NEG;
00053     if (left$ == NEG && right$ == ZERO) return NEG;
00054     if (left$ == NEG && right$ == POS) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00055     if (left$ == ZERO && right$ == NEG) return NEG;
00056     if (left$ == ZERO && right$ == ZERO) return ZERO;
00057     if (left$ == ZERO && right$ == POS) return POS;
00058     if (left$ == POS && right$ == NEG) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00059     if (left$ == POS && right$ == ZERO) return POS;
00060     if (left$ == POS && right$ == POS) return POS;
00061     throw new RuntimeException("Signs.add(" + left$ + ", " + right$ + ") is undefined");
00062   }  
00063   private static int addNoChoose(int left, int right) {
00064     int result = 0;
00065     switch (left) {
00066       case 0:
00067         switch (right) {
00068           case 0:
00069             result = 1;
00070             break;
00071           case 1:
00072             result = 2;
00073             break;
00074           case 2:
00075             result = 4;
00076             break;
00077         }
00078         break;
00079       case 1:
00080         switch (right) {
00081           case 0:
00082             result = 2;
00083             break;
00084           case 1:
00085             result = 2;
00086             break;
00087           case 2:
00088             result = 7;
00089             break;
00090         }
00091         break;
00092       case 2:
00093         switch (right) {
00094           case 0:
00095             result = 4;
00096             break;
00097           case 1:
00098             result = 7;
00099             break;
00100           case 2:
00101             result = 4;
00102             break;
00103         }
00104         break;
00105     }
00106     if (result == 0) throw new RuntimeException("Signs.addNoChoose(" + left + ", " + right + ") is undefined");
00107     return result;
00108   }  
00109   public static int addSet(int leftTokens, int rightTokens) {
00110     int result = -1;
00111     for (int left = 0; (1 << left) <= leftTokens; left++) {
00112       if ((leftTokens & (1 << left)) == 0) continue;
00113       for (int right = 0; (1 << right) <= rightTokens; right++) {
00114         if ((rightTokens & (1 << right)) != 0) {
00115           if (result == -1) result = addNoChoose(left, right);
00116           else result = Abstraction.meetArith(result, addNoChoose(left, right));
00117         }
00118       }
00119     }
00120     return result;
00121   }  
00122   public static int div(int left$, int right$) {
00123     if (left$ == NEG && right$ == NEG) return POS;
00124     if (left$ == NEG && right$ == ZERO) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00125     if (left$ == NEG && right$ == POS) return NEG;
00126     if (left$ == ZERO && right$ == NEG) return ZERO;
00127     if (left$ == ZERO && right$ == ZERO) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00128     if (left$ == ZERO && right$ == POS) return ZERO;
00129     if (left$ == POS && right$ == NEG) return NEG;
00130     if (left$ == POS && right$ == ZERO) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00131     if (left$ == POS && right$ == POS) return POS;
00132     throw new RuntimeException("Signs.div(" + left$ + ", " + right$ + ") is undefined");
00133   }  
00134   private static int divNoChoose(int left, int right) {
00135     int result = 0;
00136     switch (left) {
00137       case 0:
00138         switch (right) {
00139           case 0:
00140             result = 7;
00141             break;
00142           case 1:
00143             result = 1;
00144             break;
00145           case 2:
00146             result = 1;
00147             break;
00148         }
00149         break;
00150       case 1:
00151         switch (right) {
00152           case 0:
00153             result = 7;
00154             break;
00155           case 1:
00156             result = 4;
00157             break;
00158           case 2:
00159             result = 2;
00160             break;
00161         }
00162         break;
00163       case 2:
00164         switch (right) {
00165           case 0:
00166             result = 7;
00167             break;
00168           case 1:
00169             result = 2;
00170             break;
00171           case 2:
00172             result = 4;
00173             break;
00174         }
00175         break;
00176     }
00177     if (result == 0) throw new RuntimeException("Signs.divNoChoose(" + left + ", " + right + ") is undefined");
00178     return result;
00179   }  
00180   public static int divSet(int leftTokens, int rightTokens) {
00181     int result = -1;
00182     for (int left = 0; (1 << left) <= leftTokens; left++) {
00183       if ((leftTokens & (1 << left)) == 0) continue;
00184       for (int right = 0; (1 << right) <= rightTokens; right++) {
00185         if ((rightTokens & (1 << right)) != 0) {
00186           if (result == -1) result = divNoChoose(left, right);
00187           else result = Abstraction.meetArith(result, divNoChoose(left, right));
00188         }
00189       }
00190     }
00191     return result;
00192   }  
00193   public static boolean eq(int left$, int right$) {
00194     if (left$ == NEG && right$ == NEG) return Abstraction.choose();
00195     if (left$ == NEG && right$ == ZERO) return false;
00196     if (left$ == NEG && right$ == POS) return false;
00197     if (left$ == ZERO && right$ == NEG) return false;
00198     if (left$ == ZERO && right$ == ZERO) return true;
00199     if (left$ == ZERO && right$ == POS) return false;
00200     if (left$ == POS && right$ == NEG) return false;
00201     if (left$ == POS && right$ == ZERO) return false;
00202     if (left$ == POS && right$ == POS) return Abstraction.choose();
00203     throw new RuntimeException("Signs.eq(" + left$ + ", " + right$ + ") is undefined");
00204   }  
00205   private static byte eqNoChoose(int left, int right) {
00206     byte result = -1;
00207     switch (left) {
00208       case 0:
00209         switch (right) {
00210           case 0:
00211             result = 1;
00212             break;
00213           case 1:
00214             result = 0;
00215             break;
00216           case 2:
00217             result = 0;
00218             break;
00219         }
00220         break;
00221       case 1:
00222         switch (right) {
00223           case 0:
00224             result = 0;
00225             break;
00226           case 1:
00227             result = 2;
00228             break;
00229           case 2:
00230             result = 0;
00231             break;
00232         }
00233         break;
00234       case 2:
00235         switch (right) {
00236           case 0:
00237             result = 0;
00238             break;
00239           case 1:
00240             result = 0;
00241             break;
00242           case 2:
00243             result = 2;
00244             break;
00245         }
00246         break;
00247     }
00248     if (result == -1) throw new RuntimeException("Signs.eqNoChoose(" + left + ", " + right + ") is undefined");
00249     return result;
00250   }  
00251   public static byte eqSet(int leftTokens, int rightTokens) {
00252     byte result = -1;
00253     for (int left = 0; (1 << left) <= leftTokens; left++) {
00254       if ((leftTokens & (1 << left)) == 0) continue;
00255       for (int right = 0; (1 << right) <= rightTokens; right++) {
00256         if ((rightTokens & (1 << right)) != 0) {
00257           if (result == -1) result = eqNoChoose(left, right);
00258           else result = Abstraction.meetTest(result, eqNoChoose(left, right));
00259         }
00260       }
00261     }
00262     return result;
00263   }  
00264   public static boolean ge(int left$, int right$) {
00265     if (left$ == NEG && right$ == NEG) return Abstraction.choose();
00266     if (left$ == NEG && right$ == ZERO) return false;
00267     if (left$ == NEG && right$ == POS) return false;
00268     if (left$ == ZERO && right$ == NEG) return true;
00269     if (left$ == ZERO && right$ == ZERO) return true;
00270     if (left$ == ZERO && right$ == POS) return false;
00271     if (left$ == POS && right$ == NEG) return true;
00272     if (left$ == POS && right$ == ZERO) return true;
00273     if (left$ == POS && right$ == POS) return Abstraction.choose();
00274     throw new RuntimeException("Signs.ge(" + left$ + ", " + right$ + ") is undefined");
00275   }  
00276   private static byte geNoChoose(int left, int right) {
00277     byte result = -1;
00278     switch (left) {
00279       case 0:
00280         switch (right) {
00281           case 0:
00282             result = 1;
00283             break;
00284           case 1:
00285             result = 1;
00286             break;
00287           case 2:
00288             result = 0;
00289             break;
00290         }
00291         break;
00292       case 1:
00293         switch (right) {
00294           case 0:
00295             result = 0;
00296             break;
00297           case 1:
00298             result = 2;
00299             break;
00300           case 2:
00301             result = 0;
00302             break;
00303         }
00304         break;
00305       case 2:
00306         switch (right) {
00307           case 0:
00308             result = 1;
00309             break;
00310           case 1:
00311             result = 1;
00312             break;
00313           case 2:
00314             result = 2;
00315             break;
00316         }
00317         break;
00318     }
00319     if (result == -1) throw new RuntimeException("Signs.geNoChoose(" + left + ", " + right + ") is undefined");
00320     return result;
00321   }  
00322   public static byte geSet(int leftTokens, int rightTokens) {
00323     byte result = -1;
00324     for (int left = 0; (1 << left) <= leftTokens; left++) {
00325       if ((leftTokens & (1 << left)) == 0) continue;
00326       for (int right = 0; (1 << right) <= rightTokens; right++) {
00327         if ((rightTokens & (1 << right)) != 0) {
00328           if (result == -1) result = geNoChoose(left, right);
00329           else result = Abstraction.meetTest(result, geNoChoose(left, right));
00330         }
00331       }
00332     }
00333     return result;
00334   }  
00335   public static String getBASLRepresentation() {
00336     return
00337       "abstraction Signs extends real \n"
00338       + "  begin\n"
00339       + "    TOKENS = {NEG, ZERO, POS};\n"
00340       + "    DEFAULT = ZERO;\n"
00341       + "    ONE2ONE = {ZERO};\n"
00342       + "    abstract (n)\n"
00343       + "      begin\n"
00344       + "        n < 0 -> NEG;\n"
00345       + "        n == 0 -> ZERO;\n"
00346       + "        n > 0 -> POS;\n"
00347       + "      end\n"
00348       + "    operator + add \n"
00349       + "      begin\n"
00350       + "        (NEG, NEG) -> NEG;\n"
00351       + "        (NEG, ZERO) -> NEG;\n"
00352       + "        (NEG, POS) -> {NEG, ZERO, POS};\n"
00353       + "        (ZERO, NEG) -> NEG;\n"
00354       + "        (ZERO, ZERO) -> ZERO;\n"
00355       + "        (ZERO, POS) -> POS;\n"
00356       + "        (POS, NEG) -> {NEG, ZERO, POS};\n"
00357       + "        (POS, ZERO) -> POS;\n"
00358       + "        (POS, POS) -> POS;\n"
00359       + "      end\n"
00360       + "    operator - sub \n"
00361       + "      begin\n"
00362       + "        (NEG, NEG) -> {NEG, ZERO, POS};\n"
00363       + "        (NEG, ZERO) -> NEG;\n"
00364       + "        (NEG, POS) -> NEG;\n"
00365       + "        (ZERO, NEG) -> POS;\n"
00366       + "        (ZERO, ZERO) -> ZERO;\n"
00367       + "        (ZERO, POS) -> NEG;\n"
00368       + "        (POS, NEG) -> POS;\n"
00369       + "        (POS, ZERO) -> POS;\n"
00370       + "        (POS, POS) -> {NEG, ZERO, POS};\n"
00371       + "      end\n"
00372       + "    operator * mul \n"
00373       + "      begin\n"
00374       + "        (NEG, NEG) -> POS;\n"
00375       + "        (NEG, ZERO) -> ZERO;\n"
00376       + "        (NEG, POS) -> NEG;\n"
00377       + "        (ZERO, NEG) -> ZERO;\n"
00378       + "        (ZERO, ZERO) -> ZERO;\n"
00379       + "        (ZERO, POS) -> ZERO;\n"
00380       + "        (POS, NEG) -> NEG;\n"
00381       + "        (POS, ZERO) -> ZERO;\n"
00382       + "        (POS, POS) -> POS;\n"
00383       + "      end\n"
00384       + "    operator / div \n"
00385       + "      begin\n"
00386       + "        (NEG, NEG) -> POS;\n"
00387       + "        (NEG, ZERO) -> T;\n"
00388       + "        (NEG, POS) -> NEG;\n"
00389       + "        (ZERO, NEG) -> ZERO;\n"
00390       + "        (ZERO, ZERO) -> T;\n"
00391       + "        (ZERO, POS) -> ZERO;\n"
00392       + "        (POS, NEG) -> NEG;\n"
00393       + "        (POS, ZERO) -> T;\n"
00394       + "        (POS, POS) -> POS;\n"
00395       + "      end\n"
00396       + "    test == eq \n"
00397       + "      begin\n"
00398       + "        (NEG, NEG) -> {TRUE, FALSE};\n"
00399       + "        (NEG, ZERO) -> FALSE;\n"
00400       + "        (NEG, POS) -> FALSE;\n"
00401       + "        (ZERO, NEG) -> FALSE;\n"
00402       + "        (ZERO, ZERO) -> TRUE;\n"
00403       + "        (ZERO, POS) -> FALSE;\n"
00404       + "        (POS, NEG) -> FALSE;\n"
00405       + "        (POS, ZERO) -> FALSE;\n"
00406       + "        (POS, POS) -> {TRUE, FALSE};\n"
00407       + "      end\n"
00408       + "    test != neq \n"
00409       + "      begin\n"
00410       + "        (NEG, NEG) -> {TRUE, FALSE};\n"
00411       + "        (NEG, ZERO) -> TRUE;\n"
00412       + "        (NEG, POS) -> TRUE;\n"
00413       + "        (ZERO, NEG) -> TRUE;\n"
00414       + "        (ZERO, ZERO) -> FALSE;\n"
00415       + "        (ZERO, POS) -> TRUE;\n"
00416       + "        (POS, NEG) -> TRUE;\n"
00417       + "        (POS, ZERO) -> TRUE;\n"
00418       + "        (POS, POS) -> {TRUE, FALSE};\n"
00419       + "      end\n"
00420       + "    test < lt \n"
00421       + "      begin\n"
00422       + "        (NEG, NEG) -> {TRUE, FALSE};\n"
00423       + "        (NEG, ZERO) -> TRUE;\n"
00424       + "        (NEG, POS) -> TRUE;\n"
00425       + "        (ZERO, NEG) -> FALSE;\n"
00426       + "        (ZERO, ZERO) -> FALSE;\n"
00427       + "        (ZERO, POS) -> TRUE;\n"
00428       + "        (POS, NEG) -> FALSE;\n"
00429       + "        (POS, ZERO) -> FALSE;\n"
00430       + "        (POS, POS) -> {TRUE, FALSE};\n"
00431       + "      end\n"
00432       + "    test <= le \n"
00433       + "      begin\n"
00434       + "        (NEG, NEG) -> {TRUE, FALSE};\n"
00435       + "        (NEG, ZERO) -> TRUE;\n"
00436       + "        (NEG, POS) -> TRUE;\n"
00437       + "        (ZERO, NEG) -> FALSE;\n"
00438       + "        (ZERO, ZERO) -> TRUE;\n"
00439       + "        (ZERO, POS) -> TRUE;\n"
00440       + "        (POS, NEG) -> FALSE;\n"
00441       + "        (POS, ZERO) -> FALSE;\n"
00442       + "        (POS, POS) -> {TRUE, FALSE};\n"
00443       + "      end\n"
00444       + "    test > gt \n"
00445       + "      begin\n"
00446       + "        (NEG, NEG) -> {TRUE, FALSE};\n"
00447       + "        (NEG, ZERO) -> FALSE;\n"
00448       + "        (NEG, POS) -> FALSE;\n"
00449       + "        (ZERO, NEG) -> TRUE;\n"
00450       + "        (ZERO, ZERO) -> FALSE;\n"
00451       + "        (ZERO, POS) -> FALSE;\n"
00452       + "        (POS, NEG) -> TRUE;\n"
00453       + "        (POS, ZERO) -> TRUE;\n"
00454       + "        (POS, POS) -> {TRUE, FALSE};\n"
00455       + "      end\n"
00456       + "    test >= ge \n"
00457       + "      begin\n"
00458       + "        (NEG, NEG) -> {TRUE, FALSE};\n"
00459       + "        (NEG, ZERO) -> FALSE;\n"
00460       + "        (NEG, POS) -> FALSE;\n"
00461       + "        (ZERO, NEG) -> TRUE;\n"
00462       + "        (ZERO, ZERO) -> TRUE;\n"
00463       + "        (ZERO, POS) -> FALSE;\n"
00464       + "        (POS, NEG) -> TRUE;\n"
00465       + "        (POS, ZERO) -> TRUE;\n"
00466       + "        (POS, POS) -> {TRUE, FALSE};\n"
00467       + "      end\n"
00468       + "  end\n"
00469     ;
00470   }  
00471   public static String getName() {
00472     return "Signs";
00473   }  
00474   public static int getNumOfTokens() {
00475     return 3;
00476   }  
00477   public static String getToken(int value) {
00478     switch(value) {
00479       case ZERO: return "Signs.ZERO";
00480       case NEG: return "Signs.NEG";
00481       case POS: return "Signs.POS";
00482     }
00483     return "Signs.???";
00484   }  
00485   public static boolean gt(int left$, int right$) {
00486     if (left$ == NEG && right$ == NEG) return Abstraction.choose();
00487     if (left$ == NEG && right$ == ZERO) return false;
00488     if (left$ == NEG && right$ == POS) return false;
00489     if (left$ == ZERO && right$ == NEG) return true;
00490     if (left$ == ZERO && right$ == ZERO) return false;
00491     if (left$ == ZERO && right$ == POS) return false;
00492     if (left$ == POS && right$ == NEG) return true;
00493     if (left$ == POS && right$ == ZERO) return true;
00494     if (left$ == POS && right$ == POS) return Abstraction.choose();
00495     throw new RuntimeException("Signs.gt(" + left$ + ", " + right$ + ") is undefined");
00496   }  
00497   private static byte gtNoChoose(int left, int right) {
00498     byte result = -1;
00499     switch (left) {
00500       case 0:
00501         switch (right) {
00502           case 0:
00503             result = 0;
00504             break;
00505           case 1:
00506             result = 1;
00507             break;
00508           case 2:
00509             result = 0;
00510             break;
00511         }
00512         break;
00513       case 1:
00514         switch (right) {
00515           case 0:
00516             result = 0;
00517             break;
00518           case 1:
00519             result = 2;
00520             break;
00521           case 2:
00522             result = 0;
00523             break;
00524         }
00525         break;
00526       case 2:
00527         switch (right) {
00528           case 0:
00529             result = 1;
00530             break;
00531           case 1:
00532             result = 1;
00533             break;
00534           case 2:
00535             result = 2;
00536             break;
00537         }
00538         break;
00539     }
00540     if (result == -1) throw new RuntimeException("Signs.gtNoChoose(" + left + ", " + right + ") is undefined");
00541     return result;
00542   }  
00543   public static byte gtSet(int leftTokens, int rightTokens) {
00544     byte result = -1;
00545     for (int left = 0; (1 << left) <= leftTokens; left++) {
00546       if ((leftTokens & (1 << left)) == 0) continue;
00547       for (int right = 0; (1 << right) <= rightTokens; right++) {
00548         if ((rightTokens & (1 << right)) != 0) {
00549           if (result == -1) result = gtNoChoose(left, right);
00550           else result = Abstraction.meetTest(result, gtNoChoose(left, right));
00551         }
00552       }
00553     }
00554     return result;
00555   }  
00556   public static boolean isOne2One(int value) {
00557     switch(value) {
00558       case ZERO: return true;
00559     }
00560     return false;
00561   }  
00562   public static boolean le(int left$, int right$) {
00563     if (left$ == NEG && right$ == NEG) return Abstraction.choose();
00564     if (left$ == NEG && right$ == ZERO) return true;
00565     if (left$ == NEG && right$ == POS) return true;
00566     if (left$ == ZERO && right$ == NEG) return false;
00567     if (left$ == ZERO && right$ == ZERO) return true;
00568     if (left$ == ZERO && right$ == POS) return true;
00569     if (left$ == POS && right$ == NEG) return false;
00570     if (left$ == POS && right$ == ZERO) return false;
00571     if (left$ == POS && right$ == POS) return Abstraction.choose();
00572     throw new RuntimeException("Signs.le(" + left$ + ", " + right$ + ") is undefined");
00573   }  
00574   private static byte leNoChoose(int left, int right) {
00575     byte result = -1;
00576     switch (left) {
00577       case 0:
00578         switch (right) {
00579           case 0:
00580             result = 1;
00581             break;
00582           case 1:
00583             result = 0;
00584             break;
00585           case 2:
00586             result = 1;
00587             break;
00588         }
00589         break;
00590       case 1:
00591         switch (right) {
00592           case 0:
00593             result = 1;
00594             break;
00595           case 1:
00596             result = 2;
00597             break;
00598           case 2:
00599             result = 1;
00600             break;
00601         }
00602         break;
00603       case 2:
00604         switch (right) {
00605           case 0:
00606             result = 0;
00607             break;
00608           case 1:
00609             result = 0;
00610             break;
00611           case 2:
00612             result = 2;
00613             break;
00614         }
00615         break;
00616     }
00617     if (result == -1) throw new RuntimeException("Signs.leNoChoose(" + left + ", " + right + ") is undefined");
00618     return result;
00619   }  
00620   public static byte leSet(int leftTokens, int rightTokens) {
00621     byte result = -1;
00622     for (int left = 0; (1 << left) <= leftTokens; left++) {
00623       if ((leftTokens & (1 << left)) == 0) continue;
00624       for (int right = 0; (1 << right) <= rightTokens; right++) {
00625         if ((rightTokens & (1 << right)) != 0) {
00626           if (result == -1) result = leNoChoose(left, right);
00627           else result = Abstraction.meetTest(result, leNoChoose(left, right));
00628         }
00629       }
00630     }
00631     return result;
00632   }  
00633   public static boolean lt(int left$, int right$) {
00634     if (left$ == NEG && right$ == NEG) return Abstraction.choose();
00635     if (left$ == NEG && right$ == ZERO) return true;
00636     if (left$ == NEG && right$ == POS) return true;
00637     if (left$ == ZERO && right$ == NEG) return false;
00638     if (left$ == ZERO && right$ == ZERO) return false;
00639     if (left$ == ZERO && right$ == POS) return true;
00640     if (left$ == POS && right$ == NEG) return false;
00641     if (left$ == POS && right$ == ZERO) return false;
00642     if (left$ == POS && right$ == POS) return Abstraction.choose();
00643     throw new RuntimeException("Signs.lt(" + left$ + ", " + right$ + ") is undefined");
00644   }  
00645   private static byte ltNoChoose(int left, int right) {
00646     byte result = -1;
00647     switch (left) {
00648       case 0:
00649         switch (right) {
00650           case 0:
00651             result = 0;
00652             break;
00653           case 1:
00654             result = 0;
00655             break;
00656           case 2:
00657             result = 1;
00658             break;
00659         }
00660         break;
00661       case 1:
00662         switch (right) {
00663           case 0:
00664             result = 1;
00665             break;
00666           case 1:
00667             result = 2;
00668             break;
00669           case 2:
00670             result = 1;
00671             break;
00672         }
00673         break;
00674       case 2:
00675         switch (right) {
00676           case 0:
00677             result = 0;
00678             break;
00679           case 1:
00680             result = 0;
00681             break;
00682           case 2:
00683             result = 2;
00684             break;
00685         }
00686         break;
00687     }
00688     if (result == -1) throw new RuntimeException("Signs.ltNoChoose(" + left + ", " + right + ") is undefined");
00689     return result;
00690   }  
00691   public static byte ltSet(int leftTokens, int rightTokens) {
00692     byte result = -1;
00693     for (int left = 0; (1 << left) <= leftTokens; left++) {
00694       if ((leftTokens & (1 << left)) == 0) continue;
00695       for (int right = 0; (1 << right) <= rightTokens; right++) {
00696         if ((rightTokens & (1 << right)) != 0) {
00697           if (result == -1) result = ltNoChoose(left, right);
00698           else result = Abstraction.meetTest(result, ltNoChoose(left, right));
00699         }
00700       }
00701     }
00702     return result;
00703   }  
00704   public static int mul(int left$, int right$) {
00705     if (left$ == NEG && right$ == NEG) return POS;
00706     if (left$ == NEG && right$ == ZERO) return ZERO;
00707     if (left$ == NEG && right$ == POS) return NEG;
00708     if (left$ == ZERO && right$ == NEG) return ZERO;
00709     if (left$ == ZERO && right$ == ZERO) return ZERO;
00710     if (left$ == ZERO && right$ == POS) return ZERO;
00711     if (left$ == POS && right$ == NEG) return NEG;
00712     if (left$ == POS && right$ == ZERO) return ZERO;
00713     if (left$ == POS && right$ == POS) return POS;
00714     throw new RuntimeException("Signs.mul(" + left$ + ", " + right$ + ") is undefined");
00715   }  
00716   private static int mulNoChoose(int left, int right) {
00717     int result = 0;
00718     switch (left) {
00719       case 0:
00720         switch (right) {
00721           case 0:
00722             result = 1;
00723             break;
00724           case 1:
00725             result = 1;
00726             break;
00727           case 2:
00728             result = 1;
00729             break;
00730         }
00731         break;
00732       case 1:
00733         switch (right) {
00734           case 0:
00735             result = 1;
00736             break;
00737           case 1:
00738             result = 4;
00739             break;
00740           case 2:
00741             result = 2;
00742             break;
00743         }
00744         break;
00745       case 2:
00746         switch (right) {
00747           case 0:
00748             result = 1;
00749             break;
00750           case 1:
00751             result = 2;
00752             break;
00753           case 2:
00754             result = 4;
00755             break;
00756         }
00757         break;
00758     }
00759     if (result == 0) throw new RuntimeException("Signs.mulNoChoose(" + left + ", " + right + ") is undefined");
00760     return result;
00761   }  
00762   public static int mulSet(int leftTokens, int rightTokens) {
00763     int result = -1;
00764     for (int left = 0; (1 << left) <= leftTokens; left++) {
00765       if ((leftTokens & (1 << left)) == 0) continue;
00766       for (int right = 0; (1 << right) <= rightTokens; right++) {
00767         if ((rightTokens & (1 << right)) != 0) {
00768           if (result == -1) result = mulNoChoose(left, right);
00769           else result = Abstraction.meetArith(result, mulNoChoose(left, right));
00770         }
00771       }
00772     }
00773     return result;
00774   }  
00775   public static boolean ne(int left$, int right$) {
00776     if (left$ == NEG && right$ == NEG) return Abstraction.choose();
00777     if (left$ == NEG && right$ == ZERO) return true;
00778     if (left$ == NEG && right$ == POS) return true;
00779     if (left$ == ZERO && right$ == NEG) return true;
00780     if (left$ == ZERO && right$ == ZERO) return false;
00781     if (left$ == ZERO && right$ == POS) return true;
00782     if (left$ == POS && right$ == NEG) return true;
00783     if (left$ == POS && right$ == ZERO) return true;
00784     if (left$ == POS && right$ == POS) return Abstraction.choose();
00785     throw new RuntimeException("Signs.ne(" + left$ + ", " + right$ + ") is undefined");
00786   }  
00787   private static byte neNoChoose(int left, int right) {
00788     byte result = -1;
00789     switch (left) {
00790       case 0:
00791         switch (right) {
00792           case 0:
00793             result = 0;
00794             break;
00795           case 1:
00796             result = 1;
00797             break;
00798           case 2:
00799             result = 1;
00800             break;
00801         }
00802         break;
00803       case 1:
00804         switch (right) {
00805           case 0:
00806             result = 1;
00807             break;
00808           case 1:
00809             result = 2;
00810             break;
00811           case 2:
00812             result = 1;
00813             break;
00814         }
00815         break;
00816       case 2:
00817         switch (right) {
00818           case 0:
00819             result = 1;
00820             break;
00821           case 1:
00822             result = 1;
00823             break;
00824           case 2:
00825             result = 2;
00826             break;
00827         }
00828         break;
00829     }
00830     if (result == -1) throw new RuntimeException("Signs.neNoChoose(" + left + ", " + right + ") is undefined");
00831     return result;
00832   }  
00833   public static byte neSet(int leftTokens, int rightTokens) {
00834     byte result = -1;
00835     for (int left = 0; (1 << left) <= leftTokens; left++) {
00836       if ((leftTokens & (1 << left)) == 0) continue;
00837       for (int right = 0; (1 << right) <= rightTokens; right++) {
00838         if ((rightTokens & (1 << right)) != 0) {
00839           if (result == -1) result = neNoChoose(left, right);
00840           else result = Abstraction.meetTest(result, neNoChoose(left, right));
00841         }
00842       }
00843     }
00844     return result;
00845   }  
00846   public static int sub(int left$, int right$) {
00847     if (left$ == NEG && right$ == NEG) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00848     if (left$ == NEG && right$ == ZERO) return NEG;
00849     if (left$ == NEG && right$ == POS) return NEG;
00850     if (left$ == ZERO && right$ == NEG) return POS;
00851     if (left$ == ZERO && right$ == ZERO) return ZERO;
00852     if (left$ == ZERO && right$ == POS) return NEG;
00853     if (left$ == POS && right$ == NEG) return POS;
00854     if (left$ == POS && right$ == ZERO) return POS;
00855     if (left$ == POS && right$ == POS) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00856     throw new RuntimeException("Signs.sub(" + left$ + ", " + right$ + ") is undefined");
00857   }  
00858   private static int subNoChoose(int left, int right) {
00859     int result = 0;
00860     switch (left) {
00861       case 0:
00862         switch (right) {
00863           case 0:
00864             result = 1;
00865             break;
00866           case 1:
00867             result = 4;
00868             break;
00869           case 2:
00870             result = 2;
00871             break;
00872         }
00873         break;
00874       case 1:
00875         switch (right) {
00876           case 0:
00877             result = 2;
00878             break;
00879           case 1:
00880             result = 7;
00881             break;
00882           case 2:
00883             result = 2;
00884             break;
00885         }
00886         break;
00887       case 2:
00888         switch (right) {
00889           case 0:
00890             result = 4;
00891             break;
00892           case 1:
00893             result = 4;
00894             break;
00895           case 2:
00896             result = 7;
00897             break;
00898         }
00899         break;
00900     }
00901     if (result == 0) throw new RuntimeException("Signs.subNoChoose(" + left + ", " + right + ") is undefined");
00902     return result;
00903   }  
00904   public static int subSet(int leftTokens, int rightTokens) {
00905     int result = -1;
00906     for (int left = 0; (1 << left) <= leftTokens; left++) {
00907       if ((leftTokens & (1 << left)) == 0) continue;
00908       for (int right = 0; (1 << right) <= rightTokens; right++) {
00909         if ((rightTokens & (1 << right)) != 0) {
00910           if (result == -1) result = subNoChoose(left, right);
00911           else result = Abstraction.meetArith(result, subNoChoose(left, right));
00912         }
00913       }
00914     }
00915     return result;
00916   }  
00917   public String toString() {
00918     return getName();
00919   }  
00920   public static Signs v() {
00921     return v;
00922   }  
00923 }