remove the commutative bit, equations still treated as commutative

Forwards.hpp

@@ -99,9 +99,6 @@ class RobSubstitution;
 typedef VirtualIterator<RobSubstitution*> SubstIterator;
 typedef Lib::SmartPtr<RobSubstitution> RobSubstitutionSP;
 
-class Matcher;
-typedef VirtualIterator<Matcher*> MatchIterator;
-
 class LiteralSelector;
 
 class Ordering;

Indexing/LiteralSubstitutionTree.hpp

@@ -94,8 +94,8 @@ class LiteralSubstitutionTree
       { return tree->template iterator<Iterator>(lit, retrieveSubstitutions, reversed, args...); };
 
     return ifElseIter(
-        tree->isEmpty(), [&]() { return VirtualIterator<ELEMENT_TYPE(Iterator)>::getEmpty(); }, 
-                         [&]() { return ifElseIter(!lit->commutative(), 
+        tree->isEmpty(), [&]() { return VirtualIterator<ELEMENT_TYPE(Iterator)>::getEmpty(); },
+                         [&]() { return ifElseIter(!lit->isEquality(),
                                  [&]() { return iter(/* reverse */ false); },
                                  [&]() { return concatIters(iter(/* reverse */ false), iter(/* reverse */ true)); }); }
         );

Indexing/SubstitutionTree.hpp

@@ -797,14 +797,6 @@ class SubstitutionTree final
         }
 
         bindSpecialVar(2, SortHelper::getEqualityArgumentSort(lit));
-
-      } else if(reversed) {
-        ASS(lit->commutative());
-        ASS_EQ(lit->arity(),2);
-
-        bindSpecialVar(1,*lit->nthArgument(0));
-        bindSpecialVar(0,*lit->nthArgument(1));
-
       } else {
 
         TermList* args=lit->args();

Indexing/TermSharing.cpp

@@ -294,7 +294,6 @@ void TermSharing::computeAndSetSharedLiteralData(Literal* t)
 void TermSharing::computeAndSetSharedVarEqData(Literal* t, TermList sort)
 {
   ASS(t->isLiteral());
-  ASS(t->commutative());
   ASS(t->isEquality());
   ASS(t->nthArgument(0)->isVar());
   ASS(t->nthArgument(1)->isVar());

Indexing/TermSharing.hpp

@@ -59,7 +59,7 @@ class TermSharing
   static bool equals(const Literal* l1, const Literal* l2)
   { return Literal::literalEquals(l1, l2->functor(), l2->polarity() ^ opposite, 
         [&](auto i){ return *l2->nthArgument(i); }, 
-        l2->arity(), someIf(l2->isTwoVarEquality(), [&](){ return l2->twoVarEqSort(); }), l2->commutative()); }
+        l2->arity(), someIf(l2->isTwoVarEquality(), [&](){ return l2->twoVarEqSort(); })); }
 
   DHSet<TermList>* getArraySorts(){
     return &_arraySorts;

Inferences/Condensation.cpp

@@ -55,7 +55,6 @@ Clause* Condensation::simplify(Clause* cl)
   static DArray<Literal*> newLits(32);
   //
   static DArray<LiteralList*> alts(32);
-  //static OCMatchIterator matcher;
 
   LiteralMiniIndex cmi(cl);
 

Inferences/Induction.cpp

@@ -1352,7 +1352,7 @@ void InductionClauseIterator::performStructInductionTwo(const InductionContext&
         dargTerms.push(y);
         TermList djy;
         if (con->argSort(j)==AtomicSort::boolSort()) {
-          djy = TermList(Term::createFormula(new AtomicFormula(Literal::create(dj,dargTerms.size(),true,false,dargTerms.begin()))));
+          djy = TermList(Term::createFormula(new AtomicFormula(Literal::create(dj,dargTerms.size(),true,dargTerms.begin()))));
         } else {
           djy = TermList(Term::create(dj,dargTerms.size(),dargTerms.begin()));
         }
@@ -1448,7 +1448,7 @@ void InductionClauseIterator::performStructInductionThree(const InductionContext
         dargTerms.push(y);
         TermList djy;
         if (con->argSort(j)==AtomicSort::boolSort()) {
-          djy = TermList(Term::createFormula(new AtomicFormula(Literal::create(dj,dargTerms.size(),true,false,dargTerms.begin()))));
+          djy = TermList(Term::createFormula(new AtomicFormula(Literal::create(dj,dargTerms.size(),true,dargTerms.begin()))));
         } else {
           djy = TermList(Term::create(dj,dargTerms.size(),dargTerms.begin()));
         }

Inferences/TheoryInstAndSimp.cpp

@@ -768,7 +768,7 @@ Stack<Literal*> computeGuards(Stack<Literal*> const& lits)
       }
       args.push(destr->termArg(0));
       // asserts e.g. isCons(l) for a term that contains the subterm head(l) for lists
-      return Literal::create(discr, args.size(), /* polarity */ true, false, args.begin());
+      return Literal::create(discr, args.size(), /* polarity */ true, args.begin());
   };
 
 

Kernel/LiteralComparators.hpp

@@ -259,11 +259,12 @@ struct NormalizedLinearComparatorByWeight : public LiteralComparator
 	      static_cast<Literal*>(t2)->polarity());
     }
 
-    if(t1->commutative()) {
-      ASS(t2->commutative());
-      ASS(t1->isLiteral());
-      ASS_EQ(t1->arity(),2);
-
+    // MR: this looked suspicious to me, but MS says...
+    //
+    // t1 and t2 are assumed to be distinct initially,
+    // so this is an attempt to alpha-normalize them,
+    // before some further comparisons
+    if(t1->isLiteral() && t1->functor() == 0) {
       t1=Renaming::normalize(static_cast<Literal*>(t1));
       t2=Renaming::normalize(static_cast<Literal*>(t2));
 

Kernel/MLMatcher.cpp

@@ -469,7 +469,7 @@ void MLMatcher::Impl::initMatchingData(Literal** baseLits0, unsigned baseLen, Cl
     LiteralList::Iterator ait(s_altsArr[i]);
     while(ait.hasNext()) {
       currAltCnt++;
-      if(ait.next()->commutative()) {
+      if(ait.next()->isEquality()) {
 	currAltCnt++;
       }
     }

Kernel/MLMatcherSD.cpp

@@ -805,7 +805,7 @@ void MLMatcherSD::Impl::initMatchingData(Literal** baseLits0, unsigned baseLen,
     LiteralList::Iterator ait(s_altsArr[i]);
     while(ait.hasNext()) {
       currAltCnt++;
-      if(ait.next()->commutative()) {
+      if(ait.next()->isEquality()) {
         currAltCnt++;
       }
     }

Kernel/MLVariant.cpp

@@ -105,7 +105,7 @@ bool createLiteralBindings(Literal* baseLit, LiteralList* alts, Clause* instCl,
   while(ait.hasNext()) {
     //handle multiple matches in equality!
     Literal* alit=ait.next();
-    if(alit->commutative()) {
+    if(alit->isEquality()) {
       //we must try both possibilities
       if(MatchingUtils::haveVariantArgs(baseLit,alit)) {
         ArrayStoringBinder binder(altBindingData, variablePositions);
@@ -339,7 +339,7 @@ MatchingData* getMatchingData(Literal* const * baseLits0, unsigned baseLen, Clau
     LiteralList::Iterator ait(altsArr[i]);
     while(ait.hasNext()) {
       currAltCnt++;
-      if(ait.next()->commutative()) {
+      if(ait.next()->isEquality()) {
 	currAltCnt++;
       }
     }