projects
/
satune.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
829b441
)
1)core dump in regex for big strings 2) Boolean Var bugs 3) adding support for other...
author
Hamed Gorjiara
<hgorjiar@uci.edu>
Thu, 7 Feb 2019 00:21:09 +0000
(16:21 -0800)
committer
Hamed Gorjiara
<hgorjiar@uci.edu>
Thu, 7 Feb 2019 00:21:09 +0000
(16:21 -0800)
src/AlloyEnc/alloyenc.cc
patch
|
blob
|
history
src/AlloyEnc/signature.cc
patch
|
blob
|
history
src/AlloyEnc/signature.h
patch
|
blob
|
history
src/AlloyEnc/signatureenc.cc
patch
|
blob
|
history
src/AlloyEnc/signatureenc.h
patch
|
blob
|
history
src/classlist.h
patch
|
blob
|
history
diff --git
a/src/AlloyEnc/alloyenc.cc
b/src/AlloyEnc/alloyenc.cc
index 6a84180ee88f91edee8ecb3ea23cd7f29960811f..6a8dcdfe1a122af005f6abd8e99f87521299ddf6 100644
(file)
--- a/
src/AlloyEnc/alloyenc.cc
+++ b/
src/AlloyEnc/alloyenc.cc
@@
-10,7
+10,7
@@
#include "set.h"
#include "function.h"
#include <fstream>
#include "set.h"
#include "function.h"
#include <fstream>
-#include <
regex
>
+#include <
vector
>
using namespace std;
using namespace std;
@@
-41,7
+41,6
@@
void AlloyEnc::encode(){
while(iterator->hasNext()){
BooleanEdge constraint = iterator->next();
string constr = encodeConstraint(constraint);
while(iterator->hasNext()){
BooleanEdge constraint = iterator->next();
string constr = encodeConstraint(constraint);
- //model_print("constr=%s\n", constr.c_str());
char *cstr = new char [constr.length()+1];
strcpy (cstr, constr.c_str());
facts.push(cstr);
char *cstr = new char [constr.length()+1];
strcpy (cstr, constr.c_str());
facts.push(cstr);
@@
-72,18
+71,20
@@
int AlloyEnc::getResult(){
ifstream input(solutionFile, ios::in);
string line;
while(getline(input, line)){
ifstream input(solutionFile, ios::in);
string line;
while(getline(input, line)){
- if(
regex_match(line, regex("Unsatisfiable."))
){
+ if(
line.find("Unsatisfiable.")== 0
){
return IS_UNSAT;
}
return IS_UNSAT;
}
- if(regex_match(line, regex(".*Element.*value=.*Element\\d+.*->\\d+.*"))){
+ if(line.find("univ") == 0){
+ continue;
+ }
+ if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
vector<string> values;
const char delim = ',';
tokenize(line, delim, values);
for (uint i=0; i<values.size(); i++){
vector<string> values;
const char delim = ',';
tokenize(line, delim, values);
for (uint i=0; i<values.size(); i++){
- uint i1, i2;
- uint64_t i3;
- if (3 == sscanf(values[i].c_str(),"%*[^0123456789]%d%*[^0123456789]%d%*[^0123456789]%" PRId64 "", &i1, &i2, &i3)){
- model_print("Element%d = %" PRId64 "\n", i1, i3);
+ uint i1, i2, i3;
+ if (3 == sscanf(values[i].c_str(),"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
+ model_print("Signature%u = %u\n", i1, i3);
sigEnc.setValue(i1, i3);
}
}
sigEnc.setValue(i1, i3);
}
}
@@
-147,24
+148,46
@@
string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){
string array[size];
for (uint i = 0; i < size; i++)
array[i] = encodeConstraint(bl->inputs.get(i));
string array[size];
for (uint i = 0; i < size; i++)
array[i] = encodeConstraint(bl->inputs.get(i));
+ string op;
+ switch (bl->op){
+ case SATC_OR:
+ op = " or ";
+ break;
+ case SATC_AND:
+ op = " and ";
+ break;
+ case SATC_NOT:
+ op = " not ";
+ break;
+ case SATC_IFF:
+ op = " iff ";
+ break;
+ case SATC_IMPLIES:
+ op = " implies ";
+ break;
+ case SATC_XOR:
+ default:
+ ASSERT(0);
+ }
switch (bl->op) {
switch (bl->op) {
+ case SATC_OR:
case SATC_AND:{
ASSERT(size >= 2);
case SATC_AND:{
ASSERT(size >= 2);
- string res = "";
+ string res = "
(
";
res += array[0];
for( uint i=1; i< size; i++){
res += array[0];
for( uint i=1; i< size; i++){
- res +=
" and "
+ array[i];
+ res +=
op
+ array[i];
}
}
+ res += " )";
return res;
}
case SATC_NOT:{
return res;
}
case SATC_NOT:{
- return "not
" + array[0]
;
+ return "not
( " + array[0] + " )"
;
}
}
+ case SATC_IMPLIES:
case SATC_IFF:
case SATC_IFF:
- return array[0] + " iff " + array[1];
- case SATC_OR:
+ return "( " + array[0] + op + array[1] + " )";
case SATC_XOR:
case SATC_XOR:
- case SATC_IMPLIES:
default:
ASSERT(0);
default:
ASSERT(0);
@@
-256,17
+279,10
@@
void AlloyEnc::writeToFile(string str){
}
bool AlloyEnc::getBooleanValue(Boolean *b){
}
bool AlloyEnc::getBooleanValue(Boolean *b){
- if (b->boolVal == BV_MUSTBETRUE)
- return true;
- else if (b->boolVal == BV_MUSTBEFALSE)
- return false;
- return sigEnc.getBooleanSignature(b);
+ return (bool)sigEnc.getValue(b);
}
uint64_t AlloyEnc::getValue(Element * element){
}
uint64_t AlloyEnc::getValue(Element * element){
- ElementEncoding *elemEnc = element->getElementEncoding();
- if (elemEnc->numVars == 0)//case when the set has only one item
- return element->getRange()->getElement(0);
- return sigEnc.getValue(element);
+ return (uint64_t)sigEnc.getValue(element);
}
}
diff --git
a/src/AlloyEnc/signature.cc
b/src/AlloyEnc/signature.cc
index 7201dc2a9a996155bb68b573314b2111ece598ed..ad7d2e700fe9b81bbf2f3268c5340e07718c66bf 100644
(file)
--- a/
src/AlloyEnc/signature.cc
+++ b/
src/AlloyEnc/signature.cc
@@
-5,15
+5,20
@@
bool BooleanSig::encodeAbs = true;
bool SetSig::encodeAbs = true;
bool ElementSig::encodeAbs = true;
bool SetSig::encodeAbs = true;
bool ElementSig::encodeAbs = true;
-BooleanSig::BooleanSig(uint id):
- Signature(id),
- value(-1)
+ValuedSignature::ValuedSignature(uint id):
+ Signature(id),
+ value(-1)
{
}
{
}
-
bool BooleanSig
::getValue(){
+
int ValuedSignature
::getValue(){
ASSERT(value != -1);
ASSERT(value != -1);
- return (bool) value;
+ return value;
+}
+
+BooleanSig::BooleanSig(uint id):
+ ValuedSignature(id)
+{
}
string BooleanSig::toString() const{
}
string BooleanSig::toString() const{
@@
-50,9
+55,8
@@
string BooleanSig::getAbsSignature() const{
}
ElementSig::ElementSig(uint id, SetSig *_ssig):
}
ElementSig::ElementSig(uint id, SetSig *_ssig):
- Signature(id),
- ssig(_ssig),
- value(0)
+ ValuedSignature(id),
+ ssig(_ssig)
{
}
{
}
diff --git
a/src/AlloyEnc/signature.h
b/src/AlloyEnc/signature.h
index e395ce3d35603ee0bab57ba0782c14bcf60b2f11..1b321a6f134590f8d7bbac8fbcece632119d9861 100644
(file)
--- a/
src/AlloyEnc/signature.h
+++ b/
src/AlloyEnc/signature.h
@@
-17,17
+17,23
@@
protected:
uint id;
};
uint id;
};
-class BooleanSig: public Signature{
+class ValuedSignature: public Signature{
+public:
+ ValuedSignature(uint id);
+ int getValue();
+ void setValue(int v){value = v;}
+protected:
+ int value;
+};
+
+class BooleanSig: public ValuedSignature{
public:
BooleanSig(uint id);
public:
BooleanSig(uint id);
- bool getValue();
- void setValue(bool v) {value = v; }
virtual ~BooleanSig(){}
virtual string toString() const;
virtual string getAbsSignature() const;
virtual string getSignature() const;
private:
virtual ~BooleanSig(){}
virtual string toString() const;
virtual string getAbsSignature() const;
virtual string getSignature() const;
private:
- int value;
static bool encodeAbs;
};
static bool encodeAbs;
};
@@
-43,18
+49,15
@@
private:
string domain;
};
string domain;
};
-class ElementSig: public Signature{
+class ElementSig: public
Valued
Signature{
public:
ElementSig(uint id, SetSig *ssig);
public:
ElementSig(uint id, SetSig *ssig);
- uint64_t getValue() { return value;}
- void setValue(uint64_t v){value = v;}
virtual ~ElementSig(){}
virtual string toString() const;
virtual string getAbsSignature() const;
virtual string getSignature() const;
private:
SetSig *ssig;
virtual ~ElementSig(){}
virtual string toString() const;
virtual string getAbsSignature() const;
virtual string getSignature() const;
private:
SetSig *ssig;
- uint64_t value;
static bool encodeAbs;
};
static bool encodeAbs;
};
diff --git
a/src/AlloyEnc/signatureenc.cc
b/src/AlloyEnc/signatureenc.cc
index 6971a5edcda4978f700531735ba3d81e934d5a35..92fb03fecd8af4e999ec52e9e48da5190325fbf4 100644
(file)
--- a/
src/AlloyEnc/signatureenc.cc
+++ b/
src/AlloyEnc/signatureenc.cc
@@
-34,7
+34,7
@@
void SignatureEnc::updateMaxValue(Set *set){
BooleanSig *SignatureEnc::getBooleanSignature(Boolean *bvar){
BooleanSig *bsig = (BooleanSig *)encoded.get((void *)bvar);
if(bsig == NULL){
BooleanSig *SignatureEnc::getBooleanSignature(Boolean *bvar){
BooleanSig *bsig = (BooleanSig *)encoded.get((void *)bvar);
if(bsig == NULL){
- bsig = new BooleanSig(
signatures.getSize
());
+ bsig = new BooleanSig(
getUniqueSigID
());
encoded.put(bvar, bsig);
signatures.push(bsig);
alloyEncoder->writeToFile(bsig->getSignature());
encoded.put(bvar, bsig);
signatures.push(bsig);
alloyEncoder->writeToFile(bsig->getSignature());
@@
-48,13
+48,13
@@
ElementSig *SignatureEnc::getElementSignature(Element *element){
Set *set = element->getRange();
SetSig *ssig = (SetSig *)encoded.get((void *)set);
if(ssig == NULL){
Set *set = element->getRange();
SetSig *ssig = (SetSig *)encoded.get((void *)set);
if(ssig == NULL){
- ssig = new SetSig(
signatures.getSize
(), set);
+ ssig = new SetSig(
getUniqueSigID
(), set);
encoded.put(set, ssig);
signatures.push(ssig);
alloyEncoder->writeToFile(ssig->getSignature());
updateMaxValue(set);
}
encoded.put(set, ssig);
signatures.push(ssig);
alloyEncoder->writeToFile(ssig->getSignature());
updateMaxValue(set);
}
- esig = new ElementSig(
signatures.getSize
(), ssig);
+ esig = new ElementSig(
getUniqueSigID
(), ssig);
encoded.put(element, esig);
signatures.push(esig);
alloyEncoder->writeToFile(esig->getSignature());
encoded.put(element, esig);
signatures.push(esig);
alloyEncoder->writeToFile(esig->getSignature());
@@
-63,16
+63,14
@@
ElementSig *SignatureEnc::getElementSignature(Element *element){
return esig;
}
return esig;
}
-void SignatureEnc::setValue(uint id, uint64_t value){
- ElementSig *sig = (ElementSig *)signatures.get(id);
+void SignatureEnc::setValue(uint id, uint value){
+ ValuedSignature *sig = getValuedSignature(id);
+ ASSERT(sig != NULL);
sig->setValue(value);
}
sig->setValue(value);
}
-
uint64_t SignatureEnc::getValue(Element *element
){
-
ElementSig *sig = (ElementSig *)encoded.get((void *) element
);
+
int SignatureEnc::getValue(void *astnode
){
+
ValuedSignature *sig = (ValuedSignature *)encoded.get(astnode
);
ASSERT(sig != NULL);
ASSERT(sig != NULL);
- model_print("******************\n");
- element->print();
- model_print("Value = %" PRId64 "\n", sig->getValue());
return sig->getValue();
}
return sig->getValue();
}
diff --git
a/src/AlloyEnc/signatureenc.h
b/src/AlloyEnc/signatureenc.h
index f1756df7913c061b84f9936485d05b60d4b97022..636c2b3e500a0cbf2feeb28c4f8e8d0621274bdd 100644
(file)
--- a/
src/AlloyEnc/signatureenc.h
+++ b/
src/AlloyEnc/signatureenc.h
@@
-9,12
+9,14
@@
class SignatureEnc {
public:
SignatureEnc(AlloyEnc *_alloyEncoder);
~SignatureEnc();
public:
SignatureEnc(AlloyEnc *_alloyEncoder);
~SignatureEnc();
- void setValue(uint id, uint
64_t
value);
+ void setValue(uint id, uint value);
ElementSig *getElementSignature(Element *element);
BooleanSig *getBooleanSignature(Boolean *bvar);
int getAlloyIntScope();
ElementSig *getElementSignature(Element *element);
BooleanSig *getBooleanSignature(Boolean *bvar);
int getAlloyIntScope();
-
uint64_t getValue(Element *element
);
+
int getValue(void *astnode
);
private:
private:
+ ValuedSignature *getValuedSignature(uint uniqueID){return (ValuedSignature*)signatures.get(uniqueID-1);}
+ uint getUniqueSigID(){return signatures.getSize() +1;}
void updateMaxValue(Set *set);
CloneMap encoded;
Vector<Signature*> signatures;
void updateMaxValue(Set *set);
CloneMap encoded;
Vector<Signature*> signatures;
diff --git
a/src/classlist.h
b/src/classlist.h
index 55ead2954e92ea34cbd6a30f4bd7f625f1748f27..d81b9bc9c6e683e8f45d8cc67df45f73dd392b45 100644
(file)
--- a/
src/classlist.h
+++ b/
src/classlist.h
@@
-74,6
+74,7
@@
class EncodingEdge;
class EncodingSubGraph;
class SignatureEnc;
class Signature;
class EncodingSubGraph;
class SignatureEnc;
class Signature;
+class ValuedSignature;
class ElementSig;
class SetSig;
class BooleanSig;
class ElementSig;
class SetSig;
class BooleanSig;