diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp index b4464dc9c..987da7d43 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -638,7 +638,7 @@ bool CodeTree::Matcher::execute() } template -void CodeTree::Matcher::init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack* firstsInBlocks_) +void CodeTree::Matcher::init(CodeTree const* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack* firstsInBlocks_) { tree=tree_; entry=entry_; diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp index 7184abfff..2ce2b5a28 100644 --- a/Indexing/CodeTree.hpp +++ b/Indexing/CodeTree.hpp @@ -382,7 +382,7 @@ class CodeTree } protected: - void init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_ = 0, + void init(CodeTree const* tree_, CodeOp* entry_, LitInfo* linfos_ = 0, size_t linfoCnt_ = 0, Stack* firstsInBlocks_ = 0); bool backtrack(); @@ -416,7 +416,7 @@ class CodeTree Stack> btStack; CodeOp* entry; - CodeTree* tree; + CodeTree const* tree; /** * Array of alternative LitInfo objects diff --git a/Indexing/CodeTreeInterfaces.cpp b/Indexing/CodeTreeInterfaces.cpp index b430bed46..e235a25e5 100644 --- a/Indexing/CodeTreeInterfaces.cpp +++ b/Indexing/CodeTreeInterfaces.cpp @@ -14,14 +14,13 @@ */ #include "Indexing/Index.hpp" -#include "Indexing/ResultSubstitution.hpp" +#include "Inferences/ALASCA/Demodulation.hpp" #include "Lib/Allocator.hpp" #include "Lib/Recycled.hpp" #include "Debug/TimeProfiling.hpp" #include "Lib/VirtualIterator.hpp" #include "Kernel/Renaming.hpp" -#include "Kernel/SubstHelper.hpp" #include "Kernel/Term.hpp" #include "ClauseCodeTree.hpp" @@ -35,70 +34,19 @@ namespace Indexing using namespace Lib; using namespace Kernel; -template -class CodeTreeSubstitution -: public ResultSubstitution -{ -public: - CodeTreeSubstitution(CodeTree::BindingArray* bindings, Renaming* resultNormalizer) - : _bindings(bindings), _resultNormalizer(resultNormalizer) - {} - - USE_ALLOCATOR(CodeTreeSubstitution); - - TermList apply(unsigned var) - { - if constexpr (is_indexed_data_normalized::value) { - return (*_bindings)[var]; - } else { - ASS(_resultNormalizer->contains(var)); - unsigned nvar=_resultNormalizer->get(var); - TermList res=(*_bindings)[nvar]; - ASS(res.isTerm()||res.isOrdinaryVar()); - ASSERT_VALID(res); - return res; - } - } - - TermList applyToBoundResult(unsigned v) override - { - return apply(v); - } - - TermList applyToBoundResult(TermList t) override - { - return SubstHelper::apply(t, *this); - } - - Literal* applyToBoundResult(Literal* lit) override - { - return SubstHelper::apply(lit, *this); - } - - bool isIdentityOnQueryWhenResultBound() override {return true;} -private: - void output(std::ostream& out) const final - { out << "CodeTreeSubstitution()"; } - - CodeTree::BindingArray* _bindings; - Renaming* _resultNormalizer; -}; - -/////////////////////////////////////// - template class CodeTreeTIS::ResultIterator -: public IteratorCore> +: public IteratorCore*, Data>> { public: - ResultIterator(CodeTreeTIS* tree, TermList t, bool retrieveSubstitutions) + ResultIterator(const CodeTreeTIS& tree, TypedTermList t, bool retrieveSubstitutions) : _retrieveSubstitutions(retrieveSubstitutions), _found(0), _finished(false), _tree(tree) { - _matcher->init(&_tree->_ct, t); + _matcher->init(&_tree._ct, t); if(_retrieveSubstitutions) { - _subst = new CodeTreeSubstitution(&_matcher->bindings, &*_resultNormalizer); + _subst = new GenSubstitution(&_matcher->bindings, &*_resultNormalizer); } } @@ -126,47 +74,45 @@ class CodeTreeTIS::ResultIterator return _found; } - QueryRes next() override + QueryRes*, Data> next() override { ASS(_found); - ResultSubstitutionSP subs; if (_retrieveSubstitutions) { if constexpr (!is_indexed_data_normalized::value) { _resultNormalizer->reset(); - _resultNormalizer->normalizeVariables(_found->term); + _resultNormalizer->normalizeVariables(_found->key()); } - subs = ResultSubstitutionSP(_subst, /* nondisposable */ true); } - auto out = QueryRes(subs, _found); + auto out = QueryRes*, Data>(_subst, _found); _found=0; return out; } private: - - CodeTreeSubstitution* _subst; + GenSubstitution* _subst = nullptr; Recycled _resultNormalizer; bool _retrieveSubstitutions; Data* _found; bool _finished; - CodeTreeTIS* _tree; + const CodeTreeTIS& _tree; Recycled::TermMatcher> _matcher; }; template -VirtualIterator> CodeTreeTIS::getGeneralizations(TypedTermList t, bool retrieveSubstitutions) +VirtualIterator*, Data>> CodeTreeTIS::getGeneralizations(TypedTermList t, bool retrieveSubstitutions) const { if(_ct.isEmpty()) { - return VirtualIterator>::getEmpty(); + return VirtualIterator*, Data>>::getEmpty(); } - return vi( new ResultIterator(this, t, retrieveSubstitutions) ); + return vi( new ResultIterator(*this, t, retrieveSubstitutions) ); } template class CodeTreeTIS; template class CodeTreeTIS; template class CodeTreeTIS; template class CodeTreeTIS; +template class CodeTreeTIS; template class CodeTreeTIS>; ///////////////// CodeTreeSubsumptionIndex ////////////////////// diff --git a/Indexing/CodeTreeInterfaces.hpp b/Indexing/CodeTreeInterfaces.hpp index 9fbe7c76d..83600e164 100644 --- a/Indexing/CodeTreeInterfaces.hpp +++ b/Indexing/CodeTreeInterfaces.hpp @@ -21,7 +21,6 @@ #include "ClauseCodeTree.hpp" #include "Index.hpp" -#include "TermIndexingStructure.hpp" namespace Indexing { @@ -29,17 +28,50 @@ namespace Indexing using namespace Kernel; using namespace Lib; +template +class GenSubstitution + : public SubstApplicator +{ +public: + GenSubstitution(CodeTree::BindingArray* bindings, Renaming* resultNormalizer) + : _bindings(bindings), _resultNormalizer(resultNormalizer) {} + + USE_ALLOCATOR(GenSubstitution); + + TermList apply(unsigned var) const override { + if constexpr (is_indexed_data_normalized::value) { + return (*_bindings)[var]; + } else { + ASS(_resultNormalizer->contains(var)); + unsigned nvar=_resultNormalizer->get(var); + TermList res=(*_bindings)[nvar]; + ASS(res.isTerm()||res.isOrdinaryVar()); + ASSERT_VALID(res); + return res; + } + } + + TermList apply(TermList t) const { + return SubstHelper::apply(t, *this); + } + + Literal* apply(Literal* lit) const { + return SubstHelper::apply(lit, *this); + } +private: + CodeTree::BindingArray* _bindings; + Renaming* _resultNormalizer; +}; /** * Term indexing structure using code trees to retrieve generalizations */ - template -class CodeTreeTIS : public TermIndexingStructure +class CodeTreeTIS { public: /* INFO: we ignore unifying the sort of the keys here */ - void handle(Data data, bool insert) final + void handle(Data data, bool insert) { if (insert) { auto ti = new Data(std::move(data)); @@ -49,12 +81,9 @@ class CodeTreeTIS : public TermIndexingStructure } } - VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) final ; - // TODO: get rid of NOT_IMPLEMENTED - VirtualIterator> getUwa(TypedTermList t, Options::UnificationWithAbstraction, bool fixedPointIteration, bool funcExt) override { NOT_IMPLEMENTED; } - VirtualIterator> getUwaHOL(TypedTermList t, Options::UnificationWithAbstraction, bool fixedPointIteration, unsigned hoUnifDepth, bool funcExt) override { NOT_IMPLEMENTED; } + VirtualIterator*, Data>> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) const; - void output(std::ostream& out) const final { out << _ct; } + void output(std::ostream& out) const { out << _ct; } private: class ResultIterator; diff --git a/Indexing/Index.hpp b/Indexing/Index.hpp index a84655c25..5a3cf3df4 100644 --- a/Indexing/Index.hpp +++ b/Indexing/Index.hpp @@ -95,7 +95,7 @@ struct TermLiteralClause Literal* literal = nullptr; Clause* clause = nullptr; - TypedTermList const& key() const { return term; } + TypedTermList key() const { return term; } auto asTuple() const { return std::make_tuple(clause->number(), literal->getId(), term); } @@ -114,7 +114,7 @@ struct TermLiteralClause * left- and right-hand side normalized and cache preorderedness. */ struct DemodulatorData { - DemodulatorData(TypedTermList term, TermList rhs, Clause* clause, bool preordered, const Ordering& ord) + DemodulatorData(TypedTermList term, TypedTermList rhs, Clause* clause, bool preordered, const Ordering& ord) : term(term), rhs(rhs), clause(clause), preordered(preordered), tod(ord.createTermOrderingDiagram()) { // insert pointer to owner as non-null value representing success diff --git a/Indexing/IndexManager.cpp b/Indexing/IndexManager.cpp index 6a0adaf0b..3fa009eb8 100644 --- a/Indexing/IndexManager.cpp +++ b/Indexing/IndexManager.cpp @@ -31,7 +31,7 @@ using namespace Lib; using namespace Indexing; -SIMP_INDEX_IMPL(AlascaIndex) +SIMP_INDEX_IMPL(GeneralizingAlascaIndex) SIMP_INDEX_IMPL(AlascaIndex) SIMP_INDEX_IMPL(DemodulationLHSIndex) SIMP_INDEX_IMPL(DemodulationLHSIndex) diff --git a/Indexing/TermCodeTree.cpp b/Indexing/TermCodeTree.cpp index 4d82cd42c..3f080a1df 100644 --- a/Indexing/TermCodeTree.cpp +++ b/Indexing/TermCodeTree.cpp @@ -12,7 +12,10 @@ * Implements class TermCodeTree. */ +#include "Inferences/ALASCA/Demodulation.hpp" + #include "Kernel/FlatTerm.hpp" +#include "Kernel/Matcher.hpp" #include "Kernel/Term.hpp" #include "Index.hpp" @@ -51,9 +54,14 @@ void TermCodeTree::insert(Data* data) static CodeStack code; code.reset(); - TermList t=data->term; + auto t = data->key(); if (t.isVar()) { code.push(CodeOp::getTermOp(ASSIGN_VAR,0)); + // we match the variable sort separately, but the binding array has to be prepared + for (const auto& v : iterTraits(VariableIterator(t.sort()))) { + ASS_G(v.var(), 0); // X0 is reserved for the term itself + if (v.var()+1 > _maxVarCnt) { _maxVarCnt = v.var()+1; } + } } else { ASS(t.isTerm()); @@ -64,7 +72,7 @@ void TermCodeTree::insert(Data* data) } code.push(CodeOp::getSuccess(data)); - incorporate(code); + incorporate(code); //@b incorporate should empty the code stack ASS(code.isEmpty()); } @@ -78,9 +86,9 @@ void TermCodeTree::remove(const Data& data) static Stack firstsInBlocks; firstsInBlocks.reset(); - FlatTerm* ft=FlatTerm::create(data.term); + FlatTerm* ft=FlatTerm::create(data.key()); rtm.init(ft, this, &firstsInBlocks); - + Data* dptr = nullptr; for(;;) { if (!rtm.execute()) { @@ -93,13 +101,13 @@ void TermCodeTree::remove(const Data& data) break; } } - + rtm.op->makeFail(); ASS(dptr); delete dptr; ft->destroy(); - + optimizeMemoryAfterRemoval(&firstsInBlocks, rtm.op); } // TermCodeTree::remove @@ -108,7 +116,7 @@ void TermCodeTree::RemovingTermMatcher::init(FlatTerm* ft_, TermCodeTree* tree_, Stack* firstsInBlocks_) { Base::init(tree_, tree_->getEntryPoint(), /*linfos_=*/0, /*linfoCnt_=*/0, firstsInBlocks_); - + Base::firstsInBlocks->push(Base::entry); Base::ft=ft_; @@ -127,12 +135,13 @@ TermCodeTree::TermMatcher::TermMatcher() } template -void TermCodeTree::TermMatcher::init(CodeTree* tree, TermList t) +void TermCodeTree::TermMatcher::init(CodeTree const* tree, TypedTermList t) { Base::init(tree,tree->getEntryPoint(),/*linfos_=*/0,/*linfoCnt_=*/0); ASS(!ft); ft = FlatTerm::create(t); + _querySort = t.sort(); Base::op=Base::entry; Base::tp=0; @@ -154,20 +163,31 @@ Data* TermCodeTree::TermMatcher::next() //all possible matches are exhausted return 0; } - - Base::_matched=Base::execute(); - if (!Base::_matched) { - return 0; - } - ASS(Base::op->isSuccess()); - return Base::op->template getSuccessResult(); + while ((Base::_matched=Base::execute())) { + ASS(Base::op->isSuccess()); + auto res = Base::op->template getSuccessResult(); + if (res->key().isVar()) { + // match the variable sort separately + Substitution subst; + if (!MatchingUtils::matchTerms(res->key().sort(), _querySort, subst)) { + continue; + } + for (const auto& [v,t] : iterTraits(subst.items())) { + ASS_G(v, 0); // X0 is reserved for the term itself + Base::bindings[v] = t; + } + } + return res; + } + return nullptr; } +template class TermCodeTree; template class TermCodeTree; -template class TermCodeTree; template class TermCodeTree; template class TermCodeTree; +template class TermCodeTree; template class TermCodeTree>; }; diff --git a/Indexing/TermCodeTree.hpp b/Indexing/TermCodeTree.hpp index e8ed5c6a9..e518908b9 100644 --- a/Indexing/TermCodeTree.hpp +++ b/Indexing/TermCodeTree.hpp @@ -20,6 +20,8 @@ #include "Lib/Allocator.hpp" #include "Lib/Stack.hpp" +#include "Kernel/TypedTermList.hpp" + #include "CodeTree.hpp" @@ -29,7 +31,7 @@ using namespace Lib; using namespace Kernel; template -class TermCodeTree : public CodeTree +class TermCodeTree : public CodeTree { protected: void onCodeOpDestroying(CodeOp* op) override; @@ -60,12 +62,14 @@ class TermCodeTree : public CodeTree using Base = Matcher; using Base::ft; - void init(CodeTree* tree, TermList t); + void init(CodeTree const* tree, TypedTermList t); void reset(); - + Data* next(); - + USE_ALLOCATOR(TermMatcher); + private: + TermList _querySort; }; }; diff --git a/Indexing/TermIndex.cpp b/Indexing/TermIndex.cpp index 48552eaf8..6b77aebd5 100644 --- a/Indexing/TermIndex.cpp +++ b/Indexing/TermIndex.cpp @@ -119,8 +119,7 @@ template class DemodulationSubtermIndex; template DemodulationLHSIndex::DemodulationLHSIndex(SaturationAlgorithm& salg) -: TermIndex(new CodeTreeTIS()), _ord(salg.getOrdering()), - _preordered(salg.getOptions().forwardDemodulation()==Options::Demodulation::PREORDERED) {}; +: _ord(salg.getOrdering()), _preordered(salg.getOptions().forwardDemodulation()==Options::Demodulation::PREORDERED) {} template void DemodulationLHSIndex::handleClause(Clause* c, bool adding) @@ -134,19 +133,18 @@ void DemodulationLHSIndex::handleClause(Clause* c, bool adding) Literal* lit=(*c)[0]; auto [lhsi, preordered] = EqHelper::getDemodulationLHSIterator(lit, _preordered, _ord); - while (lhsi.hasNext()) { - auto lhs = lhsi.next(); - + for (const auto& lhs : iterTraits(std::move(lhsi))) { // DemodulatorData expects lhs and rhs to be normalized Renaming r; r.normalizeVariables(lhs); + auto sortR = r.apply(lhs.sort()); DemodulatorData dd( - TypedTermList(r.apply(lhs),r.apply(lhs.sort())), - r.apply(EqHelper::getOtherEqualitySide(lit, lhs)), + TypedTermList(r.apply(lhs),sortR), + TypedTermList(r.apply(EqHelper::getOtherEqualitySide(lit, lhs)),sortR), c, preordered, _ord ); - _is->handle(std::move(dd), adding); + GeneralizingTermIndex::_ct.handle(std::move(dd), adding); } } @@ -195,7 +193,7 @@ void InductionTermIndex::handleClause(Clause* c, bool adding) } StructInductionTermIndex::StructInductionTermIndex(SaturationAlgorithm& salg) -: TermIndex(new TermSubstitutionTree()), _inductionGroundOnly(salg.getOptions().inductionGroundOnly()) {} +: _inductionGroundOnly(salg.getOptions().inductionGroundOnly()) {} void StructInductionTermIndex::handleClause(Clause* c, bool adding) { @@ -219,11 +217,7 @@ void StructInductionTermIndex::handleClause(Clause* c, bool adding) } if (InductionHelper::isInductionTerm(t) && InductionHelper::isStructInductionTerm(t)) { - if (adding) { - _is->insert(TermLiteralClause{ t, lit, c }); - } else { - _is->remove(TermLiteralClause{ t, lit, c }); - } + _ct.handle(TermLiteralClause{ t, lit, c }, adding); } } } diff --git a/Indexing/TermIndex.hpp b/Indexing/TermIndex.hpp index 3d51cfe4d..3a0789bd8 100644 --- a/Indexing/TermIndex.hpp +++ b/Indexing/TermIndex.hpp @@ -17,6 +17,7 @@ #define __TermIndex__ #include "Index.hpp" +#include "Indexing/CodeTreeInterfaces.hpp" #include "TermIndexingStructure.hpp" namespace Indexing { @@ -41,9 +42,6 @@ class TermIndex VirtualIterator> getUnifications(TypedTermList t, bool retrieveSubstitutions = true) { return _is->getUnifications(t, retrieveSubstitutions); } - VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) - { return _is->getGeneralizations(t, retrieveSubstitutions); } - template VirtualIterator> getInstances(TypedTermList t, bool retrieveSubstitutions = true) { @@ -69,6 +67,20 @@ class TermIndex std::unique_ptr> _is; }; +template +class GeneralizingTermIndex +: public Index +{ +public: + auto getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) const + { return iterTraits(_ct.getGeneralizations(t, retrieveSubstitutions)); } + + friend std::ostream& operator<<(std::ostream& out, GeneralizingTermIndex const& self) + { return out << self._ct; } +protected: + CodeTreeTIS _ct; +}; + template class SuperpositionSubtermIndex : public TermIndex @@ -113,7 +125,7 @@ class DemodulationSubtermIndex */ template class DemodulationLHSIndex -: public TermIndex +: public GeneralizingTermIndex { public: DemodulationLHSIndex(SaturationAlgorithm& salg); @@ -142,7 +154,7 @@ class InductionTermIndex * Term index for structural induction */ class StructInductionTermIndex -: public TermIndex +: public GeneralizingTermIndex { public: StructInductionTermIndex(SaturationAlgorithm& salg); diff --git a/Indexing/TermIndexingStructure.hpp b/Indexing/TermIndexingStructure.hpp index 3bf1f123c..79672b917 100644 --- a/Indexing/TermIndexingStructure.hpp +++ b/Indexing/TermIndexingStructure.hpp @@ -32,8 +32,6 @@ class TermIndexingStructure { virtual VirtualIterator> getUnifications(TypedTermList t, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } virtual VirtualIterator> getUwa(TypedTermList t, Options::UnificationWithAbstraction uwa, bool fixedPointIteration, bool funcExt) = 0; virtual VirtualIterator> getUwaHOL(TypedTermList t, Options::UnificationWithAbstraction uwa, bool fixedPointIteration, unsigned hoUnifDepth, bool funcExt) = 0; - virtual VirtualIterator> getUnificationsUsingSorts(TypedTermList tt, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } - virtual VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } virtual VirtualIterator> getInstances(TypedTermList t, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; } virtual void output(std::ostream& output) const = 0; diff --git a/Indexing/TermSubstitutionTree.hpp b/Indexing/TermSubstitutionTree.hpp index 03897c0f2..825ad051b 100644 --- a/Indexing/TermSubstitutionTree.hpp +++ b/Indexing/TermSubstitutionTree.hpp @@ -48,7 +48,6 @@ class TermSubstitutionTree using BindingMap = typename SubstitutionTree::BindingMap; using Node = typename SubstitutionTree::Node; using FastInstancesIterator = typename SubstitutionTree::FastInstancesIterator; - using FastGeneralizationsIterator = typename SubstitutionTree::FastGeneralizationsIterator; using LDIterator = typename SubstitutionTree::LDIterator; using Leaf = typename SubstitutionTree::Leaf; using LeafIterator = typename SubstitutionTree::LeafIterator; @@ -82,10 +81,6 @@ class TermSubstitutionTree VirtualIterator> getInstances(TypedTermList t, bool retrieveSubstitutions) final { return pvi(getResultIterator(t, retrieveSubstitutions)); } - VirtualIterator> getGeneralizations(TypedTermList t, bool retrieveSubstitutions) final - { return pvi(getResultIterator(t, retrieveSubstitutions)); } - - VirtualIterator> getUwa(TypedTermList t, Options::UnificationWithAbstraction uwa, bool fixedPointIteration, bool funcExt) final { AbstractionOracle oracle(uwa, funcExt); diff --git a/Inferences/ALASCA/Demodulation.hpp b/Inferences/ALASCA/Demodulation.hpp index d9fc3a66c..a2fa2cb32 100644 --- a/Inferences/ALASCA/Demodulation.hpp +++ b/Inferences/ALASCA/Demodulation.hpp @@ -44,7 +44,7 @@ class Demodulation struct Lhs : public SelectedEquality { Lhs(SelectedEquality self) : SelectedEquality(std::move(self)) {} static const char* name() { return "alasca demodulation lhs"; } - TypedTermList key() { return TypedTermList(SelectedEquality::biggerSide().term()); } + TypedTermList key() const { return TypedTermList(SelectedEquality::biggerSide().term()); } static auto iter(AlascaState& shared, Clause* simplifyWith) { return iterTraits(iterItems(simplifyWith)) diff --git a/Inferences/ALASCA/FwdDemodulation.cpp b/Inferences/ALASCA/FwdDemodulation.cpp index 32650af88..80c7a8154 100644 --- a/Inferences/ALASCA/FwdDemodulation.cpp +++ b/Inferences/ALASCA/FwdDemodulation.cpp @@ -22,7 +22,7 @@ namespace Inferences { namespace ALASCA { FwdDemodulation::FwdDemodulation(SaturationAlgorithm& salg) - : _shared(salg.alascaState()), _index(salg.getSimplifyingIndex>()) + : _shared(salg.alascaState()), _index(salg.getSimplifyingIndex>()) {} //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -44,7 +44,7 @@ bool FwdDemodulation::perform(Clause* toSimplify, Clause*& replacement, ClauseIt Stack simplified; for (auto rhs : Rhs::iter(_shared, toSimplify)) { // DEBUG("simplifyable position: ", pos.term, " in ", *pos.lit) - for (auto lhs : _index->generalizations(rhs.term)) { + for (auto lhs : _index->getGeneralizations(rhs.term)) { auto simplified = Demodulation::apply(_shared, *lhs.data, rhs); if (simplified.isSome()) { replacement = simplified.unwrap(); diff --git a/Inferences/ALASCA/FwdDemodulation.hpp b/Inferences/ALASCA/FwdDemodulation.hpp index a437ff2f8..7cf432629 100644 --- a/Inferences/ALASCA/FwdDemodulation.hpp +++ b/Inferences/ALASCA/FwdDemodulation.hpp @@ -44,7 +44,7 @@ class FwdDemodulation private: AlascaState& _shared; - std::shared_ptr> _index; + std::shared_ptr> _index; }; } // namespaceALASCA diff --git a/Inferences/BackwardDemodulation.cpp b/Inferences/BackwardDemodulation.cpp index ae7279f1f..fe5e4611b 100644 --- a/Inferences/BackwardDemodulation.cpp +++ b/Inferences/BackwardDemodulation.cpp @@ -57,8 +57,8 @@ namespace { struct Applicator : SubstApplicator { Applicator(ResultSubstitution* subst) : subst(subst) {} - TermList operator()(unsigned v) const override { - return subst->applyToBoundQuery(TermList(v,false)); + TermList apply(unsigned v) const override { + return subst->applyToBoundQuery(TermList::var(v)); } ResultSubstitution* subst; }; diff --git a/Inferences/DemodulationHelper.hpp b/Inferences/DemodulationHelper.hpp index 6d99a49fb..550605eb1 100644 --- a/Inferences/DemodulationHelper.hpp +++ b/Inferences/DemodulationHelper.hpp @@ -43,7 +43,7 @@ class DemodulationHelper { continue; } - TermList vSubst = (*applicator)(v.var()); + TermList vSubst = applicator->apply(v.var()); if (!vSubst.isVar() || !range.insert(vSubst.var())) { return false; } diff --git a/Inferences/ForwardDemodulation.cpp b/Inferences/ForwardDemodulation.cpp index 2b1d9460e..73586f1ff 100644 --- a/Inferences/ForwardDemodulation.cpp +++ b/Inferences/ForwardDemodulation.cpp @@ -26,7 +26,6 @@ #include "Kernel/Term.hpp" #include "Kernel/TermIterators.hpp" #include "Kernel/ColorHelper.hpp" -#include "Kernel/RobSubstitution.hpp" #include "Indexing/Index.hpp" #include "Indexing/TermIndex.hpp" @@ -48,27 +47,6 @@ using namespace Kernel; using namespace Indexing; using namespace Saturation; -namespace { - -struct Applicator : SubstApplicator { - Applicator(ResultSubstitution* subst) : subst(subst) {} - TermList operator()(unsigned v) const override { - return subst->applyToBoundResult(v); - } - ResultSubstitution* subst; -}; - -struct ApplicatorWithEqSort : SubstApplicator { - ApplicatorWithEqSort(ResultSubstitution* subst, const RobSubstitution& vSubst) : subst(subst), vSubst(vSubst) {} - TermList operator()(unsigned v) const override { - return vSubst.apply(subst->applyToBoundResult(v), 0); - } - ResultSubstitution* subst; - const RobSubstitution& vSubst; -}; - -} // end namespace - template ForwardDemodulation::ForwardDemodulation(SaturationAlgorithm& salg) : _preorderedOnly(salg.getOptions().forwardDemodulation()==Options::Demodulation::PREORDERED), @@ -135,32 +113,8 @@ bool ForwardDemodulation::perform(Clause* cl, Clause*& replacement, } auto lhs = qr.data->term; - - // TODO: - // to deal with polymorphic matching - // Ideally, we would like to extend the substitution - // returned by the index to carry out the sort match. - // However, ForwardDemodulation uses a CodeTree as its - // indexing mechanism, and it is not clear how to extend - // the substitution returned by a code tree. - static RobSubstitution eqSortSubs; - if(lhs.isVar()){ - eqSortSubs.reset(); - TermList querySort = trm.sort(); - TermList eqSort = qr.data->term.sort(); - if(!eqSortSubs.match(eqSort, 0, querySort, 1)){ - continue; - } - } - auto subs = qr.unifier; - ASS(subs->isIdentityOnQueryWhenResultBound()); - - ApplicatorWithEqSort applWithEqSort(subs.ptr(), eqSortSubs); - Applicator applWithoutEqSort(subs.ptr()); - auto appl = lhs.isVar() ? (SubstApplicator*)&applWithEqSort : (SubstApplicator*)&applWithoutEqSort; - - AppliedTerm rhsApplied(qr.data->rhs,appl,true); + AppliedTerm rhsApplied(qr.data->rhs,subs,true); bool preordered = qr.data->preordered; ASS_EQ(_ord.compare(trm,rhsApplied),Ordering::reverse(_ord.compare(rhsApplied,trm))); @@ -169,7 +123,7 @@ bool ForwardDemodulation::perform(Clause* cl, Clause*& replacement, #if VDEBUG auto dcomp = _ord.compareUnidirectional(trm,rhsApplied); #endif - qr.data->tod->init(appl); + qr.data->tod->init(subs); if (!preordered && (_preorderedOnly || !qr.data->tod->next())) { ASS_NEQ(dcomp,Ordering::GREATER); continue; @@ -195,7 +149,7 @@ bool ForwardDemodulation::perform(Clause* cl, Clause*& replacement, TermList rhsS = rhsApplied.apply(); - if (redundancyCheck && !_helper.isPremiseRedundant(cl, lit, trm, rhsS, lhs, appl)) { + if (redundancyCheck && !_helper.isPremiseRedundant(cl, lit, trm, rhsS, lhs, subs)) { continue; } diff --git a/Inferences/ForwardGroundJoinability.cpp b/Inferences/ForwardGroundJoinability.cpp index ea7e0af65..bb0d4d5d3 100644 --- a/Inferences/ForwardGroundJoinability.cpp +++ b/Inferences/ForwardGroundJoinability.cpp @@ -36,18 +36,6 @@ using namespace Indexing; using namespace Saturation; using namespace std; -namespace { - -struct Applicator : SubstApplicator { - Applicator(ResultSubstitution* subst) : subst(subst) {} - TermList operator()(unsigned v) const override { - return subst->applyToBoundResult(v); - } - ResultSubstitution* subst; -}; - -} // end namespace - template ForwardGroundJoinability::ForwardGroundJoinability(SaturationAlgorithm& salg) : _ord(salg.getOrdering()), @@ -127,12 +115,7 @@ bool ForwardGroundJoinability::perform(Clause* cl, Clause*& replace } TermList rhs = qr.data->rhs; - - auto subs = qr.unifier; - ASS(subs->isIdentityOnQueryWhenResultBound()); - Applicator appl(subs.ptr()); - - AppliedTerm rhsApplied(rhs, &appl, true); + AppliedTerm rhsApplied(rhs, qr.unifier, true); #if VDEBUG POStruct dpo_struct(tpo); @@ -150,7 +133,7 @@ bool ForwardGroundJoinability::perform(Clause* cl, Clause*& replace #endif POStruct po_struct(tpo); - if (!TermOrderingDiagram::extendVarsGreater(qr.data->tod.get(), &appl, po_struct)) { + if (!TermOrderingDiagram::extendVarsGreater(qr.data->tod.get(), qr.unifier, po_struct)) { // TODO this check sometimes fails when the debug code can detect the // extension to get GREATER due to elimination of linear expressions // ASS(!success); diff --git a/Inferences/FunctionDefinitionRewriting.cpp b/Inferences/FunctionDefinitionRewriting.cpp index f00d165e6..cd7b16927 100644 --- a/Inferences/FunctionDefinitionRewriting.cpp +++ b/Inferences/FunctionDefinitionRewriting.cpp @@ -35,19 +35,9 @@ using namespace Lib; using namespace Kernel; using namespace Saturation; -namespace { -struct Applicator : SubstApplicator { - Applicator(ResultSubstitution* subst) : subst(subst) {} - TermList operator()(unsigned v) const override { - return subst->applyToBoundResult(v); - } - ResultSubstitution* subst; -}; -} - Clause* performRewriting( Clause *rwClause, Literal *rwLit, TermList rwTerm, Clause *eqClause, - Literal *eqLit, TermList eqLHS, ResultSubstitutionSP subst, + Literal *eqLit, TermList eqLHS, const GenSubstitution* subst, const DemodulationHelper* helper, bool& isEqTautology, Inference&& inf) { ASS(!eqLHS.isVar()); @@ -55,12 +45,9 @@ Clause* performRewriting( TermList tgtTerm = EqHelper::getOtherEqualitySide(eqLit, eqLHS); // This should be the case for code trees - ASS(subst->isIdentityOnQueryWhenResultBound()); - TermList tgtTermS = subst->applyToBoundResult(tgtTerm); - - Applicator appl(subst.ptr()); + TermList tgtTermS = subst->apply(tgtTerm); - if (helper && !helper->isPremiseRedundant(rwClause,rwLit,rwTerm,tgtTermS,eqLHS,&appl)) { + if (helper && !helper->isPremiseRedundant(rwClause,rwLit,rwTerm,tgtTermS,eqLHS,subst)) { return 0; } @@ -92,7 +79,7 @@ Clause* performRewriting( if (curr == eqLit) { continue; } - Literal* currAfter = subst->applyToBoundResult(curr); + Literal* currAfter = subst->apply(curr); if (EqHelper::isEqTautology(currAfter)) { isEqTautology = true; diff --git a/Inferences/HOL/CNFOnTheFly.cpp b/Inferences/HOL/CNFOnTheFly.cpp index 6ec24a318..2cb400978 100644 --- a/Inferences/HOL/CNFOnTheFly.cpp +++ b/Inferences/HOL/CNFOnTheFly.cpp @@ -214,7 +214,7 @@ ClauseIterator produceClauses(Clause* c, bool generating, SkolemisingFormulaInde if(results.hasNext()){ auto tqr = results.next(); TermList skolemTerm = tqr.data->value; - skolemTerm = tqr.unifier->applyToBoundResult(skolemTerm); + skolemTerm = tqr.unifier->apply(skolemTerm); newTerm = HOL::create::app(srt, args[0], skolemTerm); newTermCreated = true; } diff --git a/Inferences/HOL/CNFOnTheFly.hpp b/Inferences/HOL/CNFOnTheFly.hpp index 0e040c950..d2b28dd09 100644 --- a/Inferences/HOL/CNFOnTheFly.hpp +++ b/Inferences/HOL/CNFOnTheFly.hpp @@ -27,7 +27,7 @@ class SkolemisingFormulaIndex { public: void insertFormula(TermList formula, TermList skolem) { - _ct.insert(TermWithValue(TypedTermList(formula.term()), skolem)); + _ct.handle(TermWithValue(TypedTermList(formula.term()), skolem), /*insert=*/true); } auto getSkolem(Term* forTerm) { return _ct.getGeneralizations(TypedTermList(forTerm), true); diff --git a/Inferences/Induction.cpp b/Inferences/Induction.cpp index c8dc4ce38..f0e2071fc 100644 --- a/Inferences/Induction.cpp +++ b/Inferences/Induction.cpp @@ -543,7 +543,7 @@ struct InductionContextFn { InductionContextFn(Clause* premise, Literal* lit) : _premise(premise), _lit(lit) {} - VirtualIterator operator()(pair, VirtualIterator>> arg) { + VirtualIterator operator()(pair, VirtualIterator*, TermLiteralClause>>> arg) { auto indDepth = _premise->inference().inductionDepth(); // heuristic 2 if (indDepth) { @@ -722,14 +722,14 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit) } } // collect term queries for each induction term - auto sideLitsIt = VirtualIterator, VirtualIterator>>>::getEmpty(); + auto sideLitsIt = VirtualIterator, VirtualIterator*, TermLiteralClause>>>>::getEmpty(); if (_opt.nonUnitInduction()) { sideLitsIt = pvi(iterTraits(getSTLIterator(ta_terms.begin(), ta_terms.end())) .map([](const auto& kv){ return kv.first; }) .map([this](Stack ts) { - auto res = VirtualIterator>::getEmpty(); + auto res = VirtualIterator*, TermLiteralClause>>::getEmpty(); for (const auto& t : ts) { res = pvi(concatIters(std::move(res), _structInductionTermIndex->getGeneralizations(t, false))); } diff --git a/Inferences/Induction.hpp b/Inferences/Induction.hpp index 145aea20c..a3267fe73 100644 --- a/Inferences/Induction.hpp +++ b/Inferences/Induction.hpp @@ -291,7 +291,7 @@ class InductionClauseIterator public: // all the work happens in the constructor! InductionClauseIterator(Clause* premise, InductionHelper helper, const SaturationAlgorithm& salg, - TermIndex* structInductionTermIndex, InductionFormulaIndex& formulaIndex) + const StructInductionTermIndex* structInductionTermIndex, InductionFormulaIndex& formulaIndex) : _helper(helper), _opt(salg.getOptions()), _structInductionTermIndex(structInductionTermIndex), _formulaIndex(formulaIndex), _fnDefHandler(salg.getFunctionDefinitionHandler()) { @@ -355,7 +355,7 @@ class InductionClauseIterator Stack _clauses; InductionHelper _helper; const Options& _opt; - TermIndex* _structInductionTermIndex; + const StructInductionTermIndex* _structInductionTermIndex; InductionFormulaIndex& _formulaIndex; FunctionDefinitionHandler& _fnDefHandler; }; diff --git a/Inferences/SubsumptionEqualityResolution.cpp b/Inferences/SubsumptionEqualityResolution.cpp index 3cc733d06..c3e79fa0c 100644 --- a/Inferences/SubsumptionEqualityResolution.cpp +++ b/Inferences/SubsumptionEqualityResolution.cpp @@ -38,7 +38,7 @@ Clause* SubsumptionEqualityResolution::simplify(Clause* cl) bool unify(TermList lhs, TermList rhs) { return subst.unify(lhs, 0, rhs, 0); } - TermList operator()(unsigned v) const override { + TermList apply(unsigned v) const override { return subst.apply(TermList::var(v), 0); } RobSubstitution subst; diff --git a/Kernel/ALASCA/Index.hpp b/Kernel/ALASCA/Index.hpp index f786479c1..8cd1a471d 100644 --- a/Kernel/ALASCA/Index.hpp +++ b/Kernel/ALASCA/Index.hpp @@ -13,6 +13,7 @@ #include "Indexing/SubstitutionTree.hpp" +#include "Indexing/TermIndex.hpp" #include "Kernel/ALASCA.hpp" #include "Debug/TimeProfiling.hpp" @@ -54,10 +55,6 @@ class AlascaIndex : public Indexing::Index { return iterTraits(_index.template getUwa(state, key, _shared.uwaMode(), _shared.uwaFixedPointIteration)) .timeTraced(_lookupStr.c_str()); } - - auto generalizations(TypedTermList key, bool retrieveSubstitutions = true) - { return iterTraits(_index.getGeneralizations(key, retrieveSubstitutions)); } - auto instances(TypedTermList key, bool retrieveSubstitutions = true) { return iterTraits(_index.getInstances(key, retrieveSubstitutions)); } @@ -90,6 +87,21 @@ class AlascaIndex : public Indexing::Index template std::string AlascaIndex::_lookupStr = T::name() + std::string(" lookup"); template std::string AlascaIndex::_maintenanceStr = T::name() + std::string(" maintenance"); +template +class GeneralizingAlascaIndex : public Indexing::GeneralizingTermIndex +{ +public: + GeneralizingAlascaIndex(SaturationAlgorithm& salg) : _shared(salg.alascaState()) {} + + void handleClause(Clause* c, bool adding) override { + for (auto appl : T::iter(_shared, c)) { + Indexing::GeneralizingTermIndex::_ct.handle(std::move(appl), adding); + } + } +private: + Kernel::AlascaState& _shared; +}; + } // namespace Indexing #undef DEBUG diff --git a/Kernel/EqHelper.cpp b/Kernel/EqHelper.cpp index 9ba1039f6..ad22a59af 100644 --- a/Kernel/EqHelper.cpp +++ b/Kernel/EqHelper.cpp @@ -307,8 +307,10 @@ std::pair,bool> EqHelper::getDemodulationLHSItera if (lit->isNegative()) { return { VirtualIterator::getEmpty(), isPreordered }; } - TermList t0=*lit->nthArgument(0); - TermList t1=*lit->nthArgument(1); + auto [lhs, rhs] = lit->eqArgs(); + auto sort = lit->eqArgSort(); + TypedTermList t0(lhs, sort); + TypedTermList t1(rhs, sort); switch(ord.getEqualityArgumentOrder(lit)) { case Ordering::INCOMPARABLE: @@ -320,24 +322,24 @@ std::pair,bool> EqHelper::getDemodulationLHSItera // If the equation is its own variant when oriented // reversed, there's no need to index both sides if (MatchingUtils::matchReversedArgs(lit, lit)) { - return { withEqualitySort(lit, getSingletonIterator(t0) ), isPreordered }; + return { pvi(getSingletonIterator(t0)), isPreordered }; } - return { withEqualitySort(lit, iterItems(t0, t1)), isPreordered }; + return { pvi(iterItems(t0, t1)), isPreordered }; } - return { withEqualitySort(lit, getSingletonIterator(t0) ), isPreordered }; + return { pvi(getSingletonIterator(t0)), isPreordered }; } if (t1.containsAllVariablesOf(t0)) { - return { withEqualitySort(lit, getSingletonIterator(t1) ), isPreordered }; + return { pvi(getSingletonIterator(t1)), isPreordered }; } break; case Ordering::GREATER: ASS(t0.containsAllVariablesOf(t1)); isPreordered = true; - return { withEqualitySort(lit, getSingletonIterator(t0) ), isPreordered }; + return { pvi(getSingletonIterator(t0)), isPreordered }; case Ordering::LESS: ASS(t1.containsAllVariablesOf(t0)); isPreordered = true; - return { withEqualitySort(lit, getSingletonIterator(t1) ), isPreordered }; + return { pvi(getSingletonIterator(t1)), isPreordered }; //there should be no equality literals of equal terms case Ordering::EQUAL: ASSERTION_VIOLATION_REP(*lit); diff --git a/Kernel/SubstHelper.hpp b/Kernel/SubstHelper.hpp index 8e13d7703..cc961d6bd 100644 --- a/Kernel/SubstHelper.hpp +++ b/Kernel/SubstHelper.hpp @@ -30,8 +30,7 @@ using namespace Lib; struct SubstApplicator { virtual ~SubstApplicator() = default; - virtual TermList operator()(unsigned v) const = 0; - TermList apply(unsigned v) const { return (*this)(v); } + virtual TermList apply(unsigned v) const = 0; }; /** @@ -67,11 +66,11 @@ struct AppliedTerm * null is @b aboveVar is false. */ AppliedTerm(TermList t, const SubstApplicator* applicator, bool aboveVar) - : term(aboveVar && t.isVar() ? (*applicator)(t.var()) : t), + : term(aboveVar && t.isVar() ? applicator->apply(t.var()) : t), aboveVar(aboveVar && t.isVar() ? false : aboveVar), applicator(applicator) {} AppliedTerm(TermList t, AppliedTerm parent) - : term(parent.aboveVar && t.isVar() ? (*parent.applicator)(t.var()) : t), + : term(parent.aboveVar && t.isVar() ? parent.applicator->apply(t.var()) : t), aboveVar(parent.aboveVar && t.isVar() ? false : parent.aboveVar), applicator(parent.applicator) {} /** @@ -91,12 +90,12 @@ struct AppliedTerm return term.containsSubterm(var); } if (term.isVar()) { - return (*applicator)(term.var()).containsSubterm(var); + return applicator->apply(term.var()).containsSubterm(var); } VariableIterator vit(term.term()); while (vit.hasNext()) { auto v = vit.next(); - if ((*applicator)(v.var()).containsSubterm(var)) { + if (applicator->apply(v.var()).containsSubterm(var)) { return true; } } diff --git a/Kernel/TypedTermList.hpp b/Kernel/TypedTermList.hpp index 6f6b78ecc..e72c96453 100644 --- a/Kernel/TypedTermList.hpp +++ b/Kernel/TypedTermList.hpp @@ -16,6 +16,7 @@ #include "Term.hpp" #include "SortHelper.hpp" #include "Lib/Reflection.hpp" +#include "Lib/Set.hpp" namespace Kernel { using SortId = Kernel::TermList; @@ -40,6 +41,22 @@ class TypedTermList : public TermList } TypedTermList(Term* t) : TypedTermList(TermList(t), SortHelper::getResultSort(t)) {} + VirtualIterator varIter() const { + if (isVar()) { + return pvi(concatIters(getSingletonIterator(untyped()), Term::getVariableIterator(_sort))); + } + return Term::getVariableIterator(untyped()); + } + + bool containsAllVariablesOf(TypedTermList other) const { + Set vars; + vars.insertFromIterator(varIter()); + + return iterTraits(other.varIter()).all([&vars](TermList v) { + return vars.contains(v); + }); + } + friend std::ostream& operator<<(std::ostream& out, TypedTermList const& self) { return out << (TermList const&) self << ": " << self._sort; } }; diff --git a/Shell/FunctionDefinitionHandler.cpp b/Shell/FunctionDefinitionHandler.cpp index 12f725df5..42214aede 100644 --- a/Shell/FunctionDefinitionHandler.cpp +++ b/Shell/FunctionDefinitionHandler.cpp @@ -139,7 +139,7 @@ void FunctionDefinitionHandler::initAndPreprocessLate(Problem& prb,const Options defCl->setSplits(SplitSet::getEmpty()); defCl->incRefCnt(); ASS_EQ(condLits.size()+1,lits.size()); - _is->insert(TermLiteralClause {lhs.term(), lits.top(), defCl}); + _is->handle(TermLiteralClause {lhs.term(), lits.top(), defCl}, /*insert=*/true); // TODO should we store this clause anywhere else? } else { it.replace(defCl); diff --git a/Shell/FunctionDefinitionHandler.hpp b/Shell/FunctionDefinitionHandler.hpp index 0ecf8b946..2f87cc08e 100644 --- a/Shell/FunctionDefinitionHandler.hpp +++ b/Shell/FunctionDefinitionHandler.hpp @@ -97,7 +97,7 @@ class FunctionDefinitionHandler auto getGeneralizations(TypedTermList t) { if (_is.isEmpty()) { - return VirtualIterator>::getEmpty(); + return VirtualIterator*, TermLiteralClause>>::getEmpty(); } return _is->getGeneralizations(t, true); } diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp index 772539e36..6734a1744 100644 --- a/Shell/PartialRedundancyHandler.cpp +++ b/Shell/PartialRedundancyHandler.cpp @@ -133,7 +133,7 @@ class PartialRedundancyHandler::ConstraintIndex static SubstMatcher matcher; struct Applicator : public SubstApplicator { - TermList operator()(unsigned v) const override { return matcher.bindings[v]; } + TermList apply(unsigned v) const override { return matcher.bindings[v]; } } applicator; matcher.init(this, ts); diff --git a/UnitTests/tInferences_Demodulation.cpp b/UnitTests/tInferences_Demodulation.cpp index 8b008db53..16ca18433 100644 --- a/UnitTests/tInferences_Demodulation.cpp +++ b/UnitTests/tInferences_Demodulation.cpp @@ -25,14 +25,18 @@ using namespace Test; */ #define MY_SYNTAX_SUGAR \ DECL_DEFAULT_VARS \ + DECL_DEFAULT_SORT_VARS \ DECL_VAR(u, 3) \ DECL_SORT(s) \ + DECL_SORT(s2) \ DECL_LEFT_FUNC(left, {s}, s) \ DECL_RIGHT_FUNC(right, {s}, s) \ + DECL_POLY_CONST(h, 1, alpha) \ DECL_FUNC(f, {s, s}, s) \ DECL_FUNC(g, {s}, s) \ DECL_CONST(a, s) \ DECL_CONST(b, s) \ + DECL_CONST(c, s2) \ DECL_PRED (p, {s}) \ DECL_PRED (q, {s}) @@ -179,4 +183,34 @@ TEST_SIMPLIFICATION(test15, .expected({ clause({ g(left(b)) == left(a) }) }) ) +// demodulation with variable equality +TEST_SIMPLIFICATION(test16, + tester() + .simplifyWith({ clause({ TermSugar(TermList::var(0), s) == b }) }) + .toSimplify({ clause({ f(b,a) != a }) }) + .expected({ clause({ b != a }) }) +) + +TEST_SIMPLIFICATION(test17, + tester() + .simplifyWith({ clause({ x == h(y) }) }) + .toSimplify({ clause({ f(f(b,a),a) != a }) }) + .expected({ clause({ h(s) != a }) }) +) + +TEST_SIMPLIFICATION(test18, + tester() + .simplifyWith({ clause({ y == h(x) }) }) + .toSimplify({ clause({ f(f(b,a),a) != a }) }) + .expected({ clause({ h(s) != a }) }) +) + +TEST_SIMPLIFICATION(test19, + tester() + .simplifyWith({ clause({ x == c }) }) + .toSimplify({ clause({ f(f(b,a),a) != a }) }) + .expected({ /* nothing */ }) + .justifications({ /* nothing */ }) +) + }