OSHL/printByType.cpp at master · theoremprover-museum/OSHL · 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
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
/*
 *      Author: Hao Xu
 */
#include "defs.h"
#include "expansibleList.h"
#include "term.h"
#include "trie.h"
#include "printByType.h"
#include "symbols.h"

void printByType(Version version) {
    printf("%lX", version);
}
void printByType(ClauseTree::Node *node) {
    char buf[STRING_BUF_SIZE];
    if(node->literal == NULL) {
        printf("ClauseTree::Node(leaf = %d)", node->leaf);

    } else {
    node->literal->toString(buf, symtable);
    printf("ClauseTree::Node(literal = %s, sign = %d, leaf = %d)", buf, node->sign, node->leaf);
    }
}
void printByType(ClauseTree *node) {
    char buf[STRING_BUF_SIZE];
    node->toString(buf, symtable);
    printf("ClauseTree: %s", buf);
}
void printByType(TermInstances *ti) {
    printf("%p", ti);
}
void printByType(TermInstanceIterator *tii) {
    printf("%p", tii);
}
void printByType(LazyList<Trie, Sub> *ll) {
    printf("%p", ll);
}
void printByType(Term *term) {
    char buf[STRING_BUF_SIZE];
    term->toString(buf, symtable);
    printf("%s | ", buf);
    if(term->inp != NULL) {
    	term->inp->toString(buf, symtable);
    	printf("%s", buf);
    } else {
    	printf("<<uncompiled>>");
    }

}
void printByType(Sub *sub) {
	if(sub == NULL) {
		printf("<null>");
	} else {
	char buf[STRING_BUF_SIZE];
	while(sub!=NULL && sub->val!=NULL) {
	    sub->val->toString(buf, symtable);
		printf("?%lX(%s) = %s:%ld, ", (long) sub->key - VAR_ID_OFFSET, symtable[sub->key], buf, (long) sub->version);
	    sub = sub->prev;
	}
	}
    printf("\n");

}
void printByType(PMVMInstruction *fs) {
        printf("FlattermSymbol(symbol = %lX, subtermSize = %d, subterm = %p)", fs->symbol, fs->subtermSize, fs->subterm);

}
void printByType(Trie *trie) {
        printf("%p", trie);

}

void printByType(TermCache *termCacheNode) {
	printf("%p", termCacheNode);
}

void printByType(TermCacheType *termCacheNode) {
	printf("%p", termCacheNode);
}

void printByType(LinkedList<Term *>::Node *node) {
	printf("%p", node);
}

void printByType(unsigned int i) {
	printf("%u", i);
}
void printByType(int i) {
	printf("%d", i);
}
void printByType(CoroutineState *thread) {
	if(thread == NULL) {
		printf("CoroutineState(null)");
	}else{
		printf("CoroutineState(%p)(", thread);
		for(int i =0;i<LEVEL_OF_NESTING;i++) {
			printf("ar_bottom_%d = %p",i,thread->arBottoms[i]);
			printf(", ");
		}
		printf("delFlag = %d, ", thread->delFlag);
		printf("threadId = %d, ", thread->threadId);
		printf("anchor = %d, ", thread->anchor);
		printf("prev = %p,", thread->branchPointer);
		printf("super = %p", thread->super);
		//assert(thread->super!=NULL);
		printf(")");

	}
}
/*void printByType(CoroutineDataDependency *thread) {
	if(thread == NULL) {
		printf("CoroutineDataDependency(null)");
	}else{
		printf("CoroutineDataDependency()");
	}
}*/