Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

mark symbols that should skip congruence axioms explicitly #511

Merged
merged 1 commit into from
Dec 9, 2023
Merged

mark symbols that should skip congruence axioms explicitly #511

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 3 additions & 7 deletions Kernel/Signature.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down Expand Up @@ -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

/**
Expand Down
8 changes: 4 additions & 4 deletions Kernel/Signature.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand Down Expand Up @@ -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; }
Expand Down
2 changes: 2 additions & 0 deletions Shell/AnswerExtractor.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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());
}

Expand Down
8 changes: 5 additions & 3 deletions Shell/EqualityProxy.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -197,7 +197,7 @@ void EqualityProxy::addCongruenceAxioms(UnitList*& units)
for (unsigned i=0; i<funs; i++) {
Signature::Symbol* fnSym = env.signature->getFunction(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();
Expand All @@ -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) {
Expand Down Expand Up @@ -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);
Expand All @@ -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();
Expand Down
6 changes: 4 additions & 2 deletions Shell/EqualityProxyMono.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -203,7 +203,7 @@ void EqualityProxyMono::addCongruenceAxioms(UnitList*& units)
for (unsigned i=0; i<funs; i++) {
Signature::Symbol* fnSym = env.signature->getFunction(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) {
Expand All @@ -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) {
Expand Down Expand Up @@ -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());
Expand Down
4 changes: 3 additions & 1 deletion Shell/GeneralSplitting.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
2 changes: 2 additions & 0 deletions Shell/Naming.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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(
Expand Down
11 changes: 8 additions & 3 deletions Shell/NewCNF.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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());
}
Expand Down Expand Up @@ -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();
Expand Down
1 change: 1 addition & 0 deletions Shell/Skolem.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down