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 <fstream>
  11 #include <regex>
  12
  13 using namespace std;
  14
  15 const char * AlloyEnc::alloyFileName = "satune.als";
  16 const char * AlloyEnc::solutionFile = "solution.sol";
  17
  18 AlloyEnc::AlloyEnc(CSolver *_solver):
  19         csolver(_solver),
  20         sigEnc(this)
  21 {
  22         output.open(alloyFileName);
  23         if(!output.is_open()){
  24                 model_print("AlloyEnc:Error in opening the dump file satune.als\n");
  25                 exit(-1);
  26         }
  27 }
  28
  29 AlloyEnc::~AlloyEnc(){
  30         if(output.is_open()){
  31                 output.close();
  32         }
  33 }
  34
  35 void AlloyEnc::encode(){
  36         SetIteratorBooleanEdge *iterator = csolver->getConstraints();
  37         Vector<char *> facts;
  38         while(iterator->hasNext()){
  39                 BooleanEdge constraint = iterator->next();
  40                 string constr = encodeConstraint(constraint);
  41                 //model_print("constr=%s\n", constr.c_str());
  42                 char *cstr = new char [constr.length()+1];
  43                 strcpy (cstr, constr.c_str());
  44                 facts.push(cstr);
  45         }
  46         output << "fact {" << endl;
  47         for(uint i=0; i< facts.getSize(); i++){
  48                 char *cstr = facts.get(i);
  49                 writeToFile(cstr);
  50                 delete[] cstr;
  51         }
  52         output << "}" << endl;
  53         delete iterator;
  54 }
  55
  56 int AlloyEnc::getResult(){
  57         ifstream input(solutionFile, ios::in);
  58         string line;
  59         while(getline(input, line)){
  60                 if(regex_match(line, regex("Unsatisfiable."))){
  61                         return IS_UNSAT;
  62                 }
  63                 if(regex_match(line, regex(".*Element\\d+.*value=.*Element\\d+.*->\\d+.*"))){
  64                         int tmp=0, index=0, value=0;
  65                         const char* s = line.c_str();
  66                         uint i1, i2, i3;
  67                         uint64_t i4;
  68                         if (4 == sscanf(s,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%d%*[^0123456789]%" PRId64 "", &i1, &i2, &i3, &i4)){
  69                                 model_print("Element%d = %" PRId64 "\n", i1, i4);
  70                                 sigEnc.setValue(i1, i4);
  71                         }
  72                 }
  73         }
  74         return IS_SAT;
  75 }
  76
  77 int AlloyEnc::solve(){
  78         int result = IS_INDETER;
  79         char buffer [512];
  80         if( output.is_open()){
  81                 output.close();
  82         }
  83         snprintf(buffer, sizeof(buffer), "./run.sh java edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", alloyFileName, solutionFile);
  84         int status = system(buffer);
  85         if (status == 0) {
  86                 //Read data in from results file
  87                 result = getResult();
  88         }
  89         return result;
  90 }
  91
  92 string AlloyEnc::encodeConstraint(BooleanEdge c){
  93         Boolean *constraint = c.getBoolean();
  94         string res;
  95         switch(constraint->type){
  96                 case LOGICOP:{
  97                         res = encodeBooleanLogic((BooleanLogic *) constraint);
  98                         break;
  99                 }
 100                 case PREDICATEOP:{
 101                         res = encodePredicate((BooleanPredicate *) constraint);
 102                         break;
 103                 }
 104                 default:
 105                         ASSERT(0);
 106         }
 107         if(c.isNegated()){
 108                 return "not ( " + res + " )";
 109         }
 110         return res;
 111 }
 112
 113 string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){
 114         uint size = bl->inputs.getSize();
 115         string array[size];
 116         for (uint i = 0; i < size; i++)
 117                 array[i] = encodeConstraint(bl->inputs.get(i));
 118         switch (bl->op) {
 119                 case SATC_AND:{
 120                         ASSERT(size >= 2);
 121                         string res = "";
 122                         res += array[0];
 123                         for( uint i=1; i< size; i++){
 124                                 res += " and " + array[i];
 125                         }
 126                         return res;
 127                 }
 128                 case SATC_NOT:{
 129                         return "not " + array[0];
 130                 }
 131                 case SATC_IFF:
 132                         return array[0] + " iff " + array[1];
 133                 case SATC_OR:
 134                 case SATC_XOR:
 135                 case SATC_IMPLIES:
 136                 default:
 137                         ASSERT(0);
 138
 139         }
 140 }
 141
 142 string AlloyEnc::encodePredicate( BooleanPredicate *bp){
 143         switch (bp->predicate->type) {
 144                 case TABLEPRED:
 145                         ASSERT(0);
 146                 case OPERATORPRED:
 147                         return encodeOperatorPredicate(bp);
 148                 default:
 149                         ASSERT(0);
 150         }
 151 }
 152
 153 string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){
 154         PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
 155         ASSERT(constraint->inputs.getSize() == 2);
 156         Element *elem0 = constraint->inputs.get(0);
 157         ASSERT(elem0->type = ELEMSET);
 158         ElementSig *elemSig1 = sigEnc.getElementSignature(elem0);
 159         Element *elem1 = constraint->inputs.get(1);
 160         ASSERT(elem1->type = ELEMSET);
 161         ElementSig *elemSig2 = sigEnc.getElementSignature(elem1);
 162         switch (predicate->getOp()) {
 163                 case SATC_EQUALS:
 164                         return *elemSig1 + " = " + *elemSig2;
 165                 case SATC_LT:
 166                         return *elemSig1 + " < " + *elemSig2;
 167                 case SATC_GT:
 168                         return *elemSig1 + " > " + *elemSig2;
 169                 default:
 170                         ASSERT(0);
 171         }
 172         exit(-1);
 173 }
 174
 175 void AlloyEnc::writeToFile(string str){
 176         output << str << endl;
 177 }
 178
 179 uint64_t AlloyEnc::getValue(Element * element){
 180         return sigEnc.getValue(element);
 181 }
 182