#include "set.h"
#include "signature.h"
#include "alloyenc.h"
+#include "math.h"
-SignatureEnc::SignatureEnc(AlloyEnc *ae): alloyEncoder(ae){
+SignatureEnc::SignatureEnc(AlloyEnc *ae):
+ alloyEncoder(ae),
+ maxValue(0)
+{
}
SignatureEnc::~SignatureEnc(){
}
}
+int SignatureEnc::getAlloyIntScope(){
+ double mylog = log2(maxValue + 1);
+ return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2;
+}
+
+void SignatureEnc::updateMaxValue(Set *set){
+ for(uint i=0; i< set->getSize(); i++){
+ if(set->getElement(i) > maxValue){
+ maxValue = set->getElement(i);
+ }
+ }
+}
+
ElementSig *SignatureEnc::getElementSignature(Element *element){
ElementSig *esig = (ElementSig *)encoded.get((void *)element);
if(esig == NULL){
encoded.put(set, ssig);
signatures.push(ssig);
alloyEncoder->writeToFile(ssig->getSignature());
+ updateMaxValue(set);
}
esig = new ElementSig(signatures.getSize(), ssig);
+ element->print();
+ model_print(" = Element%u\n", signatures.getSize());
encoded.put(element, esig);
signatures.push(esig);
alloyEncoder->writeToFile(esig->getSignature());
uint64_t SignatureEnc::getValue(Element *element){
ElementSig *sig = (ElementSig *)encoded.get((void *) element);
ASSERT(sig != NULL);
+ model_print("******************\n");
+ element->print();
+ model_print("Value = %" PRId64 "\n", sig->getValue());
return sig->getValue();
}