021b0878ed339fd6ee1b509095c24b101d57462b
[satune.git] / src / Interpreter / alloyinterpreter.cc
1 #include "alloyinterpreter.h"
2 #include <string>
3 #include "signatureenc.h"
4 #include "structs.h"
5 #include "csolver.h"
6 #include "boolean.h"
7 #include "predicate.h"
8 #include "element.h"
9 #include "alloysig.h"
10 #include "set.h"
11 #include "function.h"
12 #include "inc_solver.h"
13 #include <fstream>
14 #include "cppvector.h"
15 #include "math.h"
16
17 using namespace std;
18
19 #define ALLOYFILENAME "satune.als"
20 #define ALLOYSOLUTIONFILE "solution.sol"
21
22 AlloyInterpreter::AlloyInterpreter(CSolver *_solver): 
23         Interpreter(_solver) 
24 {
25         output.open(ALLOYFILENAME);
26         if(!output.is_open()){
27                 model_print("AlloyEnc:Error in opening the dump file satune.als\n");
28                 exit(-1);
29         }
30 }
31
32 AlloyInterpreter::~AlloyInterpreter(){
33         if(output.is_open()){
34                 output.close();
35         }
36 }
37
38 ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id){
39         return new AlloyBoolSig(id);
40 }
41
42 ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig){
43         return new AlloyElementSig(id, ssig);
44 }
45
46 Signature *AlloyInterpreter::getSetSignature(uint id, Set *set){
47         return new AlloySetSig(id, set);
48 }
49
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);
54                 writeToFile(cstr);
55         }
56         output << "}" << endl;
57 }
58
59
60 int AlloyInterpreter::getResult(){
61         ifstream input(ALLOYSOLUTIONFILE, ios::in);
62         string line;
63         while(getline(input, line)){
64                 if(line.find("Unsatisfiable.")== 0){
65                         return IS_UNSAT;
66                 }
67                 if(line.find("univ") == 0){
68                         continue;
69                 }
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 ) {
76                                 uint i1, i2, i3;
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);
80                                 }
81                                 token = strtok(NULL, delim);
82                         }
83                 }
84         }
85         return IS_SAT;
86 }
87
88
89 int AlloyInterpreter::getAlloyIntScope(){
90         double mylog = log2(sigEnc.getMaxValue() + 1);
91         return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2;
92 }
93
94 void AlloyInterpreter::dumpFooter(){
95         output << "pred show {}" << endl;
96         output << "run show for " << getAlloyIntScope() << " int" << endl;
97 }
98
99 void AlloyInterpreter::dumpHeader(){
100         output << "open util/integer" << endl;
101 }
102
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);
106 }
107
108 string AlloyInterpreter::negateConstraint(string constr){
109         return "not ( " + constr + " )";
110 }
111
112 string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl){
113         uint size = bl->inputs.getSize();
114         string array[size];
115         for (uint i = 0; i < size; i++)
116                 array[i] = encodeConstraint(bl->inputs.get(i));
117         string op;
118         switch (bl->op){
119                 case SATC_OR:
120                         op = " or ";
121                         break;
122                 case SATC_AND:
123                         op = " and ";
124                         break;
125                 case SATC_NOT:
126                         op = " not ";
127                         break;
128                 case SATC_IFF:
129                         op = " iff ";
130                         break;
131                 case SATC_IMPLIES:
132                         op = " implies ";
133                         break;
134                 case SATC_XOR:
135                 default:
136                         ASSERT(0);
137         }
138         switch (bl->op) {
139                 case SATC_OR:
140                 case SATC_AND:{
141                         ASSERT(size >= 2);
142                         string res = "( ";
143                         res += array[0];
144                         for( uint i=1; i< size; i++){
145                                 res += op + array[i];
146                         }
147                         res += " )";
148                         return res;
149                 }
150                 case SATC_NOT:{
151                         return "not ( " + array[0] + " )";
152                 }
153                 case SATC_IMPLIES:
154                 case SATC_IFF:
155                         return "( " + array[0] + op + array[1] + " )";
156                 case SATC_XOR:
157                 default:
158                         ASSERT(0);
159
160         }
161 }
162
163 string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){
164         ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
165         return *boolSig + " = 1";
166 }
167
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];
173         string result;
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]);
179                 }
180         }
181         string op;
182         switch(function->op){
183                 case SATC_ADD:
184                         op = ".add";
185                         break;
186                 case SATC_SUB:
187                         op = ".sub";
188                         break;
189                 default:
190                         ASSERT(0);
191         }
192         result += *signature + " = " + *inputs[0];
193         for (uint i = 1; i < numDomains; i++) {
194                 result += op + "["+ *inputs[i] +"]";
195         }
196         result += "\n";
197         return result;
198 }
199
200 string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
201         switch (op) {
202                 case SATC_EQUALS:
203                         return *elemSig1 + " = " + *elemSig2;
204                 case SATC_LT:
205                         return *elemSig1 + " < " + *elemSig2;
206                 case SATC_GT:
207                         return *elemSig1 + " > " + *elemSig2;
208                 default:
209                         ASSERT(0);
210         }
211 }
212
213