projects
/
satune.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Adding SMT Interpreters
[satune.git]
/
src
/
Interpreter
/
signatureenc.cc
diff --git
a/src/Interpreter/signatureenc.cc
b/src/Interpreter/signatureenc.cc
index 888efe295b39da80f05ba7a0e9ffc4c85969f11e..cdc8aa11b26a7fce870bed915f85c43fa88cbfb7 100644
(file)
--- a/
src/Interpreter/signatureenc.cc
+++ b/
src/Interpreter/signatureenc.cc
@@
-2,8
+2,7
@@
#include "element.h"
#include "set.h"
#include "signature.h"
#include "element.h"
#include "set.h"
#include "signature.h"
-#include "alloyenc.h"
-#include "math.h"
+#include "interpreter.h"
SignatureEnc::SignatureEnc(Interpreter *inter):
interpreter(inter),
SignatureEnc::SignatureEnc(Interpreter *inter):
interpreter(inter),
@@
-18,11
+17,6
@@
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){
void SignatureEnc::updateMaxValue(Set *set){
for(uint i=0; i< set->getSize(); i++){
if(set->getElement(i) > maxValue){
@@
-31,10
+25,10
@@
void SignatureEnc::updateMaxValue(Set *set){
}
}
}
}
-
BooleanSig
*SignatureEnc::getBooleanSignature(Boolean *bvar){
-
BooleanSig *bsig = (BooleanSig
*)encoded.get((void *)bvar);
+
ValuedSignature
*SignatureEnc::getBooleanSignature(Boolean *bvar){
+
ValuedSignature *bsig = (ValuedSignature
*)encoded.get((void *)bvar);
if(bsig == NULL){
if(bsig == NULL){
- bsig =
new BooleanSig
(getUniqueSigID());
+ bsig =
interpreter->getBooleanSignature
(getUniqueSigID());
encoded.put(bvar, bsig);
signatures.push(bsig);
interpreter->writeToFile(bsig->getSignature());
encoded.put(bvar, bsig);
signatures.push(bsig);
interpreter->writeToFile(bsig->getSignature());
@@
-42,19
+36,19
@@
BooleanSig *SignatureEnc::getBooleanSignature(Boolean *bvar){
return bsig;
}
return bsig;
}
-
ElementSig
*SignatureEnc::getElementSignature(Element *element){
-
ElementSig *esig = (ElementSig
*)encoded.get((void *)element);
+
ValuedSignature
*SignatureEnc::getElementSignature(Element *element){
+
ValuedSignature *esig = (ValuedSignature
*)encoded.get((void *)element);
if(esig == NULL){
Set *set = element->getRange();
if(esig == NULL){
Set *set = element->getRange();
- S
etSig *ssig = (SetSig
*)encoded.get((void *)set);
+ S
ignature *ssig = (Signature
*)encoded.get((void *)set);
if(ssig == NULL){
if(ssig == NULL){
- ssig =
new SetSig
(getUniqueSigID(), set);
+ ssig =
interpreter->getSetSignature
(getUniqueSigID(), set);
encoded.put(set, ssig);
signatures.push(ssig);
interpreter->writeToFile(ssig->getSignature());
updateMaxValue(set);
}
encoded.put(set, ssig);
signatures.push(ssig);
interpreter->writeToFile(ssig->getSignature());
updateMaxValue(set);
}
- esig =
new ElementSig
(getUniqueSigID(), ssig);
+ esig =
interpreter->getElementSignature
(getUniqueSigID(), ssig);
encoded.put(element, esig);
signatures.push(esig);
interpreter->writeToFile(esig->getSignature());
encoded.put(element, esig);
signatures.push(esig);
interpreter->writeToFile(esig->getSignature());