My changes
authorbdemsky <bdemsky@uci.edu>
Tue, 24 Oct 2017 19:31:32 +0000 (12:31 -0700)
committerbdemsky <bdemsky@uci.edu>
Tue, 24 Oct 2017 19:31:32 +0000 (12:31 -0700)
src/AST/asthash.cc
src/AST/rewriter.cc
src/ASTAnalyses/Order/orderanalysis.cc
src/ASTAnalyses/Order/orderanalysis.h
src/Collections/hashtable.h
src/Collections/structs.cc
src/config.h
src/csolver.cc
src/csolver.h
src/mymemory.h

index bc58431..7350a7e 100644 (file)
@@ -4,6 +4,9 @@
 #include "boolean.h"
 #include "element.h"
 
+#define HASHNEXT(hash, newval) {hash+=newval; hash += hash << 10; hash ^= hash >>6;}
+#define HASHFINAL(hash) {hash += hash <<3; hash ^= hash >> 11; hash += hash << 15;}
+
 bool compareArray(Array<BooleanEdge> *inputs1, Array<BooleanEdge> *inputs2) {
        if (inputs1->getSize() != inputs2->getSize())
                return false;
@@ -25,22 +28,22 @@ bool compareArray(Array<Element *> *inputs1, Array<Element *> *inputs2) {
 }
 
 uint hashArray(Array<BooleanEdge> *inputs) {
-       uint hash = inputs->getSize();
+       uint hash = 0;
        for (uint i = 0; i < inputs->getSize(); i++) {
                uint newval = (uint)(uintptr_t) inputs->get(i).getRaw();
-               hash ^= newval;
-               hash = (hash << 3) | (hash >> 29);
+               HASHNEXT(hash, newval);
        }
+       HASHFINAL(hash);
        return hash;
 }
 
 uint hashArray(Array<Element *> *inputs) {
-       uint hash = inputs->getSize();
+       uint hash = 0;
        for (uint i = 0; i < inputs->getSize(); i++) {
                uint newval = (uint)(uintptr_t) inputs->get(i);
-               hash ^= newval;
-               hash = (hash << 3) | (hash >> 29);
+               HASHNEXT(hash, newval);
        }
+       HASHFINAL(hash);
        return hash;
 }
 
@@ -48,20 +51,29 @@ uint hashBoolean(Boolean *b) {
        switch (b->type) {
        case ORDERCONST: {
                BooleanOrder *o = (BooleanOrder *)b;
-               return ((uint)(uintptr_t) o->order) ^ ((uint) o->first) ^ (((uint)(o->second)) << 2);
+               uint hash = 0;
+               HASHNEXT(hash, (uint) o->first);
+               HASHNEXT(hash, (uint) o->second);
+               HASHNEXT(hash, (((uint)(uintptr_t) o->order) & 0xffff));
+               HASHFINAL(hash);
+               return hash;
        }
+
        case BOOLEANVAR: {
                return (uint)(uintptr_t) b;
        }
        case LOGICOP: {
                BooleanLogic *l = (BooleanLogic *)b;
-               return ((uint)l->op) ^ hashArray(&l->inputs);
+               return ((uint)l->op) + 43* hashArray(&l->inputs);
        }
        case PREDICATEOP: {
                BooleanPredicate *p = (BooleanPredicate *)b;
-               return ((uint)(uintptr_t) p->predicate) ^
-                                        (((uint)(uintptr_t) p->undefStatus) << 1) ^
-                                        hashArray(&p->inputs);
+               uint hash = 0;
+               HASHNEXT(hash, hashArray(&p->inputs));
+               HASHNEXT(hash, (uint)(uintptr_t) p->predicate);
+               HASHNEXT(hash, (uint)(uintptr_t) p->undefStatus);
+               HASHFINAL(hash);
+               return hash;
        }
        default:
                ASSERT(0);
@@ -104,9 +116,12 @@ uint hashElement(Element *e) {
        }
        case ELEMFUNCRETURN: {
                ElementFunction *ef = (ElementFunction *) e;
-               return ((uint)(uintptr_t) ef->getFunction()) ^
-                                        ((uint)(uintptr_t) ef->overflowstatus) ^
-                                        hashArray(&ef->inputs);
+               uint hash = 0;
+               HASHNEXT(hash, hashArray (&ef->inputs));
+               HASHNEXT(hash, (uint)(uintptr_t) ef->getFunction());
+               HASHNEXT(hash, (uint)(uintptr_t) ef->overflowstatus);
+               HASHFINAL(hash);
+               return hash;
        }
        case ELEMCONST: {
                ElementConst *ec = (ElementConst *) e;
index 2c946d5..804d9de 100644 (file)
@@ -15,6 +15,10 @@ void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
        replaceBooleanWithTrueNoRemove(bexpr);
 }
 
+void CSolver::replaceBooleanWithFalseNoRemove(BooleanEdge bexpr) {
+       replaceBooleanWithTrueNoRemove(bexpr.negate());
+}
+
 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
        updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
 
index c8c7e36..7e3e030 100644 (file)
 #include "mutableset.h"
 #include "tunable.h"
 
-void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
+/** Returns a table that maps a node to the set of nodes that can reach the node. */
+HashtableNodeToNodeSet * getMustReachMap(CSolver  *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
        uint size = finishNodes->getSize();
        HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
-
+       
        for (int i = size - 1; i >= 0; i--) {
                OrderNode *node = finishNodes->get(i);
                HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
                table->put(node, sources);
-
+               
                {
                        //Compute source sets
                        SetIteratorOrderEdge *iterator = node->inEdges.iterator();
@@ -34,13 +35,22 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                        }
                        delete iterator;
                }
+       }
+       return table;
+}
+
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet * table, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
+       uint size = finishNodes->getSize();
+
+       for (int i = size - 1; i >= 0; i--) {
+               OrderNode *node = finishNodes->get(i);
+               HashsetOrderNode *sources = table->get(node);
+               
                if (computeTransitiveClosure) {
                        //Compute full transitive closure for nodes
                        SetIteratorOrderNode *srciterator = sources->iterator();
                        while (srciterator->hasNext()) {
                                OrderNode *srcnode = srciterator->next();
-                               if (srcnode->removed)
-                                       continue;
                                OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
                                newedge->mustPos = true;
                                newedge->polPos = true;
@@ -83,9 +93,6 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                        delete iterator;
                }
        }
-
-       table->resetAndDeleteVals();
-       delete table;
 }
 
 /* This function finds edges that would form a cycle with must edges
@@ -98,9 +105,11 @@ void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiv
        //Topologically sort the mustPos edge graph
        graph->DFSMust(&finishNodes);
        graph->resetNodeInfoStatusSCC();
-
+       HashtableNodeToNodeSet * table=getMustReachMap(solver, graph, & finishNodes);
        //Find any backwards edges that complete cycles and force them to be mustNeg
-       DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
+       DFSClearContradictions(solver, graph, table, &finishNodes, computeTransitiveClosure);
+       table->resetAndDeleteVals();
+       delete table;
 }
 
 /* This function finds edges that must be positive and forces the
index 24ec85c..a371c85 100644 (file)
@@ -4,7 +4,9 @@
 #include "structs.h"
 #include "mymemory.h"
 
-void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet * table, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
+HashtableNodeToNodeSet * getMustReachMap(CSolver  *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes);
+
 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph);
index 218fb2d..9f5f3b3 100644 (file)
@@ -30,6 +30,7 @@ template<typename _Key, typename _Val>
 struct Hashlistnode {
        _Key key;
        _Val val;
+       uint hashcode;
 };
 
 template<typename _Key, int _Shift, typename _KeyInt>
@@ -206,7 +207,8 @@ public:
 
                struct Hashlistnode<_Key, _Val> *search;
 
-               unsigned int index = hash_function(key);
+               unsigned int hashcode = hash_function(key);
+               unsigned int index = hashcode;
                do {
                        index &= capacitymask;
                        search = &table[index];
@@ -214,15 +216,17 @@ public:
                                //key is null, probably done
                                break;
                        }
-                       if (equals(search->key, key)) {
-                               search->val = val;
-                               return;
-                       }
+                       if (search->hashcode == hashcode)
+                               if (equals(search->key, key)) {
+                                       search->val = val;
+                                       return;
+                               }
                        index++;
                } while (true);
 
                search->key = key;
                search->val = val;
+               search->hashcode = hashcode;
                size++;
        }
 
@@ -242,7 +246,8 @@ public:
                                return (_Val) 0;
                }
 
-               unsigned int oindex = hash_function(key) & capacitymask;
+               unsigned int hashcode = hash_function(key);
+               unsigned int oindex = hashcode & capacitymask;
                unsigned int index = oindex;
                do {
                        search = &table[index];
@@ -250,8 +255,9 @@ public:
                                if (!search->val)
                                        break;
                        } else
-                       if (equals(search->key, key))
-                               return search->val;
+                               if (hashcode == search->hashcode)
+                                       if (equals(search->key, key))
+                                               return search->val;
                        index++;
                        index &= capacitymask;
                        if (index == oindex)
@@ -282,7 +288,8 @@ public:
                }
 
 
-               unsigned int index = hash_function(key);
+               unsigned int hashcode = hash_function(key);
+               unsigned int index = hashcode;
                do {
                        index &= capacitymask;
                        search = &table[index];
@@ -290,14 +297,15 @@ public:
                                if (!search->val)
                                        break;
                        } else
-                       if (equals(search->key, key)) {
-                               _Val v = search->val;
-                               //empty out this bin
-                               search->val = (_Val) 1;
-                               search->key = 0;
-                               size--;
-                               return v;
-                       }
+                               if (hashcode == search->hashcode)
+                                       if (equals(search->key, key)) {
+                                               _Val v = search->val;
+                                               //empty out this bin
+                                               search->val = (_Val) 1;
+                                               search->key = 0;
+                                               size--;
+                                               return v;
+                                       }
                        index++;
                } while (true);
                return (_Val)0;
@@ -322,6 +330,7 @@ public:
                }
 
                unsigned int index = hash_function(key);
+               unsigned int hashcode = index;
                do {
                        index &= capacitymask;
                        search = &table[index];
@@ -329,8 +338,9 @@ public:
                                if (!search->val)
                                        break;
                        } else
-                       if (equals(search->key, key))
-                               return true;
+                               if (hashcode == search->hashcode)
+                                       if (equals(search->key, key))
+                                               return true;
                        index++;
                } while (true);
                return false;
@@ -365,13 +375,15 @@ public:
                        if (!key)
                                continue;
 
-                       unsigned int index = hash_function(key);
+                       unsigned int hashcode = bin->hashcode;
+                       unsigned int index = hashcode;
                        do {
                                index &= capacitymask;
                                search = &table[index];
                                index++;
                        } while (search->key);
 
+                       search->hashcode = hashcode;
                        search->key = key;
                        search->val = bin->val;
                }
index 2001242..4e2827c 100644 (file)
@@ -8,12 +8,15 @@
 #include "structs.h"
 #include "decomposeorderresolver.h"
 
+#define HASHNEXT(hash, newval) {hash+=newval; hash += hash << 10; hash ^= hash >>6;}
+#define HASHFINAL(hash) {hash += hash <<3; hash ^= hash >> 11; hash += hash << 15;}
+
 unsigned int table_entry_hash_function(TableEntry *This) {
        unsigned int h = 0;
        for (uint i = 0; i < This->inputSize; i++) {
-               h += This->inputs[i];
-               h *= 31;
+               HASHNEXT(h, This->inputs[i]);
        }
+       HASHFINAL(h);
        return h;
 }
 
@@ -35,7 +38,11 @@ bool order_node_equals(OrderNode *key1, OrderNode *key2) {
 }
 
 unsigned int order_edge_hash_function(OrderEdge *This) {
-       return (uint) (((uintptr_t)This->sink) ^ ((uintptr_t)This->source << 4));
+       uint hash=0;
+       HASHNEXT(hash, (uint)(uintptr_t) This->sink);
+       HASHNEXT(hash, (uint)(uintptr_t) This->source);
+       HASHFINAL(hash);
+       return hash;
 }
 
 bool order_edge_equals(OrderEdge *key1, OrderEdge *key2) {
@@ -51,7 +58,11 @@ bool order_element_equals(OrderElement *key1, OrderElement *key2) {
 }
 
 unsigned int order_pair_hash_function(OrderPair *This) {
-       return (uint) (This->first << 2) ^ This->second;
+       uint hash=0;
+       HASHNEXT(hash, This->first);
+       HASHNEXT(hash, This->second);
+       HASHFINAL(hash);
+       return hash;
 }
 
 bool order_pair_equals(OrderPair *key1, OrderPair *key2) {
@@ -59,7 +70,11 @@ bool order_pair_equals(OrderPair *key1, OrderPair *key2) {
 }
 
 unsigned int doredge_hash_function(DOREdge *key) {
-       return (uint) (key->newfirst << 2) ^ key->newsecond;
+       uint hash=0;
+       HASHNEXT(hash, (uint) key->newfirst);
+       HASHNEXT(hash, (uint) key->newsecond);
+       HASHFINAL(hash);
+       return hash;
 }
 
 bool doredge_equals(DOREdge *key1, DOREdge *key2) {
index 0c73cae..2e48668 100644 (file)
  * @brief Configuration file.
  */
 
-#ifndef CONFIG_H
-#define CONFIG_H
+#ifndef SATC_CONFIG_H
+#define SATC_CONFIG_H
 
 /** Turn on debugging. */
 #ifndef CONFIG_DEBUG
 //#define CONFIG_DEBUG
-#define TRACE_DEBUG
 #endif
 
 //#define SATCHECK_CONFIG
index 533fc4b..fb29cff 100644 (file)
@@ -22,6 +22,9 @@
 #include "serializer.h"
 #include "deserializer.h"
 #include "encodinggraph.h"
+#include "ordergraph.h"
+#include "orderedge.h"
+#include "orderanalysis.h"
 #include <time.h>
 
 CSolver::CSolver() :
@@ -408,6 +411,26 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
                allBooleans.push(constraint);
                boolMap.put(constraint, constraint);
                constraint->updateParents();
+               if (order->graph != NULL) {
+                       OrderGraph *graph=order->graph;
+                       OrderNode *from=graph->lookupOrderNodeFromOrderGraph(first);
+                       if (from != NULL) {
+                               OrderNode *to=graph->lookupOrderNodeFromOrderGraph(second);
+                               if (to != NULL) {
+                                       OrderEdge *edge=graph->lookupOrderEdgeFromOrderGraph(from, to);
+                                       OrderEdge *invedge;
+
+                                       if (edge != NULL && edge->mustPos) {
+                                               replaceBooleanWithTrueNoRemove(constraint);
+                                       } else if (edge != NULL && edge->mustNeg) {
+                                               replaceBooleanWithFalseNoRemove(constraint);
+                                       } else if ((invedge=graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
+                                                                                && invedge->mustPos) {
+                                               replaceBooleanWithFalseNoRemove(constraint);
+                                       }
+                               }
+                       }
+               }
        } else {
                delete constraint;
                constraint = b;
@@ -459,14 +482,45 @@ Order *CSolver::createOrder(OrderType type, Set *set) {
        return order;
 }
 
+/** Computes static ordering information to allow isTrue/isFalse
+               queries on newly created orders to work. */
+
+void CSolver::inferFixedOrder(Order *order) {
+       if (order->graph != NULL) {
+               delete order->graph;
+       }
+       order->graph = buildMustOrderGraph(order);
+       reachMustAnalysis(this, order->graph, true);
+}
+       
+void CSolver::inferFixedOrders() {
+       SetIteratorOrder *orderit = activeOrders.iterator();
+       while (orderit->hasNext()) {
+               Order *order = orderit->next();
+               inferFixedOrder(order);
+       }
+}
+
 int CSolver::solve() {
        bool deleteTuner = false;
        if (tuner == NULL) {
                tuner = new DefaultTuner();
                deleteTuner = true;
        }
+
+
+       {
+               SetIteratorOrder *orderit = activeOrders.iterator();
+               while (orderit->hasNext()) {
+                       Order *order = orderit->next();
+                       if (order->graph != NULL) {
+                               delete order->graph;
+                               order->graph = NULL;
+                       }
+               }
+               delete orderit;
+       }
        
-       long long startTime = getTimeNano();
        computePolarities(this);
 
        Preprocess pp(this);
@@ -481,8 +535,10 @@ int CSolver::solve() {
        EncodingGraph eg(this);
        eg.buildGraph();
        eg.encode();
-//     printConstraints();
+
        naiveEncodingDecision(this);
+
+       long long startTime = getTimeNano();
        satEncoder->encodeAllSATEncoder(this);
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
        int result = unsat ? IS_UNSAT : satEncoder->solve();
index 16396f9..bac1a49 100644 (file)
@@ -148,13 +148,17 @@ public:
 
        void replaceBooleanWithTrue(BooleanEdge bexpr);
        void replaceBooleanWithTrueNoRemove(BooleanEdge bexpr);
+       void replaceBooleanWithFalseNoRemove(BooleanEdge bexpr);
        void replaceBooleanWithFalse(BooleanEdge bexpr);
        void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
        CSolver *clone();
        void serialize();
        static CSolver* deserialize(const char * file);
        void autoTune(uint budget);
+       void inferFixedOrders();
+       void inferFixedOrder(Order *order);
 
+       
        void setTuner(Tuner *_tuner) { tuner = _tuner; }
        long long getElapsedTime() { return elapsedTime; }
        long long getEncodeTime();
index 700fb4f..0798860 100644 (file)
@@ -19,6 +19,8 @@
 
 #include "config.h"
 
+//#define SATCHECK_CONFIG
+
 /*
    void * ourmalloc(size_t size);
    void ourfree(void *ptr);