remove the commutative bit, equations still treated as commutative

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,8 @@ struct NormalizedLinearComparatorByWeight : public LiteralComparator
 	      static_cast<Literal*>(t2)->polarity());
     }
 
-    if(t1->commutative()) {
-      ASS(t2->commutative());
-      ASS(t1->isLiteral());
-      ASS_EQ(t1->arity(),2);
-
+    // TODO ...why?
+    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++;
       }
     }

Kernel/Matcher.cpp

@@ -103,7 +103,7 @@ bool MatchingUtils::isVariant(Literal* l1, Literal* l2, bool complementary)
   if(!complementary && l1==l2) {
     return true;
   }
-  if(l1->commutative()) {
+  if(l1->isEquality()) {
     return haveVariantArgs(l1,l2) || haveReversedVariantArgs(l1,l2);
   } else {
     return haveVariantArgs(l1,l2);
@@ -243,167 +243,6 @@ bool MatchingUtils::matchTerms(TermList base, TermList instance)
   }
 }
 
-
-//////////////// FastMatchIterator ////////////////////
-
-void OCMatchIterator::init(Literal* base, Literal* inst, bool complementary)
-{
-  //TODO we don't seem to use this iterator anywhere, so
-  //have not updated to polymorphism
-  if(!Literal::headersMatch(base, inst, complementary)) {
-    _finished=true;
-    return;
-  }
-  _finished=false;
-  _firstMatchDone=false;
-  _base=base;
-  _inst=inst;
-}
-
-bool OCMatchIterator::tryNextMatch()
-{
-  if(_finished) {
-    return false;
-  }
-  bool success=false;
-  if(!_firstMatchDone) {
-    _firstMatchDone=true;
-    if(!_base->commutative()) {
-      _finished=true;
-    }
-    reset();
-    success=tryDirectMatch();
-  }
-
-  if(!success && !_finished) {
-    ASS(_base->commutative());
-    _finished=true;
-
-    reset();
-    success=tryReversedMatch();
-  }
-  return success;
-}
-
-void OCMatchIterator::reset()
-{
-  _bindings.reset();
-  _bound.reset();
-}
-
-bool OCMatchIterator::tryDirectMatch()
-{
-  bool res=MatchingUtils::matchArgs(_base, _inst, *this);
-  res&=occursCheck();
-  return res;
-}
-
-bool OCMatchIterator::tryReversedMatch()
-{
-  ASS(_base->commutative());
-  ASS(_inst->commutative());
-
-  bool res=MatchingUtils::matchTerms(*_base->nthArgument(0), *_inst->nthArgument(1), *this);
-  if(res) {
-    res=MatchingUtils::matchTerms(*_base->nthArgument(1), *_inst->nthArgument(0), *this);
-  }
-  res&=occursCheck();
-  return res;
-}
-
-bool OCMatchIterator::occursCheck()
-{
-  static DHMap<unsigned, OCStatus> statuses;
-  static Stack<int> toDo;
-  statuses.reset();
-  toDo.reset();
-  BoundStack::Iterator bit(_bound);
-  while(bit.hasNext()) {
-    unsigned var0=bit.next();
-    OCStatus* pst0;
-    if(!statuses.getValuePtr(var0, pst0)) {
-      ASS_EQ(*pst0, CHECKED);
-      continue;
-    }
-
-    *pst0=ENQUEUED;
-    toDo.push(var0);
-
-    while(toDo.isNonEmpty()) {
-      int task=toDo.pop();
-      if(task==-1) {
-  unsigned var=toDo.pop();
-  ASS_EQ(statuses.get(var), TRAVERSING);
-  statuses.set(var, CHECKED);
-  continue;
-      }
-
-      unsigned var=task;
-
-      ASS_EQ(statuses.get(var), ENQUEUED);
-      statuses.set(var, TRAVERSING);
-
-      //this schedules the update of the state to CHECKED
-      toDo.push(var);
-      toDo.push(-1);
-
-      TermList tgt;
-      if(!_bindings.find(var, tgt)) {
-  continue;
-      }
-//      if(tgt.isVar()) {
-//  int tvar=tgt.var();
-//  if(var<tvar) {
-//
-//  }
-//  NOT_IMPLEMENTED;
-//      }
-//      VariableIterator vit(tgt.term());
-      VariableIterator vit(tgt);
-      while(vit.hasNext()) {
-  unsigned chvar=vit.next().var(); //child variable number
-
-  OCStatus* pChStatus;
-  if(!statuses.getValuePtr(chvar, pChStatus)) {
-    if(*pChStatus==TRAVERSING) {
-      return false;
-    }
-    ASS_REP(*pChStatus==CHECKED||*pChStatus==ENQUEUED, *pChStatus);
-    continue;
-  }
-  *pChStatus=ENQUEUED;
-
-  toDo.push(chvar);
-      }
-
-    }
-  }
-  return true;
-}
-
-TermList OCMatchIterator::apply(unsigned var)
-{
-  TermList bnd;
-  if(_bindings.find(var, bnd)) {
-    //this may lead to an indirect recursion, but if the occurs check
-    //has passed, it won't get into an infinite cycle
-    return apply(bnd);
-  }
-  //variable is unbound
-  return TermList(var, false);
-}
-
-TermList OCMatchIterator::apply(TermList t)
-{
-  return SubstHelper::apply(t, *this);
-}
-
-Literal* OCMatchIterator::apply(Literal* lit)
-{
-  return SubstHelper::apply(lit, *this);
-}
-
-
 //////////////// Matcher ////////////////////
 
 class Matcher::CommutativeMatchIterator
@@ -414,7 +253,7 @@ class Matcher::CommutativeMatchIterator
   : _matcher(matcher), _base(base), _instance(instance),
   _state(FIRST), _used(true)
   {
-    ASS(_base->commutative());
+    ASS(_base->isEquality());
     ASS_EQ(_base->arity(), 2);
   }
   ~CommutativeMatchIterator()
@@ -538,7 +377,7 @@ MatchIterator Matcher::matches(Literal* base, Literal* instance,
   if(base->arity()==0) {
     return pvi( getSingletonIterator(this) );
   }
-  if( !base->commutative() ) {
+  if( !base->isEquality() ) {
     return pvi( getContextualIterator(getSingletonIterator(this),
         MatchContext(base, instance)) );
   }
@@ -567,7 +406,7 @@ bool Matcher::matchArgs(Literal* base, Literal* instance)
 
 bool Matcher::matchReversedArgs(Literal* base, Literal* instance)
 {
-  ASS(base->commutative());
+  ASS(base->isEquality());
 
   BacktrackData localBD;