From e8931de7f86b261c61d8b39a33df4c8bc54dc928 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 23 Jul 2018 16:42:41 -0700 Subject: [PATCH] remove redundant domains --- src/AST/function.cc | 20 ++-------------- src/AST/function.h | 3 +-- src/AST/predicate.cc | 19 ++------------- src/AST/predicate.h | 3 +-- src/AST/table.cc | 25 ++++--------------- src/AST/table.h | 6 +---- src/ASTTransform/elementopt.cc | 29 ++++++++++++++++++++++ src/ASTTransform/elementopt.h | 1 + src/ASTTransform/integerencoding.cc | 3 +-- src/Backend/satelemencoder.cc | 2 +- src/Backend/satfuncopencoder.cc | 6 ++--- src/Backend/satfunctableencoder.cc | 12 +++++----- src/Serialize/deserializer.cc | 37 ++++------------------------- src/Test/anyvaluetest.cc | 3 +-- src/Test/buildconstraintstest.cc | 10 ++++---- src/Test/buildsimple.cc | 6 ++--- src/Test/ccsolvertest.c | 3 +-- src/Test/constraint.cc | 3 +-- src/Test/elemequalsattest.cc | 3 +-- src/Test/elemequalunsattest.cc | 3 +-- src/Test/funcencodingtest.cc | 14 ++++------- src/Test/ltelemconsttest.cc | 3 +-- src/Test/tablefuncencodetest.cc | 6 ++--- src/Test/tablepredicencodetest.cc | 9 +++---- src/ccsolver.cc | 16 ++++++------- src/ccsolver.h | 8 +++---- src/csolver.cc | 18 +++++++------- src/csolver.h | 8 +++---- 28 files changed, 103 insertions(+), 176 deletions(-) diff --git a/src/AST/function.cc b/src/AST/function.cc index ccd89dd..9f43fbe 100644 --- 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 5cfbb7d..2d65f61 100644 --- a/src/AST/function.h +++ b/src/AST/function.h @@ -21,10 +21,9 @@ public: class FunctionOperator : public Function { public: ArithOp op; - Array 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 80e8a5e..3657ecc 100644 --- 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 812d4bd..17e34d9 100644 --- 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 domains; CompOp getOp() {return op;} CMEMALLOC; private: diff --git a/src/AST/table.cc b/src/AST/table.cc index 513935d..da0188a 100644 --- 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 c196d3c..bd5bf18 100644 --- 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 domains; Set *range; HashsetTableEntry *entries; }; diff --git a/src/ASTTransform/elementopt.cc b/src/ASTTransform/elementopt.cc index 162661b..5fa38e6 100755 --- 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 0c4acd2..ad6e790 100755 --- 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 5e4bfb8..6be73ea 100644 --- 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 b80978e..3266f1c 100644 --- 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 1fea1a5..0cfce9b 100644 --- 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 9237ecc..3510d11 100644 --- 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 56acc52..42b565e 100644 --- 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 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 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 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 84e9ad6..952684a 100644 --- 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 e01fb8f..e2319f5 100644 --- 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 f7ab9d3..ab80067 100644 --- 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 bdb8898..ab2c1ab 100644 --- 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 b270524..5c95552 100644 --- 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 e041cb0..830103f 100644 --- 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 123d6cd..e179bae 100644 --- 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 72a0a83..a6a482a 100644 --- 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 11a315c..91d169d 100644 --- 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 680d1c6..a6c1f09 100644 --- 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 4007e25..64bbe34 100644 --- 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 f6b73b0..25e1761 100644 --- 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 d8e3921..f98dbf2 100644 --- 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 7c13eae..aca527a 100644 --- 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 c5c3b8d..e02e340 100644 --- 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); -- 2.34.1