remove redundant domains
authorbdemsky <bdemsky@uci.edu>
Mon, 23 Jul 2018 23:42:41 +0000 (16:42 -0700)
committerbdemsky <bdemsky@uci.edu>
Mon, 23 Jul 2018 23:42:41 +0000 (16:42 -0700)
28 files changed:
src/AST/function.cc
src/AST/function.h
src/AST/predicate.cc
src/AST/predicate.h
src/AST/table.cc
src/AST/table.h
src/ASTTransform/elementopt.cc
src/ASTTransform/elementopt.h
src/ASTTransform/integerencoding.cc
src/Backend/satelemencoder.cc
src/Backend/satfuncopencoder.cc
src/Backend/satfunctableencoder.cc
src/Serialize/deserializer.cc
src/Test/anyvaluetest.cc
src/Test/buildconstraintstest.cc
src/Test/buildsimple.cc
src/Test/ccsolvertest.c
src/Test/constraint.cc
src/Test/elemequalsattest.cc
src/Test/elemequalunsattest.cc
src/Test/funcencodingtest.cc
src/Test/ltelemconsttest.cc
src/Test/tablefuncencodetest.cc
src/Test/tablepredicencodetest.cc
src/ccsolver.cc
src/ccsolver.h
src/csolver.cc
src/csolver.h

index ccd89dd..9f43fbe 100644 (file)
@@ -4,10 +4,9 @@
 #include "csolver.h"
 #include "serializer.h"
 
-FunctionOperator::FunctionOperator(ArithOp _op, Set **domain, uint numDomain, Set *_range, OverFlowBehavior _overflowbehavior) :
+FunctionOperator::FunctionOperator(ArithOp _op, Set *_range, OverFlowBehavior _overflowbehavior) :
        Function(OPERATORFUNC),
        op(_op),
-       domains(domain, numDomain),
        range(_range),
        overflowbehavior(_overflowbehavior) {
 }
@@ -41,12 +40,8 @@ Function *FunctionOperator::clone(CSolver *solver, CloneMap *map) {
        if (f != NULL)
                return f;
 
-       Set *array[domains.getSize()];
-       for (uint i = 0; i < domains.getSize(); i++) {
-               array[i] = domains.get(i)->clone(solver, map);
-       }
        Set *rcopy = range->clone(solver, map);
-       f = solver->createFunctionOperator(op, array, domains.getSize(), rcopy, overflowbehavior);
+       f = solver->createFunctionOperator(op, rcopy, overflowbehavior);
        map->put(this, f);
        return f;
 }
