From 1259a94fa86eb9173c4eb3a6c882d195ff565baa Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Fri, 8 Dec 2023 16:00:17 +0000 Subject: [PATCH] mark symbols that should skip congruence axioms explicitly --- Kernel/Signature.cpp | 10 +++------- Kernel/Signature.hpp | 8 ++++---- Shell/AnswerExtractor.cpp | 2 ++ Shell/EqualityProxy.cpp | 8 +++++--- Shell/EqualityProxyMono.cpp | 6 ++++-- Shell/GeneralSplitting.cpp | 4 +++- Shell/Naming.cpp | 2 ++ Shell/NewCNF.cpp | 11 ++++++++--- Shell/Skolem.cpp | 1 + 9 files changed, 32 insertions(+), 20 deletions(-) diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp index 509ebead4b..a6c8be957c 100644 --- a/Kernel/Signature.cpp +++ b/Kernel/Signature.cpp @@ -58,7 +58,7 @@ Signature::Symbol::Symbol(const vstring& nm, unsigned arity, bool interpreted, b _inUnit(0), _inductionSkolem(0), _skolem(0), - _namesFormula(0), + _skipCongruence(0), _tuple(0), _computable(1), _prox(NOT_PROXY), @@ -822,17 +822,13 @@ unsigned Signature::addPredicate (const vstring& name, */ unsigned Signature::addNamePredicate(unsigned arity) { - unsigned index = addFreshPredicate(arity,"sP"); - getPredicate(index)->markNamesFormula(); - return index; + return addFreshPredicate(arity,"sP"); } // addNamePredicate unsigned Signature::addNameFunction(unsigned arity) { - unsigned index = addFreshFunction(arity,"sP"); - getFunction(index)->markNamesFormula(); - return index; + return addFreshFunction(arity,"sP"); } // addNameFunction /** diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index 307aa7469c..a83222a6a0 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -151,8 +151,8 @@ class Signature unsigned _inductionSkolem : 1; /** if skolem function in general **/ unsigned _skolem : 1; - /** if introduced for naming a subformula */ - unsigned _namesFormula : 1; + /** if does not need congruence axioms with equality proxy */ + unsigned _skipCongruence : 1; /** if tuple sort */ unsigned _tuple : 1; /** if allowed in answer literals */ @@ -265,8 +265,8 @@ class Signature inline void markSkolem(){ _skolem = 1;} inline bool skolem(){ return _skolem; } - inline void markNamesFormula() { _namesFormula = 1; } - inline bool namesFormula() { return _namesFormula; } + inline void markSkipCongruence() { _skipCongruence = 1; } + inline bool skipCongruence() { return _skipCongruence; } inline void markTuple(){ _tuple = 1; } inline bool tupleSort(){ return _tuple; } diff --git a/Shell/AnswerExtractor.cpp b/Shell/AnswerExtractor.cpp index b6c31ed3b3..60edfbeec5 100644 --- a/Shell/AnswerExtractor.cpp +++ b/Shell/AnswerExtractor.cpp @@ -354,6 +354,8 @@ Literal* AnswerLiteralManager::getAnswerLiteral(VList* vars,Formula* f) Signature::Symbol* predSym = env.signature->getPredicate(pred); predSym->setType(OperatorType::getPredicateType(sorts.size(), sorts.begin())); predSym->markAnswerPredicate(); + // don't need equality proxy for answer literals + predSym->markSkipCongruence(); return Literal::create(pred, vcnt, true, false, litArgs.begin()); } diff --git a/Shell/EqualityProxy.cpp b/Shell/EqualityProxy.cpp index 822f2ea901..d40a29ed64 100644 --- a/Shell/EqualityProxy.cpp +++ b/Shell/EqualityProxy.cpp @@ -197,7 +197,7 @@ void EqualityProxy::addCongruenceAxioms(UnitList*& units) for (unsigned i=0; igetFunction(i); // can axiomatise equality _before_ preprocessing, so skip (some) introduced symbols - if(!fnSym->usageCnt() || fnSym->skolem()) + if(!fnSym->usageCnt() || fnSym->skipCongruence()) continue; unsigned arity = fnSym->arity(); OperatorType* fnType = fnSym->fnType(); @@ -218,7 +218,7 @@ void EqualityProxy::addCongruenceAxioms(UnitList*& units) for (unsigned i = 1; i < preds; i++) { Signature::Symbol* predSym = env.signature->getPredicate(i); // can axiomatise equality _before_ preprocessing, so skip (some) introduced symbols - if(!predSym->usageCnt() || predSym->namesFormula() || predSym->equalityProxy() || predSym->answerPredicate()) + if(!predSym->usageCnt() || predSym->skipCongruence()) continue; unsigned arity = predSym->arity(); if (arity == 0) { @@ -302,7 +302,7 @@ unsigned EqualityProxy::getProxyPredicate() if(_addedPred){ return _proxyPredicate; } unsigned newPred = env.signature->addFreshPredicate(3,"sQ","eqProxy"); - + TermList sort = TermList(0,false); TermList var1 = TermList(1,false); TermList var2 = TermList(2,false); @@ -311,6 +311,8 @@ unsigned EqualityProxy::getProxyPredicate() OperatorType* predType = OperatorType::getPredicateType({sort, sort}, 1); predSym->setType(predType); predSym->markEqualityProxy(); + // don't need congruence axioms for the equality predicate itself + predSym->markSkipCongruence(); static TermStack args; args.reset(); diff --git a/Shell/EqualityProxyMono.cpp b/Shell/EqualityProxyMono.cpp index d269c277ba..eafdbffcbf 100644 --- a/Shell/EqualityProxyMono.cpp +++ b/Shell/EqualityProxyMono.cpp @@ -203,7 +203,7 @@ void EqualityProxyMono::addCongruenceAxioms(UnitList*& units) for (unsigned i=0; igetFunction(i); // can axiomatise equality _before_ preprocessing, so skip (some) introduced symbols - if(!fnSym->usageCnt() || fnSym->skolem()) + if(!fnSym->usageCnt() || fnSym->skipCongruence()) continue; unsigned arity = fnSym->arity(); if (arity == 0) { @@ -223,7 +223,7 @@ void EqualityProxyMono::addCongruenceAxioms(UnitList*& units) for (unsigned i = 1; i < preds; i++) { Signature::Symbol* predSym = env.signature->getPredicate(i); // can axiomatise equality _before_ preprocessing, so skip (some) introduced symbols - if(!predSym->usageCnt() || predSym->namesFormula() || predSym->equalityProxy() || predSym->answerPredicate()) + if(!predSym->usageCnt() || predSym->skipCongruence()) continue; unsigned arity = predSym->arity(); if (arity == 0) { @@ -340,6 +340,8 @@ unsigned EqualityProxyMono::getProxyPredicate(TermList sort) OperatorType* predType = OperatorType::getPredicateType({sort, sort}); predSym->setType(predType); predSym->markEqualityProxy(); + // don't need congruence axioms for the equality predicate itself + predSym->markSkipCongruence(); ASS(sort.isTerm()); ASS(sort.term()->shared()); diff --git a/Shell/GeneralSplitting.cpp b/Shell/GeneralSplitting.cpp index cc18b91cee..c04fc11516 100644 --- a/Shell/GeneralSplitting.cpp +++ b/Shell/GeneralSplitting.cpp @@ -228,8 +228,10 @@ bool GeneralSplitting::apply(Clause*& cl, UnitList*& resultStack) unsigned namingPred=env.signature->addNamePredicate(minDeg); + Signature::Symbol *sym = env.signature->getPredicate(namingPred); + sym->markSkipCongruence(); OperatorType* npredType = OperatorType::getPredicateType(minDeg, argSorts.begin()); - env.signature->getPredicate(namingPred)->setType(npredType); + sym->setType(npredType); if(mdvColor!=COLOR_TRANSPARENT && otherColor!=COLOR_TRANSPARENT) { ASS_EQ(mdvColor, otherColor); diff --git a/Shell/Naming.cpp b/Shell/Naming.cpp index d9740e9e63..b6a51e53d8 100644 --- a/Shell/Naming.cpp +++ b/Shell/Naming.cpp @@ -1119,6 +1119,7 @@ Literal* Naming::getDefinitionLiteral(Formula* f, VList* freeVars) { if(!_appify){ unsigned pred = env.signature->addNamePredicate(arity); Signature::Symbol* predSym = env.signature->getPredicate(pred); + predSym->markSkipCongruence(); if (env.colorUsed) { Color fc = f->getColor(); @@ -1136,6 +1137,7 @@ Literal* Naming::getDefinitionLiteral(Formula* f, VList* freeVars) { unsigned fun = env.signature->addNameFunction(typeVars.size()); TermList sort = AtomicSort::arrowSort(termVarSorts, AtomicSort::boolSort()); Signature::Symbol* sym = env.signature->getFunction(fun); + sym->markSkipCongruence(); sym->setType(OperatorType::getConstantsType(sort, typeArgArity)); TermList head = TermList(Term::create(fun, typeVars.size(), typeVars.begin())); TermList t = ApplicativeHelper::createAppTerm( diff --git a/Shell/NewCNF.cpp b/Shell/NewCNF.cpp index d40e2a60bd..47fadae0e1 100644 --- a/Shell/NewCNF.cpp +++ b/Shell/NewCNF.cpp @@ -972,17 +972,21 @@ Term* NewCNF::createSkolemTerm(unsigned var, VarSet* free) bool isPredicate = (rangeSort == AtomicSort::boolSort()); if (isPredicate) { unsigned pred = Skolem::addSkolemPredicate(arity, domainSorts.begin(), var); + Signature::Symbol *sym = env.signature->getPredicate(pred); + sym->markSkipCongruence(); if(_beingClausified->derivedFromGoal()){ - env.signature->getPredicate(pred)->markInGoal(); + sym->markInGoal(); } res = Term::createFormula(new AtomicFormula(Literal::create(pred, arity, true, false, fnArgs.begin()))); } else { unsigned fun = Skolem::addSkolemFunction(arity, domainSorts.begin(), rangeSort, var); + Signature::Symbol *sym = env.signature->getFunction(fun); + sym->markSkipCongruence(); if(_beingClausified->derivedFromGoal()){ - env.signature->getFunction(fun)->markInGoal(); + sym->markInGoal(); } if(_forInduction){ - env.signature->getFunction(fun)->markInductionSkolem(); + sym->markInductionSkolem(); } res = Term::create(fun, arity, fnArgs.begin()); } @@ -1183,6 +1187,7 @@ Literal* NewCNF::createNamingLiteral(Formula* f, VList* free) env.statistics->formulaNames++; Signature::Symbol* predSym = env.signature->getPredicate(pred); + predSym->markSkipCongruence(); if (env.colorUsed) { Color fc = f->getColor(); diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp index ce7d0e5221..75f59de1d9 100644 --- a/Shell/Skolem.cpp +++ b/Shell/Skolem.cpp @@ -137,6 +137,7 @@ unsigned Skolem::addSkolemFunction(unsigned arity, unsigned taArity, TermList* d unsigned fun = env.signature->addSkolemFunction(arity, suffix); Signature::Symbol* fnSym = env.signature->getFunction(fun); + fnSym->markSkipCongruence(); OperatorType* ot = OperatorType::getFunctionType(arity - taArity, domainSorts, rangeSort, taArity); fnSym->setType(ot); return fun;