anderson algorithm

_result.txt

=======
Answer
=======
[[p]] : {z, y, alloc_1}
[[alloc_1]] : set()    
[[q]] : {y}
[[z]] : set()
[[x]] : set()
[[y]] : set()
====
Info
====
Tokens:          {y, z, alloc_1}
Variables:       {[[p]], [[alloc_1]], [[q]], [[z]], [[x]], [[y]]}
Operator:        {'1': '∈', '2': '⊆'}
Constraints:
        1: (alloc_1 ∈  [[p]])
        2: ([[y]] ⊆  [[x]])
        3: ([[z]] ⊆  [[x]])
        4: For Each c ∈  Tokens,
                c ∈ [[p]] => [[z]] ⊆  [[c]]
        5: ([[q]] ⊆  [[p]])
        6: (y ∈  [[q]])
        7: For Each c ∈  Tokens,
                c ∈ [[p]] => [[x]] ⊆  [[c]]
        8: (z ∈  [[p]])

example.py

"""
Example.

p = alloc null;
x = y;
x = z;
*p = z;

p = q;
q = &y;
x = *p;
p = &z;
"""
import toy
from pprint import pprint

# 1
## p = alloc null;
### alloc-1 \in [[p]]
alloc_1 = toy.Token("alloc_1")
p__ = toy.Variable("[[p]]")
constraint1 = toy.ConstraintOne(alloc_1, 1, p__)

# 2
## x = y;
### [[y]] \subseteq [[x]]
x__ = toy.Variable("[[x]]")
y__ = toy.Variable("[[y]]")
constraint2 = toy.ConstraintOne(y__, 2, x__)

# 3
## x = z;
### [[z]] \subseteq [[x]]
z__ = toy.Variable("[[z]]")
constraint3 = toy.ConstraintOne(z__, 2, x__)

# 4
## *p = z;
### For each c \in Cells,
### c \in [[p]]  =>  [[z]] \subseteq [[c]]
constraint4 = toy.ConstraintForEach(p__, z__)

# 5
## p = q;
### [[q]] \subseteq [[p]]
q__ = toy.Variable("[[q]]")
constraint5 = toy.ConstraintOne(q__, 2, p__)

# 6
## q = &y;
### y \in [[q]]

y = toy.Token("y")
constraint6 = toy.ConstraintOne(y, 1, q__)

# 7
## x = *p;
### For each c \in Cells,
### c \in [[p]]  =>  [[c]] \subseteq [[x]]
constraint7 = toy.ConstraintForEach(p__, x__)


# 8
## p = &z;
### z \in [[p]]
z = toy.Token("z")
constraint8 = toy.ConstraintOne(z, 1, p__)

toy.run()

print()
print("=======")
print("Answer")
print("=======")
for i in toy.Variables:
	print(f"{i} : {i.getToken()}")

toy.printInfo()

toy.py

"""
Anderson Algorithm.
"""

Variables = set()
Tokens = set()
constraints = []

operator = {"1": "∈", 
			"2": "⊆"}


class Token:
	global Tokens
	def __init__(self, tokenName):
		self.name = tokenName
		Tokens.add(self)

	def __str__(self):
		return self.name

	def __repr__(self):
		return str(self)


class Variable:
	global Variables
	def __init__(self, variableName):
		self.name = variableName
		self.tokens = set()
		Variables.add(self)

	def getToken(self):
		return self.tokens

	def addToken(self, token):
		self.tokens.add(token)

	def __str__(self):
		return self.name

	def __repr__(self):
		return str(self)


