edits

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 0a415b918f53a169f37b32719522f525a831af60..3d7ab5c885f96db0fb94e4079ccd1ed906a2f8b4 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -9,29 +9,29 @@
 #include "set.h"
 
 
-void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
+void orderIntegerEncodingSATEncoder(CSolver *solver, BooleanOrder *boolOrder) {
        Order *order = boolOrder->order;
        if (order->elementTable == NULL) {
                order->initializeOrderElementsHashTable();
        }
        //getting two elements and using LT predicate ...
-       ElementSet *elem1 = (ElementSet *)getOrderIntegerElement(This, order, boolOrder->first);
-       ElementSet *elem2 = (ElementSet *)getOrderIntegerElement(This, order, boolOrder->second);
+       ElementSet *elem1 = (ElementSet *)getOrderIntegerElement(solver, order, boolOrder->first);
+       ElementSet *elem2 = (ElementSet *)getOrderIntegerElement(solver, order, boolOrder->second);
        Set *sarray[] = {elem1->set, elem2->set};
-       Predicate *predicate = This->solver->createPredicateOperator(LT, sarray, 2);
+       Predicate *predicate = solver->createPredicateOperator(LT, sarray, 2);
        Element *parray[] = {elem1, elem2};
-       Boolean *boolean = This->solver->applyPredicate(predicate, parray, 2);
-       This->solver->addConstraint(boolean);
-       This->solver->replaceBooleanWithBoolean(boolOrder, boolean);
+       Boolean *boolean = solver->applyPredicate(predicate, parray, 2);
+       solver->addConstraint(boolean);
+       solver->replaceBooleanWithBoolean(boolOrder, boolean);
 }
 
 
-Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item) {
+Element *getOrderIntegerElement(CSolver * solver, Order *order, uint64_t item) {
        HashSetOrderElement *eset = order->elementTable;
        OrderElement oelement(item, NULL);
        if ( !eset->contains(&oelement)) {
-               Set *set = This->solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize());
-               Element *elem = This->solver->getElementVar(set);
+               Set *set = solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize());
+               Element *elem = solver->getElementVar(set);
                eset->add(new OrderElement(item, elem));
                return elem;
        } else

diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h
index 15fbdd71682ee26037f35be69ec2990889d27256..2288dab431579cec6559ea8e08415fdd9a7af9fb 100644 (file)
--- a/src/ASTTransform/integerencoding.h
+++ b/src/ASTTransform/integerencoding.h
@@ -16,9 +16,8 @@
 #include "classlist.h"
 #include "structs.h"
 
-Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item);
-void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder);
-
+Element *getOrderIntegerElement(CSolver *solver, Order *order, uint64_t item);
+void orderIntegerEncodingSATEncoder(CSolver *solver, BooleanOrder *boolOrder);
 
 #endif/* INTEGERENCODING_H */
 

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 1c36cd15d44b32eac6420ea4367febe6aca7820c..201d7dba172f77db67b0bfbfb1a9ae51ef5ba0c6 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -328,10 +328,16 @@ Edge constraintNewVar(CNF *cnf) {
 }
 
 int solveCNF(CNF *cnf) {
+       long long startTime=getTimeNano();
        countPass(cnf);
        convertPass(cnf, false);
        finishedClauses(cnf->solver);
-       return solve(cnf->solver);
+       long long startSolve=getTimeNano();
+       int result = solve(cnf->solver);
+       long long finishTime=getTimeNano();
+       cnf->encodeTime=startSolve-startTime;
+       cnf->solveTime=finishTime-startSolve;
+       return result;
 }
 
 bool getValueCNF(CNF *cnf, Edge var) {

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 02fe3da617731c300e8d6a9adbb4f4cd009ab229..2f61d72a41e31d86acd1ca814a7eb3df43ff38e5 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -63,6 +63,8 @@ struct CNF {
        IncrementalSolver *solver;
        VectorEdge constraints;
        VectorEdge args;
+       long long solveTime;
+       long long encodeTime;
 };
 
 typedef struct CNF CNF;

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 8513d924f5c50826598529d18dbe0049f9010ed7..504f92c88216f697e4f8afdbc72a19debdf65e9f 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -32,7 +32,7 @@ Edge getElementValueBinaryIndexConstraint(SATEncoder *This, Element *elem, uint6
        ElementEncoding *elemEnc = getElementEncoding(elem);
        for (uint i = 0; i < elemEnc->encArraySize; i++) {
                if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
-                       return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
+                       return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(This->getCNF(), elemEnc->numVars, elemEnc->variables, i);
                }
        }
        return E_False;
@@ -63,7 +63,7 @@ Edge getElementValueUnaryConstraint(SATEncoder *This, Element *elem, uint64_t va
                        else if ((i + 1) == elemEnc->encArraySize)
                                return elemEnc->variables[i - 1];
                        else
-                               return constraintAND2(This->cnf, elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i]));
+                               return constraintAND2(This->getCNF(), elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i]));
                }
        }
        return E_False;
