removing cryptominisat since we're not using it

1 files changed, 0 insertions, 228 deletions

diff --git a/src/prop/cryptominisat/Solver/UselessBinRemover.cpp b/src/prop/cryptominisat/Solver/UselessBinRemover.cpp
deleted file mode 100644
index 1d848116e..000000000
--- a/src/prop/cryptominisat/Solver/UselessBinRemover.cpp
+++ /dev/null
@@ -1,228 +0,0 @@
-/***************************************************************************
-CryptoMiniSat -- Copyright (c) 2009 Mate Soos
-
-This program is free software: you can redistribute it and/or modify
-it under the terms of the GNU General Public License as published by
-the Free Software Foundation, either version 3 of the License, or
-(at your option) any later version.
-
-This program is distributed in the hope that it will be useful,
-but WITHOUT ANY WARRANTY; without even the implied warranty of
-MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-GNU General Public License for more details.
-
-You should have received a copy of the GNU General Public License
-along with this program.  If not, see <http://www.gnu.org/licenses/>.
-****************************************************************************/
-
-#include <iomanip>
-#include "UselessBinRemover.h"
-#include "VarReplacer.h"
-#include "ClauseCleaner.h"
-#include "time_mem.h"
-
-//#define VERBOSE_DEBUG
-
-using namespace CMSat;
-
-UselessBinRemover::UselessBinRemover(Solver& _solver) :
-    solver(_solver)
-{
-}
-
-/**
-@brief Time limiting
-*/
-#define MAX_REMOVE_BIN_FULL_PROPS 20000000
-/**
-@brief We measure time in (bogo)propagations and "extra" time, time not accountable in (bogo)props
-*/
-#define EXTRATIME_DIVIDER 3
-
-/**
-@brief Removes useless binary non-learnt clauses. See definiton of class for details
-
-We pick variables starting randomly at a place and going on until we stop:
-we limit ourselves in time using (bogo)propagations and "extratime"
-*/
-bool UselessBinRemover::removeUslessBinFull()
-{
-    double myTime = cpuTime();
-    toDeleteSet.clear();
-    toDeleteSet.growTo(solver.nVars()*2, 0);
-    uint32_t origHeapSize = solver.order_heap.size();
-    uint64_t origProps = solver.propagations;
-    bool fixed = false;
-    uint32_t extraTime = 0;
-    uint32_t numBinsBefore = solver.numBins;
-    solver.sortWatched(); //VERY important
-
-    uint32_t startFrom = solver.mtrand.randInt(solver.order_heap.size());
-    for (uint32_t i = 0; i != solver.order_heap.size(); i++) {
-        Var var = solver.order_heap[(i+startFrom)%solver.order_heap.size()];
-        if (solver.propagations - origProps + extraTime > MAX_REMOVE_BIN_FULL_PROPS) break;
-        if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) continue;
-
-        Lit lit(var, true);
-        if (!removeUselessBinaries(lit)) {
-            fixed = true;
-            solver.cancelUntilLight();
-            solver.uncheckedEnqueue(~lit);
-            solver.ok = (solver.propagate<false>().isNULL());
-            if (!solver.ok) return false;
-            continue;
-        }
-
-        lit = ~lit;
-        if (!removeUselessBinaries(lit)) {
-            fixed = true;
-            solver.cancelUntilLight();
-            solver.uncheckedEnqueue(~lit);
-            solver.ok = (solver.propagate<false>().isNULL());
-            if (!solver.ok) return false;
-            continue;
-        }
-    }
-
-    if (fixed) solver.order_heap.filter(Solver::VarFilter(solver));
-
-    if (solver.conf.verbosity >= 1) {
-        std::cout
-        << "c Removed useless bin:" << std::setw(8) << (numBinsBefore - solver.numBins)
-        << "  fixed: " << std::setw(5) << (origHeapSize - solver.order_heap.size())
-        << "  props: " << std::fixed << std::setprecision(2) << std::setw(6) << (double)(solver.propagations - origProps)/1000000.0 << "M"
-        << "  time: " << std::fixed << std::setprecision(2) << std::setw(5) << cpuTime() - myTime << " s"
-        << std::endl;
-    }
-
-    return true;
-}
-
-/**
-@brief Removes useless binaries of the graph portion that starts with lit
-
-We try binary-space propagation on lit. Then, we check that we cannot reach any
-of its one-hop neighboours from any of its other one-hope neighbours. If we can,
-we remove the one-hop neighbour from the neightbours (i.e. remove the binary
-clause). Example:
-
-\li a->b, a->c, b->c
-\li In claues: (-a V b), (-a V c), (-b V c)
-
-One-hop neighbours of a: b, c. But c can be reached through b! So, we remove
-a->c, the one-hop neighbour that is useless.
-*/
-bool UselessBinRemover::removeUselessBinaries(const Lit lit)
-{
-    solver.newDecisionLevel();
-    solver.uncheckedEnqueueLight(lit);
-    //Propagate only one hop
-    failed = !solver.propagateBinOneLevel();
-    if (failed) return false;
-    bool ret = true;
-
-    oneHopAway.clear();
-    assert(solver.decisionLevel() > 0);
-    int c;
-    if (solver.trail.size()-solver.trail_lim[0] == 0) {
-        solver.cancelUntilLight();
-        goto end;
-    }
-    //Fill oneHopAway and toDeleteSet with lits that are 1 hop away
-    extraTime += (solver.trail.size() - solver.trail_lim[0]) / EXTRATIME_DIVIDER;
-    for (c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) {
-        Lit x = solver.trail[c];
-        toDeleteSet[x.toInt()] = true;
-        oneHopAway.push(x);
-        solver.assigns[x.var()] = l_Undef;
-    }
-    solver.assigns[solver.trail[c].var()] = l_Undef;
-
-    solver.qhead = solver.trail_lim[0];
-    solver.trail.shrink_(solver.trail.size() - solver.trail_lim[0]);
-    solver.trail_lim.clear();
-    //solver.cancelUntil(0);
-
-    wrong.clear();
-    //We now try to reach the one-hop-away nodes from other one-hop-away
-    //nodes, but this time we propagate all the way
-    for(uint32_t i = 0; i < oneHopAway.size(); i++) {
-        //no need to visit it if it already queued for removal
-        //basically, we check if it's in 'wrong'
-        if (toDeleteSet[oneHopAway[i].toInt()]) {
-            if (!fillBinImpliesMinusLast(lit, oneHopAway[i], wrong)) {
-                ret = false;
-                goto end;
-            }
-        }
-    }
-
-    for (uint32_t i = 0; i < wrong.size(); i++) {
-        removeBin(~lit, wrong[i]);
-    }
-
-    end:
-    for(uint32_t i = 0; i < oneHopAway.size(); i++) {
-        toDeleteSet[oneHopAway[i].toInt()] = false;
-    }
-
-    return ret;
-}
-
-/**
-@brief Removes a binary clause (lit1 V lit2)
-
-The binary clause might be in twice, three times, etc. Take care to remove
-all instances of it.
-*/
-void UselessBinRemover::removeBin(const Lit lit1, const Lit lit2)
-{
-    #ifdef VERBOSE_DEBUG
-    std::cout << "Removing useless bin: " << lit1 << " " << lit2 << std::endl;
-    #endif //VERBOSE_DEBUG
-
-    std::pair<uint32_t, uint32_t> removed1 = removeWBinAll(solver.watches[(~lit1).toInt()], lit2);
-    std::pair<uint32_t, uint32_t> removed2 = removeWBinAll(solver.watches[(~lit2).toInt()], lit1);
-    assert(removed1 == removed2);
-
-    assert((removed1.first + removed2.first) % 2 == 0);
-    assert((removed1.second + removed2.second) % 2 == 0);
-    solver.learnts_literals -= (removed1.first + removed2.first);
-    solver.clauses_literals -= (removed1.second + removed2.second);
-    solver.numBins -= (removed1.first + removed2.first + removed1.second + removed2.second)/2;
-}
-
-/**
-@brief Propagates all the way lit, but doesn't propagate origLit
-
-Removes adds to "wrong" the set of one-hop lits that can be reached from
-lit AND are one-hop away from origLit. These later need to be removed
-*/
-bool UselessBinRemover::fillBinImpliesMinusLast(const Lit origLit, const Lit lit, vec<Lit>& wrong)
-{
-    solver.newDecisionLevel();
-    solver.uncheckedEnqueueLight(lit);
-    //if it's a cycle, it doesn't work, so don't propagate origLit
-    failed = !solver.propagateBinExcept(origLit);
-    if (failed) return false;
-
-    assert(solver.decisionLevel() > 0);
-    int c;
-    extraTime += (solver.trail.size() - solver.trail_lim[0]) / EXTRATIME_DIVIDER;
-    for (c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) {
-        Lit x = solver.trail[c];
-        if (toDeleteSet[x.toInt()]) {
-            wrong.push(x);
-            toDeleteSet[x.toInt()] = false;
-        };
-        solver.assigns[x.var()] = l_Undef;
-    }
-    solver.assigns[solver.trail[c].var()] = l_Undef;
-
-    solver.qhead = solver.trail_lim[0];
-    solver.trail.shrink_(solver.trail.size() - solver.trail_lim[0]);
-    solver.trail_lim.clear();
-    //solver.cancelUntil(0);
-
-    return true;
-}