X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FInterpreter%2Falloyinterpreter.cc;h=c0e4a6094d97b8784fb8680eba9656f3e454d088;hp=f910ac60529453a2d8ed660c625d9704c358e6d5;hb=4c58af641a877bb6d65769994c8fd57ecedbd22c;hpb=917bc08fb2d0ea78f6492323d52a4465b517809a

diff --git a/src/Interpreter/alloyinterpreter.cc b/src/Interpreter/alloyinterpreter.cc
index f910ac6..c0e4a60 100644
--- a/src/Interpreter/alloyinterpreter.cc
+++ b/src/Interpreter/alloyinterpreter.cc
@@ -6,12 +6,13 @@
 #include "boolean.h"
 #include "predicate.h"
 #include "element.h"
-#include "signature.h"
+#include "alloysig.h"
 #include "set.h"
 #include "function.h"
 #include "inc_solver.h"
 #include <fstream>
 #include "cppvector.h"
+#include "math.h"
 
 using namespace std;
 
@@ -34,6 +35,18 @@ AlloyInterpreter::~AlloyInterpreter(){
 	}
 }
 
+ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id){
+	return new AlloyBoolSig(id);
+}
+
+ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig){
+	return new AlloyElementSig(id, ssig);
+}
+
+Signature *AlloyInterpreter::getSetSignature(uint id, Set *set){
+	return new AlloySetSig(id, set);
+}
+
 void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts){
 	output << "fact {" << endl;
 	for(uint i=0; i< facts.getSize(); i++){
@@ -60,7 +73,6 @@ int AlloyInterpreter::getResult(){
 			strcpy ( cline, line.c_str() );
 			char *token = strtok(cline, delim);
 			while( token != NULL ) {
-				printf( " %s\n", token );
 				uint i1, i2, i3;
 				if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
 					model_print("Signature%u = %u\n", i1, i3);
@@ -73,9 +85,15 @@ int AlloyInterpreter::getResult(){
 	return IS_SAT;
 }
 
+
+int AlloyInterpreter::getAlloyIntScope(){
+	double mylog = log2(sigEnc.getMaxValue() + 1);
+	return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2;
+}
+
 void AlloyInterpreter::dumpFooter(){
 	output << "pred show {}" << endl;
-	output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
+	output << "run show for " << getAlloyIntScope() << " int" << endl;
 }
 
 void AlloyInterpreter::dumpHeader(){
@@ -142,15 +160,15 @@ string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl){
 }
 
 string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){
-	BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
+	ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
 	return *boolSig + " = 1";
 }
 
-string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
+string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
 	FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
 	uint numDomains = elemFunc->inputs.getSize();
 	ASSERT(numDomains > 1);
-	ElementSig *inputs[numDomains];
+	ValuedSignature *inputs[numDomains];
 	string result;
 	for (uint i = 0; i < numDomains; i++) {
 		Element *elem = elemFunc->inputs.get(i);
@@ -178,7 +196,7 @@ string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, Eleme
 	return result;
 }
 
-string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2){
+string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
 	switch (op) {
 		case SATC_EQUALS:
 			return *elemSig1 + " = " + *elemSig2;