IntegerEncodingTransform::IntegerEncodingTransform(CSolver *_solver)
: Transform(_solver)
{
- orderIntEncoding = new HashTableOrderIntEncoding();
}
IntegerEncodingTransform::~IntegerEncodingTransform() {
- orderIntEncoding->resetanddelete();
}
void IntegerEncodingTransform::doTransform() {
}
void IntegerEncodingTransform::integerEncode(Order *currOrder) {
- IntegerEncodingRecord *encodingRecord = NULL;
- if (!orderIntEncoding->contains(currOrder)) {
- encodingRecord = new IntegerEncodingRecord(
- solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
- orderIntEncoding->put(currOrder, encodingRecord);
- currOrder->setOrderEncodingType( INTEGERENCODING );
- } else {
- encodingRecord = orderIntEncoding->get(currOrder);
- }
+ IntegerEncodingRecord *encodingRecord = new IntegerEncodingRecord(
+ solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
+ currOrder->setOrderEncodingType( INTEGERENCODING );
uint size = currOrder->constraints.getSize();
for (uint i = 0; i < size; i++) {
- orderIntegerEncodingSATEncoder(currOrder, currOrder->constraints.get(i));
+ orderIntegerEncodingSATEncoder(currOrder->constraints.get(i), encodingRecord);
}
currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
solver->getActiveOrders()->remove(currOrder);
}
-void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(Order * currOrder, BooleanOrder *boolOrder) {
- IntegerEncodingRecord *ierec = orderIntEncoding->get(currOrder);
+void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder, IntegerEncodingRecord *ierec) {
//getting two elements and using LT predicate ...
Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);
class IntegerEncodingTransform : public Transform {
public:
IntegerEncodingTransform(CSolver *solver);
- void orderIntegerEncodingSATEncoder(Order * currOrder, BooleanOrder *boolOrder);
+ void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder, IntegerEncodingRecord *ierec);
void doTransform();
void integerEncode(Order *currOrder);
virtual ~IntegerEncodingTransform();
private:
- //FIXME:We can remove it, because we don't need it for translating anymore... -HG
- HashTableOrderIntEncoding *orderIntEncoding;
};
IntegerEncodingRecord::IntegerEncodingRecord(Set *_set) :
secondarySet(_set)
{
- elementTable = new HashsetOrderElement();
+ elementSet = new HashsetOrderElement();
}
IntegerEncodingRecord::~IntegerEncodingRecord() {
- if (elementTable != NULL) {
- delete elementTable;
+ SetIteratorOrderElement *oiterator = elementSet->iterator();
+ while (oiterator->hasNext()) {
+ OrderElement *oe = oiterator->next();
+ delete oe;
}
+ delete oiterator;
+ delete elementSet;
}
Element *IntegerEncodingRecord::getOrderIntegerElement(CSolver *This, uint64_t item, bool create) {
OrderElement oelement(item, NULL);
- if ( elementTable->contains(&oelement)) {
- return elementTable->get(&oelement)->getElement();
+ if ( elementSet->contains(&oelement)) {
+ return elementSet->get(&oelement)->getElement();
} else if (create) {
Element *elem = This->getElementVar(secondarySet);
- elementTable->add(new OrderElement(item, elem));
+ elementSet->add(new OrderElement(item, elem));
return elem;
}
return NULL;
private:
Set *secondarySet;
- HashsetOrderElement *elementTable;
+ HashsetOrderElement *elementSet;
};
#endif/* INTEGERENCODINGRECORD_H */
#include "orderencoding.h"
+#include "orderresolver.h"
OrderEncoding::OrderEncoding(Order *_order) :
+ resolver(NULL),
type(ORDER_UNASSIGNED),
- order(_order) {
+ order(_order)
+{
+}
+
+OrderEncoding::~OrderEncoding(){
+ if(resolver!= NULL){
+ delete resolver;
+ }
}
class OrderEncoding {
public:
OrderEncoding(Order *order);
-
+ virtual ~OrderEncoding();
OrderResolver *resolver;
OrderEncodingType type;
Order *order;
}
IntegerEncOrderResolver::~IntegerEncOrderResolver() {
+ delete ierecord;
}
long long startTime = getTimeNano();
computePolarities(this);
-// DecomposeOrderTransform dot(this);
-// dot.doTransform();
+ DecomposeOrderTransform dot(this);
+ dot.doTransform();
IntegerEncodingTransform iet(this);
iet.doTransform();