Skip to content

Commit

Permalink
Merge branch 'logger'
Browse files Browse the repository at this point in the history
  • Loading branch information
jhoenicke committed Jul 15, 2016
2 parents cdd5908 + f8fe823 commit 656452f
Show file tree
Hide file tree
Showing 77 changed files with 2,463 additions and 1,101 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -1066,7 +1066,7 @@ public static void main(String[] args) {
if (verbosity > 0)
System.err.println("Got golden exit code: " + goldenExit);
ParseScript ps = new ParseScript();
ParseEnvironment pe = new ParseEnvironment(ps) {
ParseEnvironment pe = new ParseEnvironment(ps, null) {

@Override
public void printSuccess() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@

import java.io.File;

import de.uni_freiburg.informatik.ultimate.smtinterpol.DefaultLogger;
import de.uni_freiburg.informatik.ultimate.smtinterpol.option.OptionMap;
import de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser;

/**
Expand Down Expand Up @@ -60,7 +62,8 @@ public static void main(String[] args) {
ProofChecker checker = new ProofChecker(filenameNoExtension,
useIsabelle, prettyOutput, fastProofs, partialProof);
checker.setOption(":verbosity", 3);

new SMTLIB2Parser().run(checker, args[0]);
DefaultLogger logger = new DefaultLogger();
OptionMap options = new OptionMap(logger, true);
new SMTLIB2Parser().run(checker, args[0], options);
}
}
1 change: 0 additions & 1 deletion SMTInterpol/.classpath
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry excluding="**/.svn/*" kind="src" path="src"/>
<classpathentry kind="lib" path="lib/java-cup-12joho.jar"/>
<classpathentry exported="true" kind="lib" path="lib/log4j-1.2.15.jar"/>
<classpathentry combineaccessrules="false" kind="src" path="/Library-SMTLIB"/>
<classpathentry kind="output" path="bin"/>
</classpath>
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright (C) 2009-2012 University of Freiburg
* Copyright (C) 2014-2015 University of Freiburg
*
* This file is part of SMTInterpol.
*
Expand All @@ -16,28 +16,22 @@
* You should have received a copy of the GNU Lesser General Public License
* along with SMTInterpol. If not, see <http://www.gnu.org/licenses/>.
*/
package de.uni_freiburg.informatik.ultimate.smtinterpol.util;
package de.uni_freiburg.informatik.ultimate.smtinterpol;

import org.apache.log4j.ConsoleAppender;
import org.apache.log4j.Level;
import org.apache.log4j.Logger;
import org.apache.log4j.SimpleLayout;
import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;

public class TestCaseWithLogger {

static {
Logger logger = Logger.getRootLogger();
if (!logger.getAllAppenders().hasMoreElements()) {
SimpleLayout layout = new SimpleLayout();
logger.addAppender(new ConsoleAppender(layout));
}
public final class ChannelUtil {
private ChannelUtil() {
// hide constructor
}

protected TestCaseWithLogger() {
this(Level.DEBUG);
}

protected TestCaseWithLogger(Level level) {
Logger.getRootLogger().setLevel(level);
public static PrintWriter createChannel(String file) throws IOException {
if ("stdout".equals(file))
return new PrintWriter(System.out);
if ("stderr".equals(file))
return new PrintWriter(System.err);
else
return new PrintWriter(new FileWriter(file));
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,6 @@
*/
package de.uni_freiburg.informatik.ultimate.smtinterpol;

import org.apache.log4j.Level;

/**
* Basic configuration of SMTInterpol.
* @author Juergen Christ
Expand All @@ -33,8 +31,8 @@ public interface Config {
/// Create timing statistics
public final static boolean PROFILE_TIME = !COMPETITION;
/// Default log level
public final static Level DEFAULT_LOG_LEVEL =
COMPETITION ? Level.ERROR : Level.INFO;
public final static int DEFAULT_LOG_LEVEL =
COMPETITION ? LogProxy.LOGLEVEL_ERROR : LogProxy.LOGLEVEL_INFO;
/// Check the status set by the user against our check-sat status
public final static boolean CHECK_STATUS_SET = !COMPETITION;

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,206 @@
/*
* Copyright (C) 2014 University of Freiburg
*
* This file is part of SMTInterpol.
*
* SMTInterpol is free software: you can redistribute it and/or modify
* it under the terms of the GNU Lesser General Public License as published
* by the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* SMTInterpol is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU Lesser General Public License for more details.
*
* You should have received a copy of the GNU Lesser General Public License
* along with SMTInterpol. If not, see <http://www.gnu.org/licenses/>.
*/
package de.uni_freiburg.informatik.ultimate.smtinterpol;

import java.io.IOException;
import java.io.PrintWriter;
import java.util.Formatter;

public class DefaultLogger implements LogProxy {

// Multithreading support
private static final Object LOCK = new Object();

// Loglevel strings
private static final String[] LEVELS = {
"FATAL",
"ERROR",
"WARN",
"INFO",
"DEBUG",
"TRACE"
};

private PrintWriter mWriter = new PrintWriter(System.err);
private Formatter mFormat = new Formatter(mWriter);
private String mDest = "stderr";

private int mLevel = Config.DEFAULT_LOG_LEVEL;

@Override
public void setLoglevel(int level) {
mLevel = level;
}

@Override
public int getLoglevel() {
return mLevel;
}

private final boolean isEnabled(int lvl) {
return lvl <= mLevel;
}

private final void log(int lvl, Object msg) {
synchronized (LOCK) {
mWriter.print(LEVELS[lvl - 1]);
mWriter.print(" - ");
mWriter.println(msg);
mWriter.flush();
}
}

private final void log(int lvl, String msg, Object[] params) {
if (params.length == 0)
log(lvl, msg);
synchronized (LOCK) {
mWriter.print(LEVELS[lvl - 1]);
mWriter.print(" - ");
mFormat.format(msg, params);
mWriter.println();
mWriter.flush();
}
}

@Override
public boolean isFatalEnabled() {
return isEnabled(LOGLEVEL_FATAL);
}

@Override
public void fatal(String msg, Object... params) {
if (isFatalEnabled())
log(LOGLEVEL_FATAL, msg, params);
}

@Override
public void fatal(Object msg) {
if (isFatalEnabled())
log(LOGLEVEL_FATAL, msg);
}

@Override
public void outOfMemory(String msg) {
if (isFatalEnabled())
log(LOGLEVEL_FATAL, msg);
}

@Override
public boolean isErrorEnabled() {
return isEnabled(LOGLEVEL_ERROR);
}

@Override
public void error(String msg, Object... params) {
if (isErrorEnabled())
log(LOGLEVEL_ERROR, msg, params);
}

@Override
public void error(Object msg) {
if (isErrorEnabled())
log(LOGLEVEL_ERROR, msg);
}

@Override
public boolean isWarnEnabled() {
return isEnabled(LOGLEVEL_WARN);
}

@Override
public void warn(String msg, Object... params) {
if (isWarnEnabled())
log(LOGLEVEL_WARN, msg, params);
}

@Override
public void warn(Object msg) {
if (isWarnEnabled())
log(LOGLEVEL_WARN, msg);
}

@Override
public boolean isInfoEnabled() {
return isEnabled(LOGLEVEL_INFO);
}

@Override
public void info(String msg, Object... params) {
if (isInfoEnabled())
log(LOGLEVEL_INFO, msg, params);
}

@Override
public void info(Object msg) {
if (isInfoEnabled())
log(LOGLEVEL_INFO, msg);
}

@Override
public boolean isDebugEnabled() {
return isEnabled(LOGLEVEL_DEBUG);
}

@Override
public void debug(String msg, Object... params) {
if (isDebugEnabled())
log(LOGLEVEL_DEBUG, msg, params);
}

@Override
public void debug(Object msg) {
if (isDebugEnabled())
log(LOGLEVEL_DEBUG, msg);
}

@Override
public boolean isTraceEnabled() {
return isEnabled(LOGLEVEL_TRACE);
}

@Override
public void trace(String msg, Object... params) {
if (isTraceEnabled())
log(LOGLEVEL_TRACE, msg, params);
}

@Override
public void trace(Object msg) {
if (isTraceEnabled())
log(LOGLEVEL_TRACE, msg);
}

@Override
public boolean canChangeDestination() {
return true;
}

@Override
public void changeDestination(String newDest) throws IOException {
mWriter = ChannelUtil.createChannel(newDest);
mFormat = new Formatter(mWriter);
mDest = newDest;
}

@Override
public String getDestination() {
return mDest;
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@
import de.uni_freiburg.informatik.ultimate.logic.LoggingScript;
import de.uni_freiburg.informatik.ultimate.logic.SMTLIBException;
import de.uni_freiburg.informatik.ultimate.logic.Term;
import de.uni_freiburg.informatik.ultimate.smtinterpol.option.OptionMap;
import de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment;

public class DefinitionExpander extends LoggingScript {
Expand All @@ -49,9 +50,10 @@ public LBool assertTerm(Term term) throws SMTLIBException {
public static void main(String[] args) {
String infile = args[0];
String outfile = args[1];
OptionMap options = new OptionMap(new DefaultLogger(), true);
try {
ParseEnvironment pe = new ParseEnvironment(
new DefinitionExpander(outfile));
new DefinitionExpander(outfile), options);
pe.parseScript(infile);
} catch (FileNotFoundException e) {
e.printStackTrace();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@
package de.uni_freiburg.informatik.ultimate.smtinterpol;

import de.uni_freiburg.informatik.ultimate.logic.Script;
import de.uni_freiburg.informatik.ultimate.smtinterpol.option.OptionMap;

/**
* Generic interface for the different parsers of SMTInterpol. Each interface
Expand All @@ -29,10 +30,12 @@
public interface IParser {
/**
* Parse a specific file. If the filename is <code>null</code>, the
* parser should parse standard input,
* @param script The script that should be used.
* @param filename The name of the file to parse.
* parser should parse standard input. The script has to be initialized.
* @param script The script that should be used.
* @param filename The name of the file to parse.
* @param options The option map used to handle all options for the
* solver and the parser.
* @return Exit code.
*/
public int run(Script script, String filename);
public int run(Script script, String filename, OptionMap options);
}
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
import java.io.FileNotFoundException;

import de.uni_freiburg.informatik.ultimate.logic.LoggingScript;
import de.uni_freiburg.informatik.ultimate.smtinterpol.option.OptionMap;
import de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment;
import de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol;

Expand All @@ -38,8 +39,11 @@ public static void main(String[] args) {
String infile = args[0];
String outfile = args[1];
try {
DefaultLogger logger = new DefaultLogger();
OptionMap options = new OptionMap(logger, true);
ParseEnvironment pe = new ParseEnvironment(
new LoggingScript(new SMTInterpol(), outfile, true));
new LoggingScript(new SMTInterpol(logger), outfile, true),
options);
pe.parseScript(infile);
} catch (FileNotFoundException e) {
e.printStackTrace();
Expand Down

0 comments on commit 656452f

Please sign in to comment.