From df1d31b86a61b4ff3d0c37c9ef23e7a0ecaa0984 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Fri, 27 Sep 2024 09:23:36 +0200 Subject: [PATCH] ignore unsupported CHC regression tests (#679) --- .../smtlib/horn/regression/.testignore | 8 ++++++ .../test/decider/ChcTestResultDecider.java | 25 +++++++++++++++-- .../generic/ChcRegressionTestSuite.java | 28 +++++++++++-------- 3 files changed, 47 insertions(+), 14 deletions(-) create mode 100644 trunk/examples/smtlib/horn/regression/.testignore diff --git a/trunk/examples/smtlib/horn/regression/.testignore b/trunk/examples/smtlib/horn/regression/.testignore new file mode 100644 index 00000000000..b7c64e4fdd4 --- /dev/null +++ b/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 diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ChcTestResultDecider.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ChcTestResultDecider.java index 1d58a4445fe..4571e2119cf 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ChcTestResultDecider.java +++ b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ChcTestResultDecider.java @@ -27,15 +27,22 @@ */ 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 { + 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); @@ -43,8 +50,7 @@ public ChcTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, @Override public SMTLibExpectedResultFinder 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 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; diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java index afee2f0b027..51a0816fddc 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java @@ -2,22 +2,22 @@ * Copyright (C) 2017 Alexander Nutz (nutz@informatik.uni-freiburg.de) * Copyright (C) 2014-2015 Daniel Dietsch (dietsch@informatik.uni-freiburg.de) * 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 . - * + * * 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 (nutz@informatik.uni-freiburg.de) * @author dietsch@informatik.uni-freiburg.de - * + * */ 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); } }