diff --git a/Inferences/Instantiation.cpp b/Inferences/Instantiation.cpp index 396b5d0c0d..cc4a23a4ce 100644 --- a/Inferences/Instantiation.cpp +++ b/Inferences/Instantiation.cpp @@ -157,11 +157,11 @@ void Instantiation::tryMakeLiteralFalse(Literal* lit, Stack& subs) CALL("Instantiation::tryMakeLiteralFalse"); if(theory->isInterpretedPredicate(lit)){ - Interpretation interpretation = theory->interpretPredicate(lit); + Interpretation itp = theory->interpretPredicate(lit); //unsigned sort = theory->getOperationSort(interpretation); //TODO, very limited consideration, expand - if (interpretation == Theory::INT_LESS || interpretation == Theory::RAT_LESS || interpretation == Theory::REAL_LESS || lit->isEquality() ) { + if (itp == Theory::EQUAL || itp == Theory::INT_LESS || itp == Theory::RAT_LESS || itp == Theory::REAL_LESS) { TermList* left = lit->nthArgument(0); TermList* right = lit->nthArgument(1); unsigned var; Term* t = 0; diff --git a/Kernel/InterpretedLiteralEvaluator.cpp b/Kernel/InterpretedLiteralEvaluator.cpp index 5c494fe69c..349c2840d6 100644 --- a/Kernel/InterpretedLiteralEvaluator.cpp +++ b/Kernel/InterpretedLiteralEvaluator.cpp @@ -71,7 +71,7 @@ class InterpretedLiteralEvaluator::EqualityEvaluator : public Evaluator { bool canEvaluatePred(unsigned pred) override { - return pred == 0; // the equality predicate + return Signature::isEqualityPredicate(pred); } template @@ -399,10 +399,6 @@ class InterpretedLiteralEvaluator::TypedEvaluator : public Evaluator { CALL("InterpretedLiteralEvaluator::TypedEvaluator::canEvaluatePred"); - if (pred == 0) { // these guyes don't do it for equality - return false; - } - if (!theory->isInterpretedPredicate(pred)) { return false; } @@ -833,10 +829,8 @@ bool InterpretedLiteralEvaluator::balancable(Literal* lit) if(!theory->isInterpretedPredicate(lit->functor())) return false; // the perdicate must be binary - if (!lit->isEquality()) { - Interpretation ip = theory->interpretPredicate(lit->functor()); - if(theory->getArity(ip)!=2) return false; - } + Interpretation ip = theory->interpretPredicate(lit->functor()); + if(theory->getArity(ip)!=2) return false; // one side must be a constant and the other interpretted // the other side can contain at most one variable or uninterpreted subterm diff --git a/Kernel/Ordering.cpp b/Kernel/Ordering.cpp index c62f81a9ea..4eb27f253a 100644 --- a/Kernel/Ordering.cpp +++ b/Kernel/Ordering.cpp @@ -287,8 +287,8 @@ Ordering::Result PrecedenceOrdering::compare(Literal* l1, Literal* l2) const int PrecedenceOrdering::predicateLevel (unsigned pred) const { int basic=pred >= _predicates ? 1 : _predicateLevels[pred]; - if(NONINTERPRETED_LEVEL_BOOST && !env.signature->getPredicate(pred)->interpreted() - && pred != 0) { // special case for equality - we don't call it interpreted anymore + if(NONINTERPRETED_LEVEL_BOOST && !env.signature->getPredicate(pred)->interpreted()) { + ASS(!Signature::isEqualityPredicate(pred)); //equality is always interpreted basic+=NONINTERPRETED_LEVEL_BOOST; } if(env.signature->predicateColored(pred)) { diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp index d4bf336f38..760e9a10fa 100644 --- a/Kernel/Signature.cpp +++ b/Kernel/Signature.cpp @@ -218,7 +218,7 @@ Signature::Signature (): CALL("Signature::Signature"); // initialize equality - addPredicate("=", 2); + addInterpretedPredicate(Theory::EQUAL, OperatorType::getPredicateType(2), "="); ASS_EQ(predicateName(0), "="); //equality must have number 0 getPredicate(0)->markSkip(); diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index 86b7915c49..210b900ca6 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -434,6 +434,12 @@ class Signature return _preds[n]; } // getPredicate + static inline bool isEqualityPredicate(unsigned p) + { + // we make sure equality is always 0 + return (p == 0); // see the ASSERT in Signature::Signature + } + Signature(); ~Signature(); diff --git a/Kernel/Theory.cpp b/Kernel/Theory.cpp index 2e8fefcb5a..2963dabe66 100644 --- a/Kernel/Theory.cpp +++ b/Kernel/Theory.cpp @@ -590,6 +590,8 @@ unsigned Theory::getArity(Interpretation i) return 1; + case EQUAL: + case INT_GREATER: case INT_GREATER_EQUAL: case INT_LESS: @@ -802,6 +804,7 @@ bool Theory::hasSingleSort(Interpretation i) CALL("Theory::hasSingleSort"); switch(i) { + case EQUAL: // This not SingleSort because we don't know the sorts of its args case INT_TO_RAT: case INT_TO_REAL: case RAT_TO_INT: @@ -828,6 +831,7 @@ bool Theory::isPolymorphic(Interpretation i) } switch(i) { + case EQUAL: case ARRAY_SELECT: case ARRAY_BOOL_SELECT: case ARRAY_STORE: @@ -1452,7 +1456,7 @@ bool Theory::isInterpretedPredicate(unsigned pred) { CALL("Theory::isInterpretedPredicate(unsigned)"); - return pred == 0 || env.signature->getPredicate(pred)->interpreted(); + return env.signature->getPredicate(pred)->interpreted(); } /** @@ -1828,6 +1832,8 @@ vstring Theory::tryGetInterpretedLaTeXName(unsigned func, bool pred,bool polarit //TODO do we want special symbols for quotient, remainder, floor, ceiling, truncate, round? switch(i){ + case EQUAL:return "a0 "+pol+"= a1"; + case INT_SUCCESSOR: return "a0++"; case INT_UNARY_MINUS: case RAT_UNARY_MINUS: diff --git a/Kernel/Theory.hpp b/Kernel/Theory.hpp index 379c04b94f..167fcfa9c6 100644 --- a/Kernel/Theory.hpp +++ b/Kernel/Theory.hpp @@ -285,6 +285,8 @@ class Theory enum Interpretation { //predicates + EQUAL, + INT_IS_INT, INT_IS_RAT, INT_IS_REAL, diff --git a/Shell/InterpretedNormalizer.cpp b/Shell/InterpretedNormalizer.cpp index 82d9965070..c30c4b8034 100644 --- a/Shell/InterpretedNormalizer.cpp +++ b/Shell/InterpretedNormalizer.cpp @@ -259,7 +259,7 @@ class InterpretedNormalizer::NLiteralTransformer : private TermTransformer { CALL("InterpretedNormalizer::NLiteralTransformer::apply"); - if (!lit->isEquality() && theory->isInterpretedPredicate(lit)) // don't do this for equality which is interpreted, but does not have an interpretation + if (!lit->isEquality() && theory->isInterpretedPredicate(lit)) { Interpretation itp = theory->interpretPredicate(lit); if(isTrivialInterpretation(itp)) { diff --git a/Shell/Property.cpp b/Shell/Property.cpp index 1c98feb079..1a8ef4be4e 100644 --- a/Shell/Property.cpp +++ b/Shell/Property.cpp @@ -615,7 +615,7 @@ void Property::scanForInterpreted(Term* t) if (t->isLiteral()) { Literal* lit = static_cast(t); if (!theory->isInterpretedPredicate(lit)) { return; } - if(lit->isEquality()){ + if (lit->isEquality()) { //cout << "this is interpreted equality " << t->toString() << endl; _hasInterpretedEquality=true; return;