@@ -83,7 +83,7 @@ Edge getElementValueBinaryValueConstraint(SATEncoder *This, Element *element, ui
        }
 
        uint64_t valueminusoffset = value - elemEnc->offset;
-       return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, valueminusoffset);
+       return generateBinaryConstraint(This->getCNF(), elemEnc->numVars, elemEnc->variables, valueminusoffset);
 }
 
 void allocElementConstraintVariables(ElementEncoding *This, uint numVars) {
@@ -108,10 +108,10 @@ void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
        getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
        for (uint i = 0; i < encoding->numVars; i++) {
                for (uint j = i + 1; j < encoding->numVars; j++) {
-                       addConstraintCNF(This->cnf, constraintNegate(constraintAND2(This->cnf, encoding->variables[i], encoding->variables[j])));
+                       addConstraintCNF(This->getCNF(), constraintNegate(constraintAND2(This->getCNF(), encoding->variables[i], encoding->variables[j])));
                }
        }
-       addConstraintCNF(This->cnf, constraintOR(This->cnf, encoding->numVars, encoding->variables));
+       addConstraintCNF(This->getCNF(), constraintOR(This->getCNF(), encoding->numVars, encoding->variables));
 }
 
 void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
@@ -119,7 +119,7 @@ void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
        getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
        //Add unary constraint
        for (uint i = 1; i < encoding->numVars; i++) {
-               addConstraintCNF(This->cnf, constraintOR2(This->cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
+               addConstraintCNF(This->getCNF(), constraintOR2(This->getCNF(), encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
        }
 }
 

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index a7513d6120eb9180c8b33f127742b4f625e21597..977147f6159f8802c0be90ce39c91d0d3ab83e4a 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -16,7 +16,6 @@
 //TODO: Should handle sharing of AST Nodes without recoding them a second time
 
 SATEncoder::SATEncoder(CSolver * _solver) :
-       varcount(1),
        cnf(createCNF()),
        solver(_solver) {
 }
@@ -25,6 +24,10 @@ SATEncoder::~SATEncoder() {
        deleteCNF(cnf);
 }
 
+int SATEncoder::solve() {
+       return solveCNF(cnf);
+}
+
 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
        HSIteratorBoolean *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
@@ -60,7 +63,7 @@ void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray) {
 }
 
 Edge getNewVarSATEncoder(SATEncoder *This) {
-       return constraintNewVar(This->cnf);
+       return constraintNewVar(This->getCNF());
 }
 
 Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint) {
@@ -77,15 +80,15 @@ Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint) {
 
        switch (constraint->op) {
        case L_AND:
-               return constraintAND(This->cnf, constraint->inputs.getSize(), array);
+               return constraintAND(This->getCNF(), constraint->inputs.getSize(), array);
        case L_OR:
-               return constraintOR(This->cnf, constraint->inputs.getSize(), array);
+               return constraintOR(This->getCNF(), constraint->inputs.getSize(), array);
        case L_NOT:
                return constraintNegate(array[0]);
        case L_XOR:
-               return constraintXOR(This->cnf, array[0], array[1]);
+               return constraintXOR(This->getCNF(), array[0], array[1]);
        case L_IMPLIES:
-               return constraintIMPLIES(This->cnf, array[0], array[1]);
+               return constraintIMPLIES(This->getCNF(), array[0], array[1]);
        default:
                model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
                exit(-1);

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index f74965b4af8ac92333ca5041d3487e7cacbd7ae7..f88e99370f641aabeef1a5e84e6aefa4fb83123c 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -12,26 +12,30 @@
 
 class SATEncoder {
  public:
-       uint varcount;
-       CNF *cnf;
-       CSolver *solver;
-
+       int solve();
        SATEncoder(CSolver *solver);
        ~SATEncoder();
        void encodeAllSATEncoder(CSolver *csolver);
        Edge encodeConstraintSATEncoder(Boolean *constraint);
+       CNF * getCNF() { return cnf;}
+       CSolver * getSolver() { return solver; }
+       long long getSolveTime() { return cnf->solveTime; }
+       long long getEncodeTime() { return cnf->encodeTime; }
+       
        MEMALLOC;
+ private:
+       CNF *cnf;
+       CSolver *solver;
 };
 
+Edge getNewVarSATEncoder(SATEncoder *This);
+void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray);
 
-       Edge getNewVarSATEncoder(SATEncoder *This);
-       void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray);
-
-       Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint);
-       Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint);
-       Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-       Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-       void encodeElementSATEncoder(SATEncoder *encoder, Element *This);
-       void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
-       void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
+Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint);
+Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint);
+Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
+Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
+void encodeElementSATEncoder(SATEncoder *encoder, Element *This);
+void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
+void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
 #endif

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 695493bb38d583212b44e313690e12794b8fe8e3..597f66bfb89432bf1bd91bbf60ec04a65481491c 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -56,7 +56,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c
                                Element *elem = constraint->inputs.get(i);
                                carray[i] = getElementValueConstraint(This, elem, vals[i]);
                        }
