6a84180ee88f91edee8ecb3ea23cd7f29960811f
[satune.git] / src / AlloyEnc / alloyenc.cc
1 #include "alloyenc.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 "signature.h"
10 #include "set.h"
11 #include "function.h"
12 #include <fstream>
13 #include <regex>
14
15 using namespace std;
16
17 const char * AlloyEnc::alloyFileName = "satune.als";
18 const char * AlloyEnc::solutionFile = "solution.sol";
19
20 AlloyEnc::AlloyEnc(CSolver *_solver): 
21         csolver(_solver),
22         sigEnc(this)
23 {
24         output.open(alloyFileName);
25         if(!output.is_open()){
26                 model_print("AlloyEnc:Error in opening the dump file satune.als\n");
27                 exit(-1);
28         }
29 }
30
31 AlloyEnc::~AlloyEnc(){
32         if(output.is_open()){
33                 output.close();
34         }
35 }
36
37 void AlloyEnc::encode(){
38         dumpAlloyHeader();
39         SetIteratorBooleanEdge *iterator = csolver->getConstraints();
40         Vector<char *> facts;
41         while(iterator->hasNext()){
42                 BooleanEdge constraint = iterator->next();
43                 string constr = encodeConstraint(constraint);
44                 //model_print("constr=%s\n", constr.c_str());
45                 char *cstr = new char [constr.length()+1];
46                 strcpy (cstr, constr.c_str());
47                 facts.push(cstr);
48         }
49         output << "fact {" << endl;
50         for(uint i=0; i< facts.getSize(); i++){
51                 char *cstr = facts.get(i);
52                 writeToFile(cstr);
53                 delete[] cstr;
54         }
55         output << "}" << endl;
56         delete iterator;
57 }
58
59 void tokenize(string const &str, const char delim, vector<std::string> &out)
60 {
61         size_t start;
62         size_t end = 0;
63
64         while ((start = str.find_first_not_of(delim, end)) != string::npos)
65         {
66                 end = str.find(delim, start);
67                 out.push_back(str.substr(start, end - start));
68         }
69 }
70
71 int AlloyEnc::getResult(){
72         ifstream input(solutionFile, ios::in);
73         string line;
74         while(getline(input, line)){
75                 if(regex_match(line, regex("Unsatisfiable."))){
76                         return IS_UNSAT;
77                 }
78                 if(regex_match(line, regex(".*Element.*value=.*Element\\d+.*->\\d+.*"))){
79                         vector<string> values;
80                         const char delim = ',';
81                         tokenize(line, delim, values);
82                         for (uint i=0; i<values.size(); i++){
83                                 uint i1, i2;
84                                 uint64_t i3;
85                                 if (3 == sscanf(values[i].c_str(),"%*[^0123456789]%d%*[^0123456789]%d%*[^0123456789]%" PRId64 "", &i1, &i2, &i3)){
86                                         model_print("Element%d = %" PRId64 "\n", i1, i3);
87                                         sigEnc.setValue(i1, i3);
88                                 }
89                         }
90                 }
91         }
92         return IS_SAT;
93 }
94
95 void AlloyEnc::dumpAlloyFooter(){
96         output << "pred show {}" << endl;
97         output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
98 }
99
100 void AlloyEnc::dumpAlloyHeader(){
101         output << "open util/integer" << endl;
102 }
103
104 int AlloyEnc::solve(){
105         dumpAlloyFooter();
106         int result = IS_INDETER;
107         char buffer [512];
108         if( output.is_open()){
109                 output.close();
110         }
111         snprintf(buffer, sizeof(buffer), "./run.sh java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", alloyFileName, solutionFile);
112         int status = system(buffer);
113         if (status == 0) {
114                 //Read data in from results file
115                 result = getResult();
116         }
117         return result;
118 }
119
120 string AlloyEnc::encodeConstraint(BooleanEdge c){
121         Boolean *constraint = c.getBoolean();
122         string res;
123         switch(constraint->type){
124                 case LOGICOP:{
125                         res = encodeBooleanLogic((BooleanLogic *) constraint);
126                         break;
127                 }
128                 case PREDICATEOP:{
129                         res = encodePredicate((BooleanPredicate *) constraint);
130                         break;
131                 }
132                 case BOOLEANVAR:{
133                         res = encodeBooleanVar( (BooleanVar *) constraint);
134                         break;
135                 }
136                 default:
137                         ASSERT(0);
138         }
139         if(c.isNegated()){
140                 return "not ( " + res + " )";
141         }
142         return res;
143 }
144
145 string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){
146         uint size = bl->inputs.getSize();
147         string array[size];
148         for (uint i = 0; i < size; i++)
149                 array[i] = encodeConstraint(bl->inputs.get(i));
150         switch (bl->op) {
151                 case SATC_AND:{
152                         ASSERT(size >= 2);
153                         string res = "";
154                         res += array[0];
155                         for( uint i=1; i< size; i++){
156                                 res += " and " + array[i];
157                         }
158                         return res;
159                 }
160                 case SATC_NOT:{
161                         return "not " + array[0];
162                 }
163                 case SATC_IFF:
164                         return array[0] + " iff " + array[1];
165                 case SATC_OR:
166                 case SATC_XOR:
167                 case SATC_IMPLIES:
168                 default:
169                         ASSERT(0);
170
171         }
172 }
173
174 string AlloyEnc::encodePredicate( BooleanPredicate *bp){
175         switch (bp->predicate->type) {
176                 case TABLEPRED:
177                         ASSERT(0);
178                 case OPERATORPRED:
179                         return encodeOperatorPredicate(bp);
180                 default:
181                         ASSERT(0);
182         }
183 }
184
185 string AlloyEnc::encodeBooleanVar( BooleanVar *bv){
186         BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
187         return *boolSig + " = 1";
188 }
189
190 string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
191         FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
192         uint numDomains = elemFunc->inputs.getSize();
193         ASSERT(numDomains > 1);
194         ElementSig *inputs[numDomains];
195         string result;
196         for (uint i = 0; i < numDomains; i++) {
197                 Element *elem = elemFunc->inputs.get(i);
198                 inputs[i] = sigEnc.getElementSignature(elem);
199                 if(elem->type == ELEMFUNCRETURN){
200                         result += processElementFunction((ElementFunction *) elem, inputs[i]);
201                 }
202         }
203         string op;
204         switch(function->op){
205                 case SATC_ADD:
206                         op = ".add";
207                         break;
208                 case SATC_SUB:
209                         op = ".sub";
210                         break;
211                 default:
212                         ASSERT(0);
213         }
214         result += *signature + " = " + *inputs[0];
215         for (uint i = 1; i < numDomains; i++) {
216                 result += op + "["+ *inputs[i] +"]";
217         }
218         result += "\n";
219         return result;
220 }
221
222 string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){
223         PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
224         ASSERT(constraint->inputs.getSize() == 2);
225         string str;
226         Element *elem0 = constraint->inputs.get(0);
227         ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
228         ElementSig *elemSig1 = sigEnc.getElementSignature(elem0);
229         if(elem0->type == ELEMFUNCRETURN){
230                 str += processElementFunction((ElementFunction *) elem0, elemSig1);
231         }
232         Element *elem1 = constraint->inputs.get(1);
233         ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
234         ElementSig *elemSig2 = sigEnc.getElementSignature(elem1);
235         if(elem1->type == ELEMFUNCRETURN){
236                 str += processElementFunction((ElementFunction *) elem1, elemSig2);
237         }
238         switch (predicate->getOp()) {
239                 case SATC_EQUALS:
240                         str += *elemSig1 + " = " + *elemSig2;
241                         break;
242                 case SATC_LT:
243                         str += *elemSig1 + " < " + *elemSig2;
244                         break;
245                 case SATC_GT:
246                         str += *elemSig1 + " > " + *elemSig2;
247                         break; 
248                 default:
249                         ASSERT(0);
250         }
251         return str;
252 }
253
254 void AlloyEnc::writeToFile(string str){
255         output << str << endl;
256 }
257
258 bool AlloyEnc::getBooleanValue(Boolean *b){
259         if (b->boolVal == BV_MUSTBETRUE)
260                 return true;
261         else if (b->boolVal == BV_MUSTBEFALSE)
262                 return false;
263         return sigEnc.getBooleanSignature(b);
264 }
265
266 uint64_t AlloyEnc::getValue(Element * element){
267         ElementEncoding *elemEnc = element->getElementEncoding();
268         if (elemEnc->numVars == 0)//case when the set has only one item
269                 return element->getRange()->getElement(0);
270         return sigEnc.getValue(element);
271 }
272