ignore unsupported CHC regression tests (#679)

trunk/examples/smtlib/horn/regression/.testignore

@@ -0,0 +1,8 @@
+UNKNOWN:
+# Introduces Skolem functions which TreeAutomizer does not support (#679)
+- task: test-nested-quantifiers-mcarthy-sat.smt2
+  settings: TreeAutomizerStandardSettings.epf
+  toolchain: TreeAutomizer.xml
+- task: test-nested-quantifiers-mcarthy-hard-sat.smt2
+  settings: TreeAutomizerStandardSettings.epf
+  toolchain: TreeAutomizer.xml

trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ChcTestResultDecider.java

@@ -27,24 +27,30 @@
  */
 package de.uni_freiburg.informatik.ultimate.test.decider;
 
+import java.util.regex.Pattern;
+
 import de.uni_freiburg.informatik.ultimate.test.UltimateRunDefinition;
 import de.uni_freiburg.informatik.ultimate.test.decider.expectedresult.IExpectedResultFinder;
 import de.uni_freiburg.informatik.ultimate.test.decider.expectedresult.SMTLibExpectedResultFinder;
-import de.uni_freiburg.informatik.ultimate.test.decider.overallresult.IOverallResultEvaluator;
 import de.uni_freiburg.informatik.ultimate.test.decider.overallresult.ChcOverallResult;
 import de.uni_freiburg.informatik.ultimate.test.decider.overallresult.ChcOverallResultEvaluator;
+import de.uni_freiburg.informatik.ultimate.test.decider.overallresult.IOverallResultEvaluator;
 
 public class ChcTestResultDecider extends ThreeTierTestResultDecider<ChcOverallResult> {
 
+	public ChcTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, final boolean unknownIsJUnitSuccess,
+			final String overriddenExpectedVerdict) {
+		super(ultimateRunDefinition, unknownIsJUnitSuccess, overriddenExpectedVerdict);
+	}
+
 	public ChcTestResultDecider(final UltimateRunDefinition ultimateRunDefinition,
 			final boolean unknownIsJUnitSuccess) {
 		super(ultimateRunDefinition, unknownIsJUnitSuccess);
 	}
 
 	@Override
 	public SMTLibExpectedResultFinder<ChcOverallResult> constructExpectedResultFinder() {
-		return new SMTLibExpectedResultFinder<>(ChcOverallResult.UNKNOWN, ChcOverallResult.SAT,
-				ChcOverallResult.UNSAT);
+		return new SMTLibExpectedResultFinder<>(ChcOverallResult.UNKNOWN, ChcOverallResult.SAT, ChcOverallResult.UNSAT);
 	}
 
 	@Override
@@ -69,6 +75,19 @@ public void evaluateTestResult(final IExpectedResultFinder<ChcOverallResult> exp
 			final ChcOverallResult expectedResult = expectedResultEvaluation.getExpectedResult();
 			final ChcOverallResult actualResult = overallResultDeterminer.getOverallResult();
 
+			if (mOverridenExpectedVerdict != null) {
+				final String overallResultMsg = overallResultDeterminer.generateOverallResultMessage();
+				final Pattern pattern = Pattern.compile(mOverridenExpectedVerdict, Pattern.CASE_INSENSITIVE);
+				if (pattern.matcher(actualResult.toString()) != null || pattern.matcher(overallResultMsg) != null) {
+					mTestResult = TestResult.IGNORE;
+				} else {
+					mTestResult = TestResult.FAIL;
+				}
+				mCategory = actualResult + " (Expected to match :" + mOverridenExpectedVerdict + ")";
+				mMessage = " UltimateResult: " + overallResultMsg;
+				return;
+			}
+
 			if (expectedResult == ChcOverallResult.UNKNOWN) {
 				mCategory = "expected result unknown";
 				mMessage = "expected: " + expectedResult + " actual: " + actualResult;

trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java

@@ -2,22 +2,22 @@
  * Copyright (C) 2017 Alexander Nutz ([email protected])
  * Copyright (C) 2014-2015 Daniel Dietsch ([email protected])
  * Copyright (C) 2015 University of Freiburg
- * 
+ *
  * This file is part of the ULTIMATE Regression Test Library.
- * 
+ *
  * The ULTIMATE Regression Test Library 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.
- * 
+ *
  * The ULTIMATE Regression Test Library 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 the ULTIMATE Regression Test Library. If not, see <http://www.gnu.org/licenses/>.
- * 
+ *
  * Additional permission under GNU GPL version 3 section 7:
  * If you modify the ULTIMATE Regression Test Library, or any covered work, by linking
  * or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
@@ -29,22 +29,23 @@
 
 import de.uni_freiburg.informatik.ultimate.regressiontest.AbstractRegressionTestSuite;
 import de.uni_freiburg.informatik.ultimate.test.UltimateRunDefinition;
-import de.uni_freiburg.informatik.ultimate.test.decider.ITestResultDecider;
 import de.uni_freiburg.informatik.ultimate.test.decider.ChcTestResultDecider;
+import de.uni_freiburg.informatik.ultimate.test.decider.ITestResultDecider;
 import de.uni_freiburg.informatik.ultimate.test.util.TestUtil;
 
 /**
- * 
+ *
  * This test suite automatically generates test cases from the example folder. If you place input files, toolchains and
  * settings files in a folder named regression, they will automatically be picked up.
- * 
+ *
  * @author Alexander Nutz ([email protected])
  * @author [email protected]
- * 
+ *
  */
 public class ChcRegressionTestSuite extends AbstractRegressionTestSuite {
 
 	private static final long DEFAULT_TIMEOUT = 20 * 1000L;
+	private static final boolean UNKNOWN_IS_SUCCESS = false;
 
 	public ChcRegressionTestSuite() {
 		super();
@@ -58,7 +59,12 @@ public ChcRegressionTestSuite() {
 
 	@Override
 	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) {
-		final boolean unknownIsSuccess = false;
-		return new ChcTestResultDecider(runDefinition, unknownIsSuccess);
+		return new ChcTestResultDecider(runDefinition, UNKNOWN_IS_SUCCESS);
+	}
+
+	@Override
+	protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition,
+			final String overriddenExpectedVerdict) {
+		return new ChcTestResultDecider(runDefinition, UNKNOWN_IS_SUCCESS, overriddenExpectedVerdict);
 	}
 }