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;