Bug Fix

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 41e9d5b536cc4c9cbb549a8cb335b5cfb1480322..ecaebaf69c89fef2ebfc77d5de1fffd4c53db2e6 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -79,4 +79,7 @@ public:
        Array<BooleanEdge> inputs;
        CMEMALLOC;
 };
        Array<BooleanEdge> inputs;
        CMEMALLOC;
 };

+BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e);
+
+

 #endif
 #endif

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 85b43b12e1d063d9cdcf98e516fb21de1abbf177..7d276e2edaf21d6e4c4c7716e824d511ee679ff5 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -60,11 +60,13 @@ void DecomposeOrderTransform::doTransform() {
                        }
                }
 
                        }
                }
 

+               /*

                bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
 
                if (mustReachPrune)
                        removeMustBeTrueNodes(solver, graph);
                bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
 
                if (mustReachPrune)
                        removeMustBeTrueNodes(solver, graph);

-
+               */
+               

                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);
                decomposeOrder(order, graph);
                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);
                decomposeOrder(order, graph);

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index b90ec4aff6062d3b4b19f1c7f585ccb3213de289..0372536ea36c3cec769a4096f768b2b91e5bd6d0 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -59,6 +59,8 @@ CNF *createCNF() {
        initDefVectorEdge(&cnf->constraints);
        initDefVectorEdge(&cnf->args);
        cnf->solver = allocIncrementalSolver();
        initDefVectorEdge(&cnf->constraints);
        initDefVectorEdge(&cnf->args);
        cnf->solver = allocIncrementalSolver();

+       cnf->solveTime = 0;
+       cnf->encodeTime = 0;

        return cnf;
 }
 
        return cnf;
 }
 

diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index 9082ae4d027b950d4b713e8f5eeae8a05d91f7e9..5247d86b0fa1d9d576cb6887ead59f73a7b4745a 100644 (file)
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -17,6 +17,7 @@ long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
        CSolver *copy = problem->clone();
        copy->setTuner(tuner);
        int result = copy->solve();
        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();
        long long elapsedTime = copy->getElapsedTime();
        long long encodeTime = copy->getEncodeTime();
        long long solveTime = copy->getSolveTime();

diff --git a/src/csolver.cc b/src/csolver.cc
index ea16b8043ca84619cd2804d24f43c007f0bedcac..b353791e768e263c87799cd6c75435deb87b03d5 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -77,7 +77,7 @@ CSolver *CSolver::clone() {
        SetIteratorBooleanEdge *it = getConstraints();
        while (it->hasNext()) {
                BooleanEdge b = it->next();
        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;
        }
        delete it;
        return copy;


@@ -374,10 +374,6 @@ void CSolver::addConstraint(BooleanEdge constraint) {
                }
                constraints.add(constraint);
                Boolean *ptr=constraint.getBoolean();
                }
                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();
                
                if (ptr->boolVal == BV_UNSAT)
                        setUnSAT();