1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
/*
* This file is part of the source code of the software program
* Vampire. It is protected by applicable
* copyright laws.
*
* This source code is distributed under the licence found here
* https://vprover.github.io/license.html
* and in the source directory
*/
/**
* @file Shuffling.hpp
* Defines class Shuffling implementing the shuffling of the input.
* @since 9/6/2021 Prague
*/
#ifndef __Shuffling__
#define __Shuffling__
#include "Forwards.hpp"
#include "Kernel/Term.hpp"
#include "Lib/List.hpp"
#include "Lib/Coproduct.hpp"
#include "Kernel/Unit.hpp"
#include "Kernel/Term.hpp"
#include <algorithm>
namespace Shell {
using namespace Lib;
using namespace Kernel;
/**
* Class implementing shuffling-related procedures.
* @since 09/06/2021 Prague
*/
class Shuffling
{
private:
typedef Coproduct<Formula*, Literal*, TermList> Shufflable;
static void shuffleIter(Shufflable sh);
public:
static void polarityFlip(Problem&);
static void shuffle(Problem&);
static void shuffle(UnitList*&);
// shuffling should not require allocating new memory, so all the objects are modified "in place"
static void shuffle(Unit*); // shuffle a unit; just dispatches to either shuffle(Clause*) or shuffle(Formula*)
static void shuffle(Clause*); // shuffling a clause; it assumes literals are shared (i.e. nothing "special" in them anyway) so it does not touch those
static void shuffle(Formula* f) { shuffleIter(Shufflable(f)); } // shuffling a formula; will try to descend also to the term level, to shuffle around commutative operators and formulas inside terms (if applicable)
static void shuffle(Literal* l) { shuffleIter(Shufflable(l)); }
static void shuffle(TermList tl) { shuffleIter(Shufflable(tl)); }
template<typename Arrayish>
// Implements Fisher–Yates shuffling (each permutation equally likely)
static void shuffleArray(Arrayish& a, unsigned len) {
for(unsigned i=0;i<len;i++){
unsigned j = Random::getInteger(len-i)+i;
std::swap(a[i],a[j]);
}
}
template<typename T>
static void shuffleArray(T* ptr, unsigned len) { shuffleArray<T*&>(ptr, len); }
// get a new list by shuffling the original
// we leak the old one
template<typename T>
static void shuffleList(List<T>*& list) {
unsigned len = List<T>::length(list);
if (len <= 1) {
return;
}
DArray<List<T>*> aux(len);
unsigned idx = 0;
List<T>* els = list;
while (els != nullptr) {
aux[idx++] = els;
els = els->tail();
}
shuffleArray(aux,len);
// create the new list
List<T>* res = nullptr;
for(idx = 0; idx < len; idx++) {
res = List<T>::cons(aux[idx]->head(),res);
}
// List<T>::destroy(list);
list = res;
}
// list2 is assumed to be of the same length as list1;
// get two new lists by shuffling the originals and leaking the old ones
// they get shuffled "in sync"
template<typename T, typename S>
static void shuffleTwoList(List<T>*& list1, List<S>*& list2) {
unsigned len = List<T>::length(list1);
if (len <= 1) {
return;
}
DArray<std::pair<List<T>*,List<S>*>> aux(len);
unsigned idx = 0;
List<T>* els1 = list1;
List<S>* els2 = list2;
while (els1 != nullptr) {
ASS_NEQ(els2,0);
aux[idx++] = std::make_pair(els1,els2);
els1 = els1->tail();
els2 = els2->tail();
}
ASS_EQ(els2,0);
shuffleArray(aux,len);
// create the new lists
List<T>* res1 = nullptr;
List<S>* res2 = nullptr;
for(idx = 0; idx < len; idx++) {
res1 = List<T>::cons(aux[idx].first->head(),res1);
res2 = List<S>::cons(aux[idx].second->head(),res2);
}
// List<T>::destroy(list1);
// List<S>::destroy(list2);
list1 = res1;
list2 = res2;
}
}; // class Shuffling
}
#endif