From 7c9674de2cb89d53417b40756b100292198c039e Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Fri, 25 Jan 2019 12:13:33 -0800
Subject: [PATCH] Adding support for ElementFunction

---
 src/AlloyEnc/alloyenc.cc  | 65 ++++++++++++++++++++++++++++++++++-----
 src/AlloyEnc/alloyenc.h   |  4 ++-
 src/AlloyEnc/signature.cc |  6 ++--
 src/AlloyEnc/signature.h  |  2 +-
 4 files changed, 64 insertions(+), 13 deletions(-)

diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc
index 9951644..35ecd45 100644
--- a/src/AlloyEnc/alloyenc.cc
+++ b/src/AlloyEnc/alloyenc.cc
@@ -8,6 +8,7 @@
 #include "element.h"
 #include "signature.h"
 #include "set.h"
+#include "function.h"
 #include <fstream>
 #include <regex>
 
@@ -34,6 +35,7 @@ AlloyEnc::~AlloyEnc(){
 }
 
 void AlloyEnc::encode(){
+	dumpAlloyHeader();
 	SetIteratorBooleanEdge *iterator = csolver->getConstraints();
 	Vector<char *> facts;
 	while(iterator->hasNext()){
@@ -75,13 +77,17 @@ int AlloyEnc::getResult(){
 	return IS_SAT;
 }
 
-void AlloyEnc::dumpAlloyIntScope(){
+void AlloyEnc::dumpAlloyFooter(){
 	output << "pred show {}" << endl;
 	output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
 }
 
+void AlloyEnc::dumpAlloyHeader(){
+	output << "open util/integer" << endl;
+}
+
 int AlloyEnc::solve(){
-	dumpAlloyIntScope();
+	dumpAlloyFooter();
 	int result = IS_INDETER;
 	char buffer [512];
 	if( output.is_open()){
@@ -166,26 +172,69 @@ string AlloyEnc::encodeBooleanVar( BooleanVar *bv){
 	return *boolSig + " = 1";
 }
 
+string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
+	FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
+	uint numDomains = elemFunc->inputs.getSize();
+	ASSERT(numDomains > 1);
+	ElementSig *inputs[numDomains];
+	string result;
+	for (uint i = 0; i < numDomains; i++) {
+		Element *elem = elemFunc->inputs.get(i);
+		inputs[i] = sigEnc.getElementSignature(elem);
+		if(elem->type == ELEMFUNCRETURN){
+			result += processElementFunction((ElementFunction *) elem, inputs[i]);
+		}
+	}
+	string op;
+	switch(function->op){
+		case SATC_ADD:
+			op = ".add";
+			break;
+		case SATC_SUB:
+			op = ".sub";
+			break;
+		default:
+			ASSERT(0);
+	}
+	result += *signature + " = " + *inputs[0];
+	for (uint i = 1; i < numDomains; i++) {
+		result += op + "["+ *inputs[i] +"]";
+	}
+	result += "\n";
+	return result;
+}
+
 string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){
+	constraint->print();
 	PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
 	ASSERT(constraint->inputs.getSize() == 2);
+	string str;
 	Element *elem0 = constraint->inputs.get(0);
-	ASSERT(elem0->type = ELEMSET);
+	ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
 	ElementSig *elemSig1 = sigEnc.getElementSignature(elem0);
+	if(elem0->type == ELEMFUNCRETURN){
+		str += processElementFunction((ElementFunction *) elem0, elemSig1);
+	}
 	Element *elem1 = constraint->inputs.get(1);
-	ASSERT(elem1->type = ELEMSET);
+	ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
 	ElementSig *elemSig2 = sigEnc.getElementSignature(elem1);
+	if(elem1->type == ELEMFUNCRETURN){
+		str += processElementFunction((ElementFunction *) elem1, elemSig2);
+	}
 	switch (predicate->getOp()) {
 		case SATC_EQUALS:
-			return *elemSig1 + " = " + *elemSig2;
+			str += *elemSig1 + " = " + *elemSig2;
+			break;
 		case SATC_LT:
-			return *elemSig1 + " < " + *elemSig2;
+			str += *elemSig1 + " < " + *elemSig2;
+			break;
 		case SATC_GT:
-			return *elemSig1 + " > " + *elemSig2; 
+			str += *elemSig1 + " > " + *elemSig2;
+			break; 
 		default:
 			ASSERT(0);
 	}
-	exit(-1);
+	return str;
 }
 
 void AlloyEnc::writeToFile(string str){
diff --git a/src/AlloyEnc/alloyenc.h b/src/AlloyEnc/alloyenc.h
index 7864b84..97049e2 100644
--- a/src/AlloyEnc/alloyenc.h
+++ b/src/AlloyEnc/alloyenc.h
@@ -17,13 +17,15 @@ public:
 	bool getBooleanValue(Boolean *element);
 	~AlloyEnc();
 private:
-	void dumpAlloyIntScope();
+	void dumpAlloyFooter();
+	void dumpAlloyHeader();
 	string encodeConstraint(BooleanEdge constraint);
 	int getResult();
 	string encodeBooleanLogic( BooleanLogic *bl);
 	string encodeBooleanVar( BooleanVar *bv);
 	string encodePredicate( BooleanPredicate *bp);
 	string encodeOperatorPredicate(BooleanPredicate *constraint);
+	string processElementFunction(ElementFunction *element, ElementSig *signature);
 	CSolver *csolver;
 	SignatureEnc sigEnc;
 	ofstream output;
diff --git a/src/AlloyEnc/signature.cc b/src/AlloyEnc/signature.cc
index 4237fd6..4b898d8 100644
--- a/src/AlloyEnc/signature.cc
+++ b/src/AlloyEnc/signature.cc
@@ -1,7 +1,7 @@
 #include "signature.h"
 #include "set.h"
 
-bool BooleanSig::encodeSet = true;
+bool BooleanSig::encodeAbsSig = true;
 
 BooleanSig::BooleanSig(uint id):
 	Signature(id),
@@ -20,8 +20,8 @@ string BooleanSig::toString() const{
 
 string BooleanSig::getSignature() const{
 	string str;
-	if(encodeSet){
-		encodeSet = false;
+	if(encodeAbsSig){
+		encodeAbsSig = false;
 		str += "one sig BooleanSet {\n\
 		domain: set Int\n\
 		}{\n\
diff --git a/src/AlloyEnc/signature.h b/src/AlloyEnc/signature.h
index 107002a..b3ebf47 100644
--- a/src/AlloyEnc/signature.h
+++ b/src/AlloyEnc/signature.h
@@ -26,7 +26,7 @@ public:
 	virtual string getSignature() const;
 private:
 	int value;
-	static bool encodeSet;
+	static bool encodeAbsSig;
 };
 
 class SetSig: public Signature{
-- 
2.34.1