class ConstraintOne:
	global constraints
	def __init__(self, operandLeft, operator, operandRight):
		self.operandLeft = operandLeft
		self.operator = operator
		self.operandRight = operandRight
		self.tokens = []
		constraints.append(self)

	def update(self):
		if( isinstance(self.operandLeft, Token) and isinstance(self.operandRight, Variable) and self.operator == 1):
			tokens_variable = self.operandRight.getToken()

			before_length = len(tokens_variable)
			self.operandRight.addToken(self.operandLeft)
			after_length = len(tokens_variable)

			if before_length != after_length:
				return 1
			else:
				return 0

		elif( isinstance(self.operandLeft, Variable) and isinstance(self.operandRight, Variable)):

			before_length = len(self.operandRight.getToken())

			for i in self.operandLeft.getToken():
				self.operandRight.addToken(i)

			after_length = len(self.operandRight.getToken())

			if before_length != after_length:
				return 1
			else:
				return 0
		return 0

	def getTokens(self):
		return self.tokens
	def __str__(self):
		return "(" + str(self.operandLeft) + " " + operator.get(str(self.operator)) + "  " + str(self.operandRight) + ")"
	def __repr__(self):
		return str(self)

class ConstraintIf:
	global constraints
	def __init__(self, ifOperandLeft, ifOperator, ifOperandRight, operandLeft, operator, operandRight):
		self.ifOperandLeft = ifOperandLeft
		self.ifOperator = ifOperator
		self.ifOperandRight = ifOperandRight
		self.operandLeft = operandLeft
		self.operator = operator
		self.operandRight = operandRight
		
	def update(self, tokens, variables):
		if( isinstance(self.ifOperandLeft, Token) and isinstance(self.ifOperandRight, Variable) and self.ifOperator == 1 and isinstance(self.operandLeft, Variable) and isinstance(self.operandRight, Variable) and self.operator == 2):
			if self.ifOperandLeft in self.ifOperandRight:
				before_length = len(self.operandRight)
				for i in self.operandLeft.getToken():
					self.operandRight.addToken(i)
				after_length = self.operandRight.getToken()

				if before_length != after_length:
					return 1
				return 0

		return 0

	def __str__(self):
		return "(" + str(self.ifOperandLeft) + " " + operator.get(str(self.ifOperator)) + "  " + str(self.ifOperandRight) \
				+ " => " + str(self.operandLeft) + " " + operator.get(str(self.operator)) + " " + str(self.operandRight) + ")"

	def __repr__(self):
		return str(self)


class ConstraintForEach:
	def __init__(self, ifVarRight, thenVarLeft):
		constraints.append(self)
		self.ifVarRight = ifVarRight
		self.thenVarLeft = thenVarLeft

	def update(self):
		if( isinstance(self.ifVarRight, Variable) and isinstance(self.thenVarLeft, Variable) ):
			for c in Tokens:
				if c in self.ifVarRight.getToken():
					if not (findVariable(f"[[{c}]]")):
						Variable(f"[[{c}]]")
					then_right_operand = findVariable(f"[[{c}]]")

					before_length = len(then_right_operand.getToken())
					for j in self.thenVarLeft.getToken():
						then_right_operand.addToken(j)
					after_length = len(then_right_operand.getToken())
					
					if before_length != after_length:
						return 1
					return 0
		return 0

	def __str__(self):
		return f"For Each c {operator.get('1')}  Tokens,\n\t\t" + f"c {operator.get('1')} {self.ifVarRight} => {self.thenVarLeft} {operator.get('2')}  [[c]]"
	def __repr__(self):
		return str(self)

class ConstraintFun:
	# 생각을 하세요.
	pass

def getTokens():
	return Tokens
def getVariables():
	return Variables
def getOperator():
	return operator
def getConstraints():
	return constraints

def findVariable(name):
	for i in Variables:
		if i.name == name:
			return i
	return 0

def run():
	"""
	run cubic Algorithm.
	How to?
	how update tokens, variables?
	"""
	while True:
		condition = 0
		for i in constraints:
			condition += i.update()
		if condition == 0:
			for i in constraints:
				condition += i.update()
			if condtion == 0:
				break;
		
	pass

#### print ####
def printInfo():
	print("====")
	print("Info")
	print("====")
	print("Tokens:\t\t", getTokens())
	print("Variables:\t", getVariables())
	print("Operator:\t", getOperator())
	print("Constraints:")
	for index, constraint in enumerate(getConstraints(), start=1):
		print(f"\t{index}: {constraint}")