Fix KBOForEPR polymorphism bug

[ibnyusuf]

KBOForEPR assumes that all arguments to a predicate symbol are either variables or constants. We were not checking this properly for polymorphic predicate symbols previously. This PR should fix the bug.

[MichaelRawson]

Nice! Theoretical question: if we have only fully-applied type constructors (like in the Z3 PR), could we still use KBOForEPR in that case?

[ibnyusuf]

Nice! Theoretical question: if we have only fully-applied type constructors (like in the Z3 PR), could we still use KBOForEPR in that case?

No. In the current implementation of KBOforEPR, we make certain assumptions that are no longer valid in the presence of function symbols or type constructors with arity > 0.

For example:

Comparison arComp=Int::compare(l1->arity(),l2->arity());
    if(arComp!=Lib::EQUAL) {
      //since on the ground level each literal argument must be a constant,
      //and all symbols are of weight 1, the literal with higher arity is
      //heavier and therefore greater
      return fromComparison(arComp);
    }

As soon as we allow symbols of arity > 0 the weight of the ground instance of a variable can be arbitrarily large, and the above optimisation is no longer valid.