Skip to content

Commit

Permalink
Merge pull request #598 from vprover/michael-remove-sort
Browse files Browse the repository at this point in the history 
remove our own sort implementation
  • Loading branch information
@quickbeam123
quickbeam123 authored Sep 6, 2024
2 parents a2a69bf + 58eefb8 commit 155f4b2
Show file tree
Hide file tree
Showing 6 changed files with 28 additions and 303 deletions.
9 changes: 4 additions & 5 deletions FMB/FiniteModelBuilder.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,6 @@
#include "Lib/List.hpp"
#include "Lib/Stack.hpp"
#include "Lib/System.hpp"
#include "Lib/Sort.hpp"
#include "Lib/Random.hpp"
#include "Lib/DHSet.hpp"
#include "Lib/ArrayMap.hpp"
Expand Down Expand Up @@ -298,11 +297,11 @@ bool FiniteModelBuilder::reset(){
// Compare function symbols by their usage in the problem
struct FMBSymmetryFunctionComparator
{
static Comparison compare(unsigned f1, unsigned f2)
static bool compare(unsigned f1, unsigned f2)
{
unsigned c1 = env.signature->getFunction(f1)->usageCnt();
unsigned c2 = env.signature->getFunction(f2)->usageCnt();
return Int::compare(c2,c1);
return c2 < c1;
}
};

Expand Down Expand Up @@ -764,8 +763,8 @@ void FiniteModelBuilder::init()
for(unsigned s=0;s<_sortedSignature->sorts;s++){
Stack<unsigned> sortedConstants = _sortedSignature->sortedConstants[s];
Stack<unsigned> sortedFunctions = _sortedSignature->sortedFunctions[s];
sort<FMBSymmetryFunctionComparator>(sortedConstants.begin(),sortedConstants.end());
sort<FMBSymmetryFunctionComparator>(sortedFunctions.begin(),sortedFunctions.end());
sort(sortedConstants.begin(),sortedConstants.end(), FMBSymmetryFunctionComparator::compare);
sort(sortedFunctions.begin(),sortedFunctions.end(), FMBSymmetryFunctionComparator::compare);
}
}
}
Expand Down
14 changes: 4 additions & 10 deletions Kernel/InferenceStore.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@
#include "Lib/Stack.hpp"
#include "Lib/StringUtils.hpp"
#include "Lib/ScopedPtr.hpp"
#include "Lib/Sort.hpp"

#include "Shell/LaTeX.hpp"
#include "Shell/Options.hpp"
Expand Down Expand Up @@ -184,14 +183,6 @@ std::string getQuantifiedStr(Unit* u, List<unsigned>* nonQuantified=0)
return getQuantifiedStr(vars, res, t_map);
}

struct UnitNumberComparator
{
static Comparison compare(Unit* u1, Unit* u2)
{
return Int::compare(u1->number(), u2->number());
}
};

