Add timing statements

[satune.git] / src / AST / order.cc

diff --git a/src/AST/order.cc b/src/AST/order.cc
index 5d9fc4ebb1a9558371c6dc3cc3de2f531da1b3d8..f3ccde419dc9e07957a62229a913c855aca7fdd8 100644 (file)
--- a/src/AST/order.cc
+++ b/src/AST/order.cc
@@ -3,37 +3,64 @@
 #include "set.h"
 #include "boolean.h"
 #include "ordergraph.h"
+#include "csolver.h"
+#include "orderpairresolver.h"
 
-Order::Order(OrderType _type, Set *_set) : type(_type), set(_set), orderPairTable(NULL), elementTable(NULL), graph(NULL) {
-       initOrderEncoding(&order, this);
+Order::Order(OrderType _type, Set *_set) :
+       type(_type),
+       set(_set),
+       graph(NULL),
+       encoding(this)
+{
 }
 
-void Order::initializeOrderHashTable() {
-       orderPairTable = new HashTableOrderPair();
+void Order::addOrderConstraint(BooleanOrder *constraint) {
+       constraints.push(constraint);
 }
 
-void Order::initializeOrderElementsHashTable() {
-       elementTable = new HashSetOrderElement();
+void Order::setOrderEncodingType(OrderEncodingType type) {
+       encoding.type = type;
 }
 
-void Order::addOrderConstraint(BooleanOrder *constraint) {
-       constraints.push(constraint);
+Order *Order::clone(CSolver *solver, CloneMap *map) {
+       Order *o = (Order *)map->get(this);
+       if (o != NULL)
+               return o;
+       o = solver->createOrder(type, set->clone(solver, map));
+       map->put(this, o);
+       return o;
 }
 
-void Order::setOrderEncodingType(OrderEncodingType type) {
-       order.type = type;
+HashtableOrderPair *Order::getOrderPairTable() {
+       ASSERT( encoding.resolver != NULL);
+       if (OrderPairResolver *t = dynamic_cast<OrderPairResolver *>(encoding.resolver)) {
+               return t->getOrderPairTable();
+       } else {
+               ASSERT(0);
+       }
 }
 
 Order::~Order() {
-       deleteOrderEncoding(&order);
-       if (orderPairTable != NULL) {
-               orderPairTable->resetanddelete();
-               delete orderPairTable;
-       }
-       if (elementTable != NULL) {
-               delete elementTable;
-       }
        if (graph != NULL) {
-               deleteOrderGraph(graph);
+               delete graph;
        }
 }
+
+void Order::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
+               return;
+       serializer->addObject(this);
+       set->serialize(serializer);
+       ASTNodeType asttype = ORDERTYPE;
+       serializer->mywrite(&asttype, sizeof(ASTNodeType));
+       Order *This = this;
+       serializer->mywrite(&This, sizeof(Order *));
+       serializer->mywrite(&type, sizeof(OrderType));
+       serializer->mywrite(&set, sizeof(Set *));
+}
+
+void Order::print() {
+       model_print("{Order on Set:\n");
+       set->print();
+       model_print("}\n");
+}