-                       Edge term = constraintAND(This->cnf, numDomains, carray);
+                       Edge term = constraintAND(This->getCNF(), numDomains, carray);
                        pushVectorEdge(clauses, term);
                }
 
@@ -79,7 +79,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c
                deleteVectorEdge(clauses);
                return E_False;
        }
-       Edge cor = constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       Edge cor = constraintOR(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
        deleteVectorEdge(clauses);
        return generateNegation ? constraintNegate(cor) : cor;
 }
@@ -137,26 +137,26 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *
                        case IGNORE:
                        case NOOVERFLOW:
                        case WRAPAROUND: {
-                               clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+                               clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]);
                                break;
                        }
                        case FLAGFORCESOVERFLOW: {
-                               clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
+                               clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), constraintAND2(This->getCNF(), carray[numDomains], constraintNegate(overFlowConstraint)));
                                break;
                        }
                        case OVERFLOWSETSFLAG: {
                                if (isInRange) {
-                                       clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+                                       clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]);
                                } else {
-                                       clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
+                                       clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), overFlowConstraint);
                                }
                                break;
                        }
                        case FLAGIFFOVERFLOW: {
                                if (isInRange) {
-                                       clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
+                                       clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), constraintAND2(This->getCNF(), carray[numDomains], constraintNegate(overFlowConstraint)));
                                } else {
-                                       clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
+                                       clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), overFlowConstraint);
                                }
                                break;
                        }
@@ -190,8 +190,8 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *
                deleteVectorEdge(clauses);
                return;
        }
-       Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-       addConstraintCNF(This->cnf, cor);
+       Edge cor = constraintAND(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       addConstraintCNF(This->getCNF(), cor);
        deleteVectorEdge(clauses);
 }
 
@@ -207,11 +207,11 @@ Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *c
        uint numVars = ee0->numVars;
        switch (predicate->op) {
        case EQUALS:
-               return generateEquivNVConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
+               return generateEquivNVConstraint(This->getCNF(), numVars, ee0->variables, ee1->variables);
        case LT:
-               return generateLTConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
+               return generateLTConstraint(This->getCNF(), numVars, ee0->variables, ee1->variables);
        case GT:
-               return generateLTConstraint(This->cnf, numVars, ee1->variables, ee0->variables);
+               return generateLTConstraint(This->getCNF(), numVars, ee1->variables, ee0->variables);
        default:
                ASSERT(0);
        }

diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index 1c5e58cb425baa1adce1b993c358309e7563689f..b2e04ccf463f265b971c2abf24bba0bc3d9770a9 100644 (file)
--- a/src/Backend/satfunctableencoder.cc
+++ b/src/Backend/satfunctableencoder.cc
@@ -42,14 +42,14 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat
                Edge row;
                switch (undefStatus) {
                case IGNOREBEHAVIOR:
-                       row = constraintAND(This->cnf, inputNum, carray);
+                       row = constraintAND(This->getCNF(), inputNum, carray);
                        break;
                case FLAGFORCEUNDEFINED: {
-                       addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray),  constraintNegate(undefConst)));
+                       addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), inputNum, carray),  constraintNegate(undefConst)));
                        if (generateNegation == (entry->output != 0)) {
                                continue;
                        }
-                       row = constraintAND(This->cnf, inputNum, carray);
+                       row = constraintAND(This->getCNF(), inputNum, carray);
                        break;
                }
                default:
