Bug Fix
authorbdemsky <bdemsky@uci.edu>
Mon, 4 Sep 2017 07:00:15 +0000 (00:00 -0700)
committerbdemsky <bdemsky@uci.edu>
Mon, 4 Sep 2017 07:00:15 +0000 (00:00 -0700)
src/AST/boolean.h
src/ASTTransform/decomposeordertransform.cc
src/Backend/constraint.cc
src/Tuner/autotuner.cc
src/csolver.cc

index 41e9d5b..ecaebaf 100644 (file)
@@ -79,4 +79,7 @@ public:
        Array<BooleanEdge> inputs;
        CMEMALLOC;
 };
+BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e);
+
+
 #endif
index 85b43b1..7d276e2 100644 (file)
@@ -60,11 +60,13 @@ void DecomposeOrderTransform::doTransform() {
                        }
                }
 
+               /*
                bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
 
                if (mustReachPrune)
                        removeMustBeTrueNodes(solver, graph);
-
+               */
+               
                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);
                decomposeOrder(order, graph);
index b90ec4a..0372536 100644 (file)
@@ -59,6 +59,8 @@ CNF *createCNF() {
        initDefVectorEdge(&cnf->constraints);
        initDefVectorEdge(&cnf->args);
        cnf->solver = allocIncrementalSolver();
+       cnf->solveTime = 0;
+       cnf->encodeTime = 0;
        return cnf;
 }
 
index 9082ae4..5247d86 100644 (file)
@@ -17,6 +17,7 @@ long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
        CSolver *copy = problem->clone();
        copy->setTuner(tuner);
        int result = copy->solve();
+       model_print("SAT %d\n", result);
        long long elapsedTime = copy->getElapsedTime();
        long long encodeTime = copy->getEncodeTime();
        long long solveTime = copy->getSolveTime();
index ea16b80..b353791 100644 (file)
@@ -77,7 +77,7 @@ CSolver *CSolver::clone() {
        SetIteratorBooleanEdge *it = getConstraints();
        while (it->hasNext()) {
                BooleanEdge b = it->next();
-               copy->addConstraint(b->clone(copy, &map));
+               copy->addConstraint(cloneEdge(copy, &map, b));
        }
        delete it;
        return copy;
@@ -374,10 +374,6 @@ void CSolver::addConstraint(BooleanEdge constraint) {
                }
                constraints.add(constraint);
                Boolean *ptr=constraint.getBoolean();
-               if (constraint.isNegated())
-                       updateMustValue(ptr, BV_MUSTBEFALSE);
-               else
-                       updateMustValue(ptr, BV_MUSTBETRUE);
                
                if (ptr->boolVal == BV_UNSAT)
                        setUnSAT();