Solver.h 22.5 KB
Newer Older
Masahiko Sakai's avatar
Masahiko Sakai committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
/****************************************************************************************[Solver.h]
Copyright (c) 2005-2010, Niklas Een, Niklas Sorensson

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/

#ifndef Solver_h
#define Solver_h

#include "MiniSat.h"
#include "SatELite.h"
#include "glueminisat/core/Solver.h"
#include "glueminisat/simp/SimpSolver.h"
#include "es1sat/core/Solver.h"
#include "es1sat/simp/SimpSolver.h"
#include "ccminisat/core/Solver.h"
#include "ccminisat/simp/SimpSolver.h"

//=================================================================================================


class Solver {
    MiniSat ::Solver*    minisat;
    SatELite::Solver*    satelite;
Masahiko Sakai's avatar
Masahiko Sakai committed
38 39 40 41 42 43
    GlueMiniSat::Solver* glueminisat;
    GlueMiniSat::SimpSolver* simp_glueminisat;
    ES1Sat::Solver*      es1sat;
    ES1Sat::SimpSolver*  simp_es1sat;
    CCMiniSat::Solver*   ccminisat;
    CCMiniSat::SimpSolver* simp_ccminisat;
Masahiko Sakai's avatar
Masahiko Sakai committed
44 45 46

    BasicSolverStats     basicStats;
    bool                 dummyOK;
Masahiko Sakai's avatar
Masahiko Sakai committed
47
    
Masahiko Sakai's avatar
Masahiko Sakai committed
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
    GlueMiniSat::Lit lit2lit(const Lit lit) {
        return GlueMiniSat::mkLit(var(lit), sign(lit));
    }
    void vec2vec(const vec<Lit>& in, GlueMiniSat::vec<GlueMiniSat::Lit>& out) {
        for (int i=0; i < in.size(); i++)
            out.push(lit2lit(in[i]));
    }
    lbool lbool2lbool(GlueMiniSat::lbool v) const {
        switch (GlueMiniSat::toInt(v)) {
            case 0: return toLbool(+1);
            case 1: return toLbool(-1);
            case 2: return toLbool( 0);
        }
        assert(false);
        return(ll_Undef);
    }

    ES1Sat::Lit elit2lit(const Lit lit) {
        return ES1Sat::mkLit(var(lit), sign(lit));
    }
    void vec2vec(const vec<Lit>& in, ES1Sat::vec<ES1Sat::Lit>& out) {
        for (int i=0; i < in.size(); i++)
            out.push(elit2lit(in[i]));
    }
    lbool lbool2lbool(ES1Sat::lbool v) const {
        switch (ES1Sat::toInt(v)) {
            case 0: return toLbool(+1);
            case 1: return toLbool(-1);
            case 2: return toLbool( 0);
        }
        assert(false);
        return ll_Undef;
    }
/*
    ES1Sat::Lit elit2lit(const Lit lit) {
        return ES1Sat::Lit(var(lit), sign(lit));
    }
    void vec2vec(const vec<Lit>& in, ES1Sat::vec<ES1Sat::Lit>& out) {
        for (int i=0; i < in.size(); i++)
            out.push(elit2lit(in[i]));
    }
    lbool lbool2lbool(ES1Sat::lbool v) const {
      return(toLbool(ES1Sat::toInt(v)));
    }
*/
    CCMiniSat::Lit clit2lit(const Lit lit) {
        return CCMiniSat::mkLit(var(lit), sign(lit));
    }
    void vec2vec(const vec<Lit>& in, CCMiniSat::vec<CCMiniSat::Lit>& out) {
        for (int i=0; i < in.size(); i++)
            out.push(clit2lit(in[i]));
    }
    lbool lbool2lbool(CCMiniSat::lbool v) const {
        switch (CCMiniSat::toInt(v)) {
            case 0: return toLbool(+1);
            case 1: return toLbool(-1);
            case 2: return toLbool( 0);
        }
        assert(false);
        return ll_Undef;
    }

