org.sat4j.core_2.3.0.v20110329

16:49:47.054 INFO  jd.cli.Main - Decompiling org.sat4j.core_2.3.0.v20110329.jar
package org.sat4j;

class AbstractLauncher$1
  extends Thread
{
  private final AbstractLauncher this$0;
  
  AbstractLauncher$1(AbstractLauncher paramAbstractLauncher) {}
  
  public void run()
  {
    this$0.displayResult();
  }
}

/* Location:
 * Qualified Name:     org.sat4j.AbstractLauncher.1
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j;

class AbstractLauncher$2
  extends Thread
{
  private final AbstractLauncher this$0;
  
  AbstractLauncher$2(AbstractLauncher paramAbstractLauncher) {}
  
  public void run()
  {
    this$0.displayResult();
  }
}

/* Location:
 * Qualified Name:     org.sat4j.AbstractLauncher.2
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j;

import java.io.BufferedReader;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.ObjectInputStream;
import java.io.PrintStream;
import java.io.PrintWriter;
import java.io.Serializable;
import java.net.URL;
import java.util.Properties;
import org.sat4j.core.ASolverFactory;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;

public abstract class AbstractLauncher
  implements Serializable
{
  private static final long serialVersionUID = 1L;
  public static final String SOLUTION_PREFIX = "v ";
  public static final String ANSWER_PREFIX = "s ";
  public static final String COMMENT_PREFIX = "c ";
  protected long beginTime;
  protected ExitCode exitCode = ExitCode.UNKNOWN;
  protected Reader reader;
  protected transient PrintWriter out = new PrintWriter(System.out, true);
  protected transient Thread shutdownHook = new Thread()
  {
    public void run()
    {
      displayResult();
    }
  };
  protected ISolver solver;
  private boolean silent = false;
  
  protected AbstractLauncher()
  {
    Runtime.getRuntime().addShutdownHook(shutdownHook);
  }
  
  protected void displayResult()
  {
    if (solver != null)
    {
      System.out.flush();
      out.flush();
      double d = (System.currentTimeMillis() - beginTime) / 1000.0D;
      solver.printStat(out, "c ");
      solver.printInfos(out, "c ");
      out.println("s " + exitCode);
      if (exitCode == ExitCode.SATISFIABLE)
      {
        int[] arrayOfInt = solver.model();
        out.print("v ");
        reader.decode(arrayOfInt, out);
        out.println();
      }
      log("Total wall clock time (in seconds) : " + d);
    }
  }
  
  public abstract void usage();
  
  protected final void displayHeader()
  {
    displayLicense();
    URL localURL = AbstractLauncher.class.getResource("/sat4j.version");
    Object localObject1;
    if (localURL == null)
    {
      log("no version file found!!!");
    }
    else
    {
      localObject1 = null;
      try
      {
        localObject1 = new BufferedReader(new InputStreamReader(localURL.openStream()));
        log("version " + ((BufferedReader)localObject1).readLine());
        if (localObject1 != null) {
          try
          {
            ((BufferedReader)localObject1).close();
          }
          catch (IOException localIOException1)
          {
            log("c ERROR: " + localIOException1.getMessage());
          }
        }
        localObject1 = System.getProperties();
      }
      catch (IOException localIOException2)
      {
        log("c ERROR: " + localIOException2.getMessage());
      }
      finally
      {
        if (localObject1 != null) {
          try
          {
            ((BufferedReader)localObject1).close();
          }
          catch (IOException localIOException4)
          {
            log("c ERROR: " + localIOException4.getMessage());
          }
        }
      }
    }
    String[] arrayOfString = { "java.runtime.name", "java.vm.name", "java.vm.version", "java.vm.vendor", "sun.arch.data.model", "java.version", "os.name", "os.version", "os.arch" };
    for (int i = 0; i < arrayOfString.length; i++)
    {
      String str = arrayOfString[i];
      log(str + (str.length() < 14 ? "\t\t" : "\t") + ((Properties)localObject1).getProperty(str));
    }
    Runtime localRuntime = Runtime.getRuntime();
    log("Free memory \t\t" + localRuntime.freeMemory());
    log("Max memory \t\t" + localRuntime.maxMemory());
    log("Total memory \t\t" + localRuntime.totalMemory());
    log("Number of processors \t" + localRuntime.availableProcessors());
  }
  
  public void displayLicense()
  {
    log("SAT4J: a SATisfiability library for Java (c) 2004-2010 Daniel Le Berre");
    log("This is free software under the dual EPL/GNU LGPL licenses.");
    log("See www.sat4j.org for details.");
  }
  
  protected IProblem readProblem(String paramString)
    throws FileNotFoundException, ParseFormatException, IOException, ContradictionException
  {
    log("solving " + paramString);
    log("reading problem ... ");
    reader = createReader(solver, paramString);
    IProblem localIProblem = reader.parseInstance(paramString);
    log("... done. Wall clock time " + (System.currentTimeMillis() - beginTime) / 1000.0D + "s.");
    log("#vars     " + localIProblem.nVars());
    log("#constraints  " + localIProblem.nConstraints());
    localIProblem.printInfos(out, "c ");
    return localIProblem;
  }
  
  protected abstract Reader createReader(ISolver paramISolver, String paramString);
  
  public void run(String[] paramArrayOfString)
  {
    try
    {
      displayHeader();
      solver = configureSolver(paramArrayOfString);
      if (solver == null)
      {
        usage();
        return;
      }
      if (!silent) {
        solver.setVerbose(true);
      }
      String str = getInstanceName(paramArrayOfString);
      if (str == null)
      {
        usage();
        return;
      }
      beginTime = System.currentTimeMillis();
      IProblem localIProblem = readProblem(str);
      try
      {
        solve(localIProblem);
      }
      catch (TimeoutException localTimeoutException)
      {
        log("timeout");
      }
    }
    catch (FileNotFoundException localFileNotFoundException)
    {
      System.err.println("FATAL " + localFileNotFoundException.getLocalizedMessage());
    }
    catch (IOException localIOException)
    {
      System.err.println("FATAL " + localIOException.getLocalizedMessage());
    }
    catch (ContradictionException localContradictionException)
    {
      exitCode = ExitCode.UNSATISFIABLE;
      log("(trivial inconsistency)");
    }
    catch (ParseFormatException localParseFormatException)
    {
      System.err.println("FATAL " + localParseFormatException.getLocalizedMessage());
    }
  }
  
  protected abstract String getInstanceName(String[] paramArrayOfString);
  
  protected abstract ISolver configureSolver(String[] paramArrayOfString);
  
  public void log(String paramString)
  {
    if (!silent) {
      out.println("c " + paramString);
    }
  }
  
  protected void solve(IProblem paramIProblem)
    throws TimeoutException
  {
    exitCode = (paramIProblem.isSatisfiable() ? ExitCode.SATISFIABLE : ExitCode.UNSATISFIABLE);
  }
  
  public final void setExitCode(ExitCode paramExitCode)
  {
    exitCode = paramExitCode;
  }
  
  public final ExitCode getExitCode()
  {
    return exitCode;
  }
  
  public final long getBeginTime()
  {
    return beginTime;
  }
  
  public final Reader getReader()
  {
    return reader;
  }
  
  public void setLogWriter(PrintWriter paramPrintWriter)
  {
    out = paramPrintWriter;
  }
  
  public PrintWriter getLogWriter()
  {
    return out;
  }
  
  protected void setSilent(boolean paramBoolean)
  {
    silent = paramBoolean;
  }
  
  private void readObject(ObjectInputStream paramObjectInputStream)
    throws IOException, ClassNotFoundException
  {
    paramObjectInputStream.defaultReadObject();
    out = new PrintWriter(System.out, true);
    shutdownHook = new Thread()
    {
      public void run()
      {
        displayResult();
      }
    };
  }
  
  protected <T extends ISolver> void showAvailableSolvers(ASolverFactory<T> paramASolverFactory)
  {
    if (paramASolverFactory != null)
    {
      log("Available solvers: ");
      String[] arrayOfString = paramASolverFactory.solverNames();
      for (int i = 0; i < arrayOfString.length; i++) {
        log(arrayOfString[i]);
      }
    }
  }
}

/* Location:
 * Qualified Name:     org.sat4j.AbstractLauncher
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j;

import java.io.PrintStream;
import java.io.PrintWriter;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IOptimizationProblem;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;

public abstract class AbstractOptimizationLauncher
  extends AbstractLauncher
{
  private static final long serialVersionUID = 1L;
  private static final String CURRENT_OPTIMUM_VALUE_PREFIX = "o ";
  private boolean incomplete = false;
  
  protected void setIncomplete(boolean paramBoolean)
  {
    incomplete = paramBoolean;
  }
  
  protected void displayResult()
  {
    displayAnswer();
    log("Total wall clock time (in seconds): " + (System.currentTimeMillis() - getBeginTime()) / 1000.0D);
  }
  
  protected void displayAnswer()
  {
    if (solver == null) {
      return;
    }
    System.out.flush();
    PrintWriter localPrintWriter = getLogWriter();
    localPrintWriter.flush();
    solver.printStat(localPrintWriter, "c ");
    solver.printInfos(localPrintWriter, "c ");
    ExitCode localExitCode = getExitCode();
    localPrintWriter.println("s " + localExitCode);
    if ((localExitCode == ExitCode.SATISFIABLE) || (localExitCode == ExitCode.OPTIMUM_FOUND) || ((incomplete) && (localExitCode == ExitCode.UPPER_BOUND)))
    {
      localPrintWriter.print("v ");
      getReader().decode(solver.model(), localPrintWriter);
      localPrintWriter.println();
      IOptimizationProblem localIOptimizationProblem = (IOptimizationProblem)solver;
      if (!localIOptimizationProblem.hasNoObjectiveFunction()) {
        log("objective function=" + localIOptimizationProblem.getObjectiveValue());
      }
    }
  }
  
  protected void solve(IProblem paramIProblem)
    throws TimeoutException
  {
    int i = 0;
    IOptimizationProblem localIOptimizationProblem = (IOptimizationProblem)paramIProblem;
    try
    {
      while (localIOptimizationProblem.admitABetterSolution())
      {
        if (i == 0)
        {
          if (localIOptimizationProblem.nonOptimalMeansSatisfiable())
          {
            setExitCode(ExitCode.SATISFIABLE);
            if (localIOptimizationProblem.hasNoObjectiveFunction()) {
              return;
            }
            log("SATISFIABLE");
          }
          else if (incomplete)
          {
            setExitCode(ExitCode.UPPER_BOUND);
          }
          i = 1;
          log("OPTIMIZING...");
        }
        log("Got one! Elapsed wall clock time (in seconds):" + (System.currentTimeMillis() - getBeginTime()) / 1000.0D);
        getLogWriter().println("o " + localIOptimizationProblem.getObjectiveValue());
        localIOptimizationProblem.discardCurrentSolution();
      }
      if (i != 0) {
        setExitCode(ExitCode.OPTIMUM_FOUND);
      } else {
        setExitCode(ExitCode.UNSATISFIABLE);
      }
    }
    catch (ContradictionException localContradictionException)
    {
      assert (i != 0);
      setExitCode(ExitCode.OPTIMUM_FOUND);
    }
  }
}

/* Location:
 * Qualified Name:     org.sat4j.AbstractOptimizationLauncher
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j;

import java.io.PrintWriter;
import org.sat4j.core.ASolverFactory;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.reader.InstanceReader;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ISolver;

public class BasicLauncher<T extends ISolver>
  extends AbstractLauncher
{
  private static final long serialVersionUID = 1L;
  private final ASolverFactory<T> factory;
  private boolean prime = false;
  
  public BasicLauncher(ASolverFactory<T> paramASolverFactory)
  {
    factory = paramASolverFactory;
  }
  
  public static void main(String[] paramArrayOfString)
  {
    BasicLauncher localBasicLauncher = new BasicLauncher(SolverFactory.instance());
    if (paramArrayOfString.length != 1)
    {
      localBasicLauncher.usage();
      return;
    }
    localBasicLauncher.run(paramArrayOfString);
    System.exit(localBasicLauncher.getExitCode().value());
  }
  
  protected ISolver configureSolver(String[] paramArrayOfString)
  {
    prime = (System.getProperty("prime") != null);
    ISolver localISolver = factory.defaultSolver();
    localISolver.setTimeout(Integer.MAX_VALUE);
    localISolver.setDBSimplificationAllowed(true);
    getLogWriter().println(localISolver.toString("c "));
    return localISolver;
  }
  
  protected Reader createReader(ISolver paramISolver, String paramString)
  {
    return new InstanceReader(paramISolver);
  }
  
  public void usage()
  {
    log("java -jar org.sat4j.core.jar <cnffile>");
  }
  
  protected String getInstanceName(String[] paramArrayOfString)
  {
    if (paramArrayOfString.length == 0) {
      return null;
    }
    return paramArrayOfString[0];
  }
  
  protected void displayResult()
  {
    super.displayResult();
    if ((prime) && (exitCode == ExitCode.SATISFIABLE))
    {
      log("For information, a prime implicant:");
      long l = System.currentTimeMillis();
      int[] arrayOfInt = solver.primeImplicant();
      out.println("c ");
      reader.decode(arrayOfInt, out);
      out.println();
      log(" prime computation time: " + (System.currentTimeMillis() - l) / 1000L + "s");
    }
  }
}

/* Location:
 * Qualified Name:     org.sat4j.BasicLauncher
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j;

public final class ExitCode
{
  public static final ExitCode OPTIMUM_FOUND = new ExitCode(30, "OPTIMUM FOUND");
  public static final ExitCode UPPER_BOUND = new ExitCode(30, "UPPER BOUND");
  public static final ExitCode SATISFIABLE = new ExitCode(10, "SATISFIABLE");
  public static final ExitCode UNKNOWN = new ExitCode(0, "UNKNOWN");
  public static final ExitCode UNSATISFIABLE = new ExitCode(20, "UNSATISFIABLE");
  private final int value;
  private final String str;
  
  private ExitCode(int paramInt, String paramString)
  {
    value = paramInt;
    str = paramString;
  }
  
  public int value()
  {
    return value;
  }
  
  public String toString()
  {
    return str;
  }
}

/* Location:
 * Qualified Name:     org.sat4j.ExitCode
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j;

import org.sat4j.core.ASolverFactory;
import org.sat4j.minisat.constraints.MixedDataStructureDanielWL;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.minisat.core.Solver;
import org.sat4j.minisat.learning.MiniSATLearning;
import org.sat4j.minisat.orders.RSATPhaseSelectionStrategy;
import org.sat4j.minisat.orders.VarOrderHeap;
import org.sat4j.minisat.restarts.ArminRestarts;
import org.sat4j.specs.ISolver;

public class LightFactory
  extends ASolverFactory<ISolver>
{
  private static final long serialVersionUID = 1460304168178023681L;
  private static LightFactory instance;
  
  private static synchronized void createInstance()
  {
    if (instance == null) {
      instance = new LightFactory();
    }
  }
  
  public static LightFactory instance()
  {
    if (instance == null) {
      createInstance();
    }
    return instance;
  }
  
  public ISolver defaultSolver()
  {
    MiniSATLearning localMiniSATLearning = new MiniSATLearning();
    Solver localSolver = new Solver(localMiniSATLearning, new MixedDataStructureDanielWL(), new VarOrderHeap(new RSATPhaseSelectionStrategy()), new ArminRestarts());
    localMiniSATLearning.setSolver(localSolver);
    localSolver.setSimplifier(EXPENSIVE_SIMPLIFICATION);
    localSolver.setSearchParams(new SearchParams(1.1D, 100));
    return localSolver;
  }
  
  public ISolver lightSolver()
  {
    return defaultSolver();
  }
  
  public static void main(String[] paramArrayOfString)
  {
    BasicLauncher localBasicLauncher = new BasicLauncher(instance());
    if (paramArrayOfString.length != 1)
    {
      localBasicLauncher.usage();
      return;
    }
    localBasicLauncher.run(paramArrayOfString);
    System.exit(localBasicLauncher.getExitCode().value());
  }
}

/* Location:
 * Qualified Name:     org.sat4j.LightFactory
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j;

import java.io.PrintWriter;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.reader.GroupedCNFReader;
import org.sat4j.reader.LecteurDimacs;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;
import org.sat4j.tools.xplain.Explainer;
import org.sat4j.tools.xplain.HighLevelXplain;
import org.sat4j.tools.xplain.MinimizationStrategy;
import org.sat4j.tools.xplain.Xplain;

public class MUSLauncher
  extends AbstractLauncher
{
  private static final long serialVersionUID = 1L;
  private int[] mus;
  private Explainer xplain;
  private boolean highLevel = false;
  
  public void usage()
  {
    log("java -jar sat4j-mus.jar [Insertion|Deletion|QuickXplain] <cnffile>|<gcnffile>");
  }
  
  protected Reader createReader(ISolver paramISolver, String paramString)
  {
    if (highLevel) {
      return new GroupedCNFReader((HighLevelXplain)paramISolver);
    }
    return new LecteurDimacs(paramISolver);
  }
  
  protected String getInstanceName(String[] paramArrayOfString)
  {
    if (paramArrayOfString.length == 0) {
      return null;
    }
    return paramArrayOfString[(paramArrayOfString.length - 1)];
  }
  
  protected ISolver configureSolver(String[] paramArrayOfString)
  {
    String str = paramArrayOfString[(paramArrayOfString.length - 1)];
    if (str.endsWith(".gcnf")) {
      highLevel = true;
    }
    Object localObject2;
    Object localObject1;
    if (highLevel)
    {
      localObject2 = new HighLevelXplain(SolverFactory.newDefault());
      xplain = ((Explainer)localObject2);
      localObject1 = localObject2;
    }
    else
    {
      localObject2 = new Xplain(SolverFactory.newDefault());
      xplain = ((Explainer)localObject2);
      localObject1 = localObject2;
    }
    if (paramArrayOfString.length == 2)
    {
      localObject2 = "org.sat4j.tools.xplain." + paramArrayOfString[0] + "Strategy";
      try
      {
        xplain.setMinimizationStrategy((MinimizationStrategy)Class.forName((String)localObject2).newInstance());
      }
      catch (Exception localException)
      {
        log(localException.getMessage());
      }
    }
    ((ISolver)localObject1).setTimeout(Integer.MAX_VALUE);
    ((ISolver)localObject1).setDBSimplificationAllowed(true);
    getLogWriter().println(((ISolver)localObject1).toString("c "));
    return (ISolver)localObject1;
  }
  
  protected void displayResult()
  {
    if (solver != null)
    {
      double d = (System.currentTimeMillis() - beginTime) / 1000.0D;
      solver.printStat(out, "c ");
      solver.printInfos(out, "c ");
      out.println("s " + exitCode);
      if (exitCode == ExitCode.SATISFIABLE)
      {
        int[] arrayOfInt = solver.model();
        out.print("v ");
        reader.decode(arrayOfInt, out);
        out.println();
      }
      else if ((exitCode == ExitCode.UNSATISFIABLE) && (mus != null))
      {
        out.print("v ");
        reader.decode(mus, out);
        out.println();
      }
      log("Total wall clock time (in seconds) : " + d);
    }
  }
  
  public void run(String[] paramArrayOfString)
  {
    mus = null;
    super.run(paramArrayOfString);
    double d1 = (System.currentTimeMillis() - beginTime) / 1000.0D;
    if (exitCode == ExitCode.UNSATISFIABLE) {
      try
      {
        log("Unsat detection wall clock time (in seconds) : " + d1);
        log("Size of initial " + (highLevel ? "high level " : "") + "unsat subformula: " + solver.unsatExplanation().size());
        log("Computing " + (highLevel ? "high level " : "") + "MUS ...");
        double d2 = System.currentTimeMillis();
        mus = xplain.minimalExplanation();
        log("Size of the " + (highLevel ? "high level " : "") + "MUS: " + mus.length);
        log("Unsat core  computation wall clock time (in seconds) : " + (System.currentTimeMillis() - d2) / 1000.0D);
      }
      catch (TimeoutException localTimeoutException)
      {
        log("Cannot compute " + (highLevel ? "high level " : "") + "MUS within the timeout.");
      }
    }
  }
  
  public static void main(String[] paramArrayOfString)
  {
    MUSLauncher localMUSLauncher = new MUSLauncher();
    if ((paramArrayOfString.length < 1) || (paramArrayOfString.length > 2))
    {
      localMUSLauncher.usage();
      return;
    }
    localMUSLauncher.run(paramArrayOfString);
    System.exit(localMUSLauncher.getExitCode().value());
  }
}

/* Location:
 * Qualified Name:     org.sat4j.MUSLauncher
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j;

import java.util.MissingResourceException;
import java.util.ResourceBundle;

public final class Messages
{
  private static final String BUNDLE_NAME = "org.sat4j.messages";
  private static final ResourceBundle RESOURCE_BUNDLE = ResourceBundle.getBundle("org.sat4j.messages");
  
  public static String getString(String paramString)
  {
    try
    {
      return RESOURCE_BUNDLE.getString(paramString);
    }
    catch (MissingResourceException localMissingResourceException) {}
    return '!' + paramString + '!';
  }
}

/* Location:
 * Qualified Name:     org.sat4j.Messages
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j;

import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.PrintStream;
import java.io.PrintWriter;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.reader.InstanceReader;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;
import org.sat4j.tools.RemiUtils;
import org.sat4j.tools.SolutionCounter;

public final class MoreThanSAT
{
  public static void main(String[] paramArrayOfString)
  {
    ISolver localISolver = SolverFactory.newDefault();
    SolutionCounter localSolutionCounter = new SolutionCounter(localISolver);
    localISolver.setTimeout(3600);
    InstanceReader localInstanceReader = new InstanceReader(localISolver);
    try
    {
      IProblem localIProblem = localInstanceReader.parseInstance(paramArrayOfString[0]);
      if (localIProblem.isSatisfiable())
      {
        System.out.println(Messages.getString("MoreThanSAT.0"));
        localInstanceReader.decode(localIProblem.model(), new PrintWriter(System.out));
        IVecInt localIVecInt = RemiUtils.backbone(localISolver);
        System.out.println(Messages.getString("MoreThanSAT.1") + localIVecInt);
        System.out.println(Messages.getString("MoreThanSAT.2"));
        System.out.println(Messages.getString("MoreThanSAT.3") + localSolutionCounter.countSolutions());
      }
      else
      {
        System.out.println(Messages.getString("MoreThanSAT.4"));
      }
    }
    catch (FileNotFoundException localFileNotFoundException)
    {
      localFileNotFoundException.printStackTrace();
    }
    catch (ParseFormatException localParseFormatException)
    {
      localParseFormatException.printStackTrace();
    }
    catch (IOException localIOException)
    {
      localIOException.printStackTrace();
    }
    catch (ContradictionException localContradictionException)
    {
      System.out.println(Messages.getString("MoreThanSAT.5"));
    }
    catch (TimeoutException localTimeoutException)
    {
      System.out.println(Messages.getString("MoreThanSAT.6"));
    }
  }
}

/* Location:
 * Qualified Name:     org.sat4j.MoreThanSAT
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.core;

import java.io.PrintStream;
import java.io.Serializable;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.util.ArrayList;
import java.util.List;
import org.sat4j.specs.ISolver;

public abstract class ASolverFactory<T extends ISolver>
  implements Serializable
{
  private static final long serialVersionUID = 1L;
  
  public String[] solverNames()
  {
    ArrayList localArrayList = new ArrayList();
    Method[] arrayOfMethod = getClass().getDeclaredMethods();
    for (int i = 0; i < arrayOfMethod.length; i++) {
      if ((arrayOfMethod[i].getParameterTypes().length == 0) && (arrayOfMethod[i].getName().startsWith("new"))) {
        localArrayList.add(arrayOfMethod[i].getName().substring(3));
      }
    }
    String[] arrayOfString = new String[localArrayList.size()];
    localArrayList.toArray(arrayOfString);
    return arrayOfString;
  }
  
  public T createSolverByName(String paramString)
  {
    try
    {
      Class[] arrayOfClass = new Class[0];
      Method localMethod = getClass().getMethod("new" + paramString, arrayOfClass);
      return (ISolver)localMethod.invoke(null, (Object[])null);
    }
    catch (SecurityException localSecurityException)
    {
      System.err.println(localSecurityException.getLocalizedMessage());
    }
    catch (IllegalArgumentException localIllegalArgumentException)
    {
      System.err.println(localIllegalArgumentException.getLocalizedMessage());
    }
    catch (NoSuchMethodException localNoSuchMethodException)
    {
      System.err.println(localNoSuchMethodException.getLocalizedMessage());
    }
    catch (IllegalAccessException localIllegalAccessException)
    {
      System.err.println(localIllegalAccessException.getLocalizedMessage());
    }
    catch (InvocationTargetException localInvocationTargetException)
    {
      System.err.println(localInvocationTargetException.getLocalizedMessage());
    }
    return null;
  }
  
  public abstract T defaultSolver();
  
  public abstract T lightSolver();
}

/* Location:
 * Qualified Name:     org.sat4j.core.ASolverFactory
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.core;

import java.io.Serializable;
import java.util.Comparator;

public final class DefaultComparator<A extends Comparable<A>>
  implements Comparator<A>, Serializable
{
  private static final long serialVersionUID = 1L;
  
  public int compare(A paramA1, A paramA2)
  {
    return paramA1.compareTo(paramA2);
  }
  
  public int compare(Object paramObject1, Object paramObject2)
  {
    return compare((Comparable)paramObject1, (Comparable)paramObject2);
  }
}

/* Location:
 * Qualified Name:     org.sat4j.core.DefaultComparator
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.core;

public final class LiteralsUtils
{
  public static int var(int paramInt)
  {
    assert (paramInt > 1);
    return paramInt >> 1;
  }
  
  public static int neg(int paramInt)
  {
    return paramInt ^ 0x1;
  }
  
  public static int posLit(int paramInt)
  {
    return paramInt << 1;
  }
  
  public static int negLit(int paramInt)
  {
    return paramInt << 1 ^ 0x1;
  }
  
  public static int toDimacs(int paramInt)
  {
    return ((paramInt & 0x1) == 0 ? 1 : -1) * (paramInt >> 1);
  }
  
  public static int toInternal(int paramInt)
  {
    return paramInt < 0 ? -paramInt << 1 ^ 0x1 : paramInt << 1;
  }
}

/* Location:
 * Qualified Name:     org.sat4j.core.LiteralsUtils
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.core;

import java.util.Comparator;
import java.util.Iterator;
import org.sat4j.specs.IVec;

public final class ReadOnlyVec<T>
  implements IVec<T>
{
  private static final long serialVersionUID = 1L;
  private final IVec<T> vec;
  
  public ReadOnlyVec(IVec<T> paramIVec)
  {
    vec = paramIVec;
  }
  
  public void clear()
  {
    throw new UnsupportedOperationException();
  }
  
  public void copyTo(IVec<T> paramIVec)
  {
    vec.copyTo(paramIVec);
  }
  
  public <E> void copyTo(E[] paramArrayOfE)
  {
    vec.copyTo(paramArrayOfE);
  }
  
  public T delete(int paramInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public void ensure(int paramInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public T get(int paramInt)
  {
    return (T)vec.get(paramInt);
  }
  
  public void growTo(int paramInt, T paramT)
  {
    throw new UnsupportedOperationException();
  }
  
  public void insertFirst(T paramT)
  {
    throw new UnsupportedOperationException();
  }
  
  public void insertFirstWithShifting(T paramT)
  {
    throw new UnsupportedOperationException();
  }
  
  public boolean isEmpty()
  {
    return vec.isEmpty();
  }
  
  public Iterator<T> iterator()
  {
    return vec.iterator();
  }
  
  public T last()
  {
    return (T)vec.last();
  }
  
  public void moveTo(IVec<T> paramIVec)
  {
    throw new UnsupportedOperationException();
  }
  
  public void moveTo(int paramInt1, int paramInt2)
  {
    throw new UnsupportedOperationException();
  }
  
  public void pop()
  {
    throw new UnsupportedOperationException();
  }
  
  public IVec<T> push(T paramT)
  {
    throw new UnsupportedOperationException();
  }
  
  public void remove(T paramT)
  {
    throw new UnsupportedOperationException();
  }
  
  public void set(int paramInt, T paramT)
  {
    throw new UnsupportedOperationException();
  }
  
  public void shrink(int paramInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public void shrinkTo(int paramInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public int size()
  {
    return vec.size();
  }
  
  public void sort(Comparator<T> paramComparator)
  {
    throw new UnsupportedOperationException();
  }
  
  public void sortUnique(Comparator<T> paramComparator)
  {
    throw new UnsupportedOperationException();
  }
  
  public T[] toArray()
  {
    Object[] arrayOfObject = (Object[])new Object[vec.size()];
    vec.copyTo(arrayOfObject);
    return arrayOfObject;
  }
  
  public void unsafePush(T paramT)
  {
    throw new UnsupportedOperationException();
  }
  
  public boolean contains(T paramT)
  {
    return vec.contains(paramT);
  }
  
  public int indexOf(T paramT)
  {
    return vec.indexOf(paramT);
  }
  
  public String toString()
  {
    return vec.toString();
  }
}

/* Location:
 * Qualified Name:     org.sat4j.core.ReadOnlyVec
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.core;

import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;

public final class ReadOnlyVecInt
  implements IVecInt
{
  private static final long serialVersionUID = 1L;
  private final IVecInt vec;
  
  public ReadOnlyVecInt(IVecInt paramIVecInt)
  {
    vec = paramIVecInt;
  }
  
  public void clear()
  {
    throw new UnsupportedOperationException();
  }
  
  public boolean contains(int paramInt)
  {
    return vec.contains(paramInt);
  }
  
  public int containsAt(int paramInt)
  {
    return vec.containsAt(paramInt);
  }
  
  public int containsAt(int paramInt1, int paramInt2)
  {
    return vec.containsAt(paramInt1, paramInt2);
  }
  
  public void copyTo(IVecInt paramIVecInt)
  {
    vec.copyTo(paramIVecInt);
  }
  
  public void copyTo(int[] paramArrayOfInt)
  {
    vec.copyTo(paramArrayOfInt);
  }
  
  public int delete(int paramInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public void ensure(int paramInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public int get(int paramInt)
  {
    return vec.get(paramInt);
  }
  
  public void growTo(int paramInt1, int paramInt2)
  {
    throw new UnsupportedOperationException();
  }
  
  public void insertFirst(int paramInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public boolean isEmpty()
  {
    return vec.isEmpty();
  }
  
  public IteratorInt iterator()
  {
    return vec.iterator();
  }
  
  public int last()
  {
    return vec.last();
  }
  
  public void moveTo(IVecInt paramIVecInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public void moveTo(int[] paramArrayOfInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public void moveTo(int paramInt1, int paramInt2)
  {
    throw new UnsupportedOperationException();
  }
  
  public void moveTo2(IVecInt paramIVecInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public IVecInt pop()
  {
    throw new UnsupportedOperationException();
  }
  
  public IVecInt push(int paramInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public void remove(int paramInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public void set(int paramInt1, int paramInt2)
  {
    throw new UnsupportedOperationException();
  }
  
  public void shrink(int paramInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public void shrinkTo(int paramInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public int size()
  {
    return vec.size();
  }
  
  public void sort()
  {
    throw new UnsupportedOperationException();
  }
  
  public void sortUnique()
  {
    throw new UnsupportedOperationException();
  }
  
  public int unsafeGet(int paramInt)
  {
    return vec.unsafeGet(paramInt);
  }
  
  public void unsafePush(int paramInt)
  {
    throw new UnsupportedOperationException();
  }
  
  public int[] toArray()
  {
    throw new UnsupportedOperationException();
  }
  
  public int indexOf(int paramInt)
  {
    return vec.indexOf(paramInt);
  }
  
  public String toString()
  {
    return vec.toString();
  }
  
  public void moveTo(int paramInt, int[] paramArrayOfInt)
  {
    throw new UnsupportedOperationException();
  }
}

/* Location:
 * Qualified Name:     org.sat4j.core.ReadOnlyVecInt
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.core;

import java.util.Iterator;
import java.util.NoSuchElementException;

class Vec$1
  implements Iterator<T>
{
  private int i = 0;
  private final Vec this$0;
  
  Vec$1(Vec paramVec) {}
  
  public boolean hasNext()
  {
    return i < Vec.access$000(this$0);
  }
  
  public T next()
  {
    if (i == Vec.access$000(this$0)) {
      throw new NoSuchElementException();
    }
    return (T)Vec.access$100(this$0)[(i++)];
  }
  
  public void remove()
  {
    throw new UnsupportedOperationException();
  }
}

/* Location:
 * Qualified Name:     org.sat4j.core.Vec.1
 * Java Class Version: 1.4 (48.0)
 * JD-Core Version:    0.7.1
 */
