From: bdemsky Date: Tue, 24 Oct 2017 19:31:32 +0000 (-0700) Subject: My changes X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=7fbe24c7815dd1b756c65174d33d7e3d8cc1d892 My changes --- diff --git a/src/AST/asthash.cc b/src/AST/asthash.cc index bc58431..7350a7e 100644 --- a/src/AST/asthash.cc +++ b/src/AST/asthash.cc @@ -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 *inputs1, Array *inputs2) { if (inputs1->getSize() != inputs2->getSize()) return false; @@ -25,22 +28,22 @@ bool compareArray(Array *inputs1, Array *inputs2) { } uint hashArray(Array *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 *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; diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index 2c946d5..804d9de 100644 --- a/src/AST/rewriter.cc +++ b/src/AST/rewriter.cc @@ -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); diff --git a/src/ASTAnalyses/Order/orderanalysis.cc b/src/ASTAnalyses/Order/orderanalysis.cc index c8c7e36..7e3e030 100644 --- a/src/ASTAnalyses/Order/orderanalysis.cc +++ b/src/ASTAnalyses/Order/orderanalysis.cc @@ -11,15 +11,16 @@ #include "mutableset.h" #include "tunable.h" -void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector *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 *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 *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, VectorresetAndDeleteVals(); - 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 diff --git a/src/ASTAnalyses/Order/orderanalysis.h b/src/ASTAnalyses/Order/orderanalysis.h index 24ec85c..a371c85 100644 --- a/src/ASTAnalyses/Order/orderanalysis.h +++ b/src/ASTAnalyses/Order/orderanalysis.h @@ -4,7 +4,9 @@ #include "structs.h" #include "mymemory.h" -void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector *finishNodes, bool computeTransitiveClosure); +void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet * table, Vector *finishNodes, bool computeTransitiveClosure); +HashtableNodeToNodeSet * getMustReachMap(CSolver *solver, OrderGraph *graph, Vector *finishNodes); + void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure); void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph); void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph); diff --git a/src/Collections/hashtable.h b/src/Collections/hashtable.h index 218fb2d..9f5f3b3 100644 --- a/src/Collections/hashtable.h +++ b/src/Collections/hashtable.h @@ -30,6 +30,7 @@ template struct Hashlistnode { _Key key; _Val val; + uint hashcode; }; template @@ -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; } diff --git a/src/Collections/structs.cc b/src/Collections/structs.cc index 2001242..4e2827c 100644 --- a/src/Collections/structs.cc +++ b/src/Collections/structs.cc @@ -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) { diff --git a/src/config.h b/src/config.h index 0c73cae..2e48668 100644 --- a/src/config.h +++ b/src/config.h @@ -11,13 +11,12 @@ * @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 diff --git a/src/csolver.cc b/src/csolver.cc index 533fc4b..fb29cff 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -22,6 +22,9 @@ #include "serializer.h" #include "deserializer.h" #include "encodinggraph.h" +#include "ordergraph.h" +#include "orderedge.h" +#include "orderanalysis.h" #include 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(); diff --git a/src/csolver.h b/src/csolver.h index 16396f9..bac1a49 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -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(); diff --git a/src/mymemory.h b/src/mymemory.h index 700fb4f..0798860 100644 --- a/src/mymemory.h +++ b/src/mymemory.h @@ -19,6 +19,8 @@ #include "config.h" +//#define SATCHECK_CONFIG + /* void * ourmalloc(size_t size); void ourfree(void *ptr);