src/AlloyEnc/signature.cc

   1 #include "signature.h"
   2 #include "set.h"
   3
   4 bool BooleanSig::encodeSet = true;
   5
   6 BooleanSig::BooleanSig(uint id):
   7         Signature(id),
   8         value(-1)
   9 {
  10 }
  11
  12 bool BooleanSig::getValue(){
  13         ASSERT(value != -1);
  14         return (bool) value;
  15 }
  16
  17 string BooleanSig::toString() const{
  18         return "Boolean" + to_string(id) + ".value";
  19 }
  20
  21 string BooleanSig::getSignature() const{
  22         string str;
  23         if(encodeSet){
  24                 encodeSet = false;
  25                 str += "one sig BooleanSet {\n\
  26                 domain: set Int\n\
  27                 }{\n\
  28                 domain = 0 + 1 \n\
  29                 }\n";
  30         }
  31         str += "one sig Boolean" + to_string(id) + " {\n\
  32         value: Int\n\
  33         }{\n\
  34         value in BooleanSet.domain\n\
  35         }";
  36         return str;
  37 }
  38
  39 ElementSig::ElementSig(uint id, SetSig *_ssig):
  40         Signature(id),
  41         ssig(_ssig),
  42         value(0)
  43 {
  44 }
  45
  46 string ElementSig::toString() const{
  47         return "Element" + to_string(id) + ".value";
  48 }
  49
  50 string ElementSig::getSignature() const{
  51         return "one sig Element" + to_string(id) + " {\n\
  52                 value: Int\n\
  53                 }{\n\
  54                 value in " + *ssig + "\n\
  55                 }";
  56
  57 }
  58
  59 SetSig::SetSig(uint id, Set *set): Signature(id){
  60         ASSERT(set->getSize() > 0);
  61         domain = to_string(set->getElement(0));
  62         for(uint i=1; i< set->getSize(); i++){
  63                 domain += " + " + to_string(set->getElement(i));
  64         }
  65 }
  66
  67 string SetSig::toString() const{
  68         return "Set" + to_string(id) + ".domain";
  69 }
  70
  71 string SetSig::getSignature() const{
  72         return "one sig Set" + to_string(id) + " {\n\
  73                 domain: set Int\n\
  74                 }{\n\
  75                 domain = " + domain + "\n\
  76                 }";
  77
  78 }
  79
  80 string Signature::operator+(const string& str){
  81         return toString() + str;
  82 }
  83
  84 string operator+(const string& str, const Signature& sig){
  85         return str + sig.toString();
  86 }