package org.sat4j.core;

import java.util.Arrays;
import java.util.Comparator;
import java.util.Iterator;
import java.util.NoSuchElementException;
import org.sat4j.specs.IVec;

public final class Vec<T>
  implements IVec<T>
{
  private static final long serialVersionUID = 1L;
  private int nbelem;
  private T[] myarray;
  
  public Vec()
  {
    this(5);
  }
  
  public Vec(T[] paramArrayOfT)
  {
    myarray = paramArrayOfT;
    nbelem = paramArrayOfT.length;
  }
  
  public Vec(int paramInt)
  {
    myarray = ((Object[])new Object[paramInt]);
  }
  
  public Vec(int paramInt, T paramT)
  {
    myarray = ((Object[])new Object[paramInt]);
    for (int i = 0; i < paramInt; i++) {
      myarray[i] = paramT;
    }
    nbelem = paramInt;
  }
  
  public int size()
  {
    return nbelem;
  }
  
  public void shrink(int paramInt)
  {
    while (paramInt-- > 0) {
      myarray[(--nbelem)] = null;
    }
  }
  
  public void shrinkTo(int paramInt)
  {
    for (int i = nbelem; i > paramInt; i--) {
      myarray[(i - 1)] = null;
    }
    nbelem = paramInt;
  }
  
  public void pop()
  {
    myarray[(--nbelem)] = null;
  }
  
  public void growTo(int paramInt, T paramT)
  {
    ensure(paramInt);
    for (int i = nbelem; i < paramInt; i++) {
      myarray[i] = paramT;
    }
    nbelem = paramInt;
  }
  
  public void ensure(int paramInt)
  {
    if (paramInt >= myarray.length)
    {
      Object[] arrayOfObject = (Object[])new Object[Math.max(paramInt, nbelem * 2)];
      System.arraycopy(myarray, 0, arrayOfObject, 0, nbelem);
      myarray = arrayOfObject;
    }
  }
  
  public IVec<T> push(T paramT)
  {
    ensure(nbelem + 1);
    myarray[(nbelem++)] = paramT;
    return this;
  }
  
  public void unsafePush(T paramT)
  {
    myarray[(nbelem++)] = paramT;
  }
  
  public void insertFirst(T paramT)
  {
    if (nbelem > 0)
    {
      push(myarray[0]);
      myarray[0] = paramT;
      return;
    }
    push(paramT);
  }
  
  public void insertFirstWithShifting(T paramT)
  {
    if (nbelem > 0)
    {
      ensure(nbelem + 1);
      for (int i = nbelem; i > 0; i--) {
        myarray[i] = myarray[(i - 1)];
      }
      myarray[0] = paramT;
      nbelem += 1;
      return;
    }
    push(paramT);
  }
  
  public void clear()
  {
    Arrays.fill(myarray, 0, nbelem, null);
    nbelem = 0;
  }
  
  public T last()
  {
    return (T)myarray[(nbelem - 1)];
  }
  
  public T get(int paramInt)
  {
    return (T)myarray[paramInt];
  }
  
  public void set(int paramInt, T paramT)
  {
    myarray[paramInt] = paramT;
  }
  
  public void remove(T paramT)
  {
    for (int i = 0; myarray[i] != paramT; i++) {
      assert (i < size());
    }
    System.arraycopy(myarray, i + 1, myarray, i, size() - i - 1);
    myarray[(--nbelem)] = null;
  }
  
  public T delete(int paramInt)
  {
    Object localObject = myarray[paramInt];
    myarray[paramInt] = myarray[(--nbelem)];
    myarray[nbelem] = null;
    return (T)localObject;
  }
  
  public void copyTo(IVec<T> paramIVec)
  {
    Vec localVec = (Vec)paramIVec;
    int i = nbelem + nbelem;
    paramIVec.ensure(i);
    System.arraycopy(myarray, 0, myarray, nbelem, nbelem);
    nbelem = i;
  }
  
  public <E> void copyTo(E[] paramArrayOfE)
  {
    System.arraycopy(myarray, 0, paramArrayOfE, 0, nbelem);
  }
  
  public void moveTo(IVec<T> paramIVec)
  {
    copyTo(paramIVec);
    clear();
  }
  
  public void moveTo(int paramInt1, int paramInt2)
  {
    if (paramInt1 != paramInt2)
    {
      myarray[paramInt1] = myarray[paramInt2];
      myarray[paramInt2] = null;
    }
  }
  
  public T[] toArray()
  {
    return myarray;
  }
  
  public String toString()
  {
    StringBuffer localStringBuffer = new StringBuffer();
    for (int i = 0; i < nbelem - 1; i++)
    {
      localStringBuffer.append(myarray[i]);
      localStringBuffer.append(",");
    }
    if (nbelem > 0) {
      localStringBuffer.append(myarray[(nbelem - 1)]);
    }
    return localStringBuffer.toString();
  }
  
  void selectionSort(int paramInt1, int paramInt2, Comparator<T> paramComparator)
  {
    for (int i = paramInt1; i < paramInt2 - 1; i++)
    {
      int k = i;
      for (int j = i + 1; j < paramInt2; j++) {
        if (paramComparator.compare(myarray[j], myarray[k]) < 0) {
          k = j;
        }
      }
      Object localObject = myarray[i];
      myarray[i] = myarray[k];
      myarray[k] = localObject;
    }
  }
  
  void sort(int paramInt1, int paramInt2, Comparator<T> paramComparator)
  {
    int i = paramInt2 - paramInt1;
    if (i <= 15)
    {
      selectionSort(paramInt1, paramInt2, paramComparator);
    }
    else
    {
      Object localObject1 = myarray[(i / 2 + paramInt1)];
      int j = paramInt1 - 1;
      int k = paramInt2;
      for (;;)
      {
        j++;
        if (paramComparator.compare(myarray[j], localObject1) >= 0)
        {
          do
          {
            k--;
          } while (paramComparator.compare(localObject1, myarray[k]) < 0);
          if (j >= k) {
            break;
          }
          Object localObject2 = myarray[j];
          myarray[j] = myarray[k];
          myarray[k] = localObject2;
        }
 
1 2 3 4 5 6 7 8 9 10 11

Further reading...

For more information on Java 1.5 Tiger, you may find Java 1.5 Tiger, A developer's Notebook by D. Flanagan and B. McLaughlin from O'Reilly of interest.

New!JAR listings


Copyright 2006-2017. Infinite Loop Ltd