From b1b0db6795f3ee118b7ae1d41ad859e3f08da6cf Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Sun, 12 Nov 2017 20:01:25 +0100 Subject: [PATCH] remove Theory::Equalit from Interpretations --- Inferences/Instantiation.cpp | 79 ++++++++++++-------------- Kernel/InterpretedLiteralEvaluator.cpp | 25 ++------ Kernel/Signature.cpp | 2 +- Kernel/Theory.cpp | 8 --- Kernel/Theory.hpp | 3 - Shell/Property.cpp | 4 +- 6 files changed, 44 insertions(+), 77 deletions(-) diff --git a/Inferences/Instantiation.cpp b/Inferences/Instantiation.cpp index 58bfa8688f..396b5d0c0d 100644 --- a/Inferences/Instantiation.cpp +++ b/Inferences/Instantiation.cpp @@ -156,53 +156,44 @@ void Instantiation::tryMakeLiteralFalse(Literal* lit, Stack& subs) { CALL("Instantiation::tryMakeLiteralFalse"); - if(theory->isInterpretedPredicate(lit)){ - Interpretation interpretation = theory->interpretPredicate(lit); - //unsigned sort = theory->getOperationSort(interpretation); - - //TODO, very limited consideration, expand - switch(interpretation){ - case Theory::EQUAL: - case Theory::INT_LESS: // do these less_equal cases make sense? - case Theory::RAT_LESS: - case Theory::REAL_LESS: - { - TermList* left = lit->nthArgument(0); TermList* right = lit->nthArgument(1); - unsigned var; - Term* t = 0; - if(left->isVar() && !right->isVar()){ - t = right->term(); - var = left->var(); - } - if(right->isVar() && !left->isVar()){ - t = left->term(); - var = right->var(); - } - if(t){ - // do occurs check - VariableIterator vit(t); - while(vit.hasNext()) if(vit.next().var()==var) return; - - // we are okay - Substitution s1; - s1.bind(var,t); - subs.push(s1); - if(lit->polarity()){ - t = tryGetDifferentValue(t); - if(t){ - Substitution s2; - s2.bind(var,t); - subs.push(s2); - } - } - } - break; + if(theory->isInterpretedPredicate(lit)){ + Interpretation interpretation = 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() ) { + TermList* left = lit->nthArgument(0); TermList* right = lit->nthArgument(1); + unsigned var; + Term* t = 0; + if(left->isVar() && !right->isVar()){ + t = right->term(); + var = left->var(); + } + if(right->isVar() && !left->isVar()){ + t = left->term(); + var = right->var(); + } + if(t){ + // do occurs check + VariableIterator vit(t); + while(vit.hasNext()) if(vit.next().var()==var) return; + + // we are okay + Substitution s1; + s1.bind(var,t); + subs.push(s1); + if(lit->polarity()){ + t = tryGetDifferentValue(t); + if(t){ + Substitution s2; + s2.bind(var,t); + subs.push(s2); + } } - default: //TODO cover other cases - break; } } - + // TODO cover other cases ... + } } Term* Instantiation::tryGetDifferentValue(Term* t) diff --git a/Kernel/InterpretedLiteralEvaluator.cpp b/Kernel/InterpretedLiteralEvaluator.cpp index 91820cd66f..8abb6e629b 100644 --- a/Kernel/InterpretedLiteralEvaluator.cpp +++ b/Kernel/InterpretedLiteralEvaluator.cpp @@ -49,7 +49,7 @@ class InterpretedLiteralEvaluator::Evaluator virtual ~Evaluator() {} - bool canEvaluateFunc(unsigned func) + virtual bool canEvaluateFunc(unsigned func) { CALL("InterpretedLiteralEvaluator::Evaluator::canEvaluateFunc"); @@ -60,7 +60,7 @@ class InterpretedLiteralEvaluator::Evaluator return canEvaluate(interp); } - bool canEvaluatePred(unsigned pred) + virtual bool canEvaluatePred(unsigned pred) { CALL("InterpretedLiteralEvaluator::Evaluator::canEvaluatePred"); @@ -71,7 +71,7 @@ class InterpretedLiteralEvaluator::Evaluator return canEvaluate(interp); } - virtual bool canEvaluate(Interpretation interp) = 0; + virtual bool canEvaluate(Interpretation interp) { return false; } virtual bool tryEvaluateFunc(Term* trm, TermList& res) { return false; } virtual bool tryEvaluatePred(Literal* trm, bool& res) { return false; } }; @@ -90,15 +90,8 @@ class InterpretedLiteralEvaluator::Evaluator class InterpretedLiteralEvaluator::EqualityEvaluator : public Evaluator { - - virtual bool canEvaluate(Interpretation interp) - { - return interp==Interpretation::EQUAL; - } - - virtual bool tryEvaluateFunc(Term* trm, TermList& res) - { - ASSERTION_VIOLATION; // EQUAL is a predicate, not a function! + bool canEvaluatePred(unsigned pred) override { + return pred == 0; // the equality predicate } template @@ -123,14 +116,8 @@ class InterpretedLiteralEvaluator::EqualityEvaluator { CALL("InterpretedLiteralEvaluator::EqualityEvaluator::tryEvaluatePred"); - // Return if this is not an equality between theory terms - if(!theory->isInterpretedPredicate(lit)){ return false; } - try{ - - Interpretation itp = theory->interpretPredicate(lit); - ASS(itp==Interpretation::EQUAL); - ASS(theory->getArity(itp)==2); + ASS(lit->isEquality()); // We try and interpret the equality as a number of different sorts // If it is not an equality between two constants of the same sort the diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp index 07af1b818d..88a4581bce 100644 --- a/Kernel/Signature.cpp +++ b/Kernel/Signature.cpp @@ -218,7 +218,7 @@ Signature::Signature (): CALL("Signature::Signature"); // initialize equality - addInterpretedPredicate(Theory::EQUAL, OperatorType::getPredicateType(2), "="); + addPredicate("=", 2); ASS_EQ(predicateName(0), "="); //equality must have number 0 getPredicate(0)->markSkip(); diff --git a/Kernel/Theory.cpp b/Kernel/Theory.cpp index 60c115e12b..7d1fe68b50 100644 --- a/Kernel/Theory.cpp +++ b/Kernel/Theory.cpp @@ -590,8 +590,6 @@ unsigned Theory::getArity(Interpretation i) return 1; - case EQUAL: - case INT_GREATER: case INT_GREATER_EQUAL: case INT_LESS: @@ -729,8 +727,6 @@ bool Theory::isFunction(Interpretation i) return true; - case EQUAL: - case INT_GREATER: case INT_GREATER_EQUAL: case INT_LESS: @@ -806,7 +802,6 @@ 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: @@ -829,7 +824,6 @@ bool Theory::isPolymorphic(Interpretation i) CALL("Theory::isPolymorphic"); switch(i) { - case EQUAL: case ARRAY_SELECT: case ARRAY_BOOL_SELECT: case ARRAY_STORE: @@ -1835,8 +1829,6 @@ vstring Theory::tryGetInterpretedLaTeXName(unsigned func, bool pred,bool polarit case RAT_UNARY_MINUS: case REAL_UNARY_MINUS: return "-a0"; - case EQUAL:return "a0 "+pol+"= a1"; - case INT_GREATER: return "a0 "+pol+"> a1"; case INT_GREATER_EQUAL: return "a0 "+pol+"\\geq a1"; case INT_LESS: return "a0 "+pol+"< a1"; diff --git a/Kernel/Theory.hpp b/Kernel/Theory.hpp index f15e451766..a7a5782da0 100644 --- a/Kernel/Theory.hpp +++ b/Kernel/Theory.hpp @@ -285,9 +285,6 @@ class Theory enum Interpretation { //predicates - - EQUAL, - INT_IS_INT, INT_IS_RAT, INT_IS_REAL, diff --git a/Shell/Property.cpp b/Shell/Property.cpp index f46399eff2..8b78ac8080 100644 --- a/Shell/Property.cpp +++ b/Shell/Property.cpp @@ -615,12 +615,12 @@ void Property::scanForInterpreted(Term* t) if (t->isLiteral()) { Literal* lit = static_cast(t); if (!theory->isInterpretedPredicate(lit)) { return; } - itp = theory->interpretPredicate(lit); - if(itp==Theory::EQUAL){ + if(lit->isEquality()){ //cout << "this is interpreted equality " << t->toString() << endl; _hasInterpretedEquality=true; return; } + itp = theory->interpretPredicate(lit); } else { if (!theory->isInterpretedFunction(t)) { return; }