@@ -62,8 +62,8 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat
        }
        delete iterator;
        ASSERT(i != 0);
-       Edge result = generateNegation ? constraintNegate(constraintOR(This->cnf, i, constraints))
-                                                               : constraintOR(This->cnf, i, constraints);
+       Edge result = generateNegation ? constraintNegate(constraintOR(This->getCNF(), i, constraints))
+                                                               : constraintOR(This->getCNF(), i, constraints);
        printCNF(result);
        return result;
 }
@@ -120,17 +120,17 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons
                switch (predicate->undefinedbehavior) {
                case UNDEFINEDSETSFLAG:
                        if (isInRange) {
-                               clause = constraintAND(This->cnf, numDomains, carray);
+                               clause = constraintAND(This->getCNF(), numDomains, carray);
                        } else {
-                               addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint) );
+                               addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), undefConstraint) );
                        }
                        break;
                case FLAGIFFUNDEFINED:
                        if (isInRange) {
-                               clause = constraintAND(This->cnf, numDomains, carray);
-                               addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint)));
+                               clause = constraintAND(This->getCNF(), numDomains, carray);
+                               addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), constraintNegate(undefConstraint)));
                        } else {
-                               addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint) );
+                               addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), undefConstraint) );
                        }
                        break;
 
@@ -164,9 +164,9 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons
        }
        Edge result = E_NULL;
        ASSERT(getSizeVectorEdge(clauses) != 0);
-       result = constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       result = constraintOR(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
        if (hasOverflow) {
-               result = constraintOR2(This->cnf, result, undefConstraint);
+               result = constraintOR2(This->getCNF(), result, undefConstraint);
        }
        if (generateNegation) {
                ASSERT(!hasOverflow);
@@ -198,12 +198,12 @@ void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction
                Edge row;
                switch (undefStatus ) {
                case IGNOREBEHAVIOR: {
-                       row = constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output);
+                       row = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), inputNum, carray), output);
                        break;
                }
                case FLAGFORCEUNDEFINED: {
                        Edge undefConst = This->encodeConstraintSATEncoder(func->overflowstatus);
-                       row = constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
+                       row = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), inputNum, carray), constraintAND2(This->getCNF(), output, constraintNegate(undefConst)));
                        break;
                }
                default:
@@ -213,7 +213,7 @@ void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction
                constraints[i++] = row;
        }
        delete iterator;
-       addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
+       addConstraintCNF(This->getCNF(), constraintAND(This->getCNF(), size, constraints));
 }
 
 void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *elemFunc) {
@@ -270,18 +270,18 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el
                case UNDEFINEDSETSFLAG: {
                        if (isInRange) {
                                //FIXME: Talk to Brian, It should be IFF not only IMPLY. --HG
-                               clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+                               clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]);
                        } else {
-                               addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint));
+                               addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), undefConstraint));
                        }
                        break;
                }
                case FLAGIFFUNDEFINED: {
                        if (isInRange) {
-                               clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
-                               addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint) ));
+                               clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]);
+                               addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(), constraintAND(This->getCNF(), numDomains, carray), constraintNegate(undefConstraint) ));
                        } else {
-                               addConstraintCNF(This->cnf,constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), undefConstraint));
+                               addConstraintCNF(This->getCNF(),constraintIMPLIES(This->getCNF(), constraintAND(This->getCNF(), numDomains, carray), undefConstraint));
                        }
                        break;
                }
@@ -316,7 +316,7 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el
                deleteVectorEdge(clauses);
                return;
        }
-       Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-       addConstraintCNF(This->cnf, cor);
+       Edge cor = constraintAND(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       addConstraintCNF(This->getCNF(), cor);
        deleteVectorEdge(clauses);
 }

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 57447364cfd537b0c999a0845d1772a09a7da886..fc8beb2a3630b371c9ba7c45baab1c307f0060bc 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -79,10 +79,10 @@ Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
        ASSERT(boolOrder->order->type == TOTAL);
        if (boolOrder->order->orderPairTable == NULL) {
                boolOrder->order->initializeOrderHashTable();
-               bool doOptOrderStructure = GETVARTUNABLE(This->solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+               bool doOptOrderStructure = GETVARTUNABLE(This->getSolver()->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
                if (doOptOrderStructure) {
                        boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
-                       reachMustAnalysis(This->solver, boolOrder->order->graph, true);
+                       reachMustAnalysis(This->getSolver(), boolOrder->order->graph, true);
                }
                createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
        }
@@ -111,7 +111,7 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
                                OrderPair pairIK(valueI, valueK, E_NULL);
                                Edge constIK = getPairConstraint(This, order, &pairIK);
                                Edge constJK = getPairConstraint(This, order, &pairJK);
-                               addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
+                               addConstraintCNF(This->getCNF(), generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
                        }
                }
        }
