#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;
}
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;
}
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);
}
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;
replaceBooleanWithTrueNoRemove(bexpr);
}
+void CSolver::replaceBooleanWithFalseNoRemove(BooleanEdge bexpr) {
+ replaceBooleanWithTrueNoRemove(bexpr.negate());
+}
+
void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
#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();
}
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;
delete iterator;
}
}
-
- table->resetAndDeleteVals();
- delete table;
}
/* This function finds edges that would form a cycle with must edges
//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
#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);
long long finishTime = getTimeNano();
cnf->encodeTime = startSolve - startTime;
cnf->solveTime = finishTime - startSolve;
+ model_print("CNF Encode time: %f\n Solve time: %f\n", cnf->encodeTime/1000000000.0, cnf->solveTime/ 1000000000.0);
return result;
}
struct Hashlistnode {
_Key key;
_Val val;
+ uint hashcode;
};
template<typename _Key, int _Shift, typename _KeyInt>
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];
//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++;
}
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];
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)
}
- unsigned int index = hash_function(key);
+ unsigned int hashcode = hash_function(key);
+ unsigned int index = hashcode;
do {
index &= capacitymask;
search = &table[index];
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;
}
unsigned int index = hash_function(key);
+ unsigned int hashcode = index;
do {
index &= capacitymask;
search = &table[index];
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;
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;
}
#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;
}
}
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) {
}
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) {
}
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) {
* @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
+#define SATCHECK_CONFIG
#ifndef CONFIG_ASSERT
#define CONFIG_ASSERT
#include "serializer.h"
#include "deserializer.h"
#include "encodinggraph.h"
+#include "ordergraph.h"
+#include "orderedge.h"
+#include "orderanalysis.h"
#include <time.h>
CSolver::CSolver() :
void CSolver::serialize() {
model_print("serializing ...\n");
char buffer[255];
- struct timespec t;
- clock_gettime(CLOCK_REALTIME, &t);
-
- unsigned long long nanotime=t.tv_sec*1000000000+t.tv_nsec;
+ long long nanotime=getTimeNano();
int numchars=sprintf(buffer, "DUMP%llu", nanotime);
Serializer serializer(buffer);
SetIteratorBooleanEdge *it = getConstraints();
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;
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);
+ }
+}
+
+#define NANOSEC 1000000000.0
int CSolver::solve() {
+ long long starttime = getTimeNano();
bool deleteTuner = false;
if (tuner == NULL) {
tuner = new DefaultTuner();
deleteTuner = true;
}
-
- long long startTime = getTimeNano();
- computePolarities(this);
+
+ {
+ SetIteratorOrder *orderit = activeOrders.iterator();
+ while (orderit->hasNext()) {
+ Order *order = orderit->next();
+ if (order->graph != NULL) {
+ delete order->graph;
+ order->graph = NULL;
+ }
+ }
+ delete orderit;
+ }
+
+ computePolarities(this);
+ long long time2 = getTimeNano();
+ model_print("Polarity time: %f\n", (time2-starttime)/NANOSEC);
Preprocess pp(this);
pp.doTransform();
-
+ long long time3 = getTimeNano();
+ model_print("Preprocess time: %f\n", (time3-time2)/NANOSEC);
+
DecomposeOrderTransform dot(this);
dot.doTransform();
+ long long time4 = getTimeNano();
+ model_print("Decompose Order: %f\n", (time4-time3)/NANOSEC);
IntegerEncodingTransform iet(this);
iet.doTransform();
EncodingGraph eg(this);
eg.buildGraph();
eg.encode();
-// printConstraints();
+
naiveEncodingDecision(this);
+ long long time5 = getTimeNano();
+ model_print("Encoding Graph Time: %f\n", (time5-time4)/NANOSEC);
+
+ long long startTime = getTimeNano();
satEncoder->encodeAllSATEncoder(this);
+ long long endTime = getTimeNano();
+
+ elapsedTime = endTime - startTime;
+ model_print("Elapse Encode time: %f\n", elapsedTime/NANOSEC);
+
model_print("Is problem UNSAT after encoding: %d\n", unsat);
int result = unsat ? IS_UNSAT : satEncoder->solve();
model_print("Result Computed in CSolver: %d\n", result);
- long long finishTime = getTimeNano();
- elapsedTime = finishTime - startTime;
+
if (deleteTuner) {
delete tuner;
tuner = NULL;
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();
#include "config.h"
+#define SATCHECK_CONFIG
+
/*
void * ourmalloc(size_t size);
void ourfree(void *ptr);
projects / satune.git / commitdiff