35ecd45ca50366ee232f690fb24430c298a7d403
[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 int AlloyEnc::getResult(){
60         ifstream input(solutionFile, ios::in);
61         string line;
62         while(getline(input, line)){
63                 if(regex_match(line, regex("Unsatisfiable."))){
64                         return IS_UNSAT;
65                 }
66                 if(regex_match(line, regex(".*Element\\d+.*value=.*Element\\d+.*->\\d+.*"))){
67                         int tmp=0, index=0, value=0;
68                         const char* s = line.c_str();
69                         uint i1, i2, i3;
70                         uint64_t i4;
71                         if (4 == sscanf(s,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%d%*[^0123456789]%" PRId64 "", &i1, &i2, &i3, &i4)){
72                                 model_print("Element%d = %" PRId64 "\n", i1, i4);
73                                 sigEnc.setValue(i1, i4);
74                         }
75                 }
76         }
77         return IS_SAT;
78 }
79
80 void AlloyEnc::dumpAlloyFooter(){
81         output << "pred show {}" << endl;
82         output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
83 }
84
85 void AlloyEnc::dumpAlloyHeader(){
86         output << "open util/integer" << endl;
87 }
88
89 int AlloyEnc::solve(){
90         dumpAlloyFooter();
91         int result = IS_INDETER;
92         char buffer [512];
93         if( output.is_open()){
94                 output.close();
95         }
96         snprintf(buffer, sizeof(buffer), "./run.sh java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", alloyFileName, solutionFile);
97         int status = system(buffer);
98         if (status == 0) {
99                 //Read data in from results file
100                 result = getResult();
101         }
102         return result;
103 }
104
105 string AlloyEnc::encodeConstraint(BooleanEdge c){
106         Boolean *constraint = c.getBoolean();
107         string res;
108         switch(constraint->type){
109                 case LOGICOP:{
110                         res = encodeBooleanLogic((BooleanLogic *) constraint);
111                         break;
112                 }
113                 case PREDICATEOP:{
114                         res = encodePredicate((BooleanPredicate *) constraint);
115                         break;
116                 }
117                 case BOOLEANVAR:{
118                         res = encodeBooleanVar( (BooleanVar *) constraint);
119                         break;
120                 }
121                 default:
122                         ASSERT(0);
123         }
124         if(c.isNegated()){
125                 return "not ( " + res + " )";
126         }
127         return res;
128 }
129
130 string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){
131         uint size = bl->inputs.getSize();
132         string array[size];
133         for (uint i = 0; i < size; i++)
134                 array[i] = encodeConstraint(bl->inputs.get(i));
135         switch (bl->op) {
136                 case SATC_AND:{
137                         ASSERT(size >= 2);
138                         string res = "";
139                         res += array[0];
140                         for( uint i=1; i< size; i++){
141                                 res += " and " + array[i];
142                         }
143                         return res;
144                 }
145                 case SATC_NOT:{
146                         return "not " + array[0];
147                 }
148                 case SATC_IFF:
149                         return array[0] + " iff " + array[1];
150                 case SATC_OR:
151                 case SATC_XOR:
152                 case SATC_IMPLIES:
153                 default:
154                         ASSERT(0);
155
156         }
157 }
158
159 string AlloyEnc::encodePredicate( BooleanPredicate *bp){
160         switch (bp->predicate->type) {
161                 case TABLEPRED:
162                         ASSERT(0);
163                 case OPERATORPRED:
164                         return encodeOperatorPredicate(bp);
165                 default:
166                         ASSERT(0);
167         }
168 }
169
170 string AlloyEnc::encodeBooleanVar( BooleanVar *bv){
171         BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
172         return *boolSig + " = 1";
173 }
174
175 string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
176         FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
177         uint numDomains = elemFunc->inputs.getSize();
178         ASSERT(numDomains > 1);
179         ElementSig *inputs[numDomains];
180         string result;
181         for (uint i = 0; i < numDomains; i++) {
182                 Element *elem = elemFunc->inputs.get(i);
183                 inputs[i] = sigEnc.getElementSignature(elem);
184                 if(elem->type == ELEMFUNCRETURN){
185                         result += processElementFunction((ElementFunction *) elem, inputs[i]);
186                 }
187         }
188         string op;
189         switch(function->op){
190                 case SATC_ADD:
191                         op = ".add";
192                         break;
193                 case SATC_SUB:
194                         op = ".sub";
195                         break;
196                 default:
197                         ASSERT(0);
198         }
199         result += *signature + " = " + *inputs[0];
200         for (uint i = 1; i < numDomains; i++) {
201                 result += op + "["+ *inputs[i] +"]";
202         }
203         result += "\n";
204         return result;
205 }
206
207 string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){
208         constraint->print();
209         PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
210         ASSERT(constraint->inputs.getSize() == 2);
211         string str;
212         Element *elem0 = constraint->inputs.get(0);
213         ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
214         ElementSig *elemSig1 = sigEnc.getElementSignature(elem0);
215         if(elem0->type == ELEMFUNCRETURN){
216                 str += processElementFunction((ElementFunction *) elem0, elemSig1);
217         }
218         Element *elem1 = constraint->inputs.get(1);
219         ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
220         ElementSig *elemSig2 = sigEnc.getElementSignature(elem1);
221         if(elem1->type == ELEMFUNCRETURN){
222                 str += processElementFunction((ElementFunction *) elem1, elemSig2);
223         }
224         switch (predicate->getOp()) {
225                 case SATC_EQUALS:
226                         str += *elemSig1 + " = " + *elemSig2;
227                         break;
228                 case SATC_LT:
229                         str += *elemSig1 + " < " + *elemSig2;
230                         break;
231                 case SATC_GT:
232                         str += *elemSig1 + " > " + *elemSig2;
233                         break; 
234                 default:
235                         ASSERT(0);
236         }
237         return str;
238 }
239
240 void AlloyEnc::writeToFile(string str){
241         output << str << endl;
242 }
243
244 bool AlloyEnc::getBooleanValue(Boolean *b){
245         if (b->boolVal == BV_MUSTBETRUE)
246                 return true;
247         else if (b->boolVal == BV_MUSTBEFALSE)
248                 return false;
249         return sigEnc.getBooleanSignature(b);
250 }
251
252 uint64_t AlloyEnc::getValue(Element * element){
253         ElementEncoding *elemEnc = element->getElementEncoding();
254         if (elemEnc->numVars == 0)//case when the set has only one item
255                 return element->getRange()->getElement(0);
256         return sigEnc.getValue(element);
257 }
258