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:
d46ee65
)
Make integerencoding a completely separate pass... Fix issue of changing ordersets
author
bdemsky
<bdemsky@uci.edu>
Sat, 2 Sep 2017 07:00:52 +0000
(
00:00
-0700)
committer
bdemsky
<bdemsky@uci.edu>
Sat, 2 Sep 2017 07:00:52 +0000
(
00:00
-0700)
src/ASTTransform/decomposeordertransform.cc
patch
|
blob
|
history
src/ASTTransform/decomposeordertransform.h
patch
|
blob
|
history
src/ASTTransform/integerencoding.cc
patch
|
blob
|
history
src/ASTTransform/integerencoding.h
patch
|
blob
|
history
src/Collections/corestructs.h
patch
|
blob
|
history
src/csolver.cc
patch
|
blob
|
history
src/csolver.h
patch
|
blob
|
history
diff --git
a/src/ASTTransform/decomposeordertransform.cc
b/src/ASTTransform/decomposeordertransform.cc
index ec8b0204c3360a3b53980a9a5e0fa97f1507dfba..85b43b12e1d063d9cdcf98e516fb21de1abbf177 100644
(file)
--- a/
src/ASTTransform/decomposeordertransform.cc
+++ b/
src/ASTTransform/decomposeordertransform.cc
@@
-27,10
+27,10
@@
DecomposeOrderTransform::~DecomposeOrderTransform() {
}
void DecomposeOrderTransform::doTransform() {
}
void DecomposeOrderTransform::doTransform() {
-
Vector<Order *> *orders = solver->getOrders
();
-
uint size = orders->getSize
();
-
for (uint i = 0; i < size; i++
) {
- Order *order = order
s->get(i
);
+
HashsetOrder *orders = solver->getActiveOrders()->copy
();
+
SetIteratorOrder * orderit=orders->iterator
();
+
while(orderit->hasNext()
) {
+ Order *order = order
it->next(
);
if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
continue;
if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
continue;
@@
-70,8
+70,11
@@
void DecomposeOrderTransform::doTransform() {
decomposeOrder(order, graph);
delete graph;
}
decomposeOrder(order, graph);
delete graph;
}
+ delete orderit;
+ delete orders;
}
}
+
void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) {
Vector<Order *> ordervec;
Vector<Order *> partialcandidatevec;
void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) {
Vector<Order *> ordervec;
Vector<Order *> partialcandidatevec;
@@
-122,6
+125,7
@@
void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
}
}
currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
}
}
currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
+ solver->getActiveOrders()->remove(currOrder);
uint pcvsize = partialcandidatevec.getSize();
for (uint i = 0; i < pcvsize; i++) {
Order *neworder = partialcandidatevec.get(i);
uint pcvsize = partialcandidatevec.getSize();
for (uint i = 0; i < pcvsize; i++) {
Order *neworder = partialcandidatevec.get(i);
diff --git
a/src/ASTTransform/decomposeordertransform.h
b/src/ASTTransform/decomposeordertransform.h
index 69f7a1f2cadbab75d8d84c8f0c390d5347bcebb3..1a2865cef6f64033752be24696005db51d4091d5 100644
(file)
--- a/
src/ASTTransform/decomposeordertransform.h
+++ b/
src/ASTTransform/decomposeordertransform.h
@@
-20,8
+20,6
@@
public:
CMEMALLOC;
private:
CMEMALLOC;
private:
- Order *currOrder;
- OrderGraph *currGraph;
};
#endif/* ORDERTRANSFORM_H */
};
#endif/* ORDERTRANSFORM_H */
diff --git
a/src/ASTTransform/integerencoding.cc
b/src/ASTTransform/integerencoding.cc
index d8150b311d633a34f3aeb932caedfda8136851ab..6664a677f2b10664e7e11ab894f8f98287e807e4 100644
(file)
--- a/
src/ASTTransform/integerencoding.cc
+++ b/
src/ASTTransform/integerencoding.cc
@@
-18,13
+18,15
@@
IntegerEncodingTransform::~IntegerEncodingTransform() {
}
void IntegerEncodingTransform::doTransform() {
}
void IntegerEncodingTransform::doTransform() {
-
Vector<Order *> *orders = solver->getOrders
();
-
uint size = orders->getSize
();
-
for (uint i = 0; i < size; i++
) {
- Order *order = order
s->get(i
);
+
HashsetOrder *orders = solver->getActiveOrders()->copy
();
+
SetIteratorOrder * orderit=orders->iterator
();
+
while(orderit->hasNext()
) {
+ Order *order = order
it->next(
);
if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
integerEncode(order);
}
if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
integerEncode(order);
}
+ delete orders;
+ delete orderit;
}
void IntegerEncodingTransform::integerEncode(Order *currOrder) {
}
void IntegerEncodingTransform::integerEncode(Order *currOrder) {
@@
-38,13
+40,14
@@
void IntegerEncodingTransform::integerEncode(Order *currOrder) {
}
uint size = currOrder->constraints.getSize();
for (uint i = 0; i < size; i++) {
}
uint size = currOrder->constraints.getSize();
for (uint i = 0; i < size; i++) {
- orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
+ orderIntegerEncodingSATEncoder(currOrder
, currOrder
->constraints.get(i));
}
currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
}
currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
+ solver->getActiveOrders()->remove(currOrder);
}
}
-void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
+void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(
Order * currOrder,
BooleanOrder *boolOrder) {
IntegerEncodingRecord *ierec = orderIntEncoding->get(currOrder);
//getting two elements and using LT predicate ...
Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
IntegerEncodingRecord *ierec = orderIntEncoding->get(currOrder);
//getting two elements and using LT predicate ...
Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
diff --git
a/src/ASTTransform/integerencoding.h
b/src/ASTTransform/integerencoding.h
index f051a41d17c66ad698f37142ff4581d91782ed20..8066c2acf678924b7b7ffb8fe3306cc6b0f9ca10 100644
(file)
--- a/
src/ASTTransform/integerencoding.h
+++ b/
src/ASTTransform/integerencoding.h
@@
-14,13
+14,12
@@
class IntegerEncodingTransform : public Transform {
public:
IntegerEncodingTransform(CSolver *solver);
class IntegerEncodingTransform : public Transform {
public:
IntegerEncodingTransform(CSolver *solver);
- void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder);
+ void orderIntegerEncodingSATEncoder(
Order * currOrder,
BooleanOrder *boolOrder);
void doTransform();
void integerEncode(Order *currOrder);
virtual ~IntegerEncodingTransform();
private:
void doTransform();
void integerEncode(Order *currOrder);
virtual ~IntegerEncodingTransform();
private:
- Order *currOrder;
//FIXME:We can remove it, because we don't need it for translating anymore... -HG
HashTableOrderIntEncoding *orderIntEncoding;
};
//FIXME:We can remove it, because we don't need it for translating anymore... -HG
HashTableOrderIntEncoding *orderIntEncoding;
};
diff --git
a/src/Collections/corestructs.h
b/src/Collections/corestructs.h
index 1e808cb6166b63052a75dd2211f099d987f19717..982e0c5cfed2d397e95a3f1f8bdf486aedfcd8e8 100644
(file)
--- a/
src/Collections/corestructs.h
+++ b/
src/Collections/corestructs.h
@@
-5,6
+5,8
@@
#include "hashset.h"
typedef Hashset<Boolean *, uintptr_t, 4> HashsetBoolean;
#include "hashset.h"
typedef Hashset<Boolean *, uintptr_t, 4> HashsetBoolean;
+typedef Hashset<Order *, uintptr_t, 4> HashsetOrder;
typedef SetIterator<Boolean *, uintptr_t, 4> SetIteratorBoolean;
typedef SetIterator<Boolean *, uintptr_t, 4> SetIteratorBoolean;
+typedef SetIterator<Order *, uintptr_t, 4> SetIteratorOrder;
#endif
#endif
diff --git
a/src/csolver.cc
b/src/csolver.cc
index de9543edc3482fe5e6f99afd577fbefc9e19748f..b351914cd2b0fbe81faa68149bd993a6056e6833 100644
(file)
--- a/
src/csolver.cc
+++ b/
src/csolver.cc
@@
-383,6
+383,7
@@
void CSolver::addConstraint(Boolean *constraint) {
Order *CSolver::createOrder(OrderType type, Set *set) {
Order *order = new Order(type, set);
allOrders.push(order);
Order *CSolver::createOrder(OrderType type, Set *set) {
Order *order = new Order(type, set);
allOrders.push(order);
+ activeOrders.add(order);
return order;
}
return order;
}
diff --git
a/src/csolver.h
b/src/csolver.h
index 1ff4cd113ef317860f116a74b45d291687e1dbae..7e8bbad871019bcc59f06d5e170de317fc2cae02 100644
(file)
--- a/
src/csolver.h
+++ b/
src/csolver.h
@@
-125,6
+125,7
@@
public:
bool isUnSAT() { return unsat; }
Vector<Order *> *getOrders() { return &allOrders;}
bool isUnSAT() { return unsat; }
Vector<Order *> *getOrders() { return &allOrders;}
+ HashsetOrder * getActiveOrders() { return &activeOrders;}
Tuner *getTuner() { return tuner; }
Tuner *getTuner() { return tuner; }
@@
-173,6
+174,8
@@
private:
/** This is a vector of all order structs that we have allocated. */
Vector<Order *> allOrders;
/** This is a vector of all order structs that we have allocated. */
Vector<Order *> allOrders;
+ HashsetOrder activeOrders;
+
/** This is a vector of all function structs that we have allocated. */
Vector<Function *> allFunctions;
/** This is a vector of all function structs that we have allocated. */
Vector<Function *> allFunctions;