@@ -137,10 +137,10 @@ Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
 
 Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) {
        Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
-       Edge loop1 = constraintOR(This->cnf, 3, carray);
+       Edge loop1 = constraintOR(This->getCNF(), 3, carray);
        Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
-       Edge loop2 = constraintOR(This->cnf, 3, carray2 );
-       return constraintAND2(This->cnf, loop1, loop2);
+       Edge loop2 = constraintOR(This->getCNF(), 3, carray2 );
+       return constraintAND2(This->getCNF(), loop1, loop2);
 }
 
 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {

diff --git a/src/Backend/sattranslator.cc b/src/Backend/sattranslator.cc
index 7b8eae0d8ff16b6b7fc0521aa3af9956eb7dc90a..1cd08156282b9263c03b2a39dc1ebc861e94d9fb 100644 (file)
--- a/src/Backend/sattranslator.cc
+++ b/src/Backend/sattranslator.cc
@@ -10,7 +10,7 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding
        uint index = 0;
        for (int i = elemEnc->numVars - 1; i >= 0; i--) {
                index = index << 1;
-               if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
+               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )))
                        index |= 1;
        }
        if (elemEnc->encArraySize <= index || !elemEnc->isinUseElement(index))
@@ -22,11 +22,11 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding
        uint64_t value = 0;
        for (int i = elemEnc->numVars - 1; i >= 0; i--) {
                value = value << 1;
-               if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
+               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) )
                        value |= 1;
        }
        if (elemEnc->isBinaryValSigned &&
-                       This->getSATEncoder()->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
+                       This->getSATEncoder()->getCNF()->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
                //Do sign extension of negative number
                uint64_t highbits = 0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
                value += highbits;
@@ -38,7 +38,7 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding
 uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
        uint index = 0;
        for (uint i = 0; i < elemEnc->numVars; i++) {
-               if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
+               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )))
                        index = i;
        }
        ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
@@ -48,7 +48,7 @@ uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elem
 uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
        uint i;
        for (i = 0; i < elemEnc->numVars; i++) {
-               if (!getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) {
+               if (!getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) ) {
                        break;
                }
        }
@@ -82,7 +82,7 @@ uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
 
 bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
        int index = getEdgeVar( ((BooleanVar *) boolean)->var );
-       return getValueSolver(This->getSATEncoder()->cnf->solver, index);
+       return getValueSolver(This->getSATEncoder()->getCNF()->solver, index);
 }
 
 HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second) {
@@ -91,6 +91,6 @@ HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order,
        Edge var = getOrderConstraint(order->orderPairTable, &pair);
        if (edgeIsNull(var))
                return UNORDERED;
-       return getValueCNF(This->getSATEncoder()->cnf, var) ? FIRST : SECOND;
+       return getValueCNF(This->getSATEncoder()->getCNF(), var) ? FIRST : SECOND;
 }
 

diff --git a/src/Tuner/tunable.cc b/src/Tuner/tunable.cc
index 5c13a126ac3f9d8d6d9214478d6d2fbd3ff605ab..1401b24bbb86ab502e979aeddbc081f5d5eb0f9d 100644 (file)
--- a/src/Tuner/tunable.cc
+++ b/src/Tuner/tunable.cc
@@ -1,11 +1,11 @@
 #include "tunable.h"
 
