From 04b29ee98bb1e665842f1cf1513b5a48f2b8c9c5 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Sat, 2 Sep 2017 00:00:52 -0700
Subject: [PATCH] Make integerencoding a completely separate pass... Fix issue
of changing ordersets
---
src/ASTTransform/decomposeordertransform.cc | 12 ++++++++----
src/ASTTransform/decomposeordertransform.h | 2 --
src/ASTTransform/integerencoding.cc | 15 +++++++++------
src/ASTTransform/integerencoding.h | 3 +--
src/Collections/corestructs.h | 2 ++
src/csolver.cc | 1 +
src/csolver.h | 3 +++
7 files changed, 24 insertions(+), 14 deletions(-)
diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index ec8b020..85b43b1 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -27,10 +27,10 @@ DecomposeOrderTransform::~DecomposeOrderTransform() {
}
void DecomposeOrderTransform::doTransform() {
- Vector<Order *> *orders = solver->getOrders();
- uint size = orders->getSize();
- for (uint i = 0; i < size; i++) {
- Order *order = orders->get(i);
+ HashsetOrder *orders = solver->getActiveOrders()->copy();
+ SetIteratorOrder * orderit=orders->iterator();
+ while(orderit->hasNext()) {
+ Order *order = orderit->next();
if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
continue;
@@ -70,8 +70,11 @@ void DecomposeOrderTransform::doTransform() {
decomposeOrder(order, graph);
delete graph;
}
+ delete orderit;
+ delete orders;
}
+
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) );
+ solver->getActiveOrders()->remove(currOrder);
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 69f7a1f..1a2865c 100644
--- a/src/ASTTransform/decomposeordertransform.h
+++ b/src/ASTTransform/decomposeordertransform.h
@@ -20,8 +20,6 @@ public:
CMEMALLOC;
private:
- Order *currOrder;
- OrderGraph *currGraph;
};
#endif/* ORDERTRANSFORM_H */
diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index d8150b3..6664a67 100644
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -18,13 +18,15 @@ IntegerEncodingTransform::~IntegerEncodingTransform() {
}
void IntegerEncodingTransform::doTransform() {
- Vector<Order *> *orders = solver->getOrders();
- uint size = orders->getSize();
- for (uint i = 0; i < size; i++) {
- Order *order = orders->get(i);
+ HashsetOrder *orders = solver->getActiveOrders()->copy();
+ SetIteratorOrder * orderit=orders->iterator();
+ while(orderit->hasNext()) {
+ Order *order = orderit->next();
if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
integerEncode(order);
}
+ delete orders;
+ delete orderit;
}
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++) {
- orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
+ orderIntegerEncodingSATEncoder(currOrder, currOrder->constraints.get(i));
}
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);
diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h
index f051a41..8066c2a 100644
--- a/src/ASTTransform/integerencoding.h
+++ b/src/ASTTransform/integerencoding.h
@@ -14,13 +14,12 @@
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:
- Order *currOrder;
//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 1e808cb..982e0c5 100644
--- a/src/Collections/corestructs.h
+++ b/src/Collections/corestructs.h
@@ -5,6 +5,8 @@
#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<Order *, uintptr_t, 4> SetIteratorOrder;
#endif
diff --git a/src/csolver.cc b/src/csolver.cc
index de9543e..b351914 100644
--- 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);
+ activeOrders.add(order);
return order;
}
diff --git a/src/csolver.h b/src/csolver.h
index 1ff4cd1..7e8bbad 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -125,6 +125,7 @@ public:
bool isUnSAT() { return unsat; }
Vector<Order *> *getOrders() { return &allOrders;}
+ HashsetOrder * getActiveOrders() { return &activeOrders;}
Tuner *getTuner() { return tuner; }
@@ -173,6 +174,8 @@ private:
/** 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;
--
2.34.1