Skip to content

Commit

Permalink
Review
Browse files Browse the repository at this point in the history
  • Loading branch information
@mezpusz
mezpusz committed Mar 11, 2024
1 parent c2fca0b commit bb662a0
Show file tree
Hide file tree
Showing 13 changed files with 173 additions and 101 deletions.
68 changes: 18 additions & 50 deletions Inferences/FunctionDefinitionRewriting.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,57 +37,25 @@ using namespace Lib;
using namespace Kernel;
using namespace Saturation;

struct FunctionDefinitionRewriting::GeneralizationsFn {
GeneralizationsFn(FunctionDefinitionHandler *index) : _index(index) {}
VirtualIterator<std::pair<std::pair<Literal*, Term*>, TermQueryResult>> operator()(std::pair<Literal*, Term*> arg)
{
return pvi(pushPairIntoRightIterator(arg, _index->getGeneralizations(arg.second)));
}

private:
FunctionDefinitionHandler *_index;
};

struct FunctionDefinitionRewriting::RewriteableSubtermsFn {
VirtualIterator<std::pair<Literal*, Term*>> operator()(Literal *lit)
{
NonVariableNonTypeIterator nvi(lit);
return pvi(pushPairIntoRightIterator(lit,
getUniquePersistentIteratorFromPtr(&nvi)));
}
};

struct FunctionDefinitionRewriting::ForwardResultFn {
ForwardResultFn(Clause *cl) : _cl(cl) {}

Clause* operator()(std::pair<std::pair<Literal*, Term*>, 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<Literal*, Term*> arg){
return pvi(pushPairIntoRightIterator(arg,
GeneratingInferenceEngine::_salg->getFunctionDefinitionHandler()->getGeneralizations(arg.second)));
})
.map([premise](std::pair<std::pair<Literal*, Term*>, 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)
Expand Down
11 changes: 7 additions & 4 deletions Inferences/FunctionDefinitionRewriting.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
57 changes: 28 additions & 29 deletions Inferences/Induction.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]) {
Expand Down Expand Up @@ -83,6 +85,8 @@ Term* getPlaceholderForTerm(const vvector<Term*>& 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());
}
Expand Down Expand Up @@ -130,6 +134,8 @@ Formula* InductionContext::getFormula(const vvector<TermList>& 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<Term*,TermList> replacementMap;
for (unsigned i = 0; i < _indTerms.size(); i++) {
auto ph = getPlaceholderForTerm(_indTerms,i);
Expand Down Expand Up @@ -181,7 +187,8 @@ Formula* InductionContext::getFormulaWithSquashedSkolems(const vvector<TermList>
return res;
}

vmap<Term*,TermList> getContextReplacementMap(const InductionContext& context, bool inverse = false) {
vmap<Term*,TermList> getContextReplacementMap(const InductionContext& context, bool inverse = false)
{
vmap<Term*,TermList> m;
for (unsigned i = 0; i < context._indTerms.size(); i++) {
auto ph = getPlaceholderForTerm(context._indTerms,i);
Expand Down Expand Up @@ -280,9 +287,15 @@ VirtualIterator<InductionContext> contextReplacementInstance(const InductionCont
auto ctx = context;
auto res = VirtualIterator<InductionContext>::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;
Expand Down Expand Up @@ -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();
}
Expand All @@ -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++) {
Expand Down Expand Up @@ -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]);
Expand Down Expand Up @@ -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()) {
Expand Down Expand Up @@ -578,7 +590,7 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit)
if (templ) {
vvector<Term*> indTerms;
if (templ->matchesTerm(lit, indTerms)) {
vvector<Term*> typeArgs; //(lit->numTypeArguments());
vvector<Term*> typeArgs;
for (unsigned i = 0; i < lit->numTypeArguments(); i++) {
typeArgs.push_back(lit->nthArgument(i)->term());
}
Expand Down Expand Up @@ -619,7 +631,7 @@ void InductionClauseIterator::processLiteral(Clause* premise, Literal* lit)
if (templ) {
vvector<Term*> indTerms;
if (templ->matchesTerm(t, indTerms)) {
vvector<Term*> typeArgs; //(t->numTypeArguments());
vvector<Term*> typeArgs;
for (unsigned i = 0; i < t->numTypeArguments(); i++) {
typeArgs.push_back(t->nthArgument(i)->term());
}
Expand Down Expand Up @@ -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);
Expand All @@ -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);
Expand Down
Loading

0 comments on commit bb662a0

Please sign in to comment.