From 119524f2bc7ba684db631e5657cb5f1d001a53fd Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Tue, 28 Jul 2026 16:00:12 +0200 Subject: [PATCH] Add predicate elimination as a new preprocessing step (option: -pel, default off) Implements the technique of Khasidashvili and Korovin (SAT 2016): a predicate P occurring at most once in every clause is eliminated by replacing S_P and S_~P with all pairwise resolvents on P. On problems without equality and theories, resolvents are computed with an mgu and non-unifiable pairs dropped; otherwise the P-literals are (virtually) flattened, introducing argument disequalities which are then simplified away by exhaustive equality substitution (this can introduce equality into a problem previously without it). FMB forces the equational mode, since its model reconstruction cannot rely on the Herbrand-interpretation argument justifying the mgu variant. Elimination steps are gated SAT-VE-style by growth limits on the estimated clause count |S_P|*|S_~P| - |S_P| - |S_~P|: a per-step tolerance factor over the current total (-pelst, default 1.05) and a global cap relative to the original total (-peltl, default 2.0). Syntactic tautologies (complementary pair, t != t, s = s) and duplicate literals are removed from generated resolvents, and the actual surviving count feeds back into the budget. The next predicate to eliminate is by default the one with the smallest estimated growth (pure predicates thus go first, their clauses being simply deleted); with -pelr the choice is uniformly random among the admissible candidates (controlled by random_seed), since the process is not confluent. With -pels, the clause set is kept forward-inter-subsumed throughout, using a standalone LiteralSubstitutionTree index (unit literal, or the least matchable one) plus SATSubsumptionAndResolution; backward subsumption is left as future work. Every elimination records a model-repairing definition P(xs) <=> \/_{D \/ P(ts) in S_P} exists ys. (xs = ts /\ ~D) via Problem::addEliminatedPredicate (addTrivialPredicate for pure ones), so both the textual model updates output and FMB model restoration stay correct (verified via --mode model_check). Skipped for higher-order/polymorphic inputs (predicates could hide inside terms, breaking the occurrence counting) and for color-annotated problems. Co-Authored-By: Claude Fable 5 --- Kernel/Inference.cpp | 2 + Kernel/Inference.hpp | 2 + Makefile | 1 + Shell/Options.cpp | 28 ++ Shell/Options.hpp | 6 + Shell/PredicateElimination.cpp | 694 ++++++++++++++++++++++++++++ Shell/PredicateElimination.hpp | 132 ++++++ Shell/Preprocess.cpp | 19 + Shell/Statistics.cpp | 6 + Shell/Statistics.hpp | 9 + UnitTests/tPredicateElimination.cpp | 374 +++++++++++++++ cmake/sources.cmake | 3 + samplers/samplerFNT.smp | 9 + samplers/samplerFOL.smp | 9 + samplers/samplerHOL.smp | 9 + samplers/samplerIND.smp | 9 + samplers/samplerSMT.smp | 9 + 17 files changed, 1321 insertions(+) create mode 100644 Shell/PredicateElimination.cpp create mode 100644 Shell/PredicateElimination.hpp create mode 100644 UnitTests/tPredicateElimination.cpp diff --git a/Kernel/Inference.cpp b/Kernel/Inference.cpp index 1ff8af68eb..df3d76aa8c 100644 --- a/Kernel/Inference.cpp +++ b/Kernel/Inference.cpp @@ -673,6 +673,8 @@ std::string Kernel::ruleName(InferenceRule rule) return "unused predicate definition removal"; case InferenceRule::PURE_PREDICATE_REMOVAL: return "pure predicate removal"; + case InferenceRule::PREDICATE_ELIMINATION: + return "predicate elimination"; case InferenceRule::INEQUALITY_SPLITTING: return "inequality splitting"; case InferenceRule::INEQUALITY_SPLITTING_NAME_INTRODUCTION: diff --git a/Kernel/Inference.hpp b/Kernel/Inference.hpp index 7ef5f3e2dc..573e344ae4 100644 --- a/Kernel/Inference.hpp +++ b/Kernel/Inference.hpp @@ -389,6 +389,8 @@ enum class InferenceRule : unsigned char { UNUSED_PREDICATE_DEFINITION_REMOVAL, /** pure predicate removal */ PURE_PREDICATE_REMOVAL, + /** predicate elimination by exhaustive resolution (preprocessing) */ + PREDICATE_ELIMINATION, /** inequality splitting */ INEQUALITY_SPLITTING, /** inequality splitting name introduction */ diff --git a/Makefile b/Makefile index 317ccb48cb..58259fb17e 100644 --- a/Makefile +++ b/Makefile @@ -392,6 +392,7 @@ VS_OBJ = Shell/AnswerLiteralManager.o\ Shell/TheoryFlattening.o\ Shell/TweeGoalTransformation.o\ Shell/BlockedClauseElimination.o\ + Shell/PredicateElimination.o\ Shell/Token.o\ Shell/TPTPPrinter.o\ Shell/UIHelper.o\ diff --git a/Shell/Options.cpp b/Shell/Options.cpp index d2b102602d..3c8ad328ff 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -570,6 +570,34 @@ void Options::init() _blockedClauseElimination.tag(OptionTag::PREPROCESSING); _blockedClauseElimination.addProblemConstraint(notWithCat(Property::UEQ)); + _predicateElimination = BoolOptionValue("predicate_elimination","pel",false); + _predicateElimination.description= + "After clausification, eliminate predicates that occur at most once in every clause" + " by replacing their clauses with all pairwise resolvents (cf. Khasidashvili and Korovin, SAT 2016)." + " On problems without equality and theories, resolvents are computed with an mgu;" + " otherwise argument disequalities are introduced via (virtual) flattening," + " which may add equality to a problem previously without it."; + _lookup.insert(&_predicateElimination); + _predicateElimination.tag(OptionTag::PREPROCESSING); + _predicateElimination.addProblemConstraint(notWithCat(Property::UEQ)); + + _predicateEliminationTotalLimit = FloatOptionValue("predicate_elimination_total_limit","peltl",2.0); + _predicateEliminationTotalLimit.description= + "A predicate elimination step is only performed if the estimated number of clauses afterwards" + " (current - |S_P| - |S_~P| + |S_P|*|S_~P|) does not exceed the number of clauses" + " before predicate elimination started times this factor."; + _lookup.insert(&_predicateEliminationTotalLimit); + _predicateEliminationTotalLimit.tag(OptionTag::PREPROCESSING); + _predicateEliminationTotalLimit.addConstraint(greaterThanEq(0.0f)); + _predicateEliminationTotalLimit.onlyUsefulWith(_predicateElimination.is(equal(true))); + + _predicateEliminationSubsumption = BoolOptionValue("predicate_elimination_subsumption","pels",true); + _predicateEliminationSubsumption.description= + "Keep the clause set forward-inter-subsumed and subsumption-resolved during predicate elimination."; + _lookup.insert(&_predicateEliminationSubsumption); + _predicateEliminationSubsumption.tag(OptionTag::PREPROCESSING); + _predicateEliminationSubsumption.onlyUsefulWith(_predicateElimination.is(equal(true))); + _distinctGroupExpansionLimit = UnsignedOptionValue("distinct_group_expansion_limit","dgel",140); _distinctGroupExpansionLimit.description = "If a distinct group (defined, e.g., via TPTP's $distinct)" " is not larger than this limit, it will be expanded during preprocessing into quadratically many disequalities." diff --git a/Shell/Options.hpp b/Shell/Options.hpp index ee8465a286..79c83d47c3 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -2059,6 +2059,9 @@ bool _hard; bool unusedPredicateDefinitionRemoval() const { return _unusedPredicateDefinitionRemoval.actualValue; } bool blockedClauseElimination() const { return _blockedClauseElimination.actualValue; } + bool predicateElimination() const { return _predicateElimination.actualValue; } + float predicateEliminationTotalLimit() const { return _predicateEliminationTotalLimit.actualValue; } + bool predicateEliminationSubsumption() const { return _predicateEliminationSubsumption.actualValue; } unsigned distinctGroupExpansionLimit() const { return _distinctGroupExpansionLimit.actualValue; } void setUnusedPredicateDefinitionRemoval(bool newVal) { _unusedPredicateDefinitionRemoval.actualValue = newVal; } SatSolver satSolver() const { return _satSolver.actualValue; } @@ -2703,6 +2706,9 @@ bool _hard; ChoiceOptionValue _unitResultingResolution; BoolOptionValue _unusedPredicateDefinitionRemoval; BoolOptionValue _blockedClauseElimination; + BoolOptionValue _predicateElimination; + FloatOptionValue _predicateEliminationTotalLimit; + BoolOptionValue _predicateEliminationSubsumption; UnsignedOptionValue _distinctGroupExpansionLimit; OptionChoiceValues _tagNames; diff --git a/Shell/PredicateElimination.cpp b/Shell/PredicateElimination.cpp new file mode 100644 index 0000000000..3a3904aa7b --- /dev/null +++ b/Shell/PredicateElimination.cpp @@ -0,0 +1,694 @@ +/* + * 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 + */ +/** + * @file PredicateElimination.cpp + * Implements class PredicateElimination. + */ + +#include "PredicateElimination.hpp" + +#include "Kernel/Clause.hpp" +#include "Kernel/EqHelper.hpp" +#include "Kernel/Formula.hpp" +#include "Kernel/FormulaUnit.hpp" +#include "Kernel/Inference.hpp" +#include "Kernel/LiteralByMatchability.hpp" +#include "Kernel/Problem.hpp" +#include "Kernel/RobSubstitution.hpp" +#include "Kernel/Signature.hpp" +#include "Kernel/SortHelper.hpp" +#include "Kernel/SubstHelper.hpp" +#include "Kernel/Term.hpp" +#include "Kernel/Unit.hpp" + +#include "Inferences/InferenceEngine.hpp" + +#include "Lib/Environment.hpp" + +#include "Shell/Options.hpp" +#include "Shell/Shuffling.hpp" +#include "Shell/Statistics.hpp" + +#include "Debug/TimeProfiling.hpp" + +#include + +namespace Shell { + +using namespace std; +using namespace Lib; +using namespace Kernel; +using namespace Indexing; + +/** + * Renames variables by adding a fixed offset. + */ +struct VarShiftApplicator { + unsigned off; + TermList apply(unsigned var) const { return TermList(var + off, false); } +}; + +/** + * Replaces a single variable by a term, leaving other variables intact. + */ +struct SingleVarApplicator { + unsigned var; + TermList term; + TermList apply(unsigned v) const { return v == var ? term : TermList(v, false); } +}; + +void PredicateElimination::apply(Problem &prb) +{ + TIME_TRACE("predicate elimination"); + + // resolving clauses of different colours could produce colour-mixing resolvents + if (env.colorUsed) { + return; + } + + // dropping non-unifiable pairs is only sound if equality and theories don't interfere + _equational = _forceEquationally || prb.hasEquality() || prb.hasInterpretedOperations() || prb.hasNumerals(); + + if (_useSubsumption) { + _subsIndex = new LiteralSubstitutionTree(); + } + + _preds.ensure(env.signature->predicates()); + + // clauses may still contain duplicate literals at this stage of preprocessing; + // besides making our occurrence counting needlessly conservative, they would, + // more importantly, violate an invariant of SATSubsumptionAndResolution + // (which in saturation is maintained by running this very simplification on every new clause) + Inferences::DuplicateLiteralRemovalISE duplicateLiteralRemoval; + + Stack input; + UnitList::Iterator uit(prb.units()); + while (uit.hasNext()) { + Unit *u = uit.next(); + ASS(u->isClause()); + Clause *cl = static_cast(u); + Clause *dedup = duplicateLiteralRemoval.simplify(cl); + if (dedup != cl) { + _modified = true; + cl = dedup; + } + input.push(cl); + } + + if (_useSubsumption) { + // inserting shorter clauses first, the forward check below + // makes the initial clause set fully inter-subsumed + std::stable_sort(input.begin(), input.end(), + [](Clause *a, Clause *b) { return a->length() < b->length(); }); + } + + for (Clause *cl : input) { + if (_useSubsumption) { + Clause *simplified = forwardSimplify(cl); + if (simplified != cl) { // subsumed away, or replaced by a subsumption resolution descendant + _modified = true; + if (!simplified) { + continue; + } + cl = simplified; + } + } + _all.push(cl); + registerClause(cl); + if (_useSubsumption) { + indexInsert(cl); + } + } + _curTotal = _origTotal = _all.size(); + + for (;;) { + int pred = pickCandidate(); + if (pred < 0) { + break; + } + eliminate(prb, (unsigned)pred); + } + + if (_modified) { + UnitList *res = 0; + Stack::Iterator it(_all); + while (it.hasNext()) { + Clause *cl = it.next(); + if (!_deleted.contains(cl)) { + UnitList::push(cl, res); + } + } + prb.units() = res; + if (_keptDisequality) { + prb.reportEqualityAdded(true, _keptVarVarDisequality); + } + prb.invalidateProperty(); + } + + delete _subsIndex; + _subsIndex = nullptr; +} + +void PredicateElimination::registerClause(Clause *cl) +{ + // for each tracked predicate of cl: +1/-1 for a single positive/negative occurrence, 2 for more than one + static DHMap occ; + occ.reset(); + + for (unsigned i = 0; i < cl->length(); i++) { + Literal *lit = (*cl)[i]; + unsigned pred = lit->functor(); + if (env.signature->getPredicate(pred)->protectedSymbol()) { // includes equality, interpreted and answer predicates + continue; + } + ASS(pred); // equality predicate is protected + int *val; + if (occ.getValuePtr(pred, val)) { + *val = lit->isPositive() ? 1 : -1; + } + else { + *val = 2; + } + } + + DHMap::Iterator oit(occ); + while (oit.hasNext()) { + unsigned pred; + int val; + oit.next(pred, val); + if (val == 2) { + _preds[pred].blockers++; + } + else if (val == 1) { + _preds[pred].pos.insert(cl); + } + else { + _preds[pred].neg.insert(cl); + } + } +} + +void PredicateElimination::unregisterClause(Clause *cl) +{ + static DHMap occ; + occ.reset(); + + for (unsigned i = 0; i < cl->length(); i++) { + Literal *lit = (*cl)[i]; + unsigned pred = lit->functor(); + if (env.signature->getPredicate(pred)->protectedSymbol()) { + continue; + } + int *val; + if (occ.getValuePtr(pred, val)) { + *val = lit->isPositive() ? 1 : -1; + } + else { + *val = 2; + } + } + + DHMap::Iterator oit(occ); + while (oit.hasNext()) { + unsigned pred; + int val; + oit.next(pred, val); + if (val == 2) { + ASS_G(_preds[pred].blockers, 0); + _preds[pred].blockers--; + } + else if (val == 1) { + ALWAYS(_preds[pred].pos.remove(cl)); + } + else { + ALWAYS(_preds[pred].neg.remove(cl)); + } + } +} + +bool PredicateElimination::eligible(unsigned pred) const +{ + const PredInfo &info = _preds[pred]; + return !info.eliminated && info.blockers == 0 && (info.pos.size() + info.neg.size() > 0); +} + +double PredicateElimination::estimatedTotalAfter(unsigned pred) const +{ + double sp = _preds[pred].pos.size(); + double sn = _preds[pred].neg.size(); + return (double)_curTotal - sp - sn + sp * sn; +} + +bool PredicateElimination::admissible(unsigned pred) const +{ + return estimatedTotalAfter(pred) <= (double)_origTotal * _totalLimit; +} + +int PredicateElimination::pickCandidate() const +{ + static Stack order; + order.reset(); + for (unsigned pred = 1; pred < _preds.size(); pred++) { + order.push(pred); + } + if (env.options->randomTraversals()) { + // ties on the estimate get broken randomly + Shuffling::shuffleArray(order, order.size()); + } + + int best = -1; + double bestEst = 0.0; + for (unsigned pred : order) { + if (eligible(pred) && admissible(pred)) { + double est = estimatedTotalAfter(pred); + if (best < 0 || est < bestEst) { + best = pred; + bestEst = est; + } + } + } + return best; +} + +Literal *PredicateElimination::findPredLiteral(Clause *cl, unsigned pred, bool polarity) const +{ + for (unsigned i = 0; i < cl->length(); i++) { + Literal *lit = (*cl)[i]; + if (lit->functor() == pred && lit->isPositive() == polarity) { + return lit; + } + } + ASSERTION_VIOLATION; + return nullptr; +} + +void PredicateElimination::eliminate(Problem &prb, unsigned pred) +{ + ASS(eligible(pred)); + + Stack posCls; + Stack negCls; + { + DHSet::Iterator pit(_preds[pred].pos); + while (pit.hasNext()) { + posCls.push(pit.next()); + } + DHSet::Iterator nit(_preds[pred].neg); + while (nit.hasNext()) { + negCls.push(nit.next()); + } + } + + if (env.options->showPreprocessing()) { + cout << "[PP] pel eliminating " << env.signature->predicateName(pred) + << " (|S_P| = " << posCls.size() << ", |S_~P| = " << negCls.size() << ")" << endl; + } + + // record the model-repairing definition while S_P is still at hand + recordElimination(prb, pred, posCls, negCls); + + Stack resolvents; + for (Clause *c : posCls) { + Literal *plitC = findPredLiteral(c, pred, true); + for (Clause *d : negCls) { + Literal *plitD = findPredLiteral(d, pred, false); + Clause *r = buildResolvent(c, plitC, d, plitD); + if (r && _useSubsumption) { + r = forwardSimplify(r); + } + if (r) { + resolvents.push(r); + env.statistics->predicateEliminationResolvents++; + if (env.options->showPreprocessing()) { + cout << "[PP] pel resolvent: " << r->toString() << endl; + } + } + } + } + + for (Clause *cl : posCls) { + unregisterClause(cl); + if (_useSubsumption) { + indexRemove(cl); + } + _deleted.insert(cl); + } + for (Clause *cl : negCls) { + unregisterClause(cl); + if (_useSubsumption) { + indexRemove(cl); + } + _deleted.insert(cl); + } + _curTotal -= posCls.size() + negCls.size(); + + for (Clause *r : resolvents) { + _all.push(r); + registerClause(r); + if (_useSubsumption) { + indexInsert(r); + } + } + _curTotal += resolvents.size(); + + _preds[pred].eliminated = true; + ASS(_preds[pred].pos.isEmpty()); + ASS(_preds[pred].neg.isEmpty()); + + _modified = true; + env.statistics->eliminatedPredicates++; +} + +Clause *PredicateElimination::buildResolvent(Clause *c, Literal *plitC, Clause *d, Literal *plitD) +{ + if (_equational) { + return buildResolventEq(c, plitC, d, plitD); + } + else { + return buildResolventMgu(c, plitC, d, plitD); + } +} + +Clause *PredicateElimination::buildResolventMgu(Clause *c, Literal *plitC, Clause *d, Literal *plitD) +{ + static RobSubstitution subst; + subst.reset(); + if (!subst.unifyArgs(plitC, 0, plitD, 1)) { + return nullptr; // sound to drop, since there is no equality (and no theories) around + } + + static Stack lits; + lits.reset(); + for (unsigned i = 0; i < c->length(); i++) { + Literal *lit = (*c)[i]; + if (lit != plitC) { + lits.push(subst.apply(lit, 0)); + } + } + for (unsigned i = 0; i < d->length(); i++) { + Literal *lit = (*d)[i]; + if (lit != plitD) { + lits.push(subst.apply(lit, 1)); + } + } + return assembleClause(lits, c, d); +} + +Clause *PredicateElimination::buildResolventEq(Clause *c, Literal *plitC, Clause *d, Literal *plitD) +{ + ASS_EQ(plitC->arity(), plitD->arity()); + + VarShiftApplicator shift{c->maxVar() + 1}; + + static Stack lits; + lits.reset(); + for (unsigned i = 0; i < c->length(); i++) { + Literal *lit = (*c)[i]; + if (lit != plitC) { + lits.push(lit); + } + } + for (unsigned i = 0; i < d->length(); i++) { + Literal *lit = (*d)[i]; + if (lit != plitD) { + lits.push(SubstHelper::apply(lit, shift)); + } + } + // this is where the "virtual flattening" happens + for (unsigned i = 0; i < plitC->arity(); i++) { + lits.push(Literal::createEquality(false, + *plitC->nthArgument(i), + SubstHelper::apply(*plitD->nthArgument(i), shift), + SortHelper::getArgSort(plitC, i))); + } + + // exhaustive equality substitution (note: no decomposition, so this is weaker than unification) + for (bool changed = true; changed;) { + changed = false; + for (unsigned idx = 0; idx < lits.size(); idx++) { + Literal *l = lits[idx]; + if (!l->isEquality() || l->isPositive()) { + continue; + } + TermList a0 = *l->nthArgument(0); + TermList a1 = *l->nthArgument(1); + if (a0 == a1) { // t != t is simply false + swap(lits[idx], lits.top()); + lits.pop(); + changed = true; + break; + } + TermList var, tgt; + if (a0.isVar() && !a1.containsSubterm(a0)) { + var = a0; + tgt = a1; + } + else if (a1.isVar() && !a0.containsSubterm(a1)) { + var = a1; + tgt = a0; + } + else { + continue; // a residual disequality (to be kept) + } + swap(lits[idx], lits.top()); + lits.pop(); + SingleVarApplicator app{var.var(), tgt}; + for (unsigned j = 0; j < lits.size(); j++) { + lits[j] = SubstHelper::apply(lits[j], app); + } + changed = true; + break; + } + } + + return assembleClause(lits, c, d); +} + +Clause *PredicateElimination::assembleClause(Stack &lits, Clause *c, Clause *d) +{ + static DHSet seen; + seen.reset(); + + static Stack out; + out.reset(); + + bool keptDiseq = false; + bool keptVarVarDiseq = false; + + for (unsigned i = 0; i < lits.size(); i++) { + Literal *l = lits[i]; + if (EqHelper::isEqTautology(l)) { // s = s + return nullptr; + } + if (l->isEquality() && l->isNegative() && *l->nthArgument(0) == *l->nthArgument(1)) { + continue; // t != t is simply false + } + if (seen.contains(Literal::complementaryLiteral(l))) { // a tautology + return nullptr; + } + if (!seen.insert(l)) { + continue; // a duplicate literal + } + out.push(l); + if (l->isEquality() && l->isNegative()) { + keptDiseq = true; + if (l->nthArgument(0)->isVar() && l->nthArgument(1)->isVar()) { + keptVarVarDiseq = true; + } + } + } + + _keptDisequality |= keptDiseq; + _keptVarVarDisequality |= keptVarVarDiseq; + + return Clause::fromStack(out, NonspecificInference2(InferenceRule::PREDICATE_ELIMINATION, c, d)); +} + +void PredicateElimination::recordElimination(Problem &prb, unsigned pred, + Stack const &posCls, Stack const &negCls) +{ + if (posCls.isEmpty()) { // P occurs only negatively; setting it to false satisfies all its clauses + prb.addTrivialPredicate(pred, false); + return; + } + if (negCls.isEmpty()) { // P occurs only positively + prb.addTrivialPredicate(pred, true); + return; + } + + /* Following the model construction from the proof (cf. the paper): + * P(x0,...,xn-1) <=> \/_{D \/ P(ts) in S_P} exists ys. (x0 = ts[0] /\ ... /\ xn-1 = ts[n-1] /\ ~D) + * where each clause's variables ys are renamed away from the head variables x0,...,xn-1. + */ + unsigned ar = env.signature->predicateArity(pred); + + TermStack hargs; + for (unsigned v = 0; v < ar; v++) { + hargs.push(TermList::var(v)); + } + Literal *head = Literal::create(pred, ar, true, hargs.begin()); + + VarShiftApplicator shift{ar}; // clause variables become >= ar, i.e. disjoint from the head's + + FormulaList *disjuncts = FormulaList::empty(); + Stack::ConstIterator cit(posCls); + while (cit.hasNext()) { + Clause *c = cit.next(); + Literal *plit = findPredLiteral(c, pred, true); + + FormulaList *conjuncts = FormulaList::empty(); + for (unsigned i = 0; i < ar; i++) { + FormulaList::push(new AtomicFormula(Literal::createEquality(true, + TermList::var(i), + SubstHelper::apply(*plit->nthArgument(i), shift), + SortHelper::getArgSort(plit, i))), + conjuncts); + } + for (unsigned i = 0; i < c->length(); i++) { + Literal *lit = (*c)[i]; + if (lit != plit) { + FormulaList::push(new AtomicFormula( + Literal::complementaryLiteral(SubstHelper::apply(lit, shift))), + conjuncts); + } + } + Formula *inner = JunctionFormula::generalJunction(AND, conjuncts); + + // existentially close over the (shifted) clause variables + DHMap varSorts; + SortHelper::collectVariableSorts(inner, varSorts); + VSList *vs = VSList::empty(); + DHMap::Iterator vit(varSorts); + while (vit.hasNext()) { + unsigned var; + TermList sort; + vit.next(var, sort); + if (var >= ar) { // skip the head variables + VSList::push(VarSort(var, sort), vs); + } + } + Formula *disjunct = vs ? (Formula *)new QuantifiedFormula(EXISTS, vs, inner) : inner; + FormulaList::push(disjunct, disjuncts); + } + + Formula *body = JunctionFormula::generalJunction(OR, disjuncts); + prb.addEliminatedPredicate(pred, new BinaryFormula(IFF, new AtomicFormula(head), body)); +} + +Clause *PredicateElimination::forwardSimplify(Clause *cl) +{ + ASS(_useSubsumption); + + // every subsumption resolution step strictly shrinks the clause, so this terminates + for (;;) { + Clause *replacement = nullptr; + if (forwardSubsumedOrResolved(cl, replacement)) { + env.statistics->predicateEliminationSubsumed++; + return nullptr; + } + if (!replacement) { + return cl; + } + env.statistics->predicateEliminationSRs++; + if (env.options->showPreprocessing()) { + cout << "[PP] pel subsumption resolution: " << replacement->toString() << endl; + } + cl = replacement; + } +} + +// a port of ForwardSubsumptionAndResolution::perform to our single-index setting +// (unit and multi-literal clauses share one tree, distinguished by their length) +bool PredicateElimination::forwardSubsumedOrResolved(Clause *cl, Clause *&replacement) +{ + ASS(_useSubsumption); + ASS(!replacement); + + static DHSet checked; // shared by both passes below, as in FSAR + checked.reset(); + + Clause *conclusion = nullptr; + + // pass 1: subsumption (and cheap subsumption resolution setup on the side) + for (unsigned i = 0; i < cl->length(); i++) { + Literal *lit = (*cl)[i]; + auto rit = _subsIndex->getGeneralizations(lit, /*complementary=*/false, /*retrieveSubstitutions=*/false); + while (rit.hasNext()) { + Clause *mcl = rit.next().data->clause; + if (!checked.insert(mcl)) { + continue; + } + if (mcl->length() == 1) { + return true; // a unit generalization subsumes outright + } + bool checkS = mcl->length() <= cl->length(); + bool checkSR = !conclusion; + if (checkS && _satSubs.checkSubsumption(mcl, cl, /*setSR=*/checkSR)) { + return true; + } + if (checkSR) { + // subsumption is preferred, so just remember the conclusion and keep scanning + conclusion = _satSubs.checkSubsumptionResolution(mcl, cl, /*forward=*/true, /*usePreviousSetUp=*/checkS); + } + } + } + + if (conclusion) { + replacement = conclusion; + return false; + } + + // pass 2: subsumption resolution against complementary matches + for (unsigned i = 0; i < cl->length(); i++) { + Literal *lit = (*cl)[i]; + auto rit = _subsIndex->getGeneralizations(lit, /*complementary=*/true, /*retrieveSubstitutions=*/false); + while (rit.hasNext()) { + Clause *mcl = rit.next().data->clause; + if (mcl->length() == 1) { // the resolved literal is lit itself, no need to involve the SAT solver + replacement = SATSubsumption::SATSubsumptionAndResolution::getSubsumptionResolutionConclusion(cl, lit, mcl, /*forward=*/true); + return false; + } + if (!checked.insert(mcl)) { + continue; + } + conclusion = _satSubs.checkSubsumptionResolution(mcl, cl, /*forward=*/true, /*usePreviousSetUp=*/false); + if (conclusion) { + replacement = conclusion; + return false; + } + } + } + + return false; +} + +void PredicateElimination::indexInsert(Clause *cl) +{ + ASS(_useSubsumption); + + if (cl->length() == 0) { + return; // the empty clause subsumes everything, but saturation will pick it up immediately anyway + } + Literal *key = (cl->length() == 1) ? (*cl)[0] : LiteralByMatchability::find_least_matchable_in(cl).lit(); + ALWAYS(_indexedKey.insert(cl, key)); + _subsIndex->insert(LiteralClause{key, cl}); +} + +void PredicateElimination::indexRemove(Clause *cl) +{ + ASS(_useSubsumption); + + Literal *key; + if (_indexedKey.pop(cl, key)) { + _subsIndex->remove(LiteralClause{key, cl}); + } +} + +} // namespace Shell diff --git a/Shell/PredicateElimination.hpp b/Shell/PredicateElimination.hpp new file mode 100644 index 0000000000..91a9055023 --- /dev/null +++ b/Shell/PredicateElimination.hpp @@ -0,0 +1,132 @@ +/* + * 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 + */ +/** + * @file PredicateElimination.hpp + * Defines class PredicateElimination. + */ + +#ifndef __PredicateElimination__ +#define __PredicateElimination__ + +#include "Forwards.hpp" + +#include "Kernel/Problem.hpp" + +#include "Lib/DArray.hpp" +#include "Lib/DHMap.hpp" +#include "Lib/DHSet.hpp" +#include "Lib/Stack.hpp" + +#include "Indexing/Index.hpp" +#include "Indexing/LiteralSubstitutionTree.hpp" +#include "SATSubsumption/SATSubsumptionAndResolution.hpp" + +namespace Shell { + +using namespace Kernel; + +/** + * Predicate elimination for preprocessing of clausified problems, + * after Khasidashvili and Korovin: "Predicate Elimination for Preprocessing + * in First-Order Theorem Proving" (SAT 2016). + * + * A predicate P which occurs at most once in every clause (is "non-self-referential") + * can be eliminated by replacing the clauses S_P and S_~P (those containing P positively, + * respectively, negatively) by all the pairwise resolvents on P. In the presence + * of equality (or theories), the resolvents need to be computed via (virtual) flattening + * of the P-literals, i.e. C \/ P(ts) and D \/ ~P(ss) yield C \/ D' \/ t1 != s1' \/ ... \/ tn != sn' + * (with D renamed apart), simplified by the equality substitution rule + * (x != t \/ C ==> C[t/x], when x not in t). Without equality/theories it is + * sound (and avoids introducing equality) to use an mgu instead and drop + * the non-unifiable pairs. + * + * Elimination steps are subject to clause-growth limits estimated + * SAT-style as |S_P|*|S_~P| resolvents replacing |S_P|+|S_~P| clauses. + */ +class PredicateElimination { +public: + /** + * @param forceEquationally force the flattening-based resolvent computation even on + * problems without equality/theories (required under FMB, whose model + * reconstruction cannot rely on the Herbrand-interpretation argument + * that justifies the mgu mode) + * @param totalLimit an elimination step is admissible only if the estimated + * number of clauses afterwards does not exceed the initial number times this factor + * @param useSubsumption keep the clause set forward-inter-subsumed and + * subsumption-resolved + */ + PredicateElimination(bool forceEquationally, float totalLimit, bool useSubsumption) + : _forceEquationally(forceEquationally), + _totalLimit(totalLimit), _useSubsumption(useSubsumption) {} + + void apply(Kernel::Problem &prb); + +private: + struct PredInfo { + Lib::DHSet pos; // S_P: clauses in which P occurs exactly once, positively + Lib::DHSet neg; // S_~P: dtto, negatively + unsigned blockers = 0; // number of clauses in which P occurs more than once + bool eliminated = false; + }; + + // options + bool _forceEquationally; + float _totalLimit; + bool _useSubsumption; + + // clause set state + Lib::Stack _all; // all clauses ever seen, in insertion order + Lib::DHSet _deleted; // those of _all that have been eliminated + Lib::DArray _preds; + size_t _curTotal = 0; + size_t _origTotal = 0; + bool _equational = false; + bool _modified = false; + bool _keptDisequality = false; // some resolvent kept a residual disequality + bool _keptVarVarDisequality = false; // ... between two variables + + void registerClause(Clause *cl); + void unregisterClause(Clause *cl); + + bool eligible(unsigned pred) const; + double estimatedTotalAfter(unsigned pred) const; + bool admissible(unsigned pred) const; + int pickCandidate() const; + + void eliminate(Problem &prb, unsigned pred); + Literal *findPredLiteral(Clause *cl, unsigned pred, bool polarity) const; + + // resolvent construction; nullptr means no clause results (tautology / non-unifiable pair) + Clause *buildResolvent(Clause *c, Literal *plitC, Clause *d, Literal *plitD); + Clause *buildResolventMgu(Clause *c, Literal *plitC, Clause *d, Literal *plitD); + Clause *buildResolventEq(Clause *c, Literal *plitC, Clause *d, Literal *plitD); + Clause *assembleClause(Lib::Stack &lits, Clause *c, Clause *d); + + // model reconstruction + void recordElimination(Problem &prb, unsigned pred, Lib::Stack const &posCls, Lib::Stack const &negCls); + + // forward subsumption (and subsumption resolution) machinery, only used with _useSubsumption; + // the backward direction (new clauses simplifying older ones) is left as future work + Indexing::LiteralSubstitutionTree *_subsIndex = nullptr; + Lib::DHMap _indexedKey; // under which literal a clause got indexed + SATSubsumption::SATSubsumptionAndResolution _satSubs; + // simplify cl against the indexed clause set (to fixpoint): returns nullptr if cl + // is subsumed, otherwise cl itself or a subsumption-resolution descendant of it + Clause *forwardSimplify(Clause *cl); + // one round: true means subsumed; otherwise replacement is set to the + // subsumption resolution conclusion (or nullptr, if nothing applied) + bool forwardSubsumedOrResolved(Clause *cl, Clause *&replacement); + void indexInsert(Clause *cl); + void indexRemove(Clause *cl); +}; + +} // namespace Shell + +#endif /* __PredicateElimination__ */ diff --git a/Shell/Preprocess.cpp b/Shell/Preprocess.cpp index 1a5b5c0f99..95a2fa00bc 100644 --- a/Shell/Preprocess.cpp +++ b/Shell/Preprocess.cpp @@ -54,6 +54,7 @@ #include "TheoryFlattening.hpp" #include "TweeGoalTransformation.hpp" #include "BlockedClauseElimination.hpp" +#include "PredicateElimination.hpp" #include "UIHelper.hpp" #include "Lib/List.hpp" @@ -466,6 +467,24 @@ void Preprocess::preprocess(Problem& prb) bce.apply(prb); } + if (_options.predicateElimination()) { + if (prb.isHigherOrder() || prb.hasPolymorphicSym()) { // in both cases, predicates could hide inside terms, breaking the occurrence counting + if (outputAllowed()) { + addCommentSignForSZS(std::cout); + std::cout << "WARNING: Not using PredicateElimination currently not compatible with polymorphic/higher-order inputs." << endl; + } + } else { + env.statistics->phase=ExecutionPhase::PREDICATE_ELIMINATION; + if (env.options->showPreprocessing()) + std::cout << "predicate elimination" << std::endl; + + PredicateElimination pel(/*forceEquationally=*/_options.saturationAlgorithm() == Options::SaturationAlgorithm::FINITE_MODEL_BUILDING, + _options.predicateEliminationTotalLimit(), + _options.predicateEliminationSubsumption()); + pel.apply(prb); + } + } + if (_options.shuffleInput()) { TIME_TRACE(TimeTrace::SHUFFLING); env.statistics->phase=ExecutionPhase::SHUFFLING; diff --git a/Shell/Statistics.cpp b/Shell/Statistics.cpp index f7b4febd40..b462d97933 100644 --- a/Shell/Statistics.cpp +++ b/Shell/Statistics.cpp @@ -189,6 +189,10 @@ void Statistics::print(std::ostream& out) ENTRY("Selected by SInE selection", selectedBySine); ENTRY("SInE iterations", sineIterations); ENTRY("Blocked clauses", blockedClauses); + ENTRY("Eliminated predicates", eliminatedPredicates); + ENTRY("Predicate elimination resolvents", predicateEliminationResolvents); + ENTRY("Predicate elimination subsumed", predicateEliminationSubsumed); + ENTRY("Predicate elimination subsumption resolutions", predicateEliminationSRs); ENTRY("Split inequalities", splitInequalities); GROUP("SATURATION"); @@ -382,6 +386,8 @@ const char* Statistics::phaseToString(ExecutionPhase p) return "Unused predicate definition removal"; case ExecutionPhase::BLOCKED_CLAUSE_ELIMINATION: return "Blocked clause elimination"; + case ExecutionPhase::PREDICATE_ELIMINATION: + return "Predicate elimination"; case ExecutionPhase::TWEE: return "Twee Goal Transformation"; case ExecutionPhase::ANSWER_LITERAL: diff --git a/Shell/Statistics.hpp b/Shell/Statistics.hpp index 163388c841..b52c3c0c0a 100644 --- a/Shell/Statistics.hpp +++ b/Shell/Statistics.hpp @@ -70,6 +70,7 @@ enum class ExecutionPhase { PREPROCESS_1, UNUSED_PREDICATE_DEFINITION_REMOVAL, BLOCKED_CLAUSE_ELIMINATION, + PREDICATE_ELIMINATION, TWEE, ANSWER_LITERAL, PREPROCESS_2, @@ -123,6 +124,14 @@ class Statistics { unsigned sineIterations = 0; /** number of detected blocked clauses */ unsigned blockedClauses = 0; + /** number of predicates eliminated by predicate elimination */ + unsigned eliminatedPredicates = 0; + /** number of resolvents kept during predicate elimination */ + unsigned predicateEliminationResolvents = 0; + /** number of clauses deleted as subsumed during predicate elimination */ + unsigned predicateEliminationSubsumed = 0; + /** number of subsumption resolutions performed during predicate elimination */ + unsigned predicateEliminationSRs = 0; // Induction unsigned maxInductionDepth = 0; diff --git a/UnitTests/tPredicateElimination.cpp b/UnitTests/tPredicateElimination.cpp new file mode 100644 index 0000000000..af8de45fc4 --- /dev/null +++ b/UnitTests/tPredicateElimination.cpp @@ -0,0 +1,374 @@ +/* + * 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 + +#include "Test/UnitTesting.hpp" +#include "Test/SyntaxSugar.hpp" + +#include "Lib/Environment.hpp" +#include "Shell/Statistics.hpp" + +#include "Kernel/Clause.hpp" +#include "Kernel/Inference.hpp" +#include "Kernel/Problem.hpp" +#include "Kernel/Unit.hpp" + +#include "Shell/PredicateElimination.hpp" + +using namespace Kernel; +using namespace Shell; + +static Problem *problemFromClauses(std::initializer_list cls) +{ + UnitList *units = UnitList::empty(); + for (Clause *cl : cls) { + UnitList::push(cl, units); + } + return new Problem(units); +} + +static Stack collectClauses(Problem &prb) +{ + Stack res; + UnitList::Iterator it(prb.units()); + while (it.hasNext()) { + Unit *u = it.next(); + ASS(u->isClause()); + res.push(static_cast(u)); + } + return res; +} + +static bool containsPredicate(const Stack &cls, unsigned pred) +{ + for (Clause *cl : cls) { + for (unsigned i = 0; i < cl->length(); i++) { + if ((*cl)[i]->functor() == pred) { + return true; + } + } + } + return false; +} + +/** the clause of the given length -- expected to exist and be unique */ +static Clause *theClauseOfLength(const Stack &cls, unsigned len) +{ + Clause *found = nullptr; + for (Clause *cl : cls) { + if (cl->length() == len) { + ASS(!found); + found = cl; + } + } + ASS(found); + return found; +} + +static Stack runPE(std::initializer_list cls, + bool forceEquationally = false, + float totalLimit = 2.0, + bool useSubsumption = false) +{ + Problem *prb = problemFromClauses(cls); + PredicateElimination pe(forceEquationally, totalLimit, useSubsumption); + pe.apply(*prb); + return collectClauses(*prb); +} + +/* Note: many tests below include the clause {q(y) \/ ~q(f(y))}, in which q is + * "self-referential" and thus protected from elimination. Without such an anchor, + * eliminating p typically leaves q occurring in one polarity only, whereupon + * PE (correctly, but distractingly for the tests) deletes all the q-clauses too. */ + +#define MY_SYNTAX_SUGAR \ + DECL_DEFAULT_VARS \ + DECL_SORT(s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) \ + DECL_CONST(c, s) \ + DECL_FUNC(f, {s}, s) \ + DECL_PRED(p, {s}) \ + DECL_PRED(q, {s}) \ + DECL_PRED(r, {s}) + +TEST_FUN(mgu_basic) +{ + MY_SYNTAX_SUGAR + + // {p(a)}, {~p(x) \/ q(x)} ---> {q(a)} + auto res = runPE({clause({p(a)}), clause({~p(x), q(x)}), + clause({q(y), ~q(f(y))})}); + + ASS_EQ(res.size(), 2); + ASS(!containsPredicate(res, p.functor())); + Clause *resolvent = theClauseOfLength(res, 1); + ASS_EQ(resolvent->literalsOnlyToString(), "q(a)"); + ASS(resolvent->inference().rule() == InferenceRule::PREDICATE_ELIMINATION); +} + +TEST_FUN(mgu_nonunifiable_pair_dropped) +{ + MY_SYNTAX_SUGAR + + // no equality in the problem: the pair does not unify, no resolvent + auto res = runPE({clause({p(a)}), clause({~p(b), q(b)}), + clause({q(y), ~q(f(y))})}); + + ASS_EQ(res.size(), 1); // just the q-anchor + ASS(!containsPredicate(res, p.functor())); +} + +TEST_FUN(mgu_empty_clause) +{ + MY_SYNTAX_SUGAR + + // {p(a)}, {~p(a)} ---> the empty clause + auto res = runPE({clause({p(a)}), clause({~p(a)})}); + + ASS_EQ(res.size(), 1); + ASS_EQ(res[0]->length(), 0); +} + +TEST_FUN(eq_residual_disequality) +{ + MY_SYNTAX_SUGAR + + // forcing the equational mode: the non-unifiable pair now leaves a residual disequality + auto res = runPE({clause({p(a)}), clause({~p(b), q(b)}), + clause({q(y), ~q(f(y))})}, + /*forceEquationally=*/true); + + ASS_EQ(res.size(), 2); + ASS(!containsPredicate(res, p.functor())); + bool sawDiseq = false; + for (Clause *cl : res) { + for (unsigned i = 0; i < cl->length(); i++) { + Literal *l = (*cl)[i]; + sawDiseq |= (l->isEquality() && l->isNegative()); + } + } + ASS(sawDiseq); +} + +TEST_FUN(eq_subst_computes_unifier) +{ + MY_SYNTAX_SUGAR + + // {p2(f(x),x)}, {~p2(y,a) \/ q(y)} ---> {q(f(a))}, even equationally, + // since equality substitution resolves all the introduced disequalities away + DECL_PRED(p2, {s, s}) + auto res = runPE({clause({p2(f(x), x)}), clause({~p2(y, a), q(y)}), + clause({q(y), ~q(f(y))})}, + /*forceEquationally=*/true); + + ASS_EQ(res.size(), 2); + ASS(!containsPredicate(res, p2.functor())); + Clause *resolvent = theClauseOfLength(res, 1); + ASS_EQ(resolvent->literalsOnlyToString(), "q(f(a))"); +} + +TEST_FUN(tautologies_dropped) +{ + MY_SYNTAX_SUGAR + + // resolving on p yields the tautology {q(x) \/ ~q(x)}; then q disappears as well + auto res = runPE({clause({p(x), q(x)}), clause({~p(y), ~q(y)})}); + + ASS_EQ(res.size(), 0); +} + +TEST_FUN(self_referential_skipped) +{ + MY_SYNTAX_SUGAR + + // p occurs twice in the first clause, so it must survive + auto res = runPE({clause({p(x), p(f(x))}), clause({~p(a)})}); + + ASS_EQ(res.size(), 2); + ASS(containsPredicate(res, p.functor())); +} + +TEST_FUN(pure_predicate_clauses_deleted) +{ + MY_SYNTAX_SUGAR + + // p occurs only positively: its clause can simply be deleted + Problem *prb = problemFromClauses({clause({p(a), q(b)}), clause({q(y), ~q(f(y))})}); + PredicateElimination pe(false, 2.0, false); + pe.apply(*prb); + auto res = collectClauses(*prb); + + ASS_EQ(res.size(), 1); + ASS(!containsPredicate(res, p.functor())); + ASS(prb->interferences.isNonEmpty()); // the model-repairing definition of p got recorded +} + +TEST_FUN(growth_limits_respected) +{ + MY_SYNTAX_SUGAR + + // 3 x 3 occurrences of both p and r: eliminating either would mean + // 9 resolvents replacing 6 clauses -- not admissible under total limit 1.0 + std::initializer_list cls = { + clause({p(x), r(a)}), clause({p(x), r(b)}), clause({p(x), r(c)}), + clause({~p(y), ~r(a)}), clause({~p(y), ~r(b)}), clause({~p(y), ~r(c)})}; + + auto res = runPE(cls, false, /*totalLimit=*/1.0); + ASS_EQ(res.size(), 6); + ASS(containsPredicate(res, p.functor())); + + // with a benevolent limit, p gets eliminated + // (of the 9 resolvents, 3 are tautologies; and r is self-referential in the remaining 6) + auto res2 = runPE(cls, false, /*totalLimit=*/2.0); + ASS_EQ(res2.size(), 6); + ASS(!containsPredicate(res2, p.functor())); +} + +TEST_FUN(duplicate_literals_removed) +{ + MY_SYNTAX_SUGAR + + // the resolvent {q(a) \/ q(a)} gets condensed to {q(a)} + auto res = runPE({clause({p(a), q(a)}), clause({~p(x), q(x)}), + clause({q(y), ~q(f(y))})}); + + ASS_EQ(res.size(), 2); + Clause *resolvent = theClauseOfLength(res, 1); + ASS_EQ(resolvent->literalsOnlyToString(), "q(a)"); +} + +TEST_FUN(subsumed_resolvents_not_added) +{ + MY_SYNTAX_SUGAR + + // the resolvent q(a) is subsumed by the input clause {q(a)} + std::initializer_list cls = { + clause({q(a)}), clause({p(a)}), clause({~p(x), q(x)}), + clause({q(y), ~q(f(y))})}; + + auto res = runPE(cls, false, 2.0, /*useSubsumption=*/true); + ASS_EQ(res.size(), 2); // {q(a)} and the anchor; without subsumption we'd also keep a second copy of {q(a)} + ASS(!containsPredicate(res, p.functor())); + + auto res2 = runPE(cls, false, 2.0, /*useSubsumption=*/false); + ASS_EQ(res2.size(), 3); +} + +/** the clause concluded by subsumption resolution -- expected to exist and be unique */ +static Clause *theSRConclusion(const Stack &cls) +{ + Clause *found = nullptr; + for (Clause *cl : cls) { + if (cl->inference().rule() == InferenceRule::FORWARD_SUBSUMPTION_RESOLUTION) { + ASS(!found); + found = cl; + } + } + ASS(found); + return found; +} + +TEST_FUN(sr_simplifies_resolvent) +{ + MY_SYNTAX_SUGAR + + // eliminating p yields the resolvent {q(a) \/ ~r(a)}, which subsumption + // resolution against the unit {r(a)} shrinks to {q(a)}; + // (afterwards, r is pure and {r(a)} goes away too) + auto res = runPE({clause({r(a)}), clause({p(a)}), clause({~p(x), q(x), ~r(x)}), + clause({q(y), ~q(f(y))})}, + false, 2.0, /*useSubsumption=*/true); + + ASS_EQ(res.size(), 2); + ASS(!containsPredicate(res, p.functor())); + ASS(!containsPredicate(res, r.functor())); + Clause *conclusion = theClauseOfLength(res, 1); + ASS_EQ(conclusion->literalsOnlyToString(), "q(a)"); + ASS(conclusion->inference().rule() == InferenceRule::FORWARD_SUBSUMPTION_RESOLUTION); +} + +TEST_FUN(sr_on_input_pass) +{ + MY_SYNTAX_SUGAR + + // already the initial pass resolves {q(b) \/ ~r(a)} against {r(x)} down to {q(b)} + auto res = runPE({clause({r(x)}), clause({q(b), ~r(a)}), + clause({q(y), ~q(f(y))})}, + false, 2.0, /*useSubsumption=*/true); + + ASS_EQ(res.size(), 2); + ASS(!containsPredicate(res, r.functor())); + Clause *conclusion = theClauseOfLength(res, 1); + ASS_EQ(conclusion->literalsOnlyToString(), "q(b)"); + ASS(conclusion->inference().rule() == InferenceRule::FORWARD_SUBSUMPTION_RESOLUTION); +} + +TEST_FUN(sr_chains_to_fixpoint) +{ + MY_SYNTAX_SUGAR + + // {~p(x) \/ q(x) \/ ~r(x) \/ ~r3(x)} gets shrunk by two successive subsumption + // resolution steps (against {r(y)} and {r3(y)}) to {~p(x) \/ q(x)} within + // a single forwardSimplify call; eliminating p then yields {q(a)} + DECL_PRED(r3, {s}) + unsigned srsBefore = env.statistics->predicateEliminationSRs; + auto res = runPE({clause({p(a)}), clause({~p(x), q(x), ~r(x), ~r3(x)}), + clause({r(y)}), clause({r3(y)}), + clause({q(y), ~q(f(y))})}, + false, 2.0, /*useSubsumption=*/true); + + ASS_EQ(env.statistics->predicateEliminationSRs - srsBefore, 2); + ASS_EQ(res.size(), 2); + ASS(!containsPredicate(res, p.functor())); + ASS(!containsPredicate(res, r.functor())); + ASS(!containsPredicate(res, r3.functor())); + Clause *resolvent = theClauseOfLength(res, 1); + ASS_EQ(resolvent->literalsOnlyToString(), "q(a)"); + ASS(resolvent->inference().rule() == InferenceRule::PREDICATE_ELIMINATION); +} + +TEST_FUN(duplicate_literals_in_input) +{ + MY_SYNTAX_SUGAR + + // clauses can still carry duplicate literals when they reach predicate elimination + // (e.g. created by EqResWithDeletion from p(X) \/ p(a) \/ X != a); + // they must be removed on input, since SATSubsumptionAndResolution relies on + // premises being duplicate-free -- feeding it {p(a) \/ p(a)} as the main premise + // against the side premise {p(x) \/ ~p(y)} used to "conclude" the empty clause! + auto res = runPE({clause({p(a), p(a)}), clause({p(x), ~p(y)})}, + false, 2.0, /*useSubsumption=*/true); + + ASS_EQ(res.size(), 2); + for (Clause *cl : res) { + ASS_G(cl->length(), 0); // and in particular: no bogus empty clause + } + Clause *dedup = theClauseOfLength(res, 1); + ASS_EQ(dedup->literalsOnlyToString(), "p(a)"); +} + +TEST_FUN(sr_multiliteral) +{ + MY_SYNTAX_SUGAR + + // a multi-literal side premise {q(x) \/ ~r(x)} resolves {q(a) \/ r(a) \/ w(a)} + // down to {q(a) \/ w(a)} (exercising the SAT-based path, not just the unit shortcut) + DECL_PRED(w, {s}) + auto res = runPE({clause({q(x), ~r(x)}), clause({q(y), ~q(f(y))}), clause({w(y), ~w(f(y))}), + clause({q(a), r(a), w(a)})}, + false, 2.0, /*useSubsumption=*/true); + + ASS_EQ(res.size(), 3); // the conclusion and the two anchors ({q(x) \/ ~r(x)} dies with pure r) + ASS(!containsPredicate(res, r.functor())); + Clause *conclusion = theSRConclusion(res); + ASS_EQ(conclusion->length(), 2); +} diff --git a/cmake/sources.cmake b/cmake/sources.cmake index bb6599d7f9..68991c5727 100644 --- a/cmake/sources.cmake +++ b/cmake/sources.cmake @@ -97,6 +97,7 @@ set(UNIT_TESTS UnitTests/tLPO.cpp UnitTests/tList.cpp UnitTests/tOption.cpp + UnitTests/tPredicateElimination.cpp UnitTests/tOptionConstraints.cpp UnitTests/tQKbo.cpp UnitTests/tQuotientE.cpp @@ -732,6 +733,8 @@ set(SOURCES Shell/PartialRedundancyHandler.hpp Shell/PredicateDefinition.cpp Shell/PredicateDefinition.hpp + Shell/PredicateElimination.cpp + Shell/PredicateElimination.hpp Shell/Preprocess.cpp Shell/Preprocess.cpp Shell/Preprocess.hpp diff --git a/samplers/samplerFNT.smp b/samplers/samplerFNT.smp index 9459b39453..b0a39332be 100644 --- a/samplers/samplerFNT.smp +++ b/samplers/samplerFNT.smp @@ -33,6 +33,15 @@ $nm=NZ > nm ~sgd 0.07,2 $ins=Z > ins ~cat 0:1 $ins=NZ > ins ~sgd 0.4,1 +# predicate_elimination +> pel ~cat off:1,on:1 + +# predicate_elimination_subsumption +pel=on > pels ~cat on:4,off:1 + +# predicate_elimination_total_limit +pel=on > peltl ~uf 0.9,5.0 + # random_polarities > rp ~cat off:3,on:1 diff --git a/samplers/samplerFOL.smp b/samplers/samplerFOL.smp index e34cc7ba78..e9526931ef 100644 --- a/samplers/samplerFOL.smp +++ b/samplers/samplerFOL.smp @@ -38,6 +38,15 @@ $nm=NZ > nm ~sgd 0.07,2 $ins=Z > ins ~cat 0:1 $ins=NZ > ins ~sgd 0.4,1 +# predicate_elimination +> pel ~cat off:1,on:1 + +# predicate_elimination_subsumption +pel=on > pels ~cat on:4,off:1 + +# predicate_elimination_total_limit +pel=on > peltl ~uf 0.9,5.0 + # random_polarities > rp ~cat off:3,on:1 diff --git a/samplers/samplerHOL.smp b/samplers/samplerHOL.smp index 109dfc2500..a98ea55d31 100644 --- a/samplers/samplerHOL.smp +++ b/samplers/samplerHOL.smp @@ -38,6 +38,15 @@ $nm=NZ > nm ~sgd 0.07,2 $ins=Z > ins ~cat 0:1 $ins=NZ > ins ~sgd 0.4,1 +# predicate_elimination +> pel ~cat off:1,on:1 + +# predicate_elimination_subsumption +pel=on > pels ~cat on:4,off:1 + +# predicate_elimination_total_limit +pel=on > peltl ~uf 0.9,5.0 + # random_polarities > rp ~cat off:3,on:1 diff --git a/samplers/samplerIND.smp b/samplers/samplerIND.smp index d5417eccd3..d756897340 100644 --- a/samplers/samplerIND.smp +++ b/samplers/samplerIND.smp @@ -33,6 +33,15 @@ $nm=NZ > nm ~sgd 0.07,2 $ins=Z > ins ~cat 0:1 $ins=NZ > ins ~sgd 0.4,1 +# predicate_elimination +> pel ~cat off:1,on:1 + +# predicate_elimination_subsumption +pel=on > pels ~cat on:4,off:1 + +# predicate_elimination_total_limit +pel=on > peltl ~uf 0.9,5.0 + # random_polarities > rp ~cat off:3,on:1 diff --git a/samplers/samplerSMT.smp b/samplers/samplerSMT.smp index c33048ceef..09d596beca 100644 --- a/samplers/samplerSMT.smp +++ b/samplers/samplerSMT.smp @@ -36,6 +36,15 @@ $nm=NZ > nm ~sgd 0.07,2 $ins=Z > ins ~cat 0:1 $ins=NZ > ins ~sgd 0.4,1 +# predicate_elimination +> pel ~cat off:1,on:1 + +# predicate_elimination_subsumption +pel=on > pels ~cat on:4,off:1 + +# predicate_elimination_total_limit +pel=on > peltl ~uf 0.9,5.0 + # random_polarities > rp ~cat off:3,on:1