From: Hamed Date: Wed, 6 Sep 2017 18:04:34 +0000 (-0700) Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=5567c0959b9e3bcdebcf3c2dfab9af3728fe25c2;hp=682109617a66ee846aa596e9661363280e517d98 Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into hamed --- diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index 4ca9c40..9786644 100644 --- a/src/AST/boolean.cc +++ b/src/AST/boolean.cc @@ -37,9 +37,6 @@ BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uin encoding(this), inputs(_inputs, _numInputs), undefStatus(_undefinedStatus) { - for (uint i = 0; i < _numInputs; i++) { - _inputs[i]->parents.push(this); - } } BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize) : @@ -47,9 +44,6 @@ BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uin op(_op), replaced(false), inputs(array, asize) { - for (uint i = 0; i < asize; i++) { - array[i]->parents.push(this); - } } BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e) { @@ -96,3 +90,11 @@ Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) { return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus).getRaw(); } + +void BooleanPredicate::updateParents() { + for(uint i=0;i < inputs.getSize(); i++) inputs.get(i)->parents.push(this); +} + +void BooleanLogic::updateParents() { + for(uint i=0;i < inputs.getSize(); i++) inputs.get(i)->parents.push(this); +} diff --git a/src/AST/boolean.h b/src/AST/boolean.h index ecaebaf..8be1d30 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -21,7 +21,8 @@ public: Polarity polarity; BooleanValue boolVal; Vector parents; - + virtual void updateParents() {} + CMEMALLOC; }; @@ -66,6 +67,8 @@ public: Array inputs; BooleanEdge undefStatus; FunctionEncoding *getFunctionEncoding() {return &encoding;} + void updateParents(); + CMEMALLOC; }; @@ -77,6 +80,8 @@ public: LogicOp op; bool replaced; Array inputs; + void updateParents(); + CMEMALLOC; }; BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e); diff --git a/src/AST/element.cc b/src/AST/element.cc index 3fe8cef..fd30812 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -22,8 +22,6 @@ ElementFunction::ElementFunction(Function *_function, Element **array, uint numA inputs(array, numArrays), overflowstatus(_overflowstatus), functionencoding(this) { - for (uint i = 0; i < numArrays; i++) - array[i]->parents.push(this); } ElementConst::ElementConst(uint64_t _value, VarType _type, Set *_set) : @@ -77,3 +75,7 @@ Element *ElementFunction::clone(CSolver *solver, CloneMap *map) { Element *e = solver->applyFunction(function->clone(solver, map), array, inputs.getSize(), overflowstatus->clone(solver, map)); return e; } + +void ElementFunction::updateParents() { + for(uint i=0;i < inputs.getSize(); i++) inputs.get(i)->parents.push(this); +} diff --git a/src/AST/element.h b/src/AST/element.h index c3a3ed9..5447256 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -15,7 +15,8 @@ public: Vector parents; ElementEncoding encoding; virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}; - + virtual void updateParents() {} + CMEMALLOC; }; @@ -44,6 +45,7 @@ public: BooleanEdge overflowstatus; FunctionEncoding functionencoding; Element *clone(CSolver *solver, CloneMap *map); + void updateParents(); CMEMALLOC; }; diff --git a/src/AST/function.cc b/src/AST/function.cc index 6715e79..d6b2d3a 100644 --- a/src/AST/function.cc +++ b/src/AST/function.cc @@ -3,10 +3,18 @@ #include "set.h" #include "csolver.h" -FunctionOperator::FunctionOperator(ArithOp _op, Set **domain, uint numDomain, Set *_range, OverFlowBehavior _overflowbehavior) : Function(OPERATORFUNC), op(_op), domains(domain, numDomain), range(_range), overflowbehavior(_overflowbehavior) { +FunctionOperator::FunctionOperator(ArithOp _op, Set **domain, uint numDomain, Set *_range, OverFlowBehavior _overflowbehavior) : + Function(OPERATORFUNC), + op(_op), + domains(domain, numDomain), + range(_range), + overflowbehavior(_overflowbehavior) { } -FunctionTable::FunctionTable (Table *_table, UndefinedBehavior _undefBehavior) : Function(TABLEFUNC), table(_table), undefBehavior(_undefBehavior) { +FunctionTable::FunctionTable (Table *_table, UndefinedBehavior _undefBehavior) : + Function(TABLEFUNC), + table(_table), + undefBehavior(_undefBehavior) { } uint64_t FunctionOperator::applyFunctionOperator(uint numVals, uint64_t *values) { diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index 937a8b7..b6908e1 100644 --- a/src/AST/rewriter.cc +++ b/src/AST/rewriter.cc @@ -17,6 +17,8 @@ void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) { void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) { updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE); + + ASSERT(bexpr->boolVal != BV_UNSAT); uint size = bexpr->parents.getSize(); for (uint i = 0; i < size; i++) { @@ -44,14 +46,25 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) { if (oldb.isNegated()) { oldb=oldb.negate(); newb=newb.negate(); + } if (constraints.contains(oldb)) { constraints.remove(oldb); constraints.add(newb); + if (newb->type == BOOLEANVAR) + replaceBooleanWithTrue(newb); + else + replaceBooleanWithTrueNoRemove(newb); + return; } if (constraints.contains(oldb.negate())) { constraints.remove(oldb.negate()); constraints.add(newb.negate()); + if (newb->type == BOOLEANVAR) + replaceBooleanWithTrue(newb.negate()); + else + replaceBooleanWithTrueNoRemove(newb.negate()); + return; } BooleanEdge oldbnegated = oldb.negate(); diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc index f75c9ec..0be8066 100644 --- a/src/ASTAnalyses/polarityassignment.cc +++ b/src/ASTAnalyses/polarityassignment.cc @@ -7,50 +7,50 @@ void computePolarities(CSolver *This) { BooleanEdge boolean = iterator->next(); Boolean *b = boolean.getBoolean(); bool isNegated = boolean.isNegated(); - if (isNegated) { - updatePolarity(b, P_FALSE); - } else { - updatePolarity(b, P_TRUE); - } - computePolarity(b); + computePolarity(b, isNegated ? P_FALSE : P_TRUE); } delete iterator; } -void updatePolarity(Boolean *This, Polarity polarity) { - This->polarity = (Polarity) (This->polarity | polarity); +bool updatePolarity(Boolean *This, Polarity polarity) { + Polarity oldpolarity = This->polarity; + Polarity newpolarity = (Polarity) (This->polarity | polarity); + This->polarity = newpolarity; + return newpolarity != oldpolarity; } void updateMustValue(Boolean *This, BooleanValue value) { This->boolVal = (BooleanValue) (This->boolVal | value); } -void computePolarity(Boolean *This) { - switch (This->type) { - case BOOLEANVAR: - case ORDERCONST: - return; - case PREDICATEOP: - return computePredicatePolarity((BooleanPredicate *)This); - case LOGICOP: - return computeLogicOpPolarity((BooleanLogic *)This); - default: - ASSERT(0); +void computePolarity(Boolean *This, Polarity polarity) { + if (updatePolarity(This, polarity)) { + switch (This->type) { + case BOOLEANVAR: + case ORDERCONST: + return; + case PREDICATEOP: + return computePredicatePolarity((BooleanPredicate *)This); + case LOGICOP: + return computeLogicOpPolarity((BooleanLogic *)This); + default: + ASSERT(0); + } } } void computePredicatePolarity(BooleanPredicate *This) { if (This->undefStatus) { - updatePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE); - computePolarity(This->undefStatus.getBoolean()); + computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE); } } void computeLogicOpPolarity(BooleanLogic *This) { - computeLogicOpPolarityChildren(This); + Polarity child=computeLogicOpPolarityChildren(This); uint size = This->inputs.getSize(); for (uint i = 0; i < size; i++) { - computePolarity(This->inputs.get(i).getBoolean()); + BooleanEdge b=This->inputs.get(i); + computePolarity(b.getBoolean(), b.isNegated() ? negatePolarity(child) : child); } } @@ -82,22 +82,13 @@ BooleanValue negateBooleanValue(BooleanValue This) { } } -void computeLogicOpPolarityChildren(BooleanLogic *This) { - Polarity parentpolarity = This->polarity; +Polarity computeLogicOpPolarityChildren(BooleanLogic *This) { switch (This->op) { case SATC_AND: { - uint size = This->inputs.getSize(); - for (uint i = 0; i < size; i++) { - BooleanEdge tmp = This->inputs.get(i); - Boolean *btmp = tmp.getBoolean(); - updatePolarity(btmp, tmp.isNegated() ? negatePolarity(parentpolarity) : parentpolarity); - } - break; + return This->polarity; } case SATC_IFF: { - updatePolarity(This->inputs.get(0).getBoolean(), P_BOTHTRUEFALSE); - updatePolarity(This->inputs.get(1).getBoolean(), P_BOTHTRUEFALSE); - break; + return P_BOTHTRUEFALSE; } default: ASSERT(0); diff --git a/src/ASTAnalyses/polarityassignment.h b/src/ASTAnalyses/polarityassignment.h index 6255875..8873ef2 100644 --- a/src/ASTAnalyses/polarityassignment.h +++ b/src/ASTAnalyses/polarityassignment.h @@ -14,13 +14,13 @@ #include "boolean.h" void computePolarities(CSolver *This); -void updatePolarity(Boolean *This, Polarity polarity); +bool updatePolarity(Boolean *This, Polarity polarity); void updateMustValue(Boolean *This, BooleanValue value); -void computePolarity(Boolean *boolean); +void computePolarity(Boolean *boolean, Polarity polarity); void computePredicatePolarity(BooleanPredicate *This); void computeLogicOpPolarity(BooleanLogic *boolean); Polarity negatePolarity(Polarity This); BooleanValue negateBooleanValue(BooleanValue This); -void computeLogicOpPolarityChildren(BooleanLogic *boolean); +Polarity computeLogicOpPolarityChildren(BooleanLogic *boolean); #endif/* POLARITYASSIGNMENT_H */ diff --git a/src/ASTTransform/preprocess.cc b/src/ASTTransform/preprocess.cc new file mode 100644 index 0000000..00d324e --- /dev/null +++ b/src/ASTTransform/preprocess.cc @@ -0,0 +1,66 @@ +#include "preprocess.h" +#include "boolean.h" +#include "csolver.h" +#include "tunable.h" + +Preprocess::Preprocess(CSolver *_solver) + : Transform(_solver) +{ +} + +Preprocess::~Preprocess() { +} + +void Preprocess::doTransform() { + if (solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0) + return; + + SetIteratorBooleanEdge *iterator = solver->getConstraints(); + while (iterator->hasNext()) { + BooleanEdge boolean = iterator->next(); + Boolean *b = boolean.getBoolean(); + transformBoolean(b); + } + delete iterator; + resolveBooleanVars(); +} + +void Preprocess::resolveBooleanVars() { + SetIteratorBoolean * iterator = toremove.iterator(); + while (iterator->hasNext()) { + BooleanVar *bv = (BooleanVar *) iterator->next(); + if (bv->polarity == P_TRUE) { + solver->replaceBooleanWithTrue(BooleanEdge(bv)); + } else if (bv->polarity == P_FALSE) { + solver->replaceBooleanWithFalse(BooleanEdge(bv)); + } + } + delete iterator; +} + +void Preprocess::transformBoolean(Boolean *b) { + if (!processed.add(b)) + return; + switch (b->type) { + case BOOLEANVAR: + processBooleanVar((BooleanVar *)b); + break; + case LOGICOP: + processLogicOp((BooleanLogic *)b); + break; + default: + break; + } +} + +void Preprocess::processBooleanVar(BooleanVar * b) { + if (b->polarity==P_TRUE || + b->polarity==P_FALSE) { + toremove.add(b); + } +} + +void Preprocess::processLogicOp(BooleanLogic * b) { + for(uint i=0; i < b->inputs.getSize(); i++) + transformBoolean(b->inputs.get(i).getBoolean()); +} diff --git a/src/ASTTransform/preprocess.h b/src/ASTTransform/preprocess.h new file mode 100644 index 0000000..3aa3749 --- /dev/null +++ b/src/ASTTransform/preprocess.h @@ -0,0 +1,22 @@ +#ifndef PREPROCESS_H +#define PREPROCESS_H +#include "classlist.h" +#include "transform.h" + +class Preprocess : public Transform { + public: + Preprocess(CSolver *_solver); + ~Preprocess(); + void doTransform(); + + CMEMALLOC; +private: + HashsetBoolean processed; + HashsetBoolean toremove; + void transformBoolean(Boolean *b); + void processBooleanVar(BooleanVar * b); + void processLogicOp(BooleanLogic * b); + void resolveBooleanVars(); +}; + +#endif diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index 61fba12..7c3a094 100644 --- a/src/Backend/constraint.cc +++ b/src/Backend/constraint.cc @@ -4,6 +4,7 @@ #include "inc_solver.h" #include "cnfexpr.h" #include "common.h" +#include "qsort.h" /* V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios, Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon. @@ -187,7 +188,7 @@ int comparefunction(const Edge *e1, const Edge *e2) { Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) { ASSERT(numEdges != 0); - qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction); + bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction); uint initindex = 0; while (initindex < numEdges && equalsEdge(edges[initindex], E_True)) initindex++; diff --git a/src/Collections/qsort.cc b/src/Collections/qsort.cc new file mode 100644 index 0000000..0c415b5 --- /dev/null +++ b/src/Collections/qsort.cc @@ -0,0 +1,412 @@ +/* $OpenBSD: qsort.c,v 1.18 2017/05/30 14:54:09 millert Exp $ */ +/*- + * Copyright (c) 1992, 1993 + * The Regents of the University of California. All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. Neither the name of the University nor the names of its contributors + * may be used to endorse or promote products derived from this software + * without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + */ + +/* $OpenBSD: heapsort.c,v 1.11 2017/05/20 12:48:56 millert Exp $ */ +/*- + * Copyright (c) 1991, 1993 + * The Regents of the University of California. All rights reserved. + * + * This code is derived from software contributed to Berkeley by + * Ronnie Kon at Mindcraft Inc., Kevin Lew and Elmer Yglesias. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. Neither the name of the University nor the names of its contributors + * may be used to endorse or promote products derived from this software + * without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + */ + + + +#include +#include +#include +#include "mymemory.h" +#include +/* + * Swap two areas of size number of bytes. Although qsort(3) permits random + * blocks of memory to be sorted, sorting pointers is almost certainly the + * common case (and, were it not, could easily be made so). Regardless, it + * isn't worth optimizing; the SWAP's get sped up by the cache, and pointer + * arithmetic gets lost in the time required for comparison function calls. + */ +#define SWAP(a, b, count, size, tmp) { \ + count = size; \ + do { \ + tmp = *a; \ + *a++ = *b; \ + *b++ = tmp; \ + } while (--count); \ +} + +/* Copy one block of size size to another. */ +#define COPY(a, b, count, size, tmp1, tmp2) { \ + count = size; \ + tmp1 = a; \ + tmp2 = b; \ + do { \ + *tmp1++ = *tmp2++; \ + } while (--count); \ +} + +/* + * Build the list into a heap, where a heap is defined such that for + * the records K1 ... KN, Kj/2 >= Kj for 1 <= j/2 <= j <= N. + * + * There are two cases. If j == nmemb, select largest of Ki and Kj. If + * j < nmemb, select largest of Ki, Kj and Kj+1. + */ +#define CREATE(initval, nmemb, par_i, child_i, par, child, size, count, tmp) { \ + for (par_i = initval; (child_i = par_i * 2) <= nmemb; \ + par_i = child_i) { \ + child = base + child_i * size; \ + if (child_i < nmemb && compar(child, child + size) < 0) { \ + child += size; \ + ++child_i; \ + } \ + par = base + par_i * size; \ + if (compar(child, par) <= 0) \ + break; \ + SWAP(par, child, count, size, tmp); \ + } \ +} + +/* + * Select the top of the heap and 'heapify'. Since by far the most expensive + * action is the call to the compar function, a considerable optimization + * in the average case can be achieved due to the fact that k, the displaced + * element, is usually quite small, so it would be preferable to first + * heapify, always maintaining the invariant that the larger child is copied + * over its parent's record. + * + * Then, starting from the *bottom* of the heap, finding k's correct place, + * again maintaining the invariant. As a result of the invariant no element + * is 'lost' when k is assigned its correct place in the heap. + * + * The time savings from this optimization are on the order of 15-20% for the + * average case. See Knuth, Vol. 3, page 158, problem 18. + * + * XXX Don't break the #define SELECT line, below. Reiser cpp gets upset. + */ +#define SELECT(par_i, child_i, nmemb, par, child, size, k, count, tmp1, tmp2) { \ + for (par_i = 1; (child_i = par_i * 2) <= nmemb; par_i = child_i) { \ + child = base + child_i * size; \ + if (child_i < nmemb && compar(child, child + size) < 0) { \ + child += size; \ + ++child_i; \ + } \ + par = base + par_i * size; \ + COPY(par, child, count, size, tmp1, tmp2); \ + } \ + for (;;) { \ + child_i = par_i; \ + par_i = child_i / 2; \ + child = base + child_i * size; \ + par = base + par_i * size; \ + if (child_i == 1 || compar(k, par) < 0) { \ + COPY(child, k, count, size, tmp1, tmp2); \ + break; \ + } \ + COPY(child, par, count, size, tmp1, tmp2); \ + } \ +} + +/* + * Heapsort -- Knuth, Vol. 3, page 145. Runs in O (N lg N), both average + * and worst. While heapsort is faster than the worst case of quicksort, + * the BSD quicksort does median selection so that the chance of finding + * a data set that will trigger the worst case is nonexistent. Heapsort's + * only advantage over quicksort is that it requires little additional memory. + */ +int +bsdheapsort(void *vbase, size_t nmemb, size_t size, + int (*compar)(const void *, const void *)) +{ + size_t cnt, i, j, l; + char tmp, *tmp1, *tmp2; + char *base, *k, *p, *t; + + if (nmemb <= 1) + return (0); + + if (!size) { + errno = EINVAL; + return (-1); + } + + if ((k = (char *) ourmalloc(size)) == NULL) + return (-1); + + /* + * Items are numbered from 1 to nmemb, so offset from size bytes + * below the starting address. + */ + base = (char *)vbase - size; + + for (l = nmemb / 2 + 1; --l;) + CREATE(l, nmemb, i, j, t, p, size, cnt, tmp); + + /* + * For each element of the heap, save the largest element into its + * final slot, save the displaced element (k), then recreate the + * heap. + */ + while (nmemb > 1) { + COPY(k, base + nmemb * size, cnt, size, tmp1, tmp2); + COPY(base + nmemb * size, base + size, cnt, size, tmp1, tmp2); + --nmemb; + SELECT(i, j, nmemb, t, p, size, k, cnt, tmp1, tmp2); + } + ourfree(k); + return (0); +} + + +static __inline char *med3(char *, char *, char *, int (*)(const void *, const void *)); +static __inline void swapfunc(char *, char *, size_t, int); + +#define min(a, b) (a) < (b) ? a : b + +/* + * Qsort routine from Bentley & McIlroy's "Engineering a Sort Function". + * + * This version differs from Bentley & McIlroy in the following ways: + * 1. The partition value is swapped into a[0] instead of being + * stored out of line. + * + * 2. The swap function can swap 32-bit aligned elements on 64-bit + * platforms instead of swapping them as byte-aligned. + * + * 3. It uses David Musser's introsort algorithm to fall back to + * heapsort(3) when the recursion depth reaches 2*lg(n + 1). + * This avoids quicksort's quadratic behavior for pathological + * input without appreciably changing the average run time. + * + * 4. Tail recursion is eliminated when sorting the larger of two + * subpartitions to save stack space. + */ +#define SWAPTYPE_BYTEV 1 +#define SWAPTYPE_INTV 2 +#define SWAPTYPE_LONGV 3 +#define SWAPTYPE_INT 4 +#define SWAPTYPE_LONG 5 + +#define TYPE_ALIGNED(TYPE, a, es) \ + (((char *)a - (char *)0) % sizeof(TYPE) == 0 && es % sizeof(TYPE) == 0) + +#define swapcode(TYPE, parmi, parmj, n) { \ + size_t i = (n) / sizeof (TYPE); \ + TYPE *pi = (TYPE *) (parmi); \ + TYPE *pj = (TYPE *) (parmj); \ + do { \ + TYPE t = *pi; \ + *pi++ = *pj; \ + *pj++ = t; \ + } while (--i > 0); \ +} + +static __inline void +swapfunc(char *a, char *b, size_t n, int swaptype) +{ + switch (swaptype) { + case SWAPTYPE_INT: + case SWAPTYPE_INTV: + swapcode(int, a, b, n); + break; + case SWAPTYPE_LONG: + case SWAPTYPE_LONGV: + swapcode(long, a, b, n); + break; + default: + swapcode(char, a, b, n); + break; + } +} + +#define swap(a, b) do { \ + switch (swaptype) { \ + case SWAPTYPE_INT: { \ + int t = *(int *)(a); \ + *(int *)(a) = *(int *)(b); \ + *(int *)(b) = t; \ + break; \ + } \ + case SWAPTYPE_LONG: { \ + long t = *(long *)(a); \ + *(long *)(a) = *(long *)(b); \ + *(long *)(b) = t; \ + break; \ + } \ + default: \ + swapfunc(a, b, es, swaptype); \ + } \ +} while (0) + +#define vecswap(a, b, n) if ((n) > 0) swapfunc(a, b, n, swaptype) + +static __inline char * +med3(char *a, char *b, char *c, int (*cmp)(const void *, const void *)) +{ + return cmp(a, b) < 0 ? + (cmp(b, c) < 0 ? b : (cmp(a, c) < 0 ? c : a )) + :(cmp(b, c) > 0 ? b : (cmp(a, c) < 0 ? a : c )); +} + +static void +introsort(char *a, size_t n, size_t es, size_t maxdepth, int swaptype, + int (*cmp)(const void *, const void *)) +{ + char *pa, *pb, *pc, *pd, *pl, *pm, *pn; + int cmp_result; + size_t r, s; + +loop: if (n < 7) { + for (pm = a + es; pm < a + n * es; pm += es) + for (pl = pm; pl > a && cmp(pl - es, pl) > 0; + pl -= es) + swap(pl, pl - es); + return; + } + if (maxdepth == 0) { + if (bsdheapsort(a, n, es, cmp) == 0) + return; + } + maxdepth--; + pm = a + (n / 2) * es; + if (n > 7) { + pl = a; + pn = a + (n - 1) * es; + if (n > 40) { + s = (n / 8) * es; + pl = med3(pl, pl + s, pl + 2 * s, cmp); + pm = med3(pm - s, pm, pm + s, cmp); + pn = med3(pn - 2 * s, pn - s, pn, cmp); + } + pm = med3(pl, pm, pn, cmp); + } + swap(a, pm); + pa = pb = a + es; + pc = pd = a + (n - 1) * es; + for (;;) { + while (pb <= pc && (cmp_result = cmp(pb, a)) <= 0) { + if (cmp_result == 0) { + swap(pa, pb); + pa += es; + } + pb += es; + } + while (pb <= pc && (cmp_result = cmp(pc, a)) >= 0) { + if (cmp_result == 0) { + swap(pc, pd); + pd -= es; + } + pc -= es; + } + if (pb > pc) + break; + swap(pb, pc); + pb += es; + pc -= es; + } + + pn = a + n * es; + r = min(pa - a, pb - pa); + vecswap(a, pb - r, r); + r = min(((uintptr_t)(pd - pc)), ((uintptr_t)(pn - pd - es))); + vecswap(pb, pn - r, r); + /* + * To save stack space we sort the smaller side of the partition first + * using recursion and eliminate tail recursion for the larger side. + */ + r = pb - pa; + s = pd - pc; + if (r < s) { + /* Recurse for 1st side, iterate for 2nd side. */ + if (s > es) { + if (r > es) { + introsort(a, r / es, es, maxdepth, + swaptype, cmp); + } + a = pn - s; + n = s / es; + goto loop; + } + } else { + /* Recurse for 2nd side, iterate for 1st side. */ + if (r > es) { + if (s > es) { + introsort(pn - s, s / es, es, maxdepth, + swaptype, cmp); + } + n = r / es; + goto loop; + } + } +} + +void +bsdqsort(void *a, size_t n, size_t es, int (*cmp)(const void *, const void *)) +{ + size_t i, maxdepth = 0; + int swaptype; + + /* Approximate 2*ceil(lg(n + 1)) */ + for (i = n; i > 0; i >>= 1) + maxdepth++; + maxdepth *= 2; + + if (TYPE_ALIGNED(long, a, es)) + swaptype = es == sizeof(long) ? SWAPTYPE_LONG : SWAPTYPE_LONGV; + else if (sizeof(int) != sizeof(long) && TYPE_ALIGNED(int, a, es)) + swaptype = es == sizeof(int) ? SWAPTYPE_INT : SWAPTYPE_INTV; + else + swaptype = SWAPTYPE_BYTEV; + + introsort((char *) a, n, es, maxdepth, swaptype, cmp); + +} diff --git a/src/Collections/qsort.h b/src/Collections/qsort.h new file mode 100644 index 0000000..ca744aa --- /dev/null +++ b/src/Collections/qsort.h @@ -0,0 +1,7 @@ +#ifndef BSD_QSORT_H +#define BSD_QSORT_H + + +void bsdqsort(void *a, size_t n, size_t es, int (*cmp)(const void *, const void *)); + +#endif diff --git a/src/Collections/structs.h b/src/Collections/structs.h index ea7fa1f..e9c645f 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -23,6 +23,8 @@ typedef Hashset HashsetOrderNode; typedef Hashset HashsetOrderEdge; typedef Hashset HashsetOrderElement; +typedef Hashset HashsetBoolean; +typedef SetIterator SetIteratorBoolean; typedef Hashtable HashtableNodeToNodeSet; typedef Hashtable HashtableOrderPair; diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc index 7c48be6..d670a94 100644 --- a/src/Translator/sattranslator.cc +++ b/src/Translator/sattranslator.cc @@ -81,8 +81,14 @@ uint64_t getElementValueSATTranslator(CSolver *This, Element *element) { } bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) { - int index = getEdgeVar( ((BooleanVar *) boolean)->var ); - return getValueSolver(This->getSATEncoder()->getCNF()->solver, index); + if (boolean->boolVal == BV_MUSTBETRUE) + return true; + else if (boolean->boolVal == BV_MUSTBEFALSE) + return false; + else { + int index = getEdgeVar( ((BooleanVar *) boolean)->var ); + return getValueSolver(This->getSATEncoder()->getCNF()->solver, index); + } } diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h index 4800345..660c77d 100644 --- a/src/Tuner/tunable.h +++ b/src/Tuner/tunable.h @@ -37,6 +37,6 @@ public: static TunableDesc onoff(0, 1, 1); static TunableDesc offon(0, 1, 0); -enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING}; +enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS}; typedef enum Tunables Tunables; #endif diff --git a/src/csolver.cc b/src/csolver.cc index d94ddfc..6454b37 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -17,7 +17,8 @@ #include "structs.h" #include "orderresolver.h" #include "integerencoding.h" -#include +#include "qsort.h" +#include "preprocess.h" CSolver::CSolver() : boolTrue(BooleanEdge(new BooleanConst(true))), @@ -143,6 +144,7 @@ Element *CSolver::applyFunction(Function *function, Element **array, uint numArr Element *element = new ElementFunction(function,array,numArrays,overflowstatus); Element *e = elemMap.get(element); if (e == NULL) { + element->updateParents(); allElements.push(element); elemMap.put(element, element); return element; @@ -212,6 +214,7 @@ BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus); Boolean *b = boolMap.get(boolean); if (b == NULL) { + boolean->updateParents(); boolMap.put(boolean, boolean); allBooleans.push(boolean); return BooleanEdge(boolean); @@ -316,7 +319,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint } else if (newindex == 1) { return newarray[0]; } else { - qsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares); + bsdqsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares); array = newarray; asize = newindex; } @@ -336,6 +339,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint Boolean *boolean = new BooleanLogic(this, op, array, asize); Boolean *b = boolMap.get(boolean); if (b == NULL) { + boolean->updateParents(); boolMap.put(boolean, boolean); allBooleans.push(boolean); return BooleanEdge(boolean); @@ -400,6 +404,9 @@ int CSolver::solve() { long long startTime = getTimeNano(); computePolarities(this); + Preprocess pp(this); + pp.doTransform(); + DecomposeOrderTransform dot(this); dot.doTransform(); diff --git a/src/mymemory.h b/src/mymemory.h index 7c63aa1..e0a60bd 100644 --- a/src/mymemory.h +++ b/src/mymemory.h @@ -26,7 +26,7 @@ void * ourrealloc(void *ptr, size_t size); */ -#if 0 +#if 1 void * model_malloc(size_t size); void model_free(void *ptr); void * model_calloc(size_t count, size_t size);