src/AlloyEnc/signature.cc

   1 #include "signature.h"
   2 #include "set.h"
   3
   4 bool BooleanSig::encodeAbs = true;
   5 bool SetSig::encodeAbs = true;
   6 bool ElementSig::encodeAbs = true;
   7
   8 BooleanSig::BooleanSig(uint id):
   9         Signature(id),
  10         value(-1)
  11 {
  12 }
  13
  14 bool BooleanSig::getValue(){
  15         ASSERT(value != -1);
  16         return (bool) value;
  17 }
  18
  19 string BooleanSig::toString() const{
  20         return "Boolean" + to_string(id) + ".value";
  21 }
  22
  23 string BooleanSig::getSignature() const{
  24         string str;
  25         if(encodeAbs){
  26                 encodeAbs = false;
  27                 str += getAbsSignature();
  28         }
  29         str += "one sig Boolean" + to_string(id) + " extends AbsBool {}";
  30         return str;
  31 }
  32
  33 string BooleanSig::getAbsSignature() const{
  34         string str;
  35         if(SetSig::encodeAbs){
  36                 SetSig::encodeAbs = false;
  37                 str += "abstract sig AbsSet {\
  38                 domain: set Int\
  39                 }\n";
  40         }
  41         str +="one sig BooleanSet extends AbsSet {}{\n\
  42         domain = 0 + 1 \n\
  43         }\n\
  44         abstract sig AbsBool {\
  45         value: Int\
  46         }{\n\
  47         value in BooleanSet.domain\n\
  48         }\n";
  49         return str;
  50 }
  51
  52 ElementSig::ElementSig(uint id, SetSig *_ssig):
  53         Signature(id),
  54         ssig(_ssig),
  55         value(0)
  56 {
  57 }
  58
  59 string ElementSig::toString() const{
  60         return "Element" + to_string(id) + ".value";
  61 }
  62
  63 string ElementSig::getSignature() const{
  64         string str;
  65         if(encodeAbs){
  66                 encodeAbs = false;
  67                 str += getAbsSignature();
  68         }
  69         str += "one sig Element" + to_string(id) + " extends AbsElement {}{\n\
  70                 value in " + *ssig + "\n\
  71                 }";
  72         return str;
  73 }
  74
  75 string ElementSig::getAbsSignature() const{
  76         return "abstract sig AbsElement {\n\
  77                 value: Int\n\
  78                 }\n";
  79
  80 }
  81
  82 SetSig::SetSig(uint id, Set *set): Signature(id){
  83         ASSERT(set->getSize() > 0);
  84         domain = to_string(set->getElement(0));
  85         for(uint i=1; i< set->getSize(); i++){
  86                 domain += " + " + to_string(set->getElement(i));
  87         }
  88 }
  89
  90 string SetSig::toString() const{
  91         return "Set" + to_string(id) + ".domain";
  92 }
  93
  94 string SetSig::getSignature() const{
  95         string str;
  96         if(encodeAbs){
  97                 encodeAbs = false;
  98                 str += getAbsSignature();
  99         }
 100         str += "one sig Set" + to_string(id) + " extends AbsSet {}{\n\
 101                 domain = " + domain + "\n\
 102                 }";
 103         return str;
 104 }
 105
 106 string SetSig::getAbsSignature() const{
 107         return "abstract sig AbsSet {\n\
 108                 domain: set Int\n\
 109                 }\n";
 110
 111 }
 112
 113 string Signature::operator+(const string& str){
 114         return toString() + str;
 115 }
 116
 117 string operator+(const string& str, const Signature& sig){
 118         return str + sig.toString();
 119 }