33 PredFactory getPredFactory() {
34 PredFactory factory(
"Term ordering");
36 nameFactoryRegister<LexComparator>(factory);
37 nameFactoryRegister<ReverseLexComparator>(factory);
46 pred->setVarCount(varCount);
51 ASSERT(a != 0 || varCount == 0);
52 ASSERT(b != 0 || varCount == 0);
54 for (
size_t var = 0; var < varCount; ++var) {
72 ASSERT(a != 0 || varCount == 0);
73 ASSERT(b != 0 || varCount == 0);
78 ASSERT(a != 0 || varCount == 0);
79 ASSERT(b != 0 || varCount == 0);
81 for (
size_t var = 0; var < varCount; ++var)
auto_ptr< AbstractProduct > createWithPrefix(const NameFactory< AbstractProduct > &factory, const string &prefix)
Creates the unique product that has the indicated prefix, or create the actual product that has name ...
bool equals(const Exponent *a, const Exponent *b, size_t varCount)
Returns whether the entries of a are equal to the entries of b.
int lexCompare(const Exponent *a, const Exponent *b, size_t varCount)
Indicates how a relates to b according to the lexicographic term order where .
auto_ptr< TermPredicate > createTermPredicate(const string &prefix, size_t varCount)
Returns the predicate whose name has the given prefix.
int reverseLexCompare(const Exponent *a, const Exponent *b, size_t varCount)
Indicates how a relates to b according to the reverse lexicographic term order where .
EqualsPredicate(size_t varCount=0)
static const char * staticGetName()
LexComparator(size_t varCount=0)
A NameFactory takes a name and then creates an instance of a class that has been previously registere...
ReverseLexComparator(size_t varCount=0)
static const char * staticGetName()
ReverseSingleDegreeComparator(size_t var, size_t varCount=0)
SingleDegreeComparator(size_t var, size_t varCount=0)
TermPredicate(size_t varCount=0)
Term represents a product of variables which does not include a coefficient.
size_t getVarCount() const