content: /**
   * Copyright (c) 2016-2020, the Alpha Team.
   * All rights reserved.
   *
   * Additional changes made by Siemens.
   *
   * Redistribution and use in source and binary forms, with or without
   * modification, are permitted provided that the following conditions are met:
   *
   * 1) Redistributions of source code must retain the above copyright notice, this
   *    list of conditions and the following disclaimer.
   *
   * 2) Redistributions in binary form must reproduce the above copyright notice,
   *    this list of conditions and the following disclaimer in the documentation
   *    and/or other materials provided with the distribution.
   *
   * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
   * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
   * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
   * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
   * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
   * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
   * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
   * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
   * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
   * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
   */
  package at.ac.tuwien.kr.alpha;
  
  import java.io.File;
  import java.io.FileNotFoundException;
  import java.io.FileOutputStream;
  import java.io.IOException;
  import java.io.PrintStream;
  import java.nio.file.Paths;
  import java.util.List;
  import java.util.Map;
  import java.util.Set;
  import java.util.concurrent.atomic.AtomicInteger;
  import java.util.function.BiConsumer;
  import java.util.stream.Collectors;
  import java.util.stream.Stream;
  
  import at.ac.tuwien.kr.alpha.api.programs.tests.Assertion;
  import at.ac.tuwien.kr.alpha.api.programs.tests.TestResult;
  import org.apache.commons.cli.ParseException;
  import org.slf4j.Logger;
  import org.slf4j.LoggerFactory;
  
  import at.ac.tuwien.kr.alpha.api.Alpha;
  import at.ac.tuwien.kr.alpha.api.AnswerSet;
  import at.ac.tuwien.kr.alpha.api.DebugSolvingContext;
  import at.ac.tuwien.kr.alpha.api.Solver;
  import at.ac.tuwien.kr.alpha.api.StatisticsReportingSolver;
  import at.ac.tuwien.kr.alpha.api.config.AlphaConfig;
  import at.ac.tuwien.kr.alpha.api.config.InputConfig;
  import at.ac.tuwien.kr.alpha.api.config.SystemConfig;
  import at.ac.tuwien.kr.alpha.api.impl.AlphaImpl;
  import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program;
  import at.ac.tuwien.kr.alpha.api.programs.NormalProgram;
  import at.ac.tuwien.kr.alpha.api.programs.analysis.ComponentGraph;
  import at.ac.tuwien.kr.alpha.api.programs.analysis.DependencyGraph;
  import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom;
  import at.ac.tuwien.kr.alpha.api.util.AnswerSetFormatter;
  import at.ac.tuwien.kr.alpha.app.ComponentGraphWriter;
  import at.ac.tuwien.kr.alpha.app.DependencyGraphWriter;
  import at.ac.tuwien.kr.alpha.app.config.CommandLineParser;
  import at.ac.tuwien.kr.alpha.commons.util.SimpleAnswerSetFormatter;
  
  /**
   * Main entry point for Alpha.
   */
  public class Main {
  
  	private static final Logger LOGGER = LoggerFactory.getLogger(Main.class);
  
  	private static final String ALPHA_CALL_SYNTAX = "java -jar alpha-bundled.jar" + System.lineSeparator() + "java -jar alpha.jar";
  
  	public static void main(String[] args) {
  		CommandLineParser commandLineParser = new CommandLineParser(Main.ALPHA_CALL_SYNTAX, (msg) -> Main.exitWithMessage(msg, 0));
  		AlphaConfig cfg = null;
  		try {
  			cfg = commandLineParser.parseCommandLine(args);
  		} catch (ParseException ex) {
  			System.err.println("Invalid usage: " + ex.getMessage());
  			Main.exitWithMessage(commandLineParser.getUsageMessage(), 1);
  		}
  
  		Alpha alpha = new AlphaImpl(cfg.getSystemConfig());
  
  		ASPCore2Program program = null;
  		try {
  			program = alpha.readProgram(cfg.getInputConfig());
  		} catch (FileNotFoundException e) {
  			Main.bailOut(e.getMessage());
  		} catch (IOException e) {
  			Main.bailOut("Failed to parse program.", e);
  		}
  
  		InputConfig inputCfg = cfg.getInputConfig();
  
  		// Note: We might potentially want to get the reified program as an AnswerSet and
  		// apply all the formatting we can do on answer sets also on reified programs.
  		if (inputCfg.isReifyInput()) {
  			Set<BasicAtom> reified = alpha.reify(program);
  			for (BasicAtom atom : reified) {
  				System.out.println(atom + ".");
  			}
  		} else if (inputCfg.isRunTests()) {
  			TestResult result = alpha.test(program);
  			printTestResult(result);
  		} else {
  			Solver solver;
  			if (inputCfg.isDebugPreprocessing()) {
  				DebugSolvingContext dbgCtx = alpha.prepareDebugSolve(program);
  				Main.writeNormalProgram(dbgCtx.getNormalizedProgram(), inputCfg.getNormalizedPath());
  				Main.writeNormalProgram(dbgCtx.getPreprocessedProgram(), inputCfg.getPreprocessedPath());
  				Main.writeDependencyGraph(dbgCtx.getDependencyGraph(), inputCfg.getDepgraphPath());
  				Main.writeComponentGraph(dbgCtx.getComponentGraph(), inputCfg.getCompgraphPath());
  				solver = dbgCtx.getSolver();
  			} else {
  				solver = alpha.prepareSolverFor(program, inputCfg.getFilter());
  			}
  			Main.computeAndConsumeAnswerSets(solver, cfg);
  		}
  	}
  
  
  	/**
  	 * Writes the given {@link DependencyGraph} to the destination passed as the second parameter
  	 * 
  	 * @param dg   the dependency graph to write
  	 * @param path the path to write the graph to
  	 */
  	private static void writeDependencyGraph(DependencyGraph dg, String path) {
  		DependencyGraphWriter depGraphWriter = new DependencyGraphWriter();
  		try (FileOutputStream os = new FileOutputStream(new File(path))) {
  			depGraphWriter.writeAsDot(dg, os);
  		} catch (IOException ex) {
  			Main.bailOut("Error writing dependency graph: " + ex.getMessage());
  		}
  	}
  
  	/**
  	 * Writes the given {@link ComponentGraph} to the destination passed as the second parameter
  	 * 
  	 * @param cg   the component graph to write
  	 * @param path the path to write the graph to
  	 */
  	private static void writeComponentGraph(ComponentGraph cg, String path) {
  		ComponentGraphWriter compGraphWriter = new ComponentGraphWriter();
  		try (FileOutputStream os = new FileOutputStream(new File(path))) {
  			compGraphWriter.writeAsDot(cg, os);
  		} catch (IOException ex) {
  			Main.bailOut("Error writing component graph: " + ex.getMessage());
  		}
  
  	}
  
  	/**
  	 * Writes the given {@link CompiledProgram} to the destination passed as the second parameter
  	 * 
  	 * @param prg  the program to write
  	 * @param path the path to write the program to
  	 */
  	private static void writeNormalProgram(NormalProgram prg, String path) {
  		LOGGER.debug("Writing program to {}", path);
  		PrintStream ps;
  		try {
  			ps = new PrintStream(new File(path));
  			ps.println(prg.toString());
  		} catch (IOException ex) {
  			LOGGER.error("Failed writing program file", ex);
  			Main.bailOut("Failed writing program file " + ex.getMessage());
  		}
  	}
  
  	private static void printTestResult(TestResult result) {
  		if (result.isSuccess()) {
  			System.out.println("TEST SUCCESSFUL");
  		} else {
  			System.out.println("TESTS FAILED!");
  		}
  		for (TestResult.TestCaseResult tcResult : result.getTestCaseResults()) {
  			System.out.println("Test case: " + tcResult.getTestCaseName() + " " + (tcResult.isSuccess() ? "PASSED" : "FAILED") +
  					", assertions passed: " + tcResult.getAssertionsPassed() +
  					", assertions failed: " + tcResult.getAssertionsFailed());
  			if (!tcResult.isSuccess()) {
  				System.out.println("Assertion failures:");
  				if (tcResult.answerSetCountVerificationResult().isPresent()) {
  					System.out.println(tcResult.answerSetCountVerificationResult().get());
  				}
  				for (Map.Entry<Assertion, List<String>> assertionError : tcResult.getAssertionErrors().entrySet()) {
  					for (String errMsg : assertionError.getValue()) {
  						System.out.println("Assertion failed: " + assertionError.getKey() + ", error = " + errMsg);
  					}
  				}
  			}
  		}
  	}
  
  	private static void computeAndConsumeAnswerSets(Solver solver, AlphaConfig alphaCfg) {
  		SystemConfig sysCfg = alphaCfg.getSystemConfig();
  		InputConfig inputCfg = alphaCfg.getInputConfig();
  		Stream<AnswerSet> stream = solver.stream();
  		if (sysCfg.isSortAnswerSets()) {
  			stream = stream.sorted();
  		}
  
  		int limit = inputCfg.getNumAnswerSets();
  		if (limit > 0) {
  			stream = stream.limit(limit);
  		}
  
  		if (!sysCfg.isQuiet()) {
  			AtomicInteger counter = new AtomicInteger(0);
  			final BiConsumer<Integer, AnswerSet> answerSetHandler;
  			final AnswerSetFormatter<String> fmt = new SimpleAnswerSetFormatter(sysCfg.getAtomSeparator());
  			BiConsumer<Integer, AnswerSet> stdoutPrinter = (n, as) -> {
  				System.out.println("Answer set " + Integer.toString(n) + ":" + System.lineSeparator() + fmt.format(as));
  			};
  			if (inputCfg.isWriteAnswerSetsAsXlsx()) {
  				BiConsumer<Integer, AnswerSet> xlsxWriter = new AnswerSetToXlsxWriter(inputCfg.getAnswerSetFileOutputPath());
  				answerSetHandler = stdoutPrinter.andThen(xlsxWriter);
  			} else {
  				answerSetHandler = stdoutPrinter;
  			}
  			stream.forEach(as -> {
  				int cnt = counter.incrementAndGet();
  				answerSetHandler.accept(cnt, as);
  			});
  			if (counter.get() == 0) {
  				System.out.println("UNSATISFIABLE");
  				if (inputCfg.isWriteAnswerSetsAsXlsx()) {
  					try {
  						AnswerSetToXlsxWriter.writeUnsatInfo(Paths.get(inputCfg.getAnswerSetFileOutputPath() + ".UNSAT.xlsx"));
  					} catch (IOException ex) {
  						System.err.println("Failed writing unsat file!");
  					}
  				}
  			} else {
  				System.out.println("SATISFIABLE");
  			}
  		} else {
  			// Note: Even though we are not consuming the result, we will still compute
  			// answer sets.
  			stream.collect(Collectors.toList());
  		}
  		if (sysCfg.isPrintStats()) {
  			if (solver instanceof StatisticsReportingSolver) {
  				((StatisticsReportingSolver) solver).printStatistics();
  			} else {
  				// Note: Should not happen with proper validation of commandline args
  				System.err.println("Solver of type " + solver.getClass().getSimpleName() + " does not support solving statistics!");
  			}
  		}
  	}
  
  	private static void exitWithMessage(String msg, int exitCode) {
  		System.out.println(msg);
  		System.exit(exitCode);
  	}
  
  	private static void bailOut(String format, Object... arguments) {
  		LOGGER.error(format, arguments);
  		System.exit(1);
  	}
  
  }
  