From 3bf75886c10b6788a25f0f37b8194b40c7c97aee Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Wed, 10 Dec 2025 14:04:03 +0100 Subject: [PATCH 01/13] Add some superposition test cases --- Inferences/Superposition.cpp | 10 +- Saturation/SaturationAlgorithm.cpp | 12 +-- Test/GenerationTester.hpp | 22 ++-- UnitTests/tSuperposition.cpp | 160 +++++++++++++++++++++++++++++ cmake/sources.cmake | 2 +- 5 files changed, 178 insertions(+), 28 deletions(-) create mode 100644 UnitTests/tSuperposition.cpp diff --git a/Inferences/Superposition.cpp b/Inferences/Superposition.cpp index f28cce904..5f9920283 100644 --- a/Inferences/Superposition.cpp +++ b/Inferences/Superposition.cpp @@ -171,7 +171,7 @@ bool Superposition::checkClauseColorCompatibility(Clause* eqClause, Clause* rwCl * * This function checks that we don't perform superpositions from * variables that occur in the remaining part of the clause either in - * a literal which is not an equality, or in a as an argument of a function. + * a literal which is not an equality, or as an argument of a function. * Such situation would mean that there is no ground substitution in which * @c eqLHS would be the larger argument of the largest literal. */ @@ -189,10 +189,10 @@ bool Superposition::checkSuperpositionFromVariable(Clause* eqClause, Literal* eq } if(lit->isEquality()) { for(unsigned aIdx=0; aIdx<2; aIdx++) { - TermList arg = *lit->nthArgument(aIdx); - if(arg.isTerm() && arg.containsSubterm(eqLHS)) { - return false; - } + TermList arg = *lit->nthArgument(aIdx); + if(arg.isTerm() && arg.containsSubterm(eqLHS)) { + return false; + } } } else if(lit->containsSubterm(eqLHS)) { diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp index 52b5242ea..8b5e39c1e 100644 --- a/Saturation/SaturationAlgorithm.cpp +++ b/Saturation/SaturationAlgorithm.cpp @@ -257,6 +257,12 @@ SaturationAlgorithm::SaturationAlgorithm(Problem& prb, const Options& opt) _extensionality = 0; } + if (opt.splitting()) { + _splitter = new Splitter(); + } + + _partialRedundancyHandler.reset(PartialRedundancyHandler::create(opt, _ordering.ptr(), _splitter)); + s_instance = this; } @@ -1437,10 +1443,6 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const NOT_IMPLEMENTED; } - if (opt.splitting()) { - res->_splitter = new Splitter(); - } - // create generating inference engine CompositeGIE *gie = new CompositeGIE(); @@ -1693,8 +1695,6 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const res->_symEl = new SymElOutput(); } - res->_partialRedundancyHandler.reset(PartialRedundancyHandler::create(opt, &ordering, res->_splitter)); - res->_answerLiteralManager = AnswerLiteralManager::getInstance(); // selects the right one, according to options! ASS(!res->_answerLiteralManager||opt.questionAnswering()!=Options::QuestionAnsweringMode::OFF); ASS( res->_answerLiteralManager||opt.questionAnswering()==Options::QuestionAnsweringMode::OFF); diff --git a/Test/GenerationTester.hpp b/Test/GenerationTester.hpp index 55a102ae8..3f31e0c3f 100644 --- a/Test/GenerationTester.hpp +++ b/Test/GenerationTester.hpp @@ -224,19 +224,17 @@ class GenerationTester friend class SymmetricTest; }; -using TestIndices = Stack>; +using OptionMap = Stack>; class AsymmetricTest { using Clause = Kernel::Clause; - using OptionMap = Stack>; using Condition = std::function; Option _rule; Clause* _input; Option _expected; Stack _context; bool _premiseRedundant; - TestIndices _indices; std::function _setup = [](SaturationAlgorithm&){}; bool _selfApplications; OptionMap _options; @@ -272,7 +270,6 @@ class AsymmetricTest __BUILDER_METHOD(bool, premiseRedundant) __BUILDER_METHOD(bool, selfApplications) __BUILDER_METHOD(SimplifyingGeneratingInference*, rule) - __BUILDER_METHOD(TestIndices, indices) __BUILDER_METHOD(std::function, setup) __BUILDER_METHOD(OptionMap, options) @@ -304,26 +301,19 @@ class AsymmetricTest _setup(alg); SimplifyingGeneratingInference& rule = *_rule.unwrapOrElse([&](){ return &simpl._rule; }); rule.attach(&alg); - Stack indices; - for (auto i : _indices) { - indices.push(i(*env.options)); - } auto container = alg.getActiveClauseContainer(); - for (auto i : indices) { - i->attachContainer(container); - } - // add the clauses to the index for (auto c : _context) { c->setStore(Clause::ACTIVE); container->add(c); } + _input->setStore(Clause::ACTIVE); + // run rule if (_selfApplications) { - _input->setStore(Clause::ACTIVE); container->add(_input); } @@ -363,7 +353,7 @@ class SymmetricTest Option _expected; bool _premiseRedundant; bool _selfApplications; - TestIndices _indices; + OptionMap _options; template void testFail(Is const& is, Expected const& expected) { @@ -390,7 +380,7 @@ class SymmetricTest __BUILDER_METHOD(bool, premiseRedundant) __BUILDER_METHOD(bool, selfApplications) __BUILDER_METHOD(SimplifyingGeneratingInference*, rule) - __BUILDER_METHOD(TestIndices, indices) + __BUILDER_METHOD(OptionMap, options) #undef __BUILDER_METHOD @@ -417,7 +407,7 @@ class SymmetricTest .premiseRedundant(_premiseRedundant) .selfApplications(_selfApplications) .rule(rule) - .indices(_indices) + .options(_options) .run(simpl); } }; diff --git a/UnitTests/tSuperposition.cpp b/UnitTests/tSuperposition.cpp new file mode 100644 index 000000000..3774b1e46 --- /dev/null +++ b/UnitTests/tSuperposition.cpp @@ -0,0 +1,160 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ + +#include "Test/UnitTesting.hpp" +#include "Test/SyntaxSugar.hpp" +#include "Test/GenerationTester.hpp" + +#include "Inferences/Superposition.hpp" + +using namespace Test; + +/** + * NECESSARY: We need to tell the tester which syntax sugar to import for creating terms & clauses. + * See Test/SyntaxSugar.hpp for which kinds of syntax sugar are available + */ +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_SORT(s) \ + DECL_FUNC(f, {s, s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_PRED (p, {s}) \ + DECL_PRED (q, {s}) \ + +REGISTER_GEN_TESTER(Generation::GenerationTester(Superposition())) + +// no superposition with negative equations +TEST_GENERATION(test_01, + Generation::SymmetricTest() + .inputs({ + clause({ selected(f(x,y) != x) }), + clause({ selected(f(x,y) != y) }) + }) + .expected(none()) + ) + +// self superposition with equation +TEST_GENERATION(test_02, + Generation::SymmetricTest() + .inputs({ clause({ selected(f(f(x,y),z) == x) }) }) + .expected({ clause({ f(x,y) == f(x,z) }) }) + ) + +// superposition from variable +TEST_GENERATION(test_03, + Generation::SymmetricTest() + .inputs({ + clause({ selected(x == a), p(y) }), + clause({ selected(f(x,y) == g(z)) }), + }) + .selfApplications(false) + .expected({ + clause({ a == g(x), p(y) }), + clause({ f(x,y) == a, p(z) }) + }) + ) + +// superposition from variable is not performed due to variable in predicate +TEST_GENERATION(test_04, + Generation::SymmetricTest() + .inputs({ + clause({ selected(x == a), p(x) }), + clause({ selected(f(x,y) == g(z)) }), + }) + .selfApplications(false) + .expected(none()) + ) + +// superposition from variable is not performed due to variable in function +TEST_GENERATION(test_05, + Generation::SymmetricTest() + .inputs({ + clause({ selected(x == a), g(x) == y }), + clause({ selected(f(x,y) == g(z)) }), + }) + .selfApplications(false) + .expected(none()) + ) + +// superposition is not performed when lhs < rhs +TEST_GENERATION(test_06, + Generation::SymmetricTest() + .inputs({ + clause({ selected(f(x,y) == f(y,x)), g(x) == y }), + clause({ selected(g(f(a,b)) != a) }), + }) + .selfApplications(false) + .expected(none()) + ) + +// superposition is not performed when lhs = rhs +TEST_GENERATION(test_07, + Generation::SymmetricTest() + .inputs({ + clause({ selected(f(x,y) == f(y,x)), g(x) == y }), + clause({ selected(g(f(a,a)) != a) }), + }) + .selfApplications(false) + .expected(none()) + ) + +// superposition is not performed when a tautology would be generated +TEST_GENERATION(test_08, + Generation::SymmetricTest() + .inputs({ + clause({ selected(f(x,y) == y), g(x) == y }), + clause({ selected(g(f(g(x),a)) == g(a)) }), + }) + .selfApplications(false) + .expected(none()) + ) + +// superposition is not performed when literal is not selected +TEST_GENERATION(test_09, + Generation::SymmetricTest() + .inputs({ + clause({ selected(f(x,y) == y), g(x) == y }), + clause({ selected(~p(x)), p(f(x,y)) }), + }) + .selfApplications(false) + .expected(none()) + ) + +// simultaneous superposition +TEST_GENERATION(test_10, + Generation::SymmetricTest() + .inputs({ + clause({ selected(f(x,y) == y), g(x) == y }), + clause({ selected(~p(f(x,y))), q(f(x,y)) }), + }) + .selfApplications(false) + .expected({ + clause({ ~p(y), q(y), g(x) == y }) + }) + ) + +// non-simultaneous superposition +TEST_GENERATION(test_11, + Generation::SymmetricTest() + .inputs({ + clause({ selected(f(x,y) == y), g(x) == y }), + clause({ selected(~p(f(x,y))), q(f(x,y)) }), + }) + .options({ { "simultaneous_superposition", "off" } }) + .selfApplications(false) + .expected({ + clause({ ~p(y), q(f(x,y)), g(x) == y }) + }) + ) + +// superposition only into bigger side of the equation +// superposition maximality aftercheck \ No newline at end of file diff --git a/cmake/sources.cmake b/cmake/sources.cmake index 5fb082254..8f7d1f806 100644 --- a/cmake/sources.cmake +++ b/cmake/sources.cmake @@ -63,7 +63,6 @@ set(UNIT_TESTS UnitTests/tInterpretedFunctions.cpp UnitTests/tIterator.cpp UnitTests/tKBO.cpp - UnitTests/tKBO.hpp UnitTests/tLPO.cpp UnitTests/tList.cpp UnitTests/tOption.cpp @@ -78,6 +77,7 @@ set(UNIT_TESTS UnitTests/tSet.cpp UnitTests/tSkipList.cpp UnitTests/tStack.cpp + UnitTests/tSuperposition.cpp UnitTests/tSyntaxSugar.cpp UnitTests/tTermAlgebra.cpp UnitTests/tTermIndex.cpp From e4788e8f8e21e2516f64116566c8d266cf234996 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Mon, 12 Jan 2026 16:13:24 +0100 Subject: [PATCH 02/13] remove GCDA files which slowed down subsequent coverage runs; add some BR tests --- Test/FwdBwdSimplificationTester.hpp | 40 ++---------- Test/GenerationTester.hpp | 8 +-- Test/MockedSaturationAlgorithm.hpp | 15 +++++ Test/SyntaxSugar.hpp | 8 --- UnitTests/tBinaryResolution.cpp | 54 ++++++++++++++++ UnitTests/tDemodulation.cpp | 68 ++++++++++++++++++++ UnitTests/tSuperposition.cpp | 96 +++++++++++++++++++++++++---- cmake/sources.cmake | 2 + 8 files changed, 229 insertions(+), 62 deletions(-) create mode 100644 UnitTests/tBinaryResolution.cpp create mode 100644 UnitTests/tDemodulation.cpp diff --git a/Test/FwdBwdSimplificationTester.hpp b/Test/FwdBwdSimplificationTester.hpp index 8dd5c82c5..d51ca7a18 100644 --- a/Test/FwdBwdSimplificationTester.hpp +++ b/Test/FwdBwdSimplificationTester.hpp @@ -28,28 +28,6 @@ namespace Test { - /** removes consecutive duplicates. instead of the operator== the given predicate is used */ - template - void dedup(Stack& self, Equal eq) -{ - if (self.size() == 0) return; - unsigned offs = 0; - for (unsigned i = 1; i < self.size(); i++) { - if (eq(self[offs], self[i])) { - /* skip */ - } else { - self[offs++ + 1] = std::move(self[i]); - } - } - self.pop(self.size() - (offs + 1)); - } - - /** removes consecutive duplicates */ - template - void dedup(Stack& self) - { dedup(self, [](auto const& l, auto const& r) { return l == r; }); } - - namespace FwdBwdSimplification { class TestCase; @@ -59,7 +37,6 @@ class FwdBwdSimplificationTester Rule _rule; public: - FwdBwdSimplificationTester(Rule rule) : _rule(std::move(rule)) { } @@ -74,8 +51,6 @@ class TestCase { using Clause = Kernel::Clause; - - void testFail(std::string const& test, Lib::Exception& e) { std::cout << std::endl; @@ -100,20 +75,19 @@ class TestCase } public: - BUILDER_METHOD(TestCase, Stack, simplifyWith) BUILDER_METHOD(TestCase, Stack, toSimplify ) BUILDER_METHOD(TestCase, Stack, expected) BUILDER_METHOD(TestCase, Stack, justifications) BUILDER_METHOD(TestCase, ForwardSimplificationEngine* , fwd) BUILDER_METHOD(TestCase, BackwardSimplificationEngine*, bwd) + BUILDER_METHOD(TestCase, OptionMap, options) void runFwd() { Problem p; - Options o; - o.resolveAwayAutoValues(p); - MockedSaturationAlgorithm alg(p, o); + resetAndFillEnvOptions(options(), p); + MockedSaturationAlgorithm alg(p, *env.options); // set up clause container and indexing structure auto container = alg.getSimplifyingClauseContainer(); @@ -149,7 +123,6 @@ class TestCase } justifications.sort(); justifications.dedup(); - // dedup(justifications); fwd.detach(); Ordering::unsetGlobalOrdering(); @@ -172,9 +145,8 @@ class TestCase void runBwd() { Problem p; - Options o; - o.resolveAwayAutoValues(p); - MockedSaturationAlgorithm alg(p, o); + resetAndFillEnvOptions(options(), p); + MockedSaturationAlgorithm alg(p, *env.options); // set up clause container and indexing structure auto container = alg.getSimplifyingClauseContainer(); @@ -188,7 +160,7 @@ class TestCase } // simplify using every clause in simplifyWith.unwrap() - Stack results; //= toSimplify().unwrap(); + ClauseStack results; //= toSimplify().unwrap(); auto simplifyWith = this->simplifyWith().unwrap(); for (auto cl : simplifyWith) { Inferences::BwSimplificationRecordIterator simpls; diff --git a/Test/GenerationTester.hpp b/Test/GenerationTester.hpp index 3f31e0c3f..1c39a25f0 100644 --- a/Test/GenerationTester.hpp +++ b/Test/GenerationTester.hpp @@ -290,13 +290,7 @@ class AsymmetricTest p.addUnits(ul); env.setMainProblem(&p); - delete env.options; - env.options = new Options; - for (const auto& kv : _options) { - env.options->set(kv.first, kv.second); - } - env.options->resolveAwayAutoValues0(); - env.options->resolveAwayAutoValues(p); + resetAndFillEnvOptions(Option(_options), p); MockedSaturationAlgorithm alg(p, *env.options); _setup(alg); SimplifyingGeneratingInference& rule = *_rule.unwrapOrElse([&](){ return &simpl._rule; }); diff --git a/Test/MockedSaturationAlgorithm.hpp b/Test/MockedSaturationAlgorithm.hpp index 5e9e0d7f1..0c19245cc 100644 --- a/Test/MockedSaturationAlgorithm.hpp +++ b/Test/MockedSaturationAlgorithm.hpp @@ -15,6 +15,21 @@ namespace Test { +using OptionMap = Stack>; + +inline void resetAndFillEnvOptions(const Option& opt, const Problem& prb) { + delete env.options; + env.options = new Options(); + // env.options->reset(); + if (opt.isSome()) { + for (const auto& kv : opt.unwrap()) { + env.options->set(kv.first, kv.second); + } + } + env.options->resolveAwayAutoValues0(); + env.options->resolveAwayAutoValues(prb); +} + class MockedSaturationAlgorithm : public Saturation::Otter { public: MockedSaturationAlgorithm(Kernel::Problem& p, Shell::Options& o) : Otter(p,o) diff --git a/Test/SyntaxSugar.hpp b/Test/SyntaxSugar.hpp index d1346f2ae..521acff6d 100644 --- a/Test/SyntaxSugar.hpp +++ b/Test/SyntaxSugar.hpp @@ -710,14 +710,6 @@ inline Clause* clause(Stack ls) inline Clause* clause(std::initializer_list ls) { return clause(Stack(ls)); } -inline Stack clauses(std::initializer_list> cls) { - auto out = Stack(); - for (auto cl : cls) { - out.push(clause(cl)); - } - return out; -} - inline void createTermAlgebra(SortSugar sort, std::initializer_list fs) { // avoid redeclaration if (env.signature->isTermAlgebraSort(sort.sugaredExpr())) { diff --git a/UnitTests/tBinaryResolution.cpp b/UnitTests/tBinaryResolution.cpp new file mode 100644 index 000000000..8004e0d1a --- /dev/null +++ b/UnitTests/tBinaryResolution.cpp @@ -0,0 +1,54 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ + +#include "Test/UnitTesting.hpp" +#include "Test/SyntaxSugar.hpp" +#include "Test/GenerationTester.hpp" + +#include "Inferences/BinaryResolution.hpp" + +using namespace Test; + +/** + * NECESSARY: We need to tell the tester which syntax sugar to import for creating terms & clauses. + * See Test/SyntaxSugar.hpp for which kinds of syntax sugar are available + */ +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_VAR(u, 3) \ + DECL_SORT(s) \ + DECL_FUNC(f, {s, s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_PRED (p, {s}) \ + DECL_PRED (q, {s}) \ + +REGISTER_GEN_TESTER(Generation::GenerationTester(BinaryResolution())) + +// binary resolution with selected literals +TEST_GENERATION(test_01, + Generation::SymmetricTest() + .inputs({ + clause({ selected(p(x)), f(x,y) == x }), + clause({ selected(~p(g(x))), ~q(x) }) + }) + .expected(exactly(clause({ f(g(x),y) == g(x), ~q(x) }))) + ) + +// no binary resolution with equalities +TEST_GENERATION(test_02, + Generation::SymmetricTest() + .inputs({ + clause({ selected(g(x) == x), f(x,y) == x }), + clause({ selected(g(x) != x), ~q(x) }) + }) + .expected(none()) + ) diff --git a/UnitTests/tDemodulation.cpp b/UnitTests/tDemodulation.cpp new file mode 100644 index 000000000..cf76a1c59 --- /dev/null +++ b/UnitTests/tDemodulation.cpp @@ -0,0 +1,68 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ + +#include "Test/SyntaxSugar.hpp" +#include "Inferences/ForwardDemodulation.hpp" +#include "Inferences/BackwardDemodulation.hpp" + +#include "Test/UnitTesting.hpp" +#include "Test/FwdBwdSimplificationTester.hpp" + +using namespace std; +using namespace Kernel; +using namespace Inferences; +using namespace Test; + +/** + * NECESSARY: We need to tell the tester which syntax sugar to import for creating terms & clauses. + * See Test/SyntaxSugar.hpp for which kinds of syntax sugar are available + */ +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_VAR(u, 3) \ + DECL_SORT(s) \ + DECL_FUNC(f, {s, s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_PRED (p, {s}) \ + DECL_PRED (q, {s}) \ + +inline auto tester() { + return FwdBwdSimplification::TestCase() + .fwd(new ForwardDemodulation()) + .bwd(new BackwardDemodulation()) + .options({ { "term_ordering", "lpo" }}); // use LPO as KBO fails due to caching things in terms +} + +// demodulation with preordered equation +TEST_SIMPLIFICATION(test01, + tester() + .simplifyWith({ clause({ f(x,y) == x }) }) + .toSimplify({ clause({ ~p(f(a,b)) }) }) + .expected({ clause({ ~p(a) }) }) +) + +// demodulation with postordered equation +TEST_SIMPLIFICATION(test02, + tester() + .simplifyWith({ clause({ f(x,y) == f(y,x) }) }) + .toSimplify({ clause({ ~p(f(b,a)) }) }) + .expected({ clause({ ~p(f(a,b)) }) }) +) + +// TODO find out why this fails +// // demodulation fails with postordered equation +// TEST_SIMPLIFICATION(test03, +// tester() +// .simplifyWith({ clause({ f(x,y) == f(y,x) }) }) +// .toSimplify({ clause({ ~p(f(a,b)) }) }) +// .expected({ /*nothing*/ }) +// ) diff --git a/UnitTests/tSuperposition.cpp b/UnitTests/tSuperposition.cpp index 3774b1e46..47b4a2e0e 100644 --- a/UnitTests/tSuperposition.cpp +++ b/UnitTests/tSuperposition.cpp @@ -22,6 +22,7 @@ using namespace Test; */ #define MY_SYNTAX_SUGAR \ DECL_DEFAULT_VARS \ + DECL_VAR(u, 3) \ DECL_SORT(s) \ DECL_FUNC(f, {s, s}, s) \ DECL_FUNC(g, {s}, s) \ @@ -46,21 +47,21 @@ TEST_GENERATION(test_01, TEST_GENERATION(test_02, Generation::SymmetricTest() .inputs({ clause({ selected(f(f(x,y),z) == x) }) }) - .expected({ clause({ f(x,y) == f(x,z) }) }) + .expected(exactly(clause({ f(x,y) == f(x,z) }))) ) // superposition from variable TEST_GENERATION(test_03, Generation::SymmetricTest() .inputs({ - clause({ selected(x == a), p(y) }), + clause({ selected(x == a), p(y), f(y,z) == g(z) }), clause({ selected(f(x,y) == g(z)) }), }) .selfApplications(false) - .expected({ - clause({ a == g(x), p(y) }), - clause({ f(x,y) == a, p(z) }) - }) + .expected(exactly( + clause({ a == g(x), p(y), f(y,z) == g(z) }), + clause({ f(x,y) == a, p(z), f(z,u) == g(u) }) + )) ) // superposition from variable is not performed due to variable in predicate @@ -137,9 +138,7 @@ TEST_GENERATION(test_10, clause({ selected(~p(f(x,y))), q(f(x,y)) }), }) .selfApplications(false) - .expected({ - clause({ ~p(y), q(y), g(x) == y }) - }) + .expected(exactly(clause({ ~p(y), q(y), g(x) == y }))) ) // non-simultaneous superposition @@ -151,10 +150,81 @@ TEST_GENERATION(test_11, }) .options({ { "simultaneous_superposition", "off" } }) .selfApplications(false) - .expected({ - clause({ ~p(y), q(f(x,y)), g(x) == y }) + .expected(exactly(clause({ ~p(y), q(f(x,y)), g(x) == y }))) + ) + +// superposition not performed due to trivial equality in superposed-from clause +TEST_GENERATION(test_12, + Generation::SymmetricTest() + .inputs({ + clause({ selected(g(x) == x), x == a }), + clause({ selected(~p(g(a))) }), }) + .selfApplications(false) + .expected(none()) + ) + +// superposition not performed due to trivial equality in superposed-into clause +TEST_GENERATION(test_13, + Generation::SymmetricTest() + .inputs({ + clause({ selected(g(a) == a) }), + clause({ selected(~p(g(x))), x == a }), + }) + .selfApplications(false) + .expected(none()) + ) + +// superposition performed despite maximality aftercheck in superposed-into clause +TEST_GENERATION(test_14, + Generation::SymmetricTest() + .inputs({ + clause({ selected(f(b,a) == g(a)) }), + clause({ selected(f(x,y) != x), selected(f(y,x) != y) }), + }) + .selfApplications(false) + .expected(exactly( + clause({ g(a) != b, f(b,a) != a }), + clause({ g(a) != b, f(b,a) != a }) + )) + ) + +// superposition not performed due to maximality aftercheck in superposed-into clause +TEST_GENERATION(test_15, + Generation::SymmetricTest() + .inputs({ + clause({ selected(f(a,b) == g(a)) }), + clause({ selected(f(x,y) != x), selected(f(y,x) != y) }), + }) + .selfApplications(false) + .expected(none()) + ) + +// superposition performed despite maximality aftercheck in superposed-from clause +TEST_GENERATION(test_16, + Generation::SymmetricTest() + .inputs({ + clause({ selected(f(x,y) == x), selected(f(y,x) == y) }), + clause({ selected(~p(f(b,a))) }), + }) + .selfApplications(false) + .expected(exactly( + clause({ ~p(b), f(a,b) == a }), + clause({ ~p(b), f(a,b) == a }) + )) + ) + +// superposition not performed due to maximality aftercheck in superposed-from clause +TEST_GENERATION(test_17, + Generation::SymmetricTest() + .inputs({ + clause({ selected(f(x,y) == x), selected(f(y,x) == y) }), + clause({ selected(~p(f(a,b))) }), + }) + .selfApplications(false) + .expected(none()) ) -// superposition only into bigger side of the equation -// superposition maximality aftercheck \ No newline at end of file +// TODO +// superposition with colors +// superposition only into bigger side of the equation \ No newline at end of file diff --git a/cmake/sources.cmake b/cmake/sources.cmake index 8f7d1f806..622861fb2 100644 --- a/cmake/sources.cmake +++ b/cmake/sources.cmake @@ -45,10 +45,12 @@ set(UNIT_TESTS UnitTests/tArithCompare.cpp UnitTests/tArithmeticSubtermGeneralization.cpp UnitTests/tBinaryHeap.cpp + UnitTests/tBinaryResolution.cpp UnitTests/tBottomUpEvaluation.cpp UnitTests/tCoproduct.cpp UnitTests/tDHMap.cpp UnitTests/tDHMultiset.cpp + UnitTests/tDemodulation.cpp UnitTests/tDeque.cpp UnitTests/tDisagreement.cpp UnitTests/tDynamicHeap.cpp From 35b8d010dd1d9cadb3c1d8eb7a2699e69c5643d4 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Tue, 13 Jan 2026 10:45:45 +0100 Subject: [PATCH 03/13] Have common prefix for inference tests (except ALASCA inferences); add duplicate literal removal test --- Inferences/InferenceEngine.hpp | 11 ------ Test/SimplificationTester.hpp | 25 +++++++------- UnitTests/tALASCA_TautologyDeletion.cpp | 15 ++------ ...ences_ArithmeticSubtermGeneralization.cpp} | 0 ...n.cpp => tInferences_BinaryResolution.cpp} | 0 ...ation.cpp => tInferences_Demodulation.cpp} | 0 ...cpp => tInferences_EqualityResolution.cpp} | 0 ... tInferences_ForwardGroundJoinability.cpp} | 0 ...nferences_FunctionDefinitionRewriting.cpp} | 0 ...nferences_GaussianVariableElimination.cpp} | 9 ----- ...nduction.cpp => tInferences_Induction.cpp} | 0 UnitTests/tInferences_InferenceEngine.cpp | 34 +++++++++++++++++++ ...nus.cpp => tInferences_PushUnaryMinus.cpp} | 19 +---------- ...tion.cpp => tInferences_Superposition.cpp} | 0 ....cpp => tInferences_TheoryInstAndSimp.cpp} | 0 cmake/sources.cmake | 23 +++++++------ 16 files changed, 62 insertions(+), 74 deletions(-) rename UnitTests/{tArithmeticSubtermGeneralization.cpp => tInferences_ArithmeticSubtermGeneralization.cpp} (100%) rename UnitTests/{tBinaryResolution.cpp => tInferences_BinaryResolution.cpp} (100%) rename UnitTests/{tDemodulation.cpp => tInferences_Demodulation.cpp} (100%) rename UnitTests/{tEqualityResolution.cpp => tInferences_EqualityResolution.cpp} (100%) rename UnitTests/{tForwardGroundJoinability.cpp => tInferences_ForwardGroundJoinability.cpp} (100%) rename UnitTests/{tFunctionDefinitionRewriting.cpp => tInferences_FunctionDefinitionRewriting.cpp} (100%) rename UnitTests/{tGaussianElimination.cpp => tInferences_GaussianVariableElimination.cpp} (96%) rename UnitTests/{tInduction.cpp => tInferences_Induction.cpp} (100%) create mode 100644 UnitTests/tInferences_InferenceEngine.cpp rename UnitTests/{tPushUnaryMinus.cpp => tInferences_PushUnaryMinus.cpp} (89%) rename UnitTests/{tSuperposition.cpp => tInferences_Superposition.cpp} (100%) rename UnitTests/{tTheoryInstAndSimp.cpp => tInferences_TheoryInstAndSimp.cpp} (100%) diff --git a/Inferences/InferenceEngine.hpp b/Inferences/InferenceEngine.hpp index b5f1cece3..0f2f9038f 100644 --- a/Inferences/InferenceEngine.hpp +++ b/Inferences/InferenceEngine.hpp @@ -275,17 +275,6 @@ class BackwardSimplificationEngine virtual void perform(Clause* premise, BwSimplificationRecordIterator& simplifications) = 0; }; - -class DummyGIE -: public GeneratingInferenceEngine -{ -public: - ClauseIterator generateClauses(Clause* premise) override - { - return ClauseIterator::getEmpty(); - } -}; - template class TupleISE : public ImmediateSimplificationEngine diff --git a/Test/SimplificationTester.hpp b/Test/SimplificationTester.hpp index a0431d743..b2b46b671 100644 --- a/Test/SimplificationTester.hpp +++ b/Test/SimplificationTester.hpp @@ -36,17 +36,25 @@ class SimplificationTester { return TestUtils::eqModAC(lhs, rhs); } }; +template +class RuleSimplificationTester + : public SimplificationTester +{ + T _rule; +public: + Kernel::Clause* simplify(Kernel::Clause* cl) override + { return _rule.simplify(cl); } +}; + class Redundant { }; // TODO use builder pattern macros from GenerationTester here class Success { - Kernel::Clause* _input; + Kernel::Clause* _input = nullptr; Option> _expected; public: - Success() : _input(nullptr) {} - Success input(Kernel::Clause* x) { _input = x; @@ -101,18 +109,15 @@ class NotApplicable { Kernel::Clause* _input; public: - NotApplicable() {} - NotApplicable input(Kernel::Clause* x) { _input = x; return *this; } - void run(SimplificationTester& simpl) { auto res = simpl.simplify(_input); - if (res != _input ) { + if (res != _input) { std::cout << std::endl; std::cout << "[ case ]: " << pretty(*_input) << std::endl; std::cout << "[ is ]: " << pretty(*res) << std::endl; @@ -137,8 +142,6 @@ class NotApplicableMany { Kernel::Clause* _input; public: - NotApplicableMany() {} - NotApplicableMany input(Kernel::Clause* x) { _input = x; @@ -161,12 +164,10 @@ class NotApplicableMany class SuccessMany { - Kernel::Clause* _input; + Kernel::Clause* _input = nullptr; Option _expected; public: - SuccessMany() : _input(nullptr) {} - SuccessMany input(Kernel::Clause* x) { _input = x; diff --git a/UnitTests/tALASCA_TautologyDeletion.cpp b/UnitTests/tALASCA_TautologyDeletion.cpp index 30b816b89..94c93bae2 100644 --- a/UnitTests/tALASCA_TautologyDeletion.cpp +++ b/UnitTests/tALASCA_TautologyDeletion.cpp @@ -9,15 +9,10 @@ */ #include "Inferences/ALASCA/Normalization.hpp" #include "Inferences/ALASCA/TautologyDeletion.hpp" -#include "Inferences/InferenceEngine.hpp" -#include "Kernel/ALASCA/State.hpp" #include "Test/UnitTesting.hpp" -#include "Test/TestUtils.hpp" #include "Test/SyntaxSugar.hpp" -#include "Inferences/GaussianVariableElimination.hpp" +#include "Inferences/LfpRule.hpp" -#include "Test/SyntaxSugar.hpp" -#include "Test/TestUtils.hpp" #include "Test/SimplificationTester.hpp" using namespace std; @@ -29,7 +24,6 @@ using namespace Test; ////// TEST UNIT INITIALIZATION ///////////////////////////////////// - /** * NECESSARY: We need a subclass of SimplificationTester */ @@ -44,13 +38,8 @@ class AlascaSimplTester : public Test::Simplification::SimplificationTester , _rule(lfpISE(tupleISE(ALASCA::Normalization(_state), Rule(_state)))) { } - virtual Kernel::Clause* simplify(Kernel::Clause* in) override + Kernel::Clause* simplify(Kernel::Clause* in) override { return _rule.simplify(in); } - - virtual bool eq(Kernel::Clause* lhs, Kernel::Clause* rhs) const override - { - return TestUtils::eqModAC(lhs, rhs); - } }; REGISTER_SIMPL_TESTER(AlascaSimplTester) diff --git a/UnitTests/tArithmeticSubtermGeneralization.cpp b/UnitTests/tInferences_ArithmeticSubtermGeneralization.cpp similarity index 100% rename from UnitTests/tArithmeticSubtermGeneralization.cpp rename to UnitTests/tInferences_ArithmeticSubtermGeneralization.cpp diff --git a/UnitTests/tBinaryResolution.cpp b/UnitTests/tInferences_BinaryResolution.cpp similarity index 100% rename from UnitTests/tBinaryResolution.cpp rename to UnitTests/tInferences_BinaryResolution.cpp diff --git a/UnitTests/tDemodulation.cpp b/UnitTests/tInferences_Demodulation.cpp similarity index 100% rename from UnitTests/tDemodulation.cpp rename to UnitTests/tInferences_Demodulation.cpp diff --git a/UnitTests/tEqualityResolution.cpp b/UnitTests/tInferences_EqualityResolution.cpp similarity index 100% rename from UnitTests/tEqualityResolution.cpp rename to UnitTests/tInferences_EqualityResolution.cpp diff --git a/UnitTests/tForwardGroundJoinability.cpp b/UnitTests/tInferences_ForwardGroundJoinability.cpp similarity index 100% rename from UnitTests/tForwardGroundJoinability.cpp rename to UnitTests/tInferences_ForwardGroundJoinability.cpp diff --git a/UnitTests/tFunctionDefinitionRewriting.cpp b/UnitTests/tInferences_FunctionDefinitionRewriting.cpp similarity index 100% rename from UnitTests/tFunctionDefinitionRewriting.cpp rename to UnitTests/tInferences_FunctionDefinitionRewriting.cpp diff --git a/UnitTests/tGaussianElimination.cpp b/UnitTests/tInferences_GaussianVariableElimination.cpp similarity index 96% rename from UnitTests/tGaussianElimination.cpp rename to UnitTests/tInferences_GaussianVariableElimination.cpp index 2dc8fce2c..3d9f9a63f 100644 --- a/UnitTests/tGaussianElimination.cpp +++ b/UnitTests/tInferences_GaussianVariableElimination.cpp @@ -60,15 +60,6 @@ class GveSimplTester : public Test::Simplification::SimplificationTester } while (latest != last); return latest; } - - /** - * OPTIONAL: override how equality between clauses is checked. - * Defaults to TestUtils::eqModAC(Clause*, Clause*). - */ - virtual bool eq(Kernel::Clause* lhs, Kernel::Clause* rhs) const override - { - return TestUtils::eqModAC(lhs, rhs); - } }; /** diff --git a/UnitTests/tInduction.cpp b/UnitTests/tInferences_Induction.cpp similarity index 100% rename from UnitTests/tInduction.cpp rename to UnitTests/tInferences_Induction.cpp diff --git a/UnitTests/tInferences_InferenceEngine.cpp b/UnitTests/tInferences_InferenceEngine.cpp new file mode 100644 index 000000000..c7d235343 --- /dev/null +++ b/UnitTests/tInferences_InferenceEngine.cpp @@ -0,0 +1,34 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ +#include "Test/UnitTesting.hpp" +#include "Test/SyntaxSugar.hpp" +#include "Inferences/InferenceEngine.hpp" + +#include "Test/SimplificationTester.hpp" + +using namespace Test; + +REGISTER_SIMPL_TESTER(Simplification::RuleSimplificationTester) + +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_SORT(s) \ + DECL_FUNC(f, {s, s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_PRED (p, {s}) \ + DECL_PRED (q, {s}) \ + +TEST_SIMPLIFY(test01, + Simplification::Success() + .input(clause({ p(a), p(a) })) + .expected(clause({ p(a) })) + ) diff --git a/UnitTests/tPushUnaryMinus.cpp b/UnitTests/tInferences_PushUnaryMinus.cpp similarity index 89% rename from UnitTests/tPushUnaryMinus.cpp rename to UnitTests/tInferences_PushUnaryMinus.cpp index 69a74ddf7..37571a13d 100644 --- a/UnitTests/tPushUnaryMinus.cpp +++ b/UnitTests/tInferences_PushUnaryMinus.cpp @@ -24,24 +24,7 @@ using namespace Test; ////// TEST UNIT INITIALIZATION ///////////////////////////////////// -/** - * NECESSARY: We need a subclass of SimplificationTester - */ -class PumSimplTester : public Test::Simplification::SimplificationTester -{ -public: - - virtual Kernel::Clause* simplify(Kernel::Clause* in) override - { - PushUnaryMinus pum; - return pum.simplify(in); - } - - virtual bool eq(Kernel::Clause* lhs, Kernel::Clause* rhs) const override - { return TestUtils::eqModAC(lhs, rhs); } -}; - -REGISTER_SIMPL_TESTER(PumSimplTester) +REGISTER_SIMPL_TESTER(Simplification::RuleSimplificationTester) #define MY_SYNTAX_SUGAR \ NUMBER_SUGAR(Real) \ diff --git a/UnitTests/tSuperposition.cpp b/UnitTests/tInferences_Superposition.cpp similarity index 100% rename from UnitTests/tSuperposition.cpp rename to UnitTests/tInferences_Superposition.cpp diff --git a/UnitTests/tTheoryInstAndSimp.cpp b/UnitTests/tInferences_TheoryInstAndSimp.cpp similarity index 100% rename from UnitTests/tTheoryInstAndSimp.cpp rename to UnitTests/tInferences_TheoryInstAndSimp.cpp diff --git a/cmake/sources.cmake b/cmake/sources.cmake index 622861fb2..2f90d66b5 100644 --- a/cmake/sources.cmake +++ b/cmake/sources.cmake @@ -43,24 +43,27 @@ set(UNIT_TESTS UnitTests/tALASCA_VariableElimination.cpp UnitTests/tAnswerLiteralProcessors_Synthesis.cpp UnitTests/tArithCompare.cpp - UnitTests/tArithmeticSubtermGeneralization.cpp UnitTests/tBinaryHeap.cpp - UnitTests/tBinaryResolution.cpp UnitTests/tBottomUpEvaluation.cpp UnitTests/tCoproduct.cpp UnitTests/tDHMap.cpp UnitTests/tDHMultiset.cpp - UnitTests/tDemodulation.cpp UnitTests/tDeque.cpp UnitTests/tDisagreement.cpp UnitTests/tDynamicHeap.cpp - UnitTests/tEqualityResolution.cpp - UnitTests/tForwardGroundJoinability.cpp UnitTests/tFunctionDefinitionHandler.cpp - UnitTests/tFunctionDefinitionRewriting.cpp - UnitTests/tGaussianElimination.cpp UnitTests/tIndexManager.cpp - UnitTests/tInduction.cpp + UnitTests/tInferences_ArithmeticSubtermGeneralization.cpp + UnitTests/tInferences_BinaryResolution.cpp + UnitTests/tInferences_Demodulation.cpp + UnitTests/tInferences_EqualityResolution.cpp + UnitTests/tInferences_ForwardGroundJoinability.cpp + UnitTests/tInferences_FunctionDefinitionRewriting.cpp + UnitTests/tInferences_GaussianVariableElimination.cpp + UnitTests/tInferences_Induction.cpp + UnitTests/tInferences_InferenceEngine.cpp + UnitTests/tInferences_PushUnaryMinus.cpp + UnitTests/tInferences_Superposition.cpp UnitTests/tIntegerConstantType.cpp UnitTests/tInterpretedFunctions.cpp UnitTests/tIterator.cpp @@ -69,7 +72,6 @@ set(UNIT_TESTS UnitTests/tList.cpp UnitTests/tOption.cpp UnitTests/tOptionConstraints.cpp - UnitTests/tPushUnaryMinus.cpp UnitTests/tQKbo.cpp UnitTests/tQuotientE.cpp UnitTests/tRebalance.cpp @@ -79,7 +81,6 @@ set(UNIT_TESTS UnitTests/tSet.cpp UnitTests/tSkipList.cpp UnitTests/tStack.cpp - UnitTests/tSuperposition.cpp UnitTests/tSyntaxSugar.cpp UnitTests/tTermAlgebra.cpp UnitTests/tTermIndex.cpp @@ -96,7 +97,7 @@ set(UNIT_TESTS # unit tests (only if Z3 enabled) ################################################################ set(UNIT_TESTS_Z3 - UnitTests/tTheoryInstAndSimp.cpp + UnitTests/tInferences_TheoryInstAndSimp.cpp UnitTests/tZ3Interfacing.cpp ) From 53ab56f56fe6175caa48b5ad2bc22bacabce1fbf Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Tue, 13 Jan 2026 15:05:11 +0100 Subject: [PATCH 04/13] Add some tests for immediate simplifications add demodulation tests; remove unused include add more demodulation tests; add factoring tests Add demodulation/superposition tests with colored symbols --- Test/FwdBwdSimplificationTester.hpp | 15 +- Test/GenerationTester.hpp | 2 +- Test/SyntaxSugar.hpp | 8 +- UnitTests/tALASCA_TautologyDeletion.cpp | 1 - .../tAnswerLiteralProcessors_Synthesis.cpp | 1 - UnitTests/tInferences_BinaryResolution.cpp | 1 - UnitTests/tInferences_Demodulation.cpp | 133 ++++++++++++++++-- UnitTests/tInferences_EqualityResolution.cpp | 1 - UnitTests/tInferences_Factoring.cpp | 91 ++++++++++++ ...Inferences_FunctionDefinitionRewriting.cpp | 1 - ...Inferences_GaussianVariableElimination.cpp | 3 - UnitTests/tInferences_InferenceEngine.cpp | 75 +++++++++- UnitTests/tInferences_PushUnaryMinus.cpp | 7 +- UnitTests/tInferences_Superposition.cpp | 41 +++++- .../tInferences_TautologyDeletionISE.cpp | 57 ++++++++ UnitTests/tInferences_TheoryInstAndSimp.cpp | 2 - UnitTests/tIntegerConstantType.cpp | 1 - cmake/sources.cmake | 2 + 18 files changed, 397 insertions(+), 45 deletions(-) create mode 100644 UnitTests/tInferences_Factoring.cpp create mode 100644 UnitTests/tInferences_TautologyDeletionISE.cpp diff --git a/Test/FwdBwdSimplificationTester.hpp b/Test/FwdBwdSimplificationTester.hpp index d51ca7a18..93b429366 100644 --- a/Test/FwdBwdSimplificationTester.hpp +++ b/Test/FwdBwdSimplificationTester.hpp @@ -19,12 +19,13 @@ * Don't rely on any part of the interface, but the things contained in the examples, * because it's rather unstable. */ +#include "TestUtils.hpp" +#include "ClausePattern.hpp" +#include "MockedSaturationAlgorithm.hpp" +#include "BuilderPattern.hpp" +#include "UnitTesting.hpp" -#include "Test/TestUtils.hpp" #include "Kernel/Clause.hpp" -#include "Test/ClausePattern.hpp" -#include "Test/MockedSaturationAlgorithm.hpp" -#include "Test/BuilderPattern.hpp" namespace Test { @@ -114,7 +115,7 @@ class TestCase testFail("fwd", e); } - if (succ ) { + if (succ) { if (replacement) { results.push(replacement); } @@ -170,7 +171,9 @@ class TestCase testFail("bwd", e); } for (auto simpl : iterTraits(std::move(simpls))) { - results.push(simpl.replacement); + if (simpl.replacement) { + results.push(simpl.replacement); + } } } bwd.detach(); diff --git a/Test/GenerationTester.hpp b/Test/GenerationTester.hpp index 1c39a25f0..eb1072c35 100644 --- a/Test/GenerationTester.hpp +++ b/Test/GenerationTester.hpp @@ -26,7 +26,7 @@ #include "Lib/Coproduct.hpp" #include "Test/ClausePattern.hpp" #include "Kernel/Problem.hpp" -#include "Shell/Options.hpp" +#include "UnitTesting.hpp" #include "Lib/STL.hpp" #include "Test/MockedSaturationAlgorithm.hpp" diff --git a/Test/SyntaxSugar.hpp b/Test/SyntaxSugar.hpp index 521acff6d..048adf030 100644 --- a/Test/SyntaxSugar.hpp +++ b/Test/SyntaxSugar.hpp @@ -67,6 +67,8 @@ #define DECL_CONST(f, sort) auto f = ConstSugar(#f, sort); #define DECL_SKOLEM_CONST(f, sort) auto f = ConstSugar(#f, sort, true); #define DECL_FUNC(f, ...) auto f = FuncSugar(#f, __VA_ARGS__); +#define DECL_LEFT_FUNC(f, ...) auto f = FuncSugar(#f, __VA_ARGS__, /*taArity=*/0, /*skolem=*/false, Color::COLOR_LEFT); +#define DECL_RIGHT_FUNC(f, ...) auto f = FuncSugar(#f, __VA_ARGS__, /*taArity=*/0, /*skolem=*/false, Color::COLOR_RIGHT); #define DECL_SKOLEM_FUNC(f, ...) auto f = FuncSugar(#f, __VA_ARGS__, /*taArity=*/0, true); #define DECL_POLY_FUNC(f, i, ...) auto f = FuncSugar(#f, __VA_ARGS__, i); #define DECL_POLY_CONST(f, i, sort) auto f = FuncSugar(#f, {}, sort, i); @@ -555,7 +557,7 @@ class FuncSugar { , _arity(env.signature->getFunction(functor)->arity()) {} FuncSugar(std::string const& name, std::initializer_list as_, - ExpressionSugar result, unsigned taArity = 0, bool skolem = false) + ExpressionSugar result, unsigned taArity = 0, bool skolem = false, Color c = COLOR_TRANSPARENT) { Stack as; for (auto a : as_) @@ -579,6 +581,10 @@ class FuncSugar { if (skolem) { env.signature->getFunction(_functor)->markSkolem(); } + if (c != COLOR_TRANSPARENT) { + env.colorUsed = true; + env.signature->getFunction(_functor)->addColor(c); + } } } diff --git a/UnitTests/tALASCA_TautologyDeletion.cpp b/UnitTests/tALASCA_TautologyDeletion.cpp index 94c93bae2..fd3b3e1dd 100644 --- a/UnitTests/tALASCA_TautologyDeletion.cpp +++ b/UnitTests/tALASCA_TautologyDeletion.cpp @@ -9,7 +9,6 @@ */ #include "Inferences/ALASCA/Normalization.hpp" #include "Inferences/ALASCA/TautologyDeletion.hpp" -#include "Test/UnitTesting.hpp" #include "Test/SyntaxSugar.hpp" #include "Inferences/LfpRule.hpp" diff --git a/UnitTests/tAnswerLiteralProcessors_Synthesis.cpp b/UnitTests/tAnswerLiteralProcessors_Synthesis.cpp index 74ec2c069..5c18cead9 100644 --- a/UnitTests/tAnswerLiteralProcessors_Synthesis.cpp +++ b/UnitTests/tAnswerLiteralProcessors_Synthesis.cpp @@ -11,7 +11,6 @@ #include "Inferences/ProofExtra.hpp" #include "Kernel/Inference.hpp" #include "Shell/AnswerLiteralManager.hpp" -#include "Test/UnitTesting.hpp" #include "Test/SyntaxSugar.hpp" #include "Test/SimplificationTester.hpp" diff --git a/UnitTests/tInferences_BinaryResolution.cpp b/UnitTests/tInferences_BinaryResolution.cpp index 8004e0d1a..cde45898b 100644 --- a/UnitTests/tInferences_BinaryResolution.cpp +++ b/UnitTests/tInferences_BinaryResolution.cpp @@ -8,7 +8,6 @@ * and in the source directory */ -#include "Test/UnitTesting.hpp" #include "Test/SyntaxSugar.hpp" #include "Test/GenerationTester.hpp" diff --git a/UnitTests/tInferences_Demodulation.cpp b/UnitTests/tInferences_Demodulation.cpp index cf76a1c59..979b8729a 100644 --- a/UnitTests/tInferences_Demodulation.cpp +++ b/UnitTests/tInferences_Demodulation.cpp @@ -12,7 +12,6 @@ #include "Inferences/ForwardDemodulation.hpp" #include "Inferences/BackwardDemodulation.hpp" -#include "Test/UnitTesting.hpp" #include "Test/FwdBwdSimplificationTester.hpp" using namespace std; @@ -28,18 +27,20 @@ using namespace Test; DECL_DEFAULT_VARS \ DECL_VAR(u, 3) \ DECL_SORT(s) \ + DECL_LEFT_FUNC(left, {s}, s) \ + DECL_RIGHT_FUNC(right, {s}, s) \ DECL_FUNC(f, {s, s}, s) \ DECL_FUNC(g, {s}, s) \ DECL_CONST(a, s) \ DECL_CONST(b, s) \ DECL_PRED (p, {s}) \ - DECL_PRED (q, {s}) \ + DECL_PRED (q, {s}) inline auto tester() { return FwdBwdSimplification::TestCase() .fwd(new ForwardDemodulation()) .bwd(new BackwardDemodulation()) - .options({ { "term_ordering", "lpo" }}); // use LPO as KBO fails due to caching things in terms + .options({ { "term_ordering", "lpo" } }); // use LPO as KBO fails due to caching things in terms } // demodulation with preordered equation @@ -58,11 +59,121 @@ TEST_SIMPLIFICATION(test02, .expected({ clause({ ~p(f(a,b)) }) }) ) -// TODO find out why this fails -// // demodulation fails with postordered equation -// TEST_SIMPLIFICATION(test03, -// tester() -// .simplifyWith({ clause({ f(x,y) == f(y,x) }) }) -// .toSimplify({ clause({ ~p(f(a,b)) }) }) -// .expected({ /*nothing*/ }) -// ) +// demodulation fails with postordered equation +TEST_SIMPLIFICATION(test03, + tester() + .simplifyWith({ clause({ f(x,y) == f(y,x) }) }) + .toSimplify({ clause({ ~p(f(a,b)) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +// encompassment demodulation +TEST_SIMPLIFICATION(test04, + tester() + .simplifyWith({ clause({ f(x,y) == f(y,x) }) }) + .toSimplify({ clause({ f(b,a) == a }) }) + .expected({ clause({ f(a,b) == a }) }) +) + +// encompassment demodulation fails due to equation being equally general and demodulator being bigger +TEST_SIMPLIFICATION(test05, + tester() + .simplifyWith({ clause({ f(b,a) == f(a,b) }) }) + .toSimplify({ clause({ f(b,a) == a }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +// drc=ordering fails due to other side being smaller than the terms we demodulate into +TEST_SIMPLIFICATION(test06, + tester() + .simplifyWith({ clause({ f(a,b) == a }) }) + .toSimplify({ clause({ f(a,b) == b }) }) + .expected({ clause({ a == b }) }) + .options({ { "term_ordering", "lpo" }, { "demodulation_redundancy_check", "ordering" } }); +) + +// drc=ordering fails due to other side being smaller than the terms we demodulate into +TEST_SIMPLIFICATION(test07, + tester() + .simplifyWith({ clause({ f(x,y) == f(y,x) }) }) + .toSimplify({ clause({ f(b,a) == a }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) + .options({ { "term_ordering", "lpo" }, { "demodulation_redundancy_check", "ordering" } }); +) + +// drc=ordering does not care about ordering of equations +TEST_SIMPLIFICATION(test08, + tester() + .simplifyWith({ clause({ f(b,a) == f(a,b) }) }) + .toSimplify({ clause({ f(b,a) == a }) }) + .expected({ clause({ f(a,b) == a }) }) + .options({ { "term_ordering", "lpo" }, { "demodulation_redundancy_check", "off" } }); +) + +// non-preordered equation is not used with bd/fd=preordered +TEST_SIMPLIFICATION(test09, + tester() + .simplifyWith({ clause({ f(x,y) == f(y,x) }) }) + .toSimplify({ clause({ p(f(b,a)) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) + .options({ { "term_ordering", "lpo" }, { "backward_demodulation", "preordered" }, { "forward_demodulation", "preordered" } }); +) + +// TODO this should be a simplification, but maybe not worth checking, +// otherwise I'm not sure if we should even handle variable equations +// +// demodulation with variable equality +TEST_SIMPLIFICATION(test10, + tester() + .simplifyWith({ clause({ TermSugar(TermList::var(0), s) == y }) }) + .toSimplify({ clause({ f(b,a) == a }) }) + // .expected({ clause({ x == a }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +// demodulation of the smaller side of an equation +TEST_SIMPLIFICATION(test11, + tester() + .simplifyWith({ clause({ f(b,a) == f(a,b) }) }) + .toSimplify({ clause({ g(f(x,b)) == f(b,a) }) }) + .expected({ clause({ g(f(x,b)) == f(a,b) }) }) +) + +// demodulation results in equational tautology +TEST_SIMPLIFICATION(test12, + tester() + .simplifyWith({ clause({ f(b,a) == f(a,b) }) }) + .toSimplify({ clause({ g(f(b,a)) == g(f(a,b)) }) }) + .expected({ /* nothing */ }) + .justifications({ clause({ f(b,a) == f(a,b) }) }) +) + +// demodulation into non-unit clause +TEST_SIMPLIFICATION(test13, + tester() + .simplifyWith({ clause({ f(b,a) == f(a,b) }) }) + .toSimplify({ clause({ f(b,a) == a, ~p(x) }) }) + .expected({ clause({ f(a,b) == a, ~p(x) }) }) +) + +// no demodulation due to different colors +TEST_SIMPLIFICATION(test14, + tester() + .simplifyWith({ clause({ f(x,y) == left(y) }) }) + .toSimplify({ clause({ g(f(a,b)) == right(a) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +// demodulation with colors +TEST_SIMPLIFICATION(test15, + tester() + .simplifyWith({ clause({ f(x,y) == left(y) }) }) + .toSimplify({ clause({ g(f(a,b)) == left(a) }) }) + .expected({ clause({ g(left(b)) == left(a) }) }) +) diff --git a/UnitTests/tInferences_EqualityResolution.cpp b/UnitTests/tInferences_EqualityResolution.cpp index 90063c860..c769efb37 100644 --- a/UnitTests/tInferences_EqualityResolution.cpp +++ b/UnitTests/tInferences_EqualityResolution.cpp @@ -8,7 +8,6 @@ * and in the source directory */ -#include "Test/UnitTesting.hpp" #include "Test/SyntaxSugar.hpp" #include "Test/GenerationTester.hpp" diff --git a/UnitTests/tInferences_Factoring.cpp b/UnitTests/tInferences_Factoring.cpp new file mode 100644 index 000000000..0b0cbd138 --- /dev/null +++ b/UnitTests/tInferences_Factoring.cpp @@ -0,0 +1,91 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ + +#include "Test/SyntaxSugar.hpp" +#include "Test/GenerationTester.hpp" + +#include "Inferences/Factoring.hpp" + +using namespace Test; + +REGISTER_GEN_TESTER(Test::Generation::GenerationTester(Factoring())) + +/** + * NECESSARY: We need to tell the tester which syntax sugar to import for creating terms & clauses. + * See Test/SyntaxSugar.hpp for which kinds of syntax sugar are available + */ +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_SORT(s) \ + DECL_FUNC(f, {s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_PRED (p, {s}) \ + DECL_PRED (q, {s}) + +// no factoring for unit clauses +TEST_GENERATION(test01, + Generation::AsymmetricTest() + .input( clause({ selected(p(f(x))) })) + .expected(none()) + ) + +// no factoring for equalities +TEST_GENERATION(test02, + Generation::AsymmetricTest() + .input( clause({ selected(f(x) == x), selected(f(f(y)) == f(y)) })) + .expected(none()) + ) + +// no factoring for negative literals +TEST_GENERATION(test03, + Generation::AsymmetricTest() + .input( clause({ selected(~p(f(x))), selected(~p(y)) })) + .expected(none()) + ) + +// no factoring for non-unifiable predicates +TEST_GENERATION(test04, + Generation::AsymmetricTest() + .input( clause({ selected(p(f(x))), selected(q(y)) })) + .expected(none()) + ) + +// no factoring for non-unifiable functions +TEST_GENERATION(test05, + Generation::AsymmetricTest() + .input( clause({ selected(p(f(x))), selected(p(g(y))) })) + .expected(none()) + ) + +// no factoring for non-selected literals +TEST_GENERATION(test06, + Generation::AsymmetricTest() + .input( clause({ p(f(x)), p(y) })) + .expected(none()) + ) + +// factoring between positive literals where one is selected +TEST_GENERATION(test07, + Generation::AsymmetricTest() + .input( clause({ selected(p(f(x))), p(y) })) + .expected(exactly(clause({ p(f(x)) }))) + ) + +// factoring between only two positive literals +TEST_GENERATION(test08, + Generation::AsymmetricTest() + .input( clause({ selected(p(f(x))), p(y), p(f(g(z))) })) + .expected(exactly( + clause({ p(f(x)), p(f(g(y))) }), + clause({ p(f(g(x))), p(y) }) + )) + ) diff --git a/UnitTests/tInferences_FunctionDefinitionRewriting.cpp b/UnitTests/tInferences_FunctionDefinitionRewriting.cpp index 51ae971a0..713d56c51 100644 --- a/UnitTests/tInferences_FunctionDefinitionRewriting.cpp +++ b/UnitTests/tInferences_FunctionDefinitionRewriting.cpp @@ -8,7 +8,6 @@ * and in the source directory */ -#include "Test/UnitTesting.hpp" #include "Test/SyntaxSugar.hpp" #include "Test/GenerationTester.hpp" diff --git a/UnitTests/tInferences_GaussianVariableElimination.cpp b/UnitTests/tInferences_GaussianVariableElimination.cpp index 3d9f9a63f..551f54627 100644 --- a/UnitTests/tInferences_GaussianVariableElimination.cpp +++ b/UnitTests/tInferences_GaussianVariableElimination.cpp @@ -8,15 +8,12 @@ * and in the source directory */ #include "Test/AlascaTestUtils.hpp" -#include "Test/TestUtils.hpp" #include "Test/SyntaxSugar.hpp" #include "Inferences/GaussianVariableElimination.hpp" #include "Kernel/Ordering.hpp" #include "Inferences/PolynomialEvaluation.hpp" #include "Inferences/Cancellation.hpp" -#include "Test/SyntaxSugar.hpp" -#include "Test/TestUtils.hpp" #include "Test/SimplificationTester.hpp" #include "Test/GenerationTester.hpp" #include "Kernel/KBO.hpp" diff --git a/UnitTests/tInferences_InferenceEngine.cpp b/UnitTests/tInferences_InferenceEngine.cpp index c7d235343..fe5548d9e 100644 --- a/UnitTests/tInferences_InferenceEngine.cpp +++ b/UnitTests/tInferences_InferenceEngine.cpp @@ -7,7 +7,6 @@ * https://vprover.github.io/license.html * and in the source directory */ -#include "Test/UnitTesting.hpp" #include "Test/SyntaxSugar.hpp" #include "Inferences/InferenceEngine.hpp" @@ -15,8 +14,6 @@ using namespace Test; -REGISTER_SIMPL_TESTER(Simplification::RuleSimplificationTester) - #define MY_SYNTAX_SUGAR \ DECL_DEFAULT_VARS \ DECL_SORT(s) \ @@ -27,8 +24,78 @@ REGISTER_SIMPL_TESTER(Simplification::RuleSimplificationTester) + +TEST_SIMPLIFY(dlr_test01, + Simplification::Success() + .input(clause({ p(a) })) + .expected(clause({ p(a) })) + ) + +TEST_SIMPLIFY(dlr_test02, Simplification::Success() .input(clause({ p(a), p(a) })) .expected(clause({ p(a) })) ) + +TEST_SIMPLIFY(dlr_test03, + Simplification::Success() + .input(clause({ p(a), q(b) })) + .expected(clause({ p(a), q(b) })) + ) + +TEST_SIMPLIFY(dlr_test04, + Simplification::Success() + .input(clause({ p(x), p(y) })) + .expected(clause({ p(x), p(y) })) + ) + +TEST_SIMPLIFY(dlr_test05, + Simplification::Success() + .input(clause({ p(a), ~p(x), q(f(a,y)), q(b), q(f(a,y)), p(a), ~p(x), p(a) })) + .expected(clause({ p(a), ~p(x), q(f(a,y)), q(b) })) + ) + +TEST_SIMPLIFY(dlr_test06, + Simplification::Success() + .input(clause({ p(a), ~p(a), ~p(a), p(a), q(b) })) + .expected(clause({ p(a), ~p(a), q(b) })) + ) +} + +namespace TrivialInequalitiesRemovalISETest { + +REGISTER_SIMPL_TESTER(Simplification::RuleSimplificationTester) + +TEST_SIMPLIFY(tir_test01, + Simplification::Success() + .input(clause({ a == b })) + .expected(clause({ a == b })) + ) + +TEST_SIMPLIFY(tir_test02, + Simplification::Success() + .input(clause({ a != b })) + .expected(clause({ a != b })) + ) + +TEST_SIMPLIFY(tir_test03, + Simplification::Success() + .input(clause({ a == a })) + .expected(clause({ a == a })) + ) + +TEST_SIMPLIFY(tir_test04, + Simplification::Success() + .input(clause({ a != a })) + .expected(clause({ })) + ) + +TEST_SIMPLIFY(tir_test05, + Simplification::Success() + .input(clause({ p(a), a != a, f(x,y) != g(y), f(x,y) != f(x,y), ~q(x), a != a, g(y) == g(y) })) + .expected(clause({ p(a), f(x,y) != g(y), ~q(x), g(y) == g(y) })) + ) +} diff --git a/UnitTests/tInferences_PushUnaryMinus.cpp b/UnitTests/tInferences_PushUnaryMinus.cpp index 37571a13d..444f3103c 100644 --- a/UnitTests/tInferences_PushUnaryMinus.cpp +++ b/UnitTests/tInferences_PushUnaryMinus.cpp @@ -7,14 +7,11 @@ * https://vprover.github.io/license.html * and in the source directory */ -#include "Test/UnitTesting.hpp" #include "Test/SyntaxSugar.hpp" -#include "Inferences/PushUnaryMinus.hpp" - -#include "Test/SyntaxSugar.hpp" -#include "Test/TestUtils.hpp" #include "Test/SimplificationTester.hpp" +#include "Inferences/PushUnaryMinus.hpp" + using namespace std; using namespace Kernel; using namespace Inferences; diff --git a/UnitTests/tInferences_Superposition.cpp b/UnitTests/tInferences_Superposition.cpp index 47b4a2e0e..5d8fd9678 100644 --- a/UnitTests/tInferences_Superposition.cpp +++ b/UnitTests/tInferences_Superposition.cpp @@ -7,8 +7,6 @@ * https://vprover.github.io/license.html * and in the source directory */ - -#include "Test/UnitTesting.hpp" #include "Test/SyntaxSugar.hpp" #include "Test/GenerationTester.hpp" @@ -26,10 +24,12 @@ using namespace Test; DECL_SORT(s) \ DECL_FUNC(f, {s, s}, s) \ DECL_FUNC(g, {s}, s) \ + DECL_LEFT_FUNC(left, {s}, s) \ + DECL_RIGHT_FUNC(right, {s}, s) \ DECL_CONST(a, s) \ DECL_CONST(b, s) \ DECL_PRED (p, {s}) \ - DECL_PRED (q, {s}) \ + DECL_PRED (q, {s}) REGISTER_GEN_TESTER(Generation::GenerationTester(Superposition())) @@ -225,6 +225,35 @@ TEST_GENERATION(test_17, .expected(none()) ) -// TODO -// superposition with colors -// superposition only into bigger side of the equation \ No newline at end of file +// superposition not performed due to rewriting smaller side of equality +TEST_GENERATION(test_18, + Generation::SymmetricTest() + .inputs({ + clause({ selected(f(a,b) == a) }), + clause({ selected(g(f(x,y)) != g(f(y,x))) }), + }) + .selfApplications(false) + .expected(none()) + ) + +// superposition not performed due to different colors +TEST_GENERATION(test_19, + Generation::SymmetricTest() + .inputs({ + clause({ selected(g(left(x)) == x) }), + clause({ selected(f(g(x),y) != right(x)) }), + }) + .selfApplications(false) + .expected(none()) + ) + +// superposition performed with colors +TEST_GENERATION(test_20, + Generation::SymmetricTest() + .inputs({ + clause({ selected(g(left(x)) == x) }), + clause({ selected(f(g(x),y) != left(x)) }), + }) + .selfApplications(false) + .expected(exactly(clause({ f(x,y) != left(left(x)) }))) + ) diff --git a/UnitTests/tInferences_TautologyDeletionISE.cpp b/UnitTests/tInferences_TautologyDeletionISE.cpp new file mode 100644 index 000000000..312260e58 --- /dev/null +++ b/UnitTests/tInferences_TautologyDeletionISE.cpp @@ -0,0 +1,57 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ +#include "Test/SyntaxSugar.hpp" +#include "Inferences/TautologyDeletionISE.hpp" + +#include "Test/SimplificationTester.hpp" + +using namespace Test; + +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_SORT(s) \ + DECL_FUNC(f, {s, s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_PRED (p, {s}) \ + DECL_PRED (q, {s}) \ + +REGISTER_SIMPL_TESTER(Simplification::RuleSimplificationTester) + +TEST_SIMPLIFY(test01, + Simplification::Success() + .input(clause({ f(x,y) == g(x) })) + .expected(clause({ f(x,y) == g(x) })) + ) + +TEST_SIMPLIFY(test02, + Simplification::Success() + .input(clause({ p(x) })) + .expected(clause({ p(x) })) + ) + +TEST_SIMPLIFY(test03, + Simplification::Success() + .input(clause({ f(x,y) == f(x,y) })) + .expected(Simplification::Redundant{}) + ) + +TEST_SIMPLIFY(test04, + Simplification::Success() + .input(clause({ p(x), ~p(y) })) + .expected(clause({ p(x), ~p(y) })) + ) + +TEST_SIMPLIFY(test05, + Simplification::Success() + .input(clause({ p(x), ~p(x) })) + .expected(Simplification::Redundant{}) + ) diff --git a/UnitTests/tInferences_TheoryInstAndSimp.cpp b/UnitTests/tInferences_TheoryInstAndSimp.cpp index 7d8905106..e0aaca5ff 100644 --- a/UnitTests/tInferences_TheoryInstAndSimp.cpp +++ b/UnitTests/tInferences_TheoryInstAndSimp.cpp @@ -10,7 +10,6 @@ #if VZ3 -#include "Test/UnitTesting.hpp" #include "Test/SyntaxSugar.hpp" #include "Inferences/TheoryInstAndSimp.hpp" @@ -87,7 +86,6 @@ TheoryInstAndSimp* theoryInstAndSimp(Options::TheoryInstSimp mode, bool withGene ); } -using Shell::Int; REGISTER_GEN_TESTER(Test::Generation::GenerationTester(std::move(*theoryInstAndSimp(Options::TheoryInstSimp::ALL)))) TEST_GENERATION(test_01, diff --git a/UnitTests/tIntegerConstantType.cpp b/UnitTests/tIntegerConstantType.cpp index 56910e10c..200fa062f 100644 --- a/UnitTests/tIntegerConstantType.cpp +++ b/UnitTests/tIntegerConstantType.cpp @@ -13,7 +13,6 @@ #include "Lib/BitUtils.hpp" // TODO rename to theory test #include "Kernel/Theory.hpp" -#include "Lib/Int.hpp" #include "Test/UnitTesting.hpp" diff --git a/cmake/sources.cmake b/cmake/sources.cmake index 2f90d66b5..4566e4040 100644 --- a/cmake/sources.cmake +++ b/cmake/sources.cmake @@ -57,6 +57,7 @@ set(UNIT_TESTS UnitTests/tInferences_BinaryResolution.cpp UnitTests/tInferences_Demodulation.cpp UnitTests/tInferences_EqualityResolution.cpp + UnitTests/tInferences_Factoring.cpp UnitTests/tInferences_ForwardGroundJoinability.cpp UnitTests/tInferences_FunctionDefinitionRewriting.cpp UnitTests/tInferences_GaussianVariableElimination.cpp @@ -64,6 +65,7 @@ set(UNIT_TESTS UnitTests/tInferences_InferenceEngine.cpp UnitTests/tInferences_PushUnaryMinus.cpp UnitTests/tInferences_Superposition.cpp + UnitTests/tInferences_TautologyDeletionISE.cpp UnitTests/tIntegerConstantType.cpp UnitTests/tInterpretedFunctions.cpp UnitTests/tIterator.cpp From 82bba333767aff785a56684ab5cd61014619f75e Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Tue, 13 Jan 2026 17:41:01 +0100 Subject: [PATCH 05/13] Fix bug in testing equality modulo AC --- Test/TestUtils.cpp | 3 ++- UnitTests/tInferences_Superposition.cpp | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/Test/TestUtils.cpp b/Test/TestUtils.cpp index e40f4efa5..41a44ebb4 100644 --- a/Test/TestUtils.cpp +++ b/Test/TestUtils.cpp @@ -184,7 +184,8 @@ void __collect(unsigned functor, Term* t, Stack& out) { out.push(*trm); } else { ASS(trm->isTerm()); - if (trm->term()->functor() == functor) { + // Note: the input term can be a literal as well, so let's check it + if (trm->term()->functor() == functor && trm->term()->isLiteral() == t->isLiteral()) { __collect(functor, trm->term(), out); } else { out.push(*trm); diff --git a/UnitTests/tInferences_Superposition.cpp b/UnitTests/tInferences_Superposition.cpp index 5d8fd9678..88d520e45 100644 --- a/UnitTests/tInferences_Superposition.cpp +++ b/UnitTests/tInferences_Superposition.cpp @@ -184,8 +184,8 @@ TEST_GENERATION(test_14, }) .selfApplications(false) .expected(exactly( - clause({ g(a) != b, f(b,a) != a }), - clause({ g(a) != b, f(b,a) != a }) + clause({ g(a) != b, f(a,b) != a }), + clause({ g(a) != b, f(a,b) != a }) )) ) From 67b96e97527243a22cc5f4ce7b805a2dcc8933a8 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Wed, 14 Jan 2026 11:06:31 +0100 Subject: [PATCH 06/13] Add subsumption demodulation and subsumption/subsumption resolution tests --- ...ences_CodeTreeSubsumptionAndResolution.cpp | 379 ++++++++++++++++++ UnitTests/tInferences_Demodulation.cpp | 4 + .../tInferences_SubsumptionAndResolution.cpp | 379 ++++++++++++++++++ .../tInferences_SubsumptionDemodulation.cpp | 53 +++ cmake/sources.cmake | 3 + 5 files changed, 818 insertions(+) create mode 100644 UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp create mode 100644 UnitTests/tInferences_SubsumptionAndResolution.cpp create mode 100644 UnitTests/tInferences_SubsumptionDemodulation.cpp diff --git a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp new file mode 100644 index 000000000..1f81c9769 --- /dev/null +++ b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp @@ -0,0 +1,379 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ + +#include "Test/SyntaxSugar.hpp" +#include "Inferences/CodeTreeForwardSubsumptionAndResolution.hpp" +#include "Inferences/BackwardSubsumptionAndResolution.hpp" + +#include "Test/FwdBwdSimplificationTester.hpp" + +using namespace std; +using namespace Kernel; +using namespace Inferences; +using namespace Test; + +#define MY_SYNTAX_SUGAR \ + __ALLOW_UNUSED( \ + DECL_DEFAULT_VARS \ + DECL_VAR(x1, 1) \ + DECL_VAR(x2, 2) \ + DECL_VAR(x3, 3) \ + DECL_VAR(x4, 4) \ + DECL_VAR(x5, 5) \ + DECL_VAR(x6, 6) \ + DECL_VAR(x7, 7) \ + DECL_VAR(y1, 11) \ + DECL_VAR(y2, 12) \ + DECL_VAR(y3, 13) \ + DECL_VAR(y4, 14) \ + DECL_VAR(y5, 15) \ + DECL_VAR(y6, 16) \ + DECL_VAR(y7, 17) \ + DECL_SORT(s) \ + DECL_CONST(c, s) \ + DECL_CONST(d, s) \ + DECL_CONST(e, s) \ + DECL_FUNC(f, {s}, s) \ + DECL_FUNC(f2, {s, s}, s) \ + DECL_FUNC(f3, {s, s, s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_FUNC(g2, {s, s}, s) \ + DECL_FUNC(h, {s}, s) \ + DECL_FUNC(h2, {s, s}, s) \ + DECL_FUNC(i, {s}, s) \ + DECL_FUNC(i2, {s, s}, s) \ + DECL_PRED(p, {s}) \ + DECL_PRED(p2, {s, s}) \ + DECL_PRED(p3, {s, s, s}) \ + DECL_PRED(q, {s}) \ + DECL_PRED(q2, {s, s}) \ + DECL_PRED(r, {s}) \ + DECL_PRED(r2, {s, s}) \ + ) + +namespace CodeTreeForwardSubsumptionAndResolutionTest { + +inline auto tester() { + return FwdBwdSimplification::TestCase() + .fwd(new CodeTreeForwardSubsumptionAndResolution(/*subsumptionResolution=*/true)) + .bwd(new BackwardSubsumptionAndResolution(/*subsumption=*/true, /*subsumptionByUnitsOnly=*/false, /*subsumptionResolution=*/true, /*srByUnitsOnly=*/false)); +} + +// Note: most of these tests were taken from the SAT subsumption test suite + +// positive subsumptions + +TEST_SIMPLIFICATION(pos_sub_test01, + tester() + .simplifyWith({ clause({ p2(x, f(y)) }) }) + .toSimplify({ clause({ p2(c, f(d)) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test02, + tester() + .simplifyWith({ clause({ ~p2(g(x), f(y)) }) }) + .toSimplify({ clause({ ~p2(g(x), f(x)) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test03, + tester() + .simplifyWith({ clause({ p3(x1, x2, x3), p3(f(x2), x4, x4) }) }) + .toSimplify({ clause({ p3(f(c), d, y1), p3(f(d), c, c) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test04, + tester() + .simplifyWith({ clause({ p3(x1, x2, x3), p3(f(x2), x4, x4) }) }) + .toSimplify({ clause({ p3(f(c), d, y1), p3(f(d), c, c), r(x1) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test05, + tester() + .simplifyWith({ clause({ p(f2(f(g(x1)), x1)), c == g(x1) }) }) + .toSimplify({ clause({ g(y1) == c, p(f2(f(g(y1)), y1)) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test06, + tester() + .simplifyWith({ clause({ f2(x1, x2) == c, ~p2(x1, x3), p2(f(f2(x1, x2)), f(x3)) }) }) + .toSimplify({ clause({ c == f2(x3, y2), ~p2(x3, y1), p2(f(f2(x3, y2)), f(y1)) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test07, + tester() + .simplifyWith({ clause({ p(f2(f(e), g2(x4, x3))), p2(f2(f(e), g2(x4, x3)), x3), f(e) == g2(x4, x3) }) }) + .toSimplify({ clause({ p(f2(f(e), g2(y1, y3))), p2(f2(f(e), g2(y1, y3)), y3), f(e) == g2(y1, y3) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test08, + tester() + .simplifyWith({ clause({ p3(y7, f(y1), x4), ~p3(y7, y1, x4) }) }) + .toSimplify({ clause({ p3(x6, f(y3), d), ~p3(x6, y3, d) }) }) + .expected({ /* nothing */ }) +) + +// negative subsumptions + +TEST_SIMPLIFICATION(neg_sub_test01, + tester() + .simplifyWith({ clause({ p2(f2(g2(x1, x2), x3), x3), p2(f2(g2(x1, x2), x3), x2), g2(x1, x2) == x3 }) }) + .toSimplify({ clause({ p2(f2(g2(y1, y2), y2), y2), g2(y1, y2) == y2, ~p2(f2(g2(y1, y2), y2), g2(y1, y2)) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_test02, + tester() + .simplifyWith({ clause({ ~p2(x1, x2), p(x1) }) }) + .toSimplify({ clause({ p(y1), ~p(f(f2(f2(y2, y2), f2(y2, y3)))), ~p(y3), ~p(y2) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_test03, + tester() + .simplifyWith({ clause({ p2(y5, f(f2(c, x1))), ~p(c), ~p(y5) }) }) + .toSimplify({ clause({ ~q(f(d)), p2(c, f(f2(c, x4))), r(e), ~p(c), d == g(c) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_test04, + tester() + .simplifyWith({ clause({ p2(y5, f(f2(x1, c))), ~p(c), ~p(y5) }) }) + .toSimplify({ clause({ ~q(d), p2(c, f(f2(x4, c))), r(d), ~p(c), d == g(c) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_test05, + tester() + .simplifyWith({ clause({ p(x1), x1 == f(x2), p(x2) }) }) + .toSimplify({ clause({ p(y1), y1 == f(y1) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_test06, + tester() + .simplifyWith({ clause({ p(x1), x1 == f(x2), p(x2), q(x1) }) }) + .toSimplify({ clause({ p(y1), y1 == f(y1), q(y2), r(y3) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_test07, + tester() + .simplifyWith({ clause({ p(f(x1)), p(f(x2)) }) }) + .toSimplify({ clause({ p(f(y1)), p(g(y2)) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +// positive subsumption resolutions + +TEST_SIMPLIFICATION(pos_sub_res_test01, + tester() + .simplifyWith({ clause({ ~p(x1), q(x1) }) }) + .toSimplify({ clause({ p(c), q(c), r(e) }) }) + .expected({ clause({ q(c), r(e) }) }) +) + +TEST_SIMPLIFICATION(pos_sub_res_test02, + tester() + .simplifyWith({ clause({ p2(x1, x2), p2(f(x2), x3) }) }) + .toSimplify({ clause({ ~p2(f(y1), d), p2(g(y1), c), ~p2(f(c), e) }) }) + .expected({ clause({ ~p2(f(y1), d), p2(g(y1), c) }) }) +) + +TEST_SIMPLIFICATION(pos_sub_res_test03, + tester() + .simplifyWith({ clause({ p3(x2, f(x2), e) }) }) + .toSimplify({ clause({ p3(f(e), x5, x5), ~p3(x4, f(x4), e) }) }) + .expected({ clause({ p3(f(e), x5, x5) }) }) +) + +TEST_SIMPLIFICATION(pos_sub_res_test04, + tester() + .simplifyWith({ clause({ p(c) }) }) + .toSimplify({ clause({ ~p(c) }) }) + .expected({ clause({}) }) +) + +TEST_SIMPLIFICATION(pos_sub_res_test05, + tester() + .simplifyWith({ clause({ ~p(f(x1)), q(x1) }) }) + .toSimplify({ clause({ ~p2(x2, x5), q(x2), p(f(x2)), ~q(g(x5)) }) }) + .expected({ clause({ ~p2(x2, x5), q(x2), ~q(g(x5)) }) }) +) + +// TODO I'm assuming these give different results for forwards and backwards, so they cannot be enabled +// TEST_SIMPLIFICATION(pos_sub_res_test06, +// tester() +// .simplifyWith({ clause({ p(f2(y7, x6)), p2(y7, x6) }) }) +// .toSimplify({ clause({ p2(f(g(x5)), y4), ~p(f2(f(g(x5)), y4)), ~p2(f2(f(g(x5)), y4), x5) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// TEST_SIMPLIFICATION(pos_sub_res_test07, +// tester() +// .simplifyWith({ clause({ p(f2(y7, x6)), p2(y7, x6) }) }) +// .toSimplify({ clause({ p2(f(g(x5)), y4), ~p(f2(f(g(x5)), y4)), ~p2(f2(f(g(x5)), y4), x5) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// TEST_SIMPLIFICATION(pos_sub_res_test08, +// tester() +// .simplifyWith({ clause({ ~p2(y7, d) }) }) +// .toSimplify({ clause({ ~p(x6), ~p(x5), ~p2(f(f2(f2(x5, x5), f2(x5, x6))), x6), p2(f2(f2(x5, x5), f2(x5, x6)), d) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// TEST_SIMPLIFICATION(pos_sub_res_test09, +// tester() +// .simplifyWith({ clause({ ~p3(d, y7, d), ~p3(y7, e, c) }) }) +// .toSimplify({ clause({ p3(d, x6, d), ~p3(x6, e, c) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// TEST_SIMPLIFICATION(pos_sub_res_test10, +// tester() +// .simplifyWith({ clause({ p2(y7, x6), f2(y7, x6) == f2(f3(x5, y4, x4), x4), p2(y4, x4) }) }) +// .toSimplify({ clause({ ~p2(g2(h2(y3, x2), x2), x7), f2(g2(h2(y3, x2), x2), x7) == f2(f3(y6, g2(h2(y3, x2), x2), x7), x7) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// TEST_SIMPLIFICATION(pos_sub_res_test11, +// tester() +// .simplifyWith({ clause({ p2(y7, x6), ~q2(x5, x6), ~p2(y7, x5) }) }) +// .toSimplify({ clause({ p2(f2(y4, x6), y4), ~p2(x6, y7), ~r2(y4, y7), ~p2(x6, d), ~q2(y4, d), ~q2(y7, d) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// TEST_SIMPLIFICATION(pos_sub_res_test12, +// tester() +// .simplifyWith({ clause({ p(d) }) }) +// .toSimplify({ clause({ q(d), ~p(d) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// negative subsumption resolutions + +TEST_SIMPLIFICATION(neg_sub_res_test01, + tester() + .simplifyWith({ clause({ ~p(x1), q(x1) }) }) + .toSimplify({ clause({ p(c), q(d), r(e) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test02, + tester() + .simplifyWith({ clause({ ~p(x1), ~q(x2) }) }) + .toSimplify({ clause({ p(c), q(d), r(e) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test03, + tester() + .simplifyWith({ clause({ ~p(x1), r(c) }) }) + .toSimplify({ clause({ p(c), q(d), r(e) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test04, + tester() + .simplifyWith({ clause({ ~p(x1), p2(x1, x2) }) }) + .toSimplify({ clause({ p(c), q(d), r(e) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test05, + tester() + .simplifyWith({ clause({ p3(x1, x2, x2), ~p3(x2, c, c) }) }) + .toSimplify({ clause({ p3(y1, c, c), ~p3(y1, y2, y2) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test06, + tester() + .simplifyWith({ clause({ p3(y7, x6, x6), ~p3(y7, d, d) }) }) + .toSimplify({ clause({ p3(x5, d, d), ~p3(x5, x6, x6) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test07, + tester() + .simplifyWith({ clause({ ~p3(y7, d, d), p3(y7, x6, x6) }) }) + .toSimplify({ clause({ ~p3(x5, y4, f(f2(x4, f(y3)))), p3(x2, d, d), ~p3(x7, x4, y3), ~p3(x2, f2(x5, y4), x7) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test08, + tester() + .simplifyWith({ clause({ ~p3(y7, d, d), p3(y7, x6, x6) }) }) + .toSimplify({ clause({ ~p3(x5, x6, x6), p3(d, d, x5) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test09, + tester() + .simplifyWith({ clause({ ~p3(d, y7, d), p3(x6, y7, x6) }) }) + .toSimplify({ clause({ p3(d, x5, d), ~p3(y4, f(y4), f(x5)) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test10, + tester() + .simplifyWith({ clause({ ~p3(d, d, d), p3(f(f(y7)), d, y7) }) }) + .toSimplify({ clause({ p3(d, x6, x6) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test11, + tester() + .simplifyWith({ clause({ p2(y7, d), p2(e, y7), e == y7 }) }) + .toSimplify({ clause({ ~p2(x6, x5), ~p2(y7, x6), p2(y7, x5) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test12, + tester() + .simplifyWith({ clause({ f2(y1, y3) == x1, ~p2(g2(x1, f2(y1, y3)), x1), ~p2(g2(x1, f2(y1, y3)), y1), ~p2(g2(x1, f2(y1, y3)), y3) }) }) + .toSimplify({ clause({ p2(g2(x2, f2(y1, y3)), x2), f2(y1, y3) == x2, p2(g2(x2, f2(y1, y3)), y3) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +} diff --git a/UnitTests/tInferences_Demodulation.cpp b/UnitTests/tInferences_Demodulation.cpp index 979b8729a..143d7f930 100644 --- a/UnitTests/tInferences_Demodulation.cpp +++ b/UnitTests/tInferences_Demodulation.cpp @@ -36,6 +36,8 @@ using namespace Test; DECL_PRED (p, {s}) \ DECL_PRED (q, {s}) +namespace DemodulationTester { + inline auto tester() { return FwdBwdSimplification::TestCase() .fwd(new ForwardDemodulation()) @@ -177,3 +179,5 @@ TEST_SIMPLIFICATION(test15, .toSimplify({ clause({ g(f(a,b)) == left(a) }) }) .expected({ clause({ g(left(b)) == left(a) }) }) ) + +} diff --git a/UnitTests/tInferences_SubsumptionAndResolution.cpp b/UnitTests/tInferences_SubsumptionAndResolution.cpp new file mode 100644 index 000000000..5dc2cfb66 --- /dev/null +++ b/UnitTests/tInferences_SubsumptionAndResolution.cpp @@ -0,0 +1,379 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ + +#include "Test/SyntaxSugar.hpp" +#include "Inferences/ForwardSubsumptionAndResolution.hpp" +#include "Inferences/BackwardSubsumptionAndResolution.hpp" + +#include "Test/FwdBwdSimplificationTester.hpp" + +using namespace std; +using namespace Kernel; +using namespace Inferences; +using namespace Test; + +#define MY_SYNTAX_SUGAR \ + __ALLOW_UNUSED( \ + DECL_DEFAULT_VARS \ + DECL_VAR(x1, 1) \ + DECL_VAR(x2, 2) \ + DECL_VAR(x3, 3) \ + DECL_VAR(x4, 4) \ + DECL_VAR(x5, 5) \ + DECL_VAR(x6, 6) \ + DECL_VAR(x7, 7) \ + DECL_VAR(y1, 11) \ + DECL_VAR(y2, 12) \ + DECL_VAR(y3, 13) \ + DECL_VAR(y4, 14) \ + DECL_VAR(y5, 15) \ + DECL_VAR(y6, 16) \ + DECL_VAR(y7, 17) \ + DECL_SORT(s) \ + DECL_CONST(c, s) \ + DECL_CONST(d, s) \ + DECL_CONST(e, s) \ + DECL_FUNC(f, {s}, s) \ + DECL_FUNC(f2, {s, s}, s) \ + DECL_FUNC(f3, {s, s, s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_FUNC(g2, {s, s}, s) \ + DECL_FUNC(h, {s}, s) \ + DECL_FUNC(h2, {s, s}, s) \ + DECL_FUNC(i, {s}, s) \ + DECL_FUNC(i2, {s, s}, s) \ + DECL_PRED(p, {s}) \ + DECL_PRED(p2, {s, s}) \ + DECL_PRED(p3, {s, s, s}) \ + DECL_PRED(q, {s}) \ + DECL_PRED(q2, {s, s}) \ + DECL_PRED(r, {s}) \ + DECL_PRED(r2, {s, s}) \ + ) + +namespace SubsumptionAndResolutionTester { + +inline auto tester() { + return FwdBwdSimplification::TestCase() + .fwd(new ForwardSubsumptionAndResolution()) + .bwd(new BackwardSubsumptionAndResolution(/*subsumption=*/true, /*subsumptionByUnitsOnly=*/false, /*subsumptionResolution=*/true, /*srByUnitsOnly=*/false)); +} + +// Note: most of these tests were taken from the SAT subsumption test suite + +// positive subsumptions + +TEST_SIMPLIFICATION(pos_sub_test01, + tester() + .simplifyWith({ clause({ p2(x, f(y)) }) }) + .toSimplify({ clause({ p2(c, f(d)) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test02, + tester() + .simplifyWith({ clause({ ~p2(g(x), f(y)) }) }) + .toSimplify({ clause({ ~p2(g(x), f(x)) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test03, + tester() + .simplifyWith({ clause({ p3(x1, x2, x3), p3(f(x2), x4, x4) }) }) + .toSimplify({ clause({ p3(f(c), d, y1), p3(f(d), c, c) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test04, + tester() + .simplifyWith({ clause({ p3(x1, x2, x3), p3(f(x2), x4, x4) }) }) + .toSimplify({ clause({ p3(f(c), d, y1), p3(f(d), c, c), r(x1) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test05, + tester() + .simplifyWith({ clause({ p(f2(f(g(x1)), x1)), c == g(x1) }) }) + .toSimplify({ clause({ g(y1) == c, p(f2(f(g(y1)), y1)) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test06, + tester() + .simplifyWith({ clause({ f2(x1, x2) == c, ~p2(x1, x3), p2(f(f2(x1, x2)), f(x3)) }) }) + .toSimplify({ clause({ c == f2(x3, y2), ~p2(x3, y1), p2(f(f2(x3, y2)), f(y1)) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test07, + tester() + .simplifyWith({ clause({ p(f2(f(e), g2(x4, x3))), p2(f2(f(e), g2(x4, x3)), x3), f(e) == g2(x4, x3) }) }) + .toSimplify({ clause({ p(f2(f(e), g2(y1, y3))), p2(f2(f(e), g2(y1, y3)), y3), f(e) == g2(y1, y3) }) }) + .expected({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(pos_sub_test08, + tester() + .simplifyWith({ clause({ p3(y7, f(y1), x4), ~p3(y7, y1, x4) }) }) + .toSimplify({ clause({ p3(x6, f(y3), d), ~p3(x6, y3, d) }) }) + .expected({ /* nothing */ }) +) + +// negative subsumptions + +TEST_SIMPLIFICATION(neg_sub_test01, + tester() + .simplifyWith({ clause({ p2(f2(g2(x1, x2), x3), x3), p2(f2(g2(x1, x2), x3), x2), g2(x1, x2) == x3 }) }) + .toSimplify({ clause({ p2(f2(g2(y1, y2), y2), y2), g2(y1, y2) == y2, ~p2(f2(g2(y1, y2), y2), g2(y1, y2)) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_test02, + tester() + .simplifyWith({ clause({ ~p2(x1, x2), p(x1) }) }) + .toSimplify({ clause({ p(y1), ~p(f(f2(f2(y2, y2), f2(y2, y3)))), ~p(y3), ~p(y2) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_test03, + tester() + .simplifyWith({ clause({ p2(y5, f(f2(c, x1))), ~p(c), ~p(y5) }) }) + .toSimplify({ clause({ ~q(f(d)), p2(c, f(f2(c, x4))), r(e), ~p(c), d == g(c) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_test04, + tester() + .simplifyWith({ clause({ p2(y5, f(f2(x1, c))), ~p(c), ~p(y5) }) }) + .toSimplify({ clause({ ~q(d), p2(c, f(f2(x4, c))), r(d), ~p(c), d == g(c) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_test05, + tester() + .simplifyWith({ clause({ p(x1), x1 == f(x2), p(x2) }) }) + .toSimplify({ clause({ p(y1), y1 == f(y1) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_test06, + tester() + .simplifyWith({ clause({ p(x1), x1 == f(x2), p(x2), q(x1) }) }) + .toSimplify({ clause({ p(y1), y1 == f(y1), q(y2), r(y3) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_test07, + tester() + .simplifyWith({ clause({ p(f(x1)), p(f(x2)) }) }) + .toSimplify({ clause({ p(f(y1)), p(g(y2)) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +// positive subsumption resolutions + +TEST_SIMPLIFICATION(pos_sub_res_test01, + tester() + .simplifyWith({ clause({ ~p(x1), q(x1) }) }) + .toSimplify({ clause({ p(c), q(c), r(e) }) }) + .expected({ clause({ q(c), r(e) }) }) +) + +TEST_SIMPLIFICATION(pos_sub_res_test02, + tester() + .simplifyWith({ clause({ p2(x1, x2), p2(f(x2), x3) }) }) + .toSimplify({ clause({ ~p2(f(y1), d), p2(g(y1), c), ~p2(f(c), e) }) }) + .expected({ clause({ ~p2(f(y1), d), p2(g(y1), c) }) }) +) + +TEST_SIMPLIFICATION(pos_sub_res_test03, + tester() + .simplifyWith({ clause({ p3(x2, f(x2), e) }) }) + .toSimplify({ clause({ p3(f(e), x5, x5), ~p3(x4, f(x4), e) }) }) + .expected({ clause({ p3(f(e), x5, x5) }) }) +) + +TEST_SIMPLIFICATION(pos_sub_res_test04, + tester() + .simplifyWith({ clause({ p(c) }) }) + .toSimplify({ clause({ ~p(c) }) }) + .expected({ clause({}) }) +) + +TEST_SIMPLIFICATION(pos_sub_res_test05, + tester() + .simplifyWith({ clause({ ~p(f(x1)), q(x1) }) }) + .toSimplify({ clause({ ~p2(x2, x5), q(x2), p(f(x2)), ~q(g(x5)) }) }) + .expected({ clause({ ~p2(x2, x5), q(x2), ~q(g(x5)) }) }) +) + +// TODO I'm assuming these give different results for forwards and backwards, so they cannot be enabled +// TEST_SIMPLIFICATION(pos_sub_res_test06, +// tester() +// .simplifyWith({ clause({ p(f2(y7, x6)), p2(y7, x6) }) }) +// .toSimplify({ clause({ p2(f(g(x5)), y4), ~p(f2(f(g(x5)), y4)), ~p2(f2(f(g(x5)), y4), x5) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// TEST_SIMPLIFICATION(pos_sub_res_test07, +// tester() +// .simplifyWith({ clause({ p(f2(y7, x6)), p2(y7, x6) }) }) +// .toSimplify({ clause({ p2(f(g(x5)), y4), ~p(f2(f(g(x5)), y4)), ~p2(f2(f(g(x5)), y4), x5) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// TEST_SIMPLIFICATION(pos_sub_res_test08, +// tester() +// .simplifyWith({ clause({ ~p2(y7, d) }) }) +// .toSimplify({ clause({ ~p(x6), ~p(x5), ~p2(f(f2(f2(x5, x5), f2(x5, x6))), x6), p2(f2(f2(x5, x5), f2(x5, x6)), d) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// TEST_SIMPLIFICATION(pos_sub_res_test09, +// tester() +// .simplifyWith({ clause({ ~p3(d, y7, d), ~p3(y7, e, c) }) }) +// .toSimplify({ clause({ p3(d, x6, d), ~p3(x6, e, c) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// TEST_SIMPLIFICATION(pos_sub_res_test10, +// tester() +// .simplifyWith({ clause({ p2(y7, x6), f2(y7, x6) == f2(f3(x5, y4, x4), x4), p2(y4, x4) }) }) +// .toSimplify({ clause({ ~p2(g2(h2(y3, x2), x2), x7), f2(g2(h2(y3, x2), x2), x7) == f2(f3(y6, g2(h2(y3, x2), x2), x7), x7) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// TEST_SIMPLIFICATION(pos_sub_res_test11, +// tester() +// .simplifyWith({ clause({ p2(y7, x6), ~q2(x5, x6), ~p2(y7, x5) }) }) +// .toSimplify({ clause({ p2(f2(y4, x6), y4), ~p2(x6, y7), ~r2(y4, y7), ~p2(x6, d), ~q2(y4, d), ~q2(y7, d) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// TEST_SIMPLIFICATION(pos_sub_res_test12, +// tester() +// .simplifyWith({ clause({ p(d) }) }) +// .toSimplify({ clause({ q(d), ~p(d) }) }) +// .expected({ /* nothing */ }) +// .justifications({ /* nothing */ }) +// ) + +// negative subsumption resolutions + +TEST_SIMPLIFICATION(neg_sub_res_test01, + tester() + .simplifyWith({ clause({ ~p(x1), q(x1) }) }) + .toSimplify({ clause({ p(c), q(d), r(e) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test02, + tester() + .simplifyWith({ clause({ ~p(x1), ~q(x2) }) }) + .toSimplify({ clause({ p(c), q(d), r(e) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test03, + tester() + .simplifyWith({ clause({ ~p(x1), r(c) }) }) + .toSimplify({ clause({ p(c), q(d), r(e) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test04, + tester() + .simplifyWith({ clause({ ~p(x1), p2(x1, x2) }) }) + .toSimplify({ clause({ p(c), q(d), r(e) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test05, + tester() + .simplifyWith({ clause({ p3(x1, x2, x2), ~p3(x2, c, c) }) }) + .toSimplify({ clause({ p3(y1, c, c), ~p3(y1, y2, y2) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test06, + tester() + .simplifyWith({ clause({ p3(y7, x6, x6), ~p3(y7, d, d) }) }) + .toSimplify({ clause({ p3(x5, d, d), ~p3(x5, x6, x6) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test07, + tester() + .simplifyWith({ clause({ ~p3(y7, d, d), p3(y7, x6, x6) }) }) + .toSimplify({ clause({ ~p3(x5, y4, f(f2(x4, f(y3)))), p3(x2, d, d), ~p3(x7, x4, y3), ~p3(x2, f2(x5, y4), x7) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test08, + tester() + .simplifyWith({ clause({ ~p3(y7, d, d), p3(y7, x6, x6) }) }) + .toSimplify({ clause({ ~p3(x5, x6, x6), p3(d, d, x5) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test09, + tester() + .simplifyWith({ clause({ ~p3(d, y7, d), p3(x6, y7, x6) }) }) + .toSimplify({ clause({ p3(d, x5, d), ~p3(y4, f(y4), f(x5)) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test10, + tester() + .simplifyWith({ clause({ ~p3(d, d, d), p3(f(f(y7)), d, y7) }) }) + .toSimplify({ clause({ p3(d, x6, x6) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test11, + tester() + .simplifyWith({ clause({ p2(y7, d), p2(e, y7), e == y7 }) }) + .toSimplify({ clause({ ~p2(x6, x5), ~p2(y7, x6), p2(y7, x5) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +TEST_SIMPLIFICATION(neg_sub_res_test12, + tester() + .simplifyWith({ clause({ f2(y1, y3) == x1, ~p2(g2(x1, f2(y1, y3)), x1), ~p2(g2(x1, f2(y1, y3)), y1), ~p2(g2(x1, f2(y1, y3)), y3) }) }) + .toSimplify({ clause({ p2(g2(x2, f2(y1, y3)), x2), f2(y1, y3) == x2, p2(g2(x2, f2(y1, y3)), y3) }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +} diff --git a/UnitTests/tInferences_SubsumptionDemodulation.cpp b/UnitTests/tInferences_SubsumptionDemodulation.cpp new file mode 100644 index 000000000..1022bc2f1 --- /dev/null +++ b/UnitTests/tInferences_SubsumptionDemodulation.cpp @@ -0,0 +1,53 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ + +#include "Test/SyntaxSugar.hpp" +#include "Inferences/ForwardSubsumptionDemodulation.hpp" +#include "Inferences/BackwardSubsumptionDemodulation.hpp" + +#include "Test/FwdBwdSimplificationTester.hpp" + +using namespace std; +using namespace Kernel; +using namespace Inferences; +using namespace Test; + +/** + * NECESSARY: We need to tell the tester which syntax sugar to import for creating terms & clauses. + * See Test/SyntaxSugar.hpp for which kinds of syntax sugar are available + */ +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_VAR(u, 3) \ + DECL_SORT(s) \ + DECL_FUNC(f, {s, s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_PRED (p, {s}) \ + DECL_PRED (q, {s}) \ + +namespace SubsumptionDemodulationTester { + +inline auto tester() { + return FwdBwdSimplification::TestCase() + .fwd(new ForwardSubsumptionDemodulation(/*doSubsumption=*/false, /*enableOrderingOptimizations=*/true)) + .bwd(new BackwardSubsumptionDemodulation(/*enableOrderingOptimizations=*/true)); +} + +// subsumption demodulation with preordered equation +TEST_SIMPLIFICATION(test01, + tester() + .simplifyWith({ clause({ f(x,y) == x, g(x) != a }) }) + .toSimplify({ clause({ ~p(f(a,b)), g(a) != a }) }) + .expected({ clause({ ~p(a), g(a) != a }) }) +) + +} diff --git a/cmake/sources.cmake b/cmake/sources.cmake index 4566e4040..2e5862315 100644 --- a/cmake/sources.cmake +++ b/cmake/sources.cmake @@ -55,6 +55,7 @@ set(UNIT_TESTS UnitTests/tIndexManager.cpp UnitTests/tInferences_ArithmeticSubtermGeneralization.cpp UnitTests/tInferences_BinaryResolution.cpp + UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp UnitTests/tInferences_Demodulation.cpp UnitTests/tInferences_EqualityResolution.cpp UnitTests/tInferences_Factoring.cpp @@ -64,6 +65,8 @@ set(UNIT_TESTS UnitTests/tInferences_Induction.cpp UnitTests/tInferences_InferenceEngine.cpp UnitTests/tInferences_PushUnaryMinus.cpp + UnitTests/tInferences_SubsumptionDemodulation.cpp + UnitTests/tInferences_SubsumptionAndResolution.cpp UnitTests/tInferences_Superposition.cpp UnitTests/tInferences_TautologyDeletionISE.cpp UnitTests/tIntegerConstantType.cpp From bf48e1aab9e7ab6727cf9cd3fabc936fef990afc Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Wed, 14 Jan 2026 13:08:32 +0100 Subject: [PATCH 07/13] Delete simplification rules after test --- Test/FwdBwdSimplificationTester.hpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Test/FwdBwdSimplificationTester.hpp b/Test/FwdBwdSimplificationTester.hpp index 93b429366..603c83dce 100644 --- a/Test/FwdBwdSimplificationTester.hpp +++ b/Test/FwdBwdSimplificationTester.hpp @@ -192,7 +192,14 @@ class TestCase void run() { runFwd(); + if (fwd().isSome()) { + delete fwd().unwrap(); + } + runBwd(); + if (bwd().isSome()) { + delete bwd().unwrap(); + } } template From b78d9541c0b0517be75ffe129981822acb3e6f50 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Wed, 14 Jan 2026 15:56:51 +0100 Subject: [PATCH 08/13] Add some URResolution tests Add more unit tests Add more tests Add more BR tests Add more tests Add back missing initial value in URResolution --- Inferences/EqualityFactoring.cpp | 5 +- Inferences/EqualityFactoring.hpp | 4 +- Inferences/InnerRewriting.cpp | 22 ++--- Inferences/InnerRewriting.hpp | 10 ++- Inferences/URResolution.cpp | 5 +- Inferences/URResolution.hpp | 4 +- Saturation/SaturationAlgorithm.cpp | 16 ++-- Test/FwdBwdSimplificationTester.hpp | 17 ---- ...> tInferences_AnswerLiteralProcessors.cpp} | 0 UnitTests/tInferences_BinaryResolution.cpp | 28 +++++- ...ences_CodeTreeSubsumptionAndResolution.cpp | 2 +- UnitTests/tInferences_Condensation.cpp | 60 +++++++++++++ UnitTests/tInferences_Demodulation.cpp | 2 +- UnitTests/tInferences_EqualityFactoring.cpp | 45 ++++++++++ UnitTests/tInferences_FastCondensation.cpp | 60 +++++++++++++ ...Inferences_FunctionDefinitionRewriting.cpp | 2 +- UnitTests/tInferences_InferenceEngine.cpp | 30 ++++--- UnitTests/tInferences_InnerRewriting.cpp | 88 +++++++++++++++++++ .../tInferences_SubsumptionDemodulation.cpp | 44 ++++++++++ UnitTests/tInferences_URResolution.cpp | 80 +++++++++++++++++ cmake/sources.cmake | 7 +- 21 files changed, 464 insertions(+), 67 deletions(-) rename UnitTests/{tAnswerLiteralProcessors_Synthesis.cpp => tInferences_AnswerLiteralProcessors.cpp} (100%) create mode 100644 UnitTests/tInferences_Condensation.cpp create mode 100644 UnitTests/tInferences_EqualityFactoring.cpp create mode 100644 UnitTests/tInferences_FastCondensation.cpp create mode 100644 UnitTests/tInferences_InnerRewriting.cpp create mode 100644 UnitTests/tInferences_URResolution.cpp diff --git a/Inferences/EqualityFactoring.cpp b/Inferences/EqualityFactoring.cpp index df6843e3a..c222450ec 100644 --- a/Inferences/EqualityFactoring.cpp +++ b/Inferences/EqualityFactoring.cpp @@ -40,9 +40,8 @@ using namespace Indexing; using namespace Saturation; using std::pair; -EqualityFactoring::EqualityFactoring() - : _abstractionOracle(AbstractionOracle::createOnlyHigherOrder()) - , _uwaFixedPointIteration(env.options->unificationWithAbstractionFixedPointIteration()) +EqualityFactoring::EqualityFactoring(Options::UnificationWithAbstraction uwa, bool uwaFixedPointIteration) + : _abstractionOracle(uwa), _uwaFixedPointIteration(uwaFixedPointIteration) { } diff --git a/Inferences/EqualityFactoring.hpp b/Inferences/EqualityFactoring.hpp index bf10d3748..c411f2d7a 100644 --- a/Inferences/EqualityFactoring.hpp +++ b/Inferences/EqualityFactoring.hpp @@ -18,6 +18,8 @@ #include "Forwards.hpp" +#include "Kernel/UnificationWithAbstraction.hpp" + #include "InferenceEngine.hpp" #include "ProofExtra.hpp" @@ -31,7 +33,7 @@ class EqualityFactoring : public GeneratingInferenceEngine { public: - EqualityFactoring(); + EqualityFactoring(Options::UnificationWithAbstraction uwa, bool uwaFixedPointIteration); ClauseIterator generateClauses(Clause* premise) override; private: struct IsPositiveEqualityFn; diff --git a/Inferences/InnerRewriting.cpp b/Inferences/InnerRewriting.cpp index 3d6751ee9..94405a885 100644 --- a/Inferences/InnerRewriting.cpp +++ b/Inferences/InnerRewriting.cpp @@ -15,25 +15,23 @@ #include "InnerRewriting.hpp" #include "Kernel/EqHelper.hpp" -#include "Kernel/Inference.hpp" - -#include "Saturation/SaturationAlgorithm.hpp" +#include "Kernel/Clause.hpp" +#include "Lib/Environment.hpp" +#include "Shell/Statistics.hpp" namespace Inferences { using namespace Lib; using namespace Kernel; -bool InnerRewriting::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) +Clause* InnerRewriting::simplify(Clause* cl) { - Ordering& ordering = _salg->getOrdering(); - // look for the first equality which rewrites something and rewrite everything with it (check for EqTaut as you go) unsigned len = cl->length(); for (unsigned i = 0; i < len; i++) { Literal* rwLit=(*cl)[i]; TermList lhs, rhs; - if (rwLit->isEquality() && rwLit->isNegative() && EqHelper::hasGreaterEqualitySide(rwLit,ordering,lhs,rhs)) { + if (rwLit->isEquality() && rwLit->isNegative() && EqHelper::hasGreaterEqualitySide(rwLit,_ord,lhs,rhs)) { for (unsigned j = 0; j < len; j++) { if (i != j) { Literal* lit = (*cl)[j]; @@ -41,7 +39,7 @@ bool InnerRewriting::perform(Clause* cl, Clause*& replacement, ClauseIterator& p if (nLit != lit) { if(EqHelper::isEqTautology(nLit)) { env.statistics->innerRewritesToEqTaut++; - return true; + return nullptr; } RStack resLits; @@ -58,22 +56,20 @@ bool InnerRewriting::perform(Clause* cl, Clause*& replacement, ClauseIterator& p Literal* rLit = EqHelper::replace(oLit,lhs,rhs); if(EqHelper::isEqTautology(rLit)) { env.statistics->innerRewritesToEqTaut++; - return true; + return nullptr; } resLits->push(rLit); } } - replacement = Clause::fromStack(*resLits,SimplifyingInference1(InferenceRule::INNER_REWRITING, cl)); - return true; + return Clause::fromStack(*resLits,SimplifyingInference1(InferenceRule::INNER_REWRITING, cl)); } } } } } - return false; + return cl; } - } diff --git a/Inferences/InnerRewriting.hpp b/Inferences/InnerRewriting.hpp index 6eca83394..5e44e01e3 100644 --- a/Inferences/InnerRewriting.hpp +++ b/Inferences/InnerRewriting.hpp @@ -25,11 +25,17 @@ namespace Inferences using namespace Kernel; using namespace Saturation; +// TODO this should be an immediate simplification class InnerRewriting -: public ForwardSimplificationEngine +: public ImmediateSimplificationEngine { public: - bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override; + InnerRewriting(const Ordering& ord) : _ord(ord) {} + + Clause* simplify(Clause* cl) override; + +private: + const Ordering& _ord; }; }; diff --git a/Inferences/URResolution.cpp b/Inferences/URResolution.cpp index ed71bbf1b..6d18085c0 100644 --- a/Inferences/URResolution.cpp +++ b/Inferences/URResolution.cpp @@ -39,10 +39,6 @@ using namespace Kernel; using namespace Indexing; using namespace Saturation; -template -URResolution::URResolution(bool full) -: _full(full), _selectedOnly(false) {} - template void URResolution::attach(SaturationAlgorithm* salg) { @@ -53,6 +49,7 @@ void URResolution::attach(SaturationAlgorithm* salg) Options::URResolution optSetting = _salg->getOptions().unitResultingResolution(); ASS_NEQ(optSetting, Options::URResolution::OFF); + _full = optSetting==Options::URResolution::FULL; _emptyClauseOnly = optSetting==Options::URResolution::EC_ONLY; } diff --git a/Inferences/URResolution.hpp b/Inferences/URResolution.hpp index 3bc5a22bf..45cc10e3b 100644 --- a/Inferences/URResolution.hpp +++ b/Inferences/URResolution.hpp @@ -32,8 +32,6 @@ class URResolution : public GeneratingInferenceEngine { public: - URResolution(bool full); - void attach(SaturationAlgorithm* salg) override; void detach() override; @@ -51,7 +49,7 @@ class URResolution bool _full; bool _emptyClauseOnly; - bool _selectedOnly; + bool _selectedOnly = false; using UnitIndexType = std::conditional_t; using NonUnitIndexType = std::conditional_t; std::shared_ptr _unitIndex; diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp index 8b5e39c1e..23e798cc8 100644 --- a/Saturation/SaturationAlgorithm.cpp +++ b/Saturation/SaturationAlgorithm.cpp @@ -1465,7 +1465,7 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const if (mayHaveEquality) { if (!alascaTakesOver) { // in alasca we have a special equality factoring rule - gie->addFront(new EqualityFactoring()); + gie->addFront(new EqualityFactoring(AbstractionOracle::createOnlyHigherOrder(), opt.unificationWithAbstractionFixedPointIteration())); } gie->addFront(new EqualityResolution()); if(env.options->superposition() && !alascaTakesOver){ // in alasca we have a special superposition rule @@ -1486,9 +1486,9 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const } if (opt.unitResultingResolution() != Options::URResolution::OFF) { if (env.options->questionAnswering() == Options::QuestionAnsweringMode::SYNTHESIS) { - gie->addFront(new URResolution(opt.unitResultingResolution() == Options::URResolution::FULL)); + gie->addFront(new URResolution()); } else { - gie->addFront(new URResolution(opt.unitResultingResolution() == Options::URResolution::FULL)); + gie->addFront(new URResolution()); } } if (opt.extensionalityResolution() != Options::ExtensionalityResolution::OFF) { @@ -1611,9 +1611,6 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const // create simplification engine // create forward simplification engine - if (mayHaveEquality && opt.innerRewriting()) { - res->addForwardSimplifierToFront(new InnerRewriting()); - } if (opt.globalSubsumption()) { res->addForwardSimplifierToFront(new GlobalSubsumption(opt)); } @@ -1803,5 +1800,12 @@ std::pair SaturationAlgorithm::createISE(Proble // Note: SynthesisAnswerLiteralProcessor must be THE LAST added simplification-many rule. resMany.addFront(std::make_unique()); } + + // This was earlier at the beginning of forward simplifications, + // so let's put it for now to the end of immediate simplifications + if (mayHaveEquality && opt.innerRewriting()) { + res->addFront(new InnerRewriting(ordering)); + } + return std::make_pair(res, std::move(resMany)); } diff --git a/Test/FwdBwdSimplificationTester.hpp b/Test/FwdBwdSimplificationTester.hpp index 603c83dce..9ae235a60 100644 --- a/Test/FwdBwdSimplificationTester.hpp +++ b/Test/FwdBwdSimplificationTester.hpp @@ -30,23 +30,6 @@ namespace Test { namespace FwdBwdSimplification { -class TestCase; - -template -class FwdBwdSimplificationTester -{ - Rule _rule; - -public: - FwdBwdSimplificationTester(Rule rule) - : _rule(std::move(rule)) - { } - - virtual bool eq(Kernel::Clause* lhs, Kernel::Clause* rhs) const - { return TestUtils::eqModAC(lhs, rhs); } - - friend class TestCase; -}; class TestCase { diff --git a/UnitTests/tAnswerLiteralProcessors_Synthesis.cpp b/UnitTests/tInferences_AnswerLiteralProcessors.cpp similarity index 100% rename from UnitTests/tAnswerLiteralProcessors_Synthesis.cpp rename to UnitTests/tInferences_AnswerLiteralProcessors.cpp diff --git a/UnitTests/tInferences_BinaryResolution.cpp b/UnitTests/tInferences_BinaryResolution.cpp index cde45898b..c4255b389 100644 --- a/UnitTests/tInferences_BinaryResolution.cpp +++ b/UnitTests/tInferences_BinaryResolution.cpp @@ -33,7 +33,7 @@ using namespace Test; REGISTER_GEN_TESTER(Generation::GenerationTester(BinaryResolution())) // binary resolution with selected literals -TEST_GENERATION(test_01, +TEST_GENERATION(test01, Generation::SymmetricTest() .inputs({ clause({ selected(p(x)), f(x,y) == x }), @@ -43,7 +43,7 @@ TEST_GENERATION(test_01, ) // no binary resolution with equalities -TEST_GENERATION(test_02, +TEST_GENERATION(test02, Generation::SymmetricTest() .inputs({ clause({ selected(g(x) == x), f(x,y) == x }), @@ -51,3 +51,27 @@ TEST_GENERATION(test_02, }) .expected(none()) ) + +// no resolution due to maximality check in left premise +TEST_GENERATION(test03, + Generation::SymmetricTest() + .inputs({ + clause({ selected(p(f(x,b))), selected(p(f(b,x))) }), + clause({ selected(~p(f(a,x))), ~q(x) }) + }) + // sadly the default is based on frequency which changes in + // the second round due to sharing + .options({ { "symbol_precedence", "occurrence" }}) + .expected(none()) + ) + +// no resolution due to maximality check in right premise +TEST_GENERATION(test04, + Generation::SymmetricTest() + .inputs({ + clause({ selected(p(f(x,b))), ~q(x) }), + clause({ selected(~p(f(a,x))), selected(p(f(x,a))) }) + }) + .options({ { "symbol_precedence", "occurrence" }}) + .expected(none()) + ) diff --git a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp index 1f81c9769..d630a2e06 100644 --- a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp +++ b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp @@ -58,7 +58,7 @@ using namespace Test; DECL_PRED(r2, {s, s}) \ ) -namespace CodeTreeForwardSubsumptionAndResolutionTest { +namespace { inline auto tester() { return FwdBwdSimplification::TestCase() diff --git a/UnitTests/tInferences_Condensation.cpp b/UnitTests/tInferences_Condensation.cpp new file mode 100644 index 000000000..54d3bfe9c --- /dev/null +++ b/UnitTests/tInferences_Condensation.cpp @@ -0,0 +1,60 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ +#include "Test/SyntaxSugar.hpp" +#include "Inferences/Condensation.hpp" + +#include "Test/SimplificationTester.hpp" + +using namespace Test; + +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_SORT(s) \ + DECL_FUNC(f, {s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_PRED (p, {s}) \ + DECL_PRED (q, {s}) + +REGISTER_SIMPL_TESTER(Simplification::RuleSimplificationTester) + +// nothing happens with one literal +TEST_SIMPLIFY(test01, + Simplification::NotApplicable() + .input(clause({ f(x) == a })) + ) + +// condensation happens with two literals +TEST_SIMPLIFY(test02, + Simplification::Success() + .input(clause({ f(g(x)) == a, f(y) == a })) + .expected(clause({ f(g(x)) == a })) + ) + +// condensation happens between first two literals found +TEST_SIMPLIFY(test03, + Simplification::Success() + .input(clause({ ~p(g(f(x))), q(x), ~p(y), ~p(g(z)), g(x) != x })) + .expected(clause({ ~p(g(f(x))), q(x), ~p(g(y)), g(x) != x })) + ) + +// condensation does not happen due to some literal that needs to be instantiated +TEST_SIMPLIFY(test04, + Simplification::NotApplicable() + .input(clause({ ~p(f(x)), ~p(y), q(y) })) + ) + +// condensation happens but not with first two literals due to some literal that would need to be instantiated +TEST_SIMPLIFY(test05, + Simplification::Success() + .input(clause({ ~p(g(f(x))), ~p(g(y)), ~p(z), q(y) })) + .expected(clause({ ~p(g(f(x))), ~p(g(y)), q(y) })) + ) diff --git a/UnitTests/tInferences_Demodulation.cpp b/UnitTests/tInferences_Demodulation.cpp index 143d7f930..30144dd3d 100644 --- a/UnitTests/tInferences_Demodulation.cpp +++ b/UnitTests/tInferences_Demodulation.cpp @@ -36,7 +36,7 @@ using namespace Test; DECL_PRED (p, {s}) \ DECL_PRED (q, {s}) -namespace DemodulationTester { +namespace { inline auto tester() { return FwdBwdSimplification::TestCase() diff --git a/UnitTests/tInferences_EqualityFactoring.cpp b/UnitTests/tInferences_EqualityFactoring.cpp new file mode 100644 index 000000000..d0f865269 --- /dev/null +++ b/UnitTests/tInferences_EqualityFactoring.cpp @@ -0,0 +1,45 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ + +#include "Test/SyntaxSugar.hpp" +#include "Test/GenerationTester.hpp" + +#include "Inferences/EqualityFactoring.hpp" + +using namespace Test; + +REGISTER_GEN_TESTER(Test::Generation::GenerationTester(EqualityFactoring(Options::UnificationWithAbstraction::OFF, /*uwaFixedPointIteration=*/false))) + +/** + * NECESSARY: We need to tell the tester which syntax sugar to import for creating terms & clauses. + * See Test/SyntaxSugar.hpp for which kinds of syntax sugar are available + */ +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_SORT(s) \ + DECL_FUNC(f, {s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_PRED (p, {s}) + +// inferences is performed +TEST_GENERATION(test01, + Generation::AsymmetricTest() + .input( clause({ selected(f(f(x)) == x), f(y) == y, g(x) == x, p(y) })) + .expected({ clause({ f(f(x)) == f(x), f(x) != x, g(x) == x, p(f(x)) }) }) + ) + +// not performed because on of the literal is not selected +TEST_GENERATION(test02, + Generation::AsymmetricTest() + .input( clause({ f(f(x)) == x, f(y) == y, selected(g(x) == x), p(y) })) + .expected(none()) + ) diff --git a/UnitTests/tInferences_FastCondensation.cpp b/UnitTests/tInferences_FastCondensation.cpp new file mode 100644 index 000000000..54d3bfe9c --- /dev/null +++ b/UnitTests/tInferences_FastCondensation.cpp @@ -0,0 +1,60 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ +#include "Test/SyntaxSugar.hpp" +#include "Inferences/Condensation.hpp" + +#include "Test/SimplificationTester.hpp" + +using namespace Test; + +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_SORT(s) \ + DECL_FUNC(f, {s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_PRED (p, {s}) \ + DECL_PRED (q, {s}) + +REGISTER_SIMPL_TESTER(Simplification::RuleSimplificationTester) + +// nothing happens with one literal +TEST_SIMPLIFY(test01, + Simplification::NotApplicable() + .input(clause({ f(x) == a })) + ) + +// condensation happens with two literals +TEST_SIMPLIFY(test02, + Simplification::Success() + .input(clause({ f(g(x)) == a, f(y) == a })) + .expected(clause({ f(g(x)) == a })) + ) + +// condensation happens between first two literals found +TEST_SIMPLIFY(test03, + Simplification::Success() + .input(clause({ ~p(g(f(x))), q(x), ~p(y), ~p(g(z)), g(x) != x })) + .expected(clause({ ~p(g(f(x))), q(x), ~p(g(y)), g(x) != x })) + ) + +// condensation does not happen due to some literal that needs to be instantiated +TEST_SIMPLIFY(test04, + Simplification::NotApplicable() + .input(clause({ ~p(f(x)), ~p(y), q(y) })) + ) + +// condensation happens but not with first two literals due to some literal that would need to be instantiated +TEST_SIMPLIFY(test05, + Simplification::Success() + .input(clause({ ~p(g(f(x))), ~p(g(y)), ~p(z), q(y) })) + .expected(clause({ ~p(g(f(x))), ~p(g(y)), q(y) })) + ) diff --git a/UnitTests/tInferences_FunctionDefinitionRewriting.cpp b/UnitTests/tInferences_FunctionDefinitionRewriting.cpp index 713d56c51..b11216db1 100644 --- a/UnitTests/tInferences_FunctionDefinitionRewriting.cpp +++ b/UnitTests/tInferences_FunctionDefinitionRewriting.cpp @@ -19,7 +19,7 @@ using namespace Test; REGISTER_GEN_TESTER(Generation::GenerationTester(FunctionDefinitionRewriting())) -namespace FunctionDefinitionRewritingTest { +namespace { /** * NECESSARY: We need to tell the tester which syntax sugar to import for creating terms & clauses. diff --git a/UnitTests/tInferences_InferenceEngine.cpp b/UnitTests/tInferences_InferenceEngine.cpp index fe5548d9e..19b647bc4 100644 --- a/UnitTests/tInferences_InferenceEngine.cpp +++ b/UnitTests/tInferences_InferenceEngine.cpp @@ -7,6 +7,7 @@ * https://vprover.github.io/license.html * and in the source directory */ +#include "Kernel/Clause.hpp" #include "Test/SyntaxSugar.hpp" #include "Inferences/InferenceEngine.hpp" @@ -29,9 +30,8 @@ namespace DuplicateLiteralRemovalISETest { REGISTER_SIMPL_TESTER(Simplification::RuleSimplificationTester) TEST_SIMPLIFY(dlr_test01, - Simplification::Success() + Simplification::NotApplicable() .input(clause({ p(a) })) - .expected(clause({ p(a) })) ) TEST_SIMPLIFY(dlr_test02, @@ -41,15 +41,13 @@ TEST_SIMPLIFY(dlr_test02, ) TEST_SIMPLIFY(dlr_test03, - Simplification::Success() + Simplification::NotApplicable() .input(clause({ p(a), q(b) })) - .expected(clause({ p(a), q(b) })) ) TEST_SIMPLIFY(dlr_test04, - Simplification::Success() + Simplification::NotApplicable() .input(clause({ p(x), p(y) })) - .expected(clause({ p(x), p(y) })) ) TEST_SIMPLIFY(dlr_test05, @@ -63,6 +61,17 @@ TEST_SIMPLIFY(dlr_test06, .input(clause({ p(a), ~p(a), ~p(a), p(a), q(b) })) .expected(clause({ p(a), ~p(a), q(b) })) ) + +TEST_SIMPLIFY(dlr_test07, + Simplification::NotApplicable() + .input(clause({ p(a), f(x,y) == x, q(b) })) + ) + +TEST_SIMPLIFY(dlr_test08, + Simplification::Success() + .input(clause({ f(x,y) == x, f(x,y) == x, q(b) })) + .expected((clause({ f(x,y) == x, q(b) }))) + ) } namespace TrivialInequalitiesRemovalISETest { @@ -70,21 +79,18 @@ namespace TrivialInequalitiesRemovalISETest { REGISTER_SIMPL_TESTER(Simplification::RuleSimplificationTester) TEST_SIMPLIFY(tir_test01, - Simplification::Success() + Simplification::NotApplicable() .input(clause({ a == b })) - .expected(clause({ a == b })) ) TEST_SIMPLIFY(tir_test02, - Simplification::Success() + Simplification::NotApplicable() .input(clause({ a != b })) - .expected(clause({ a != b })) ) TEST_SIMPLIFY(tir_test03, - Simplification::Success() + Simplification::NotApplicable() .input(clause({ a == a })) - .expected(clause({ a == a })) ) TEST_SIMPLIFY(tir_test04, diff --git a/UnitTests/tInferences_InnerRewriting.cpp b/UnitTests/tInferences_InnerRewriting.cpp new file mode 100644 index 000000000..024aab7fa --- /dev/null +++ b/UnitTests/tInferences_InnerRewriting.cpp @@ -0,0 +1,88 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ + +#include "Test/SyntaxSugar.hpp" +#include "Inferences/InnerRewriting.hpp" +#include "Kernel/KBO.hpp" + +#include "Test/SimplificationTester.hpp" + +using namespace std; +using namespace Kernel; +using namespace Inferences; +using namespace Test; + +/** + * NECESSARY: We need to tell the tester which syntax sugar to import for creating terms & clauses. + * See Test/SyntaxSugar.hpp for which kinds of syntax sugar are available + */ +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_VAR(u, 3) \ + DECL_SORT(s) \ + DECL_LEFT_FUNC(left, {s}, s) \ + DECL_RIGHT_FUNC(right, {s}, s) \ + DECL_FUNC(f, {s, s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_PRED (p, {s}) \ + DECL_PRED (q, {s}) + + +class InnerRewritingTester + : public Simplification::SimplificationTester +{ + KBO _kbo; + InnerRewriting _rule; +public: + InnerRewritingTester() + : _kbo(KBO::testKBO(/*rand=*/false, /*qkbo=*/false)), _rule(_kbo) {} + + Kernel::Clause* simplify(Kernel::Clause* cl) override { + return _rule.simplify(cl); + } +}; + +REGISTER_SIMPL_TESTER(InnerRewritingTester) + +// inner rewriting with preordered equation +TEST_SIMPLIFY(test01, + Simplification::Success() + .input(clause({ ~p(f(x,y)), f(x,y) != x, q(y) })) + .expected(clause({ ~p(x), f(x,y) != x, q(y) })) + ) + +// inner rewriting fails with postordered equation +TEST_SIMPLIFY(test02, + Simplification::NotApplicable() + .input(clause({ ~p(f(x,y)), f(x,y) == f(y,x) })) +) + +// inner rewriting not performed with positive equations +TEST_SIMPLIFY(test03, + Simplification::Success() + .input(clause({ ~p(f(x,y)), f(x,y) == x })) + .expected(clause({ ~p(f(x,y)), f(x,y) == x })) + ) + +// inner rewriting to tautology +TEST_SIMPLIFY(test04, + Simplification::Success() + .input(clause({ g(f(x,y)) == g(x), f(x,y) != x })) + .expected(Simplification::Redundant{}) + ) + +// inner rewriting to tautology after rewriting a non-tautological literal +TEST_SIMPLIFY(test05, + Simplification::Success() + .input(clause({ q(z), p(f(x,y)), g(f(x,y)) == g(x), f(x,y) != x })) + .expected(Simplification::Redundant{}) + ) diff --git a/UnitTests/tInferences_SubsumptionDemodulation.cpp b/UnitTests/tInferences_SubsumptionDemodulation.cpp index 1022bc2f1..ae460df8e 100644 --- a/UnitTests/tInferences_SubsumptionDemodulation.cpp +++ b/UnitTests/tInferences_SubsumptionDemodulation.cpp @@ -50,4 +50,48 @@ TEST_SIMPLIFICATION(test01, .expected({ clause({ ~p(a), g(a) != a }) }) ) +// subsumption demodulation does not happen due to too many literals in simplifierwith preordered equation +TEST_SIMPLIFICATION(test02, + tester() + .simplifyWith({ clause({ f(x,y) == x, g(x) != a, q(a) }) }) + .toSimplify({ clause({ ~p(f(a,b)), g(a) != a }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +// subsumption demodulation does not happen due to unorientable equation +TEST_SIMPLIFICATION(test03, + tester() + .simplifyWith({ clause({ f(x,x) == g(y), g(x) != a }) }) + .toSimplify({ clause({ ~p(f(a,b)), g(a) != a }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +// subsumption demodulation does not happen due to post-ordering check +TEST_SIMPLIFICATION(test04, + tester() + .simplifyWith({ clause({ f(x,y) == f(y,x), g(x) != y }) }) + .toSimplify({ clause({ ~p(f(a,b)), g(a) != b }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +// subsumption demodulation does not happen due to the rewriting instance being larger than the rewritten clause +TEST_SIMPLIFICATION(test05, + tester() + .simplifyWith({ clause({ f(x,y) == f(y,x), g(x) != y }) }) + .toSimplify({ clause({ f(a,b) == a, g(a) != b }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + +// subsumption demodulation happens because we rewrite the second largest term in clause +TEST_SIMPLIFICATION(test06, + tester() + .simplifyWith({ clause({ f(x,y) == g(y), g(x) != y }) }) + .toSimplify({ clause({ f(a,b) == g(g(g(b))), g(a) != b }) }) + .expected({ clause({ g(b) == g(g(g(b))), g(a) != b }) }) +) + } diff --git a/UnitTests/tInferences_URResolution.cpp b/UnitTests/tInferences_URResolution.cpp new file mode 100644 index 000000000..6419b9f9c --- /dev/null +++ b/UnitTests/tInferences_URResolution.cpp @@ -0,0 +1,80 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ + +#include "Test/SyntaxSugar.hpp" +#include "Test/GenerationTester.hpp" + +#include "Inferences/URResolution.hpp" + +using namespace Test; + +/** + * NECESSARY: We need to tell the tester which syntax sugar to import for creating terms & clauses. + * See Test/SyntaxSugar.hpp for which kinds of syntax sugar are available + */ +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_VAR(u, 3) \ + DECL_SORT(s) \ + DECL_FUNC(f, {s, s}, s) \ + DECL_FUNC(g, {s}, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_PRED (p, {s}) \ + DECL_PRED (q, {s}) \ + +REGISTER_GEN_TESTER(Generation::GenerationTester>(URResolution())) + +// simple resolution +TEST_GENERATION(test01, + Generation::SymmetricTest() + .inputs({ + clause({ p(x), f(x,y) == x }), + clause({ ~p(g(x)) }) + }) + .options({ { "unit_resulting_resolution", "full" } }) + .expected(exactly(clause({ f(g(x),y) == g(x) }))) + ) + +// no resolution due to result not being unit +TEST_GENERATION(test02, + Generation::SymmetricTest() + .inputs({ + clause({ p(x), f(x,y) == x }), + clause({ ~p(g(x)), ~q(x) }) + }) + .options({ { "unit_resulting_resolution", "full" } }) + .expected(none()) + ) + +// resolution with multiple clauses +TEST_GENERATION(test03, + Generation::SymmetricTest() + .inputs({ + clause({ f(g(a),b) != g(a) }), + clause({ p(x) }), + clause({ ~p(g(x)), ~q(x), f(x,y) == x }) + }) + .options({ { "unit_resulting_resolution", "full" } }) + .expected(exactly(clause({ ~q(g(a)) }))) + ) + +// resolution with multiple clauses resulting in empty clause +TEST_GENERATION(test04, + Generation::SymmetricTest() + .inputs({ + clause({ q(g(y)) }), + clause({ f(g(a),b) != g(a) }), + clause({ p(x) }), + clause({ ~p(g(x)), ~q(x), f(x,y) == x }) + }) + .options({ { "unit_resulting_resolution", "ec_only" } }) + .expected(exactly(clause({ }))) + ) diff --git a/cmake/sources.cmake b/cmake/sources.cmake index 2e5862315..e1f5f953b 100644 --- a/cmake/sources.cmake +++ b/cmake/sources.cmake @@ -41,7 +41,6 @@ set(UNIT_TESTS UnitTests/tALASCA_TermFactoring.cpp UnitTests/tALASCA_VIRAS.cpp UnitTests/tALASCA_VariableElimination.cpp - UnitTests/tAnswerLiteralProcessors_Synthesis.cpp UnitTests/tArithCompare.cpp UnitTests/tBinaryHeap.cpp UnitTests/tBottomUpEvaluation.cpp @@ -53,22 +52,28 @@ set(UNIT_TESTS UnitTests/tDynamicHeap.cpp UnitTests/tFunctionDefinitionHandler.cpp UnitTests/tIndexManager.cpp + UnitTests/tInferences_AnswerLiteralProcessors.cpp UnitTests/tInferences_ArithmeticSubtermGeneralization.cpp UnitTests/tInferences_BinaryResolution.cpp UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp + UnitTests/tInferences_Condensation.cpp UnitTests/tInferences_Demodulation.cpp + UnitTests/tInferences_EqualityFactoring.cpp UnitTests/tInferences_EqualityResolution.cpp UnitTests/tInferences_Factoring.cpp + UnitTests/tInferences_FastCondensation.cpp UnitTests/tInferences_ForwardGroundJoinability.cpp UnitTests/tInferences_FunctionDefinitionRewriting.cpp UnitTests/tInferences_GaussianVariableElimination.cpp UnitTests/tInferences_Induction.cpp UnitTests/tInferences_InferenceEngine.cpp + UnitTests/tInferences_InnerRewriting.cpp UnitTests/tInferences_PushUnaryMinus.cpp UnitTests/tInferences_SubsumptionDemodulation.cpp UnitTests/tInferences_SubsumptionAndResolution.cpp UnitTests/tInferences_Superposition.cpp UnitTests/tInferences_TautologyDeletionISE.cpp + UnitTests/tInferences_URResolution.cpp UnitTests/tIntegerConstantType.cpp UnitTests/tInterpretedFunctions.cpp UnitTests/tIterator.cpp From 8d012180b9fe6447f59bb993218bee8c018e3313 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Fri, 16 Jan 2026 16:04:57 +0100 Subject: [PATCH 09/13] Remove some unused stuff --- Test/GenerationTester.hpp | 22 +------ ...ences_CodeTreeSubsumptionAndResolution.cpp | 57 ------------------- .../tInferences_SubsumptionAndResolution.cpp | 57 ------------------- 3 files changed, 1 insertion(+), 135 deletions(-) diff --git a/Test/GenerationTester.hpp b/Test/GenerationTester.hpp index eb1072c35..67ae8a197 100644 --- a/Test/GenerationTester.hpp +++ b/Test/GenerationTester.hpp @@ -32,20 +32,6 @@ namespace Test { -#define TEST_FN_ASS_EQ(VAL1, VAL2) \ - [] (std::string& s1, std::string& s2) { \ - bool res = (VAL1 == VAL2); \ - if (!res) { \ - s1 = Int::toString(VAL1); \ - s1.append(" != "); \ - s1.append(Int::toString(VAL2)); \ - s2 = std::string(#VAL1); \ - s2.append(" == "); \ - s2.append(#VAL2); \ - } \ - return res; \ - } - namespace Generation { template class GenerationTester; @@ -104,8 +90,6 @@ class ExactlyStackMatcher { class TodoStackMatcher { public: - TodoStackMatcher() {} - template TodoStackMatcher mapClauses(F fun) const { return TodoStackMatcher(); } @@ -229,7 +213,6 @@ using OptionMap = Stack>; class AsymmetricTest { using Clause = Kernel::Clause; - using Condition = std::function; Option _rule; Clause* _input; Option _expected; @@ -238,8 +221,6 @@ class AsymmetricTest std::function _setup = [](SaturationAlgorithm&){}; bool _selfApplications; OptionMap _options; - Stack _preConditions; - Stack _postConditions; template void testFail(Is const& is, Expected const& expected) { @@ -285,8 +266,7 @@ class AsymmetricTest // init problem Problem p; - auto ul = UnitList::empty(); - UnitList::pushFromIterator(ClauseStack::Iterator(_context), ul); + auto ul = UnitList::fromIterator(ClauseStack::Iterator(_context)); p.addUnits(ul); env.setMainProblem(&p); diff --git a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp index d630a2e06..792c05d4f 100644 --- a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp +++ b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp @@ -221,63 +221,6 @@ TEST_SIMPLIFICATION(pos_sub_res_test05, .expected({ clause({ ~p2(x2, x5), q(x2), ~q(g(x5)) }) }) ) -// TODO I'm assuming these give different results for forwards and backwards, so they cannot be enabled -// TEST_SIMPLIFICATION(pos_sub_res_test06, -// tester() -// .simplifyWith({ clause({ p(f2(y7, x6)), p2(y7, x6) }) }) -// .toSimplify({ clause({ p2(f(g(x5)), y4), ~p(f2(f(g(x5)), y4)), ~p2(f2(f(g(x5)), y4), x5) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - -// TEST_SIMPLIFICATION(pos_sub_res_test07, -// tester() -// .simplifyWith({ clause({ p(f2(y7, x6)), p2(y7, x6) }) }) -// .toSimplify({ clause({ p2(f(g(x5)), y4), ~p(f2(f(g(x5)), y4)), ~p2(f2(f(g(x5)), y4), x5) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - -// TEST_SIMPLIFICATION(pos_sub_res_test08, -// tester() -// .simplifyWith({ clause({ ~p2(y7, d) }) }) -// .toSimplify({ clause({ ~p(x6), ~p(x5), ~p2(f(f2(f2(x5, x5), f2(x5, x6))), x6), p2(f2(f2(x5, x5), f2(x5, x6)), d) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - -// TEST_SIMPLIFICATION(pos_sub_res_test09, -// tester() -// .simplifyWith({ clause({ ~p3(d, y7, d), ~p3(y7, e, c) }) }) -// .toSimplify({ clause({ p3(d, x6, d), ~p3(x6, e, c) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - -// TEST_SIMPLIFICATION(pos_sub_res_test10, -// tester() -// .simplifyWith({ clause({ p2(y7, x6), f2(y7, x6) == f2(f3(x5, y4, x4), x4), p2(y4, x4) }) }) -// .toSimplify({ clause({ ~p2(g2(h2(y3, x2), x2), x7), f2(g2(h2(y3, x2), x2), x7) == f2(f3(y6, g2(h2(y3, x2), x2), x7), x7) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - -// TEST_SIMPLIFICATION(pos_sub_res_test11, -// tester() -// .simplifyWith({ clause({ p2(y7, x6), ~q2(x5, x6), ~p2(y7, x5) }) }) -// .toSimplify({ clause({ p2(f2(y4, x6), y4), ~p2(x6, y7), ~r2(y4, y7), ~p2(x6, d), ~q2(y4, d), ~q2(y7, d) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - -// TEST_SIMPLIFICATION(pos_sub_res_test12, -// tester() -// .simplifyWith({ clause({ p(d) }) }) -// .toSimplify({ clause({ q(d), ~p(d) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - // negative subsumption resolutions TEST_SIMPLIFICATION(neg_sub_res_test01, diff --git a/UnitTests/tInferences_SubsumptionAndResolution.cpp b/UnitTests/tInferences_SubsumptionAndResolution.cpp index 5dc2cfb66..6082e20f1 100644 --- a/UnitTests/tInferences_SubsumptionAndResolution.cpp +++ b/UnitTests/tInferences_SubsumptionAndResolution.cpp @@ -221,63 +221,6 @@ TEST_SIMPLIFICATION(pos_sub_res_test05, .expected({ clause({ ~p2(x2, x5), q(x2), ~q(g(x5)) }) }) ) -// TODO I'm assuming these give different results for forwards and backwards, so they cannot be enabled -// TEST_SIMPLIFICATION(pos_sub_res_test06, -// tester() -// .simplifyWith({ clause({ p(f2(y7, x6)), p2(y7, x6) }) }) -// .toSimplify({ clause({ p2(f(g(x5)), y4), ~p(f2(f(g(x5)), y4)), ~p2(f2(f(g(x5)), y4), x5) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - -// TEST_SIMPLIFICATION(pos_sub_res_test07, -// tester() -// .simplifyWith({ clause({ p(f2(y7, x6)), p2(y7, x6) }) }) -// .toSimplify({ clause({ p2(f(g(x5)), y4), ~p(f2(f(g(x5)), y4)), ~p2(f2(f(g(x5)), y4), x5) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - -// TEST_SIMPLIFICATION(pos_sub_res_test08, -// tester() -// .simplifyWith({ clause({ ~p2(y7, d) }) }) -// .toSimplify({ clause({ ~p(x6), ~p(x5), ~p2(f(f2(f2(x5, x5), f2(x5, x6))), x6), p2(f2(f2(x5, x5), f2(x5, x6)), d) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - -// TEST_SIMPLIFICATION(pos_sub_res_test09, -// tester() -// .simplifyWith({ clause({ ~p3(d, y7, d), ~p3(y7, e, c) }) }) -// .toSimplify({ clause({ p3(d, x6, d), ~p3(x6, e, c) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - -// TEST_SIMPLIFICATION(pos_sub_res_test10, -// tester() -// .simplifyWith({ clause({ p2(y7, x6), f2(y7, x6) == f2(f3(x5, y4, x4), x4), p2(y4, x4) }) }) -// .toSimplify({ clause({ ~p2(g2(h2(y3, x2), x2), x7), f2(g2(h2(y3, x2), x2), x7) == f2(f3(y6, g2(h2(y3, x2), x2), x7), x7) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - -// TEST_SIMPLIFICATION(pos_sub_res_test11, -// tester() -// .simplifyWith({ clause({ p2(y7, x6), ~q2(x5, x6), ~p2(y7, x5) }) }) -// .toSimplify({ clause({ p2(f2(y4, x6), y4), ~p2(x6, y7), ~r2(y4, y7), ~p2(x6, d), ~q2(y4, d), ~q2(y7, d) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - -// TEST_SIMPLIFICATION(pos_sub_res_test12, -// tester() -// .simplifyWith({ clause({ p(d) }) }) -// .toSimplify({ clause({ q(d), ~p(d) }) }) -// .expected({ /* nothing */ }) -// .justifications({ /* nothing */ }) -// ) - // negative subsumption resolutions TEST_SIMPLIFICATION(neg_sub_res_test01, From 66d53a6d4c407ceff09cdf28c0581760b26b2cbb Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Tue, 20 Jan 2026 11:16:23 +0100 Subject: [PATCH 10/13] Upload all coverage files into artifact --- .github/workflows/coverage.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index cb2bf76df..d58539d77 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -42,6 +42,6 @@ jobs: with: name: vcoverage-${{ github.sha }} path: | - ${{ runner.workspace }}/vampire/build/vcoverage/*.html + ${{ runner.workspace }}/vampire/build/vcoverage/* overwrite: true if-no-files-found: error From 2f107744f844b0b072a21facc0687e923b99a428 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Wed, 21 Jan 2026 15:44:38 +0100 Subject: [PATCH 11/13] Remove TODO --- Inferences/InnerRewriting.hpp | 1 - 1 file changed, 1 deletion(-) diff --git a/Inferences/InnerRewriting.hpp b/Inferences/InnerRewriting.hpp index 5e44e01e3..d8d5dbbcd 100644 --- a/Inferences/InnerRewriting.hpp +++ b/Inferences/InnerRewriting.hpp @@ -25,7 +25,6 @@ namespace Inferences using namespace Kernel; using namespace Saturation; -// TODO this should be an immediate simplification class InnerRewriting : public ImmediateSimplificationEngine { From cdcec672eae19af3ab4b72a4156f065a542c5fc2 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Wed, 21 Jan 2026 17:07:13 +0100 Subject: [PATCH 12/13] InnerRewriting was wrongly placed as first and not the last simplifier --- Saturation/SaturationAlgorithm.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp index 23e798cc8..ccafd14c3 100644 --- a/Saturation/SaturationAlgorithm.cpp +++ b/Saturation/SaturationAlgorithm.cpp @@ -1708,6 +1708,12 @@ std::pair SaturationAlgorithm::createISE(Proble bool mayHaveEquality = couldEqualityArise(prb,opt); + // This was earlier at the beginning of forward simplifications, + // so let's put it for now to the end of immediate simplifications + if (mayHaveEquality && opt.innerRewriting()) { + res->addFront(new InnerRewriting(ordering)); + } + if (mayHaveEquality && opt.equationalTautologyRemoval()) { res->addFront(new EquationalTautologyRemoval()); } @@ -1801,11 +1807,5 @@ std::pair SaturationAlgorithm::createISE(Proble resMany.addFront(std::make_unique()); } - // This was earlier at the beginning of forward simplifications, - // so let's put it for now to the end of immediate simplifications - if (mayHaveEquality && opt.innerRewriting()) { - res->addFront(new InnerRewriting(ordering)); - } - return std::make_pair(res, std::move(resMany)); } From d59c7acbc01742c8e5b9d2be32e2b690bbf82e14 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Fri, 23 Jan 2026 11:11:31 +0100 Subject: [PATCH 13/13] a new comment --- Saturation/SaturationAlgorithm.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp index ccafd14c3..97696e6e0 100644 --- a/Saturation/SaturationAlgorithm.cpp +++ b/Saturation/SaturationAlgorithm.cpp @@ -1708,8 +1708,8 @@ std::pair SaturationAlgorithm::createISE(Proble bool mayHaveEquality = couldEqualityArise(prb,opt); - // This was earlier at the beginning of forward simplifications, - // so let's put it for now to the end of immediate simplifications + // InnerRewriting is relatively expensive, so let's insert it first, + // so that it gets applied as the last ImmediateSimplification if (mayHaveEquality && opt.innerRewriting()) { res->addFront(new InnerRewriting(ordering)); }