1 #include "alloyinterpreter.h"
3 #include "signatureenc.h"
12 #include "inc_solver.h"
14 #include "cppvector.h"
19 #define ALLOYFILENAME "satune.als"
20 #define ALLOYSOLUTIONFILE "solution.sol"
22 AlloyInterpreter::AlloyInterpreter(CSolver *_solver):
25 output.open(ALLOYFILENAME);
26 if(!output.is_open()){
27 model_print("AlloyEnc:Error in opening the dump file satune.als\n");
32 AlloyInterpreter::~AlloyInterpreter(){
38 ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id){
39 return new AlloyBoolSig(id);
42 ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig){
43 return new AlloyElementSig(id, ssig);
46 Signature *AlloyInterpreter::getSetSignature(uint id, Set *set){
47 return new AlloySetSig(id, set);
50 void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts){
51 output << "fact {" << endl;
52 for(uint i=0; i< facts.getSize(); i++){
53 char *cstr = facts.get(i);
56 output << "}" << endl;
60 int AlloyInterpreter::getResult(){
61 ifstream input(ALLOYSOLUTIONFILE, ios::in);
63 while(getline(input, line)){
64 if(line.find("Unsatisfiable.")== 0){
67 if(line.find("univ") == 0){
70 if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
71 const char delim [2] = ",";
72 char cline [line.size()+1];
73 strcpy ( cline, line.c_str() );
74 char *token = strtok(cline, delim);
75 while( token != NULL ) {
77 if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
78 model_print("Signature%u = %u\n", i1, i3);
79 sigEnc.setValue(i1, i3);
81 token = strtok(NULL, delim);
89 int AlloyInterpreter::getAlloyIntScope(){
90 double mylog = log2(sigEnc.getMaxValue() + 1);
91 return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2;
94 void AlloyInterpreter::dumpFooter(){
95 output << "pred show {}" << endl;
96 output << "run show for " << getAlloyIntScope() << " int" << endl;
99 void AlloyInterpreter::dumpHeader(){
100 output << "open util/integer" << endl;
103 void AlloyInterpreter::compileRunCommand(char * command, size_t size){
104 model_print("Calling Alloy...\n");
105 snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), ALLOYFILENAME, ALLOYSOLUTIONFILE);
108 string AlloyInterpreter::negateConstraint(string constr){
109 return "not ( " + constr + " )";
112 string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl){
113 uint size = bl->inputs.getSize();
115 for (uint i = 0; i < size; i++)
116 array[i] = encodeConstraint(bl->inputs.get(i));
144 for( uint i=1; i< size; i++){
145 res += op + array[i];
151 return "not ( " + array[0] + " )";
155 return "( " + array[0] + op + array[1] + " )";
163 string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){
164 ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
165 return *boolSig + " = 1";
168 string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
169 FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
170 uint numDomains = elemFunc->inputs.getSize();
171 ASSERT(numDomains > 1);
172 ValuedSignature *inputs[numDomains];
174 for (uint i = 0; i < numDomains; i++) {
175 Element *elem = elemFunc->inputs.get(i);
176 inputs[i] = sigEnc.getElementSignature(elem);
177 if(elem->type == ELEMFUNCRETURN){
178 result += processElementFunction((ElementFunction *) elem, inputs[i]);
182 switch(function->op){
192 result += *signature + " = " + *inputs[0];
193 for (uint i = 1; i < numDomains; i++) {
194 result += op + "["+ *inputs[i] +"]";
200 string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
203 return *elemSig1 + " = " + *elemSig2;
205 return *elemSig1 + " < " + *elemSig2;
207 return *elemSig1 + " > " + *elemSig2;