diff --git a/.gitignore b/.gitignore index 7f953ccdb..42635d337 100644 --- a/.gitignore +++ b/.gitignore @@ -107,3 +107,4 @@ gradle-app.setting /.dbeaver /Scripts /.vscode/ +workspace.code-workspace diff --git a/README.md b/README.md index 6992cc5c6..6e5147a2c 100644 --- a/README.md +++ b/README.md @@ -42,6 +42,8 @@ $ java -jar alpha.jar -i benchmarks/omiga/omiga-testcases/3col/3col-10-18.txt -f Note that in this example the path to the input file is relative to the root of this repository. If you have not checked out the repository, you can just [download the example file from GitHub](/benchmarks/omiga/omiga-testcases/3col/3col-10-18.txt). +[A coder's guide to answer set programming](https://madmike200590.github.io/asp-guide/) provides a short and high-level tutorial on Answer Set Programming. + ## Building Alpha uses the [Gradle build automation system](https://gradle.org). Executing @@ -73,6 +75,10 @@ run into trouble feel free to file an issue. ## Suggested Reading +### Beginners' Tutorials + * [A coder's guide to answer set programming](https://madmike200590.github.io/asp-guide/) + +### Theoretical Background and Language Specification * [Answer Set Programming: A Primer](http://www.kr.tuwien.ac.at/staff/tkren/pub/2009/rw2009-asp.pdf) * [ASP-Core-2 Input Language Format](https://www.mat.unical.it/aspcomp2013/files/ASP-CORE-2.01c.pdf) * [Conflict-Driven Answer Set Solving: From Theory to Practice](http://www.cs.uni-potsdam.de/wv/pdfformat/gekasc12c.pdf) @@ -82,6 +88,10 @@ run into trouble feel free to file an issue. Peer-reviewed publications part of journals, conferences and workshops: +#### 2021 + + * [Solving Configuration Problems with ASP and Declarative Domain-Specific Heuristics](http://ceur-ws.org/Vol-2945/21-RT-ConfWS21_paper_4.pdf) + #### 2020 * [Conflict Generalisation in ASP: Learning Correct and Effective Non-Ground Constraints](https://doi.org/10.1017/S1471068420000368) diff --git a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java index 27019ce10..f32750183 100644 --- a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java +++ b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java @@ -58,6 +58,7 @@ public class SystemConfig { public static final boolean DEFAULT_SORT_ANSWER_SETS = false; public static final List DEFAULT_REPLAY_CHOICES = Collections.emptyList(); public static final boolean DEFAULT_STRATIFIED_EVALUATION = true; + public static final boolean DEFAULT_PREPROCESSING_ENABLED = true; public static final boolean DEFAULT_DISABLE_NOGOOD_DELETION = false; public static final String DEFAULT_GROUNDER_TOLERANCE_CONSTRAINTS = GrounderHeuristicsConfiguration.STRICT_STRING; public static final String DEFAULT_GROUNDER_TOLERANCE_RULES = GrounderHeuristicsConfiguration.STRICT_STRING; @@ -79,6 +80,7 @@ public class SystemConfig { private boolean sortAnswerSets = DEFAULT_SORT_ANSWER_SETS; private List replayChoices = DEFAULT_REPLAY_CHOICES; private boolean evaluateStratifiedPart = DEFAULT_STRATIFIED_EVALUATION; + private boolean enablePreprocessing = DEFAULT_PREPROCESSING_ENABLED; private boolean disableNoGoodDeletion = DEFAULT_DISABLE_NOGOOD_DELETION; private String grounderToleranceConstraints = DEFAULT_GROUNDER_TOLERANCE_CONSTRAINTS; private String grounderToleranceRules = DEFAULT_GROUNDER_TOLERANCE_RULES; @@ -232,6 +234,14 @@ public void setEvaluateStratifiedPart(boolean evaluateStratifiedPart) { this.evaluateStratifiedPart = evaluateStratifiedPart; } + public boolean isPreprocessingEnabled() { + return this.enablePreprocessing; + } + + public void setPreprocessingEnabled(boolean enablePreprocessing) { + this.enablePreprocessing = enablePreprocessing; + } + public boolean isDisableNoGoodDeletion() { return this.disableNoGoodDeletion; } diff --git a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/terms/IntervalTerm.java b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/terms/IntervalTerm.java new file mode 100644 index 000000000..3e3a7f394 --- /dev/null +++ b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/terms/IntervalTerm.java @@ -0,0 +1,14 @@ +package at.ac.tuwien.kr.alpha.api.terms; + +/** + * A term representing an interval of integers. + * Intervals are syntactic sugar, e.g. the rule "p(X) :- X = 1..2." is a shorthand for + * "p(X) :- X = 1. p(X) :- X = 2.". + */ +public interface IntervalTerm extends Term { + + Term getLowerBound(); + + Term getUpperBound(); + +} diff --git a/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java b/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java index 4b3ccf1f5..ea461dd57 100644 --- a/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java +++ b/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java @@ -149,6 +149,9 @@ public class CommandLineParser { .desc("a character (sequence) to use as separator for atoms in printed answer sets (default: " + SystemConfig.DEFAULT_ATOM_SEPARATOR + ")") .build(); + private static final Option OPT_DISABLE_PROGRAM_PREPROCESSING = Option.builder("dpp").longOpt("disableProgramPreprocessing") + .desc("disable preprocessing of input program") + .build(); //@formatter:on private static final Options CLI_OPTS = new Options(); @@ -189,6 +192,7 @@ public class CommandLineParser { CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_TOLERANCE_RULES); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_ACCUMULATOR_ENABLED); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_OUTPUT_ATOM_SEPARATOR); + CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_DISABLE_PROGRAM_PREPROCESSING); } /* @@ -240,12 +244,13 @@ private void initializeGlobalOptionHandlers() { this.globalOptionHandlers.put(CommandLineParser.OPT_NO_JUSTIFICATION.getOpt(), this::handleNoJustification); this.globalOptionHandlers.put(CommandLineParser.OPT_AGGREGATES_NO_SORTING_GRID.getOpt(), this::handleDisableSortingGrid); this.globalOptionHandlers.put(CommandLineParser.OPT_AGGREGATES_NO_NEGATIVE_INTEGERS.getOpt(), this::handleDisableNegativeSumElements); - this.globalOptionHandlers.put(CommandLineParser.OPT_NO_EVAL_STRATIFIED.getOpt(), this::handleDisableStratifedEval); + this.globalOptionHandlers.put(CommandLineParser.OPT_NO_EVAL_STRATIFIED.getOpt(), this::handleDisableStratifiedEval); this.globalOptionHandlers.put(CommandLineParser.OPT_NO_NOGOOD_DELETION.getOpt(), this::handleNoNoGoodDeletion); this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_TOLERANCE_CONSTRAINTS.getOpt(), this::handleGrounderToleranceConstraints); this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_TOLERANCE_RULES.getOpt(), this::handleGrounderToleranceRules); this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_ACCUMULATOR_ENABLED.getOpt(), this::handleGrounderNoInstanceRemoval); this.globalOptionHandlers.put(CommandLineParser.OPT_OUTPUT_ATOM_SEPARATOR.getOpt(), this::handleAtomSeparator); + this.globalOptionHandlers.put(CommandLineParser.OPT_DISABLE_PROGRAM_PREPROCESSING.getOpt(), this::handleDisablePreprocessing); } private void initializeInputOptionHandlers() { @@ -441,7 +446,7 @@ private void handleDisableNegativeSumElements(Option opt, SystemConfig cfg) { cfg.getAggregateRewritingConfig().setSupportNegativeValuesInSums(false); } - private void handleDisableStratifedEval(Option opt, SystemConfig cfg) { + private void handleDisableStratifiedEval(Option opt, SystemConfig cfg) { cfg.setEvaluateStratifiedPart(false); } @@ -470,5 +475,9 @@ private void handleGrounderNoInstanceRemoval(Option opt, SystemConfig cfg) { private void handleAtomSeparator(Option opt, SystemConfig cfg) { cfg.setAtomSeparator(StringEscapeUtils.unescapeJava(opt.getValue(SystemConfig.DEFAULT_ATOM_SEPARATOR))); } + + private void handleDisablePreprocessing(Option opt, SystemConfig cfg) { + cfg.setPreprocessingEnabled(false); + } } diff --git a/alpha-cli-app/src/main/resources/simplelogger.properties b/alpha-cli-app/src/main/resources/simplelogger.properties index e9d221fed..2585a0852 100644 --- a/alpha-cli-app/src/main/resources/simplelogger.properties +++ b/alpha-cli-app/src/main/resources/simplelogger.properties @@ -22,8 +22,7 @@ org.slf4j.simpleLogger.log.at.ac.tuwien.kr.alpha.core.solver.heuristics.HeapOfAc org.slf4j.simpleLogger.showDateTime=true # Format for logged timestamps. -# For Alpha, we use milliseconds since startup -org.slf4j.simpleLogger.dateTimeFormat=S +# For Alpha, we use milliseconds since startup, which is the default time format # Disable including thread name in logged line since Alpha is currently single-threaded. org.slf4j.simpleLogger.showThreadName=false \ No newline at end of file diff --git a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParserTest.java b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParserTest.java index f77f6527e..52ac06c16 100644 --- a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParserTest.java +++ b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParserTest.java @@ -181,4 +181,11 @@ public void atomSeparator() throws ParseException { assertEquals("some-string", cfg.getSystemConfig().getAtomSeparator()); } + @Test + public void disableProgramPreprocessing() throws ParseException { + CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION); + AlphaConfig ctx = parser.parseCommandLine(new String[]{"-str", "aString.", "-dpp"}); + assertFalse(ctx.getSystemConfig().isPreprocessingEnabled()); + } + } diff --git a/alpha-cli-app/src/test/resources/simplelogger.properties b/alpha-cli-app/src/test/resources/simplelogger.properties index a4e464d4a..f2ae884d2 100644 --- a/alpha-cli-app/src/test/resources/simplelogger.properties +++ b/alpha-cli-app/src/test/resources/simplelogger.properties @@ -22,8 +22,7 @@ org.slf4j.simpleLogger.log.at.ac.tuwien.kr.alpha.core.solver.heuristics.HeapOfAc org.slf4j.simpleLogger.showDateTime=true # Format for logged timestamps. -# For Alpha, we use milliseconds since startup -org.slf4j.simpleLogger.dateTimeFormat=S +# For Alpha, we use milliseconds since startup, which is the default time format # Disable including thread name in logged line since Alpha is currently single-threaded. org.slf4j.simpleLogger.showThreadName=false \ No newline at end of file diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/terms/IntervalTerm.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/terms/IntervalTermImpl.java similarity index 51% rename from alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/terms/IntervalTerm.java rename to alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/terms/IntervalTermImpl.java index 069a47382..eb14b44f7 100644 --- a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/terms/IntervalTerm.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/terms/IntervalTermImpl.java @@ -4,28 +4,25 @@ import java.util.Set; import at.ac.tuwien.kr.alpha.api.grounder.Substitution; -import at.ac.tuwien.kr.alpha.api.terms.FunctionTerm; +import at.ac.tuwien.kr.alpha.api.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; import at.ac.tuwien.kr.alpha.commons.util.Interner; -import at.ac.tuwien.kr.alpha.commons.util.Util; /** * An IntervalTerm represents the shorthand notation for a set of rules where all elements in this interval occur once, e.g., fact(2..5). * An IntervalTerm is a meta-term and the grounder must replace it with its corresponding set of facts or rules. * Copyright (c) 2017, the Alpha Team. */ -public class IntervalTerm extends AbstractTerm { - private static final Interner INTERNER = new Interner<>(); +class IntervalTermImpl extends AbstractTerm implements IntervalTerm { + + private static final Interner INTERNER = new Interner<>(); private final Term lowerBoundTerm; private final Term upperBoundTerm; - private final int lowerBound; - private final int upperBound; - private final boolean ground; - private IntervalTerm(Term lowerBound, Term upperBound) { + private IntervalTermImpl(Term lowerBound, Term upperBound) { if (lowerBound == null || upperBound == null) { throw new IllegalArgumentException(); } @@ -34,18 +31,10 @@ private IntervalTerm(Term lowerBound, Term upperBound) { this.lowerBoundTerm = lowerBound; this.upperBoundTerm = upperBound; - - if (this.ground) { - this.upperBound = Integer.parseInt(upperBoundTerm.toString()); - this.lowerBound = Integer.parseInt(lowerBoundTerm.toString()); - } else { - this.upperBound = -1; - this.lowerBound = -1; - } } - public static IntervalTerm getInstance(Term lowerBound, Term upperBound) { - return INTERNER.intern(new IntervalTerm(lowerBound, upperBound)); + static IntervalTermImpl getInstance(Term lowerBound, Term upperBound) { + return INTERNER.intern(new IntervalTermImpl(lowerBound, upperBound)); } @Override @@ -53,25 +42,11 @@ public boolean isGround() { return this.ground; } - public int getLowerBound() { - if (!isGround()) { - throw Util.oops("Cannot get the lower bound of non-ground interval"); - } - return this.lowerBound; - } - - public int getUpperBound() { - if (!isGround()) { - throw Util.oops("Cannot get the upper bound of non-ground interval"); - } - return this.upperBound; - } - - public Term getLowerBoundTerm() { + public Term getLowerBound() { return lowerBoundTerm; } - public Term getUpperBoundTerm() { + public Term getUpperBound() { return upperBoundTerm; } @@ -88,11 +63,11 @@ public Set getOccurringVariables() { } @Override - public IntervalTerm substitute(Substitution substitution) { + public IntervalTermImpl substitute(Substitution substitution) { if (isGround()) { return this; } - return new IntervalTerm(lowerBoundTerm.substitute(substitution), upperBoundTerm.substitute(substitution)); + return new IntervalTermImpl(lowerBoundTerm.substitute(substitution), upperBoundTerm.substitute(substitution)); } @Override @@ -109,7 +84,7 @@ public boolean equals(Object o) { return false; } - IntervalTerm that = (IntervalTerm) o; + IntervalTermImpl that = (IntervalTermImpl) o; if (!lowerBoundTerm.equals(that.lowerBoundTerm)) { return false; @@ -130,41 +105,14 @@ public int compareTo(Term o) { @Override public Term renameVariables(String renamePrefix) { - return new IntervalTerm(lowerBoundTerm.renameVariables(renamePrefix), upperBoundTerm.renameVariables(renamePrefix)); + return new IntervalTermImpl(lowerBoundTerm.renameVariables(renamePrefix), upperBoundTerm.renameVariables(renamePrefix)); } @Override public Term normalizeVariables(String renamePrefix, Term.RenameCounter counter) { - return IntervalTerm.getInstance( + return IntervalTermImpl.getInstance( lowerBoundTerm.normalizeVariables(renamePrefix, counter), upperBoundTerm.normalizeVariables(renamePrefix, counter)); } - /** - * Returns true if the term contains (or is) some IntervalTerm. - * @param term the term to test - * @return true iff an IntervalTerm occurs in term. - */ - public static boolean termContainsIntervalTerm(Term term) { - if (term instanceof IntervalTerm) { - return true; - } else if (term instanceof FunctionTermImpl) { - return functionTermContainsIntervals((FunctionTermImpl) term); - } else { - return false; - } - } - - public static boolean functionTermContainsIntervals(FunctionTerm functionTerm) { - // Test whether a function term contains an interval term (recursively). - for (Term term : functionTerm.getTerms()) { - if (term instanceof IntervalTerm) { - return true; - } - if (term instanceof FunctionTermImpl && functionTermContainsIntervals((FunctionTerm) term)) { - return true; - } - } - return false; - } } \ No newline at end of file diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/terms/Terms.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/terms/Terms.java index b02e00c7b..c651a70aa 100644 --- a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/terms/Terms.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/terms/Terms.java @@ -9,6 +9,7 @@ import at.ac.tuwien.kr.alpha.api.terms.ArithmeticTerm; import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.api.terms.FunctionTerm; +import at.ac.tuwien.kr.alpha.api.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; import at.ac.tuwien.kr.alpha.commons.substitutions.Unifier; @@ -65,6 +66,10 @@ public static Term newMinusTerm(Term negatedTerm) { return MinusTerm.getInstance(negatedTerm); } + public static IntervalTerm newIntervalTerm(Term lowerBound, Term upperBound) { + return IntervalTermImpl.getInstance(lowerBound, upperBound); + } + @SafeVarargs public static > List> asTermList(T... values) { List> retVal = new ArrayList<>(); @@ -117,4 +122,36 @@ static Integer evaluateGroundTermHelper(Term term) { } } + /** + * Returns true if the term contains (or is) some IntervalTerm. + * @param term the term to test + * @return true iff an IntervalTerm occurs in term. + */ + public static boolean termContainsIntervalTerm(Term term) { + if (term instanceof IntervalTermImpl) { + return true; + } else if (term instanceof FunctionTermImpl) { + return functionTermContainsIntervals((FunctionTermImpl) term); + } else { + return false; + } + } + + /** + * Returns true if the given {@link FunctionTerm} contains some IntervalTerm. + * @param functionTerm the term to test + * @return true iff an IntervalTerm occurs in functionTerm. + */ + public static boolean functionTermContainsIntervals(FunctionTerm functionTerm) { + for (Term term : functionTerm.getTerms()) { + if (term instanceof IntervalTermImpl) { + return true; + } + if (term instanceof FunctionTermImpl && functionTermContainsIntervals((FunctionTerm) term)) { + return true; + } + } + return false; + } + } diff --git a/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/terms/TermTest.java b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/terms/TermTest.java index ea0ebcfc1..ebb36c0b8 100644 --- a/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/terms/TermTest.java +++ b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/terms/TermTest.java @@ -12,9 +12,14 @@ import org.junit.jupiter.api.Test; +import at.ac.tuwien.kr.alpha.api.grounder.Substitution; +import at.ac.tuwien.kr.alpha.api.terms.ArithmeticOperator; import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; +import at.ac.tuwien.kr.alpha.api.terms.FunctionTerm; +import at.ac.tuwien.kr.alpha.api.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; +import at.ac.tuwien.kr.alpha.commons.substitutions.BasicSubstitution; /** * Copyright (c) 2016-2021, the Alpha Team. @@ -27,10 +32,13 @@ public void testTermReferenceEquality() { // Terms must have a unique representation so that reference comparison is // sufficient to check // whether two terms are equal. + + // Test for constant terms. ConstantTerm ta1 = Terms.newConstant("a"); ConstantTerm ta2 = Terms.newConstant("a"); assertTrue(ta1 == ta2, "Two instances of ConstantTerms for the same term symbol must be the same object"); + // Test for function terms. List termList = new LinkedList<>(); termList.add(ta1); termList.add(ta2); @@ -40,6 +48,21 @@ public void testTermReferenceEquality() { termList2.add(ta2); FunctionTermImpl ft2 = FunctionTermImpl.getInstance("f", termList2); assertTrue(ft1 == ft2, "Two instances of FunctionTerms for the same term symbol and equal term lists must be the same object"); + + // Test for arithmetic terms. + Term tArith1 = ArithmeticTermImpl.getInstance(Terms.newConstant(2), ArithmeticOperator.PLUS, Terms.newConstant(2)); + Term tArith2 = ArithmeticTermImpl.getInstance(Terms.newConstant(2), ArithmeticOperator.PLUS, Terms.newConstant(2)); + assertTrue(tArith1 == tArith2, "Two instances of ArithmeticTerms for the same operator symbol and equal term lists must be the same object"); + + // Test for interval terms. + IntervalTerm tInt1 = IntervalTermImpl.getInstance(Terms.newConstant(-3), Terms.newVariable("X")); + IntervalTerm tInt2 = IntervalTermImpl.getInstance(Terms.newConstant(-3), Terms.newVariable("X")); + assertTrue(tInt1 == tInt2, "Two instances of IntervalTerms for the same bounds must be the same object"); + + // Test for variables. + VariableTerm tVar1 = VariableTermImpl.getInstance("X"); + VariableTerm tVar2 = VariableTermImpl.getInstance("X"); + assertTrue(tVar1 == tVar2, "Two instances of VariableTerms for the same name must be the same object"); } @Test @@ -90,4 +113,30 @@ public void testStringVsConstantSymbolEquality() { // hashCode, i.e. return a non-zero result for non-equal objects assertNotEquals(0, stringConstant.compareTo(constantSymbol)); } + + @Test + public void testVariableSubstitution() { + Substitution substitution = new BasicSubstitution(); + substitution.put(Terms.newVariable("X"), Terms.newConstant(1)); + + // Test variable term (trivial case, substituting results in constant). + VariableTerm var = VariableTermImpl.getInstance("X"); + Term substitutedVar = var.substitute(substitution); + assertEquals(Terms.newConstant(1), substitutedVar); + + // Test function term. + FunctionTerm func = FunctionTermImpl.getInstance("f", VariableTermImpl.getInstance("X")); + Term substitutedFunc = func.substitute(substitution); + assertTrue(substitutedFunc.isGround()); + + // Test arithmetic term (note that arithmetic term with ground operands gets evaluated, result is therefore "2" rather than "1 + 1" ). + Term arith = ArithmeticTermImpl.getInstance(VariableTermImpl.getInstance("X"), ArithmeticOperator.PLUS, ConstantTermImpl.getInstance(1)); + Term substitutedArith = arith.substitute(substitution); + assertEquals(Terms.newConstant(2), substitutedArith); + + // Test interval term. + IntervalTerm interval = IntervalTermImpl.getInstance(VariableTermImpl.getInstance("X"), Terms.newConstant(3)); + Term substitutedInterval = interval.substitute(substitution); + assertEquals(Terms.newIntervalTerm(Terms.newConstant(1), Terms.newConstant(3)), substitutedInterval); + } } diff --git a/alpha-commons/src/test/resources/simplelogger.properties b/alpha-commons/src/test/resources/simplelogger.properties index a4e464d4a..f2ae884d2 100644 --- a/alpha-commons/src/test/resources/simplelogger.properties +++ b/alpha-commons/src/test/resources/simplelogger.properties @@ -22,8 +22,7 @@ org.slf4j.simpleLogger.log.at.ac.tuwien.kr.alpha.core.solver.heuristics.HeapOfAc org.slf4j.simpleLogger.showDateTime=true # Format for logged timestamps. -# For Alpha, we use milliseconds since startup -org.slf4j.simpleLogger.dateTimeFormat=S +# For Alpha, we use milliseconds since startup, which is the default time format # Disable including thread name in logged line since Alpha is currently single-threaded. org.slf4j.simpleLogger.showThreadName=false \ No newline at end of file diff --git a/alpha-core/src/main/antlr/at/ac/tuwien/kr/alpha/core/antlr/ASPCore2.g4 b/alpha-core/src/main/antlr/at/ac/tuwien/kr/alpha/core/antlr/ASPCore2.g4 index aeca5cc2d..4f80be1a2 100644 --- a/alpha-core/src/main/antlr/at/ac/tuwien/kr/alpha/core/antlr/ASPCore2.g4 +++ b/alpha-core/src/main/antlr/at/ac/tuwien/kr/alpha/core/antlr/ASPCore2.g4 @@ -56,7 +56,7 @@ terms : term (COMMA terms)?; term : ID # term_const | ID (PAREN_OPEN terms? PAREN_CLOSE) # term_func - | NUMBER # term_number + | numeral # term_number | QUOTED_STRING # term_string | VARIABLE # term_variable | ANONYMOUS_VARIABLE # term_anonymousVariable @@ -69,7 +69,11 @@ term : ID # term_const | term BITXOR term # term_bitxorArithTerm ; -interval : lower = (NUMBER | VARIABLE) DOT DOT upper = (NUMBER | VARIABLE); // NOT Core2 syntax, but widespread +numeral : MINUS? NUMBER; + +interval : lower = interval_bound DOT DOT upper = interval_bound; // NOT Core2 syntax, but widespread + +interval_bound : numeral | VARIABLE; external_atom : MINUS? AMPERSAND ID (SQUARE_OPEN input = terms SQUARE_CLOSE)? (PAREN_OPEN output = terms PAREN_CLOSE)?; // NOT Core2 syntax. @@ -81,7 +85,7 @@ basic_terms : basic_term (COMMA basic_terms)? ; basic_term : ground_term | variable_term; -ground_term : /*SYMBOLIC_CONSTANT*/ ID | QUOTED_STRING | MINUS? NUMBER; +ground_term : /*SYMBOLIC_CONSTANT*/ ID | QUOTED_STRING | numeral; variable_term : VARIABLE | ANONYMOUS_VARIABLE; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/atoms/IntervalAtom.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/atoms/IntervalAtom.java index 4c0236f95..f9d39be68 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/atoms/IntervalAtom.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/atoms/IntervalAtom.java @@ -34,10 +34,10 @@ import at.ac.tuwien.kr.alpha.api.programs.Predicate; import at.ac.tuwien.kr.alpha.api.programs.VariableNormalizableAtom; import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; +import at.ac.tuwien.kr.alpha.api.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.commons.Predicates; import at.ac.tuwien.kr.alpha.commons.atoms.AbstractAtom; -import at.ac.tuwien.kr.alpha.commons.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.commons.terms.Terms; import at.ac.tuwien.kr.alpha.commons.util.Util; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/atoms/IntervalLiteral.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/atoms/IntervalLiteral.java index b0f142c94..a0d762bf2 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/atoms/IntervalLiteral.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/atoms/IntervalLiteral.java @@ -37,12 +37,13 @@ import at.ac.tuwien.kr.alpha.api.grounder.Substitution; import at.ac.tuwien.kr.alpha.api.programs.literals.FixedInterpretationLiteral; import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; +import at.ac.tuwien.kr.alpha.api.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; import at.ac.tuwien.kr.alpha.commons.literals.AbstractLiteral; import at.ac.tuwien.kr.alpha.commons.substitutions.BasicSubstitution; -import at.ac.tuwien.kr.alpha.commons.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.commons.terms.Terms; +import at.ac.tuwien.kr.alpha.commons.util.Util; /** * @see IntervalAtom @@ -68,10 +69,20 @@ private List getIntervalSubstitutions(Substitution partialSubstitu List terms = getTerms(); Term intervalRepresentingVariable = terms.get(1); IntervalTerm intervalTerm = (IntervalTerm) terms.get(0); + if (!(intervalTerm.getLowerBound() instanceof ConstantTerm)) { + throw Util.oops("Lower bound of interval term " + intervalTerm + " is not a constant!"); + } + @SuppressWarnings("unchecked") + int intervalLowerBound = ((ConstantTerm) intervalTerm.getLowerBound()).getObject(); + if (!(intervalTerm.getUpperBound() instanceof ConstantTerm)) { + throw Util.oops("Upper bound of interval term " + intervalTerm + " is not a constant!"); + } + @SuppressWarnings("unchecked") + int intervalUpperBound = ((ConstantTerm) intervalTerm.getUpperBound()).getObject(); // Check whether intervalRepresentingVariable is bound already. if (intervalRepresentingVariable instanceof VariableTerm) { // Still a variable, generate all elements in the interval. - for (int i = intervalTerm.getLowerBound(); i <= intervalTerm.getUpperBound(); i++) { + for (int i = intervalLowerBound; i <= intervalUpperBound; i++) { Substitution ith = new BasicSubstitution(partialSubstitution); ith.put((VariableTerm) intervalRepresentingVariable, Terms.newConstant(i)); substitutions.add(ith); @@ -84,10 +95,9 @@ private List getIntervalSubstitutions(Substitution partialSubstitu // Term is not bound to an integer constant, not in the interval. return Collections.emptyList(); } - // TODO to avoid that type of unchecked cast, we may want interval terms to not extend AbstractTerm @SuppressWarnings("unchecked") Integer integer = ((ConstantTerm) intervalRepresentingVariable).getObject(); - if (intervalTerm.getLowerBound() <= integer && integer <= intervalTerm.getUpperBound()) { + if (intervalLowerBound <= integer && integer <= intervalUpperBound) { return Collections.singletonList(partialSubstitution); } return Collections.emptyList(); diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/NoGood.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/NoGood.java index 3575669ba..3705b0c18 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/NoGood.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/NoGood.java @@ -27,6 +27,14 @@ */ package at.ac.tuwien.kr.alpha.core.common; +import at.ac.tuwien.kr.alpha.commons.util.Util; +import at.ac.tuwien.kr.alpha.core.solver.Antecedent; + +import java.util.Arrays; +import java.util.Iterator; +import java.util.List; +import java.util.stream.IntStream; + import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomOf; import static at.ac.tuwien.kr.alpha.core.atoms.Literals.isNegated; import static at.ac.tuwien.kr.alpha.core.atoms.Literals.isPositive; @@ -37,14 +45,6 @@ import static at.ac.tuwien.kr.alpha.core.common.NoGoodInterface.Type.STATIC; import static at.ac.tuwien.kr.alpha.core.common.NoGoodInterface.Type.SUPPORT; -import java.util.Arrays; -import java.util.Iterator; -import java.util.List; -import java.util.stream.IntStream; - -import at.ac.tuwien.kr.alpha.commons.util.Util; -import at.ac.tuwien.kr.alpha.core.solver.Antecedent; - public class NoGood implements NoGoodInterface, Comparable { public static final int HEAD = 0; public static final NoGood UNSAT = new NoGood(); @@ -163,6 +163,11 @@ public void bumpActivity() { @Override public void decreaseActivity() { } + + @Override + public String toString() { + return NoGood.this + "(unwatched)"; + } }; } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/FactIntervalEvaluator.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/FactIntervalEvaluator.java index 197df1254..508f25cbe 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/FactIntervalEvaluator.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/FactIntervalEvaluator.java @@ -5,10 +5,11 @@ import java.util.List; import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; +import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.api.terms.FunctionTerm; +import at.ac.tuwien.kr.alpha.api.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.commons.substitutions.Instance; -import at.ac.tuwien.kr.alpha.commons.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.commons.terms.Terms; /** @@ -34,7 +35,7 @@ public static List constructFactInstances(Atom fact) { currentTerms[i] = term; if (term instanceof IntervalTerm) { containsIntervals = true; - } else if (term instanceof FunctionTerm && IntervalTerm.functionTermContainsIntervals((FunctionTerm) term)) { + } else if (term instanceof FunctionTerm && Terms.functionTermContainsIntervals((FunctionTerm) term)) { containsIntervals = true; throw new UnsupportedOperationException("Intervals inside function terms in facts are not supported yet. Try turning the fact into a rule."); } @@ -47,6 +48,7 @@ public static List constructFactInstances(Atom fact) { return unrollInstances(currentTerms, 0); } + @SuppressWarnings("unchecked") private static List unrollInstances(Term[] currentTerms, int currentPosition) { if (currentPosition == currentTerms.length) { return Collections.singletonList(new Instance(currentTerms)); @@ -58,8 +60,18 @@ private static List unrollInstances(Term[] currentTerms, int currentPo List instances = new ArrayList<>(); - int lower = ((IntervalTerm) currentTerm).getLowerBound(); - int upper = ((IntervalTerm) currentTerm).getUpperBound(); + Term lowerBoundTerm = ((IntervalTerm) currentTerm).getLowerBound(); + Term upperBoundTerm = ((IntervalTerm) currentTerm).getUpperBound(); + if (!(lowerBoundTerm instanceof ConstantTerm)) { + throw new IllegalArgumentException("Cannot unroll interval term with non-integer bound: " + lowerBoundTerm); + } + if (!(upperBoundTerm instanceof ConstantTerm)) { + throw new IllegalArgumentException("Cannot unroll interval term with non-integer bound: " + upperBoundTerm); + } + + int lower = ((ConstantTerm) lowerBoundTerm).getObject(); + int upper = ((ConstantTerm) upperBoundTerm).getObject(); + for (int i = lower; i <= upper; i++) { Term[] clonedTerms = currentTerms.clone(); diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounder.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounder.java index 1e498d50d..1b8483a0d 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounder.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounder.java @@ -221,7 +221,7 @@ private Set getRulesWithUniqueHead() { /** * Registers a starting literal of a NonGroundRule at its corresponding working memory. - * + * * @param nonGroundRule the rule in which the literal occurs. */ private void registerLiteralAtWorkingMemory(Literal literal, CompiledRule nonGroundRule) { @@ -291,7 +291,7 @@ public AnswerSet assignmentToAnswerSet(Iterable trueAtoms) { /** * Prepares facts of the input program for joining and derives all NoGoods representing ground rules. May only be called once. - * + * * @return */ protected HashMap bootstrap() { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/Unification.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/Unification.java index ab2647942..819890808 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/Unification.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/Unification.java @@ -65,10 +65,10 @@ public static Unifier instantiate(Atom general, Atom specific) { private static Unifier unifyAtoms(Atom left, Atom right, boolean keepLeftAsIs) { Set leftOccurringVariables = left.getOccurringVariables(); - Set rightOccurringVaribles = right.getOccurringVariables(); - boolean leftSmaller = leftOccurringVariables.size() < rightOccurringVaribles.size(); - Set smallerSet = leftSmaller ? leftOccurringVariables : rightOccurringVaribles; - Set largerSet = leftSmaller ? rightOccurringVaribles : leftOccurringVariables; + Set rightOccurringVariables = right.getOccurringVariables(); + boolean leftSmaller = leftOccurringVariables.size() < rightOccurringVariables.size(); + Set smallerSet = leftSmaller ? leftOccurringVariables : rightOccurringVariables; + Set largerSet = leftSmaller ? rightOccurringVariables : leftOccurringVariables; for (VariableTerm variableTerm : smallerSet) { if (largerSet.contains(variableTerm)) { throw oops("Left and right atom share variables."); diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ParseTreeVisitor.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ParseTreeVisitor.java index 1498a4f0c..868222d85 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ParseTreeVisitor.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ParseTreeVisitor.java @@ -61,6 +61,7 @@ import at.ac.tuwien.kr.alpha.api.terms.ArithmeticOperator; import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.api.terms.FunctionTerm; +import at.ac.tuwien.kr.alpha.api.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; import at.ac.tuwien.kr.alpha.commons.AnswerSets; @@ -69,10 +70,8 @@ import at.ac.tuwien.kr.alpha.commons.comparisons.ComparisonOperators; import at.ac.tuwien.kr.alpha.commons.literals.Literals; import at.ac.tuwien.kr.alpha.commons.rules.heads.Heads; -import at.ac.tuwien.kr.alpha.commons.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.commons.terms.Terms; import at.ac.tuwien.kr.alpha.core.antlr.ASPCore2BaseVisitor; -import at.ac.tuwien.kr.alpha.core.antlr.ASPCore2Lexer; import at.ac.tuwien.kr.alpha.core.antlr.ASPCore2Parser; import at.ac.tuwien.kr.alpha.core.programs.InputProgram; import at.ac.tuwien.kr.alpha.core.rules.BasicRule; @@ -320,7 +319,6 @@ public List visitBody(ASPCore2Parser.BodyContext ctx) { @Override public AggregateLiteral visitAggregate(ASPCore2Parser.AggregateContext ctx) { - // aggregate : NAF? (lt=term lop=binop)? aggregate_function CURLY_OPEN aggregate_elements CURLY_CLOSE (uop=binop ut=term)?; boolean isPositive = ctx.NAF() == null; Term lt = null; @@ -383,18 +381,17 @@ public Term visitBasic_term(ASPCore2Parser.Basic_termContext ctx) { @Override public Term visitGround_term(ASPCore2Parser.Ground_termContext ctx) { - // ground_term : ID | QUOTED_STRING | MINUS? NUMBER; + // ground_term : ID | QUOTED_STRING | numeral; if (ctx.ID() != null) { + // ID return Terms.newSymbolicConstant(ctx.ID().getText()); } else if (ctx.QUOTED_STRING() != null) { + // QUOTED_STRING String quotedString = ctx.QUOTED_STRING().getText(); return Terms.newConstant(quotedString.substring(1, quotedString.length() - 1)); } else { - int multiplier = 1; - if (ctx.MINUS() != null) { - multiplier = -1; - } - return Terms.newConstant(multiplier * Integer.parseInt(ctx.NUMBER().getText())); + // numeral + return Terms.newConstant(visitNumeral(ctx.numeral())); } } @@ -496,7 +493,14 @@ public List visitTerms(ASPCore2Parser.TermsContext ctx) { @Override public ConstantTerm visitTerm_number(ASPCore2Parser.Term_numberContext ctx) { - return Terms.newConstant(Integer.parseInt(ctx.NUMBER().getText())); + // term : numeral + return Terms.newConstant(visitNumeral(ctx.numeral())); + } + + public Integer visitNumeral(ASPCore2Parser.NumeralContext ctx) { + // numeral : MINUS? NUMBER; + int absValue = Integer.valueOf(ctx.NUMBER().getText()); + return ctx.MINUS() != null ? -1 * absValue : absValue; } @Override @@ -520,7 +524,6 @@ public VariableTerm visitTerm_anonymousVariable(ASPCore2Parser.Term_anonymousVar if (!acceptVariables) { throw notSupported(ctx); } - return Terms.newAnonymousVariable(); } @@ -529,7 +532,6 @@ public VariableTerm visitTerm_variable(ASPCore2Parser.Term_variableContext ctx) if (!acceptVariables) { throw notSupported(ctx); } - return Terms.newVariable(ctx.VARIABLE().getText()); } @@ -564,13 +566,21 @@ public ExternalAtom visitExternal_atom(ASPCore2Parser.External_atomContext ctx) @Override public IntervalTerm visitTerm_interval(ASPCore2Parser.Term_intervalContext ctx) { - // interval : lower = (NUMBER | VARIABLE) DOT DOT upper = (NUMBER | VARIABLE); + // interval : lower = interval_bound DOT DOT upper = interval_bound; ASPCore2Parser.IntervalContext ictx = ctx.interval(); - String lowerText = ictx.lower.getText(); - String upperText = ictx.upper.getText(); - Term lower = ictx.lower.getType() == ASPCore2Lexer.NUMBER ? Terms.newConstant(Integer.parseInt(lowerText)) : Terms.newVariable(lowerText); - Term upper = ictx.upper.getType() == ASPCore2Lexer.NUMBER ? Terms.newConstant(Integer.parseInt(upperText)) : Terms.newVariable(upperText); - return IntervalTerm.getInstance(lower, upper); + Term lower = visitInterval_bound(ictx.lower); + Term upper = visitInterval_bound(ictx.upper); + return Terms.newIntervalTerm(lower, upper); + } + + @Override + public Term visitInterval_bound(ASPCore2Parser.Interval_boundContext ctx) { + // interval_bound : numeral | VARIABLE; + if (ctx.numeral() != null) { + return Terms.newConstant(visitNumeral(ctx.numeral())); + } else { + return Terms.newVariable(ctx.VARIABLE().getText()); + } } @Override diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ArithmeticTermsRewriting.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ArithmeticTermsRewriting.java index 026cde8c5..259d410a9 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ArithmeticTermsRewriting.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ArithmeticTermsRewriting.java @@ -13,12 +13,12 @@ import at.ac.tuwien.kr.alpha.api.terms.ArithmeticTerm; import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.api.terms.FunctionTerm; +import at.ac.tuwien.kr.alpha.api.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; import at.ac.tuwien.kr.alpha.commons.comparisons.ComparisonOperators; import at.ac.tuwien.kr.alpha.commons.rules.heads.Heads; -import at.ac.tuwien.kr.alpha.commons.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.commons.terms.Terms; import at.ac.tuwien.kr.alpha.commons.util.Util; import at.ac.tuwien.kr.alpha.core.programs.NormalProgramImpl; @@ -171,7 +171,7 @@ private boolean containsArithmeticTerm(Term term) { } return false; } else if (term instanceof IntervalTerm) { - return containsArithmeticTerm(((IntervalTerm) term).getLowerBoundTerm()) || containsArithmeticTerm(((IntervalTerm) term).getUpperBoundTerm()); + return containsArithmeticTerm(((IntervalTerm) term).getLowerBound()) || containsArithmeticTerm(((IntervalTerm) term).getUpperBound()); } else { throw Util.oops("Unexpected term type: " + term.getClass()); } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ChoiceHeadToNormal.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ChoiceHeadToNormal.java index f54778b8c..70da8e765 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ChoiceHeadToNormal.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ChoiceHeadToNormal.java @@ -44,7 +44,6 @@ import at.ac.tuwien.kr.alpha.commons.Predicates; import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; import at.ac.tuwien.kr.alpha.commons.rules.heads.Heads; -import at.ac.tuwien.kr.alpha.commons.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.commons.terms.Terms; import at.ac.tuwien.kr.alpha.core.programs.InputProgram; import at.ac.tuwien.kr.alpha.core.rules.BasicRule; @@ -121,7 +120,7 @@ public ASPCore2Program apply(ASPCore2Program inputProgram) { private static boolean containsIntervalTerms(Atom atom) { for (Term term : atom.getTerms()) { - if (IntervalTerm.termContainsIntervalTerm(term)) { + if (Terms.termContainsIntervalTerm(term)) { return true; } } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/IntervalTermToIntervalAtom.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/IntervalTermToIntervalAtom.java index 36920ec71..013aaab5d 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/IntervalTermToIntervalAtom.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/IntervalTermToIntervalAtom.java @@ -41,10 +41,10 @@ import at.ac.tuwien.kr.alpha.api.rules.NormalRule; import at.ac.tuwien.kr.alpha.api.rules.heads.NormalHead; import at.ac.tuwien.kr.alpha.api.terms.FunctionTerm; +import at.ac.tuwien.kr.alpha.api.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; import at.ac.tuwien.kr.alpha.commons.rules.heads.Heads; -import at.ac.tuwien.kr.alpha.commons.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.commons.terms.Terms; import at.ac.tuwien.kr.alpha.core.atoms.IntervalAtom; import at.ac.tuwien.kr.alpha.core.programs.NormalProgramImpl; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/SimplePreprocessing.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/SimplePreprocessing.java new file mode 100644 index 000000000..565286378 --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/SimplePreprocessing.java @@ -0,0 +1,212 @@ +package at.ac.tuwien.kr.alpha.core.programs.transformation; + +import at.ac.tuwien.kr.alpha.api.programs.NormalProgram; +import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; +import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.api.programs.literals.BasicLiteral; +import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; +import at.ac.tuwien.kr.alpha.api.rules.NormalRule; +import at.ac.tuwien.kr.alpha.api.rules.Rule; +import at.ac.tuwien.kr.alpha.commons.rules.heads.Heads; +import at.ac.tuwien.kr.alpha.core.grounder.Unification; +import at.ac.tuwien.kr.alpha.core.programs.NormalProgramImpl; +import at.ac.tuwien.kr.alpha.core.rules.NormalRuleImpl; + +import java.util.*; + +import static java.util.stream.Collectors.toList; + +/** + * Simplifies the input program by deleting redundant literals and rules, as well as identifying rule heads that can + * always be derived from facts and adding them to the known facts. The approach is adopted from preprocessing + * techniques employed by traditional ground ASP solvers, as seen in: + * @see doi:10.3233/978-1-58603-891-5-15 + */ +public class SimplePreprocessing extends ProgramTransformation { + + + /** + * Evaluates all rules of the input program and tries to simplify them by applying a number of rule transformations. + * @param inputProgram a normalized ASP program to be preprocessed. + * @return the preprocessed program. + */ + @Override + public NormalProgram apply(NormalProgram inputProgram) { + List srcRules = inputProgram.getRules(); + Set newRules = new LinkedHashSet<>(); + Set facts = new LinkedHashSet<>(inputProgram.getFacts()); + + // Check if the rules are redundant or will never fire, without taking other rules into consideration. + for (NormalRule rule: srcRules) { + if (facts.contains(rule.getHeadAtom()) || containsConflictingBodyLiterals(rule) || containsHeadInPositiveBody(rule)) { + continue; + } + if (containsHeadInNegativeBody(rule)) { + newRules.add(new NormalRuleImpl(null, new ArrayList<>(rule.getBody()))); + } + newRules.add(rule); + } + srcRules = new LinkedList<>(newRules); + + // Analyze every rule in regard to the other rules and facts and if applicable, simplify or remove it. Repeat + // until a fixpoint is reached. + boolean canBePreprocessed = true; + while (canBePreprocessed) { + newRules = new LinkedHashSet<>(); + canBePreprocessed = false; + for (NormalRule rule : srcRules) { + RuleEvaluation eval = evaluateRule(rule, srcRules, facts); + if (eval == RuleEvaluation.NO_FIRE) { + canBePreprocessed = true; + } else if (eval.isFact()) { + facts.add(eval.getRule().getHeadAtom()); + canBePreprocessed = true; + } else if (eval.isModified()) { + newRules.add(eval.getRule()); + canBePreprocessed = true; + } else { + newRules.add(rule); + } + } + srcRules = new LinkedList<>(newRules); + } + return new NormalProgramImpl(new LinkedList<>(newRules), new LinkedList<>(facts), inputProgram.getInlineDirectives()); + } + + private boolean containsConflictingBodyLiterals(NormalRule rule) { + for (Literal positiveLiteral : rule.getPositiveBody()) { + if (rule.getNegativeBody().contains(positiveLiteral.negate())) { + return true; + } + } + return false; + } + + private boolean containsHeadInPositiveBody(NormalRule rule) { + Atom headAtom = rule.getHeadAtom(); + for (Literal literal : rule.getPositiveBody()) { + if (literal.getAtom().equals(headAtom)) { + return true; + } + } + return false; + } + + private boolean containsHeadInNegativeBody(NormalRule rule) { + Atom headAtom = rule.getHeadAtom(); + for (Literal literal : rule.getNegativeBody()) { + if (literal.getAtom().equals(headAtom)) { + return true; + } + } + return false; + } + + /** + * Evaluates and attempts to simplify a rule by looking for always-true and always-false literals. + * @param rule the rule to be evaluated. + * @param rules the rules from which literals could be derived from. + * @param facts the facts from which literals could be derived from. + * @return The ({@link RuleEvaluation}) contains the possibly simplified rule and indicates whether it was + * modified, is a fact or will never fire. + */ + private RuleEvaluation evaluateRule(NormalRule rule, List rules, Set facts) { + // Collect all literals that can be removed from the rule here. + Set redundantLiterals = new LinkedHashSet<>(); + + // Check if body literals can be derived from facts or other rules. If a body literal is not derivable, the + // rule can never fire. If a literal is already proven within the program context, the rule will be simplified + // by removing the literal. + List basicBodyLiterals = rule.getBody().stream().filter(BasicLiteral.class::isInstance).collect(toList()); + for (Literal literal : basicBodyLiterals) { + if (literal.isNegated() && facts.contains(literal.getAtom()) + || !literal.isNegated() && isNonDerivable(literal.getAtom(), rules, facts)) { + return RuleEvaluation.NO_FIRE; + } + if (literal.isNegated() && isNonDerivable(literal.getAtom(), rules, facts) + || !literal.isNegated() && facts.contains(literal.getAtom())) { + redundantLiterals.add(literal); + } + } + + // Checks if a constraint has the same body, meaning the had of the rule cannot be derived by the rule. + List constraints = rules.stream().filter(Rule::isConstraint).collect(toList()); + for (NormalRule constraint : constraints) { + if (!rule.isConstraint() && rule.getBody().equals(constraint.getBody())) { + return RuleEvaluation.NO_FIRE; + } + } + + if (redundantLiterals.isEmpty()) { + return new RuleEvaluation(rule, false, false); + } else { + return removeLiteralsFromRule(rule, redundantLiterals); + } + } + + // Checks if an atom cannot be derived from a rule or a fact. + private boolean isNonDerivable(Atom atom, List rules, Set facts) { + Atom tempAtom = atom.renameVariables("Prep"); + for (NormalRule rule : rules) { + if (!rule.isConstraint() && Unification.unifyAtoms(rule.getHeadAtom(), tempAtom) != null) { + return false; + } + } + for (Atom fact:facts) { + if ((Unification.instantiate(tempAtom, fact)) != null) { + return false; + } + } + return true; + } + + /** + * Removes a set of given literals from the rule body. + * @param rule the rule from which literals should be removed. + * @param literals The literals to remove. + * @return the resulting rule or fact. + */ + private RuleEvaluation removeLiteralsFromRule(NormalRule rule, Set literals) { + BasicAtom headAtom = rule.getHeadAtom(); + Set newBody = new LinkedHashSet<>(); + for (Literal bodyLiteral : rule.getBody()) { + if (!literals.contains(bodyLiteral)) { + newBody.add(bodyLiteral); + } + } + NormalRuleImpl newRule = new NormalRuleImpl(headAtom != null ? Heads.newNormalHead(headAtom) : null, new LinkedList<>(newBody)); + if (newRule.isConstraint() && newBody.isEmpty()) { + return RuleEvaluation.NO_FIRE; + } + return new RuleEvaluation(newRule, !literals.isEmpty(), newBody.isEmpty() && !newRule.isConstraint()); + } + + /** + * Internal helper class containing the possibly simplified rule and indicates whether it could + * or could not be simplified, is a fact or will never fire. + */ + private static class RuleEvaluation { + public static final RuleEvaluation NO_FIRE = new RuleEvaluation(null, false, false); + private final NormalRule rule; + private final boolean isModified; + private final boolean isFact; + + public RuleEvaluation(NormalRule rule, boolean isModified, boolean isFact) { + this.rule = rule; + this.isModified = isModified; + this.isFact = isFact; + } + + public NormalRule getRule() { + return rule; + } + + public boolean isModified() { + return isModified; + } + + public boolean isFact() { + return isFact; + } + } +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStoreAlphaRoaming.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStoreAlphaRoaming.java index 8b4d1977e..4e80e769f 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStoreAlphaRoaming.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStoreAlphaRoaming.java @@ -774,7 +774,7 @@ public int size() { @Override public String toString() { - return "BinaryWatchList(" + forLiteral + ")"; + return "BinaryWatchList(" + literalToString(forLiteral) + ")"; } @Override diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java index 9194925d8..10716621d 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java @@ -27,6 +27,19 @@ */ package at.ac.tuwien.kr.alpha.core.solver; +import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.core.common.Assignment; +import at.ac.tuwien.kr.alpha.core.common.AtomStore; +import at.ac.tuwien.kr.alpha.core.common.IntIterator; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; +import java.util.List; +import java.util.Set; + import static at.ac.tuwien.kr.alpha.commons.util.Util.arrayGrowthSize; import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomOf; @@ -37,20 +50,6 @@ import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.MBT; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.TRUE; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.HashSet; -import java.util.List; -import java.util.Set; - -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; -import at.ac.tuwien.kr.alpha.core.common.Assignment; -import at.ac.tuwien.kr.alpha.core.common.AtomStore; -import at.ac.tuwien.kr.alpha.core.common.IntIterator; - /** * An implementation of Assignment using a trail (of literals) and arrays as underlying structures for storing * assignments. @@ -73,7 +72,11 @@ public void bumpActivity() { @Override public void decreaseActivity() { + } + @Override + public String toString() { + return "ClosingIndicatorAntecedent"; } }; diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/parser/ParserTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/parser/ParserTest.java index d63009bbb..08f95a453 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/parser/ParserTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/parser/ParserTest.java @@ -27,6 +27,23 @@ */ package at.ac.tuwien.kr.alpha.core.parser; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertThrows; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import java.io.IOException; +import java.nio.channels.ReadableByteChannel; +import java.util.Arrays; +import java.util.Collections; +import java.util.List; +import java.util.Optional; +import java.util.stream.Stream; + +import org.antlr.v4.runtime.CharStream; +import org.antlr.v4.runtime.CharStreams; +import org.junit.jupiter.api.Test; + import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; import at.ac.tuwien.kr.alpha.api.programs.InlineDirectives; import at.ac.tuwien.kr.alpha.api.programs.atoms.AggregateAtom; @@ -35,30 +52,14 @@ import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; import at.ac.tuwien.kr.alpha.api.rules.heads.ChoiceHead; import at.ac.tuwien.kr.alpha.api.terms.FunctionTerm; +import at.ac.tuwien.kr.alpha.api.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; import at.ac.tuwien.kr.alpha.commons.Predicates; import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; import at.ac.tuwien.kr.alpha.commons.comparisons.ComparisonOperators; -import at.ac.tuwien.kr.alpha.commons.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.commons.terms.Terms; import at.ac.tuwien.kr.alpha.commons.util.Util; -import org.antlr.v4.runtime.CharStream; -import org.antlr.v4.runtime.CharStreams; -import org.junit.jupiter.api.Test; - -import java.io.IOException; -import java.nio.channels.ReadableByteChannel; -import java.util.Arrays; -import java.util.Collections; -import java.util.List; -import java.util.Optional; -import java.util.stream.Stream; - -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertFalse; -import static org.junit.jupiter.api.Assertions.assertThrows; -import static org.junit.jupiter.api.Assertions.assertTrue; /** * Copyright (c) 2016, the Alpha Team. @@ -124,9 +125,9 @@ public void parseProgramWithDisjunctionInHead() { public void parseInterval() { ASPCore2Program parsedProgram = parser.parse("fact(2..5). p(X) :- q(a, 3 .. X)."); IntervalTerm factInterval = (IntervalTerm) parsedProgram.getFacts().get(0).getTerms().get(0); - assertTrue(factInterval.equals(IntervalTerm.getInstance(Terms.newConstant(2), Terms.newConstant(5)))); + assertTrue(factInterval.equals(Terms.newIntervalTerm(Terms.newConstant(2), Terms.newConstant(5)))); IntervalTerm bodyInterval = (IntervalTerm) parsedProgram.getRules().get(0).getBody().stream().findFirst().get().getTerms().get(1); - assertTrue(bodyInterval.equals(IntervalTerm.getInstance(Terms.newConstant(3), Terms.newVariable("X")))); + assertTrue(bodyInterval.equals(Terms.newIntervalTerm(Terms.newConstant(3), Terms.newVariable("X")))); } @Test diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/SimplePreprocessingTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/SimplePreprocessingTest.java new file mode 100644 index 000000000..ccdbc4ec9 --- /dev/null +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/SimplePreprocessingTest.java @@ -0,0 +1,121 @@ +package at.ac.tuwien.kr.alpha.core.programs.transformation; + +import at.ac.tuwien.kr.alpha.api.programs.NormalProgram; +import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; +import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; +import at.ac.tuwien.kr.alpha.core.programs.NormalProgramImpl; +import org.junit.jupiter.api.Test; + +import java.util.HashSet; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +public class SimplePreprocessingTest { + + private final ProgramParser parser = new ProgramParserImpl(); + private final SimplePreprocessing evaluator = new SimplePreprocessing(); + + private NormalProgram parse(String str) { + return NormalProgramImpl.fromInputProgram(parser.parse(str)); + } + + private NormalProgram parseAndPreprocess(String str) { + return evaluator.apply(NormalProgramImpl.fromInputProgram(parser.parse(str))); + } + + @Test + public void testDuplicateRuleRemoval() { + String aspStr1 = "a :- not b. a :- not b. b :- not a."; + String aspStr2 = "a :- not b. b :- not a."; + NormalProgram preprocessedProgram = parseAndPreprocess(aspStr1); + NormalProgram parsedProgram = parse(aspStr2); + assertEquals(parsedProgram.getRules(), preprocessedProgram.getRules()); + assertEquals(new HashSet<>(parsedProgram.getFacts()), new HashSet<>(preprocessedProgram.getFacts())); + } + + @Test + public void testConflictingRuleRemoval() { + String aspStr1 = "a :- b, not b. b :- not c. c :- not b."; + String aspStr2 = " b :- not c. c :- not b."; + NormalProgram preprocessedProgram = parseAndPreprocess(aspStr1); + NormalProgram parsedProgram = parse(aspStr2); + assertEquals(parsedProgram.getRules(), preprocessedProgram.getRules()); + assertEquals(new HashSet<>(parsedProgram.getFacts()), new HashSet<>(preprocessedProgram.getFacts())); + } + + @Test + public void testHeadInBodyRuleRemoval() { + String aspStr1 = "a :- a, not b. b :- not c. c :- not b."; + String aspStr2 = " b :- not c. c :- not b."; + NormalProgram preprocessedProgram = parseAndPreprocess(aspStr1); + NormalProgram parsedProgram = parse(aspStr2); + assertEquals(parsedProgram.getRules(), preprocessedProgram.getRules()); + assertEquals(new HashSet<>(parsedProgram.getFacts()), new HashSet<>(preprocessedProgram.getFacts())); + } + + @Test + public void testNoFireRuleRemoval() { + String aspStr1 = "a :- not b. b :- not a. b :- c. d. e :- not d."; + String aspStr2 = "a :- not b. b :- not a. d."; + NormalProgram preprocessedProgram = parseAndPreprocess(aspStr1); + NormalProgram parsedProgram = parse(aspStr2); + assertEquals(parsedProgram.getRules(), preprocessedProgram.getRules()); + assertEquals(new HashSet<>(parsedProgram.getFacts()), new HashSet<>(preprocessedProgram.getFacts())); + } + + @Test + public void testAlwaysTrueLiteralRemoval() { + String aspStr1 = "a :- b, not c. b. c :- not a."; + String aspStr2 = "a :- not c. b. c :- not a."; + NormalProgram preprocessedProgram = parseAndPreprocess(aspStr1); + NormalProgram parsedProgram = parse(aspStr2); + assertEquals(parsedProgram.getRules(), preprocessedProgram.getRules()); + assertEquals(new HashSet<>(parsedProgram.getFacts()), new HashSet<>(preprocessedProgram.getFacts())); + } + + @Test + public void testNonDerivableLiteralRemovalNonGround() { + String aspStr1 = "r(X) :- p(X), not q(c). p(a). u(Y) :- s(Y), not v(Y). s(b) :- p(a), not v(a). v(a) :- not u(b)."; + String aspStr2 = "r(X) :- p(X). p(a). u(Y) :- s(Y), not v(Y). s(b) :- not v(a). v(a) :- not u(b)."; + NormalProgram preprocessedProgram = parseAndPreprocess(aspStr1); + NormalProgram parsedProgram = parse(aspStr2); + assertEquals(parsedProgram.getRules(), preprocessedProgram.getRules()); + assertEquals(new HashSet<>(parsedProgram.getFacts()), new HashSet<>(preprocessedProgram.getFacts())); + } + + @Test void testNonDerivableLiteralRemovalNonGround2() { + String aspStr1 = "p(X) :- q(X), not r(X). q(Y) :- p(Y), s(a). s(a)."; + String aspStr2 = "p(X) :- q(X). q(Y) :- p(Y). s(a)."; + NormalProgram preprocessedProgram = parseAndPreprocess(aspStr1); + NormalProgram parsedProgram = parse(aspStr2); + assertEquals(parsedProgram.getRules(), preprocessedProgram.getRules()); + assertEquals(new HashSet<>(parsedProgram.getFacts()), new HashSet<>(preprocessedProgram.getFacts())); + } + + @Test void testRuleToFact() { + String aspStr1 = "r(c) :- q(a), not p(b). q(a)."; + String aspStr2 = "r(c). q(a)."; + NormalProgram preprocessedProgram = parseAndPreprocess(aspStr1); + NormalProgram parsedProgram = parse(aspStr2); + assertEquals(parsedProgram.getRules(), preprocessedProgram.getRules()); + assertEquals(new HashSet<>(parsedProgram.getFacts()), new HashSet<>(preprocessedProgram.getFacts())); + } + + @Test void testAlwaysTrueLiteralRemovalNonGround() { + String aspStr1 = "r(X) :- t(X), s(b), not q(a). s(b). t(X) :- r(X). q(a) :- not r(a)."; + String aspStr2 = "r(X) :- t(X), not q(a). s(b). t(X) :- r(X). q(a) :- not r(a)."; + NormalProgram preprocessedProgram = parseAndPreprocess(aspStr1); + NormalProgram parsedProgram = parse(aspStr2); + assertEquals(parsedProgram.getRules(), preprocessedProgram.getRules()); + assertEquals(new HashSet<>(parsedProgram.getFacts()), new HashSet<>(preprocessedProgram.getFacts())); + } + + @Test void testHeadIsFactRuleRemoval() { + String aspStr1 = "r(a) :- not p(b). r(a). p(b) :- not q(c). q(c) :- not p(b)."; + String aspStr2 = " r(a). p(b) :- not q(c). q(c) :- not p(b)."; + NormalProgram preprocessedProgram = parseAndPreprocess(aspStr1); + NormalProgram parsedProgram = parse(aspStr2); + assertEquals(parsedProgram.getRules(), preprocessedProgram.getRules()); + assertEquals(new HashSet<>(parsedProgram.getFacts()), new HashSet<>(preprocessedProgram.getFacts())); + } +} \ No newline at end of file diff --git a/alpha-core/src/test/resources/simplelogger.properties b/alpha-core/src/test/resources/simplelogger.properties index a4e464d4a..f2ae884d2 100644 --- a/alpha-core/src/test/resources/simplelogger.properties +++ b/alpha-core/src/test/resources/simplelogger.properties @@ -22,8 +22,7 @@ org.slf4j.simpleLogger.log.at.ac.tuwien.kr.alpha.core.solver.heuristics.HeapOfAc org.slf4j.simpleLogger.showDateTime=true # Format for logged timestamps. -# For Alpha, we use milliseconds since startup -org.slf4j.simpleLogger.dateTimeFormat=S +# For Alpha, we use milliseconds since startup, which is the default time format # Disable including thread name in logged line since Alpha is currently single-threaded. org.slf4j.simpleLogger.showThreadName=false \ No newline at end of file diff --git a/alpha-solver/src/main/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImpl.java b/alpha-solver/src/main/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImpl.java index c49a5ca39..aaf619131 100644 --- a/alpha-solver/src/main/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImpl.java +++ b/alpha-solver/src/main/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImpl.java @@ -71,6 +71,7 @@ import at.ac.tuwien.kr.alpha.core.programs.InternalProgram; import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation; import at.ac.tuwien.kr.alpha.core.programs.transformation.StratifiedEvaluation; +import at.ac.tuwien.kr.alpha.core.programs.transformation.SimplePreprocessing; import at.ac.tuwien.kr.alpha.core.solver.SolverFactory; public class AlphaImpl implements Alpha { @@ -141,8 +142,13 @@ public NormalProgram normalizeProgram(ASPCore2Program program) { @VisibleForTesting InternalProgram performProgramPreprocessing(NormalProgram program) { - LOGGER.debug("Preprocessing InternalProgram!"); + LOGGER.debug("Performing program preprocessing!"); InternalProgram retVal = InternalProgram.fromNormalProgram(program); + if (config.isPreprocessingEnabled()) { + SimplePreprocessing simplePreprocessing = new SimplePreprocessing(); + NormalProgram simplePreprocessed = simplePreprocessing.apply(program); + retVal = InternalProgram.fromNormalProgram(simplePreprocessed); + } if (config.isEvaluateStratifiedPart()) { AnalyzedProgram analyzed = new AnalyzedProgram(retVal.getRules(), retVal.getFacts()); retVal = new StratifiedEvaluation().apply(analyzed); diff --git a/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImplTest.java b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImplTest.java index 176862d40..1d73948c1 100644 --- a/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImplTest.java +++ b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImplTest.java @@ -618,6 +618,7 @@ public void testLearnedUnaryNoGoodCausingOutOfOrderLiteralsConflict() throws IOE config.setDebugInternalChecks(true); config.setDisableJustificationSearch(false); config.setEvaluateStratifiedPart(false); + config.setPreprocessingEnabled(false); config.setReplayChoices(Arrays.asList(21, 26, 36, 56, 91, 96, 285, 166, 101, 290, 106, 451, 445, 439, 448, 433, 427, 442, 421, 415, 436, 409, 430, 397, 391, 424, 385, 379, 418, 373, 412, 406, 394, 388, 382, 245, 232, 208 @@ -626,5 +627,5 @@ public void testLearnedUnaryNoGoodCausingOutOfOrderLiteralsConflict() throws IOE Optional answerSet = alpha.solve(parsedProgram).findFirst(); assertTrue(answerSet.isPresent()); } - + } diff --git a/alpha-solver/src/test/resources/simplelogger.properties b/alpha-solver/src/test/resources/simplelogger.properties index a4e464d4a..f2ae884d2 100644 --- a/alpha-solver/src/test/resources/simplelogger.properties +++ b/alpha-solver/src/test/resources/simplelogger.properties @@ -22,8 +22,7 @@ org.slf4j.simpleLogger.log.at.ac.tuwien.kr.alpha.core.solver.heuristics.HeapOfAc org.slf4j.simpleLogger.showDateTime=true # Format for logged timestamps. -# For Alpha, we use milliseconds since startup -org.slf4j.simpleLogger.dateTimeFormat=S +# For Alpha, we use milliseconds since startup, which is the default time format # Disable including thread name in logged line since Alpha is currently single-threaded. org.slf4j.simpleLogger.showThreadName=false \ No newline at end of file