TPTP4X/Randomize.c at master · TPTPWorld/TPTP4X · GitHub

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
#include <stdio.h>
#include <assert.h>
#include <ctype.h>
#include <string.h>
#include <stdlib.h>
#include "DataTypes.h"
#include "Utilities.h"
#include "Examine.h"
#include "List.h"
#include "PrintTSTP.h"
#include "tptp4X.h"
//-------------------------------------------------------------------------------------------------
void RandomizeFormulaeBelowIncludes(LISTNODE * Head) {

    LISTNODE * FirstLogical;

    FirstLogical = Head;
    while (*FirstLogical != NULL &&
!LogicalAnnotatedFormula((*FirstLogical)->AnnotatedFormula)) {
        FirstLogical = &((*FirstLogical)->Next);
    }

    RandomizeListOfAnnotatedFormulae(FirstLogical,1);
}
//-------------------------------------------------------------------------------------------------
void RandomizeCommutativeFormulae(LISTNODE * Head) {

    LISTNODE * Target;
    LISTNODE Randomized;
    LISTNODE * AddHere;

    Randomized = NULL;
    AddHere = &Randomized;
//----Move all includes to front
    Target = Head;
    while (*Target != NULL) {
        if (
(*Target)->AnnotatedFormula->Syntax == include ||
( LogicalAnnotatedFormulaWithRole((*Target)->AnnotatedFormula,type) ||
  LogicalAnnotatedFormulaWithRole((*Target)->AnnotatedFormula,definition))) {
            *AddHere = *Target;
            *Target = (*Target)->Next;
            (*AddHere)->Next = NULL;
            AddHere = &((*AddHere)->Next);
        } else {
            Target = &((*Target)->Next);
        }
    }

//----Randomize the rest
    RandomizeListOfAnnotatedFormulae(Head,1);
    *AddHere = *Head;
    *Head = Randomized;
}
//-------------------------------------------------------------------------------------------------