Merge pull request #511 from vprover/michael-mark-congruence-skips

mark symbols that should skip congruence axioms explicitly
vprover · Dec 9, 2023 · d8a68bc · d8a68bc
2 parents a1de9df + 1259a94
commit d8a68bc
Show file tree

Hide file tree

Showing 9 changed files with 32 additions and 20 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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();
@@ -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
@@ -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) {
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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;