@@ -92,12 +87,6 @@ void FunctionOperator::serialize(Serializer *serializer) {
        if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
-
-       uint size = domains.getSize();
-       for (uint i = 0; i < size; i++) {
-               Set *domain = domains.get(i);
-               domain->serialize(serializer);
-       }
        range->serialize(serializer);
 
        ASTNodeType nodeType = FUNCOPTYPE;
@@ -105,11 +94,6 @@ void FunctionOperator::serialize(Serializer *serializer) {
        FunctionOperator *This = this;
        serializer->mywrite(&This, sizeof(FunctionOperator *));
        serializer->mywrite(&op, sizeof(ArithOp));
-       serializer->mywrite(&size, sizeof(uint));
-       for (uint i = 0; i < size; i++) {
-               Set *domain = domains.get(i);
-               serializer->mywrite(&domain, sizeof(Set *));
-       }
        serializer->mywrite(&range, sizeof(Set *));
        serializer->mywrite(&overflowbehavior, sizeof(OverFlowBehavior));
 }
index 5cfbb7d..2d65f61 100644 (file)
@@ -21,10 +21,9 @@ public:
 class FunctionOperator : public Function {
 public:
        ArithOp op;
-       Array<Set *> domains;
        Set *range;
        OverFlowBehavior overflowbehavior;
-       FunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range, OverFlowBehavior overflowbehavior);
+       FunctionOperator(ArithOp op, Set *range, OverFlowBehavior overflowbehavior);
        uint64_t applyFunctionOperator(uint numVals, uint64_t *values);
        bool isInRangeFunction(uint64_t val);
        Function *clone(CSolver *solver, CloneMap *map);
index 80e8a5e..3657ecc 100644 (file)
@@ -4,7 +4,7 @@
 #include "table.h"
 #include "csolver.h"
 
-PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), domains(domain, numDomain), op(_op) {
+PredicateOperator::PredicateOperator(CompOp _op) : Predicate(OPERATORPRED), op(_op) {
 }
 
 PredicateTable::PredicateTable(Table *_table, UndefinedBehavior _undefBehavior) : Predicate(TABLEPRED), table(_table), undefinedbehavior(_undefBehavior) {
@@ -32,11 +32,7 @@ Predicate *PredicateOperator::clone(CSolver *solver, CloneMap *map) {
        if (p != NULL)
                return p;
 
-       Set *array[domains.getSize()];
-       for (uint i = 0; i < domains.getSize(); i++)
-               array[i] = domains.get(i)->clone(solver, map);
-
-       p = solver->createPredicateOperator(op, array, domains.getSize());
+       p = solver->createPredicateOperator(op);
        map->put(this, p);
        return p;
 }
@@ -77,22 +73,11 @@ void PredicateOperator::serialize(Serializer *serializer) {
                return;
        serializer->addObject(this);
 
-       uint size = domains.getSize();
-       for (uint i = 0; i < size; i++) {
-               Set *domain = domains.get(i);
-               domain->serialize(serializer);
-       }
-
        ASTNodeType type = PREDOPERTYPE;
        serializer->mywrite(&type, sizeof(ASTNodeType));
        PredicateOperator *This = this;
        serializer->mywrite(&This, sizeof(PredicateOperator *));
        serializer->mywrite(&op, sizeof(CompOp));
-       serializer->mywrite(&size, sizeof(uint));
-       for (uint i = 0; i < size; i++) {
-               Set *domain = domains.get(i);
-               serializer->mywrite(&domain, sizeof(Set *));
-       }
 }
 
 void PredicateOperator::print() {
index 812d4bd..17e34d9 100644 (file)
@@ -20,12 +20,11 @@ public:
 
 class PredicateOperator : public Predicate {
 public:
-       PredicateOperator(CompOp op, Set **domain, uint numDomain);
+       PredicateOperator(CompOp op);
        bool evalPredicateOperator(uint64_t *inputs);
        Predicate *clone(CSolver *solver, CloneMap *map);
        virtual void serialize(Serializer *serializer);
        virtual void print();
-       Array<Set *> domains;
        CompOp getOp() {return op;}
        CMEMALLOC;
 private:
index 513935d..da0188a 100644 (file)
@@ -7,8 +7,7 @@
 #include "csolver.h"
 #include "serializer.h"
 
-Table::Table(Set **_domains, uint numDomain, Set *_range) :
-       domains(_domains, numDomain),
+Table::Table(Set *_range) :
        range(_range) {
        entries = new HashsetTableEntry();
 }
@@ -34,12 +33,9 @@ Table *Table::clone(CSolver *solver, CloneMap *map) {
        Table *t = (Table *) map->get(this);
        if (t != NULL)
                return t;
-       Set *array[domains.getSize()];
-       for (uint i = 0; i < domains.getSize(); i++) {
-               array[i] = domains.get(i)->clone(solver, map);
-       }
+
        Set *rcopy = range != NULL ? range->clone(solver, map) : NULL;
-       t = solver->createTable(array, domains.getSize(), rcopy);
+       t = solver->createTable(rcopy);
        SetIteratorTableEntry *entryit = entries->iterator();
        while (entryit->hasNext()) {
                TableEntry *te = entryit->next();
@@ -59,18 +55,11 @@ Table::~Table() {
        delete entries;
 }
 
-
-
 void Table::serialize(Serializer *serializer) {
        if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
 
-       uint size = domains.getSize();
-       for (uint i = 0; i < size; i++) {
-               Set *domain = domains.get(i);
-               domain->serialize(serializer);
-       }
        if (range != NULL)
                range->serialize(serializer);
 
@@ -78,13 +67,8 @@ void Table::serialize(Serializer *serializer) {
        serializer->mywrite(&type, sizeof(ASTNodeType));
        Table *This = this;
        serializer->mywrite(&This, sizeof(Table *));
-       serializer->mywrite(&size, sizeof(uint));
-       for (uint i = 0; i < size; i++) {
-               Set *domain = domains.get(i);
-               serializer->mywrite(&domain, sizeof(Set *));
-       }
        serializer->mywrite(&range, sizeof(Set *));
-       size = entries->getSize();
+       uint size = entries->getSize();
        serializer->mywrite(&size, sizeof(uint));
        SetIteratorTableEntry *iterator = getEntries();
        while (iterator->hasNext()) {
@@ -96,7 +80,6 @@ void Table::serialize(Serializer *serializer) {
        delete iterator;
 }
 
-
 void Table::print() {
        model_print("{Table<%p>:\n", this);
        SetIteratorTableEntry *iterator = getEntries();
index c196d3c..bd5bf18 100644 (file)
@@ -6,7 +6,7 @@
 
 class Table {
 public:
-       Table(Set **domains, uint numDomain, Set *range);
+       Table(Set *range);
        void addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result);
        TableEntry *getTableEntry(uint64_t *inputs, uint inputSize);
        Table *clone(CSolver *solver, CloneMap *map);
@@ -15,16 +15,12 @@ public:
        ~Table();
        Set *getRange() {return range;}
 
-       Set *getDomain(uint i) {return domains.get(i);}
-       uint numDomains() {return domains.getSize();}
-
        SetIteratorTableEntry *getEntries() {return entries->iterator();}
        uint getSize() {return entries->getSize();}
 
        CMEMALLOC;
 
 private:
-       Array<Set *> domains;
        Set *range;
        HashsetTableEntry *entries;
 };
index 162661b..5fa38e6 100755 (executable)
@@ -2,6 +2,9 @@
 #include "csolver.h"
 #include "tunable.h"
 #include "iterator.h"
+#include "boolean.h"
+#include "element.h"
+#include "predicate.h"
 
 ElementOpt::ElementOpt(CSolver *_solver)
        : Transform(_solver)
@@ -18,5 +21,31 @@ void ElementOpt::doTransform() {
        BooleanIterator bit(solver);
        while (bit.hasNext()) {
                Boolean *b = bit.next();
+               if (b->type == PREDICATEOP)
+                       processPredicate((BooleanPredicate *)b);
+       }
+}
+
+void ElementOpt::processPredicate(BooleanPredicate * pred) {
+       uint numInputs = pred->inputs.getSize();
+       if (numInputs != 2)
+               return;
+
+       Predicate * p = pred->getPredicate();
+       if (p->type == TABLEPRED)
+                       return;
+
+       PredicateOperator * pop = (PredicateOperator *) p;
+       CompOp op = pop->getOp();
+
+       Element * left = pred->inputs.get(0);
+       Element * right = pred->inputs.get(1);
+
+       if (left->type == ELEMCONST) {
+
+       } else if (right->type == ELEMCONST) {
+
+       } else {
+               return;
        }
 }
index 0c4acd2..ad6e790 100755 (executable)
@@ -11,6 +11,7 @@ public:
 
        CMEMALLOC;
 private:
+       void processPredicate(BooleanPredicate *);
 };
 
 #endif
index 5e4bfb8..6be73ea 100644 (file)
@@ -45,8 +45,7 @@ void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *bool
        //getting two elements and using LT predicate ...
        Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
        Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);
-       Set *sarray[] = {ierec->getSecondarySet(), ierec->getSecondarySet()};
-       Predicate *predicate = solver->createPredicateOperator(SATC_LT, sarray, 2);
+       Predicate *predicate = solver->createPredicateOperator(SATC_LT);
        Element *parray[] = {elem1, elem2};
        BooleanEdge boolean = solver->applyPredicate(predicate, parray, 2);
        updateEdgePolarity(boolean, boolOrder);
index b80978e..3266f1c 100644 (file)
@@ -42,7 +42,7 @@ void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool & memo) {
                                                if (generateNegation)
                                                        tpolarity = negatePolarity(tpolarity);
                                                PredicateOperator *predicate = (PredicateOperator *)pred->predicate;
-                                               uint numDomains = predicate->domains.getSize();
+                                               uint numDomains = pred->inputs.getSize();
                                                bool isConstant = true;
                                                for (uint i = 0; i < numDomains; i++) {
                                                        Element *e = pred->inputs.get(i);
index 1fea1a5..0cfce9b 100644 (file)
@@ -24,7 +24,7 @@ Edge SATEncoder::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint)
 
 Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
        PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
-       uint numDomains = predicate->domains.getSize();
+       uint numDomains = constraint->inputs.getSize();
        Polarity polarity = constraint->polarity;
        FunctionEncodingType encType = constraint->encoding.type;
        bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
@@ -43,7 +43,7 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
 
        uint64_t vals[numDomains];//setup value array
        for (uint i = 0; i < numDomains; i++) {
-               Set *set = predicate->domains.get(i);
+               Set *set = constraint->inputs.get(i)->getRange();
                vals[i] = set->getElement(indices[i]);
        }
 
@@ -64,7 +64,7 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
                notfinished = false;
                for (uint i = 0; i < numDomains; i++) {
                        uint index = ++indices[i];
-                       Set *set = predicate->domains.get(i);
+                       Set *set = constraint->inputs.get(i)->getRange();
 
                        if (index < set->getSize()) {
                                vals[i] = set->getElement(index);
index 9237ecc..3510d11 100644 (file)
@@ -92,7 +92,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
                break;
        }
        bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
-       uint numDomains = predicate->table->numDomains();
+       uint numDomains = constraint->inputs.getSize();
 
        if (generateNegation)
                polarity = negatePolarity(polarity);
@@ -105,7 +105,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
 
        uint64_t vals[numDomains];//setup value array
        for (uint i = 0; i < numDomains; i++) {
-               Set *set = predicate->table->getDomain(i);
+               Set *set = constraint->inputs.get(i)->getRange();
                vals[i] = set->getElement(indices[i]);
        }
        bool hasOverflow = false;
@@ -159,7 +159,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
                notfinished = false;
                for (uint i = 0; i < numDomains; i++) {
                        uint index = ++indices[i];
-                       Set *set = predicate->table->getDomain(i);
+                       Set *set = constraint->inputs.get(i)->getRange();
 
                        if (index < set->getSize()) {
                                vals[i] = set->getElement(index);
@@ -254,14 +254,14 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
                break;
        }
 
-       uint numDomains = function->table->numDomains();
+       uint numDomains = elemFunc->inputs.getSize();
 
        uint indices[numDomains];       //setup indices
        bzero(indices, sizeof(uint) * numDomains);
 
        uint64_t vals[numDomains];//setup value array
        for (uint i = 0; i < numDomains; i++) {
-               Set *set = function->table->getDomain(i);
+               Set *set = elemFunc->inputs.get(i)->getRange();
                vals[i] = set->getElement(indices[i]);
        }
 
@@ -324,7 +324,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
                notfinished = false;
                for (uint i = 0; i < numDomains; i++) {
                        uint index = ++indices[i];
-                       Set *set = function->table->getDomain(i);
+                       Set *set = elemFunc->inputs.get(i)->getRange();
 
                        if (index < set->getSize()) {
                                vals[i] = set->getElement(index);
index 56acc52..42b565e 100644 (file)
@@ -283,40 +283,21 @@ void Deserializer::deserializePredicateOperator() {
        myread(&po_ptr, sizeof(PredicateOperator *));
        CompOp op;
        myread(&op, sizeof(CompOp));
-       uint size;
-       myread(&size, sizeof(uint));
-       Vector<Set *> domains;
-       for (uint i = 0; i < size; i++) {
-               Set *domain;
-               myread(&domain, sizeof(Set *));
-               ASSERT(map.contains(domain));
-               domain = (Set *) map.get(domain);
-               domains.push(domain);
-       }
 
-       map.put(po_ptr, solver->createPredicateOperator(op, domains.expose(), size));
+       map.put(po_ptr, solver->createPredicateOperator(op));
 }
 
 void Deserializer::deserializeTable() {
        Table *t_ptr;
        myread(&t_ptr, sizeof(Table *));
-       uint size;
-       myread(&size, sizeof(uint));
-       Vector<Set *> domains;
-       for (uint i = 0; i < size; i++) {
-               Set *domain;
-               myread(&domain, sizeof(Set *));
-               ASSERT(map.contains(domain));
-               domain = (Set *) map.get(domain);
-               domains.push(domain);
-       }
        Set *range;
        myread(&range, sizeof(Set *));
        if (range != NULL) {
                ASSERT(map.contains(range));
                range = (Set *) map.get(range);
        }
-       Table *table = solver->createTable(domains.expose(), size, range);
+       Table *table = solver->createTable(range);
+       uint size;
        myread(&size, sizeof(uint));
        for (uint i = 0; i < size; i++) {
                uint64_t output;
@@ -388,23 +369,13 @@ void Deserializer::deserializeFunctionOperator() {
        myread(&fo_ptr, sizeof(FunctionOperator *));
        ArithOp op;
        myread(&op, sizeof(ArithOp));
-       uint size;
-       myread(&size, sizeof(uint));
-       Vector<Set *> domains;
-       for (uint i = 0; i < size; i++) {
-               Set *domain;
-               myread(&domain, sizeof(Set *));
-               ASSERT(map.contains(domain));
-               domain = (Set *) map.get(domain);
-               domains.push(domain);
-       }
        Set *range;
        myread(&range, sizeof(Set *));
        ASSERT(map.contains(range));
        range = (Set *) map.get(range);
        OverFlowBehavior overflowbehavior;
        myread(&overflowbehavior, sizeof(OverFlowBehavior));
-       map.put(fo_ptr, solver->createFunctionOperator(op, domains.expose(), size, range, overflowbehavior));
+       map.put(fo_ptr, solver->createFunctionOperator(op, range, overflowbehavior));
 }
 
 void Deserializer::deserializeFunctionTable() {
index 84e9ad6..952684a 100644 (file)
@@ -12,8 +12,7 @@ int main(int numargs, char **argv) {
        solver->mustHaveValue(e1);
        solver->mustHaveValue(e2);
        
-       Set *domain[] = {s1, s2};
-       Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
+       Predicate *equals = solver->createPredicateOperator(SATC_EQUALS);
        Element *inputs[] = {e1, e2};
        BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
        b = solver->applyLogicalOperation(SATC_NOT, b);
index e01fb8f..e2319f5 100644 (file)
@@ -22,17 +22,16 @@ int main(int numargs, char **argv) {
        Set *setbig = solver->createSet(0, setbigarray, 5);
        Element *e1 = solver->getElementVar(s);
        Element *e2 = solver->getElementVar(s);
-       Set *domain[] = {s, s};
-       Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
+       Predicate *equals = solver->createPredicateOperator(SATC_EQUALS);
        Element *inputs[] = {e1, e2};
        BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
        solver->addConstraint(b);
 
        uint64_t set2[] = {2, 3};
        Set *rangef1 = solver->createSet(1, set2, 2);
-       Function *f1 = solver->createFunctionOperator(SATC_ADD, domain, 2, setbig, SATC_IGNORE);
+       Function *f1 = solver->createFunctionOperator(SATC_ADD, setbig, SATC_IGNORE);
 
-       Table *table = solver->createTable(domain, 2, s);
+       Table *table = solver->createTable(s);
        uint64_t row1[] = {0, 1};
        uint64_t row2[] = {1, 1};
        uint64_t row3[] = {2, 1};
@@ -45,8 +44,7 @@ int main(int numargs, char **argv) {
        BooleanEdge overflow = solver->getBooleanVar(2);
        Element *e3 = solver->applyFunction(f1, inputs, 2, overflow);
        Element *e4 = solver->applyFunction(f2, inputs, 2, overflow);
-       Set *domain2[] = {s,rangef1};
-       Predicate *equal2 = solver->createPredicateOperator(SATC_EQUALS, domain2, 2);
+       Predicate *equal2 = solver->createPredicateOperator(SATC_EQUALS);
        Element *inputs2 [] = {e4, e3};
        BooleanEdge pred = solver->applyPredicate(equal2, inputs2, 2);
        solver->addConstraint(pred);
index f7ab9d3..ab80067 100644 (file)
@@ -23,18 +23,16 @@ int main(int numargs, char **argv) {
        Element *e2 = solver->getElementVar(s2);
        solver->mustHaveValue(e1);
        solver->mustHaveValue(e2);
-       Set *domain[] = {s1, s2};
        Element *inputs[] = {e1, e2};
 
        uint64_t set2[] = {3};
        Set *rangef1 = solver->createSet(1, set2, 1);
-       Function *f1 = solver->createFunctionOperator(SATC_ADD, domain, 2, rangef1, SATC_FLAGIFFOVERFLOW);
+       Function *f1 = solver->createFunctionOperator(SATC_ADD, rangef1, SATC_FLAGIFFOVERFLOW);
 
        BooleanEdge overflow = solver->getBooleanVar(2);
        Element *e3 = solver->applyFunction(f1, inputs, 2, overflow);
        Element *e4 = solver->getElementConst(5, 3);
-       Set *domain2[] = {rangef1,rangef1};
-       Predicate *equal2 = solver->createPredicateOperator(SATC_EQUALS, domain2, 2);
+       Predicate *equal2 = solver->createPredicateOperator(SATC_EQUALS);
        Element *inputs2 [] = {e4, e3};
        BooleanEdge pred = solver->applyPredicate(equal2, inputs2, 2);
        solver->addConstraint(pred);
index bdb8898..ab2c1ab 100644 (file)
@@ -11,8 +11,7 @@ int main (int num, char** args){
         void *s2 = createSet(solver,0, set2, 3);
         void *e1 = getElementVar(solver,s1);
         void *e2 = getElementVar(solver,s2);
-        void *domain[] = {s1, s2};
-        void *equals = createPredicateOperator(solver,SATC_EQUALS, domain, 2);
+        void *equals = createPredicateOperator(solver,SATC_EQUALS);
         void *inputs[] = {e1, e2};
         void* b = applyPredicate(solver,equals, inputs, 2);
         addConstraint(solver,b);
index b270524..5c95552 100644 (file)
@@ -6,8 +6,7 @@ int main(int numargs, char **argv) {
        Set *s = solver->createSet(1, elements, 2);
        Element *e1 = solver->getElementVar(s);
        Element *e2 = solver->getElementVar(s);
-       Set *sarray[] = {s, s};
-       Predicate *p = solver->createPredicateOperator(SATC_LT, sarray, 2);
+       Predicate *p = solver->createPredicateOperator(SATC_LT);
        Element *earray[] = {e1, e2};
        BooleanEdge be = solver->applyPredicate(p, earray, 2);
        solver->addConstraint(be);
index e041cb0..830103f 100644 (file)
@@ -19,8 +19,7 @@ int main(int numargs, char **argv) {
        Set *s2 = solver->createSet(0, set2, 3);
        Element *e1 = solver->getElementVar(s1);
        Element *e2 = solver->getElementVar(s2);
-       Set *domain[] = {s1, s2};
-       Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
+       Predicate *equals = solver->createPredicateOperator(SATC_EQUALS);
        Element *inputs[] = {e1, e2};
        BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
        solver->addConstraint(b);
index 123d6cd..e179bae 100644 (file)
@@ -14,8 +14,7 @@ int main(int numargs, char **argv) {
        Set *s2 = solver->createSet(0, set2, 2);
        Element *e1 = solver->getElementVar(s1);
        Element *e2 = solver->getElementVar(s2);
-       Set *domain[] = {s1, s2};
-       Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
+       Predicate *equals = solver->createPredicateOperator(SATC_EQUALS);
        Element *inputs[] = {e1, e2};
        BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
        solver->addConstraint(b);
index 72a0a83..a6a482a 100644 (file)
@@ -32,12 +32,11 @@ int main(int numargs, char **argv) {
        Element *e2 = solver->getElementVar(s2);
        Element *e7 = solver->getElementVar(s5);
        BooleanEdge overflow = solver->getBooleanVar(2);
-       Set *d1[] = {s1, s2};
        //change the overflow flag
-       Function *f1 = solver->createFunctionOperator(SATC_SUB, d1, 2, s2, SATC_IGNORE);
+       Function *f1 = solver->createFunctionOperator(SATC_SUB, s2, SATC_IGNORE);
        Element *in1[] = {e1, e2};
        Element *e3 = solver->applyFunction(f1, in1, 2, overflow);
-       Table *t1 = solver->createTable(d1, 2, s3);
+       Table *t1 = solver->createTable(s3);
        uint64_t row1[] = {6, 2};
        uint64_t row2[] = {6, 4};
        solver->addTableEntry(t1, row1, 2, 3);
@@ -45,17 +44,15 @@ int main(int numargs, char **argv) {
        Function *f2 = solver->completeTable(t1, SATC_IGNOREBEHAVIOR);
        Element *e4 = solver->applyFunction(f2, in1, 2, overflow);
 
-       Set *d2[] = {s1};
        Element *in2[] = {e1};
-       Table *t2 = solver->createTable(d2, 1, s1);
+       Table *t2 = solver->createTable(s1);
        uint64_t row3[] = {6};
        solver->addTableEntry(t2, row3, 1, 6);
        Function *f3 = solver->completeTable(t2, SATC_IGNOREBEHAVIOR);
        Element *e5 = solver->applyFunction(f3, in2, 1, overflow);
 
-       Set *d3[] = {s2, s3, s1};
        Element *in3[] = {e3, e4, e5};
-       Table *t3 = solver->createTable(d3, 3, s4);
+       Table *t3 = solver->createTable(s4);
        uint64_t row4[] = {4, 3, 6};
        uint64_t row5[] = {2, 1, 6};
        uint64_t row6[] = {2, 3, 6};
@@ -67,8 +64,7 @@ int main(int numargs, char **argv) {
        Function *f4 = solver->completeTable(t3, SATC_IGNOREBEHAVIOR);
        Element *e6 = solver->applyFunction(f4, in3, 3, overflow);
 
-       Set *deq[] = {s5,s4};
-       Predicate *gt = solver->createPredicateOperator(SATC_GT, deq, 2);
+       Predicate *gt = solver->createPredicateOperator(SATC_GT);
        Element *inputs2 [] = {e7, e6};
        BooleanEdge pred = solver->applyPredicate(gt, inputs2, 2);
        solver->addConstraint(pred);
index 11a315c..91d169d 100644 (file)
@@ -13,8 +13,7 @@ int main(int numargs, char **argv) {
        Set *s3 = solver->createSet(0, set3, 4);
        Element *e1 = solver->getElementConst(4, 5);
        Element *e2 = solver->getElementVar(s3);
-       Set *domain2[] = {s1, s3};
-       Predicate *lt = solver->createPredicateOperator(SATC_LT, domain2, 2);
+       Predicate *lt = solver->createPredicateOperator(SATC_LT);
        Element *inputs2[] = {e1, e2};
        BooleanEdge b = solver->applyPredicate(lt, inputs2, 2);
        solver->addConstraint(b);
index 680d1c6..a6c1f09 100644 (file)
@@ -25,9 +25,8 @@ int main(int numargs, char **argv) {
        Element *e2 = solver->getElementVar(s2);
        Element *e4 = solver->getElementVar(s3);
        BooleanEdge overflow = solver->getBooleanVar(2);
-       Set *d1[] = {s1, s2};
        //change the overflow flag
-       Table *t1 = solver->createTable(d1, 2, s2);
+       Table *t1 = solver->createTable(s2);
        uint64_t row1[] = {1, 5};
        uint64_t row2[] = {2, 3};
        uint64_t row3[] = {1, 7};
@@ -44,8 +43,7 @@ int main(int numargs, char **argv) {
        Element *tmparray[] = {e1, e2};
        Element *e3 = solver->applyFunction(f1, tmparray, 2, overflow);
 
-       Set *deq[] = {s3,s2};
-       Predicate *lte = solver->createPredicateOperator(SATC_LTE, deq, 2);
+       Predicate *lte = solver->createPredicateOperator(SATC_LTE);
        Element *inputs2 [] = {e4, e3};
        BooleanEdge pred = solver->applyPredicate(lte, inputs2, 2);
        solver->addConstraint(pred);
index 4007e25..64bbe34 100644 (file)
@@ -25,9 +25,8 @@ int main(int numargs, char **argv) {
        Element *e1 = solver->getElementVar(s1);
        Element *e2 = solver->getElementVar(s2);
        Element *e3 = solver->getElementVar(s3);
-       Set *d2[] = {s1, s2, s3};
        //change the overflow flag
-       Table *t1 = solver->createTableForPredicate(d2, 3);
+       Table *t1 = solver->createTableForPredicate();
        uint64_t row1[] = {1, 5, 6};
        uint64_t row2[] = {2, 3, 19};
        uint64_t row3[] = {1, 3, 19};
@@ -46,14 +45,12 @@ int main(int numargs, char **argv) {
        BooleanEdge b1 = solver->applyPredicateTable(p1, tmparray, 3, undef);
        solver->addConstraint(b1);
 
-       Set *deq[] = {s3,s2};
-       Predicate *gte = solver->createPredicateOperator(SATC_GTE, deq, 2);
+       Predicate *gte = solver->createPredicateOperator(SATC_GTE);
        Element *inputs2 [] = {e3, e2};
        BooleanEdge pred = solver->applyPredicate(gte, inputs2, 2);
        solver->addConstraint(pred);
 
-       Set *d1[] = {s1, s2};
-       Predicate *eq = solver->createPredicateOperator(SATC_EQUALS, d1, 2);
+       Predicate *eq = solver->createPredicateOperator(SATC_EQUALS);
        Element *tmparray2[] = {e1, e2};
        BooleanEdge pred2 = solver->applyPredicate(eq, tmparray2, 2);
        solver->addConstraint(pred2);
index f6b73b0..25e1761 100644 (file)
@@ -50,24 +50,24 @@ void* getBooleanVar(void* solver,unsigned int type){
        return CCSOLVER(solver)->getBooleanVar((VarType) type).getRaw();
 }
 
-void *createFunctionOperator(void* solver,unsigned int op, void **domain, unsigned int numDomain, void *range,unsigned int overflowbehavior){
-       return CCSOLVER(solver)->createFunctionOperator((ArithOp) op, (Set **)domain, (uint) numDomain, (Set *)range, (OverFlowBehavior) overflowbehavior);
+void *createFunctionOperator(void* solver,unsigned int op, void *range,unsigned int overflowbehavior){
+       return CCSOLVER(solver)->createFunctionOperator((ArithOp) op, (Set *)range, (OverFlowBehavior) overflowbehavior);
 }
 
-void *createPredicateOperator(void* solver,unsigned int op, void **domain, unsigned int numDomain){
-       return CCSOLVER(solver)->createPredicateOperator((CompOp) op, (Set **)domain, (uint) numDomain);
+void *createPredicateOperator(void* solver,unsigned int op{
+       return CCSOLVER(solver)->createPredicateOperator((CompOp) op);
 }
 
 void *createPredicateTable(void* solver,void *table, unsigned int behavior){
        return CCSOLVER(solver)->createPredicateTable((Table *)table, (UndefinedBehavior) behavior);
 }
 
-void *createTable(void* solver,void**domains, unsigned int numDomain, void *range){
-       return CCSOLVER(solver)->createTable((Set **)domains, (uint) numDomain, (Set *)range);
+void *createTable(void* solver, void *range){
+       return CCSOLVER(solver)->createTable((Set *)range);
 }
 
-void *createTableForPredicate(void* solver,void**domains, unsigned int numDomain){
-       return CCSOLVER(solver)->createTableForPredicate((Set **)domains, (uint) numDomain);
+void *createTableForPredicate(void* solver{
+       return CCSOLVER(solver)->createTableForPredicate();
 }
 
 void addTableEntry(void* solver,void *table, void *inputs, unsigned int inputSize, long result){
index d8e3921..f98dbf2 100644 (file)
@@ -18,11 +18,11 @@ void *getElementVar(void* solver,void *set);
 void *getElementConst(void* solver,unsigned int type, long value);
 void *getElementRange (void* solver,void *element);
 void* getBooleanVar(void* solver,unsigned int type);
-void *createFunctionOperator(void* solver,unsigned int op, void **domain, unsigned int numDomain, void *range,unsigned int overflowbehavior);
-void *createPredicateOperator(void* solver,unsigned int op, void **domain, unsigned int numDomain);
+void *createFunctionOperator(void* solver,unsigned int op, void *range,unsigned int overflowbehavior);
+void *createPredicateOperator(void* solver,unsigned int op);
 void *createPredicateTable(void* solver,void *table, unsigned int behavior);
-void *createTable(void* solver,void**domains, unsigned int numDomain, void *range);
-void *createTableForPredicate(void* solver,void**domains, unsigned int numDomain);
+void *createTable(void* solver, void *range);
+void *createTableForPredicate(void* solver);
 void addTableEntry(void* solver,void *table, void *inputs, unsigned int inputSize, long result);
 void *completeTable(void* solver,void *table, unsigned int behavior);
 void *applyFunction(void* solver,void *function, void**array, unsigned int numArrays, void* overflowstatus);
index 7c13eae..aca527a 100644 (file)
@@ -263,14 +263,14 @@ Element *CSolver::applyFunction(Function *function, Element **array, uint numArr
        }
 }
 
-Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
-       Function *function = new FunctionOperator(op, domain, numDomain, range, overflowbehavior);
+Function *CSolver::createFunctionOperator(ArithOp op, Set *range, OverFlowBehavior overflowbehavior) {
+       Function *function = new FunctionOperator(op, range, overflowbehavior);
        allFunctions.push(function);
        return function;
 }
 
-Predicate *CSolver::createPredicateOperator(CompOp op, Set **domain, uint numDomain) {
-       Predicate *predicate = new PredicateOperator(op, domain,numDomain);
+Predicate *CSolver::createPredicateOperator(CompOp op) {
+       Predicate *predicate = new PredicateOperator(op);
        allPredicates.push(predicate);
        return predicate;
 }
@@ -281,14 +281,14 @@ Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavio
        return predicate;
 }
 
-Table *CSolver::createTable(Set **domains, uint numDomain, Set *range) {
-       Table *table = new Table(domains,numDomain,range);
+Table *CSolver::createTable(Set *range) {
+       Table *table = new Table(range);
        allTables.push(table);
        return table;
 }
 
-Table *CSolver::createTableForPredicate(Set **domains, uint numDomain) {
-       return createTable(domains, numDomain, NULL);
+Table *CSolver::createTableForPredicate() {
+       return createTable(NULL);
 }
 
 void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
@@ -704,4 +704,4 @@ void CSolver::autoTune(uint budget) {
 //        }
 //        va_end(args);
 //        return createSet(set->getType(), members, newSize);
-//}
\ No newline at end of file
+//}
index c5c3b8d..e02e340 100644 (file)
@@ -69,20 +69,20 @@ public:
 
        /** This function creates a function operator. */
 
-       Function *createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,
+       Function *createFunctionOperator(ArithOp op, Set *range,
                                                                                                                                         OverFlowBehavior overflowbehavior);
 
        /** This function creates a predicate operator. */
 
-       Predicate *createPredicateOperator(CompOp op, Set **domain, uint numDomain);
+       Predicate *createPredicateOperator(CompOp op);
 
        Predicate *createPredicateTable(Table *table, UndefinedBehavior behavior);
 
        /** This function creates an empty instance table.*/
 
-       Table *createTable(Set **domains, uint numDomain, Set *range);
+       Table *createTable(Set *range);
 
-       Table *createTableForPredicate(Set **domains, uint numDomain);
+       Table *createTableForPredicate();
        /** This function adds an input output relation to a table. */
 
        void addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result);