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

diff --git a/include/wildcard.h b/include/wildcard.h
new file mode 100644
index 0000000..2a18c4c
--- /dev/null
+++ b/include/wildcard.h
@@ -0,0 +1,36 @@
+#ifndef _WILDCARD_H
+#define _WILDCARD_H
+#include "memoryorder.h"
+
+#define MAX_WILDCARD_NUM 50
+
+#define memory_order_normal ((memory_order) (0x2000))
+
+#define memory_order_wildcard(x) ((memory_order) (0x1000+x))
+
+#define wildcard(x) ((memory_order) (0x1000+x))
+#define get_wildcard_id(x) ((int) (x-0x1000))
+#define get_wildcard_id_zero(x) ((get_wildcard_id(x)) > 0 ? get_wildcard_id(x) : 0)
+
+#define INIT_WILDCARD_NUM 20
+#define WILDCARD_NONEXIST (memory_order) -1
+#define INFERENCE_INCOMPARABLE(x) (!(-1 <= (x) <= 1))
+
+#define is_wildcard(x) (!(x >= memory_order_relaxed && x <= memory_order_seq_cst) && x != memory_order_normal)
+#define is_normal_mo_infer(x) ((x >= memory_order_relaxed && x <= memory_order_seq_cst) || x == WILDCARD_NONEXIST || x == memory_order_normal)
+#define is_normal_mo(x) ((x >= memory_order_relaxed && x <= memory_order_seq_cst) || x == memory_order_normal)
+
+#define assert_infer(x) for (int i = 0; i <= wildcardNum; i++)\
+	ASSERT(is_normal_mo_infer((x[i])));
+
+#define assert_infers(x) for (ModelList<memory_order *>::iterator iter =\
+	(x)->begin(); iter != (x)->end(); iter++)\
+	assert_infer((*iter));
+
+#define relaxed memory_order_relaxed
+#define release memory_order_release
+#define acquire memory_order_acquire
+#define seqcst memory_order_seq_cst
+#define acqrel memory_order_acq_rel
+
+#endif