From 7ff6b652facc717751a11cb7516450bf21993118 Mon Sep 17 00:00:00 2001 From: Simon Robillard Date: Fri, 3 Nov 2017 15:59:57 +0100 Subject: [PATCH 1/5] LPO ordering implemented --- Kernel/KBO.cpp | 536 +---------------------------------------- Kernel/KBO.hpp | 30 +-- Kernel/KBOForEPR.cpp | 2 +- Kernel/KBOForEPR.hpp | 2 +- Kernel/LPO.cpp | 280 ++++++++++++++++++++++ Kernel/LPO.hpp | 54 +++++ Kernel/Ordering.cpp | 554 ++++++++++++++++++++++++++++++++++++++++++- Kernel/Ordering.hpp | 30 +++ Makefile | 1 + Shell/Options.cpp | 9 +- Shell/Options.hpp | 7 + 11 files changed, 933 insertions(+), 572 deletions(-) create mode 100644 Kernel/LPO.cpp create mode 100644 Kernel/LPO.hpp diff --git a/Kernel/KBO.cpp b/Kernel/KBO.cpp index 2c12e00faf..291e8262ed 100644 --- a/Kernel/KBO.cpp +++ b/Kernel/KBO.cpp @@ -10,11 +10,6 @@ #include "Lib/Environment.hpp" #include "Lib/Comparison.hpp" -#include "Lib/DArray.hpp" -#include "Lib/DHMap.hpp" -#include "Lib/Int.hpp" -#include "Lib/Metaiterators.hpp" -#include "Lib/Random.hpp" #include "Indexing/TermSharing.hpp" @@ -24,16 +19,7 @@ #include "KBO.hpp" #include "Signature.hpp" -#include - - -#define NONINTERPRETED_PRECEDENCE_BOOST 0x1000 - -#define NONINTERPRETED_LEVEL_BOOST 0x1000 #define COLORED_WEIGHT_BOOST 0x10000 -#define COLORED_LEVEL_BOOST 0x10000 - -#include namespace Kernel { @@ -294,7 +280,7 @@ void KBO::State::traverse(Term* t1, Term* t2) * Create a KBO object. */ KBO::KBO(Problem& prb, const Options& opt) - : KBOBase(prb, opt) + : PrecedenceOrdering(prb, opt) { CALL("KBO::KBO"); @@ -458,525 +444,5 @@ int KBO::functionSymbolWeight(unsigned fun) const return weight; } -////////////////////////////////////////////////// -// KBOBase class -////////////////////////////////////////////////// - -/** - * Return the predicate level. If @b pred is less than or equal to - * @b _predicates, then the value is taken from the array _predicateLevels, - * otherwise it is defined to be 1 (to make it greater than the level - * of equality). If a predicate is colored, its level is multiplied by - * the COLORED_LEVEL_BOOST value. - * @since 11/05/2008 Manchester - */ -int KBOBase::predicateLevel (unsigned pred) const -{ - int basic=pred >= _predicates ? 1 : _predicateLevels[pred]; - if(NONINTERPRETED_LEVEL_BOOST && !env.signature->getPredicate(pred)->interpreted()) { - ASS_NEQ(pred,0); //equality is always interpreted - basic+=NONINTERPRETED_LEVEL_BOOST; - } - if(env.signature->predicateColored(pred)) { - ASS_NEQ(pred,0); //equality should never be colored - return COLORED_LEVEL_BOOST*basic; - } else { - return basic; - } -} // KBO::predicateLevel - - -/** - * Return the predicate precedence. If @b pred is less than or equal to - * @b _predicates, then the value is taken from the array _predicatePrecedences, - * otherwise it is defined to be @b pred (to make it greater than all - * previously introduced predicates). - * @since 11/05/2008 Manchester - */ -int KBOBase::predicatePrecedence (unsigned pred) const -{ - int res=pred >= _predicates ? (int)pred : _predicatePrecedences[pred]; - if(NONINTERPRETED_PRECEDENCE_BOOST) { - ASS_EQ(NONINTERPRETED_PRECEDENCE_BOOST & 1, 0); // an even number - - bool intp = env.signature->getPredicate(pred)->interpreted(); - res *= 2; - return intp ? res+1 : res+NONINTERPRETED_PRECEDENCE_BOOST; - } - return res; -} // KBO::predicatePrecedences - -Comparison KBOBase::compareFunctors(unsigned fun1, unsigned fun2) const -{ - CALL("KBOBase::compareFunctors"); - - if(fun1==fun2) { - return Lib::EQUAL; - } - switch(compareFunctionPrecedences(fun1, fun2)) { - case GREATER: return Lib::GREATER; - case LESS: return Lib::LESS; - default: - ASSERTION_VIOLATION; - } -} - -/** - * Compare precedences of two function symbols - */ -Ordering::Result KBOBase::compareFunctionPrecedences(unsigned fun1, unsigned fun2) const -{ - CALL("KBOBase::compareFunctionPrecedences"); - ASS_NEQ(fun1, fun2); - - // $$false is the smallest - if (env.signature->isFoolConstantSymbol(false,fun1)) { - return LESS; - } - if (env.signature->isFoolConstantSymbol(false,fun2)) { - return GREATER; - } - - // $$true is the second smallest - if (env.signature->isFoolConstantSymbol(true,fun1)) { - return LESS; - } - - if (env.signature->isFoolConstantSymbol(true,fun2)) { - return GREATER; - } - - Signature::Symbol* s1=env.signature->getFunction(fun1); - Signature::Symbol* s2=env.signature->getFunction(fun2); - // uninterpreted things are greater than interpreted things - if(!s1->interpreted()) { - if(s2->interpreted()) { - return GREATER; - } - //two non-interpreted functions - return fromComparison(Int::compare( - fun1 >= _functions ? (int)fun1 : _functionPrecedences[fun1], - fun2 >= _functions ? (int)fun2 : _functionPrecedences[fun2] )); - } - if(!s2->interpreted()) { - return LESS; - } - if(s1->arity()) { - if(!s2->arity()) { - return GREATER; - } - //two interpreted functions - return fromComparison(Int::compare(fun1, fun2)); - } - if(s2->arity()) { - return LESS; - } - //two interpreted constants - - if (!s1->numericConstant() || !s2->numericConstant()) { - return fromComparison(Int::compare(fun1, fun2)); - } - - Comparison cmpRes; - if(s1->integerConstant() && s2->integerConstant()) { - cmpRes = IntegerConstantType::comparePrecedence(s1->integerValue(), s2->integerValue()); - } - else if(s1->rationalConstant() && s2->rationalConstant()) { - cmpRes = RationalConstantType::comparePrecedence(s1->rationalValue(), s2->rationalValue()); - } - else if(s1->realConstant() && s2->realConstant()) { - cmpRes = RealConstantType::comparePrecedence(s1->realValue(), s2->realValue()); - } - else if(s1->integerConstant()) { - ASS_REP(s2->rationalConstant() || s2->realConstant(), s2->name()); - cmpRes = Lib::LESS; - } - else if(s2->integerConstant()) { - ASS_REP(s1->rationalConstant() || s1->realConstant(), s1->name()); - cmpRes = Lib::GREATER; - } - else if(s1->rationalConstant()) { - ASS_REP(s2->realConstant(), s2->name()); - cmpRes = Lib::LESS; - } - else if(s2->rationalConstant()) { - ASS_REP(s1->realConstant(), s1->name()); - cmpRes = Lib::GREATER; - } - else { - ASSERTION_VIOLATION; - cmpRes = Int::compare(fun1, fun2); - } - return fromComparison(cmpRes); -} - -template -struct FnBoostWrapper -{ - FnBoostWrapper(Comparator comp) : _comp(comp) {} - Comparator _comp; - - Comparison compare(unsigned f1, unsigned f2) - { - static Options::SymbolPrecedenceBoost boost = env.options->symbolPrecedenceBoost(); - Comparison res = EQUAL; - bool u1 = env.signature->getFunction(f1)->inUnit(); - bool u2 = env.signature->getFunction(f2)->inUnit(); - bool g1 = env.signature->getFunction(f1)->inGoal(); - bool g2 = env.signature->getFunction(f2)->inGoal(); - switch(boost){ - case Options::SymbolPrecedenceBoost::NONE: - break; - case Options::SymbolPrecedenceBoost::GOAL: - if(g1 && !g2){ res = GREATER; } - else if(!g1 && g2){ res = LESS; } - break; - case Options::SymbolPrecedenceBoost::UNIT: - if(u1 && !u2){ res = GREATER; } - else if(!u1 && u2){ res = LESS; } - break; - case Options::SymbolPrecedenceBoost::GOAL_UNIT: - if(g1 && !g2){ res = GREATER; } - else if(!g1 && g2){ res = LESS; } - else if(u1 && !u2){ res = GREATER; } - else if(!u1 && u2){ res = LESS; } - break; - } - if(res==EQUAL){ - res = _comp.compare(f1,f2); - } - return res; - } - -}; -template -struct PredBoostWrapper -{ - PredBoostWrapper(Comparator comp) : _comp(comp) {} - Comparator _comp; - - Comparison compare(unsigned p1, unsigned p2) - { - static Options::SymbolPrecedenceBoost boost = env.options->symbolPrecedenceBoost(); - Comparison res = EQUAL; - bool u1 = env.signature->getPredicate(p1)->inUnit(); - bool u2 = env.signature->getPredicate(p2)->inUnit(); - bool g1 = env.signature->getPredicate(p1)->inGoal(); - bool g2 = env.signature->getPredicate(p2)->inGoal(); - switch(boost){ - case Options::SymbolPrecedenceBoost::NONE: - break; - case Options::SymbolPrecedenceBoost::GOAL: - if(g1 && !g2){ res = GREATER; } - else if(!g1 && g2){ res = LESS; } - break; - case Options::SymbolPrecedenceBoost::UNIT: - if(u1 && !u2){ res = GREATER; } - else if(!u1 && u2){ res = LESS; } - break; - case Options::SymbolPrecedenceBoost::GOAL_UNIT: - if(g1 && !g2){ res = GREATER; } - else if(!g1 && g2){ res = LESS; } - else if(u1 && !u2){ res = GREATER; } - else if(!u1 && u2){ res = LESS; } - break; - } - if(res==EQUAL){ - res = _comp.compare(p1,p2); - } - return res; - } -}; - -struct FnFreqComparator -{ - Comparison compare(unsigned f1, unsigned f2) - { - unsigned c1 = env.signature->getFunction(f1)->usageCnt(); - unsigned c2 = env.signature->getFunction(f2)->usageCnt(); - Comparison res = Int::compare(c2,c1); - if(res==EQUAL){ - res = Int::compare(f1,f2); - } - return res; - } -}; -struct PredFreqComparator -{ - Comparison compare(unsigned p1, unsigned p2) - { - unsigned c1 = env.signature->getPredicate(p1)->usageCnt(); - unsigned c2 = env.signature->getPredicate(p2)->usageCnt(); - Comparison res = Int::compare(c2,c1); - if(res==EQUAL){ - res = Int::compare(p1,p2); - } - return res; - } -}; -struct FnRevFreqComparator -{ - Comparison compare(unsigned f1, unsigned f2) - { - unsigned c1 = env.signature->getFunction(f1)->usageCnt(); - unsigned c2 = env.signature->getFunction(f2)->usageCnt(); - Comparison res = Int::compare(c1,c2); - if(res==EQUAL){ - res = Int::compare(f1,f2); - } - return res; - } -}; -struct PredRevFreqComparator -{ - Comparison compare(unsigned p1, unsigned p2) - { - unsigned c1 = env.signature->getPredicate(p1)->usageCnt(); - unsigned c2 = env.signature->getPredicate(p2)->usageCnt(); - Comparison res = Int::compare(c1,c2); - if(res==EQUAL){ - res = Int::compare(p1,p2); - } - return res; - } -}; - -struct FnArityComparator -{ - Comparison compare(unsigned u1, unsigned u2) - { - Comparison res=Int::compare(env.signature->functionArity(u1), - env.signature->functionArity(u2)); - if(res==EQUAL) { - res=Int::compare(u1,u2); - } - return res; - } -}; -struct PredArityComparator -{ - Comparison compare(unsigned u1, unsigned u2) - { - Comparison res=Int::compare(env.signature->predicateArity(u1), - env.signature->predicateArity(u2)); - if(res==EQUAL) { - res=Int::compare(u1,u2); - } - return res; - } -}; - -struct FnRevArityComparator -{ - Comparison compare(unsigned u1, unsigned u2) - { - Comparison res=Int::compare(env.signature->functionArity(u2), - env.signature->functionArity(u1)); - if(res==EQUAL) { - res=Int::compare(u1,u2); - } - return res; - } -}; -struct PredRevArityComparator -{ - Comparison compare(unsigned u1, unsigned u2) - { - Comparison res=Int::compare(env.signature->predicateArity(u2), - env.signature->predicateArity(u1)); - if(res==EQUAL) { - res=Int::compare(u1,u2); - } - return res; - } -}; - -static void loadPermutationFromString(DArray& p, const vstring& str) { - CALL("loadPermutationFromString"); - - std::stringstream ss(str.c_str()); - unsigned i = 0; - unsigned val; - while (ss >> val) - { - if (i >= p.size()) { - break; - } - - if (val >= p.size()) { - break; - } - - p[i++] = val; - - if (ss.peek() == ',') - ss.ignore(); - } -} - -/** - * Create a KBOBase object. - */ -KBOBase::KBOBase(Problem& prb, const Options& opt) - : _predicates(env.signature->predicates()), - _functions(env.signature->functions()), - _predicateLevels(_predicates), - _predicatePrecedences(_predicates), - _functionPrecedences(_functions) -{ - CALL("KBOBase::KBOBase"); - ASS_G(_predicates, 0); - - DArray aux(32); - if(_functions) { - aux.initFromIterator(getRangeIterator(0u, _functions), _functions); - - if (!opt.functionPrecedence().empty()) { - BYPASSING_ALLOCATOR; - - vstring precedence; - ifstream precedence_file (opt.functionPrecedence().c_str()); - if (precedence_file.is_open() && getline(precedence_file, precedence)) { - loadPermutationFromString(aux,precedence); - precedence_file.close(); - } - } else { - switch(opt.symbolPrecedence()) { - case Shell::Options::SymbolPrecedence::ARITY: - aux.sort(FnBoostWrapper(FnArityComparator())); - break; - case Shell::Options::SymbolPrecedence::REVERSE_ARITY: - aux.sort(FnBoostWrapper(FnRevArityComparator())); - break; - case Shell::Options::SymbolPrecedence::FREQUENCY: - case Shell::Options::SymbolPrecedence::WEIGHTED_FREQUENCY: - aux.sort(FnBoostWrapper(FnFreqComparator())); - break; - case Shell::Options::SymbolPrecedence::REVERSE_FREQUENCY: - case Shell::Options::SymbolPrecedence::REVERSE_WEIGHTED_FREQUENCY: - aux.sort(FnBoostWrapper(FnRevFreqComparator())); - break; - case Shell::Options::SymbolPrecedence::OCCURRENCE: - break; - case Shell::Options::SymbolPrecedence::SCRAMBLE: - for(unsigned i=0;i<_functions;i++){ - unsigned j = Random::getInteger(_functions-i)+i; - unsigned tmp = aux[j]; - aux[j]=aux[i]; - aux[i]=tmp; - } - break; - } - } - - /* - cout << "Function precedences:" << endl; - for(unsigned i=0;i<_functions;i++){ - cout << env.signature->functionName(aux[i]) << " "; - } - cout << endl; - */ - - /* - cout << "Function precedence: "; - for(unsigned i=0;i<_functions;i++){ - cout << aux[i] << ","; - } - cout << endl; - */ - - for(unsigned i=0;i<_functions;i++) { - _functionPrecedences[aux[i]]=i; - } - } - - aux.initFromIterator(getRangeIterator(0u, _predicates), _predicates); - - if (!opt.predicatePrecedence().empty()) { - BYPASSING_ALLOCATOR; - - vstring precedence; - ifstream precedence_file (opt.predicatePrecedence().c_str()); - if (precedence_file.is_open() && getline(precedence_file, precedence)) { - loadPermutationFromString(aux,precedence); - precedence_file.close(); - } - } else { - switch(opt.symbolPrecedence()) { - case Shell::Options::SymbolPrecedence::ARITY: - aux.sort(PredBoostWrapper(PredArityComparator())); - break; - case Shell::Options::SymbolPrecedence::REVERSE_ARITY: - aux.sort(PredBoostWrapper(PredRevArityComparator())); - break; - case Shell::Options::SymbolPrecedence::FREQUENCY: - case Shell::Options::SymbolPrecedence::WEIGHTED_FREQUENCY: - aux.sort(PredBoostWrapper(PredFreqComparator())); - break; - case Shell::Options::SymbolPrecedence::REVERSE_FREQUENCY: - case Shell::Options::SymbolPrecedence::REVERSE_WEIGHTED_FREQUENCY: - aux.sort(PredBoostWrapper(PredRevFreqComparator())); - break; - case Shell::Options::SymbolPrecedence::OCCURRENCE: - break; - case Shell::Options::SymbolPrecedence::SCRAMBLE: - for(unsigned i=0;i<_predicates;i++){ - unsigned j = Random::getInteger(_predicates-i)+i; - unsigned tmp = aux[j]; - aux[j]=aux[i]; - aux[i]=tmp; - } - break; - } - } - /* - cout << "Predicate precedences:" << endl; - for(unsigned i=0;i<_predicates;i++){ - cout << env.signature->predicateName(aux[i]) << " "; - } - cout << endl; - */ - /* - cout << "Predicate precedence: "; - for(unsigned i=0;i<_predicates;i++){ - cout << aux[i] << ","; - } - cout << endl; - */ - - for(unsigned i=0;i<_predicates;i++) { - _predicatePrecedences[aux[i]]=i; - } - - switch(opt.literalComparisonMode()) { - case Shell::Options::LiteralComparisonMode::STANDARD: - _predicateLevels.init(_predicates, 1); - break; - case Shell::Options::LiteralComparisonMode::PREDICATE: - case Shell::Options::LiteralComparisonMode::REVERSE: - for(unsigned i=1;i<_predicates;i++) { - _predicateLevels[i]=_predicatePrecedences[i]+1; - } - break; - } - //equality is on the lowest level - _predicateLevels[0]=0; - - _reverseLCM = opt.literalComparisonMode()==Shell::Options::LiteralComparisonMode::REVERSE; - - for(unsigned i=1;i<_predicates;i++) { - Signature::Symbol* predSym = env.signature->getPredicate(i); - //consequence-finding name predicates have the lowest level - if(predSym->label()) { - _predicateLevels[i]=-1; - } - else if(predSym->equalityProxy()) { - //equality proxy predicates have the highest level (lower than colored predicates) - _predicateLevels[i]=_predicates+2; - } - - } -} - } diff --git a/Kernel/KBO.hpp b/Kernel/KBO.hpp index d087050797..2b77f2bed9 100644 --- a/Kernel/KBO.hpp +++ b/Kernel/KBO.hpp @@ -18,40 +18,12 @@ namespace Kernel { using namespace Lib; -class KBOBase -: public Ordering -{ -public: - virtual Comparison compareFunctors(unsigned fun1, unsigned fun2) const; - -protected: - KBOBase(Problem& prb, const Options& opt); - - Result compareFunctionPrecedences(unsigned fun1, unsigned fun2) const; - - int predicatePrecedence(unsigned pred) const; - int predicateLevel(unsigned pred) const; - - /** number of predicates in the signature at the time the order was created */ - unsigned _predicates; - /** number of functions in the signature at the time the order was created */ - unsigned _functions; - /** Array of predicate levels */ - DArray _predicateLevels; - /** Array of predicate precedences */ - DArray _predicatePrecedences; - /** Array of function precedences */ - DArray _functionPrecedences; - - bool _reverseLCM; -}; - /** * Class for instances of the Knuth-Bendix orderings * @since 30/04/2008 flight Brussels-Tel Aviv */ class KBO -: public KBOBase +: public PrecedenceOrdering { public: CLASS_NAME(KBO); diff --git a/Kernel/KBOForEPR.cpp b/Kernel/KBOForEPR.cpp index 7472a903fb..f6e75f0c00 100644 --- a/Kernel/KBOForEPR.cpp +++ b/Kernel/KBOForEPR.cpp @@ -33,7 +33,7 @@ using namespace Lib; * before any comparisons using this object are being made. */ KBOForEPR::KBOForEPR(Problem& prb, const Options& opt) - : KBOBase(prb, opt) + : PrecedenceOrdering(prb, opt) { CALL("KBOForEPR::KBOForEPR"); ASS_EQ(prb.getProperty()->maxFunArity(),0); diff --git a/Kernel/KBOForEPR.hpp b/Kernel/KBOForEPR.hpp index 34fd4b8cb0..ac29c28dff 100644 --- a/Kernel/KBOForEPR.hpp +++ b/Kernel/KBOForEPR.hpp @@ -19,7 +19,7 @@ using namespace Lib; * @since 30/04/2008 flight Brussels-Tel Aviv */ class KBOForEPR -: public KBOBase +: public PrecedenceOrdering { public: CLASS_NAME(KBOForEPR); diff --git a/Kernel/LPO.cpp b/Kernel/LPO.cpp new file mode 100644 index 0000000000..a245b8fcdb --- /dev/null +++ b/Kernel/LPO.cpp @@ -0,0 +1,280 @@ +/** + * @file LPO.cpp + * Implements class LPO for instances of the lexicographic path + * ordering + * + */ + +#include "Debug/Tracer.hpp" + + +#include "Lib/Environment.hpp" +#include "Lib/Comparison.hpp" + +#include "Indexing/TermSharing.hpp" + +#include "Shell/Options.hpp" + +#include "Term.hpp" +#include "LPO.hpp" +#include "Signature.hpp" + +namespace Kernel { + +using namespace Lib; +using namespace Shell; + +/** + * Compare arguments of literals l1 and l2 and return the result + * of the comparison. + */ +Ordering::Result LPO::compare(Literal* l1, Literal* l2) const +{ + CALL("LPO::compare(Literal*...)"); + ASS(l1->shared()); + ASS(l2->shared()); + + if (l1 == l2) { + return EQUAL; + } + + unsigned p1 = l1->functor(); + unsigned p2 = l2->functor(); + + if( (l1->isNegative() ^ l2->isNegative()) && (p1==p2) && + l1->weight()==l2->weight() && l1->vars()==l2->vars() && //this line is just optimization, so we don't check whether literals are opposite when they cannot be + l1==env.sharing->tryGetOpposite(l2)) { + return l1->isNegative() ? LESS : GREATER; + } + + if (p1 != p2) { + int lev1 = predicateLevel(p1); + int lev2 = predicateLevel(p2); + if (lev1 > lev2) { + return GREATER; + } + if (lev2 > lev1) { + return LESS; + } + } + + if(l1->isEquality()) { + ASS(l2->isEquality()); + return compareEqualities(l1, l2); + } + ASS(!l1->isEquality()); + + for (unsigned i = 0; i < l1->arity(); i++) { + Result res = compare(*l1->nthArgument(i), *l2->nthArgument(i)); + if (res != EQUAL) + return res; + } + return EQUAL; +} // LPO::compare() + +Ordering::Result LPO::compare(TermList tl1, TermList tl2) const +{ + CALL("LPO::compare(TermList, TermList)"); + + if(tl1==tl2) { + return EQUAL; + } + if(tl1.isOrdinaryVar()) { + return tl2.containsSubterm(tl1) ? LESS : INCOMPARABLE; + } + ASS(tl1.isTerm()); + return clpo(tl1.term(), tl2); +} + +Ordering::Result LPO::clpo(Term* t1, TermList tl2) const +{ + CALL("LPO::clpo"); + ASS(t1->shared()); + + if(tl2.isOrdinaryVar()) { + return t1->containsSubterm(tl2) ? GREATER : INCOMPARABLE; + } + + ASS(tl2.isTerm()); + Term* t2=tl2.term(); + + switch (compareFunctionPrecedences(t1->functor(), t2->functor())) { + case EQUAL: + return cLMA(t1, t2, t1->args(), t2->args(), t1->arity()); + case GREATER: + return cMA(t1, t2->args(), t2->arity()); + case LESS: + return Ordering::reverse(cMA(t2, t1->args(), t1->arity())); + default: + ASSERTION_VIOLATION; + // shouldn't happen because symbol precedence is assumed to be + // total, but if it is not then the following call is correct + return cAA(t1, t2, t1->args(), t2->args(), t1->arity(), t2->arity()); + } +} + +/* + * All TermList* are stored in reverse order (by design in Term), + * hence the weird pointer arithmetic + */ +Ordering::Result LPO::cMA(Term *s, TermList* tl, unsigned arity) const +{ + CALL("LPO::cMA"); + + ASS(s->shared()); + + for (unsigned i = 0; i < arity; i++) { + switch(clpo(s, *(tl - i))) { + case EQUAL: + case LESS: + return LESS; + case INCOMPARABLE: + return reverse(alpha(tl - i - 1, arity - i - 1, s)); + case GREATER: + break; + default: + ASSERTION_VIOLATION; + } + } + return GREATER; +} + +Ordering::Result LPO::cLMA(Term* s, Term* t, TermList* sl, TermList* tl, unsigned arity) const +{ + CALL("LPO::cLMA"); + ASS(s->shared()); + ASS(t->shared()); + + for (unsigned i = 0; i < arity; i++) { + switch(compare(*(sl - i), *(tl - i))) { + case EQUAL: + break; + case GREATER: + return cMA(s, tl - i - 1, arity - i - 1); + case LESS: + return reverse(cMA(t, sl - i - 1, arity - i - 1)); + case INCOMPARABLE: + return cAA(s, t, sl - i - 1, tl - i - 1, arity - i - 1, arity - i - 1); + default: + ASSERTION_VIOLATION; + } + } + return EQUAL; +} + +Ordering::Result LPO::cAA(Term* s, Term* t, TermList* sl, TermList* tl, unsigned arity1, unsigned arity2) const +{ + CALL("LPO::cAA"); + ASS(s->shared()); + ASS(t->shared()); + + switch (alpha(sl, arity1, t)) { + case GREATER: + return GREATER; + case INCOMPARABLE: + return reverse(alpha(tl, arity2, s)); + default: + ASSERTION_VIOLATION; + } +} + +// greater iff some exists s_i in sl such that s_i >= t +Ordering::Result LPO::alpha(TermList* sl, unsigned arity, Term *t) const +{ + CALL("LPO::alpha"); + ASS(t->shared()); + + for (unsigned i = 0; i < arity; i++) { + switch (lpo(t, *(sl - i))) { + case EQUAL: + case LESS: + return GREATER; + case GREATER: + case INCOMPARABLE: + break; + default: + ASSERTION_VIOLATION; + } + } + return INCOMPARABLE; +} + +Ordering::Result LPO::lpo(TermList tl1, TermList tl2) const +{ + CALL("LPO::lpo(TermList, TermList)"); + + if(tl1.isOrdinaryVar()) { + return INCOMPARABLE; + } + ASS(tl1.isTerm()); + return lpo(tl1.term(), tl2); +} + +// used when the first term is not a variable +Ordering::Result LPO::lpo(Term* t1, TermList tl2) const +{ + CALL("LPO::lpo(Term*, TermList)"); + + ASS(t1->shared()); + + if(tl2.isOrdinaryVar()) { + return t1->containsSubterm(tl2) ? GREATER : INCOMPARABLE; + } + + ASS(tl2.isTerm()); + Term* t2=tl2.term(); + + switch (compareFunctionPrecedences(t1->functor(), t2->functor())) { + case EQUAL: + lexMAE(t1, t2, t1->args(), t2->args(), t1->arity()); + case GREATER: + return majo(t1, t2->args(), t2->arity()); + default: + return alpha(t1->args(), t1->arity(), t2); + } +} + +Ordering::Result LPO::lexMAE(Term* s, Term* t, TermList* sl, TermList* tl, unsigned arity) const +{ + CALL("LPO::lexMAE"); + + ASS(s->shared()); + ASS(t->shared()); + + for (unsigned i = 0; i < arity; i++) { + switch (lpo(*(sl - i), *(tl - i))) { + case EQUAL: + break; + case GREATER: + return majo(s, tl - i - 1, arity - i - 1); + case INCOMPARABLE: + return alpha(sl - i - 1, arity - i - 1, t); + default: + ASSERTION_VIOLATION; + } + } + return GREATER; +} + +// greater if s is greater than every term in tl +Ordering::Result LPO::majo(Term* s, TermList* tl, unsigned arity) const +{ + CALL("LPO::majo"); + + ASS(s->shared()); + + for (unsigned i = 0; i < arity; i++) { + switch(lpo(s, *(tl - i))) { + case GREATER: + break; + case EQUAL: + case INCOMPARABLE: + return INCOMPARABLE; + default: + ASSERTION_VIOLATION; + } + } + return GREATER; +} + +} diff --git a/Kernel/LPO.hpp b/Kernel/LPO.hpp new file mode 100644 index 0000000000..5e1d242965 --- /dev/null +++ b/Kernel/LPO.hpp @@ -0,0 +1,54 @@ +/** + * @file LPO.hpp + * Defines class LPO for instances of the lexicographic path ordering + * + * The implementation of LPO follows "THINGS TO KNOW WHEN IMPLEMENTING + * LPO" (Löchner, 2006), in particular the function called "clpo_6". + */ + +#ifndef __LPO__ +#define __LPO__ + +#include "Forwards.hpp" + +#include "Ordering.hpp" + +namespace Kernel { + +using namespace Lib; + +/** + * Class for instances of the Knuth-Bendix orderings + */ +class LPO +: public PrecedenceOrdering +{ +public: + CLASS_NAME(LPO); + USE_ALLOCATOR(LPO); + + LPO(Problem& prb, const Options& opt) : + PrecedenceOrdering(prb, opt) + {} + virtual ~LPO() {} + + virtual Result compare(Literal* l1, Literal* l2) const; + virtual Result compare(TermList tl1, TermList tl2) const; +protected: + + Result cLMA(Term* s, Term* t, TermList* sl, TermList* tl, unsigned arity) const; + Result cMA(Term* t, TermList* tl, unsigned arity) const; + Result cAA(Term* s, Term* t, TermList* sl, TermList* tl, unsigned arity1, unsigned arity2) const; + Result alpha(TermList* tl, unsigned arity, Term *t) const; + Result clpo(Term* t1, TermList tl2) const; + Result lpo(TermList tl1, TermList tl2) const; + Result lpo(Term* t1, TermList tl2) const; + Result lexMAE(Term* s, Term* t, TermList* sl, TermList* tl, unsigned arity) const; + Result majo(Term* s, TermList* tl, unsigned arity) const; + + int functionSymbolWeight(unsigned fun) const; + +}; + +} +#endif diff --git a/Kernel/Ordering.cpp b/Kernel/Ordering.cpp index 3ae653e2d6..9fafb8b53e 100644 --- a/Kernel/Ordering.cpp +++ b/Kernel/Ordering.cpp @@ -3,16 +3,23 @@ * Implements class Ordering. */ +#include + #include "Forwards.hpp" #include "Lib/Environment.hpp" #include "Lib/Exception.hpp" #include "Lib/List.hpp" #include "Lib/SmartPtr.hpp" +#include "Lib/DHMap.hpp" +#include "Lib/Int.hpp" +#include "Lib/Metaiterators.hpp" +#include "Lib/Random.hpp" #include "Shell/Options.hpp" #include "Shell/Property.hpp" +#include "LPO.hpp" #include "KBO.hpp" #include "KBOForEPR.hpp" #include "Problem.hpp" @@ -20,6 +27,11 @@ #include "Ordering.hpp" +#define NONINTERPRETED_PRECEDENCE_BOOST 0x1000 + +#define NONINTERPRETED_LEVEL_BOOST 0x1000 +#define COLORED_LEVEL_BOOST 0x10000 + using namespace Lib; using namespace Kernel; @@ -93,11 +105,18 @@ Ordering* Ordering::create(Problem& prb, const Options& opt) { CALL("Ordering::create"); - // KBOForEPR does not support colors; TODO fix this! - if(prb.getProperty()->maxFunArity()==0 && !env.colorUsed) { - return new KBOForEPR(prb, opt); + switch (env.options->termOrdering()) { + case Options::TermOrdering::KBO: + // KBOForEPR does not support colors; TODO fix this! + if(prb.getProperty()->maxFunArity()==0 && !env.colorUsed) { + return new KBOForEPR(prb, opt); + } + return new KBO(prb, opt); + case Options::TermOrdering::LPO: + return new LPO(prb, opt); + default: + ASSERTION_VIOLATION; } - return new KBO(prb, opt); } @@ -191,4 +210,531 @@ Ordering::Result Ordering::getEqualityArgumentOrder(Literal* eq) const return res; } +////////////////////////////////////////////////// +// PrecedenceOrdering class +////////////////////////////////////////////////// + +/** + * Return the predicate level. If @b pred is less than or equal to + * @b _predicates, then the value is taken from the array _predicateLevels, + * otherwise it is defined to be 1 (to make it greater than the level + * of equality). If a predicate is colored, its level is multiplied by + * the COLORED_LEVEL_BOOST value. + */ +int PrecedenceOrdering::predicateLevel (unsigned pred) const +{ + int basic=pred >= _predicates ? 1 : _predicateLevels[pred]; + if(NONINTERPRETED_LEVEL_BOOST && !env.signature->getPredicate(pred)->interpreted()) { + ASS_NEQ(pred,0); //equality is always interpreted + basic+=NONINTERPRETED_LEVEL_BOOST; + } + if(env.signature->predicateColored(pred)) { + ASS_NEQ(pred,0); //equality should never be colored + return COLORED_LEVEL_BOOST*basic; + } else { + return basic; + } +} // LPO::predicateLevel + + +/** + * Return the predicate precedence. If @b pred is less than or equal to + * @b _predicates, then the value is taken from the array _predicatePrecedences, + * otherwise it is defined to be @b pred (to make it greater than all + * previously introduced predicates). + */ +int PrecedenceOrdering::predicatePrecedence (unsigned pred) const +{ + int res=pred >= _predicates ? (int)pred : _predicatePrecedences[pred]; + if(NONINTERPRETED_PRECEDENCE_BOOST) { + ASS_EQ(NONINTERPRETED_PRECEDENCE_BOOST & 1, 0); // an even number + + bool intp = env.signature->getPredicate(pred)->interpreted(); + res *= 2; + return intp ? res+1 : res+NONINTERPRETED_PRECEDENCE_BOOST; + } + return res; +} // LPO::predicatePrecedences + +Comparison PrecedenceOrdering::compareFunctors(unsigned fun1, unsigned fun2) const +{ + CALL("PrecedenceOrdering::compareFunctors"); + + if(fun1==fun2) { + return Lib::EQUAL; + } + switch(compareFunctionPrecedences(fun1, fun2)) { + case GREATER: return Lib::GREATER; + case LESS: return Lib::LESS; + default: + ASSERTION_VIOLATION; + } +} + +/** + * Compare precedences of two function symbols + */ +Ordering::Result PrecedenceOrdering::compareFunctionPrecedences(unsigned fun1, unsigned fun2) const +{ + CALL("PrecedenceOrdering::compareFunctionPrecedences"); + + if (fun1 == fun2) + return EQUAL; + + // $$false is the smallest + if (env.signature->isFoolConstantSymbol(false,fun1)) { + return LESS; + } + if (env.signature->isFoolConstantSymbol(false,fun2)) { + return GREATER; + } + + // $$true is the second smallest + if (env.signature->isFoolConstantSymbol(true,fun1)) { + return LESS; + } + + if (env.signature->isFoolConstantSymbol(true,fun2)) { + return GREATER; + } + + Signature::Symbol* s1=env.signature->getFunction(fun1); + Signature::Symbol* s2=env.signature->getFunction(fun2); + // term algebra constructors are smaller than other symbols + if(s1->termAlgebraCons() && !s2->termAlgebraCons()) { + return LESS; + } + if(!s1->termAlgebraCons() && s2->termAlgebraCons()) { + return GREATER; + } + // uninterpreted things are greater than interpreted things + if(!s1->interpreted()) { + if(s2->interpreted()) { + return GREATER; + } + //two non-interpreted functions + return fromComparison(Int::compare( + fun1 >= _functions ? (int)fun1 : _functionPrecedences[fun1], + fun2 >= _functions ? (int)fun2 : _functionPrecedences[fun2] )); + } + if(!s2->interpreted()) { + return LESS; + } + if(s1->arity()) { + if(!s2->arity()) { + return GREATER; + } + //two interpreted functions + return fromComparison(Int::compare(fun1, fun2)); + } + if(s2->arity()) { + return LESS; + } + //two interpreted constants + + if (!s1->numericConstant() || !s2->numericConstant()) { + return fromComparison(Int::compare(fun1, fun2)); + } + + Comparison cmpRes; + if(s1->integerConstant() && s2->integerConstant()) { + cmpRes = IntegerConstantType::comparePrecedence(s1->integerValue(), s2->integerValue()); + } + else if(s1->rationalConstant() && s2->rationalConstant()) { + cmpRes = RationalConstantType::comparePrecedence(s1->rationalValue(), s2->rationalValue()); + } + else if(s1->realConstant() && s2->realConstant()) { + cmpRes = RealConstantType::comparePrecedence(s1->realValue(), s2->realValue()); + } + else if(s1->integerConstant()) { + ASS_REP(s2->rationalConstant() || s2->realConstant(), s2->name()); + cmpRes = Lib::LESS; + } + else if(s2->integerConstant()) { + ASS_REP(s1->rationalConstant() || s1->realConstant(), s1->name()); + cmpRes = Lib::GREATER; + } + else if(s1->rationalConstant()) { + ASS_REP(s2->realConstant(), s2->name()); + cmpRes = Lib::LESS; + } + else if(s2->rationalConstant()) { + ASS_REP(s1->realConstant(), s1->name()); + cmpRes = Lib::GREATER; + } + else { + ASSERTION_VIOLATION; + cmpRes = Int::compare(fun1, fun2); + } + return fromComparison(cmpRes); +} + +template +struct FnBoostWrapper +{ + FnBoostWrapper(Comparator comp) : _comp(comp) {} + Comparator _comp; + + Comparison compare(unsigned f1, unsigned f2) + { + static Options::SymbolPrecedenceBoost boost = env.options->symbolPrecedenceBoost(); + Comparison res = EQUAL; + bool u1 = env.signature->getFunction(f1)->inUnit(); + bool u2 = env.signature->getFunction(f2)->inUnit(); + bool g1 = env.signature->getFunction(f1)->inGoal(); + bool g2 = env.signature->getFunction(f2)->inGoal(); + switch(boost){ + case Options::SymbolPrecedenceBoost::NONE: + break; + case Options::SymbolPrecedenceBoost::GOAL: + if(g1 && !g2){ res = GREATER; } + else if(!g1 && g2){ res = LESS; } + break; + case Options::SymbolPrecedenceBoost::UNIT: + if(u1 && !u2){ res = GREATER; } + else if(!u1 && u2){ res = LESS; } + break; + case Options::SymbolPrecedenceBoost::GOAL_UNIT: + if(g1 && !g2){ res = GREATER; } + else if(!g1 && g2){ res = LESS; } + else if(u1 && !u2){ res = GREATER; } + else if(!u1 && u2){ res = LESS; } + break; + } + if(res==EQUAL){ + res = _comp.compare(f1,f2); + } + return res; + } + +}; +template +struct PredBoostWrapper +{ + PredBoostWrapper(Comparator comp) : _comp(comp) {} + Comparator _comp; + + Comparison compare(unsigned p1, unsigned p2) + { + static Options::SymbolPrecedenceBoost boost = env.options->symbolPrecedenceBoost(); + Comparison res = EQUAL; + bool u1 = env.signature->getPredicate(p1)->inUnit(); + bool u2 = env.signature->getPredicate(p2)->inUnit(); + bool g1 = env.signature->getPredicate(p1)->inGoal(); + bool g2 = env.signature->getPredicate(p2)->inGoal(); + switch(boost){ + case Options::SymbolPrecedenceBoost::NONE: + break; + case Options::SymbolPrecedenceBoost::GOAL: + if(g1 && !g2){ res = GREATER; } + else if(!g1 && g2){ res = LESS; } + break; + case Options::SymbolPrecedenceBoost::UNIT: + if(u1 && !u2){ res = GREATER; } + else if(!u1 && u2){ res = LESS; } + break; + case Options::SymbolPrecedenceBoost::GOAL_UNIT: + if(g1 && !g2){ res = GREATER; } + else if(!g1 && g2){ res = LESS; } + else if(u1 && !u2){ res = GREATER; } + else if(!u1 && u2){ res = LESS; } + break; + } + if(res==EQUAL){ + res = _comp.compare(p1,p2); + } + return res; + } +}; + +struct FnFreqComparator +{ + Comparison compare(unsigned f1, unsigned f2) + { + unsigned c1 = env.signature->getFunction(f1)->usageCnt(); + unsigned c2 = env.signature->getFunction(f2)->usageCnt(); + Comparison res = Int::compare(c2,c1); + if(res==EQUAL){ + res = Int::compare(f1,f2); + } + return res; + } +}; +struct PredFreqComparator +{ + Comparison compare(unsigned p1, unsigned p2) + { + unsigned c1 = env.signature->getPredicate(p1)->usageCnt(); + unsigned c2 = env.signature->getPredicate(p2)->usageCnt(); + Comparison res = Int::compare(c2,c1); + if(res==EQUAL){ + res = Int::compare(p1,p2); + } + return res; + } +}; +struct FnRevFreqComparator +{ + Comparison compare(unsigned f1, unsigned f2) + { + unsigned c1 = env.signature->getFunction(f1)->usageCnt(); + unsigned c2 = env.signature->getFunction(f2)->usageCnt(); + Comparison res = Int::compare(c1,c2); + if(res==EQUAL){ + res = Int::compare(f1,f2); + } + return res; + } +}; +struct PredRevFreqComparator +{ + Comparison compare(unsigned p1, unsigned p2) + { + unsigned c1 = env.signature->getPredicate(p1)->usageCnt(); + unsigned c2 = env.signature->getPredicate(p2)->usageCnt(); + Comparison res = Int::compare(c1,c2); + if(res==EQUAL){ + res = Int::compare(p1,p2); + } + return res; + } +}; + +struct FnArityComparator +{ + Comparison compare(unsigned u1, unsigned u2) + { + Comparison res=Int::compare(env.signature->functionArity(u1), + env.signature->functionArity(u2)); + if(res==EQUAL) { + res=Int::compare(u1,u2); + } + return res; + } +}; +struct PredArityComparator +{ + Comparison compare(unsigned u1, unsigned u2) + { + Comparison res=Int::compare(env.signature->predicateArity(u1), + env.signature->predicateArity(u2)); + if(res==EQUAL) { + res=Int::compare(u1,u2); + } + return res; + } +}; + +struct FnRevArityComparator +{ + Comparison compare(unsigned u1, unsigned u2) + { + Comparison res=Int::compare(env.signature->functionArity(u2), + env.signature->functionArity(u1)); + if(res==EQUAL) { + res=Int::compare(u1,u2); + } + return res; + } +}; +struct PredRevArityComparator +{ + Comparison compare(unsigned u1, unsigned u2) + { + Comparison res=Int::compare(env.signature->predicateArity(u2), + env.signature->predicateArity(u1)); + if(res==EQUAL) { + res=Int::compare(u1,u2); + } + return res; + } +}; + +static void loadPermutationFromString(DArray& p, const vstring& str) { + CALL("loadPermutationFromString"); + + std::stringstream ss(str.c_str()); + unsigned i = 0; + unsigned val; + while (ss >> val) + { + if (i >= p.size()) { + break; + } + + if (val >= p.size()) { + break; + } + + p[i++] = val; + + if (ss.peek() == ',') + ss.ignore(); + } +} + +/** + * Create a PrecedenceOrdering object. + */ +PrecedenceOrdering::PrecedenceOrdering(Problem& prb, const Options& opt) + : _predicates(env.signature->predicates()), + _functions(env.signature->functions()), + _predicateLevels(_predicates), + _predicatePrecedences(_predicates), + _functionPrecedences(_functions) +{ + CALL("PrecedenceOrdering::PrecedenceOrdering"); + ASS_G(_predicates, 0); + + DArray aux(32); + if(_functions) { + aux.initFromIterator(getRangeIterator(0u, _functions), _functions); + + if (!opt.functionPrecedence().empty()) { + BYPASSING_ALLOCATOR; + + vstring precedence; + ifstream precedence_file (opt.functionPrecedence().c_str()); + if (precedence_file.is_open() && getline(precedence_file, precedence)) { + loadPermutationFromString(aux,precedence); + precedence_file.close(); + } + } else { + switch(opt.symbolPrecedence()) { + case Shell::Options::SymbolPrecedence::ARITY: + aux.sort(FnBoostWrapper(FnArityComparator())); + break; + case Shell::Options::SymbolPrecedence::REVERSE_ARITY: + aux.sort(FnBoostWrapper(FnRevArityComparator())); + break; + case Shell::Options::SymbolPrecedence::FREQUENCY: + case Shell::Options::SymbolPrecedence::WEIGHTED_FREQUENCY: + aux.sort(FnBoostWrapper(FnFreqComparator())); + break; + case Shell::Options::SymbolPrecedence::REVERSE_FREQUENCY: + case Shell::Options::SymbolPrecedence::REVERSE_WEIGHTED_FREQUENCY: + aux.sort(FnBoostWrapper(FnRevFreqComparator())); + break; + case Shell::Options::SymbolPrecedence::OCCURRENCE: + break; + case Shell::Options::SymbolPrecedence::SCRAMBLE: + for(unsigned i=0;i<_functions;i++){ + unsigned j = Random::getInteger(_functions-i)+i; + unsigned tmp = aux[j]; + aux[j]=aux[i]; + aux[i]=tmp; + } + break; + } + } + + + /*cout << "Function precedences:" << endl; + for(unsigned i=0;i<_functions;i++){ + cout << env.signature->functionName(aux[i]) << " "; + } + cout << endl;*/ + + + /* + cout << "Function precedence: "; + for(unsigned i=0;i<_functions;i++){ + cout << aux[i] << ","; + } + cout << endl; + */ + + for(unsigned i=0;i<_functions;i++) { + _functionPrecedences[aux[i]]=i; + } + } + + aux.initFromIterator(getRangeIterator(0u, _predicates), _predicates); + + if (!opt.predicatePrecedence().empty()) { + BYPASSING_ALLOCATOR; + + vstring precedence; + ifstream precedence_file (opt.predicatePrecedence().c_str()); + if (precedence_file.is_open() && getline(precedence_file, precedence)) { + loadPermutationFromString(aux,precedence); + precedence_file.close(); + } + } else { + switch(opt.symbolPrecedence()) { + case Shell::Options::SymbolPrecedence::ARITY: + aux.sort(PredBoostWrapper(PredArityComparator())); + break; + case Shell::Options::SymbolPrecedence::REVERSE_ARITY: + aux.sort(PredBoostWrapper(PredRevArityComparator())); + break; + case Shell::Options::SymbolPrecedence::FREQUENCY: + case Shell::Options::SymbolPrecedence::WEIGHTED_FREQUENCY: + aux.sort(PredBoostWrapper(PredFreqComparator())); + break; + case Shell::Options::SymbolPrecedence::REVERSE_FREQUENCY: + case Shell::Options::SymbolPrecedence::REVERSE_WEIGHTED_FREQUENCY: + aux.sort(PredBoostWrapper(PredRevFreqComparator())); + break; + case Shell::Options::SymbolPrecedence::OCCURRENCE: + break; + case Shell::Options::SymbolPrecedence::SCRAMBLE: + for(unsigned i=0;i<_predicates;i++){ + unsigned j = Random::getInteger(_predicates-i)+i; + unsigned tmp = aux[j]; + aux[j]=aux[i]; + aux[i]=tmp; + } + break; + } + } + /* + cout << "Predicate precedences:" << endl; + for(unsigned i=0;i<_predicates;i++){ + cout << env.signature->predicateName(aux[i]) << " "; + } + cout << endl; + */ + /* + cout << "Predicate precedence: "; + for(unsigned i=0;i<_predicates;i++){ + cout << aux[i] << ","; + } + cout << endl; + */ + + for(unsigned i=0;i<_predicates;i++) { + _predicatePrecedences[aux[i]]=i; + } + + switch(opt.literalComparisonMode()) { + case Shell::Options::LiteralComparisonMode::STANDARD: + _predicateLevels.init(_predicates, 1); + break; + case Shell::Options::LiteralComparisonMode::PREDICATE: + case Shell::Options::LiteralComparisonMode::REVERSE: + for(unsigned i=1;i<_predicates;i++) { + _predicateLevels[i]=_predicatePrecedences[i]+1; + } + break; + } + //equality is on the lowest level + _predicateLevels[0]=0; + + _reverseLCM = opt.literalComparisonMode()==Shell::Options::LiteralComparisonMode::REVERSE; + + for(unsigned i=1;i<_predicates;i++) { + Signature::Symbol* predSym = env.signature->getPredicate(i); + //consequence-finding name predicates have the lowest level + if(predSym->label()) { + _predicateLevels[i]=-1; + } + else if(predSym->equalityProxy()) { + //equality proxy predicates have the highest level (lower than colored predicates) + _predicateLevels[i]=_predicates+2; + } + + } +} + diff --git a/Kernel/Ordering.hpp b/Kernel/Ordering.hpp index 481a4eefa2..fd1ca74e39 100644 --- a/Kernel/Ordering.hpp +++ b/Kernel/Ordering.hpp @@ -14,6 +14,7 @@ #include "Lib/Comparison.hpp" #include "Lib/SmartPtr.hpp" +#include "Lib/DArray.hpp" #include "Lib/Allocator.hpp" @@ -138,6 +139,35 @@ class Ordering static OrderingSP s_globalOrdering; }; // class Ordering +// orderings that rely on symbol precedence +class PrecedenceOrdering +: public Ordering +{ +public: + virtual Comparison compareFunctors(unsigned fun1, unsigned fun2) const; + +protected: + PrecedenceOrdering(Problem& prb, const Options& opt); + + Result compareFunctionPrecedences(unsigned fun1, unsigned fun2) const; + + int predicatePrecedence(unsigned pred) const; + int predicateLevel(unsigned pred) const; + + /** number of predicates in the signature at the time the order was created */ + unsigned _predicates; + /** number of functions in the signature at the time the order was created */ + unsigned _functions; + /** Array of predicate levels */ + DArray _predicateLevels; + /** Array of predicate precedences */ + DArray _predicatePrecedences; + /** Array of function precedences */ + DArray _functionPrecedences; + + bool _reverseLCM; +}; + } #endif diff --git a/Makefile b/Makefile index d6ebd7aa2e..b7d1c2185a 100644 --- a/Makefile +++ b/Makefile @@ -190,6 +190,7 @@ VK_OBJ= Kernel/Clause.o\ Kernel/KBOForEPR.o\ Kernel/LiteralSelector.o\ Kernel/LookaheadLiteralSelector.o\ + Kernel/LPO.o\ Kernel/MainLoop.o\ Kernel/Matcher.o\ Kernel/MaximalLiteralSelector.o\ diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 09cb9c12d5..acb20bcd9c 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -1495,7 +1495,7 @@ void Options::Options::init() _literalComparisonMode = ChoiceOptionValue("literal_comparison_mode","lcm", LiteralComparisonMode::STANDARD, {"predicate","reverse","standard"}); - _literalComparisonMode.description="Vampire uses KBO which uses an ordering of predicates. Standard places equality (and certain other special predicates) first and all others second. Predicate depends on symbol precedence (see symbol_precedence). Reverse reverses the order."; + _literalComparisonMode.description="Vampire uses term orderings which use an ordering of predicates. Standard places equality (and certain other special predicates) first and all others second. Predicate depends on symbol precedence (see symbol_precedence). Reverse reverses the order."; _lookup.insert(&_literalComparisonMode); _literalComparisonMode.tag(OptionTag::SATURATION); _literalComparisonMode.addProblemConstraint(hasNonUnits()); @@ -1559,11 +1559,16 @@ void Options::Options::init() _activationLimit.setExperimental(); _lookup.insert(&_activationLimit); + _termOrdering = ChoiceOptionValue("term_ordering","to", TermOrdering::KBO, + {"kbo","lpo"}); + _termOrdering.description="The term ordering used by Vampire to orient equations and order literals"; + _termOrdering.tag(OptionTag::SATURATION); + _lookup.insert(&_termOrdering); _symbolPrecedence = ChoiceOptionValue("symbol_precedence","sp",SymbolPrecedence::ARITY, {"arity","occurrence","reverse_arity","scramble", "frequency","reverse_frequency", "weighted_frequency","reverse_weighted_frequency"}); - _symbolPrecedence.description="Vampire uses KBO which requires a precedence relation between symbols. Arity orders symbols by their arity (and reverse_arity takes the reverse of this) and occurence orders symbols by the order they appear in the problem."; + _symbolPrecedence.description="Vampire uses term orderings which require a precedence relation between symbols. Arity orders symbols by their arity (and reverse_arity takes the reverse of this) and occurence orders symbols by the order they appear in the problem."; _lookup.insert(&_symbolPrecedence); _symbolPrecedence.tag(OptionTag::SATURATION); _symbolPrecedence.setRandomChoices({"arity","occurence","reverse_arity","frequency"}); diff --git a/Shell/Options.hpp b/Shell/Options.hpp index bdabfd2cb3..00cc5fe64a 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -519,6 +519,11 @@ class Options ON = 2 }; + enum class TermOrdering : unsigned int { + KBO = 0, + LPO = 1, + }; + enum class SymbolPrecedence : unsigned int { ARITY = 0, OCCURRENCE = 1, @@ -1874,6 +1879,7 @@ class Options int simulatedTimeLimit() const { return _simulatedTimeLimit.actualValue; } void setSimulatedTimeLimit(int newVal) { _simulatedTimeLimit.actualValue = newVal; } int maxInferenceDepth() const { return _maxInferenceDepth.actualValue; } + TermOrdering termOrdering() const { return _termOrdering.actualValue; } SymbolPrecedence symbolPrecedence() const { return _symbolPrecedence.actualValue; } SymbolPrecedenceBoost symbolPrecedenceBoost() const { return _symbolPrecedenceBoost.actualValue; } const vstring& functionPrecedence() const { return _functionPrecedence.actualValue; } @@ -2338,6 +2344,7 @@ class Options ChoiceOptionValue _statistics; BoolOptionValue _superpositionFromVariables; + ChoiceOptionValue _termOrdering; ChoiceOptionValue _symbolPrecedence; ChoiceOptionValue _symbolPrecedenceBoost; StringOptionValue _functionPrecedence; From 07f710c68742adff1e960010db384bd62ec72b77 Mon Sep 17 00:00:00 2001 From: Simon Robillard Date: Fri, 3 Nov 2017 17:25:29 +0100 Subject: [PATCH 2/5] fix bug in LPO, related to predicate precedence --- Kernel/LPO.cpp | 35 ++++++++++++++++------------------- Kernel/LPO.hpp | 2 -- 2 files changed, 16 insertions(+), 21 deletions(-) diff --git a/Kernel/LPO.cpp b/Kernel/LPO.cpp index a245b8fcdb..17ad4efc62 100644 --- a/Kernel/LPO.cpp +++ b/Kernel/LPO.cpp @@ -47,29 +47,24 @@ Ordering::Result LPO::compare(Literal* l1, Literal* l2) const return l1->isNegative() ? LESS : GREATER; } - if (p1 != p2) { - int lev1 = predicateLevel(p1); - int lev2 = predicateLevel(p2); - if (lev1 > lev2) { - return GREATER; - } - if (lev2 > lev1) { - return LESS; + if (p1 == p2) { + if(l1->isEquality()) { + ASS(l2->isEquality()); + return compareEqualities(l1, l2); } - } + ASS(!l1->isEquality()); - if(l1->isEquality()) { - ASS(l2->isEquality()); - return compareEqualities(l1, l2); + // compare arguments in lexicographic order + for (unsigned i = 0; i < l1->arity(); i++) { + Result res = compare(*l1->nthArgument(i), *l2->nthArgument(i)); + if (res != EQUAL) + return res; + } + return EQUAL; } - ASS(!l1->isEquality()); - for (unsigned i = 0; i < l1->arity(); i++) { - Result res = compare(*l1->nthArgument(i), *l2->nthArgument(i)); - if (res != EQUAL) - return res; - } - return EQUAL; + ASS_NEQ(_predicatePrecedences[p1], _predicatePrecedences[p2]); // precedence should be total + return (_predicatePrecedences[p1] > _predicatePrecedences[p2]) ? GREATER : LESS; } // LPO::compare() Ordering::Result LPO::compare(TermList tl1, TermList tl2) const @@ -199,6 +194,8 @@ Ordering::Result LPO::alpha(TermList* sl, unsigned arity, Term *t) const return INCOMPARABLE; } +// unidirectional comparison function (returns correct result if tl1 > +// tl2 or tl1 = tl2) Ordering::Result LPO::lpo(TermList tl1, TermList tl2) const { CALL("LPO::lpo(TermList, TermList)"); diff --git a/Kernel/LPO.hpp b/Kernel/LPO.hpp index 5e1d242965..ebbf452997 100644 --- a/Kernel/LPO.hpp +++ b/Kernel/LPO.hpp @@ -46,8 +46,6 @@ class LPO Result lexMAE(Term* s, Term* t, TermList* sl, TermList* tl, unsigned arity) const; Result majo(Term* s, TermList* tl, unsigned arity) const; - int functionSymbolWeight(unsigned fun) const; - }; } From f054a674b389e9bfeaa22d105c9f0955167e147a Mon Sep 17 00:00:00 2001 From: Simon Robillard Date: Tue, 7 Nov 2017 10:12:30 +0100 Subject: [PATCH 3/5] fix lpo literal precedence --- Kernel/LPO.cpp | 7 ++++--- Kernel/LPO.hpp | 2 +- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/Kernel/LPO.cpp b/Kernel/LPO.cpp index 17ad4efc62..414790a4b9 100644 --- a/Kernel/LPO.cpp +++ b/Kernel/LPO.cpp @@ -28,7 +28,7 @@ using namespace Shell; * Compare arguments of literals l1 and l2 and return the result * of the comparison. */ -Ordering::Result LPO::compare(Literal* l1, Literal* l2) const +Ordering::Result LPO::compare(Literal* l1, Literal *l2) const { CALL("LPO::compare(Literal*...)"); ASS(l1->shared()); @@ -48,6 +48,7 @@ Ordering::Result LPO::compare(Literal* l1, Literal* l2) const } if (p1 == p2) { + ASS_EQ(l1->isNegative(), l1->isNegative()) if(l1->isEquality()) { ASS(l2->isEquality()); return compareEqualities(l1, l2); @@ -63,8 +64,8 @@ Ordering::Result LPO::compare(Literal* l1, Literal* l2) const return EQUAL; } - ASS_NEQ(_predicatePrecedences[p1], _predicatePrecedences[p2]); // precedence should be total - return (_predicatePrecedences[p1] > _predicatePrecedences[p2]) ? GREATER : LESS; + ASS_NEQ(predicatePrecedence(p1), predicatePrecedence(p2)); // precedence should be total + return (predicatePrecedence(p1) > predicatePrecedence(p2)) ? GREATER : LESS; } // LPO::compare() Ordering::Result LPO::compare(TermList tl1, TermList tl2) const diff --git a/Kernel/LPO.hpp b/Kernel/LPO.hpp index ebbf452997..97f8fd0a82 100644 --- a/Kernel/LPO.hpp +++ b/Kernel/LPO.hpp @@ -18,7 +18,7 @@ namespace Kernel { using namespace Lib; /** - * Class for instances of the Knuth-Bendix orderings + * Class for instances of the lexicographic path orderings */ class LPO : public PrecedenceOrdering From 2efc8a62f983e41750d7a0ee520c356706eff3eb Mon Sep 17 00:00:00 2001 From: Simon Robillard Date: Wed, 8 Nov 2017 18:25:45 +0100 Subject: [PATCH 4/5] Factorize the common part of literal comparison across the different orders in PrecedenceOrdering::compare, the specialized part being implemented by comparePredicates --- Kernel/KBO.cpp | 94 ++++++++++++-------------------------------- Kernel/KBO.hpp | 3 +- Kernel/KBOForEPR.cpp | 74 ++++++++-------------------------- Kernel/KBOForEPR.hpp | 4 +- Kernel/LPO.cpp | 29 ++++---------- Kernel/LPO.hpp | 3 +- Kernel/Ordering.cpp | 49 +++++++++++++++++++++++ Kernel/Ordering.hpp | 4 ++ 8 files changed, 109 insertions(+), 151 deletions(-) diff --git a/Kernel/KBO.cpp b/Kernel/KBO.cpp index 291e8262ed..16c4d1abbe 100644 --- a/Kernel/KBO.cpp +++ b/Kernel/KBO.cpp @@ -11,8 +11,6 @@ #include "Lib/Environment.hpp" #include "Lib/Comparison.hpp" -#include "Indexing/TermSharing.hpp" - #include "Shell/Options.hpp" #include "Term.hpp" @@ -302,87 +300,47 @@ KBO::~KBO() * of the comparison. * @since 07/05/2008 flight Manchester-Brussels */ -Ordering::Result KBO::compare(Literal* l1, Literal* l2) const +Ordering::Result KBO::comparePredicates(Literal* l1, Literal* l2) const { - CALL("KBO::compare(Literal*...)"); + CALL("KBO::comparePredicates"); ASS(l1->shared()); ASS(l2->shared()); - - if (l1 == l2) { - return EQUAL; - } + ASS(!l1->isEquality()); + ASS(!l2->isEquality()); unsigned p1 = l1->functor(); unsigned p2 = l2->functor(); - if( (l1->isNegative() ^ l2->isNegative()) && (p1==p2) && - l1->weight()==l2->weight() && l1->vars()==l2->vars() && //this line is just optimization, so we don't check whether literals are opposite when they cannot be - l1==env.sharing->tryGetOpposite(l2)) { - return l1->isNegative() ? LESS : GREATER; - } - Result res; - - if (p1 != p2) { - int lev1 = predicateLevel(p1); - int lev2 = predicateLevel(p2); - if (lev1 > lev2) { - res=GREATER; - goto fin; - } - if (lev2 > lev1) { - res=LESS; - goto fin; - } - } - - if(l1->isEquality()) { - ASS(l2->isEquality()); - return compareEqualities(l1, l2); - } - ASS(!l1->isEquality()); - - { - ASS(_state); - State* state=_state; + ASS(_state); + State* state=_state; #if VDEBUG - //this is to make sure _state isn't used while we're using it - _state=0; + //this is to make sure _state isn't used while we're using it + _state=0; #endif - state->init(); - if(p1!=p2) { - TermList* ts; - ts=l1->args(); - while(!ts->isEmpty()) { - state->traverse(*ts,1); - ts=ts->next(); - } - ts=l2->args(); - while(!ts->isEmpty()) { - state->traverse(*ts,-1); - ts=ts->next(); - } - } else { - state->traverse(l1,l2); + state->init(); + if(p1!=p2) { + TermList* ts; + ts=l1->args(); + while(!ts->isEmpty()) { + state->traverse(*ts,1); + ts=ts->next(); + } + ts=l2->args(); + while(!ts->isEmpty()) { + state->traverse(*ts,-1); + ts=ts->next(); } + } else { + state->traverse(l1,l2); + } - res=state->result(l1,l2); + res=state->result(l1,l2); #if VDEBUG - _state=state; + _state=state; #endif - } - -fin: - if(_reverseLCM && (l1->isNegative() || l2->isNegative()) ) { - if(l1->isNegative() && l2->isNegative()) { - res = reverse(res); - } - else { - res = l1->isNegative() ? LESS : GREATER; - } - } return res; -} // KBO::compare() +} // KBO::comparePredicates() Ordering::Result KBO::compare(TermList tl1, TermList tl2) const { diff --git a/Kernel/KBO.hpp b/Kernel/KBO.hpp index 2b77f2bed9..6b90965938 100644 --- a/Kernel/KBO.hpp +++ b/Kernel/KBO.hpp @@ -32,10 +32,11 @@ class KBO KBO(Problem& prb, const Options& opt); virtual ~KBO(); - virtual Result compare(Literal* l1, Literal* l2) const; virtual Result compare(TermList tl1, TermList tl2) const; protected: + virtual Result comparePredicates(Literal* l1, Literal* l2) const; + class State; /** Weight of variables */ int _variableWeight; diff --git a/Kernel/KBOForEPR.cpp b/Kernel/KBOForEPR.cpp index f6e75f0c00..82c5df708c 100644 --- a/Kernel/KBOForEPR.cpp +++ b/Kernel/KBOForEPR.cpp @@ -10,8 +10,6 @@ #include "Lib/Comparison.hpp" #include "Lib/Int.hpp" -#include "Indexing/TermSharing.hpp" - #include "Shell/Property.hpp" #include "Problem.hpp" @@ -40,85 +38,45 @@ KBOForEPR::KBOForEPR(Problem& prb, const Options& opt) } /** - * Compare arguments of literals l1 and l2 and return the result - * of the comparison. + * Compare arguments of non-equality literals l1 and l2 and return the + * result of the comparison. * @since 07/05/2008 flight Manchester-Brussels */ -Ordering::Result KBOForEPR::compare(Literal* l1, Literal* l2) const +Ordering::Result KBOForEPR::comparePredicates(Literal* l1, Literal* l2) const { - CALL("KBOForEPR::compare(Literal*...)"); + CALL("KBOForEPR::comparePredicates(Literal*...)"); ASS(l1->shared()); ASS(l2->shared()); - - if (l1 == l2) { - return EQUAL; - } + ASS(!l1->isEquality()); + ASS(!l2->isEquality()); unsigned p1 = l1->functor(); unsigned p2 = l2->functor(); - if( (l1->isNegative() ^ l2->isNegative()) && (p1==p2) && - l1->weight()==l2->weight() && l1->vars()==l2->vars() && - l1==env.sharing->tryGetOpposite(l2)) { - return l1->isNegative() ? LESS : GREATER; - } - - Result res; - if (p1 != p2) { - Comparison levComp=Int::compare(predicateLevel(p1),predicateLevel(p2)); - if(levComp!=Lib::EQUAL) { - res = fromComparison(levComp); - goto fin; - } - } - - if(l1->isEquality()) { - ASS(l2->isEquality()); - return compareEqualities(l1, l2); - } - ASS(!l1->isEquality()); - ASS(!l2->isEquality()); - if (p1 != p2) { 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 - res = fromComparison(arComp); - goto fin; + return fromComparison(arComp); } Comparison prComp=Int::compare(predicatePrecedence(p1),predicatePrecedence(p2)); ASS_NEQ(prComp, Lib::EQUAL); //precedence ordering is total - res = fromComparison(prComp); - goto fin; + return fromComparison(prComp); } - { - TermList* t1=l1->args(); - TermList* t2=l2->args(); + TermList* t1=l1->args(); + TermList* t2=l2->args(); - ASS(!t1->isEmpty()); - while(*t1==*t2) { - t1=t1->next(); - t2=t2->next(); - ASS(!t1->isEmpty()); //if we're at the end of the term, the literals would have been the same - } - res = compare(*t1, *t2); - goto fin; - } - -fin: - if(_reverseLCM && (l1->isNegative() || l2->isNegative()) ) { - if(l1->isNegative() && l2->isNegative()) { - res = reverse(res); - } - else { - res = l1->isNegative() ? LESS : GREATER; - } + ASS(!t1->isEmpty()); + while(*t1==*t2) { + t1=t1->next(); + t2=t2->next(); + ASS(!t1->isEmpty()); //if we're at the end of the term, the literals would have been the same } - return res; + return compare(*t1, *t2); } Ordering::Result KBOForEPR::compare(TermList tl1, TermList tl2) const diff --git a/Kernel/KBOForEPR.hpp b/Kernel/KBOForEPR.hpp index ac29c28dff..4cbc8dd677 100644 --- a/Kernel/KBOForEPR.hpp +++ b/Kernel/KBOForEPR.hpp @@ -27,8 +27,10 @@ class KBOForEPR KBOForEPR(Problem& prb, const Options& opt); - virtual Result compare(Literal* l1, Literal* l2) const; virtual Result compare(TermList tl1, TermList tl2) const; + +protected: + virtual Result comparePredicates(Literal* l1, Literal* l2) const; }; } diff --git a/Kernel/LPO.cpp b/Kernel/LPO.cpp index 414790a4b9..af2ebeb2f3 100644 --- a/Kernel/LPO.cpp +++ b/Kernel/LPO.cpp @@ -11,8 +11,6 @@ #include "Lib/Environment.hpp" #include "Lib/Comparison.hpp" -#include "Indexing/TermSharing.hpp" - #include "Shell/Options.hpp" #include "Term.hpp" @@ -25,35 +23,22 @@ using namespace Lib; using namespace Shell; /** - * Compare arguments of literals l1 and l2 and return the result - * of the comparison. + * Compare arguments of non-equality literals l1 and l2 and return the + * result of the comparison. */ -Ordering::Result LPO::compare(Literal* l1, Literal *l2) const +Ordering::Result LPO::comparePredicates(Literal* l1, Literal *l2) const { - CALL("LPO::compare(Literal*...)"); + CALL("LPO::comparePredicates"); ASS(l1->shared()); ASS(l2->shared()); - - if (l1 == l2) { - return EQUAL; - } + ASS(!l1->isEquality()); + ASS(!l2->isEquality()); unsigned p1 = l1->functor(); unsigned p2 = l2->functor(); - if( (l1->isNegative() ^ l2->isNegative()) && (p1==p2) && - l1->weight()==l2->weight() && l1->vars()==l2->vars() && //this line is just optimization, so we don't check whether literals are opposite when they cannot be - l1==env.sharing->tryGetOpposite(l2)) { - return l1->isNegative() ? LESS : GREATER; - } - if (p1 == p2) { ASS_EQ(l1->isNegative(), l1->isNegative()) - if(l1->isEquality()) { - ASS(l2->isEquality()); - return compareEqualities(l1, l2); - } - ASS(!l1->isEquality()); // compare arguments in lexicographic order for (unsigned i = 0; i < l1->arity(); i++) { @@ -66,7 +51,7 @@ Ordering::Result LPO::compare(Literal* l1, Literal *l2) const ASS_NEQ(predicatePrecedence(p1), predicatePrecedence(p2)); // precedence should be total return (predicatePrecedence(p1) > predicatePrecedence(p2)) ? GREATER : LESS; -} // LPO::compare() +} // LPO::comparePredicates() Ordering::Result LPO::compare(TermList tl1, TermList tl2) const { diff --git a/Kernel/LPO.hpp b/Kernel/LPO.hpp index 97f8fd0a82..ca18a4cb4c 100644 --- a/Kernel/LPO.hpp +++ b/Kernel/LPO.hpp @@ -32,10 +32,11 @@ class LPO {} virtual ~LPO() {} - virtual Result compare(Literal* l1, Literal* l2) const; virtual Result compare(TermList tl1, TermList tl2) const; protected: + virtual Result comparePredicates(Literal* l1, Literal* l2) const; + Result cLMA(Term* s, Term* t, TermList* sl, TermList* tl, unsigned arity) const; Result cMA(Term* t, TermList* tl, unsigned arity) const; Result cAA(Term* s, Term* t, TermList* sl, TermList* tl, unsigned arity1, unsigned arity2) const; diff --git a/Kernel/Ordering.cpp b/Kernel/Ordering.cpp index 9fafb8b53e..dc708622e6 100644 --- a/Kernel/Ordering.cpp +++ b/Kernel/Ordering.cpp @@ -7,6 +7,8 @@ #include "Forwards.hpp" +#include "Indexing/TermSharing.hpp" + #include "Lib/Environment.hpp" #include "Lib/Exception.hpp" #include "Lib/List.hpp" @@ -214,6 +216,53 @@ Ordering::Result Ordering::getEqualityArgumentOrder(Literal* eq) const // PrecedenceOrdering class ////////////////////////////////////////////////// +Ordering::Result PrecedenceOrdering::compare(Literal* l1, Literal* l2) const +{ + CALL("PrecedenceOrdering::compare(Literal*...)"); + ASS(l1->shared()); + ASS(l2->shared()); + + if (l1 == l2) { + return EQUAL; + } + + unsigned p1 = l1->functor(); + unsigned p2 = l2->functor(); + + if( (l1->isNegative() ^ l2->isNegative()) && (p1==p2) && + l1->weight()==l2->weight() && l1->vars()==l2->vars() && //this line is just optimization, so we don't check whether literals are opposite when they cannot be + l1==env.sharing->tryGetOpposite(l2)) { + return l1->isNegative() ? LESS : GREATER; + } + + Result res; + + if (p1 != p2) { + Comparison levComp=Int::compare(predicateLevel(p1),predicateLevel(p2)); + if(levComp!=Lib::EQUAL) { + return fromComparison(levComp); + } + } + + if(l1->isEquality()) { + ASS(l2->isEquality()); + return compareEqualities(l1, l2); + } + ASS(!l1->isEquality()); + + res = comparePredicates(l1, l2); + + if(_reverseLCM && (l1->isNegative() || l2->isNegative()) ) { + if(l1->isNegative() && l2->isNegative()) { + res = reverse(res); + } + else { + res = l1->isNegative() ? LESS : GREATER; + } + } + return res; +} // PrecedenceOrdering::compare() + /** * Return the predicate level. If @b pred is less than or equal to * @b _predicates, then the value is taken from the array _predicateLevels, diff --git a/Kernel/Ordering.hpp b/Kernel/Ordering.hpp index fd1ca74e39..4fa86c080a 100644 --- a/Kernel/Ordering.hpp +++ b/Kernel/Ordering.hpp @@ -144,9 +144,13 @@ class PrecedenceOrdering : public Ordering { public: + virtual Result compare(Literal* l1,Literal* l2) const; virtual Comparison compareFunctors(unsigned fun1, unsigned fun2) const; protected: + // l1 and l2 are not equalities and have the same predicate + virtual Result comparePredicates(Literal* l1,Literal* l2) const = 0; + PrecedenceOrdering(Problem& prb, const Options& opt); Result compareFunctionPrecedences(unsigned fun1, unsigned fun2) const; From 1a97214e410621badbd80d9a948e89baf1113200 Mon Sep 17 00:00:00 2001 From: Simon Robillard Date: Wed, 8 Nov 2017 18:28:52 +0100 Subject: [PATCH 5/5] small optimization in PrecedenceOrdering::compare --- Kernel/Ordering.cpp | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/Kernel/Ordering.cpp b/Kernel/Ordering.cpp index dc708622e6..a9d27c855a 100644 --- a/Kernel/Ordering.cpp +++ b/Kernel/Ordering.cpp @@ -235,8 +235,6 @@ Ordering::Result PrecedenceOrdering::compare(Literal* l1, Literal* l2) const return l1->isNegative() ? LESS : GREATER; } - Result res; - if (p1 != p2) { Comparison levComp=Int::compare(predicateLevel(p1),predicateLevel(p2)); if(levComp!=Lib::EQUAL) { @@ -250,17 +248,15 @@ Ordering::Result PrecedenceOrdering::compare(Literal* l1, Literal* l2) const } ASS(!l1->isEquality()); - res = comparePredicates(l1, l2); - if(_reverseLCM && (l1->isNegative() || l2->isNegative()) ) { if(l1->isNegative() && l2->isNegative()) { - res = reverse(res); + return reverse(comparePredicates(l1, l2)); } else { - res = l1->isNegative() ? LESS : GREATER; + return l1->isNegative() ? LESS : GREATER; } } - return res; + return comparePredicates(l1, l2); } // PrecedenceOrdering::compare() /**