public:
Masahiko Sakai's avatar
Masahiko Sakai committed
111
    double               solving_time;
Masahiko Sakai's avatar
Masahiko Sakai committed
112 113 114 115
    bool& ok_ref() {
        if (minisat)     return minisat->ok;
        if (satelite)    return satelite->ok;
        if (glueminisat) return glueminisat->getOK();
Masahiko Sakai's avatar
Masahiko Sakai committed
116
        if (simp_glueminisat) return simp_glueminisat->getOK();
Masahiko Sakai's avatar
Masahiko Sakai committed
117
        if (es1sat)      return es1sat->getOK();
Masahiko Sakai's avatar
Masahiko Sakai committed
118
        if (simp_es1sat)      return simp_es1sat->getOK();
Masahiko Sakai's avatar
Masahiko Sakai committed
119
	if (ccminisat)      return ccminisat->getOK();
Masahiko Sakai's avatar
Masahiko Sakai committed
120
	if (simp_ccminisat)      return simp_ccminisat->getOK();
Masahiko Sakai's avatar
Masahiko Sakai committed
121 122 123 124 125 126 127 128 129 130
        assert(false);
        return dummyOK;
    }
//    vec<int>&         assigns_ref() { return (minisat != NULL) ? minisat->assigns : (satelite != NULL) ? satelite->assigns : glueminisat->assigns; }
//    vec<Lit>&         trail_ref  () { return (minisat != NULL) ? minisat->trail   : (satelite != NULL) ? satelite->trail   : glueminisat->trail; }
//    BasicSolverStats& stats_ref  () { return (minisat != NULL) ? (BasicSolverStats&)minisat->stats : (BasicSolverStats&)satelite->stats  ; }
    BasicSolverStats& stats_ref  () {
        if (minisat ) return (BasicSolverStats&)minisat->stats;
        if (satelite) return (BasicSolverStats&)satelite->stats;
        // if (glueminisat||es1sat) return basicStats;
Masahiko Sakai's avatar
Masahiko Sakai committed
131 132 133
	if (glueminisat||simp_glueminisat
            ||es1sat||simp_es1sat
            ||ccminisat||simp_ccminisat) return basicStats;
Masahiko Sakai's avatar
Masahiko Sakai committed
134 135 136 137 138 139 140 141
        assert(false);
        return basicStats;
    }

    int assigns(Var v) const {
        if (minisat     != NULL) return minisat->assigns[v];
        if (satelite    != NULL) return satelite->assigns[v];
        if (glueminisat != NULL) return lbool2lbool(glueminisat->getAssign(v)).toInt();
Masahiko Sakai's avatar
Masahiko Sakai committed
142
        if (simp_glueminisat != NULL) return lbool2lbool(simp_glueminisat->getAssign(v)).toInt();
Masahiko Sakai's avatar
Masahiko Sakai committed
143
        if (es1sat      != NULL) return lbool2lbool(es1sat     ->getAssign(v)).toInt();
Masahiko Sakai's avatar
Masahiko Sakai committed
144
        if (simp_es1sat != NULL) return lbool2lbool(simp_es1sat->getAssign(v)).toInt();
Masahiko Sakai's avatar
Masahiko Sakai committed
145 146 147

	//   if (es1sat      != NULL) return es1sat->getAssign(v);
        if (ccminisat      != NULL) return lbool2lbool(ccminisat     ->getAssign(v)).toInt();
Masahiko Sakai's avatar
Masahiko Sakai committed
148
        if (simp_ccminisat != NULL) return lbool2lbool(simp_ccminisat->getAssign(v)).toInt();
Masahiko Sakai's avatar
Masahiko Sakai committed
149 150 151 152 153 154 155
        assert(false);
        return 0;
    }
    int trail_size() {
        if (minisat     != NULL) return minisat->trail.size();
        if (satelite    != NULL) return satelite->trail.size();
        if (glueminisat != NULL) return glueminisat->getTrailSize();
Masahiko Sakai's avatar
Masahiko Sakai committed
156
        if (simp_glueminisat != NULL) return simp_glueminisat->getTrailSize();
Masahiko Sakai's avatar
Masahiko Sakai committed
157
        if (es1sat      != NULL) return es1sat->getTrailSize();
Masahiko Sakai's avatar
Masahiko Sakai committed
158
        if (simp_es1sat      != NULL) return simp_es1sat->getTrailSize();
Masahiko Sakai's avatar
Masahiko Sakai committed
159
	if (ccminisat      != NULL) return ccminisat->getTrailSize();
Masahiko Sakai's avatar
Masahiko Sakai committed
160
	if (simp_ccminisat      != NULL) return simp_ccminisat->getTrailSize();
Masahiko Sakai's avatar
Masahiko Sakai committed
161 162 163 164 165 166 167
        assert(false);
        return 0;
    }
    Lit trail(int index) {
        if (minisat     != NULL) return minisat->trail[index];
        if (satelite    != NULL) return satelite->trail[index];
        if (glueminisat != NULL) return Lit(GlueMiniSat::var(glueminisat->getTrail(index)), GlueMiniSat::sign(glueminisat->getTrail(index)));
Masahiko Sakai's avatar
Masahiko Sakai committed
168
        if (simp_glueminisat != NULL) return Lit(GlueMiniSat::var(simp_glueminisat->getTrail(index)), GlueMiniSat::sign(simp_glueminisat->getTrail(index)));
Masahiko Sakai's avatar
Masahiko Sakai committed
169
        if (es1sat      != NULL) return Lit(ES1Sat::var(es1sat->getTrail(index)), ES1Sat::sign(es1sat->getTrail(index)));
Masahiko Sakai's avatar
Masahiko Sakai committed
170
        if (simp_es1sat      != NULL) return Lit(ES1Sat::var(simp_es1sat->getTrail(index)), ES1Sat::sign(simp_es1sat->getTrail(index)));
Masahiko Sakai's avatar
Masahiko Sakai committed
171
	if (ccminisat      != NULL) return Lit(CCMiniSat::var(ccminisat->getTrail(index)), CCMiniSat::sign(ccminisat->getTrail(index)));
Masahiko Sakai's avatar
Masahiko Sakai committed
172
	if (simp_ccminisat      != NULL) return Lit(CCMiniSat::var(simp_ccminisat->getTrail(index)), CCMiniSat::sign(simp_ccminisat->getTrail(index)));
Masahiko Sakai's avatar
Masahiko Sakai committed
173 174 175 176 177 178 179
        assert(false);
        return lit_Error;
    }
    void setVerbosity(int level) {
        if (minisat    ) minisat->verbosity = level;
        if (satelite   ) satelite->verbosity = level;
        if (glueminisat) glueminisat->verbosity = level;
Masahiko Sakai's avatar
Masahiko Sakai committed
180
        if (simp_glueminisat) simp_glueminisat->verbosity = level;
Masahiko Sakai's avatar
Masahiko Sakai committed
181
        if (es1sat     ) es1sat->verbosity = level;
Masahiko Sakai's avatar
Masahiko Sakai committed
182
        if (simp_es1sat     ) simp_es1sat->verbosity = level;
Masahiko Sakai's avatar
Masahiko Sakai committed
183
	if (ccminisat  ) ccminisat->verbosity = level;
Masahiko Sakai's avatar
Masahiko Sakai committed
184
	if (simp_ccminisat  ) simp_ccminisat->verbosity = level;
Masahiko Sakai's avatar
Masahiko Sakai committed
185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
    }