struct InferenceStore::ProofPrinter
{
ProofPrinter(ostream& out, InferenceStore* is)
Expand Down Expand Up @@ -290,7 +281,10 @@ struct InferenceStore::ProofPrinter
void printDelayed()
{
// Sort
sort<UnitNumberComparator>(delayed.begin(),delayed.end());
sort(
delayed.begin(), delayed.end(),
[](Unit *u1, Unit *u2) -> bool { return u1->number() < u2->number(); }
);

// Print
for(unsigned i=0;i<delayed.size();i++){
Expand Down
5 changes: 4 additions & 1 deletion Lib/SharedSet.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -360,7 +360,10 @@ class SharedSet {
}
}
if(!sorted) {
sort<DefaultComparator>(is.begin(), is.end());
std::sort(
is.begin(), is.end(),
[](const T &l, const T &r) -> bool { return DefaultComparator::compare(l, r) == LESS; }
);
unique = false; //maybe they are unique, we just need to check
}
if(!unique) {
Expand Down
282 changes: 2 additions & 280 deletions Lib/Sort.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,13 +17,11 @@


#ifndef __Sort__
# define __Sort__
#define __Sort__

#include "Comparison.hpp"
#include "Debug/Assertion.hpp"

#include "Allocator.hpp"
#include "DArray.hpp"

namespace Lib {

/** A type level predicate that tells whether there is a function `Result T::compare(T const&) const;` for some result type Result. o
Expand Down Expand Up @@ -70,282 +68,6 @@ struct DefaultComparator
}
};

template <class Comparator, typename C>
void sort(C* first, C* afterLast)
{
//modified sorting code, that was originally in Resolution::Tautology::sort

C* arr=first;
size_t size=afterLast-first;
if(size<=1) {
//nothing to sort
return;
}

// array behaves as a stack of calls to quicksort
static DArray<size_t> ft(32);

size_t from = 0;
size_t to=size-1;
ft.ensure(to);

size_t p = 0; // pointer to the next element in ft
for (;;) {
ASS(from<size && to<size); //checking for underflows
// invariant: from < to
size_t m = from + Random::getInteger(to-from+1);
C mid = arr[m];
size_t l = from;
size_t r = to;
while (l < m) {
switch (Comparator::compare(arr[l],mid))
{
case EQUAL:
case LESS:
l++;
break;
case GREATER:
if (m == r) {
arr[m] = arr[l];
arr[l] = arr[m-1];
arr[m-1] = mid;
m--;
r--;
}
else {
ASS(m < r);
C aux = arr[l];
arr[l] = arr[r];
arr[r] = aux;
r--;
}
break;
}
}
// l == m
// now literals in lits[from ... m-1] are smaller than lits[m]
// and literals in lits[r+1 ... to] are greater than lits[m]
while (m < r) {
switch (Comparator::compare(mid,arr[m+1]))
{
case LESS:
{
C aux = arr[r];
arr[r] = arr[m+1];
arr[m+1] = aux;
r--;
}
break;
case EQUAL:
case GREATER:
arr[m] = arr[m+1];
arr[m+1] = mid;
m++;
}
}
// now literals in lits[from ... m-1] are smaller than lits[m]
// and all literals in lits[m+1 ... to] are greater than lits[m]
if (m+1 < to) {
ft[p++] = m+1;
ft[p++] = to;
}

to = m-1;
if (m!=0 && from < to) {
continue;
}
if (p != 0) {
p -= 2;
ASS(p >= 0);
from = ft[p];
to = ft[p+1];
continue;
}
return;
}
}

/**
* A template class to sort data. The type ToCompare is the
* type of elements to sort. The type Comparator is the class that
* contains a function bool lessThan(ToCompare, ToCompare).
* A typical work with this class is as follows:
*
* <ol>
* <li>a comparator c and an element s of the class Sort are created;</li>
* <li>elements of the class ToCompare are added one by one;</li>
* <li>s.sort() is called</li>
* <li>the resulting sorted collection is read.</li>
* </ol>
* @since 16/07/2003 flight Moscow-London, changed from a
* previous one-type version.
* @since 03/04/2004 Torrevieja, changed to use a comparator instead of
* a static function
*/
template <typename ToCompare, class Comparator>
class Sort
{
public:
/**
* Initialize the sort element.
*
* @param length the number of elements to sort
* @param comparator object used for comparison
*/
Sort (int length,Comparator& comparator)
:
_size(length),
_length(0),
_comparator(comparator)
{
void* mem = ALLOC_KNOWN(length*sizeof(ToCompare),"Sort<>");
_elems = array_new<ToCompare>(mem, length);
}

inline ~Sort ()
{
array_delete(_elems,_size);
DEALLOC_KNOWN(_elems,_size*sizeof(ToCompare),"Sort<>");
}

/**
* Return the length (the number of elements to sort)
*/
inline int length () const { return _length; }

/**
* Return the nth element, used to retrieve sorted elements
*/
inline ToCompare operator [] (int n) const
{
ASS(n < _length);
return _elems[n];
} // Sort::operator []

/**
* Add an element to sort.
*
* @param elem the element.
*/
inline void add (ToCompare elem)
{
ASS(_length < _size);

_elems[_length++] = elem;
} // Sort::add

/**
* Sort elements.
*/
inline void sort ()
{
sort (0,_length-1);
}

/**
* Check membership in the sorted list. Membership is checked using
* == for equality.
*
* @return true if elem is the member of Sort
* @since 17/07/2003 Manchester, changed to the new two-argument Sort class
*/
inline bool member (const ToCompare elem) const {
return member (elem,0,_length-1);
}

protected: // structure
/** array of elements */
ToCompare* _elems;
/** capacity */
int _size;
/** the number of elements */
int _length;
/** object used to compare elements */
Comparator& _comparator;

/**
* Quicksort elements between, and including indexes p and r, was taken
* from the Rivest et al. book - never use this book for practical
* algorithms :)
* @since 16/04/2006 Bellevue, improved: the algorithm sometimes
* compared elements with themselves
* @since 27/06/2008 Manchester, replaced since the old one was showing
* quadratic behaviour
*/
void sort(int p,int r)
{
ASS(r < _length);

if (p >= r) {
return;
}
int m = (p+r)/2;
int i = p;
int j = r;
ToCompare a = _elems[m];
while (i < m) {
ToCompare b = _elems[i];
if (! _comparator.lessThan(a,b)) { // a[i] <= a[m]
i++;
continue;
}
if (m < j) {
_elems[i] = _elems[j];
_elems[j] = b;
j--;
continue;
}
_elems[m] = b;
_elems[i] = _elems[m-1];
m--;
j--;
}
while (m < j) {
ToCompare b = _elems[j];
if (! _comparator.lessThan(b,a)) { // a[m] <= a[j]
j--;
continue;
}
_elems[m] = b;
_elems[j] = _elems[m+1];
m++;
}
_elems[m] = a;
sort(p,m-1);
sort(m+1,r);
} // sort

/**
* Check membership in the sorted list between the indexes fst
* and snd. Membership is checked using == for equality. The function
* works correctly only if lessThan is a total order.
*
* @return true if elem is the member of Sort[fst] ... Sort[snd]
* @since 17/07/2003 Manchester, changed to the new two-argument Sort class
*/
bool member (const ToCompare elem, int fst, int lst) const
{
for (;;) {
if (fst > lst) {
return false;
}

int mid = (fst + lst) / 2;

if (_elems[mid] == elem) {
return true;
}

if (_comparator.lessThan(_elems[mid],elem)) {
lst = mid-1;
}
else { // _elems[mid] > c
fst = mid+1;
}
}
} // Sort::member
}; // class Sort

} // namespace Lib

#endif
Expand Down
Loading

0 comments on commit 155f4b2

Please sign in to comment.