Signs.java Source File

00001 package edu.ksu.cis.bandera.abstraction.lib.integral;
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 IntegralAbstraction {
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(long 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 Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00124     if (left$ == NEG && right$ == ZERO) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00125     if (left$ == NEG && right$ == POS) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << 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 Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00130     if (left$ == POS && right$ == ZERO) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00131     if (left$ == POS && right$ == POS) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
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 = 7;
00157             break;
00158           case 2:
00159             result = 7;
00160             break;
00161         }
00162         break;
00163       case 2:
00164         switch (right) {
00165           case 0:
00166             result = 7;
00167             break;
00168           case 1:
00169             result = 7;
00170             break;
00171           case 2:
00172             result = 7;
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 integral \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) -> {NEG, ZERO, POS};\n"
00387       + "        (NEG, ZERO) -> T;\n"
00388       + "        (NEG, POS) -> {NEG, ZERO, POS};\n"
00389       + "        (ZERO, NEG) -> ZERO;\n"
00390       + "        (ZERO, ZERO) -> T;\n"
00391       + "        (ZERO, POS) -> ZERO;\n"
00392       + "        (POS, NEG) -> {NEG, ZERO, POS};\n"
00393       + "        (POS, ZERO) -> T;\n"
00394       + "        (POS, POS) -> {NEG, ZERO, POS};\n"
00395       + "      end\n"
00396       + "    operator % rem \n"
00397       + "      begin\n"
00398       + "        (NEG, NEG) -> {NEG, ZERO, POS};\n"
00399       + "        (NEG, ZERO) -> T;\n"
00400       + "        (NEG, POS) -> {NEG, ZERO, POS};\n"
00401       + "        (ZERO, NEG) -> ZERO;\n"
00402       + "        (ZERO, ZERO) -> T;\n"
00403       + "        (ZERO, POS) -> ZERO;\n"
00404       + "        (POS, NEG) -> {NEG, ZERO, POS};\n"
00405       + "        (POS, ZERO) -> T;\n"
00406       + "        (POS, POS) -> {NEG, ZERO, POS};\n"
00407       + "      end\n"
00408       + "    test == eq \n"
00409       + "      begin\n"
00410       + "        (NEG, NEG) -> {TRUE, FALSE};\n"
00411       + "        (NEG, ZERO) -> FALSE;\n"
00412       + "        (NEG, POS) -> FALSE;\n"
00413       + "        (ZERO, NEG) -> FALSE;\n"
00414       + "        (ZERO, ZERO) -> TRUE;\n"
00415       + "        (ZERO, POS) -> FALSE;\n"
00416       + "        (POS, NEG) -> FALSE;\n"
00417       + "        (POS, ZERO) -> FALSE;\n"
00418       + "        (POS, POS) -> {TRUE, FALSE};\n"
00419       + "      end\n"
00420       + "    test != neq \n"
00421       + "      begin\n"
00422       + "        (NEG, NEG) -> {TRUE, FALSE};\n"
00423       + "        (NEG, ZERO) -> TRUE;\n"
00424       + "        (NEG, POS) -> TRUE;\n"
00425       + "        (ZERO, NEG) -> TRUE;\n"
00426       + "        (ZERO, ZERO) -> FALSE;\n"
00427       + "        (ZERO, POS) -> TRUE;\n"
00428       + "        (POS, NEG) -> TRUE;\n"
00429       + "        (POS, ZERO) -> TRUE;\n"
00430       + "        (POS, POS) -> {TRUE, FALSE};\n"
00431       + "      end\n"
00432       + "    test < lt \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) -> FALSE;\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 <= le \n"
00445       + "      begin\n"
00446       + "        (NEG, NEG) -> {TRUE, FALSE};\n"
00447       + "        (NEG, ZERO) -> TRUE;\n"
00448       + "        (NEG, POS) -> TRUE;\n"
00449       + "        (ZERO, NEG) -> FALSE;\n"
00450       + "        (ZERO, ZERO) -> TRUE;\n"
00451       + "        (ZERO, POS) -> TRUE;\n"
00452       + "        (POS, NEG) -> FALSE;\n"
00453       + "        (POS, ZERO) -> FALSE;\n"
00454       + "        (POS, POS) -> {TRUE, FALSE};\n"
00455       + "      end\n"
00456       + "    test > gt \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) -> FALSE;\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       + "    test >= ge \n"
00469       + "      begin\n"
00470       + "        (NEG, NEG) -> {TRUE, FALSE};\n"
00471       + "        (NEG, ZERO) -> FALSE;\n"
00472       + "        (NEG, POS) -> FALSE;\n"
00473       + "        (ZERO, NEG) -> TRUE;\n"
00474       + "        (ZERO, ZERO) -> TRUE;\n"
00475       + "        (ZERO, POS) -> FALSE;\n"
00476       + "        (POS, NEG) -> TRUE;\n"
00477       + "        (POS, ZERO) -> TRUE;\n"
00478       + "        (POS, POS) -> {TRUE, FALSE};\n"
00479       + "      end\n"
00480       + "  end\n"
00481     ;
00482   }  
00483   public static String getName() {
00484     return "Signs";
00485   }  
00486   public static int getNumOfTokens() {
00487     return 3;
00488   }  
00489   public static String getToken(int value) {
00490     switch(value) {
00491       case ZERO: return "Signs.ZERO";
00492       case NEG: return "Signs.NEG";
00493       case POS: return "Signs.POS";
00494     }
00495     return "Signs.???";
00496   }  
00497   public static boolean gt(int left$, int right$) {
00498     if (left$ == NEG && right$ == NEG) return Abstraction.choose();
00499     if (left$ == NEG && right$ == ZERO) return false;
00500     if (left$ == NEG && right$ == POS) return false;
00501     if (left$ == ZERO && right$ == NEG) return true;
00502     if (left$ == ZERO && right$ == ZERO) return false;
00503     if (left$ == ZERO && right$ == POS) return false;
00504     if (left$ == POS && right$ == NEG) return true;
00505     if (left$ == POS && right$ == ZERO) return true;
00506     if (left$ == POS && right$ == POS) return Abstraction.choose();
00507     throw new RuntimeException("Signs.gt(" + left$ + ", " + right$ + ") is undefined");
00508   }  
00509   private static byte gtNoChoose(int left, int right) {
00510     byte result = -1;
00511     switch (left) {
00512       case 0:
00513         switch (right) {
00514           case 0:
00515             result = 0;
00516             break;
00517           case 1:
00518             result = 1;
00519             break;
00520           case 2:
00521             result = 0;
00522             break;
00523         }
00524         break;
00525       case 1:
00526         switch (right) {
00527           case 0:
00528             result = 0;
00529             break;
00530           case 1:
00531             result = 2;
00532             break;
00533           case 2:
00534             result = 0;
00535             break;
00536         }
00537         break;
00538       case 2:
00539         switch (right) {
00540           case 0:
00541             result = 1;
00542             break;
00543           case 1:
00544             result = 1;
00545             break;
00546           case 2:
00547             result = 2;
00548             break;
00549         }
00550         break;
00551     }
00552     if (result == -1) throw new RuntimeException("Signs.gtNoChoose(" + left + ", " + right + ") is undefined");
00553     return result;
00554   }  
00555   public static byte gtSet(int leftTokens, int rightTokens) {
00556     byte result = -1;
00557     for (int left = 0; (1 << left) <= leftTokens; left++) {
00558       if ((leftTokens & (1 << left)) == 0) continue;
00559       for (int right = 0; (1 << right) <= rightTokens; right++) {
00560         if ((rightTokens & (1 << right)) != 0) {
00561           if (result == -1) result = gtNoChoose(left, right);
00562           else result = Abstraction.meetTest(result, gtNoChoose(left, right));
00563         }
00564       }
00565     }
00566     return result;
00567   }  
00568   public static boolean isOne2One(int value) {
00569     switch(value) {
00570       case ZERO: return true;
00571     }
00572     return false;
00573   }  
00574   public static boolean le(int left$, int right$) {
00575     if (left$ == NEG && right$ == NEG) return Abstraction.choose();
00576     if (left$ == NEG && right$ == ZERO) return true;
00577     if (left$ == NEG && right$ == POS) return true;
00578     if (left$ == ZERO && right$ == NEG) return false;
00579     if (left$ == ZERO && right$ == ZERO) return true;
00580     if (left$ == ZERO && right$ == POS) return true;
00581     if (left$ == POS && right$ == NEG) return false;
00582     if (left$ == POS && right$ == ZERO) return false;
00583     if (left$ == POS && right$ == POS) return Abstraction.choose();
00584     throw new RuntimeException("Signs.le(" + left$ + ", " + right$ + ") is undefined");
00585   }  
00586   private static byte leNoChoose(int left, int right) {
00587     byte result = -1;
00588     switch (left) {
00589       case 0:
00590         switch (right) {
00591           case 0:
00592             result = 1;
00593             break;
00594           case 1:
00595             result = 0;
00596             break;
00597           case 2:
00598             result = 1;
00599             break;
00600         }
00601         break;
00602       case 1:
00603         switch (right) {
00604           case 0:
00605             result = 1;
00606             break;
00607           case 1:
00608             result = 2;
00609             break;
00610           case 2:
00611             result = 1;
00612             break;
00613         }
00614         break;
00615       case 2:
00616         switch (right) {
00617           case 0:
00618             result = 0;
00619             break;
00620           case 1:
00621             result = 0;
00622             break;
00623           case 2:
00624             result = 2;
00625             break;
00626         }
00627         break;
00628     }
00629     if (result == -1) throw new RuntimeException("Signs.leNoChoose(" + left + ", " + right + ") is undefined");
00630     return result;
00631   }  
00632   public static byte leSet(int leftTokens, int rightTokens) {
00633     byte result = -1;
00634     for (int left = 0; (1 << left) <= leftTokens; left++) {
00635       if ((leftTokens & (1 << left)) == 0) continue;
00636       for (int right = 0; (1 << right) <= rightTokens; right++) {
00637         if ((rightTokens & (1 << right)) != 0) {
00638           if (result == -1) result = leNoChoose(left, right);
00639           else result = Abstraction.meetTest(result, leNoChoose(left, right));
00640         }
00641       }
00642     }
00643     return result;
00644   }  
00645   public static boolean lt(int left$, int right$) {
00646     if (left$ == NEG && right$ == NEG) return Abstraction.choose();
00647     if (left$ == NEG && right$ == ZERO) return true;
00648     if (left$ == NEG && right$ == POS) return true;
00649     if (left$ == ZERO && right$ == NEG) return false;
00650     if (left$ == ZERO && right$ == ZERO) return false;
00651     if (left$ == ZERO && right$ == POS) return true;
00652     if (left$ == POS && right$ == NEG) return false;
00653     if (left$ == POS && right$ == ZERO) return false;
00654     if (left$ == POS && right$ == POS) return Abstraction.choose();
00655     throw new RuntimeException("Signs.lt(" + left$ + ", " + right$ + ") is undefined");
00656   }  
00657   private static byte ltNoChoose(int left, int right) {
00658     byte result = -1;
00659     switch (left) {
00660       case 0:
00661         switch (right) {
00662           case 0:
00663             result = 0;
00664             break;
00665           case 1:
00666             result = 0;
00667             break;
00668           case 2:
00669             result = 1;
00670             break;
00671         }
00672         break;
00673       case 1:
00674         switch (right) {
00675           case 0:
00676             result = 1;
00677             break;
00678           case 1:
00679             result = 2;
00680             break;
00681           case 2:
00682             result = 1;
00683             break;
00684         }
00685         break;
00686       case 2:
00687         switch (right) {
00688           case 0:
00689             result = 0;
00690             break;
00691           case 1:
00692             result = 0;
00693             break;
00694           case 2:
00695             result = 2;
00696             break;
00697         }
00698         break;
00699     }
00700     if (result == -1) throw new RuntimeException("Signs.ltNoChoose(" + left + ", " + right + ") is undefined");
00701     return result;
00702   }  
00703   public static byte ltSet(int leftTokens, int rightTokens) {
00704     byte result = -1;
00705     for (int left = 0; (1 << left) <= leftTokens; left++) {
00706       if ((leftTokens & (1 << left)) == 0) continue;
00707       for (int right = 0; (1 << right) <= rightTokens; right++) {
00708         if ((rightTokens & (1 << right)) != 0) {
00709           if (result == -1) result = ltNoChoose(left, right);
00710           else result = Abstraction.meetTest(result, ltNoChoose(left, right));
00711         }
00712       }
00713     }
00714     return result;
00715   }  
00716   public static int mul(int left$, int right$) {
00717     if (left$ == NEG && right$ == NEG) return POS;
00718     if (left$ == NEG && right$ == ZERO) return ZERO;
00719     if (left$ == NEG && right$ == POS) return NEG;
00720     if (left$ == ZERO && right$ == NEG) return ZERO;
00721     if (left$ == ZERO && right$ == ZERO) return ZERO;
00722     if (left$ == ZERO && right$ == POS) return ZERO;
00723     if (left$ == POS && right$ == NEG) return NEG;
00724     if (left$ == POS && right$ == ZERO) return ZERO;
00725     if (left$ == POS && right$ == POS) return POS;
00726     throw new RuntimeException("Signs.mul(" + left$ + ", " + right$ + ") is undefined");
00727   }  
00728   private static int mulNoChoose(int left, int right) {
00729     int result = 0;
00730     switch (left) {
00731       case 0:
00732         switch (right) {
00733           case 0:
00734             result = 1;
00735             break;
00736           case 1:
00737             result = 1;
00738             break;
00739           case 2:
00740             result = 1;
00741             break;
00742         }
00743         break;
00744       case 1:
00745         switch (right) {
00746           case 0:
00747             result = 1;
00748             break;
00749           case 1:
00750             result = 4;
00751             break;
00752           case 2:
00753             result = 2;
00754             break;
00755         }
00756         break;
00757       case 2:
00758         switch (right) {
00759           case 0:
00760             result = 1;
00761             break;
00762           case 1:
00763             result = 2;
00764             break;
00765           case 2:
00766             result = 4;
00767             break;
00768         }
00769         break;
00770     }
00771     if (result == 0) throw new RuntimeException("Signs.mulNoChoose(" + left + ", " + right + ") is undefined");
00772     return result;
00773   }  
00774   public static int mulSet(int leftTokens, int rightTokens) {
00775     int result = -1;
00776     for (int left = 0; (1 << left) <= leftTokens; left++) {
00777       if ((leftTokens & (1 << left)) == 0) continue;
00778       for (int right = 0; (1 << right) <= rightTokens; right++) {
00779         if ((rightTokens & (1 << right)) != 0) {
00780           if (result == -1) result = mulNoChoose(left, right);
00781           else result = Abstraction.meetArith(result, mulNoChoose(left, right));
00782         }
00783       }
00784     }
00785     return result;
00786   }  
00787   public static boolean ne(int left$, int right$) {
00788     if (left$ == NEG && right$ == NEG) return Abstraction.choose();
00789     if (left$ == NEG && right$ == ZERO) return true;
00790     if (left$ == NEG && right$ == POS) return true;
00791     if (left$ == ZERO && right$ == NEG) return true;
00792     if (left$ == ZERO && right$ == ZERO) return false;
00793     if (left$ == ZERO && right$ == POS) return true;
00794     if (left$ == POS && right$ == NEG) return true;
00795     if (left$ == POS && right$ == ZERO) return true;
00796     if (left$ == POS && right$ == POS) return Abstraction.choose();
00797     throw new RuntimeException("Signs.ne(" + left$ + ", " + right$ + ") is undefined");
00798   }  
00799   private static byte neNoChoose(int left, int right) {
00800     byte result = -1;
00801     switch (left) {
00802       case 0:
00803         switch (right) {
00804           case 0:
00805             result = 0;
00806             break;
00807           case 1:
00808             result = 1;
00809             break;
00810           case 2:
00811             result = 1;
00812             break;
00813         }
00814         break;
00815       case 1:
00816         switch (right) {
00817           case 0:
00818             result = 1;
00819             break;
00820           case 1:
00821             result = 2;
00822             break;
00823           case 2:
00824             result = 1;
00825             break;
00826         }
00827         break;
00828       case 2:
00829         switch (right) {
00830           case 0:
00831             result = 1;
00832             break;
00833           case 1:
00834             result = 1;
00835             break;
00836           case 2:
00837             result = 2;
00838             break;
00839         }
00840         break;
00841     }
00842     if (result == -1) throw new RuntimeException("Signs.neNoChoose(" + left + ", " + right + ") is undefined");
00843     return result;
00844   }  
00845   public static byte neSet(int leftTokens, int rightTokens) {
00846     byte result = -1;
00847     for (int left = 0; (1 << left) <= leftTokens; left++) {
00848       if ((leftTokens & (1 << left)) == 0) continue;
00849       for (int right = 0; (1 << right) <= rightTokens; right++) {
00850         if ((rightTokens & (1 << right)) != 0) {
00851           if (result == -1) result = neNoChoose(left, right);
00852           else result = Abstraction.meetTest(result, neNoChoose(left, right));
00853         }
00854       }
00855     }
00856     return result;
00857   }  
00858   public static int rem(int left$, int right$) {
00859     if (left$ == NEG && right$ == NEG) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00860     if (left$ == NEG && right$ == ZERO) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00861     if (left$ == NEG && right$ == POS) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00862     if (left$ == ZERO && right$ == NEG) return ZERO;
00863     if (left$ == ZERO && right$ == ZERO) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00864     if (left$ == ZERO && right$ == POS) return ZERO;
00865     if (left$ == POS && right$ == NEG) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00866     if (left$ == POS && right$ == ZERO) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00867     if (left$ == POS && right$ == POS) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00868     throw new RuntimeException("Signs.rem(" + left$ + ", " + right$ + ") is undefined");
00869   }  
00870   private static int remNoChoose(int left, int right) {
00871     int result = 0;
00872     switch (left) {
00873       case 0:
00874         switch (right) {
00875           case 0:
00876             result = 7;
00877             break;
00878           case 1:
00879             result = 1;
00880             break;
00881           case 2:
00882             result = 1;
00883             break;
00884         }
00885         break;
00886       case 1:
00887         switch (right) {
00888           case 0:
00889             result = 7;
00890             break;
00891           case 1:
00892             result = 7;
00893             break;
00894           case 2:
00895             result = 7;
00896             break;
00897         }
00898         break;
00899       case 2:
00900         switch (right) {
00901           case 0:
00902             result = 7;
00903             break;
00904           case 1:
00905             result = 7;
00906             break;
00907           case 2:
00908             result = 7;
00909             break;
00910         }
00911         break;
00912     }
00913     if (result == 0) throw new RuntimeException("Signs.remNoChoose(" + left + ", " + right + ") is undefined");
00914     return result;
00915   }  
00916   public static int remSet(int leftTokens, int rightTokens) {
00917     int result = -1;
00918     for (int left = 0; (1 << left) <= leftTokens; left++) {
00919       if ((leftTokens & (1 << left)) == 0) continue;
00920       for (int right = 0; (1 << right) <= rightTokens; right++) {
00921         if ((rightTokens & (1 << right)) != 0) {
00922           if (result == -1) result = remNoChoose(left, right);
00923           else result = Abstraction.meetArith(result, remNoChoose(left, right));
00924         }
00925       }
00926     }
00927     return result;
00928   }  
00929   public static int sub(int left$, int right$) {
00930     if (left$ == NEG && right$ == NEG) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00931     if (left$ == NEG && right$ == ZERO) return NEG;
00932     if (left$ == NEG && right$ == POS) return NEG;
00933     if (left$ == ZERO && right$ == NEG) return POS;
00934     if (left$ == ZERO && right$ == ZERO) return ZERO;
00935     if (left$ == ZERO && right$ == POS) return NEG;
00936     if (left$ == POS && right$ == NEG) return POS;
00937     if (left$ == POS && right$ == ZERO) return POS;
00938     if (left$ == POS && right$ == POS) return Abstraction.choose((1 << ZERO) | (1 << POS) | (1 << NEG));
00939     throw new RuntimeException("Signs.sub(" + left$ + ", " + right$ + ") is undefined");
00940   }  
00941   private static int subNoChoose(int left, int right) {
00942     int result = 0;
00943     switch (left) {
00944       case 0:
00945         switch (right) {
00946           case 0:
00947             result = 1;
00948             break;
00949           case 1:
00950             result = 4;
00951             break;
00952           case 2:
00953             result = 2;
00954             break;
00955         }
00956         break;
00957       case 1:
00958         switch (right) {
00959           case 0:
00960             result = 2;
00961             break;
00962           case 1:
00963             result = 7;
00964             break;
00965           case 2:
00966             result = 2;
00967             break;
00968         }
00969         break;
00970       case 2:
00971         switch (right) {
00972           case 0:
00973             result = 4;
00974             break;
00975           case 1:
00976             result = 4;
00977             break;
00978           case 2:
00979             result = 7;
00980             break;
00981         }
00982         break;
00983     }
00984     if (result == 0) throw new RuntimeException("Signs.subNoChoose(" + left + ", " + right + ") is undefined");
00985     return result;
00986   }  
00987   public static int subSet(int leftTokens, int rightTokens) {
00988     int result = -1;
00989     for (int left = 0; (1 << left) <= leftTokens; left++) {
00990       if ((leftTokens & (1 << left)) == 0) continue;
00991       for (int right = 0; (1 << right) <= rightTokens; right++) {
00992         if ((rightTokens & (1 << right)) != 0) {
00993           if (result == -1) result = subNoChoose(left, right);
00994           else result = Abstraction.meetArith(result, subNoChoose(left, right));
00995         }
00996       }
00997     }
00998     return result;
00999   }  
01000   public String toString() {
01001     return getName();
01002   }  
01003   public static Signs v() {
01004     return v;
01005   }  
01006 }