-Tuner::Tuner() {
+DefaultTuner::DefaultTuner() {
 }
 
-int Tuner::getTunable(TunableParam param, TunableDesc *descriptor) {
+int DefaultTuner::getTunable(TunableParam param, TunableDesc *descriptor) {
        return descriptor->defaultValue;
 }
-int Tuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {
+int DefaultTuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {
        return descriptor->defaultValue;
 }

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 6077891a5cff896daa2c990796dd3a74e58da7a6..8d696af0c58197576697beb64ada3e9f43482e15 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -5,12 +5,22 @@
 
 class Tuner {
 public:
-       Tuner();
+       virtual int getTunable(TunableParam param, TunableDesc *descriptor);
+       virtual int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
+       virtual ~Tuner();
+       MEMALLOC;
+};
+
+class DefaultTuner : public Tuner {
+public:
+       DefaultTuner();
        int getTunable(TunableParam param, TunableDesc *descriptor);
        int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
        MEMALLOC;
 };
 
+
+
 class TunableDesc {
 public:
        TunableDesc(int _lowValue, int _highValue, int _defaultValue) : lowValue(_lowValue), highValue(_highValue), defaultValue(_defaultValue) {}

diff --git a/src/classlist.h b/src/classlist.h
index aac331d1154c75139e9cb4d2b00cb30399685b5d..dd97e086c3675e2599969bae8beb5bb406969625 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -50,6 +50,7 @@ class OrderGraph;
 class OrderNode;
 class OrderEdge;
 
+class AutoTuner;
 
 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;

diff --git a/src/common.h b/src/common.h
index 0ebb7ece4c73a9263613a02a3705616a5c10d778..3fffb3419b88f3dc516c48ea915af6f7cb13167c 100644 (file)
--- a/src/common.h
+++ b/src/common.h
@@ -16,6 +16,7 @@
 
 #include <stdio.h>
 #include "config.h"
+#include "time.h"
 
 /*
    extern int model_out;
@@ -65,4 +66,10 @@ void assert_hook(void);
 #define error_msg(...) fprintf(stderr, "Error: " __VA_ARGS__)
 
 void print_trace(void);
+
+static inline long long getTimeNano() {
+       struct timespec time;
+       clock_gettime(CLOCK_REALTIME, & time);
+       return time.tv_sec * 1000000000 + time.tv_nsec;
+}
 #endif/* __COMMON_H__ */

diff --git a/src/csolver.cc b/src/csolver.cc
index 47e22a14c159f2a283ea9e06fcbd3fe0fded3ce0..c83f4b942644bbd3c063e848688265e3adf2eae7 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -12,9 +12,13 @@
 #include "tunable.h"
 #include "polarityassignment.h"
 #include "orderdecompose.h"
+#include "autotuner.h"
 
-CSolver::CSolver() : unsat(false) {
-       tuner = new Tuner();
+CSolver::CSolver() :
+       unsat(false),
+       tuner(new DefaultTuner()),
+       elapsedTime(0)
+{
        satEncoder = new SATEncoder(this);
 }
 
@@ -198,16 +202,14 @@ Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second)
 }
 
 int CSolver::startEncoding() {
+       long long startTime = getTimeNano();
        computePolarities(this);
        orderAnalysis(this);
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
-       int result = solveCNF(satEncoder->cnf);
-       model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);
-       for (int i = 1; i <= satEncoder->cnf->solver->solutionsize; i++) {
-               model_print("%d, ", satEncoder->cnf->solver->solution[i]);
-       }
-       model_print("\n");
+       int result = satEncoder->solve();
+       long long finishTime = getTimeNano();
+       elapsedTime = finishTime - startTime;
        return result;
 }
 
@@ -237,3 +239,11 @@ HappenedBefore CSolver::getOrderConstraintValue(Order *order, uint64_t first, ui
        return getOrderConstraintValueSATTranslator(this, order, first, second);
 }
 
+long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
+
+long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
+
+void CSolver::autoTune() {
+       AutoTuner * autotuner=new AutoTuner();
+       autotuner->tune(this);
+}

diff --git a/src/csolver.h b/src/csolver.h
index 1f779935eb4f1ad24250ce4b911bd7fceabe3afd..7939ee516f7fae5ea24c73311929e7c635b7e8bd 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -108,7 +108,7 @@ public:
        Vector<Order *> *getOrders() { return &allOrders;}
 
        Tuner *getTuner() { return tuner; }
-
+       
        HSIteratorBoolean *getConstraints() { return constraints.iterator(); }
 
        SATEncoder *getSATEncoder() {return satEncoder;}
@@ -117,7 +117,13 @@ public:
        void replaceBooleanWithFalse(Boolean *bexpr);
        void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
        CSolver *clone();
+       void autoTune();
 
+       void setTuner(Tuner * _tuner) { tuner = _tuner; }
+       long long getElapsedTime() { return elapsedTime; }
+       long long getEncodeTime();
+       long long getSolveTime();
+       
        MEMALLOC;
 
 private:
@@ -154,5 +160,7 @@ private:
        SATEncoder *satEncoder;
        bool unsat;
        Tuner *tuner;
+
+       long long elapsedTime;
 };
 #endif