remove redundant domains

diff --git a/src/AST/function.cc b/src/AST/function.cc
index ccd89dd28c624d32714df88787715ef83dbc84e3..9f43fbe4c0c2323da185568e05974fb864797358 100644 (file)
--- a/src/AST/function.cc
+++ b/src/AST/function.cc
@@ -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));
 }

diff --git a/src/AST/function.h b/src/AST/function.h
index 5cfbb7d4117a5169312d5910b776b116a3aeb014..2d65f61a009d0e4d6d744b527bbb7aadf37edf21 100644 (file)
--- a/src/AST/function.h
+++ b/src/AST/function.h
@@ -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);

diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc
index 80e8a5e38e5be4aee0fad516ef9d4fb67fc0d03e..3657ecc04deae73b79c750a9b73de0a5d0a33927 100644 (file)
--- a/src/AST/predicate.cc
+++ b/src/AST/predicate.cc
@@ -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() {

diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index 812d4bda8ec4d4abb70915fb9d8ae98923b3abce..17e34d948c88eebe7516992dd472cfe2be9b988a 100644 (file)
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -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:

diff --git a/src/AST/table.cc b/src/AST/table.cc
index 513935dab5bd4bff7736ca5bf1d3128eba673224..da0188a59af4ed5b5a8a29c0771528a6d0cc0b34 100644 (file)
--- a/src/AST/table.cc
+++ b/src/AST/table.cc
@@ -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();

diff --git a/src/AST/table.h b/src/AST/table.h
index c196d3cf0801db83449123b45905663ba7e1b80d..bd5bf182bfff4eebb7c6623e79991d009a395fdc 100644 (file)
--- a/src/AST/table.h
+++ b/src/AST/table.h
@@ -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;
 };

diff --git a/src/ASTTransform/elementopt.cc b/src/ASTTransform/elementopt.cc
index 162661b1d69c662470f2e28ae22627f3618dce2e..5fa38e6684cf2baf772e2440654df485575f7263 100755 (executable)
--- a/src/ASTTransform/elementopt.cc
+++ b/src/ASTTransform/elementopt.cc
@@ -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;
        }
 }

diff --git a/src/ASTTransform/elementopt.h b/src/ASTTransform/elementopt.h
index 0c4acd278ac560f4e5935421bb6936b11bbd9a3b..ad6e7902dd05004bec307e2c364d732260c584da 100755 (executable)
--- a/src/ASTTransform/elementopt.h
+++ b/src/ASTTransform/elementopt.h
@@ -11,6 +11,7 @@ public:
 
        CMEMALLOC;
 private:
+       void processPredicate(BooleanPredicate *);
 };
 
 #endif

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 5e4bfb8d9b30ab0515eaba20a7c9de88604e0c8d..6be73ea9bfbf648d7e2eac98e8610a98c6c8aff6 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -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);

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index b80978ec0c5a620809544b08376171d939729662..3266f1ca9e5f3be1d9473c3a3be1ffa969d88400 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -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);

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 1fea1a58f41ebf23391bba824a6744bc84662ae8..0cfce9bec8814031d6f5c240c3b6ebc18c2a61e0 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -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);

diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index 9237eccb2cfded8de3f999f7e4277f523f49e675..3510d118175d5fa5494381e7ee6b2c64c68cd155 100644 (file)
--- a/src/Backend/satfunctableencoder.cc
+++ b/src/Backend/satfunctableencoder.cc
@@ -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);

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index 56acc523676c382af2a15edb3a1abebd76f243eb..42b565e1cf962a8ea2f52bfecc2e7951cd42b603 100644 (file)
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -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() {

diff --git a/src/Test/anyvaluetest.cc b/src/Test/anyvaluetest.cc
index 84e9ad6c885719f0705ad1b00546705c0c573c43..952684a2cc5d427e3295682e032558bbe8a4d19c 100644 (file)
--- a/src/Test/anyvaluetest.cc
+++ b/src/Test/anyvaluetest.cc
@@ -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);

diff --git a/src/Test/buildconstraintstest.cc b/src/Test/buildconstraintstest.cc
index e01fb8f8e315aeb7032f7a6345948b8a2fed2ce9..e2319f5a7b58f69428752513c38f29b9fcb04616 100644 (file)
--- a/src/Test/buildconstraintstest.cc
+++ b/src/Test/buildconstraintstest.cc
@@ -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);

