libs/ezsat/ezminisat.h

   1 /*
   2  *  ezSAT -- A simple and easy to use CNF generator for SAT solvers
   3  *
   4  *  Copyright (C) 2013  Claire Xenia Wolf <claire@yosyshq.com>
   5  *
   6  *  Permission to use, copy, modify, and/or distribute this software for any
   7  *  purpose with or without fee is hereby granted, provided that the above
   8  *  copyright notice and this permission notice appear in all copies.
   9  *
  10  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17  *
  18  */
  19
  20 #ifndef EZMINISAT_H
  21 #define EZMINISAT_H
  22
  23 #define EZMINISAT_SIMPSOLVER 1
  24 #define EZMINISAT_VERBOSITY 0
  25 #define EZMINISAT_INCREMENTAL 1
  26
  27 #include "ezsat.h"
  28 #include <time.h>
  29
  30 // minisat is using limit macros and format macros in their headers that
  31 // can be the source of some troubles when used from c++11. therefore we
  32 // don't force ezSAT users to use minisat headers..
  33 namespace Minisat {
  34         class Solver;
  35         class SimpSolver;
  36 }
  37
  38 class ezMiniSAT : public ezSAT
  39 {
  40 private:
  41 #if EZMINISAT_SIMPSOLVER
  42         typedef Minisat::SimpSolver Solver;
  43 #else
  44         typedef Minisat::Solver Solver;
  45 #endif
  46         Solver *minisatSolver;
  47         std::vector<int> minisatVars;
  48         bool foundContradiction;
  49
  50 #if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
  51         std::set<int> cnfFrozenVars;
  52 #endif
  53
  54 #ifndef _WIN32
  55         static ezMiniSAT *alarmHandlerThis;
  56         static clock_t alarmHandlerTimeout;
  57         static void alarmHandler(int);
  58 #endif
  59
  60 public:
  61         ezMiniSAT();
  62         virtual ~ezMiniSAT();
  63         virtual void clear();
  64 #if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
  65         virtual void freeze(int id);
  66         virtual bool eliminated(int idx);
  67 #endif
  68         virtual bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions);
  69 };
  70
  71 #endif