From bb662a0061e79153e45d4a2ed244fb6d878a1f08 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Mon, 11 Mar 2024 15:10:11 +0100 Subject: [PATCH] Review --- Inferences/FunctionDefinitionRewriting.cpp | 68 +++++------------- Inferences/FunctionDefinitionRewriting.hpp | 11 +-- Inferences/Induction.cpp | 57 ++++++++------- Inferences/Induction.hpp | 81 +++++++++++++++++++++- Inferences/InductionHelper.cpp | 10 ++- Inferences/InductionHelper.hpp | 2 +- Kernel/Signature.cpp | 2 +- Kernel/Signature.hpp | 9 +++ Parse/SMTLIB2.cpp | 10 +-- Shell/FunctionDefinitionHandler.cpp | 11 ++- Shell/FunctionDefinitionHandler.hpp | 6 +- Shell/Options.cpp | 2 + Shell/TermAlgebra.hpp | 5 ++ 13 files changed, 173 insertions(+), 101 deletions(-) diff --git a/Inferences/FunctionDefinitionRewriting.cpp b/Inferences/FunctionDefinitionRewriting.cpp index 7032d5e2d9..6b77c3825a 100644 --- a/Inferences/FunctionDefinitionRewriting.cpp +++ b/Inferences/FunctionDefinitionRewriting.cpp @@ -37,57 +37,25 @@ using namespace Lib; using namespace Kernel; using namespace Saturation; -struct FunctionDefinitionRewriting::GeneralizationsFn { - GeneralizationsFn(FunctionDefinitionHandler *index) : _index(index) {} - VirtualIterator, TermQueryResult>> operator()(std::pair arg) - { - return pvi(pushPairIntoRightIterator(arg, _index->getGeneralizations(arg.second))); - } - -private: - FunctionDefinitionHandler *_index; -}; - -struct FunctionDefinitionRewriting::RewriteableSubtermsFn { - VirtualIterator> operator()(Literal *lit) - { - NonVariableNonTypeIterator nvi(lit); - return pvi(pushPairIntoRightIterator(lit, - getUniquePersistentIteratorFromPtr(&nvi))); - } -}; - -struct FunctionDefinitionRewriting::ForwardResultFn { - ForwardResultFn(Clause *cl) : _cl(cl) {} - - Clause* operator()(std::pair, TermQueryResult> arg) - { - TermQueryResult &qr = arg.second; - bool temp; - return FunctionDefinitionRewriting::perform(_cl, arg.first.first, TermList(arg.first.second), qr.clause, - qr.literal, qr.term, qr.unifier, false, temp, - Inference(GeneratingInference2(InferenceRule::FUNCTION_DEFINITION_REWRITING, _cl, qr.clause))); - } -private: - Clause *_cl; -}; - -ClauseIterator FunctionDefinitionRewriting::generateClauses(Clause *premise) +Kernel::ClauseIterator FunctionDefinitionRewriting::generateClauses(Clause *premise) { - auto itf1 = premise->iterLits(); - - // Get an iterator of pairs of selected literals and rewritable subterms - // of those literals. Here all subterms of a literal are rewritable. - auto itf2 = getMapAndFlattenIterator(itf1, RewriteableSubtermsFn()); - - // Get clauses with a function definition literal whose lhs is a generalization of the rewritable subterm, - // returns a pair with the original pair and the generalization result (includes substitution) - auto itf3 = getMapAndFlattenIterator(itf2, GeneralizationsFn(GeneratingInferenceEngine::_salg->getFunctionDefinitionHandler())); - - //Perform forward rewriting - auto it = pvi(getMappingIterator(itf3, ForwardResultFn(premise))); - // Remove null elements - return pvi(getFilteredIterator(it, NonzeroFn())); + return pvi(premise->iterLits() + .flatMap([](Literal *lit) { + NonVariableNonTypeIterator nvi(lit); + return pvi(pushPairIntoRightIterator(lit, getUniquePersistentIteratorFromPtr(&nvi))); + }) + .flatMap([this](std::pair arg){ + return pvi(pushPairIntoRightIterator(arg, + GeneratingInferenceEngine::_salg->getFunctionDefinitionHandler()->getGeneralizations(arg.second))); + }) + .map([premise](std::pair, TermQueryResult> arg) { + TermQueryResult &qr = arg.second; + bool temp; + return (Clause*)FunctionDefinitionRewriting::perform(premise, arg.first.first, TermList(arg.first.second), qr.clause, + qr.literal, qr.term, qr.unifier, false, temp, + Inference(GeneratingInference2(InferenceRule::FUNCTION_DEFINITION_REWRITING, premise, qr.clause))); + }) + .filter(NonzeroFn())); } bool FunctionDefinitionRewriting::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) diff --git a/Inferences/FunctionDefinitionRewriting.hpp b/Inferences/FunctionDefinitionRewriting.hpp index 148281194e..02cb6dae9a 100644 --- a/Inferences/FunctionDefinitionRewriting.hpp +++ b/Inferences/FunctionDefinitionRewriting.hpp @@ -22,6 +22,13 @@ namespace Inferences { using namespace Kernel; using namespace Shell; +/** + * Inference implementing function definition rewriting. + * Function definitions are assumed to be available when saturation begins, + * so there is only a forward version of the inference. Moreover, we use + * a forward simplification variant to eagerly perform rewritings which + * are also demodulations. + */ class FunctionDefinitionRewriting : public GeneratingInferenceEngine , public ForwardSimplificationEngine @@ -38,10 +45,6 @@ class FunctionDefinitionRewriting Clause *eqClause, Literal *eqLiteral, TermList eqLHS, ResultSubstitutionSP subst, bool toplevelCheck, bool& isEqTautology, const Inference& inf, SaturationAlgorithm* salg = nullptr); - - struct ForwardResultFn; - struct RewriteableSubtermsFn; - struct GeneralizationsFn; }; }; // namespace Inferences diff --git a/Inferences/Induction.cpp b/Inferences/Induction.cpp index 3ec2de26b9..04eb86b0dc 100644 --- a/Inferences/Induction.cpp +++ b/Inferences/Induction.cpp @@ -52,6 +52,8 @@ Term* ActiveOccurrenceIterator::next() InductionTemplate* templ = _fnDefHandler ? _fnDefHandler->getInductionTemplate(t) : nullptr; if (templ) { + // if there is an induction template, + // only induct on the active occurrences auto& actPos = templ->inductionPositions(); for (unsigned i = t->numTypeArguments(); i < t->arity(); i++) { if (actPos[i]) { @@ -83,6 +85,8 @@ Term* getPlaceholderForTerm(const vvector& ts, unsigned i) TermList TermReplacement::transformSubterm(TermList trm) { + // if we reach any of the mapped terms, + // replace it with the term it is mapped to if(trm.isTerm() && _m.count(trm.term())){ return _m.at(trm.term()); } @@ -130,6 +134,8 @@ Formula* InductionContext::getFormula(const vvector& r, bool opposite, { ASS_EQ(_indTerms.size(), r.size()); + // Assuming this object is the result of a ContextReplacement (or similar iterator) + // we can replace the ith placeholder with the ith term in r. vmap replacementMap; for (unsigned i = 0; i < _indTerms.size(); i++) { auto ph = getPlaceholderForTerm(_indTerms,i); @@ -181,7 +187,8 @@ Formula* InductionContext::getFormulaWithSquashedSkolems(const vvector return res; } -vmap getContextReplacementMap(const InductionContext& context, bool inverse = false) { +vmap getContextReplacementMap(const InductionContext& context, bool inverse = false) +{ vmap m; for (unsigned i = 0; i < context._indTerms.size(); i++) { auto ph = getPlaceholderForTerm(context._indTerms,i); @@ -280,9 +287,15 @@ VirtualIterator contextReplacementInstance(const InductionCont auto ctx = context; auto res = VirtualIterator::getEmpty(); if (opt.inductionOnActiveOccurrences()) { + // In case of using active occurrences, we replace the input + // context with one where the active occurrences are already + // replaced, so that we only iterate on the rest of them below. ActiveOccurrenceContextReplacement aor(context, fnDefHandler); ASS(aor.hasNext()); auto ao_ctx = aor.next(); + // If there are no active occurrences, we get an empty context + // and we simply fall back to inducting on all occurrences. + // // TODO do this filtering inside ActiveOccurrenceContextReplacement if (!ao_ctx._cls.empty()) { ctx = ao_ctx; @@ -317,6 +330,7 @@ ContextSubsetReplacement::ContextSubsetReplacement(const InductionContext& conte _iteration[i] = _maxIterations[i]-1; } } + // find first iteration that shouldn't be skipped while (!_done && shouldSkipIteration()) { stepIteration(); } @@ -343,22 +357,18 @@ bool ContextSubsetReplacement::hasNext() return !_done; } _ready = true; - // Increment _iteration, since it either is 0, or was already used. - // _iteration++; - // unsigned setBits = BitUtils::oneBits(_iteration); - // // Skip this iteration if not all bits are set, but more than maxSubset are set. - // while (hasNextInner() && - // ((_maxSubsetSize > 0) && (setBits < _occurrences) && (setBits > _maxSubsetSize))) { - // _iteration++; - // setBits = BitUtils::oneBits(_iteration); - stepIteration(); - while (!_done && shouldSkipIteration()) { + // we step forward until we find an + // iteration which shouldn't be skipped + // or we run out of iterations + do { stepIteration(); - } + } while (!_done && shouldSkipIteration()); + return !_done; } -InductionContext ContextSubsetReplacement::next() { +InductionContext ContextSubsetReplacement::next() +{ ASS(_ready); InductionContext context(_context._indTerms); for (unsigned i = 0; i < _context._indTerms.size(); i++) { @@ -386,6 +396,8 @@ InductionContext ContextSubsetReplacement::next() { bool ContextSubsetReplacement::shouldSkipIteration() const { + // We skip an iteration if too many (but not all) + // occurrences of an induction term are used. const bool subsetSizeCheck = _maxSubsetSize > 0; for (unsigned i = 0; i < _iteration.size(); i++) { unsigned setBits = __builtin_popcount(_iteration[i]); @@ -492,7 +504,7 @@ struct InductionContextFn } auto indTerm = arg.first[0]; // check for complex term and non-equality - if (_lit->isEquality()/* || !indTerm->arity() */) { + if (_lit->isEquality() || !indTerm->arity()) { return res; } while (arg.second.hasNext()) { @@ -578,7 +590,7 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit) if (templ) { vvector indTerms; if (templ->matchesTerm(lit, indTerms)) { - vvector typeArgs; //(lit->numTypeArguments()); + vvector typeArgs; for (unsigned i = 0; i < lit->numTypeArguments(); i++) { typeArgs.push_back(lit->nthArgument(i)->term()); } @@ -619,7 +631,7 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit) if (templ) { vvector indTerms; if (templ->matchesTerm(t, indTerms)) { - vvector typeArgs; //(t->numTypeArguments()); + vvector typeArgs; for (unsigned i = 0; i < t->numTypeArguments(); i++) { typeArgs.push_back(t->nthArgument(i)->term()); } @@ -1571,15 +1583,6 @@ void InductionClauseIterator::performRecursionInduction(const InductionContext& e->add(std::move(cls), std::move(subst)); } -// Whether an induction formula is applicable (or has already been generated) -// is determined by its conclusion part, which is resolved against the literals -// and bounds we induct on. From this point of view, an integer induction formula -// can have one lower bound and/or one upper bound. This function wraps this -// information by adding the bounds and querying the index with the resulting context. -// -// TODO: default bounds are now stored as special cases with no bounds (this makes -// the resolve part easier) but this means some default bound induction formulas -// are duplicates of normal formulas. bool InductionClauseIterator::notDoneInt(InductionContext context, Literal* bound1, Literal* bound2, InductionFormulaIndex::Entry*& e) { ASS_EQ(context._indTerms.size(), 1); @@ -1599,10 +1602,6 @@ bool InductionClauseIterator::notDoneInt(InductionContext context, Literal* boun return _formulaIndex.findOrInsert(context, e, b1, b2); } -// If the integer induction literal is a comparison, and the induction term is -// one of its arguments, the other argument should not be allowed as a bound -// (such inductions are useless and can lead to redundant literals in the -// induction axiom). bool InductionClauseIterator::isValidBound(const InductionContext& context, const TermQueryResult& bound) { ASS_EQ(context._indTerms.size(), 1); diff --git a/Inferences/Induction.hpp b/Inferences/Induction.hpp index 3a4f3df1c2..9a0cb6dd55 100644 --- a/Inferences/Induction.hpp +++ b/Inferences/Induction.hpp @@ -48,6 +48,12 @@ using namespace Saturation; using namespace Shell; using namespace Lib; +/** + * This class is similar to @b NonVariableNonTypeIterator and is + * used to iterate over terms in active positions inside a literal. + * The active positions are given by a @b FunctionDefinitionHandler + * instance. + */ class ActiveOccurrenceIterator : public IteratorCore { @@ -67,17 +73,33 @@ class ActiveOccurrenceIterator FunctionDefinitionHandler* _fnDefHandler; }; +/** + * Hash used to make hashing over shared terms deterministic. + */ struct SharedTermHash { static bool equals(Term* t1, Term* t2) { return t1==t2; } static unsigned hash(Term* t) { return t->getId(); } }; +/** + * Hash used to make hashing over clauses deterministic. + */ struct StlClauseHash { std::size_t operator()(Clause* c) const { return std::hash()(c->number()); } }; +/** + * This function replaces the induction terms given in @b ts + * with static placeholders, so that already generated induction + * formulas can be easily detected. We allow multiple induction terms, + * so we have to index the placeholders as well with @b i. + */ Term* getPlaceholderForTerm(const vvector& ts, unsigned i); +/** + * Term transformer class that replaces + * terms according to the mapping @b _m. + */ class TermReplacement : public TermTransformer { public: TermReplacement(const vmap& m) : _m(m) {} @@ -86,6 +108,10 @@ class TermReplacement : public TermTransformer { vmap _m; }; +/** + * Same as @b TermReplacement, except we replace non-sort Skolems + * with variables, used for strengthening induction hypotheses. + */ class SkolemSquashingTermReplacement : public TermReplacement { public: SkolemSquashingTermReplacement(const vmap& m, unsigned& var) @@ -93,9 +119,15 @@ class SkolemSquashingTermReplacement : public TermReplacement { TermList transformSubterm(TermList trm) override; DHMap _tv; // maps terms to their variable replacement private: - unsigned& _v; // fresh variable counter supported by caller + unsigned& _v; // fresh variable counter supported by caller }; +/** + * Class representing an induction. This includes: + * - induction terms in @b _indTerms, + * - selected literals from clauses in @b _cls, + * which are inducted upon. + */ struct InductionContext { explicit InductionContext(vvector&& ts) : _indTerms(ts) {} @@ -113,6 +145,9 @@ struct InductionContext { node->second.push(lit); } + // These two functions should be only called on objects where + // all induction term occurrences actually inducted upon are + // replaced with placeholders (e.g. with ContextReplacement). Formula* getFormula(const vvector& r, bool opposite, Substitution* subst = nullptr) const; Formula* getFormulaWithSquashedSkolems(const vvector& r, bool opposite, unsigned& var, VList** varList = nullptr, Substitution* subst = nullptr) const; @@ -141,9 +176,20 @@ struct InductionContext { // clause as well. vunordered_map _cls; private: + /** + * Creates a formula which corresponds to the conjunction of disjunction + * of selected literals for each clause in @b _cls, where we apply the term + * replacement @b tr on each literal. Opposite means we get the negated + * formula, i.e. each literal is negated and conjunction and disjunction + * are switched. + */ Formula* getFormula(TermReplacement& tr, bool opposite) const; }; +/** + * Gives @b InductionContext instances with + * induction terms replaced with placeholders. + */ class ContextReplacement : public TermReplacement, public IteratorCore { public: @@ -159,6 +205,10 @@ class ContextReplacement bool _used; }; +/** + * Same as @b ContextReplacement but replaces only active occurrences + * of induction terms, given by a @b FunctionDefinitionHandler instance. + */ class ActiveOccurrenceContextReplacement : public ContextReplacement { public: @@ -176,6 +226,11 @@ class ActiveOccurrenceContextReplacement bool _hasNonActive; }; +/** + * Same as @b ContextReplacement but iterates over all non-empty + * subsets of occurrences of the induction terms and replaces + * only the occurrences in these subsets with placeholder terms. + */ class ContextSubsetReplacement : public ContextReplacement { public: @@ -201,6 +256,9 @@ class ContextSubsetReplacement bool _done; }; +/** + * The induction inference. + */ class Induction : public GeneratingInferenceEngine { @@ -227,6 +285,10 @@ class Induction InductionFormulaIndex _recFormulaIndex; }; +/** + * Helper class that generates all induction clauses for + * a premise and serves as an iterator for these clauses. + */ class InductionClauseIterator { public: @@ -265,8 +327,25 @@ class InductionClauseIterator void performStructInductionThree(const InductionContext& context, InductionFormulaIndex::Entry* e); void performRecursionInduction(const InductionContext& context, const InductionTemplate* templ, const vvector& typeArgs, InductionFormulaIndex::Entry* e); + /** + * Whether an induction formula is applicable (or has already been generated) + * is determined by its conclusion part, which is resolved against the literals + * and bounds we induct on. From this point of view, an integer induction formula + * can have one lower bound and/or one upper bound. This function wraps this + * information by adding the bounds and querying the index with the resulting context. + * + * TODO: default bounds are now stored as special cases with no bounds (this makes + * the resolve part easier) but this means some default bound induction formulas + * are duplicates of normal formulas. + */ bool notDoneInt(InductionContext context, Literal* bound1, Literal* bound2, InductionFormulaIndex::Entry*& e); + /** + * If the integer induction literal is a comparison, and the induction term is + * one of its arguments, the other argument should not be allowed as a bound + * (such inductions are useless and can lead to redundant literals in the + * induction axiom). + */ bool isValidBound(const InductionContext& context, const TermQueryResult& bound); Stack _clauses; diff --git a/Inferences/InductionHelper.cpp b/Inferences/InductionHelper.cpp index c60d48e088..9d5a40552e 100644 --- a/Inferences/InductionHelper.cpp +++ b/Inferences/InductionHelper.cpp @@ -255,13 +255,11 @@ bool InductionHelper::isStructInductionTerm(Term* t) { Term* InductionHelper::getOtherTermFromComparison(Literal* l, Term* t) { if (isIntegerComparisonLiteral(l)) { + ASS(l->ground()); + ASS_EQ(l->arity(),2); for (unsigned i = 0; i < 2; ++i) { - TermList* tp1 = l->nthArgument(i); - if (tp1->isTerm() && t == tp1->term()) { - TermList* tp2 = l->nthArgument(1-i); - if (tp2->isTerm()) { - return tp2->term(); - } + if (l->termArg(i).term() == t) { + return l->termArg(1-i).term(); } } } diff --git a/Inferences/InductionHelper.hpp b/Inferences/InductionHelper.hpp index 4e3c7a0479..a2629a5dfd 100644 --- a/Inferences/InductionHelper.hpp +++ b/Inferences/InductionHelper.hpp @@ -54,7 +54,7 @@ class InductionHelper { static bool isStructInductionTerm(Term* t); static bool isValidBound(Term* t, Clause* c, const TermQueryResult& b) { ASS(b.term.isTerm()); - return (b.clause != c && (t != b.term.term())); + return ((b.clause != c) && (t != b.term.term())); } static Term* getOtherTermFromComparison(Literal* l, Term* t); diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp index 887097b441..0d1e0c0cf4 100644 --- a/Kernel/Signature.cpp +++ b/Kernel/Signature.cpp @@ -702,7 +702,7 @@ unsigned Signature::getFnDef(unsigned fn) auto type = getFunction(fn)->fnType(); auto sort = type->result(); bool added = false; - auto name = "$def_"+sort.toString(); + auto name = "$def_"+getFunction(fn)->name(); unsigned p = addPredicate(name, 2, added); if (added) { ALWAYS(_fnDefPreds.insert(p)); diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index 5ca494dfac..38bd5eb891 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -435,7 +435,16 @@ class Signature unsigned getApp(); unsigned getDiff(); unsigned getChoice(); + /** + * For a function f with result type t, this introduces a predicate + * $def_f with the type t x t. This is used to track expressions of + * the form f(s) = s' as $def_f(f(s),s') through preprocessing. + */ unsigned getFnDef(unsigned fn); + /** + * For a predicate p, this introduces a predicate $def_p with the same signature, + * which is used to track a predicate definition "headers" through preprocessing. + */ unsigned getBoolDef(unsigned fn); // Interpreted symbol declarations diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp index 680ee3cf64..bc82dd4235 100644 --- a/Parse/SMTLIB2.cpp +++ b/Parse/SMTLIB2.cpp @@ -772,7 +772,7 @@ SMTLIB2::DeclaredSymbol SMTLIB2::declareFunctionOrPredicate(const vstring& name, // ---------------------------------------------------------------------- -bool shouldCreateFunctionDefinition(unsigned fn) +bool shouldCreateFunctionDefinition() { return env.options->functionDefinitionRewriting() || env.options->inductionOnActiveOccurrences() || env.options->structInduction()==Options::StructuralInductionKind::RECURSION; @@ -844,7 +844,7 @@ void SMTLIB2::readDefineFun(const vstring& name, LExprList* iArgs, LExpr* oSort, Literal* lit; if (isTrueFun) { TermList lhs(Term::create(symbIdx,args.size(),args.begin())); - if (shouldCreateFunctionDefinition(symbIdx)) { + if (shouldCreateFunctionDefinition()) { auto p = env.signature->getFnDef(symbIdx); auto defArgs = typeArgs; defArgs.push(lhs); @@ -854,7 +854,7 @@ void SMTLIB2::readDefineFun(const vstring& name, LExprList* iArgs, LExpr* oSort, lit = Literal::createEquality(true,lhs,rhs,rangeSort); } } else { - if (shouldCreateFunctionDefinition(symbIdx)) { + if (shouldCreateFunctionDefinition()) { auto p = env.signature->getBoolDef(symbIdx); lit = Literal::create(p,args.size(),true,false,args.begin()); } else { @@ -949,7 +949,7 @@ void SMTLIB2::readDefineFunsRec(LExprList* declsExpr, LExprList* defsExpr) Literal* lit; if (isTrueFun) { TermList lhs(Term::create(symbIdx,decl.args.size(),decl.args.begin())); - if (shouldCreateFunctionDefinition(symbIdx)) { + if (shouldCreateFunctionDefinition()) { auto p = env.signature->getFnDef(symbIdx); TermStack defArgs; // no type arguments (yet) in this case defArgs.push(lhs); @@ -959,7 +959,7 @@ void SMTLIB2::readDefineFunsRec(LExprList* declsExpr, LExprList* defsExpr) lit = Literal::createEquality(true,lhs,rhs,decl.rangeSort); } } else { - if (shouldCreateFunctionDefinition(symbIdx)) { + if (shouldCreateFunctionDefinition()) { auto p = env.signature->getBoolDef(symbIdx); lit = Literal::create(p,decl.args.size(),true,false,decl.args.begin()); } else { diff --git a/Shell/FunctionDefinitionHandler.cpp b/Shell/FunctionDefinitionHandler.cpp index 30747d7a2c..819e162e19 100644 --- a/Shell/FunctionDefinitionHandler.cpp +++ b/Shell/FunctionDefinitionHandler.cpp @@ -287,11 +287,12 @@ bool InductionTemplate::checkUsefulness() const bool InductionTemplate::checkWellFoundedness() { - // fill in bit vector of induction variables vvector> relatedTerms; for (auto& b : _branches) { for (auto& r : b._recursiveCalls) { relatedTerms.push_back(make_pair(b._header, r)); + + // fill in bit vector of induction variables for (unsigned i = 0; i < _arity; i++) { if (env.signature->isTermAlgebraSort(_type->arg(i))) { _indPos[i] = _indPos[i] || (*b._header->nthArgument(i) != *r->nthArgument(i)); @@ -361,6 +362,10 @@ vstring InductionTemplate::toString() const return str.str(); } +/** + * Try to find a lexicographic order between the arguments + * by exhaustively trying all combinations. + */ bool checkWellFoundednessHelper(const vvector>& relatedTerms, const vset& indices, const vset& positions) { @@ -422,6 +427,10 @@ bool InductionPreprocessor::checkWellFoundedness(const vvector return checkWellFoundednessHelper(relatedTerms, indices, positions); } +/** + * Check well-definedness for term algebra arguments and + * in the process generate all missing cases. + */ bool InductionPreprocessor::checkWellDefinedness(const vvector& cases, vvector>& missingCases) { if (cases.empty()) { diff --git a/Shell/FunctionDefinitionHandler.hpp b/Shell/FunctionDefinitionHandler.hpp index be8ddbcde3..747a240215 100644 --- a/Shell/FunctionDefinitionHandler.hpp +++ b/Shell/FunctionDefinitionHandler.hpp @@ -28,9 +28,9 @@ using namespace Kernel; using namespace Lib; /** - * Corresponds to the branches of a function definition. - * Stores the branches and the active positions - * (i.e. the changing arguments) of the function. + * Corresponds to the branches of a function definition, + * including recursive calls and the active argument positions + * which are not variables in some branch. */ struct InductionTemplate { USE_ALLOCATOR(InductionTemplate); diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 6b58d094a2..5f9a21e3fb 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -1291,6 +1291,8 @@ void Options::init() _structInduction.onlyUsefulWith(Or(_induction.is(equal(Induction::STRUCTURAL)),_induction.is(equal(Induction::BOTH)))); _structInduction.addHardConstraint(If(equal(StructuralInductionKind::RECURSION)).then(_newCNF.is(equal(true)))); _structInduction.addHardConstraint(If(equal(StructuralInductionKind::RECURSION)).then(_equalityResolutionWithDeletion.is(equal(true)))); + _structInduction.addHardConstraint(If(equal(StructuralInductionKind::ALL)).then(_newCNF.is(equal(true)))); + _structInduction.addHardConstraint(If(equal(StructuralInductionKind::ALL)).then(_equalityResolutionWithDeletion.is(equal(true)))); _lookup.insert(&_structInduction); _intInduction = ChoiceOptionValue("int_induction_kind","iik", diff --git a/Shell/TermAlgebra.hpp b/Shell/TermAlgebra.hpp index 43f3800d93..0efecbe214 100644 --- a/Shell/TermAlgebra.hpp +++ b/Shell/TermAlgebra.hpp @@ -157,6 +157,11 @@ namespace Shell { unsigned getSubtermPredicate(); void getTypeSub(Kernel::Term* t, Kernel::Substitution& subst); + /** + * Given a set of (possibly variable) term algebra terms in @b availables + * and a term algebra term @b e, compute a new set of terms in @b availables + * which covers the same term algebra terms, except for terms covered by @b e. + */ static void excludeTermFromAvailables(Kernel::TermStack& availables, Kernel::TermList e, unsigned& var); friend std::ostream& operator<<(std::ostream& out, TermAlgebra const& self);