//    void setVerbosity(int level) {
//        if (minisat != NULL)
//            minisat->verbosity = level;
//        else
//            satelite->verbosity = level; }

//    Var         newVar         (bool dvar = true)   { return (minisat != NULL) ? minisat->newVar(dvar) : satelite->newVar(dvar); }
//    bool        addClause      (const vec<Lit>& ps) { return (minisat != NULL) ? minisat->addClause(ps) : (satelite->addClause(ps), satelite->okay()); }
//    bool        addUnit        (Lit p)              { return (minisat != NULL) ? minisat->addUnit(p) : (satelite->addUnit(p), satelite->okay()); }
//    void        freeze         (Var x)              { if (minisat == NULL) satelite->freeze(x); }
//    void        suggestPolarity(Var x, lbool value) { if (minisat != NULL) minisat->polarity_sug[x] = toInt(value); else satelite->polarity_sug[x] = toInt(value); }
//    bool        solve     (const vec<Lit>& assumps) { return (minisat != NULL) ? minisat->solve(assumps) : satelite->solve(assumps); }
//    bool        solve          ()                   { vec<Lit> tmp; return solve(tmp); }
//    vec<lbool>& model          ()                   { return (minisat != NULL) ? minisat->model : satelite->model; }
//    bool        varElimed      (Var x)              { return (minisat != NULL) ? false : satelite->var_elimed[x]; }
//    bool        okay           ()                   { return (minisat != NULL) ? minisat->okay() : satelite->okay(); }
//    int         nVars          ()        const      { return (minisat != NULL) ? minisat->nVars() : satelite ? satelite->nVars() : glueminisat->nVars(); }


    Var newVar(bool dvar = true)   {
      //      printf("m %d, s %d, g %d\n", minisat, satelite, glueminisat);
        if (minisat)     return minisat    ->newVar(dvar);
        if (satelite)    return satelite   ->newVar(dvar);
        if (glueminisat) return glueminisat->newVar(true, dvar);
Masahiko Sakai's avatar
Masahiko Sakai committed
211
        if (simp_glueminisat) return simp_glueminisat->newVar(true, dvar);
Masahiko Sakai's avatar
Masahiko Sakai committed
212
        if (es1sat)      return es1sat     ->newVar(true, dvar);
Masahiko Sakai's avatar
Masahiko Sakai committed
213
        if (simp_es1sat)      return simp_es1sat     ->newVar(true, dvar);
Masahiko Sakai's avatar
Masahiko Sakai committed
214
	if (ccminisat)   return ccminisat  ->newVar(true, dvar);
Masahiko Sakai's avatar
Masahiko Sakai committed
215
	if (simp_ccminisat)   return simp_ccminisat  ->newVar(true, dvar);
Masahiko Sakai's avatar
Masahiko Sakai committed
216 217 218 219 220 221 222 223 224 225 226
        assert(false);
        return 0;
    }
    bool addClause(const vec<Lit>& ps) {
        if (minisat)     return minisat    ->addClause(ps);
        if (satelite)    return (satelite->addClause(ps), satelite->okay());
        if (glueminisat) {
            GlueMiniSat::vec<GlueMiniSat::Lit> ps_;
            vec2vec(ps, ps_);
            return glueminisat->addClause_(ps_);
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
227 228 229 230 231
        if (simp_glueminisat) {
            GlueMiniSat::vec<GlueMiniSat::Lit> ps_;
            vec2vec(ps, ps_);
            return simp_glueminisat->addClause_(ps_);
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
232 233 234 235 236
        if (es1sat) {
            ES1Sat::vec<ES1Sat::Lit> ps_;
            vec2vec(ps, ps_);
            return es1sat->addClause_(ps_);
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
237 238 239 240 241
        if (simp_es1sat) {
            ES1Sat::vec<ES1Sat::Lit> ps_;
            vec2vec(ps, ps_);
            return simp_es1sat->addClause_(ps_);
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
242 243 244 245 246
        if (ccminisat) {
            CCMiniSat::vec<CCMiniSat::Lit> ps_;
            vec2vec(ps, ps_);
            return ccminisat->addClause_(ps_);
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
247 248 249 250 251
        if (simp_ccminisat) {
            CCMiniSat::vec<CCMiniSat::Lit> ps_;
            vec2vec(ps, ps_);
            return simp_ccminisat->addClause_(ps_);
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
252 253 254 255 256 257 258 259 260
        assert(false);
        return false;
    }
    bool add_ESClause(const vec<Lit>& ps) {
        if (es1sat) {
            ES1Sat::vec<ES1Sat::Lit> ps_;
            vec2vec(ps, ps_);
            return es1sat->add_ESClause_(ps_);
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
261 262 263 264 265
        if (simp_es1sat) {
            ES1Sat::vec<ES1Sat::Lit> ps_;
            vec2vec(ps, ps_);
            return simp_es1sat->add_ESClause_(ps_);
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
266 267 268 269 270 271 272 273 274
        assert(false);
        return false;
    }
    bool add_CCClause(const vec<Lit>& ps, int k) {
        if (ccminisat) {
            CCMiniSat::vec<CCMiniSat::Lit> ps_;
            vec2vec(ps, ps_);
            return ccminisat->add_CCClause_(ps_, k);
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
275 276 277 278 279
        if (simp_ccminisat) {
            CCMiniSat::vec<CCMiniSat::Lit> ps_;
            vec2vec(ps, ps_);
            return simp_ccminisat->add_CCClause_(ps_, k);
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
280 281 282 283 284 285 286
        assert(false);
        return false;
    }
    bool addUnit(Lit p) {
        if (minisat)     return minisat    ->addUnit(p);
        if (satelite)    return (satelite  ->addUnit(p), satelite->okay());
        if (glueminisat) return glueminisat->addClause(lit2lit(p));
Masahiko Sakai's avatar
Masahiko Sakai committed
287
        if (simp_glueminisat) return simp_glueminisat->addClause(lit2lit(p));
Masahiko Sakai's avatar
Masahiko Sakai committed
288
        if (es1sat)      return es1sat     ->addClause(elit2lit(p));
Masahiko Sakai's avatar
Masahiko Sakai committed
289
        if (simp_es1sat)      return simp_es1sat     ->addClause(elit2lit(p));
Masahiko Sakai's avatar
Masahiko Sakai committed
290
	if (ccminisat)   return ccminisat  ->addClause(clit2lit(p));
Masahiko Sakai's avatar
Masahiko Sakai committed
291
	if (simp_ccminisat)   return simp_ccminisat  ->addClause(clit2lit(p));
Masahiko Sakai's avatar
Masahiko Sakai committed
292 293 294 295 296 297
        assert(false);
        return false;
    }
    void freeze(Var x) {
      if (satelite)
	satelite->freeze(x);
Masahiko Sakai's avatar
Masahiko Sakai committed
298 299
      if (simp_glueminisat) {
	simp_glueminisat->setFrozen(x, true); //            printf("variable %d is frozen\n", x);
Masahiko Sakai's avatar
Masahiko Sakai committed
300
      }
Masahiko Sakai's avatar
Masahiko Sakai committed
301 302
      if (simp_es1sat) simp_es1sat->setFrozen(x, true);
      if (simp_ccminisat) simp_ccminisat->setFrozen(x, true);
Masahiko Sakai's avatar
Masahiko Sakai committed
303 304 305 306 307 308 309
      // else  assert(false);
      }
    void suggestPolarity(Var x, lbool value) {
        if (minisat ) minisat->polarity_sug[x] = toInt(value);
        else if (satelite) satelite->polarity_sug[x] = toInt(value);
	//  else assert(false);
    }
Masahiko Sakai's avatar
Masahiko Sakai committed
310
    bool solve_(const vec<Lit>& assumps) {
Masahiko Sakai's avatar
Masahiko Sakai committed
311 312 313 314 315 316 317 318 319 320 321 322
        if (minisat)  return minisat->solve(assumps);
        if (satelite) return satelite->solve(assumps);
        if (glueminisat) {
            GlueMiniSat::vec<GlueMiniSat::Lit> assumps_;
            vec2vec(assumps, assumps_);
            bool ret = glueminisat->solve(assumps_);
            basicStats.conflicts    += glueminisat->conflicts;
            basicStats.decisions    += glueminisat->decisions;
            basicStats.propagations += glueminisat->propagations;
            basicStats.starts       += glueminisat->starts;
            return ret;
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
323 324 325 326 327 328 329 330 331 332
        if (simp_glueminisat) {
            GlueMiniSat::vec<GlueMiniSat::Lit> assumps_;
            vec2vec(assumps, assumps_);
            bool ret = simp_glueminisat->solve(assumps_);
            basicStats.conflicts    += simp_glueminisat->conflicts;
            basicStats.decisions    += simp_glueminisat->decisions;
            basicStats.propagations += simp_glueminisat->propagations;
            basicStats.starts       += simp_glueminisat->starts;
            return ret;
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
333 334 335 336 337 338 339 340 341 342
        if (es1sat) {
            ES1Sat::vec<ES1Sat::Lit> assumps_;
            vec2vec(assumps, assumps_);
            bool ret = es1sat->solve(assumps_);
            basicStats.conflicts    += es1sat->conflicts;
            basicStats.decisions    += es1sat->decisions;
            basicStats.propagations += es1sat->propagations;
            basicStats.starts       += es1sat->starts;
            return ret;
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
343 344 345 346 347 348 349 350 351 352
        if (simp_es1sat) {
            ES1Sat::vec<ES1Sat::Lit> assumps_;
            vec2vec(assumps, assumps_);
            bool ret = simp_es1sat->solve(assumps_);
            basicStats.conflicts    += simp_es1sat->conflicts;
            basicStats.decisions    += simp_es1sat->decisions;
            basicStats.propagations += simp_es1sat->propagations;
            basicStats.starts       += simp_es1sat->starts;
            return ret;
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
353 354 355 356 357 358 359 360 361 362
        if (ccminisat) {
            CCMiniSat::vec<CCMiniSat::Lit> assumps_;
            vec2vec(assumps, assumps_);
            bool ret = ccminisat->solve(assumps_);
            basicStats.conflicts    += ccminisat->conflicts;
            basicStats.decisions    += ccminisat->decisions;
            basicStats.propagations += ccminisat->propagations;
            basicStats.starts       += ccminisat->starts;
            return ret;
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
363 364 365 366 367 368 369 370 371 372
        if (simp_ccminisat) {
            CCMiniSat::vec<CCMiniSat::Lit> assumps_;
            vec2vec(assumps, assumps_);
            bool ret = simp_ccminisat->solve(assumps_);
            basicStats.conflicts    += simp_ccminisat->conflicts;
            basicStats.decisions    += simp_ccminisat->decisions;
            basicStats.propagations += simp_ccminisat->propagations;
            basicStats.starts       += simp_ccminisat->starts;
            return ret;
        }
Masahiko Sakai's avatar
Masahiko Sakai committed
373 374 375
        assert(false);
        return false;
    }
Masahiko Sakai's avatar
Masahiko Sakai committed
376 377 378 379 380 381
    bool solve(const vec<Lit>& assumps) {
      double start_time = cpuTime();
      bool result = solve_(assumps);
      solving_time += (cpuTime() - start_time);
      return result;
    }
Masahiko Sakai's avatar
Masahiko Sakai committed
382 383 384 385 386 387 388 389
    bool solve() {
        vec<Lit> tmp; return solve(tmp);
    }
//    vec<lbool>& model          ()                   { return (minisat != NULL) ? minisat->model : satelite->model; }
    lbool model(Var v) {
        if (minisat)     return minisat ->model[v];
        if (satelite)    return satelite->model[v];
        if (glueminisat) return lbool2lbool(glueminisat->model[v]);
Masahiko Sakai's avatar
Masahiko Sakai committed
390
        if (simp_glueminisat) return lbool2lbool(simp_glueminisat->model[v]);
Masahiko Sakai's avatar
Masahiko Sakai committed
391
        if (es1sat)      return lbool2lbool(es1sat->model[v]);
Masahiko Sakai's avatar
Masahiko Sakai committed
392
        if (simp_es1sat)      return lbool2lbool(simp_es1sat->model[v]);
Masahiko Sakai's avatar
Masahiko Sakai committed
393
	if (ccminisat)   return lbool2lbool(ccminisat->model[v]);
Masahiko Sakai's avatar
Masahiko Sakai committed
394
	if (simp_ccminisat)   return lbool2lbool(simp_ccminisat->model[v]);
Masahiko Sakai's avatar
Masahiko Sakai committed
395 396 397 398
        assert(false);
        return ll_Undef;
    }
    bool varElimed(Var x) {
Masahiko Sakai's avatar
Masahiko Sakai committed
399 400 401 402 403
      if (simp_glueminisat) return simp_glueminisat->isEliminated(x);
      if (simp_es1sat) return simp_es1sat->isEliminated(x);
      if (simp_ccminisat) return simp_ccminisat->isEliminated(x);
      if (satelite) return satelite->var_elimed[x];
      else return false;
Masahiko Sakai's avatar
Masahiko Sakai committed
404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438
    }
    int ucore_vars(int idx) {
      if (glueminisat)
	return glueminisat->ucore_vars[idx];
//	return glueminisat->getUcore_vars(idx);
      else
        assert(false);
      return(0);
    }
    int ucore_varsSize() {
      if (glueminisat)
	return glueminisat->ucore_vars.size();
//	return glueminisat->getUcore_varsSize();
      else
        assert(false);
      return(0);
    }
    int ucore_clauses(int idx) {
      if (glueminisat)
	return glueminisat->ucore_clauses[idx];
//	return glueminisat->getUcore_clauses(idx);
      else
        assert(false);
      return(0);
    }
    int ucore_clausesSize() {
      if (glueminisat)
	return glueminisat->ucore_clauses.size();
//	return glueminisat->getUcore_clausesSize();
      else
        assert(false);
      return(0);
    }
    bool okay() {
        if (glueminisat) return glueminisat->okay();
Masahiko Sakai's avatar
Masahiko Sakai committed
439
        if (simp_glueminisat) return simp_glueminisat->okay();
Masahiko Sakai's avatar
Masahiko Sakai committed
440
        if (es1sat)      return es1sat->okay();
Masahiko Sakai's avatar
Masahiko Sakai committed
441
        if (simp_es1sat)      return simp_es1sat->okay();
Masahiko Sakai's avatar
Masahiko Sakai committed
442
	if (ccminisat)   return ccminisat->okay();
Masahiko Sakai's avatar
Masahiko Sakai committed
443 444 445
	if (simp_ccminisat)   return simp_ccminisat->okay();
        if (minisat)     return minisat->okay();
        if (satelite)    return satelite->okay();
Masahiko Sakai's avatar
Masahiko Sakai committed
446 447 448 449 450
        assert(false);
        return false;
    }
    int nVars() const {
      //      return (minisat != NULL) ? minisat->nVars() : satelite ? satelite->nVars() : glueminisat ? glueminisat->nVars() : es1sat->nVars();
Masahiko Sakai's avatar
Masahiko Sakai committed
451 452 453 454 455 456 457 458
      return (minisat != NULL) ? minisat->nVars() : 
             satelite ? satelite->nVars() : 
             glueminisat ? glueminisat->nVars() :
             simp_glueminisat ? simp_glueminisat->nVars() :
             es1sat ? es1sat->nVars() : 
             simp_es1sat ? simp_es1sat->nVars() : 
             ccminisat ? ccminisat->nVars() : 
             simp_ccminisat->nVars() ;
Masahiko Sakai's avatar
Masahiko Sakai committed
459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483
    }
    void exportCnf(cchar* filename) {
        if (minisat) {
            // Prohibited minisat-simplification before exporting CNF's
            // because of BUG that produce satisfiable CNF
            // even if it is un-satisfiable.
            //	    minisat->simplifyDB();
            //            reportf("ok=%s\n", minisat->ok ? "true" : "false");
            minisat->exportClauses(filename);
        } else if (satelite) {
            SatELite::opt_pre_sat = true;
            SatELite::output_file = filename;
            if (opt_verbosity >= 1) reportf("=================================[SATELITE+]==================================\n");
            satelite->simplifyDB(true);
        } else if (glueminisat) {
            glueminisat->toDimacs(filename);
        } else
            assert(false);
    }
    //- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

    //Solver(bool use_minisat) : minisat(use_minisat ? new MiniSat::Solver : NULL), satelite(use_minisat ? NULL : new SatELite::Solver) {}
    Solver(SolverT type) :
        minisat    (type == st_MiniSat  ? new MiniSat::Solver     : NULL),
        satelite   (type == st_SatELite ? new SatELite::Solver    : NULL),
Masahiko Sakai's avatar
Masahiko Sakai committed
484 485 486 487 488 489 490
        glueminisat(!opt_simp_solver && (type == st_GlueMiniSat || type == st_MiniSat22 || type == st_Glucose10) ? new GlueMiniSat::Solver : NULL),
        simp_glueminisat(opt_simp_solver && (type == st_GlueMiniSat || type == st_MiniSat22 || type == st_Glucose10) ? new GlueMiniSat::SimpSolver : NULL),
        es1sat     (!opt_simp_solver && type == st_ES1Sat   ? new ES1Sat::Solver : NULL),
        simp_es1sat     (opt_simp_solver && type == st_ES1Sat   ? new ES1Sat::SimpSolver : NULL),
	ccminisat  (!opt_simp_solver && type == st_CCMiniSat? new CCMiniSat::Solver : NULL),
        simp_ccminisat  (opt_simp_solver && type == st_CCMiniSat? new CCMiniSat::SimpSolver : NULL),
        solving_time (0.0)
Masahiko Sakai's avatar
Masahiko Sakai committed
491 492
    {
      if (opt_extract_ucore) glueminisat->setUcoreExtract(opt_ucore_mode);
Masahiko Sakai's avatar
Masahiko Sakai committed
493 494 495 496 497 498 499 500 501 502 503 504 505 506
      // if (type == st_MiniSat22) glueminisat->setMiniSat22Params();
      // if (type == st_Glucose10) glueminisat->setGlucose10Params();
      if (type == st_MiniSat22) opt_simp_solver ? simp_glueminisat->setMiniSat22Params() : glueminisat->setMiniSat22Params();
      if (type == st_Glucose10) opt_simp_solver ? simp_glueminisat->setGlucose10Params() : glueminisat->setGlucose10Params();
      /*
      if (minisat)     solver_name = "MiniSat";
      if (satelite)    solver_name = "SatELite";
      if (glueminisat) solver_name = "GlueMiniSat";
      if (simp_glueminisat) solver_name = "GlueMiniSat with simplification";
      if (es1sat)      solver_name = "Es1sat";
      if (simp_es1sat) solver_name = "Es1sat with simplification";
      if (ccminisat)   solver_name = "CcMiniSat";
      if (simp_ccminisat)   solver_name = "CcMiniSat with simplification";
      */
Masahiko Sakai's avatar
Masahiko Sakai committed
507 508 509 510 511 512 513
    }
};


//=================================================================================================

#endif