X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=scfence%2Finferlist.h;fp=scfence%2Finferlist.h;h=bc3476ac33185827727d62a9be530505b769566a;hp=0000000000000000000000000000000000000000;hb=a65e234b607444355eb6e34097ee55ba93d4c01b;hpb=7c510878f9679da10de79c289df402356b092396

diff --git a/scfence/inferlist.h b/scfence/inferlist.h
new file mode 100644
index 0000000..bc3476a
--- /dev/null
+++ b/scfence/inferlist.h
@@ -0,0 +1,64 @@
+#ifndef _INFERLIST_H
+#define _INFERLIST_H
+
+#include "fence_common.h"
+#include "patch.h"
+#include "inference.h"
+
+class Patch;
+class PatchUnit;
+class Inference;
+
+/** This class represents that the list of inferences that can fix the problem
+ */
+class InferenceList {
+	private:
+	ModelList<Inference*> *list;
+
+	public:
+	InferenceList();
+	int getSize();	
+	Inference* back();
+
+	/** We should not call this function too often because we want a nicer
+	 *  abstraction of the list of inferences. So far, it will only be called in
+	 *  the functions in InferenceSet */
+	ModelList<Inference*>* getList();	
+	void push_back(Inference *infer);
+	void pop_front();
+	void pop_back();
+	bool applyPatch(Inference *curInfer, Inference *newInfer, Patch *patch);
+
+	void applyPatch(Inference *curInfer, Patch* patch);
+
+	void applyPatch(Inference *curInfer, SnapVector<Patch*> *patches);
+	
+	/** Append another list to this list */
+	bool append(InferenceList *inferList);
+
+	/** Only choose the weakest existing candidates & they must be stronger than the
+	 * current inference */
+	void pruneCandidates(Inference *curInfer);
+	
+	void clearAll();
+
+	void clearList();
+
+	static void clearAll(ModelList<Inference*> *l);
+
+	static void clearAll(InferenceList *inferList);
+	
+	static void print(ModelList<Inference*> *inferList, const char *msg);
+
+	static void print(InferenceList *inferList, const char *msg);
+
+	void print();
+
+	void print(const char *msg);
+
+	MEMALLOC
+
+};
+
+
+#endif