Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into...
authorHamed <hamed.gorjiara@gmail.com>
Wed, 6 Sep 2017 18:04:34 +0000 (11:04 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Wed, 6 Sep 2017 18:04:34 +0000 (11:04 -0700)
18 files changed:
src/AST/boolean.cc
src/AST/boolean.h
src/AST/element.cc
src/AST/element.h
src/AST/function.cc
src/AST/rewriter.cc
src/ASTAnalyses/polarityassignment.cc
src/ASTAnalyses/polarityassignment.h
src/ASTTransform/preprocess.cc [new file with mode: 0644]
src/ASTTransform/preprocess.h [new file with mode: 0644]
src/Backend/constraint.cc
src/Collections/qsort.cc [new file with mode: 0644]
src/Collections/qsort.h [new file with mode: 0644]
src/Collections/structs.h
src/Translator/sattranslator.cc
src/Tuner/tunable.h
src/csolver.cc
src/mymemory.h

index 4ca9c404522deb2e324fc617580e8243d2159b37..978664450ba930b9eab9b61794197519a4309632 100644 (file)
@@ -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);
+}
index ecaebaf69c89fef2ebfc77d5de1fffd4c53db2e6..8be1d30626c93f6c3612ab0447157bb3f4825dc1 100644 (file)
@@ -21,7 +21,8 @@ public:
        Polarity polarity;
        BooleanValue boolVal;
        Vector<Boolean *> parents;
-
+       virtual void updateParents() {}
+       
        CMEMALLOC;
 };
 
@@ -66,6 +67,8 @@ public:
        Array<Element *> inputs;
        BooleanEdge undefStatus;
        FunctionEncoding *getFunctionEncoding() {return &encoding;}
+       void updateParents();
+
        CMEMALLOC;
 };
 
@@ -77,6 +80,8 @@ public:
        LogicOp op;
        bool replaced;
        Array<BooleanEdge> inputs;
+       void updateParents();
+       
        CMEMALLOC;
 };
 BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e);
index 3fe8cef45710eee5c3ced313c9325700c73629db..fd308122caee3b28cd5a71226d4f591872113f57 100644 (file)
@@ -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);
+}
index c3a3ed9fe2bd764207756b8fdfbc755cd1dfd0cc..544725624c4d4ab3ef6426fd4cc8fba070a756d0 100644 (file)
@@ -15,7 +15,8 @@ public:
        Vector<ASTNode *> 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;
 };
 
index 6715e79e06e0115dc91449c02c768f4a7028472d..d6b2d3af814c02d589722406614ef101b2c7f0b4 100644 (file)
@@ -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) {
index 937a8b74cb442f2f6a0738fa039da845a0558eb8..b6908e1f1dc1b7435b21fa637345492ad4f98971 100644 (file)
@@ -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();
index f75c9ece2b11f5178c39e3ac4dbfc2c79a145824..0be806623602a3ae1d59fbce9e073d2a24c91a80 100644 (file)
@@ -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);
index 625587543b2e86131320baab2b4da189c365fec0..8873ef247f6ae1238c745ab7fb8b070c77effbad 100644 (file)
 #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 (file)
index 0000000..00d324e
--- /dev/null
@@ -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 (file)
index 0000000..3aa3749
--- /dev/null
@@ -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
index 61fba12ed5ed190aa967347bc3c05fefa74e0c29..7c3a094701d3c12ffa08d5a3fba5c83dd6b3f4d8 100644 (file)
@@ -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 (file)
index 0000000..0c415b5
--- /dev/null
@@ -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 <sys/types.h>
+#include <stdlib.h>
+#include <errno.h>
+#include "mymemory.h"
+#include <inttypes.h>
+/*
+ * 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 (file)
index 0000000..ca744aa
--- /dev/null
@@ -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
index ea7fa1f138dce7fe0fffeab80239f51eaf3460c7..e9c645f3a1dc85c1b8ed166cd820aa6910c9ff1f 100644 (file)
@@ -23,6 +23,8 @@ typedef Hashset<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_ent
 typedef Hashset<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HashsetOrderNode;
 typedef Hashset<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HashsetOrderEdge;
 typedef Hashset<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HashsetOrderElement;
+typedef Hashset<Boolean *, uintptr_t, 4> HashsetBoolean;
+typedef SetIterator<Boolean *, uintptr_t, 4> SetIteratorBoolean;
 
 typedef Hashtable<OrderNode *, HashsetOrderNode *, uintptr_t, 4> HashtableNodeToNodeSet;
 typedef Hashtable<OrderPair *, OrderPair *, uintptr_t, 4, order_pair_hash_function, order_pair_equals> HashtableOrderPair;
index 7c48be6324430b094e51477ac696b8f0075e9ebd..d670a94fdff895d795ff6240233d3ff6d84369bf 100644 (file)
@@ -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);
+       }
 }
 
 
index 480034516bb328fd1e418386aeb6d985ee894509..660c77db7ab0e64162b510036aaceb0f88c64235 100644 (file)
@@ -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
index d94ddfce66ffed8a98b4e849c129ae8751b3c678..6454b376ed4672d05fbf31a52c77fd33695570e8 100644 (file)
@@ -17,7 +17,8 @@
 #include "structs.h"
 #include "orderresolver.h"
 #include "integerencoding.h"
-#include <stdlib.h>
+#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();
 
index 7c63aa11c10edb99f259ab9a11fffcae8df89794..e0a60bd13294b871199b826e88c0ea13261c1b3d 100644 (file)
@@ -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);