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

diff --git a/scfence/inferlist.cc b/scfence/inferlist.cc
new file mode 100644
index 0000000..5cb6326
--- /dev/null
+++ b/scfence/inferlist.cc
@@ -0,0 +1,207 @@
+#include "inferlist.h"
+
+InferenceList::InferenceList() {
+	list = new ModelList<Inference*>;
+}
+
+int InferenceList::getSize() {
+	return list->size();
+}
+
+void InferenceList::pop_back() {
+	list->pop_back();
+}
+
+Inference* InferenceList::back() {
+	return list->back();
+}
+
+void InferenceList::push_back(Inference *infer) {
+	list->push_back(infer);
+}
+
+void InferenceList::pop_front() {
+	list->pop_front();
+}
+
+/** 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*>* InferenceList::getList() {
+	return list;
+}
+
+bool InferenceList::applyPatch(Inference *curInfer, Inference *newInfer, Patch *patch) {
+	bool canUpdate = true,
+		hasUpdated = false,
+		updateState = false;
+	for (int i = 0; i < patch->getSize(); i++) {
+		canUpdate = true;
+		hasUpdated = false;
+		PatchUnit *unit = patch->get(i);
+		newInfer->strengthen(unit->getAct(), unit->getMO(), canUpdate, hasUpdated);
+		if (!canUpdate) {
+			// This is not a feasible patch, bail
+			break;
+		} else if (hasUpdated) {
+			updateState = true;
+		}
+	}
+	if (updateState) {
+		return true;
+	} else {
+		return false;
+	}
+}
+
+void InferenceList::applyPatch(Inference *curInfer, Patch* patch) {
+	if (list->empty()) {
+		Inference *newInfer = new Inference(curInfer);
+		if (!applyPatch(curInfer, newInfer, patch)) {
+			delete newInfer;
+		} else {
+			list->push_back(newInfer);
+		}
+	} else {
+		ModelList<Inference*> *newList = new ModelList<Inference*>;
+		for (ModelList<Inference*>::iterator it = list->begin(); it !=
+			list->end(); it++) {
+			Inference *oldInfer = *it;
+			Inference *newInfer = new Inference(oldInfer);
+			if (!applyPatch(curInfer, newInfer, patch)) {
+				delete newInfer;
+			} else {
+				newList->push_back(newInfer);
+			}
+		}
+		// Clean the old list
+		for (ModelList<Inference*>::iterator it = list->begin(); it !=
+			list->end(); it++) {
+			delete *it;
+		}
+		delete list;
+		list = newList;
+	}	
+}
+
+void InferenceList::applyPatch(Inference *curInfer, SnapVector<Patch*> *patches) {
+	if (list->empty()) {
+		for (unsigned i = 0; i < patches->size(); i++) {
+			Inference *newInfer = new Inference(curInfer);
+			Patch *patch = (*patches)[i];
+			if (!applyPatch(curInfer, newInfer, patch)) {
+				delete newInfer;
+			} else {
+				list->push_back(newInfer);
+			}
+		}
+	} else {
+		ModelList<Inference*> *newList = new ModelList<Inference*>;
+		for (ModelList<Inference*>::iterator it = list->begin(); it !=
+			list->end(); it++) {
+			Inference *oldInfer = *it;
+			for (unsigned i = 0; i < patches->size(); i++) {
+				Inference *newInfer = new Inference(oldInfer);
+				Patch *patch = (*patches)[i];
+				if (!applyPatch(curInfer, newInfer, patch)) {
+					delete newInfer;
+				} else {
+					newList->push_back(newInfer);
+				}
+			}
+		}
+		// Clean the old list
+		for (ModelList<Inference*>::iterator it = list->begin(); it !=
+			list->end(); it++) {
+			delete *it;
+		}
+		delete list;
+		list = newList;
+	}
+}
+
+/** Append another list to this list */
+bool InferenceList::append(InferenceList *inferList) {
+	if (!inferList)
+		return false;
+	ModelList<Inference*> *l = inferList->list;
+	list->insert(list->end(), l->begin(), l->end());
+	return true;
+}
+
+/** Only choose the weakest existing candidates & they must be stronger than the
+ * current inference */
+void InferenceList::pruneCandidates(Inference *curInfer) {
+	ModelList<Inference*> *newCandidates = new ModelList<Inference*>(),
+		*candidates = list;
+
+	ModelList<Inference*>::iterator it1, it2;
+	int compVal;
+	for (it1 = candidates->begin(); it1 != candidates->end(); it1++) {
+		Inference *cand = *it1;
+		compVal = cand->compareTo(curInfer);
+		if (compVal == 0) {
+			// If as strong as curInfer, bail
+			delete cand;
+			continue;
+		}
+		// Check if the cand is any stronger than those in the newCandidates
+		for (it2 = newCandidates->begin(); it2 != newCandidates->end(); it2++) {
+			Inference *addedInfer = *it2;
+			compVal = addedInfer->compareTo(cand);
+			if (compVal == 0 || compVal == 1) { // Added inference is stronger
+				delete addedInfer;
+				it2 = newCandidates->erase(it2);
+				it2--;
+			}
+		}
+		// Now push the cand to the list
+		newCandidates->push_back(cand);
+	}
+	delete candidates;
+	list = newCandidates;
+}
+
+void InferenceList::clearAll() {
+	clearAll(list);
+}
+
+void InferenceList::clearList() {
+	delete list;
+}
+
+void InferenceList::clearAll(ModelList<Inference*> *l) {
+	for (ModelList<Inference*>::iterator it = l->begin(); it !=
+		l->end(); it++) {
+		Inference *infer = *it;
+		delete infer;
+	}
+	delete l;
+}
+
+void InferenceList::clearAll(InferenceList *inferList) {
+	clearAll(inferList->list);
+}
+
+void InferenceList::print(InferenceList *inferList, const char *msg) {
+	print(inferList->getList(), msg);
+}
+
+void InferenceList::print(ModelList<Inference*> *inferList, const char *msg) {
+	for (ModelList<Inference*>::iterator it = inferList->begin(); it !=
+		inferList->end(); it++) {
+		int idx = distance(inferList->begin(), it);
+		Inference *infer = *it;
+		model_print("%s %d:\n", msg, idx);
+		infer->print();
+		model_print("\n");
+	}
+}
+
+void InferenceList::print() {
+	print(list, "Inference");
+}
+
+void InferenceList::print(const char *msg) {
+	print(list, msg);
+}