diff --git a/src/Test/buildsimple.cc b/src/Test/buildsimple.cc
index f7ab9d32c1ee4c0c03294adf3968329762ca83fc..ab80067347d79fa3898252bb4c9abcbb21f2d338 100644 (file)
--- a/src/Test/buildsimple.cc
+++ b/src/Test/buildsimple.cc
@@ -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);

diff --git a/src/Test/ccsolvertest.c b/src/Test/ccsolvertest.c
index bdb8898f05267e0f1651417c1eb92d970aa72f86..ab2c1abb394a5595d9e4e6918ac0081eba977f60 100644 (file)
--- a/src/Test/ccsolvertest.c
+++ b/src/Test/ccsolvertest.c
@@ -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);

diff --git a/src/Test/constraint.cc b/src/Test/constraint.cc
index b270524b70785ffc4ccbad6b0377e664d69a88f9..5c955520371ad24883b60c2d4d7c2de95d59b08c 100644 (file)
--- a/src/Test/constraint.cc
+++ b/src/Test/constraint.cc
@@ -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);

diff --git a/src/Test/elemequalsattest.cc b/src/Test/elemequalsattest.cc
index e041cb0a1dd2155a689cdcb69d070e800657f518..830103fa76dfb1088dce984f55775da67dfc5cbe 100644 (file)
--- a/src/Test/elemequalsattest.cc
+++ b/src/Test/elemequalsattest.cc
@@ -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);

diff --git a/src/Test/elemequalunsattest.cc b/src/Test/elemequalunsattest.cc
index 123d6cd5916a7b5f207b9ddb9064d7d17daed0ed..e179bae74f49fbf483b74dfc62b8ceef7f22df91 100644 (file)
--- a/src/Test/elemequalunsattest.cc
+++ b/src/Test/elemequalunsattest.cc
@@ -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);

diff --git a/src/Test/funcencodingtest.cc b/src/Test/funcencodingtest.cc
index 72a0a8389a2540069d6e00ac8a705c67f8379cb0..a6a482a7d5d4d39d2239a7ce072d5e596708cd16 100644 (file)
--- a/src/Test/funcencodingtest.cc
+++ b/src/Test/funcencodingtest.cc
@@ -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);

diff --git a/src/Test/ltelemconsttest.cc b/src/Test/ltelemconsttest.cc
index 11a315c8ddaeda1f2ca1f9e53f4b2e3e92702397..91d169d2744ce08295ab6a6343c30190f762720b 100644 (file)
--- a/src/Test/ltelemconsttest.cc
+++ b/src/Test/ltelemconsttest.cc
@@ -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);

diff --git a/src/Test/tablefuncencodetest.cc b/src/Test/tablefuncencodetest.cc
index 680d1c64fc47bf47db01593827a05d168d42196f..a6c1f09cdc8e5d3e4b78bc50f3c2f1e727f8e1b6 100644 (file)
--- a/src/Test/tablefuncencodetest.cc
+++ b/src/Test/tablefuncencodetest.cc
@@ -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);

diff --git a/src/Test/tablepredicencodetest.cc b/src/Test/tablepredicencodetest.cc
index 4007e2539016798e72843e68ad89b0f6c57d14a1..64bbe34eec9e88277c261831a1c65c7b6faf1da2 100644 (file)
--- a/src/Test/tablepredicencodetest.cc
+++ b/src/Test/tablepredicencodetest.cc
@@ -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);

diff --git a/src/ccsolver.cc b/src/ccsolver.cc
index f6b73b0ee21a7082ed51010cd0465bd77e554f22..25e176172cd7abfcb1d86af445805b84e4dbe4bf 100644 (file)
--- a/src/ccsolver.cc
+++ b/src/ccsolver.cc
@@ -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){

diff --git a/src/ccsolver.h b/src/ccsolver.h
index d8e392150ec0cb06dd3b07f3ad5c350eef74f8e1..f98dbf266a257033b98d669c3c1fecec7cdf80c0 100644 (file)
--- a/src/ccsolver.h
+++ b/src/ccsolver.h
@@ -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);

diff --git a/src/csolver.cc b/src/csolver.cc
index 7c13eae9c8bebe007000abf801f735522dd36d67..aca527a3ec9769c4c6fefeb6242a6c4bf5c648f4 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -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
+//}

diff --git a/src/csolver.h b/src/csolver.h
index c5c3b8d6fff90869b2be6338a3c0bcd3c477bfb1..e02e3407c626928aa9a810a96518ad951a5d5c16 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -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);