Fix snapshot code
[model-checker.git] / scfence / inferlist.h
1 #ifndef _INFERLIST_H
2 #define _INFERLIST_H
3
4 #include "fence_common.h"
5 #include "patch.h"
6 #include "inference.h"
7
8 class Patch;
9 class PatchUnit;
10 class Inference;
11
12 /** This class represents that the list of inferences that can fix the problem
13  */
14 class InferenceList {
15         private:
16         ModelList<Inference*> *list;
17
18         public:
19         InferenceList();
20         int getSize();  
21         Inference* back();
22
23         /** We should not call this function too often because we want a nicer
24          *  abstraction of the list of inferences. So far, it will only be called in
25          *  the functions in InferenceSet */
26         ModelList<Inference*>* getList();       
27         void push_back(Inference *infer);
28         void pop_front();
29         void pop_back();
30         bool applyPatch(Inference *curInfer, Inference *newInfer, Patch *patch);
31
32         void applyPatch(Inference *curInfer, Patch* patch);
33
34         void applyPatch(Inference *curInfer, SnapVector<Patch*> *patches);
35         
36         /** Append another list to this list */
37         bool append(InferenceList *inferList);
38
39         /** Only choose the weakest existing candidates & they must be stronger than the
40          * current inference */
41         void pruneCandidates(Inference *curInfer);
42         
43         void clearAll();
44
45         void clearList();
46
47         static void clearAll(ModelList<Inference*> *l);
48
49         static void clearAll(InferenceList *inferList);
50         
51         static void print(ModelList<Inference*> *inferList, const char *msg);
52
53         static void print(InferenceList *inferList, const char *msg);
54
55         void print();
56
57         void print(const char *msg);
58
59         MEMALLOC
60
61 };
62
63
64 #endif