packages feed

minisat (empty) → 0.1

raw patch · 28 files changed

+5445/−0 lines, 28 filesdep +asyncdep +basedep +zlibsetup-changed

Dependencies added: async, base, zlib

Files

+ LICENSE view
@@ -0,0 +1,21 @@+MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson+           Copyright (c) 2007-2010  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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ minisat-c-bindings/minisat.cc view
@@ -0,0 +1,146 @@+/**************************************************************************************[minisat.cc]+Copyright (c) 2008-2010, Niklas Sorensson+              2008, Koen Claessen++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.+**************************************************************************************************/++#include <stdlib.h>+#include "minisat/simp/SimpSolver.h"++using namespace Minisat;++struct minisat_solver_t : public SimpSolver { +    vec<Lit> clause;+    vec<Lit> assumps;+};++extern "C" {++#include "minisat.h"++// This implementation of lbool may or not may be an exact mirror of the C++ implementation:+//+extern const minisat_lbool minisat_l_True  = 1;+extern const minisat_lbool minisat_l_False = 0;+extern const minisat_lbool minisat_l_Undef = -1;++static inline minisat_lbool toC(lbool a)+{+    return a == l_True  ? minisat_l_True+         : a == l_False ? minisat_l_False+         : minisat_l_Undef;+}++static inline lbool fromC(minisat_lbool a)+{+    return a == minisat_l_True  ? l_True+         : a == minisat_l_False ? l_False+         : l_Undef;+}+++// TODO: why are these here?+minisat_lbool minisat_get_l_True     (void){ return minisat_l_True; }+minisat_lbool minisat_get_l_False    (void){ return minisat_l_False; }+minisat_lbool minisat_get_l_Undef    (void){ return minisat_l_Undef; }++// Solver C-API wrapper functions:+//+minisat_solver* minisat_new             (void){ return new minisat_solver_t(); }+void          minisat_delete          (minisat_solver *s){ delete s; }+minisat_Var   minisat_newVar          (minisat_solver *s){ return s->newVar(); }+minisat_Lit   minisat_newLit          (minisat_solver *s){ return toInt(mkLit(s->newVar())); }+minisat_Lit   minisat_mkLit           (minisat_Var x){ return toInt(mkLit(x)); }+minisat_Lit   minisat_mkLit_args      (minisat_Var x, int sign){ return toInt(mkLit(x,sign)); }+minisat_Lit   minisat_negate          (minisat_Lit p){ return toInt(~toLit(p)); }+minisat_Var   minisat_var             (minisat_Lit p){ return var(toLit(p)); }+int          minisat_sign            (minisat_Lit p){ return sign(toLit(p)); }+void         minisat_addClause_begin (minisat_solver *s){ s->clause.clear(); }+void         minisat_addClause_addLit(minisat_solver *s, minisat_Lit p){ s->clause.push(toLit(p)); }+int          minisat_addClause_commit(minisat_solver *s){ return s->addClause_(s->clause); }+int          minisat_simplify        (minisat_solver *s){ return s->simplify(); }++// NOTE: Currently these run with default settings for implicitly calling preprocessing. Turn off+// before if you don't need it. This may change in the future.+void         minisat_solve_begin     (minisat_solver *s){ s->assumps.clear(); }+void         minisat_solve_addLit    (minisat_solver *s, minisat_Lit p){ s->assumps.push(toLit(p)); }+int          minisat_solve_commit    (minisat_solver *s){ return s->solve(s->assumps); }+minisat_lbool minisat_limited_solve_commit (minisat_solver *s){ return toC(s->solveLimited(s->assumps)); }++int          minisat_okay            (minisat_solver *s){ return s->okay(); }+void         minisat_setPolarity     (minisat_solver *s, minisat_Var v, minisat_lbool lb){ s->setPolarity(v, fromC(lb)); }+void         minisat_setDecisionVar  (minisat_solver *s, minisat_Var v, int b){ s->setDecisionVar(v, b); }+minisat_lbool minisat_value_Var      (minisat_solver *s, minisat_Var x){ return toC(s->value(x)); }+minisat_lbool minisat_value_Lit      (minisat_solver *s, minisat_Lit p){ return toC(s->value(toLit(p))); }+minisat_lbool minisat_modelValue_Var (minisat_solver *s, minisat_Var x){ return toC(s->modelValue(x)); }+minisat_lbool minisat_modelValue_Lit (minisat_solver *s, minisat_Lit p){ return toC(s->modelValue(toLit(p))); }+int          minisat_num_assigns     (minisat_solver *s){ return s->nAssigns(); }+int          minisat_num_clauses     (minisat_solver *s){ return s->nClauses(); }+int          minisat_num_learnts     (minisat_solver *s){ return s->nLearnts(); }+int          minisat_num_vars        (minisat_solver *s){ return s->nVars(); }+int          minisat_num_freeVars    (minisat_solver *s){ return s->nFreeVars(); }+int          minisat_conflict_len    (minisat_solver *s){ return s->conflict.size(); }+minisat_Lit  minisat_conflict_nthLit (minisat_solver *s, int i){ return toInt(s->conflict[i]); }+void         minisat_set_verbosity   (minisat_solver *s, int v){ s->verbosity = v; }+int          minisat_get_verbosity   (minisat_solver *s){ return s->verbosity; }+int          minisat_num_conflicts   (minisat_solver *s){ return s->conflicts; }+int          minisat_num_decisions   (minisat_solver *s){ return s->decisions; }+int          minisat_num_restarts    (minisat_solver *s){ return s->starts; }+int          minisat_num_propagations(minisat_solver *s){ return s->propagations; }+void         minisat_set_conf_budget (minisat_solver* s, int x){ s->setConfBudget(x); }+void         minisat_set_prop_budget (minisat_solver* s, int x){ s->setPropBudget(x); }+void         minisat_no_budget       (minisat_solver* s){ s->budgetOff(); }++// Resource constraints:+void minisat_interrupt(minisat_solver* s) {s->interrupt (); }+void minisat_clearInterrupt(minisat_solver* s) {s->clearInterrupt (); }++// SimpSolver methods:+void         minisat_setFrozen       (minisat_solver* s, minisat_Var v, minisat_bool b) { s->setFrozen(v, b); }+minisat_bool minisat_isEliminated    (minisat_solver* s, minisat_Var v) { return s->isEliminated(v); }+minisat_bool minisat_eliminate       (minisat_solver* s, minisat_bool turn_off_elim){ return s->eliminate(turn_off_elim); }++// Convenience functions for actual c-programmers (not language interfacing people):+//+int  minisat_solve(minisat_solver *s, int len, minisat_Lit *ps)+{+    s->assumps.clear();+    for (int i = 0; i < len; i++)+        s->assumps.push(toLit(ps[i]));+    return s->solve(s->assumps);+}+++minisat_lbool minisat_limited_solve(minisat_solver *s, int len, minisat_Lit *ps)+{+    s->assumps.clear();+    for (int i = 0; i < len; i++)+        s->assumps.push(toLit(ps[i]));+    return toC(s->solveLimited(s->assumps));+}+++int  minisat_addClause(minisat_solver *s, int len, minisat_Lit *ps)+{+    s->clause.clear();+    for (int i = 0; i < len; i++)+        s->clause.push(toLit(ps[i]));+    return s->addClause_(s->clause);+}+++}
+ minisat-c-bindings/minisat.h view
@@ -0,0 +1,149 @@+/***************************************************************************************[minisat.h]+Copyright (c) 2008-2011, Niklas Sorensson+              2008, Koen Claessen++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 Minisat_C_Bindings_h+#define Minisat_C_Bindings_h++// SolverTypes:+//+typedef struct minisat_solver_t minisat_solver;+#ifdef Minisat_Opaque+#define opaque(x) struct { x f; }+#else+#define opaque(x) x+#endif+typedef opaque(int) minisat_Var;+typedef opaque(int) minisat_Lit;+typedef opaque(int) minisat_lbool;+typedef opaque(int) minisat_bool; // Only for clarity in the declarations below (this is just a plain c-bool).+#undef opaque++// Constants: (can these be made inline-able?)+//++extern const minisat_lbool minisat_l_True;+extern const minisat_lbool minisat_l_False;+extern const minisat_lbool minisat_l_Undef;+++minisat_solver* minisat_new             (void);+void            minisat_delete          (minisat_solver* s);+             +minisat_Var     minisat_newVar          (minisat_solver *s);+minisat_Lit     minisat_newLit          (minisat_solver *s);+             +minisat_Lit     minisat_mkLit           (minisat_Var x);+minisat_Lit     minisat_mkLit_args      (minisat_Var x, int sign);+minisat_Lit     minisat_negate          (minisat_Lit p);+                                    +minisat_Var     minisat_var             (minisat_Lit p);+minisat_bool    minisat_sign            (minisat_Lit p);+             +minisat_bool    minisat_addClause       (minisat_solver *s, int len, minisat_Lit *ps);+void            minisat_addClause_begin (minisat_solver *s);+void            minisat_addClause_addLit(minisat_solver *s, minisat_Lit p);+minisat_bool    minisat_addClause_commit(minisat_solver *s);+             +minisat_bool    minisat_simplify        (minisat_solver *s);+             +minisat_bool    minisat_solve           (minisat_solver *s, int len, minisat_Lit *ps);+minisat_lbool   minisat_limited_solve   (minisat_solver *s, int len, minisat_Lit *ps);+void            minisat_solve_begin     (minisat_solver *s);+void            minisat_solve_addLit    (minisat_solver *s, minisat_Lit p);+minisat_bool    minisat_solve_commit    (minisat_solver *s);+minisat_lbool   minisat_limited_solve_commit+                                        (minisat_solver *s);+             +minisat_bool    minisat_okay            (minisat_solver *s);+             +void            minisat_setPolarity     (minisat_solver *s, minisat_Var v, int b);+void            minisat_setDecisionVar  (minisat_solver *s, minisat_Var v, int b);++minisat_lbool   minisat_get_l_True      (void);+minisat_lbool   minisat_get_l_False     (void);+minisat_lbool   minisat_get_l_Undef     (void);++minisat_lbool   minisat_value_Var       (minisat_solver *s, minisat_Var x);+minisat_lbool   minisat_value_Lit       (minisat_solver *s, minisat_Lit p);+minisat_lbool   minisat_modelValue_Var  (minisat_solver *s, minisat_Var x);+minisat_lbool   minisat_modelValue_Lit  (minisat_solver *s, minisat_Lit p);++int             minisat_num_assigns     (minisat_solver *s);+int             minisat_num_clauses     (minisat_solver *s);     +int             minisat_num_learnts     (minisat_solver *s);     +int             minisat_num_vars        (minisat_solver *s);  +int             minisat_num_freeVars    (minisat_solver *s);++int             minisat_conflict_len    (minisat_solver *s);+minisat_Lit     minisat_conflict_nthLit (minisat_solver *s, int i);++void            minisat_set_conf_budget (minisat_solver* s, int x);+void            minisat_set_prop_budget (minisat_solver* s, int x);+void            minisat_no_budget       (minisat_solver* s);++// Resource constraints:+void minisat_interrupt(minisat_solver* s);+void minisat_clearInterrupt(minisat_solver* s);++// SimpSolver methods:+void            minisat_setFrozen       (minisat_solver* s, minisat_Var v, minisat_bool b);+minisat_bool    minisat_isEliminated    (minisat_solver* s, minisat_Var v);+minisat_bool    minisat_eliminate       (minisat_solver* s, minisat_bool turn_off_elim);++// Setters:++void            minisat_set_verbosity   (minisat_solver *s, int v);++// Getters:++int             minisat_num_conflicts   (minisat_solver *s);+int             minisat_num_decisions   (minisat_solver *s);+int             minisat_num_restarts    (minisat_solver *s);+int             minisat_num_propagations(minisat_solver *s);++/* TODO++    // Mode of operation:+    //+    int       verbosity;+    double    var_decay;+    double    clause_decay;+    double    random_var_freq;+    double    random_seed;+    double    restart_luby_start; // The factor with which the values of the luby sequence is multiplied to get the restart    (default 100)+    double    restart_luby_inc;   // The constant that the luby sequence uses powers of                                        (default 2)+    bool      expensive_ccmin;    // FIXME: describe.+    bool      rnd_pol;            // FIXME: describe.++    int       restart_first;      // The initial restart limit.                                                                (default 100)+    double    restart_inc;        // The factor with which the restart limit is multiplied in each restart.                    (default 1.5)+    double    learntsize_factor;  // The intitial limit for learnt clauses is a factor of the original clauses.                (default 1 / 3)+    double    learntsize_inc;     // The limit for learnt clauses is multiplied with this factor each restart.                 (default 1.1)++    int       learntsize_adjust_start_confl;+    double    learntsize_adjust_inc;++    // Statistics: (read-only member variable)+    //+    uint64_t starts, decisions, rnd_decisions, propagations, conflicts;+    uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;+*/++#endif
+ minisat-haskell-bindings/MiniSat.hsc view
@@ -0,0 +1,179 @@+{-# LANGUAGE ForeignFunctionInterface #-}+{-# LANGUAGE ScopedTypeVariables #-}++module MiniSat where++import Foreign.Ptr     ( Ptr, nullPtr )+import Foreign.C.Types ( CInt(..) )+import Control.Exception (bracket, finally, mask_, onException )+import Control.Concurrent.Async++#include "minisat.h"+#include "hsc-magic.h"++-- | Run a minisat instance in such a way that it is+-- interruptable (by sending killThread).+-- cf. https://github.com/niklasso/minisat-haskell-bindings/issues/1+withNewSolverAsync :: (Solver -> IO a) -> IO a+withNewSolverAsync h = +  bracket newSolver deleteSolver $ \  s -> do+    mask_ $ withAsync (h s) $ \ a -> do+      wait a `onException` minisat_interrupt s++withNewSolver :: (Solver -> IO a) -> IO a+withNewSolver h =+  do s <- newSolver+     h s `finally` deleteSolver s++newSolver :: IO Solver+newSolver =+  do s <- minisat_new+     eliminate s True -- make the default behave as a normal solver (avoiding common bugs)+     return s++deleteSolver :: Solver -> IO ()+deleteSolver = minisat_delete++newLit :: Solver -> IO Lit+newLit = minisat_newLit++neg :: Lit -> Lit+neg = minisat_negate++addClause :: Solver -> [Lit] -> IO Bool+addClause s xs =+  do minisat_addClause_begin s+     sequence_ [ minisat_addClause_addLit s x | x <- xs ]+     minisat_addClause_commit s++simplify :: Solver -> IO Bool+simplify = minisat_simplify++eliminate :: Solver -> Bool -> IO Bool+eliminate = minisat_eliminate++setFrozen :: Solver -> Var -> Bool -> IO ()+setFrozen = minisat_setFrozen++isEliminated :: Solver -> Var -> IO Bool+isEliminated = minisat_isEliminated++{-+solve :: Solver -> [Lit] -> Model a -> IO (Either [Lit] a)+-}++solve :: Solver -> [Lit] -> IO Bool+solve s xs =+  do minisat_solve_begin s+     sequence_ [ minisat_solve_addLit s x | x <- xs ]+     minisat_solve_commit s++limited_solve :: Solver -> [Lit] -> IO LBool+limited_solve s xs =+  do minisat_solve_begin s+     sequence_ [ minisat_solve_addLit s x | x <- xs ]+     minisat_limited_solve_commit s++value, modelValue :: Solver -> Lit -> IO (Maybe Bool)+(value,modelValue) = (get minisat_value_Lit, get minisat_modelValue_Lit)+ where+  get f s x = mbool `fmap` f s x++  mbool b +    | b == l_False = Just False+    | b == l_True  = Just True+    | otherwise    = Nothing++conflict :: Solver -> IO [Lit]+conflict s =+  do n <- minisat_conflict_len s+     sequence [ minisat_conflict_nthLit s i | i <- [0..n-1] ]++-- TODO: Is it possible to FFI C constants, instead of using a dummy function?+l_True, l_False, l_Undef :: LBool+l_True  = minisat_get_l_True+l_False = minisat_get_l_False+l_Undef = minisat_get_l_Undef++----------------------------------------------------------------------------++newtype Solver = MkSolver (Ptr ())+newtype Var    = MkVar CInt  deriving ( Eq, Ord )+newtype Lit    = MkLit CInt  deriving ( Eq, Ord )+newtype LBool  = MkLBool CInt deriving ( Eq, Ord )++instance Show Var where+  show (MkVar n) = 'v' : show n++instance Show Lit where+  show x = (if minisat_sign x then "~" else "") ++ show (minisat_var x) ++instance Show LBool where+  show b+    | b == l_False = "False"+    | b == l_True  = "True"+    | otherwise    = "Undef"++#define CTYPE_solver minisat_solver*+#define HTYPE_solver Solver+#define CTYPE_bool minisat_bool+#define HTYPE_bool Bool+#define CTYPE_lit minisat_Lit+#define HTYPE_lit Lit+#define CTYPE_int int+#define HTYPE_int Int+#define CTYPE_var minisat_Var+#define HTYPE_var Var+#define CTYPE_lbool minisat_lbool+#define HTYPE_lbool LBool++#unsafe minisat_new,              0, io(solver)+#unsafe minisat_delete,           1(solver), io(unit)+#unsafe minisat_newVar,           1(solver), io(var)+#unsafe minisat_newLit,           1(solver), io(lit)+#unsafe minisat_mkLit,            1(var), lit+#unsafe minisat_mkLit_args,       2(var, int), lit+#unsafe minisat_negate,           1(lit), lit+#unsafe minisat_var,              1(lit), var+#unsafe minisat_sign,             1(lit), bool+#unsafe minisat_addClause,        3(solver, int, ptr(lit)), io(bool)+#unsafe minisat_addClause_begin,  1(solver), io(unit)+#unsafe minisat_addClause_addLit, 2(solver, lit), io(unit)+#unsafe minisat_addClause_commit, 1(solver), io(bool)+#unsafe minisat_simplify,         1(solver), io(bool)+#safe minisat_solve,              3(solver, int, ptr(lit)), io(bool)+#unsafe minisat_solve_begin,      1(solver), io(unit)+#unsafe minisat_solve_addLit,     2(solver, lit), io(unit)+#safe minisat_solve_commit,       1(solver), io(bool)+#safe minisat_limited_solve_commit,       1(solver), io(lbool)++#safe minisat_interrupt,          1(solver), io(unit)+#safe minisat_clearInterrupt,     1(solver), io(unit)++#unsafe minisat_okay,             1(solver), io(bool)+#unsafe minisat_setPolarity,      3(solver, var, int), io(unit)+#unsafe minisat_setDecisionVar,   3(solver, var, int), io(unit)+#unsafe minisat_value_Var,        2(solver, var), io(lbool)+#unsafe minisat_value_Lit,        2(solver, lit), io(lbool)+#unsafe minisat_modelValue_Var,   2(solver, var), io(lbool)+#unsafe minisat_modelValue_Lit,   2(solver, lit), io(lbool)++#unsafe minisat_get_l_True,       0, lbool+#unsafe minisat_get_l_False,      0, lbool+#unsafe minisat_get_l_Undef,      0, lbool++-- // Simpsolver methods:+#unsafe minisat_setFrozen,        3(solver, var, bool), io(unit)+#unsafe minisat_isEliminated,     2(solver, var), io(bool)+#unsafe minisat_eliminate,        2(solver, bool), io(bool)++#unsafe minisat_num_assigns,      1(solver), io(int)+#unsafe minisat_num_clauses,      1(solver), io(int)+#unsafe minisat_num_learnts,      1(solver), io(int)+#unsafe minisat_num_vars,         1(solver), io(int)+#unsafe minisat_num_freeVars,     1(solver), io(int)+#unsafe minisat_num_conflicts,    1(solver), io(int)++#unsafe minisat_conflict_len,     1(solver), io(int)+#unsafe minisat_conflict_nthLit,  2(solver, int), io(lit)+#unsafe minisat_set_verbosity,    2(solver, int), io(unit)
+ minisat-haskell-bindings/hsc-magic.h view
@@ -0,0 +1,28 @@+#include <stdio.h>+#define hsc_unsafe(name, args, res) GO(unsafe, name, args, res)+#define hsc_safe(name, args, res) GO(safe, name, args, res)++#define GO(safety, name, args, res) \+    extern CTYPE_##res name(CTYPE_##args);     \+    printf("%s\n", STR(foreign import ccall safety name :: HTYPE_##args HTYPE_##res));++#define STR(x) STR2(x)+#define STR2(x) #x++#define CTYPE_io(x) CTYPE_##x+#define CTYPE_ptr(x) CTYPE_##x*+#define CTYPE_unit void+#define CTYPE_0+#define CTYPE_1(x) CTYPE_##x+#define CTYPE_2(x,y) CTYPE_##x, CTYPE_##y+#define CTYPE_3(x,y,z) CTYPE_##x, CTYPE_##y, CTYPE_##z+#define CTYPE_4(x,y,z,w) CTYPE_##x, CTYPE_##y, CTYPE_##z, CTYPE_##w++#define HTYPE_io(x) IO (HTYPE_##x)+#define HTYPE_ptr(x) Ptr (HTYPE_##x)+#define HTYPE_unit ()+#define HTYPE_0+#define HTYPE_1(x) HTYPE_##x ->+#define HTYPE_2(x,y) HTYPE_##x -> HTYPE_##y ->+#define HTYPE_3(x,y,z) HTYPE_##x -> HTYPE_##y -> HTYPE_##z ->+#define HTYPE_4(x,y,z,w) HTYPE_##x -> HTYPE_##y -> HTYPE_##z -> HTYPE_##w ->
+ minisat.cabal view
@@ -0,0 +1,37 @@+name:            minisat+version:         0.1+build-type:      Simple+cabal-version:   >= 1.6+Synopsis:        A Haskell bundle of the Minisat SAT solver+Category:        Logic+License:         BSD3+License-File:    LICENSE+extra-source-files: minisat-c-bindings/minisat.h+                    minisat-haskell-bindings/hsc-magic.h+                    minisat/minisat/simp/*.h+                    minisat/minisat/mtl/*.h+                    minisat/minisat/core/*.h+                    minisat/minisat/utils/*.h++source-repository head+  type:     git+  location: https://github.com/jbransen/minisat-bundle.git++library+  extensions:      ForeignFunctionInterface+  build-depends:   base >= 3 && < 5, async+  -- On Windows finding the library is harder, so depend on+  -- Haskell zlib package which also contains the z library+  if os(windows)+     build-depends: zlib+  else+     extra-libraries: z+  C-sources:       minisat-c-bindings/minisat.cc+                   minisat/minisat/core/Solver.cc+                   minisat/minisat/simp/SimpSolver.cc+                   minisat/minisat/utils/System.cc+  CC-options:      -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS+  extra-libraries: stdc+++  hs-source-dirs:  minisat-haskell-bindings+  include-dirs:    minisat-haskell-bindings, minisat-c-bindings, minisat+  exposed-modules: MiniSat
+ minisat/minisat/core/Dimacs.h view
@@ -0,0 +1,87 @@+/****************************************************************************************[Dimacs.h]+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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 Minisat_Dimacs_h+#define Minisat_Dimacs_h++#include <stdio.h>++#include "minisat/utils/ParseUtils.h"+#include "minisat/core/SolverTypes.h"++namespace Minisat {++//=================================================================================================+// DIMACS Parser:++template<class B, class Solver>+static void readClause(B& in, Solver& S, vec<Lit>& lits) {+    int     parsed_lit, var;+    lits.clear();+    for (;;){+        parsed_lit = parseInt(in);+        if (parsed_lit == 0) break;+        var = abs(parsed_lit)-1;+        while (var >= S.nVars()) S.newVar();+        lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );+    }+}++template<class B, class Solver>+static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) {+    vec<Lit> lits;+    int vars    = 0;+    int clauses = 0;+    int cnt     = 0;+    for (;;){+        skipWhitespace(in);+        if (*in == EOF) break;+        else if (*in == 'p'){+            if (eagerMatch(in, "p cnf")){+                vars    = parseInt(in);+                clauses = parseInt(in);+                // SATRACE'06 hack+                // if (clauses > 4000000)+                //     S.eliminate(true);+            }else{+                printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);+            }+        } else if (*in == 'c' || *in == 'p')+            skipLine(in);+        else{+            cnt++;+            readClause(in, S, lits);+            S.addClause_(lits); }+    }+    if (strictp && cnt != clauses)+        printf("PARSE ERROR! DIMACS header mismatch: wrong number of clauses\n");+}++// Inserts problem into solver.+//+template<class Solver>+static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {+    StreamBuffer in(input_stream);+    parse_DIMACS_main(in, S, strictp); }++//=================================================================================================+}++#endif
+ minisat/minisat/core/Solver.cc view
@@ -0,0 +1,1072 @@+/***************************************************************************************[Solver.cc]+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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.+**************************************************************************************************/++// It seems that we trigger a compiler bug in MinGW in the code below, so+// turn off the optimisations for now+#if defined(__MINGW32__)+#pragma GCC optimize "O0"+#endif++#include <math.h>++#include "minisat/mtl/Alg.h"+#include "minisat/mtl/Sort.h"+#include "minisat/utils/System.h"+#include "minisat/core/Solver.h"++using namespace Minisat;++//=================================================================================================+// Options:+++static const char* _cat = "CORE";++static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));+static DoubleOption  opt_clause_decay      (_cat, "cla-decay",   "The clause activity decay factor",              0.999,    DoubleRange(0, false, 1, false));+static DoubleOption  opt_random_var_freq   (_cat, "rnd-freq",    "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true));+static DoubleOption  opt_random_seed       (_cat, "rnd-seed",    "Used by the random variable selection",         91648253, DoubleRange(0, false, HUGE_VAL, false));+static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2));+static IntOption     opt_phase_saving      (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));+static BoolOption    opt_rnd_init_act      (_cat, "rnd-init",    "Randomize the initial activity", false);+static BoolOption    opt_luby_restart      (_cat, "luby",        "Use the Luby restart sequence", true);+static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 100, IntRange(1, INT32_MAX));+static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false));+static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction of wasted memory allowed before a garbage collection is triggered",  0.20, DoubleRange(0, false, HUGE_VAL, false));+static IntOption     opt_min_learnts_lim   (_cat, "min-learnts", "Minimum learnt clause limit",  0, IntRange(0, INT32_MAX));+++//=================================================================================================+// Constructor/Destructor:+++Solver::Solver() :++    // Parameters (user settable):+    //+    verbosity        (0)+  , var_decay        (opt_var_decay)+  , clause_decay     (opt_clause_decay)+  , random_var_freq  (opt_random_var_freq)+  , random_seed      (opt_random_seed)+  , luby_restart     (opt_luby_restart)+  , ccmin_mode       (opt_ccmin_mode)+  , phase_saving     (opt_phase_saving)+  , rnd_pol          (false)+  , rnd_init_act     (opt_rnd_init_act)+  , garbage_frac     (opt_garbage_frac)+  , min_learnts_lim  (opt_min_learnts_lim)+  , restart_first    (opt_restart_first)+  , restart_inc      (opt_restart_inc)++    // Parameters (the rest):+    //+  , learntsize_factor((double)1/(double)3), learntsize_inc(1.1)++    // Parameters (experimental):+    //+  , learntsize_adjust_start_confl (100)+  , learntsize_adjust_inc         (1.5)++    // Statistics: (formerly in 'SolverStats')+    //+  , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)+  , dec_vars(0), num_clauses(0), num_learnts(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)++  , watches            (WatcherDeleted(ca))+  , order_heap         (VarOrderLt(activity))+  , ok                 (true)+  , cla_inc            (1)+  , var_inc            (1)+  , qhead              (0)+  , simpDB_assigns     (-1)+  , simpDB_props       (0)+  , progress_estimate  (0)+  , remove_satisfied   (true)+  , next_var           (0)++    // Resource constraints:+    //+  , conflict_budget    (-1)+  , propagation_budget (-1)+  , asynch_interrupt   (false)+{}+++Solver::~Solver()+{+}+++//=================================================================================================+// Minor methods:+++// Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be+// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).+//+Var Solver::newVar(lbool upol, bool dvar)+{+    Var v;+    if (free_vars.size() > 0){+        v = free_vars.last();+        free_vars.pop();+    }else+        v = next_var++;++    watches  .init(mkLit(v, false));+    watches  .init(mkLit(v, true ));+    assigns  .insert(v, l_Undef);+    vardata  .insert(v, mkVarData(CRef_Undef, 0));+    activity .insert(v, rnd_init_act ? drand(random_seed) * 0.00001 : 0);+    seen     .insert(v, 0);+    polarity .insert(v, true);+    user_pol .insert(v, upol);+    decision .reserve(v);+    trail    .capacity(v+1);+    setDecisionVar(v, dvar);+    return v;+}+++// Note: at the moment, only unassigned variable will be released (this is to avoid duplicate+// releases of the same variable).+void Solver::releaseVar(Lit l)+{+    if (value(l) == l_Undef){+        addClause(l);+        released_vars.push(var(l));+    }+}+++bool Solver::addClause_(vec<Lit>& ps)+{+    assert(decisionLevel() == 0);+    if (!ok) return false;++    // Check if clause is satisfied and remove false/duplicate literals:+    sort(ps);+    Lit p; int i, j;+    for (i = j = 0, p = lit_Undef; i < ps.size(); i++)+        if (value(ps[i]) == l_True || ps[i] == ~p)+            return true;+        else if (value(ps[i]) != l_False && ps[i] != p)+            ps[j++] = p = ps[i];+    ps.shrink(i - j);++    if (ps.size() == 0)+        return ok = false;+    else if (ps.size() == 1){+        uncheckedEnqueue(ps[0]);+        return ok = (propagate() == CRef_Undef);+    }else{+        CRef cr = ca.alloc(ps, false);+        clauses.push(cr);+        attachClause(cr);+    }++    return true;+}+++void Solver::attachClause(CRef cr){+    const Clause& c = ca[cr];+    assert(c.size() > 1);+    watches[~c[0]].push(Watcher(cr, c[1]));+    watches[~c[1]].push(Watcher(cr, c[0]));+    if (c.learnt()) num_learnts++, learnts_literals += c.size();+    else            num_clauses++, clauses_literals += c.size();+}+++void Solver::detachClause(CRef cr, bool strict){+    const Clause& c = ca[cr];+    assert(c.size() > 1);+    +    // Strict or lazy detaching:+    if (strict){+        remove(watches[~c[0]], Watcher(cr, c[1]));+        remove(watches[~c[1]], Watcher(cr, c[0]));+    }else{+        watches.smudge(~c[0]);+        watches.smudge(~c[1]);+    }++    if (c.learnt()) num_learnts--, learnts_literals -= c.size();+    else            num_clauses--, clauses_literals -= c.size();+}+++void Solver::removeClause(CRef cr) {+    Clause& c = ca[cr];+    detachClause(cr);+    // Don't leave pointers to free'd memory!+    if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;+    c.mark(1); +    ca.free(cr);+}+++bool Solver::satisfied(const Clause& c) const {+    for (int i = 0; i < c.size(); i++)+        if (value(c[i]) == l_True)+            return true;+    return false; }+++// Revert to the state at given level (keeping all assignment at 'level' but not beyond).+//+void Solver::cancelUntil(int level) {+    if (decisionLevel() > level){+        for (int c = trail.size()-1; c >= trail_lim[level]; c--){+            Var      x  = var(trail[c]);+            assigns [x] = l_Undef;+            if (phase_saving > 1 || (phase_saving == 1 && c > trail_lim.last()))+                polarity[x] = sign(trail[c]);+            insertVarOrder(x); }+        qhead = trail_lim[level];+        trail.shrink(trail.size() - trail_lim[level]);+        trail_lim.shrink(trail_lim.size() - level);+    } }+++//=================================================================================================+// Major methods:+++Lit Solver::pickBranchLit()+{+    Var next = var_Undef;++    // Random decision:+    if (drand(random_seed) < random_var_freq && !order_heap.empty()){+        next = order_heap[irand(random_seed,order_heap.size())];+        if (value(next) == l_Undef && decision[next])+            rnd_decisions++; }++    // Activity based decision:+    while (next == var_Undef || value(next) != l_Undef || !decision[next])+        if (order_heap.empty()){+            next = var_Undef;+            break;+        }else+            next = order_heap.removeMin();++    // Choose polarity based on different polarity modes (global or per-variable):+    if (next == var_Undef)+        return lit_Undef;+    else if (user_pol[next] != l_Undef)+        return mkLit(next, user_pol[next] == l_True);+    else if (rnd_pol)+        return mkLit(next, drand(random_seed) < 0.5);+    else+        return mkLit(next, polarity[next]);+}+++/*_________________________________________________________________________________________________+|+|  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->  [void]+|  +|  Description:+|    Analyze conflict and produce a reason clause.+|  +|    Pre-conditions:+|      * 'out_learnt' is assumed to be cleared.+|      * Current decision level must be greater than root level.+|  +|    Post-conditions:+|      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.+|      * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the +|        rest of literals. There may be others from the same level though.+|  +|________________________________________________________________________________________________@*/+void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)+{+    int pathC = 0;+    Lit p     = lit_Undef;++    // Generate conflict clause:+    //+    out_learnt.push();      // (leave room for the asserting literal)+    int index   = trail.size() - 1;++    do{+        assert(confl != CRef_Undef); // (otherwise should be UIP)+        Clause& c = ca[confl];++        if (c.learnt())+            claBumpActivity(c);++        for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){+            Lit q = c[j];++            if (!seen[var(q)] && level(var(q)) > 0){+                varBumpActivity(var(q));+                seen[var(q)] = 1;+                if (level(var(q)) >= decisionLevel())+                    pathC++;+                else+                    out_learnt.push(q);+            }+        }+        +        // Select next clause to look at:+        while (!seen[var(trail[index--])]);+        p     = trail[index+1];+        confl = reason(var(p));+        seen[var(p)] = 0;+        pathC--;++    }while (pathC > 0);+    out_learnt[0] = ~p;++    // Simplify conflict clause:+    //+    int i, j;+    out_learnt.copyTo(analyze_toclear);+    if (ccmin_mode == 2){+        for (i = j = 1; i < out_learnt.size(); i++)+            if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i]))+                out_learnt[j++] = out_learnt[i];+        +    }else if (ccmin_mode == 1){+        for (i = j = 1; i < out_learnt.size(); i++){+            Var x = var(out_learnt[i]);++            if (reason(x) == CRef_Undef)+                out_learnt[j++] = out_learnt[i];+            else{+                Clause& c = ca[reason(var(out_learnt[i]))];+                for (int k = 1; k < c.size(); k++)+                    if (!seen[var(c[k])] && level(var(c[k])) > 0){+                        out_learnt[j++] = out_learnt[i];+                        break; }+            }+        }+    }else+        i = j = out_learnt.size();++    max_literals += out_learnt.size();+    out_learnt.shrink(i - j);+    tot_literals += out_learnt.size();++    // Find correct backtrack level:+    //+    if (out_learnt.size() == 1)+        out_btlevel = 0;+    else{+        int max_i = 1;+        // Find the first literal assigned at the next-highest level:+        for (int i = 2; i < out_learnt.size(); i++)+            if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))+                max_i = i;+        // Swap-in this literal at index 1:+        Lit p             = out_learnt[max_i];+        out_learnt[max_i] = out_learnt[1];+        out_learnt[1]     = p;+        out_btlevel       = level(var(p));+    }++    for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)+}+++// Check if 'p' can be removed from a conflict clause.+bool Solver::litRedundant(Lit p)+{+    enum { seen_undef = 0, seen_source = 1, seen_removable = 2, seen_failed = 3 };+    assert(seen[var(p)] == seen_undef || seen[var(p)] == seen_source);+    assert(reason(var(p)) != CRef_Undef);++    Clause*               c     = &ca[reason(var(p))];+    vec<ShrinkStackElem>& stack = analyze_stack;+    stack.clear();++    for (uint32_t i = 1; ; i++){+        if (i < (uint32_t)c->size()){+            // Checking 'p'-parents 'l':+            Lit l = (*c)[i];+            +            // Variable at level 0 or previously removable:+            if (level(var(l)) == 0 || seen[var(l)] == seen_source || seen[var(l)] == seen_removable){+                continue; }+            +            // Check variable can not be removed for some local reason:+            if (reason(var(l)) == CRef_Undef || seen[var(l)] == seen_failed){+                stack.push(ShrinkStackElem(0, p));+                for (int i = 0; i < stack.size(); i++)+                    if (seen[var(stack[i].l)] == seen_undef){+                        seen[var(stack[i].l)] = seen_failed;+                        analyze_toclear.push(stack[i].l);+                    }+                    +                return false;+            }++            // Recursively check 'l':+            stack.push(ShrinkStackElem(i, p));+            i  = 0;+            p  = l;+            c  = &ca[reason(var(p))];+        }else{+            // Finished with current element 'p' and reason 'c':+            if (seen[var(p)] == seen_undef){+                seen[var(p)] = seen_removable;+                analyze_toclear.push(p);+            }++            // Terminate with success if stack is empty:+            if (stack.size() == 0) break;+            +            // Continue with top element on stack:+            i  = stack.last().i;+            p  = stack.last().l;+            c  = &ca[reason(var(p))];++            stack.pop();+        }+    }++    return true;+}+++/*_________________________________________________________________________________________________+|+|  analyzeFinal : (p : Lit)  ->  [void]+|  +|  Description:+|    Specialized analysis procedure to express the final conflict in terms of assumptions.+|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and+|    stores the result in 'out_conflict'.+|________________________________________________________________________________________________@*/+void Solver::analyzeFinal(Lit p, LSet& out_conflict)+{+    out_conflict.clear();+    out_conflict.insert(p);++    if (decisionLevel() == 0)+        return;++    seen[var(p)] = 1;++    for (int i = trail.size()-1; i >= trail_lim[0]; i--){+        Var x = var(trail[i]);+        if (seen[x]){+            if (reason(x) == CRef_Undef){+                assert(level(x) > 0);+                out_conflict.insert(~trail[i]);+            }else{+                Clause& c = ca[reason(x)];+                for (int j = 1; j < c.size(); j++)+                    if (level(var(c[j])) > 0)+                        seen[var(c[j])] = 1;+            }+            seen[x] = 0;+        }+    }++    seen[var(p)] = 0;+}+++void Solver::uncheckedEnqueue(Lit p, CRef from)+{+    assert(value(p) == l_Undef);+    assigns[var(p)] = lbool(!sign(p));+    vardata[var(p)] = mkVarData(from, decisionLevel());+    trail.push_(p);+}+++/*_________________________________________________________________________________________________+|+|  propagate : [void]  ->  [Clause*]+|  +|  Description:+|    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,+|    otherwise CRef_Undef.+|  +|    Post-conditions:+|      * the propagation queue is empty, even if there was a conflict.+|________________________________________________________________________________________________@*/+CRef Solver::propagate()+{+    CRef    confl     = CRef_Undef;+    int     num_props = 0;++    while (qhead < trail.size()){+        Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.+        vec<Watcher>&  ws  = watches.lookup(p);+        Watcher        *i, *j, *end;+        num_props++;++        for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){+            // Try to avoid inspecting the clause:+            Lit blocker = i->blocker;+            if (value(blocker) == l_True){+                *j++ = *i++; continue; }++            // Make sure the false literal is data[1]:+            CRef     cr        = i->cref;+            Clause&  c         = ca[cr];+            Lit      false_lit = ~p;+            if (c[0] == false_lit)+                c[0] = c[1], c[1] = false_lit;+            assert(c[1] == false_lit);+            i++;++            // If 0th watch is true, then clause is already satisfied.+            Lit     first = c[0];+            Watcher w     = Watcher(cr, first);+            if (first != blocker && value(first) == l_True){+                *j++ = w; continue; }++            // Look for new watch:+            for (int k = 2; k < c.size(); k++)+                if (value(c[k]) != l_False){+                    c[1] = c[k]; c[k] = false_lit;+                    watches[~c[1]].push(w);+                    goto NextClause; }++            // Did not find watch -- clause is unit under assignment:+            *j++ = w;+            if (value(first) == l_False){+                confl = cr;+                qhead = trail.size();+                // Copy the remaining watches:+                while (i < end)+                    *j++ = *i++;+            }else+                uncheckedEnqueue(first, cr);++        NextClause:;+        }+        ws.shrink(i - j);+    }+    propagations += num_props;+    simpDB_props -= num_props;++    return confl;+}+++/*_________________________________________________________________________________________________+|+|  reduceDB : ()  ->  [void]+|  +|  Description:+|    Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked+|    clauses are clauses that are reason to some assignment. Binary clauses are never removed.+|________________________________________________________________________________________________@*/+struct reduceDB_lt { +    ClauseAllocator& ca;+    reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}+    bool operator () (CRef x, CRef y) { +        return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } +};+void Solver::reduceDB()+{+    int     i, j;+    double  extra_lim = cla_inc / learnts.size();    // Remove any clause below this activity++    sort(learnts, reduceDB_lt(ca));+    // Don't delete binary or locked clauses. From the rest, delete clauses from the first half+    // and clauses with activity smaller than 'extra_lim':+    for (i = j = 0; i < learnts.size(); i++){+        Clause& c = ca[learnts[i]];+        if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim))+            removeClause(learnts[i]);+        else+            learnts[j++] = learnts[i];+    }+    learnts.shrink(i - j);+    checkGarbage();+}+++void Solver::removeSatisfied(vec<CRef>& cs)+{+    int i, j;+    for (i = j = 0; i < cs.size(); i++){+        Clause& c = ca[cs[i]];+        if (satisfied(c))+            removeClause(cs[i]);+        else{+            // Trim clause:+            assert(value(c[0]) == l_Undef && value(c[1]) == l_Undef);+            for (int k = 2; k < c.size(); k++)+                if (value(c[k]) == l_False){+                    c[k--] = c[c.size()-1];+                    c.pop();+                }+            cs[j++] = cs[i];+        }+    }+    cs.shrink(i - j);+}+++void Solver::rebuildOrderHeap()+{+    vec<Var> vs;+    for (Var v = 0; v < nVars(); v++)+        if (decision[v] && value(v) == l_Undef)+            vs.push(v);+    order_heap.build(vs);+}+++/*_________________________________________________________________________________________________+|+|  simplify : [void]  ->  [bool]+|  +|  Description:+|    Simplify the clause database according to the current top-level assigment. Currently, the only+|    thing done here is the removal of satisfied clauses, but more things can be put here.+|________________________________________________________________________________________________@*/+bool Solver::simplify()+{+    assert(decisionLevel() == 0);++    if (!ok || propagate() != CRef_Undef)+        return ok = false;++    if (nAssigns() == simpDB_assigns || (simpDB_props > 0))+        return true;++    // Remove satisfied clauses:+    removeSatisfied(learnts);+    if (remove_satisfied){       // Can be turned off.+        removeSatisfied(clauses);++        // TODO: what todo in if 'remove_satisfied' is false?++        // Remove all released variables from the trail:+        for (int i = 0; i < released_vars.size(); i++){+            assert(seen[released_vars[i]] == 0);+            seen[released_vars[i]] = 1;+        }++        int i, j;+        for (i = j = 0; i < trail.size(); i++)+            if (seen[var(trail[i])] == 0)+                trail[j++] = trail[i];+        trail.shrink(i - j);+        //printf("trail.size()= %d, qhead = %d\n", trail.size(), qhead);+        qhead = trail.size();++        for (int i = 0; i < released_vars.size(); i++)+            seen[released_vars[i]] = 0;++        // Released variables are now ready to be reused:+        append(released_vars, free_vars);+        released_vars.clear();+    }+    checkGarbage();+    rebuildOrderHeap();++    simpDB_assigns = nAssigns();+    simpDB_props   = clauses_literals + learnts_literals;   // (shouldn't depend on stats really, but it will do for now)++    return true;+}+++/*_________________________________________________________________________________________________+|+|  search : (nof_conflicts : int) (params : const SearchParams&)  ->  [lbool]+|  +|  Description:+|    Search for a model the specified number of conflicts. +|    NOTE! Use negative value for 'nof_conflicts' indicate infinity.+|  +|  Output:+|    'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If+|    all variables are decision variables, this means that the clause set is satisfiable. 'l_False'+|    if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.+|________________________________________________________________________________________________@*/+lbool Solver::search(int nof_conflicts)+{+    assert(ok);+    int         backtrack_level;+    int         conflictC = 0;+    vec<Lit>    learnt_clause;+    starts++;++    for (;;){+        CRef confl = propagate();+        if (confl != CRef_Undef){+            // CONFLICT+            conflicts++; conflictC++;+            if (decisionLevel() == 0) return l_False;++            learnt_clause.clear();+            analyze(confl, learnt_clause, backtrack_level);+            cancelUntil(backtrack_level);++            if (learnt_clause.size() == 1){+                uncheckedEnqueue(learnt_clause[0]);+            }else{+                CRef cr = ca.alloc(learnt_clause, true);+                learnts.push(cr);+                attachClause(cr);+                claBumpActivity(ca[cr]);+                uncheckedEnqueue(learnt_clause[0], cr);+            }++            varDecayActivity();+            claDecayActivity();++            if (--learntsize_adjust_cnt == 0){+                learntsize_adjust_confl *= learntsize_adjust_inc;+                learntsize_adjust_cnt    = (int)learntsize_adjust_confl;+                max_learnts             *= learntsize_inc;++                if (verbosity >= 1)+                    printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", +                           (int)conflicts, +                           (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, +                           (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);+            }++        }else{+            // NO CONFLICT+            if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){+                // Reached bound on number of conflicts:+                progress_estimate = progressEstimate();+                cancelUntil(0);+                return l_Undef; }++            // Simplify the set of problem clauses:+            if (decisionLevel() == 0 && !simplify())+                return l_False;++            if (learnts.size()-nAssigns() >= max_learnts)+                // Reduce the set of learnt clauses:+                reduceDB();++            Lit next = lit_Undef;+            while (decisionLevel() < assumptions.size()){+                // Perform user provided assumption:+                Lit p = assumptions[decisionLevel()];+                if (value(p) == l_True){+                    // Dummy decision level:+                    newDecisionLevel();+                }else if (value(p) == l_False){+                    analyzeFinal(~p, conflict);+                    return l_False;+                }else{+                    next = p;+                    break;+                }+            }++            if (next == lit_Undef){+                // New variable decision:+                decisions++;+                next = pickBranchLit();++                if (next == lit_Undef)+                    // Model found:+                    return l_True;+            }++            // Increase decision level and enqueue 'next'+            newDecisionLevel();+            uncheckedEnqueue(next);+        }+    }+}+++double Solver::progressEstimate() const+{+    double  progress = 0;+    double  F = 1.0 / nVars();++    for (int i = 0; i <= decisionLevel(); i++){+        int beg = i == 0 ? 0 : trail_lim[i - 1];+        int end = i == decisionLevel() ? trail.size() : trail_lim[i];+        progress += pow(F, i) * (end - beg);+    }++    return progress / nVars();+}++/*+  Finite subsequences of the Luby-sequence:++  0: 1+  1: 1 1 2+  2: 1 1 2 1 1 2 4+  3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8+  ...+++ */++static double luby(double y, int x){++    // Find the finite subsequence that contains index 'x', and the+    // size of that subsequence:+    int size, seq;+    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1);++    while (size-1 != x){+        size = (size-1)>>1;+        seq--;+        x = x % size;+    }++    return pow(y, seq);+}++// NOTE: assumptions passed in member-variable 'assumptions'.+lbool Solver::solve_()+{+    model.clear();+    conflict.clear();+    if (!ok) return l_False;++    solves++;++    max_learnts = nClauses() * learntsize_factor;+    if (max_learnts < min_learnts_lim)+        max_learnts = min_learnts_lim;++    learntsize_adjust_confl   = learntsize_adjust_start_confl;+    learntsize_adjust_cnt     = (int)learntsize_adjust_confl;+    lbool   status            = l_Undef;++    if (verbosity >= 1){+        printf("============================[ Search Statistics ]==============================\n");+        printf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");+        printf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");+        printf("===============================================================================\n");+    }++    // Search:+    int curr_restarts = 0;+    while (status == l_Undef){+        double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);+        status = search(rest_base * restart_first);+        if (!withinBudget()) break;+        curr_restarts++;+    }++    if (verbosity >= 1)+        printf("===============================================================================\n");+++    if (status == l_True){+        // Extend & copy model:+        model.growTo(nVars());+        for (int i = 0; i < nVars(); i++) model[i] = value(i);+    }else if (status == l_False && conflict.size() == 0)+        ok = false;++    cancelUntil(0);+    return status;+}+++bool Solver::implies(const vec<Lit>& assumps, vec<Lit>& out)+{+    trail_lim.push(trail.size());+    for (int i = 0; i < assumps.size(); i++){+        Lit a = assumps[i];++        if (value(a) == l_False){+            cancelUntil(0);+            return false;+        }else if (value(a) == l_Undef)+            uncheckedEnqueue(a);+    }++    unsigned trail_before = trail.size();+    bool     ret          = true;+    if (propagate() == CRef_Undef){+        out.clear();+        for (int j = trail_before; j < trail.size(); j++)+            out.push(trail[j]);+    }else+        ret = false;+    +    cancelUntil(0);+    return ret;+}++//=================================================================================================+// Writing CNF to DIMACS:+// +// FIXME: this needs to be rewritten completely.++static Var mapVar(Var x, vec<Var>& map, Var& max)+{+    if (map.size() <= x || map[x] == -1){+        map.growTo(x+1, -1);+        map[x] = max++;+    }+    return map[x];+}+++void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)+{+    if (satisfied(c)) return;++    for (int i = 0; i < c.size(); i++)+        if (value(c[i]) != l_False)+            fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1);+    fprintf(f, "0\n");+}+++void Solver::toDimacs(const char *file, const vec<Lit>& assumps)+{+    FILE* f = fopen(file, "wr");+    if (f == NULL)+        fprintf(stderr, "could not open file %s\n", file), exit(1);+    toDimacs(f, assumps);+    fclose(f);+}+++void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)+{+    // Handle case when solver is in contradictory state:+    if (!ok){+        fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");+        return; }++    vec<Var> map; Var max = 0;++    // Cannot use removeClauses here because it is not safe+    // to deallocate them at this point. Could be improved.+    int cnt = 0;+    for (int i = 0; i < clauses.size(); i++)+        if (!satisfied(ca[clauses[i]]))+            cnt++;+        +    for (int i = 0; i < clauses.size(); i++)+        if (!satisfied(ca[clauses[i]])){+            Clause& c = ca[clauses[i]];+            for (int j = 0; j < c.size(); j++)+                if (value(c[j]) != l_False)+                    mapVar(var(c[j]), map, max);+        }++    // Assumptions are added as unit clauses:+    cnt += assumps.size();++    fprintf(f, "p cnf %d %d\n", max, cnt);++    for (int i = 0; i < assumps.size(); i++){+        assert(value(assumps[i]) != l_False);+        fprintf(f, "%s%d 0\n", sign(assumps[i]) ? "-" : "", mapVar(var(assumps[i]), map, max)+1);+    }++    for (int i = 0; i < clauses.size(); i++)+        toDimacs(f, ca[clauses[i]], map, max);++    if (verbosity > 0)+        printf("Wrote DIMACS with %d variables and %d clauses.\n", max, cnt);+}+++void Solver::printStats() const+{+    double cpu_time = cpuTime();+    double mem_used = memUsedPeak();+    printf("restarts              : %"PRIu64"\n", starts);+    printf("conflicts             : %-12"PRIu64"   (%.0f /sec)\n", conflicts   , conflicts   /cpu_time);+    printf("decisions             : %-12"PRIu64"   (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions   /cpu_time);+    printf("propagations          : %-12"PRIu64"   (%.0f /sec)\n", propagations, propagations/cpu_time);+    printf("conflict literals     : %-12"PRIu64"   (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals);+    if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used);+    printf("CPU time              : %g s\n", cpu_time);+}+++//=================================================================================================+// Garbage Collection methods:++void Solver::relocAll(ClauseAllocator& to)+{+    // All watchers:+    //+    watches.cleanAll();+    for (int v = 0; v < nVars(); v++)+        for (int s = 0; s < 2; s++){+            Lit p = mkLit(v, s);+            vec<Watcher>& ws = watches[p];+            for (int j = 0; j < ws.size(); j++)+                ca.reloc(ws[j].cref, to);+        }++    // All reasons:+    //+    for (int i = 0; i < trail.size(); i++){+        Var v = var(trail[i]);++        // Note: it is not safe to call 'locked()' on a relocated clause. This is why we keep+        // 'dangling' reasons here. It is safe and does not hurt.+        if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)]))){+            assert(!isRemoved(reason(v)));+            ca.reloc(vardata[v].reason, to);+        }+    }++    // All learnt:+    //+    int i, j;+    for (i = j = 0; i < learnts.size(); i++)+        if (!isRemoved(learnts[i])){+            ca.reloc(learnts[i], to);+            learnts[j++] = learnts[i];+        }+    learnts.shrink(i - j);++    // All original:+    //+    for (i = j = 0; i < clauses.size(); i++)+        if (!isRemoved(clauses[i])){+            ca.reloc(clauses[i], to);+            clauses[j++] = clauses[i];+        }+    clauses.shrink(i - j);+}+++void Solver::garbageCollect()+{+    // Initialize the next region to a size corresponding to the estimated utilization degree. This+    // is not precise but should avoid some unnecessary reallocations for the new region:+    ClauseAllocator to(ca.size() - ca.wasted()); ++    relocAll(to);+    if (verbosity >= 2)+        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", +               ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);+    to.moveTo(ca);+}
+ minisat/minisat/core/Solver.h view
@@ -0,0 +1,409 @@+/****************************************************************************************[Solver.h]+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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 Minisat_Solver_h+#define Minisat_Solver_h++#include "minisat/mtl/Vec.h"+#include "minisat/mtl/Heap.h"+#include "minisat/mtl/Alg.h"+#include "minisat/mtl/IntMap.h"+#include "minisat/utils/Options.h"+#include "minisat/core/SolverTypes.h"+++namespace Minisat {++//=================================================================================================+// Solver -- the main class:++class Solver {+public:++    // Constructor/Destructor:+    //+    Solver();+    virtual ~Solver();++    // Problem specification:+    //+    Var     newVar    (lbool upol = l_Undef, bool dvar = true); // Add a new variable with parameters specifying variable mode.+    void    releaseVar(Lit l);                                  // Make literal true and promise to never refer to variable again.++    bool    addClause (const vec<Lit>& ps);                     // Add a clause to the solver. +    bool    addEmptyClause();                                   // Add the empty clause, making the solver contradictory.+    bool    addClause (Lit p);                                  // Add a unit clause to the solver. +    bool    addClause (Lit p, Lit q);                           // Add a binary clause to the solver. +    bool    addClause (Lit p, Lit q, Lit r);                    // Add a ternary clause to the solver. +    bool    addClause (Lit p, Lit q, Lit r, Lit s);             // Add a quaternary clause to the solver. +    bool    addClause_(      vec<Lit>& ps);                     // Add a clause to the solver without making superflous internal copy. Will+                                                                // change the passed vector 'ps'.++    // Solving:+    //+    bool    simplify     ();                        // Removes already satisfied clauses.+    bool    solve        (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.+    lbool   solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).+    bool    solve        ();                        // Search without assumptions.+    bool    solve        (Lit p);                   // Search for a model that respects a single assumption.+    bool    solve        (Lit p, Lit q);            // Search for a model that respects two assumptions.+    bool    solve        (Lit p, Lit q, Lit r);     // Search for a model that respects three assumptions.+    bool    okay         () const;                  // FALSE means solver is in a conflicting state++    bool    implies      (const vec<Lit>& assumps, vec<Lit>& out);++    // Iterate over clauses and top-level assignments:+    ClauseIterator clausesBegin() const;+    ClauseIterator clausesEnd()   const;+    TrailIterator  trailBegin()   const;+    TrailIterator  trailEnd  ()   const;++    void    toDimacs     (FILE* f, const vec<Lit>& assumps);            // Write CNF to file in DIMACS-format.+    void    toDimacs     (const char *file, const vec<Lit>& assumps);+    void    toDimacs     (FILE* f, Clause& c, vec<Var>& map, Var& max);++    // Convenience versions of 'toDimacs()':+    void    toDimacs     (const char* file);+    void    toDimacs     (const char* file, Lit p);+    void    toDimacs     (const char* file, Lit p, Lit q);+    void    toDimacs     (const char* file, Lit p, Lit q, Lit r);+    +    // Variable mode:+    // +    void    setPolarity    (Var v, lbool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.+    void    setDecisionVar (Var v, bool b);  // Declare if a variable should be eligible for selection in the decision heuristic.++    // Read state:+    //+    lbool   value      (Var x) const;       // The current value of a variable.+    lbool   value      (Lit p) const;       // The current value of a literal.+    lbool   modelValue (Var x) const;       // The value of a variable in the last model. The last call to solve must have been satisfiable.+    lbool   modelValue (Lit p) const;       // The value of a literal in the last model. The last call to solve must have been satisfiable.+    int     nAssigns   ()      const;       // The current number of assigned literals.+    int     nClauses   ()      const;       // The current number of original clauses.+    int     nLearnts   ()      const;       // The current number of learnt clauses.+    int     nVars      ()      const;       // The current number of variables.+    int     nFreeVars  ()      const;+    void    printStats ()      const;       // Print some current statistics to standard output.++    // Resource contraints:+    //+    void    setConfBudget(int64_t x);+    void    setPropBudget(int64_t x);+    void    budgetOff();+    void    interrupt();          // Trigger a (potentially asynchronous) interruption of the solver.+    void    clearInterrupt();     // Clear interrupt indicator flag.++    // Memory managment:+    //+    virtual void garbageCollect();+    void    checkGarbage(double gf);+    void    checkGarbage();++    // Extra results: (read-only member variable)+    //+    vec<lbool> model;             // If problem is satisfiable, this vector contains the model (if any).+    LSet       conflict;          // If problem is unsatisfiable (possibly under assumptions),+                                  // this vector represent the final conflict clause expressed in the assumptions.++    // Mode of operation:+    //+    int       verbosity;+    double    var_decay;+    double    clause_decay;+    double    random_var_freq;+    double    random_seed;+    bool      luby_restart;+    int       ccmin_mode;         // Controls conflict clause minimization (0=none, 1=basic, 2=deep).+    int       phase_saving;       // Controls the level of phase saving (0=none, 1=limited, 2=full).+    bool      rnd_pol;            // Use random polarities for branching heuristics.+    bool      rnd_init_act;       // Initialize variable activities with a small random value.+    double    garbage_frac;       // The fraction of wasted memory allowed before a garbage collection is triggered.+    int       min_learnts_lim;    // Minimum number to set the learnts limit to.++    int       restart_first;      // The initial restart limit.                                                                (default 100)+    double    restart_inc;        // The factor with which the restart limit is multiplied in each restart.                    (default 1.5)+    double    learntsize_factor;  // The intitial limit for learnt clauses is a factor of the original clauses.                (default 1 / 3)+    double    learntsize_inc;     // The limit for learnt clauses is multiplied with this factor each restart.                 (default 1.1)++    int       learntsize_adjust_start_confl;+    double    learntsize_adjust_inc;++    // Statistics: (read-only member variable)+    //+    uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;+    uint64_t dec_vars, num_clauses, num_learnts, clauses_literals, learnts_literals, max_literals, tot_literals;++protected:++    // Helper structures:+    //+    struct VarData { CRef reason; int level; };+    static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }++    struct Watcher {+        CRef cref;+        Lit  blocker;+        Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}+        bool operator==(const Watcher& w) const { return cref == w.cref; }+        bool operator!=(const Watcher& w) const { return cref != w.cref; }+    };++    struct WatcherDeleted+    {+        const ClauseAllocator& ca;+        WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}+        bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }+    };++    struct VarOrderLt {+        const IntMap<Var, double>&  activity;+        bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }+        VarOrderLt(const IntMap<Var, double>&  act) : activity(act) { }+    };++    struct ShrinkStackElem {+        uint32_t i;+        Lit      l;+        ShrinkStackElem(uint32_t _i, Lit _l) : i(_i), l(_l){}+    };++    // Solver state:+    //+    vec<CRef>           clauses;          // List of problem clauses.+    vec<CRef>           learnts;          // List of learnt clauses.+    vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.+    vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail'.+    vec<Lit>            assumptions;      // Current set of assumptions provided to solve by the user.++    VMap<double>        activity;         // A heuristic measurement of the activity of a variable.+    VMap<lbool>         assigns;          // The current assignments.+    VMap<char>          polarity;         // The preferred polarity of each variable.+    VMap<lbool>         user_pol;         // The users preferred polarity of each variable.+    VMap<char>          decision;         // Declares if a variable is eligible for selection in the decision heuristic.+    VMap<VarData>       vardata;          // Stores reason and level for each variable.+    OccLists<Lit, vec<Watcher>, WatcherDeleted, MkIndexLit>+                        watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).++    Heap<Var,VarOrderLt>order_heap;       // A priority queue of variables ordered with respect to the variable activity.++    bool                ok;               // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!+    double              cla_inc;          // Amount to bump next clause with.+    double              var_inc;          // Amount to bump next variable with.+    int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).+    int                 simpDB_assigns;   // Number of top-level assignments since last execution of 'simplify()'.+    int64_t             simpDB_props;     // Remaining number of propagations that must be made before next execution of 'simplify()'.+    double              progress_estimate;// Set by 'search()'.+    bool                remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.+    Var                 next_var;         // Next variable to be created.+    ClauseAllocator     ca;++    vec<Var>            released_vars;+    vec<Var>            free_vars;++    // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is+    // used, exept 'seen' wich is used in several places.+    //+    VMap<char>          seen;+    vec<ShrinkStackElem>analyze_stack;+    vec<Lit>            analyze_toclear;+    vec<Lit>            add_tmp;++    double              max_learnts;+    double              learntsize_adjust_confl;+    int                 learntsize_adjust_cnt;++    // Resource contraints:+    //+    int64_t             conflict_budget;    // -1 means no budget.+    int64_t             propagation_budget; // -1 means no budget.+    bool                asynch_interrupt;++    // Main internal methods:+    //+    void     insertVarOrder   (Var x);                                                 // Insert a variable in the decision order priority queue.+    Lit      pickBranchLit    ();                                                      // Return the next decision variable.+    void     newDecisionLevel ();                                                      // Begins a new decision level.+    void     uncheckedEnqueue (Lit p, CRef from = CRef_Undef);                         // Enqueue a literal. Assumes value of literal is undefined.+    bool     enqueue          (Lit p, CRef from = CRef_Undef);                         // Test if fact 'p' contradicts current state, enqueue otherwise.+    CRef     propagate        ();                                                      // Perform unit propagation. Returns possibly conflicting clause.+    void     cancelUntil      (int level);                                             // Backtrack until a certain level.+    void     analyze          (CRef confl, vec<Lit>& out_learnt, int& out_btlevel);    // (bt = backtrack)+    void     analyzeFinal     (Lit p, LSet& out_conflict);                             // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?+    bool     litRedundant     (Lit p);                                                 // (helper method for 'analyze()')+    lbool    search           (int nof_conflicts);                                     // Search for a given number of conflicts.+    lbool    solve_           ();                                                      // Main solve method (assumptions given in 'assumptions').+    void     reduceDB         ();                                                      // Reduce the set of learnt clauses.+    void     removeSatisfied  (vec<CRef>& cs);                                         // Shrink 'cs' to contain only non-satisfied clauses.+    void     rebuildOrderHeap ();++    // Maintaining Variable/Clause activity:+    //+    void     varDecayActivity ();                      // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.+    void     varBumpActivity  (Var v, double inc);     // Increase a variable with the current 'bump' value.+    void     varBumpActivity  (Var v);                 // Increase a variable with the current 'bump' value.+    void     claDecayActivity ();                      // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.+    void     claBumpActivity  (Clause& c);             // Increase a clause with the current 'bump' value.++    // Operations on clauses:+    //+    void     attachClause     (CRef cr);               // Attach a clause to watcher lists.+    void     detachClause     (CRef cr, bool strict = false); // Detach a clause to watcher lists.+    void     removeClause     (CRef cr);               // Detach and free a clause.+    bool     isRemoved        (CRef cr) const;         // Test if a clause has been removed.+    bool     locked           (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.+    bool     satisfied        (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.++    // Misc:+    //+    int      decisionLevel    ()      const; // Gives the current decisionlevel.+    uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.+    CRef     reason           (Var x) const;+    int      level            (Var x) const;+    double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...+    bool     withinBudget     ()      const;+    void     relocAll         (ClauseAllocator& to);++    // Static helpers:+    //++    // Returns a random float 0 <= x < 1. Seed must never be 0.+    static inline double drand(double& seed) {+        seed *= 1389796;+        int q = (int)(seed / 2147483647);+        seed -= (double)q * 2147483647;+        return seed / 2147483647; }++    // Returns a random integer 0 <= x < size. Seed must never be 0.+    static inline int irand(double& seed, int size) {+        return (int)(drand(seed) * size); }+};+++//=================================================================================================+// Implementation of inline methods:++inline CRef Solver::reason(Var x) const { return vardata[x].reason; }+inline int  Solver::level (Var x) const { return vardata[x].level; }++inline void Solver::insertVarOrder(Var x) {+    if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }++inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }+inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }+inline void Solver::varBumpActivity(Var v, double inc) {+    if ( (activity[v] += inc) > 1e100 ) {+        // Rescale:+        for (int i = 0; i < nVars(); i++)+            activity[i] *= 1e-100;+        var_inc *= 1e-100; }++    // Update order_heap with respect to new activity:+    if (order_heap.inHeap(v))+        order_heap.decrease(v); }++inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }+inline void Solver::claBumpActivity (Clause& c) {+        if ( (c.activity() += cla_inc) > 1e20 ) {+            // Rescale:+            for (int i = 0; i < learnts.size(); i++)+                ca[learnts[i]].activity() *= 1e-20;+            cla_inc *= 1e-20; } }++inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }+inline void Solver::checkGarbage(double gf){+    if (ca.wasted() > ca.size() * gf)+        garbageCollect(); }++// NOTE: enqueue does not set the ok flag! (only public methods do)+inline bool     Solver::enqueue         (Lit p, CRef from)      { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }+inline bool     Solver::addClause       (const vec<Lit>& ps)    { ps.copyTo(add_tmp); return addClause_(add_tmp); }+inline bool     Solver::addEmptyClause  ()                      { add_tmp.clear(); return addClause_(add_tmp); }+inline bool     Solver::addClause       (Lit p)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }+inline bool     Solver::addClause       (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }+inline bool     Solver::addClause       (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }+inline bool     Solver::addClause       (Lit p, Lit q, Lit r, Lit s){ add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); add_tmp.push(s); return addClause_(add_tmp); }++inline bool     Solver::isRemoved       (CRef cr)         const { return ca[cr].mark() == 1; }+inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; }+inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }++inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }+inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }+inline lbool    Solver::value         (Var x) const   { return assigns[x]; }+inline lbool    Solver::value         (Lit p) const   { return assigns[var(p)] ^ sign(p); }+inline lbool    Solver::modelValue    (Var x) const   { return model[x]; }+inline lbool    Solver::modelValue    (Lit p) const   { return model[var(p)] ^ sign(p); }+inline int      Solver::nAssigns      ()      const   { return trail.size(); }+inline int      Solver::nClauses      ()      const   { return num_clauses; }+inline int      Solver::nLearnts      ()      const   { return num_learnts; }+inline int      Solver::nVars         ()      const   { return next_var; }+// TODO: nFreeVars() is not quite correct, try to calculate right instead of adapting it like below:+inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }+inline void     Solver::setPolarity   (Var v, lbool b){ user_pol[v] = b; }+inline void     Solver::setDecisionVar(Var v, bool b) +{ +    if      ( b && !decision[v]) dec_vars++;+    else if (!b &&  decision[v]) dec_vars--;++    decision[v] = b;+    insertVarOrder(v);+}+inline void     Solver::setConfBudget(int64_t x){ conflict_budget    = conflicts    + x; }+inline void     Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }+inline void     Solver::interrupt(){ asynch_interrupt = true; }+inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }+inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }+inline bool     Solver::withinBudget() const {+    return !asynch_interrupt &&+           (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&+           (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }++// FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a+// pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or+// all calls to solve must return an 'lbool'. I'm not yet sure which I prefer.+inline bool     Solver::solve         ()                    { budgetOff(); assumptions.clear(); return solve_() == l_True; }+inline bool     Solver::solve         (Lit p)               { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }+inline bool     Solver::solve         (Lit p, Lit q)        { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }+inline bool     Solver::solve         (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; }+inline bool     Solver::solve         (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }+inline lbool    Solver::solveLimited  (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }+inline bool     Solver::okay          ()      const   { return ok; }++inline ClauseIterator Solver::clausesBegin() const { return ClauseIterator(ca, &clauses[0]); }+inline ClauseIterator Solver::clausesEnd  () const { return ClauseIterator(ca, &clauses[clauses.size()]); }+inline TrailIterator  Solver::trailBegin  () const { return TrailIterator(&trail[0]); }+inline TrailIterator  Solver::trailEnd    () const { +    return TrailIterator(&trail[decisionLevel() == 0 ? trail.size() : trail_lim[0]]); }++inline void     Solver::toDimacs     (const char* file){ vec<Lit> as; toDimacs(file, as); }+inline void     Solver::toDimacs     (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }+inline void     Solver::toDimacs     (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }+inline void     Solver::toDimacs     (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }+++//=================================================================================================+// Debug etc:+++//=================================================================================================+}++#endif
+ minisat/minisat/core/SolverTypes.h view
@@ -0,0 +1,475 @@+/***********************************************************************************[SolverTypes.h]+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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 Minisat_SolverTypes_h+#define Minisat_SolverTypes_h++#include <assert.h>++#include "minisat/mtl/IntTypes.h"+#include "minisat/mtl/Alg.h"+#include "minisat/mtl/Vec.h"+#include "minisat/mtl/IntMap.h"+#include "minisat/mtl/Map.h"+#include "minisat/mtl/Alloc.h"++namespace Minisat {++//=================================================================================================+// Variables, literals, lifted booleans, clauses:+++// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,+// so that they can be used as array indices.++typedef int Var;+#if defined(MINISAT_CONSTANTS_AS_MACROS)+#define var_Undef (-1)+#else+  const Var var_Undef = -1;+#endif+++struct Lit {+    int     x;++    bool operator == (Lit p) const { return x == p.x; }+    bool operator != (Lit p) const { return x != p.x; }+    bool operator <  (Lit p) const { return x < p.x;  } // '<' makes p, ~p adjacent in the ordering.+};+++inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }+inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }+inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }+inline  bool sign      (Lit p)              { return p.x & 1; }+inline  int  var       (Lit p)              { return p.x >> 1; }++// Mapping Literals to and from compact integers suitable for array indexing:+inline  int  toInt     (Var v)              { return v; } +inline  int  toInt     (Lit p)              { return p.x; } +inline  Lit  toLit     (int i)              { Lit p; p.x = i; return p; } ++//const Lit lit_Undef = mkLit(var_Undef, false);  // }- Useful special constants.+//const Lit lit_Error = mkLit(var_Undef, true );  // }++const Lit lit_Undef = { -2 };  // }- Useful special constants.+const Lit lit_Error = { -1 };  // }++struct MkIndexLit { vec<Lit>::Size operator()(Lit l) const { return vec<Lit>::Size(l.x); } };++template<class T> class VMap : public IntMap<Var, T>{};+template<class T> class LMap : public IntMap<Lit, T, MkIndexLit>{};+class LSet : public IntSet<Lit, MkIndexLit>{};++//=================================================================================================+// Lifted booleans:+//+// NOTE: this implementation is optimized for the case when comparisons between values are mostly+//       between one variable and one constant. Some care had to be taken to make sure that gcc +//       does enough constant propagation to produce sensible code, and this appears to be somewhat+//       fragile unfortunately.++class lbool {+    uint8_t value;++public:+    explicit lbool(uint8_t v) : value(v) { }++    lbool()       : value(0) { }+    explicit lbool(bool x) : value(!x) { }++    bool  operator == (lbool b) const { return ((b.value&2) & (value&2)) | (!(b.value&2)&(value == b.value)); }+    bool  operator != (lbool b) const { return !(*this == b); }+    lbool operator ^  (bool  b) const { return lbool((uint8_t)(value^(uint8_t)b)); }++    lbool operator && (lbool b) const { +        uint8_t sel = (this->value << 1) | (b.value << 3);+        uint8_t v   = (0xF7F755F4 >> sel) & 3;+        return lbool(v); }++    lbool operator || (lbool b) const {+        uint8_t sel = (this->value << 1) | (b.value << 3);+        uint8_t v   = (0xFCFCF400 >> sel) & 3;+        return lbool(v); }++    friend int   toInt  (lbool l);+    friend lbool toLbool(int   v);+};+inline int   toInt  (lbool l) { return l.value; }+inline lbool toLbool(int   v) { return lbool((uint8_t)v);  }++#if defined(MINISAT_CONSTANTS_AS_MACROS)+  #define l_True  (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.+  #define l_False (lbool((uint8_t)1))+  #define l_Undef (lbool((uint8_t)2))+#else+  const lbool l_True ((uint8_t)0);+  const lbool l_False((uint8_t)1);+  const lbool l_Undef((uint8_t)2);+#endif+++//=================================================================================================+// Clause -- a simple class for representing a clause:++class Clause;+typedef RegionAllocator<uint32_t>::Ref CRef;++class Clause {+    struct {+        unsigned mark      : 2;+        unsigned learnt    : 1;+        unsigned has_extra : 1;+        unsigned reloced   : 1;+        unsigned size      : 27; }                        header;+    union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];++    friend class ClauseAllocator;++    // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).+    Clause(const vec<Lit>& ps, bool use_extra, bool learnt) {+        header.mark      = 0;+        header.learnt    = learnt;+        header.has_extra = use_extra;+        header.reloced   = 0;+        header.size      = ps.size();++        for (int i = 0; i < ps.size(); i++) +            data[i].lit = ps[i];++        if (header.has_extra){+            if (header.learnt)+                data[header.size].act = 0;+            else+                calcAbstraction();+    }+    }++    // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).+    Clause(const Clause& from, bool use_extra){+        header           = from.header;+        header.has_extra = use_extra;   // NOTE: the copied clause may lose the extra field.++        for (int i = 0; i < from.size(); i++)+            data[i].lit = from[i];++        if (header.has_extra){+            if (header.learnt)+                data[header.size].act = from.data[header.size].act;+            else +                data[header.size].abs = from.data[header.size].abs;+    }+    }++public:+    void calcAbstraction() {+        assert(header.has_extra);+        uint32_t abstraction = 0;+        for (int i = 0; i < size(); i++)+            abstraction |= 1 << (var(data[i].lit) & 31);+        data[header.size].abs = abstraction;  }+++    int          size        ()      const   { return header.size; }+    void         shrink      (int i)         { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }+    void         pop         ()              { shrink(1); }+    bool         learnt      ()      const   { return header.learnt; }+    bool         has_extra   ()      const   { return header.has_extra; }+    uint32_t     mark        ()      const   { return header.mark; }+    void         mark        (uint32_t m)    { header.mark = m; }+    const Lit&   last        ()      const   { return data[header.size-1].lit; }++    bool         reloced     ()      const   { return header.reloced; }+    CRef         relocation  ()      const   { return data[0].rel; }+    void         relocate    (CRef c)        { header.reloced = 1; data[0].rel = c; }++    // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for+    //       subsumption operations to behave correctly.+    Lit&         operator [] (int i)         { return data[i].lit; }+    Lit          operator [] (int i) const   { return data[i].lit; }+    operator const Lit* (void) const         { return (Lit*)data; }++    float&       activity    ()              { assert(header.has_extra); return data[header.size].act; }+    uint32_t     abstraction () const        { assert(header.has_extra); return data[header.size].abs; }++    Lit          subsumes    (const Clause& other) const;+    void         strengthen  (Lit p);+};+++//=================================================================================================+// ClauseAllocator -- a simple class for allocating memory for clauses:++const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef;+class ClauseAllocator+{+    RegionAllocator<uint32_t> ra;++    static uint32_t clauseWord32Size(int size, bool has_extra){+        return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); }++ public:+    enum { Unit_Size = RegionAllocator<uint32_t>::Unit_Size };++    bool extra_clause_field;++    ClauseAllocator(uint32_t start_cap) : ra(start_cap), extra_clause_field(false){}+    ClauseAllocator() : extra_clause_field(false){}++    void moveTo(ClauseAllocator& to){+        to.extra_clause_field = extra_clause_field;+        ra.moveTo(to.ra); }++    CRef alloc(const vec<Lit>& ps, bool learnt = false)+    {+        assert(sizeof(Lit)      == sizeof(uint32_t));+        assert(sizeof(float)    == sizeof(uint32_t));+        bool use_extra = learnt | extra_clause_field;+        CRef cid       = ra.alloc(clauseWord32Size(ps.size(), use_extra));+        new (lea(cid)) Clause(ps, use_extra, learnt);++        return cid;+    }++    CRef alloc(const Clause& from)+    {+        bool use_extra = from.learnt() | extra_clause_field;+        CRef cid       = ra.alloc(clauseWord32Size(from.size(), use_extra));+        new (lea(cid)) Clause(from, use_extra);+        return cid; }++    uint32_t size      () const      { return ra.size(); }+    uint32_t wasted    () const      { return ra.wasted(); }++    // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):+    Clause&       operator[](CRef r)         { return (Clause&)ra[r]; }+    const Clause& operator[](CRef r) const   { return (Clause&)ra[r]; }+    Clause*       lea       (CRef r)         { return (Clause*)ra.lea(r); }+    const Clause* lea       (CRef r) const   { return (Clause*)ra.lea(r);; }+    CRef          ael       (const Clause* t){ return ra.ael((uint32_t*)t); }++    void free(CRef cid)+    {+        Clause& c = operator[](cid);+        ra.free(clauseWord32Size(c.size(), c.has_extra()));+    }++    void reloc(CRef& cr, ClauseAllocator& to)+    {+        Clause& c = operator[](cr);+        +        if (c.reloced()) { cr = c.relocation(); return; }+        +        cr = to.alloc(c);+        c.relocate(cr);+    }+};++//=================================================================================================+// Simple iterator classes (for iterating over clauses and top-level assignments):++class ClauseIterator {+    const ClauseAllocator& ca;+    const CRef*            crefs;+public:+    ClauseIterator(const ClauseAllocator& _ca, const CRef* _crefs) : ca(_ca), crefs(_crefs){}++    void operator++(){ crefs++; }+    const Clause& operator*() const { return ca[*crefs]; }++    // NOTE: does not compare that references use the same clause-allocator:+    bool operator==(const ClauseIterator& ci) const { return crefs == ci.crefs; }+    bool operator!=(const ClauseIterator& ci) const { return crefs != ci.crefs; }+};+++class TrailIterator {+    const Lit* lits;+public:+    TrailIterator(const Lit* _lits) : lits(_lits){}++    void operator++()   { lits++; }+    Lit  operator*() const { return *lits; }++    bool operator==(const TrailIterator& ti) const { return lits == ti.lits; }+    bool operator!=(const TrailIterator& ti) const { return lits != ti.lits; }+};+++//=================================================================================================+// OccLists -- a class for maintaining occurence lists with lazy deletion:++template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K> >+class OccLists+{+    IntMap<K, Vec,  MkIndex> occs;+    IntMap<K, char, MkIndex> dirty;+    vec<K>                   dirties;+    Deleted                  deleted;++ public:+    OccLists(const Deleted& d, MkIndex _index = MkIndex()) :+        occs(_index), +        dirty(_index), +        deleted(d){}+    +    void  init      (const K& idx){ occs.reserve(idx); occs[idx].clear(); dirty.reserve(idx, 0); }+    Vec&  operator[](const K& idx){ return occs[idx]; }+    Vec&  lookup    (const K& idx){ if (dirty[idx]) clean(idx); return occs[idx]; }++    void  cleanAll  ();+    void  clean     (const K& idx);+    void  smudge    (const K& idx){+        if (dirty[idx] == 0){+            dirty[idx] = 1;+            dirties.push(idx);+        }+    }++    void  clear(bool free = true){+        occs   .clear(free);+        dirty  .clear(free);+        dirties.clear(free);+    }+};+++template<class K, class Vec, class Deleted, class MkIndex>+void OccLists<K,Vec,Deleted,MkIndex>::cleanAll()+{+    for (int i = 0; i < dirties.size(); i++)+        // Dirties may contain duplicates so check here if a variable is already cleaned:+        if (dirty[dirties[i]])+            clean(dirties[i]);+    dirties.clear();+}+++template<class K, class Vec, class Deleted, class MkIndex>+void OccLists<K,Vec,Deleted,MkIndex>::clean(const K& idx)+{+    Vec& vec = occs[idx];+    int  i, j;+    for (i = j = 0; i < vec.size(); i++)+        if (!deleted(vec[i]))+            vec[j++] = vec[i];+    vec.shrink(i - j);+    dirty[idx] = 0;+}+++//=================================================================================================+// CMap -- a class for mapping clauses to values:+++template<class T>+class CMap+{+    struct CRefHash {+        uint32_t operator()(CRef cr) const { return (uint32_t)cr; } };++    typedef Map<CRef, T, CRefHash> HashTable;+    HashTable map;+        + public:+    // Size-operations:+    void     clear       ()                           { map.clear(); }+    int      size        ()                const      { return map.elems(); }++    +    // Insert/Remove/Test mapping:+    void     insert      (CRef cr, const T& t){ map.insert(cr, t); }+    void     growTo      (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility+    void     remove      (CRef cr)            { map.remove(cr); }+    bool     has         (CRef cr, T& t)      { return map.peek(cr, t); }++    // Vector interface (the clause 'c' must already exist):+    const T& operator [] (CRef cr) const      { return map[cr]; }+    T&       operator [] (CRef cr)            { return map[cr]; }++    // Iteration (not transparent at all at the moment):+    int  bucket_count() const { return map.bucket_count(); }+    const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); }++    // Move contents to other map:+    void moveTo(CMap& other){ map.moveTo(other.map); }++    // TMP debug:+    void debug(){+        printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }+};+++/*_________________________________________________________________________________________________+|+|  subsumes : (other : const Clause&)  ->  Lit+|  +|  Description:+|       Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'+|       by subsumption resolution.+|  +|    Result:+|       lit_Error  - No subsumption or simplification+|       lit_Undef  - Clause subsumes 'other'+|       p          - The literal p can be deleted from 'other'+|________________________________________________________________________________________________@*/+inline Lit Clause::subsumes(const Clause& other) const+{+    //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)+    //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))+    assert(!header.learnt);   assert(!other.header.learnt);+    assert(header.has_extra); assert(other.header.has_extra);+    if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)+        return lit_Error;++    Lit        ret = lit_Undef;+    const Lit* c   = (const Lit*)(*this);+    const Lit* d   = (const Lit*)other;++    for (unsigned i = 0; i < header.size; i++) {+        // search for c[i] or ~c[i]+        for (unsigned j = 0; j < other.header.size; j++)+            if (c[i] == d[j])+                goto ok;+            else if (ret == lit_Undef && c[i] == ~d[j]){+                ret = c[i];+                goto ok;+            }++        // did not find it+        return lit_Error;+    ok:;+    }++    return ret;+}++inline void Clause::strengthen(Lit p)+{+    remove(*this, p);+    calcAbstraction();+}++//=================================================================================================+}++#endif
+ minisat/minisat/mtl/Alg.h view
@@ -0,0 +1,84 @@+/*******************************************************************************************[Alg.h]+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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 Minisat_Alg_h+#define Minisat_Alg_h++#include "minisat/mtl/Vec.h"++namespace Minisat {++//=================================================================================================+// Useful functions on vector-like types:++//=================================================================================================+// Removing and searching for elements:+//++template<class V, class T>+static inline void remove(V& ts, const T& t)+{+    int j = 0;+    for (; j < (int)ts.size() && ts[j] != t; j++);+    assert(j < (int)ts.size());+    for (; j < (int)ts.size()-1; j++) ts[j] = ts[j+1];+    ts.pop();+}+++template<class V, class T>+static inline bool find(V& ts, const T& t)+{+    int j = 0;+    for (; j < (int)ts.size() && ts[j] != t; j++);+    return j < (int)ts.size();+}+++//=================================================================================================+// Copying vectors with support for nested vector types:+//++// Base case:+template<class T>+static inline void copy(const T& from, T& to)+{+    to = from;+}++// Recursive case:+template<class T>+static inline void copy(const vec<T>& from, vec<T>& to, bool append = false)+{+    if (!append)+        to.clear();+    for (int i = 0; i < from.size(); i++){+        to.push();+        copy(from[i], to.last());+    }+}++template<class T>+static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); }++//=================================================================================================+}++#endif
+ minisat/minisat/mtl/Alloc.h view
@@ -0,0 +1,131 @@+/*****************************************************************************************[Alloc.h]+Copyright (c) 2008-2010, 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 Minisat_Alloc_h+#define Minisat_Alloc_h++#include "minisat/mtl/XAlloc.h"+#include "minisat/mtl/Vec.h"++namespace Minisat {++//=================================================================================================+// Simple Region-based memory allocator:++template<class T>+class RegionAllocator+{+    T*        memory;+    uint32_t  sz;+    uint32_t  cap;+    uint32_t  wasted_;++    void capacity(uint32_t min_cap);++ public:+    // TODO: make this a class for better type-checking?+    typedef uint32_t Ref;+    enum { Ref_Undef = UINT32_MAX };+    enum { Unit_Size = sizeof(T) };++    explicit RegionAllocator(uint32_t start_cap = 1024*1024) : memory(NULL), sz(0), cap(0), wasted_(0){ capacity(start_cap); }+    ~RegionAllocator()+    {+        if (memory != NULL)+            ::free(memory);+    }+++    uint32_t size      () const      { return sz; }+    uint32_t wasted    () const      { return wasted_; }++    Ref      alloc     (int size); +    void     free      (int size)    { wasted_ += size; }++    // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):+    T&       operator[](Ref r)       { assert(r < sz); return memory[r]; }+    const T& operator[](Ref r) const { assert(r < sz); return memory[r]; }++    T*       lea       (Ref r)       { assert(r < sz); return &memory[r]; }+    const T* lea       (Ref r) const { assert(r < sz); return &memory[r]; }+    Ref      ael       (const T* t)  { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);+        return  (Ref)(t - &memory[0]); }++    void     moveTo(RegionAllocator& to) {+        if (to.memory != NULL) ::free(to.memory);+        to.memory = memory;+        to.sz = sz;+        to.cap = cap;+        to.wasted_ = wasted_;++        memory = NULL;+        sz = cap = wasted_ = 0;+    }+++};++template<class T>+void RegionAllocator<T>::capacity(uint32_t min_cap)+{+    if (cap >= min_cap) return;++    uint32_t prev_cap = cap;+    while (cap < min_cap){+        // NOTE: Multiply by a factor (13/8) without causing overflow, then add 2 and make the+        // result even by clearing the least significant bit. The resulting sequence of capacities+        // is carefully chosen to hit a maximum capacity that is close to the '2^32-1' limit when+        // using 'uint32_t' as indices so that as much as possible of this space can be used.+        uint32_t delta = ((cap >> 1) + (cap >> 3) + 2) & ~1;+        cap += delta;++        if (cap <= prev_cap)+            throw OutOfMemoryException();+    }+    // printf(" .. (%p) cap = %u\n", this, cap);++    assert(cap > 0);+    memory = (T*)xrealloc(memory, sizeof(T)*cap);+}+++template<class T>+typename RegionAllocator<T>::Ref+RegionAllocator<T>::alloc(int size)+{ +    // printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout);+    assert(size > 0);+    capacity(sz + size);++    uint32_t prev_sz = sz;+    sz += size;+    +    // Handle overflow:+    if (sz < prev_sz)+        throw OutOfMemoryException();++    return prev_sz;+}+++//=================================================================================================+}++#endif
+ minisat/minisat/mtl/Heap.h view
@@ -0,0 +1,168 @@+/******************************************************************************************[Heap.h]+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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 Minisat_Heap_h+#define Minisat_Heap_h++#include "minisat/mtl/Vec.h"+#include "minisat/mtl/IntMap.h"++namespace Minisat {++//=================================================================================================+// A heap implementation with support for decrease/increase key.+++template<class K, class Comp, class MkIndex = MkIndexDefault<K> >+class Heap {+    vec<K>                heap;     // Heap of Keys+    IntMap<K,int,MkIndex> indices;  // Each Key's position (index) in the Heap+    Comp                  lt;       // The heap is a minimum-heap with respect to this comparator++    // Index "traversal" functions+    static inline int left  (int i) { return i*2+1; }+    static inline int right (int i) { return (i+1)*2; }+    static inline int parent(int i) { return (i-1) >> 1; }+++    void percolateUp(int i)+    {+        K   x  = heap[i];+        int p  = parent(i);+        +        while (i != 0 && lt(x, heap[p])){+            heap[i]          = heap[p];+            indices[heap[p]] = i;+            i                = p;+            p                = parent(p);+        }+        heap   [i] = x;+        indices[x] = i;+    }+++    void percolateDown(int i)+    {+        K x = heap[i];+        while (left(i) < heap.size()){+            int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);+            if (!lt(heap[child], x)) break;+            heap[i]          = heap[child];+            indices[heap[i]] = i;+            i                = child;+        }+        heap   [i] = x;+        indices[x] = i;+    }+++  public:+    Heap(const Comp& c, MkIndex _index = MkIndex()) : indices(_index), lt(c) {}++    int  size      ()          const { return heap.size(); }+    bool empty     ()          const { return heap.size() == 0; }+    bool inHeap    (K k)       const { return indices.has(k) && indices[k] >= 0; }+    int  operator[](int index) const { assert(index < heap.size()); return heap[index]; }++    void decrease  (K k) { assert(inHeap(k)); percolateUp  (indices[k]); }+    void increase  (K k) { assert(inHeap(k)); percolateDown(indices[k]); }+++    // Safe variant of insert/decrease/increase:+    void update(K k)+    {+        if (!inHeap(k))+            insert(k);+        else {+            percolateUp(indices[k]);+            percolateDown(indices[k]); }+    }+++    void insert(K k)+    {+        indices.reserve(k, -1);+        assert(!inHeap(k));++        indices[k] = heap.size();+        heap.push(k);+        percolateUp(indices[k]);+    }+++    void remove(K k)+    {+        assert(inHeap(k));++        int k_pos  = indices[k];+        indices[k] = -1;++        if (k_pos < heap.size()-1){+            heap[k_pos]          = heap.last();+            indices[heap[k_pos]] = k_pos;+            heap.pop();+            percolateDown(k_pos);+        }else+            heap.pop();+    }+++    K removeMin()+    {+        K x              = heap[0];+        heap[0]          = heap.last();+        indices[heap[0]] = 0;+        indices[x]       = -1;+        heap.pop();+        if (heap.size() > 1) percolateDown(0);+        return x; +    }+++    // Rebuild the heap from scratch, using the elements in 'ns':+    void build(const vec<K>& ns) {+        for (int i = 0; i < heap.size(); i++)+            indices[heap[i]] = -1;+        heap.clear();++        for (int i = 0; i < ns.size(); i++){+            // TODO: this should probably call reserve instead of relying on it being reserved already.+            assert(indices.has(ns[i]));+            indices[ns[i]] = i;+            heap.push(ns[i]); }++        for (int i = heap.size() / 2 - 1; i >= 0; i--)+            percolateDown(i);+    }++    void clear(bool dispose = false) +    { +        // TODO: shouldn't the 'indices' map also be dispose-cleared?+        for (int i = 0; i < heap.size(); i++)+            indices[heap[i]] = -1;+        heap.clear(dispose); +    }+};+++//=================================================================================================+}++#endif
+ minisat/minisat/mtl/IntMap.h view
@@ -0,0 +1,106 @@+/****************************************************************************************[IntMap.h]+Copyright (c) 2011, 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 Minisat_IntMap_h+#define Minisat_IntMap_h++#include "minisat/mtl/Vec.h"++namespace Minisat {++    template<class T> struct MkIndexDefault {+        typename vec<T>::Size operator()(T t) const { return (typename vec<T>::Size)t; }+    };+    +    template<class K, class V, class MkIndex = MkIndexDefault<K> >+    class IntMap {+        vec<V>   map;+        MkIndex  index;+    public:+        explicit IntMap(MkIndex _index = MkIndex()) : index(_index){}+        +        bool     has       (K k) const { return index(k) < map.size(); }++        const V& operator[](K k) const { assert(has(k)); return map[index(k)]; }+        V&       operator[](K k)       { assert(has(k)); return map[index(k)]; }++        const V* begin  () const { return &map[0]; }+        const V* end    () const { return &map[map.size()]; }+        V*       begin  ()       { return &map[0]; }+        V*       end    ()       { return &map[map.size()]; }++        void     reserve(K key, V pad)       { map.growTo(index(key)+1, pad); }+        void     reserve(K key)              { map.growTo(index(key)+1); }+        void     insert (K key, V val, V pad){ reserve(key, pad); operator[](key) = val; }+        void     insert (K key, V val)       { reserve(key); operator[](key) = val; }++        void     clear  (bool dispose = false) { map.clear(dispose); }+        void     moveTo (IntMap& to)           { map.moveTo(to.map); to.index = index; }+        void     copyTo (IntMap& to) const     { map.copyTo(to.map); to.index = index; }+    };+++    template<class K, class MkIndex = MkIndexDefault<K> >+    class IntSet+    {+        IntMap<K, char, MkIndex> in_set;+        vec<K>                   xs;+        +    public:+        // Size operations:+        int      size        (void)      const  { return xs.size(); }+        void     clear       (bool free = false){+            if (free)+                in_set.clear(true); +            else+                for (int i = 0; i < xs.size(); i++)+                    in_set[xs[i]] = 0;+            xs.clear(free);+        }++        // Allow inspecting the internal vector:+        const vec<K>&+                 toVec       ()          const  { return xs; }+        +        // Vector interface:+        K        operator [] (int index) const  { return xs[index]; }+        +        +        void     insert      (K k) { in_set.reserve(k, 0); if (!in_set[k]) { in_set[k] = 1; xs.push(k); } }+        bool     has         (K k) { in_set.reserve(k, 0); return in_set[k]; }+    };++    #if 0+    template<class K, class V, V nil, class MkIndex = MkIndexDefault<K> >+    class IntMapNil {+        vec<V> map;+        V      nil;++    public:+        IntMap(){}+        +        void     reserve(K);+        V&       find   (K);+        const V& operator[](K k) const;++    };+    #endif++//=================================================================================================+} // namespace Minisat+#endif
+ minisat/minisat/mtl/IntTypes.h view
@@ -0,0 +1,42 @@+/**************************************************************************************[IntTypes.h]+Copyright (c) 2009-2010, 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 Minisat_IntTypes_h+#define Minisat_IntTypes_h++#ifdef __sun+    // Not sure if there are newer versions that support C99 headers. The+    // needed features are implemented in the headers below though:++#   include <sys/int_types.h>+#   include <sys/int_fmtio.h>+#   include <sys/int_limits.h>++#else++#   include <stdint.h>+#   include <inttypes.h>++#endif++#include <limits.h>++//=================================================================================================++#endif
+ minisat/minisat/mtl/Map.h view
@@ -0,0 +1,193 @@+/*******************************************************************************************[Map.h]+Copyright (c) 2006-2010, 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 Minisat_Map_h+#define Minisat_Map_h++#include "minisat/mtl/IntTypes.h"+#include "minisat/mtl/Vec.h"++namespace Minisat {++//=================================================================================================+// Default hash/equals functions+//++template<class K> struct Hash  { uint32_t operator()(const K& k)               const { return hash(k);  } };+template<class K> struct Equal { bool     operator()(const K& k1, const K& k2) const { return k1 == k2; } };++template<class K> struct DeepHash  { uint32_t operator()(const K* k)               const { return hash(*k);  } };+template<class K> struct DeepEqual { bool     operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };++static inline uint32_t hash(uint32_t x){ return x; }+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }+++//=================================================================================================+// Some primes+//++static const int nprimes          = 25;+static const int primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 };++//=================================================================================================+// Hash table implementation of Maps+//++template<class K, class D, class H = Hash<K>, class E = Equal<K> >+class Map {+ public:+    struct Pair { K key; D data; };++ private:+    H          hash;+    E          equals;++    vec<Pair>* table;+    int        cap;+    int        size;++    // Don't allow copying (error prone):+    Map<K,D,H,E>&  operator = (Map<K,D,H,E>& other);+                   Map        (Map<K,D,H,E>& other);++    bool    checkCap(int new_size) const { return new_size > cap; }++    int32_t index  (const K& k) const { return hash(k) % cap; }+    void   _insert (const K& k, const D& d) { +        vec<Pair>& ps = table[index(k)];+        ps.push(); ps.last().key = k; ps.last().data = d; }++    void    rehash () {+        const vec<Pair>* old = table;++        int old_cap = cap;+        int newsize = primes[0];+        for (int i = 1; newsize <= cap && i < nprimes; i++)+           newsize = primes[i];++        table = new vec<Pair>[newsize];+        cap   = newsize;++        for (int i = 0; i < old_cap; i++){+            for (int j = 0; j < old[i].size(); j++){+                _insert(old[i][j].key, old[i][j].data); }}++        delete [] old;++        // printf(" --- rehashing, old-cap=%d, new-cap=%d\n", cap, newsize);+    }++    + public:++    Map () : table(NULL), cap(0), size(0) {}+    Map (const H& h, const E& e) : hash(h), equals(e), table(NULL), cap(0), size(0){}+    ~Map () { delete [] table; }++    // PRECONDITION: the key must already exist in the map.+    const D& operator [] (const K& k) const+    {+        assert(size != 0);+        const D*         res = NULL;+        const vec<Pair>& ps  = table[index(k)];+        for (int i = 0; i < ps.size(); i++)+            if (equals(ps[i].key, k))+                res = &ps[i].data;+        assert(res != NULL);+        return *res;+    }++    // PRECONDITION: the key must already exist in the map.+    D& operator [] (const K& k)+    {+        assert(size != 0);+        D*         res = NULL;+        vec<Pair>& ps  = table[index(k)];+        for (int i = 0; i < ps.size(); i++)+            if (equals(ps[i].key, k))+                res = &ps[i].data;+        assert(res != NULL);+        return *res;+    }++    // PRECONDITION: the key must *NOT* exist in the map.+    void insert (const K& k, const D& d) { if (checkCap(size+1)) rehash(); _insert(k, d); size++; }+    bool peek   (const K& k, D& d) const {+        if (size == 0) return false;+        const vec<Pair>& ps = table[index(k)];+        for (int i = 0; i < ps.size(); i++)+            if (equals(ps[i].key, k)){+                d = ps[i].data;+                return true; } +        return false;+    }++    bool has   (const K& k) const {+        if (size == 0) return false;+        const vec<Pair>& ps = table[index(k)];+        for (int i = 0; i < ps.size(); i++)+            if (equals(ps[i].key, k))+                return true;+        return false;+    }++    // PRECONDITION: the key must exist in the map.+    void remove(const K& k) {+        assert(table != NULL);+        vec<Pair>& ps = table[index(k)];+        int j = 0;+        for (; j < ps.size() && !equals(ps[j].key, k); j++);+        assert(j < ps.size());+        ps[j] = ps.last();+        ps.pop();+        size--;+    }++    void clear  () {+        cap = size = 0;+        delete [] table;+        table = NULL;+    }++    int  elems() const { return size; }+    int  bucket_count() const { return cap; }++    // NOTE: the hash and equality objects are not moved by this method:+    void moveTo(Map& other){+        delete [] other.table;++        other.table = table;+        other.cap   = cap;+        other.size  = size;++        table = NULL;+        size = cap = 0;+    }++    // NOTE: given a bit more time, I could make a more C++-style iterator out of this:+    const vec<Pair>& bucket(int i) const { return table[i]; }+};++//=================================================================================================+}++#endif
+ minisat/minisat/mtl/Queue.h view
@@ -0,0 +1,69 @@+/*****************************************************************************************[Queue.h]+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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 Minisat_Queue_h+#define Minisat_Queue_h++#include "minisat/mtl/Vec.h"++namespace Minisat {++//=================================================================================================++template<class T>+class Queue {+    vec<T>  buf;+    int     first;+    int     end;++public:+    typedef T Key;++    Queue() : buf(1), first(0), end(0) {}++    void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; }+    int  size  () const { return (end >= first) ? end - first : end - first + buf.size(); }++    const T& operator [] (int index) const  { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }+    T&       operator [] (int index)        { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }++    T    peek  () const { assert(first != end); return buf[first]; }+    void pop   () { assert(first != end); first++; if (first == buf.size()) first = 0; }+    void insert(T elem) {   // INVARIANT: buf[end] is always unused+        buf[end++] = elem;+        if (end == buf.size()) end = 0;+        if (first == end){  // Resize:+            vec<T>  tmp((buf.size()*3 + 1) >> 1);+            //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0);+            int     i = 0;+            for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j];+            for (int j = 0    ; j < end       ; j++) tmp[i++] = buf[j];+            first = 0;+            end   = buf.size();+            tmp.moveTo(buf);+        }+    }+};+++//=================================================================================================+}++#endif
+ minisat/minisat/mtl/Rnd.h view
@@ -0,0 +1,67 @@+/*******************************************************************************************[Rnd.h]+Copyright (c) 2012, 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 Minisat_Rnd_h+#define Minisat_Rnd_h++#include "minisat/mtl/Vec.h"++namespace Minisat {++// Generate a random double:+static inline double drand(double& seed)+{+    seed *= 1389796;+    int q = (int)(seed / 2147483647);+    seed -= (double)q * 2147483647;+    return seed / 2147483647;+}+++// Generate a random integer:+static inline int irand(double& seed, int size) { return (int)(drand(seed) * size); }+++// Randomly shuffle the contents of a vector:+template<class T>+static void randomShuffle(double& seed, vec<T>& xs)+{+    for (int i = 0; i < xs.size(); i++){+        int pick = i + irand(seed, xs.size() - i);+        T tmp = xs[i];+        xs[i] = xs[pick];+        xs[pick] = tmp;+    }+}++// Randomly shuffle a vector of a vector (ugly)+template<class T>+static void randomShuffle(double& seed, vec<vec<T> >& xs)+{+    for (int i = 0; i < xs.size(); i++){+        int pick = i + irand(seed, xs.size() - i);+        vec<T> tmp; xs[i].moveTo(tmp);+        xs[pick].moveTo(xs[i]);+        tmp.moveTo(xs[pick]);+    }+}+++//=================================================================================================+} // namespace Minisat+#endif
+ minisat/minisat/mtl/Sort.h view
@@ -0,0 +1,98 @@+/******************************************************************************************[Sort.h]+Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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 Minisat_Sort_h+#define Minisat_Sort_h++#include "minisat/mtl/Vec.h"++//=================================================================================================+// Some sorting algorithms for vec's+++namespace Minisat {++template<class T>+struct LessThan_default {+    bool operator () (T x, T y) { return x < y; }+};+++template <class T, class LessThan>+void selectionSort(T* array, int size, LessThan lt)+{+    int     i, j, best_i;+    T       tmp;++    for (i = 0; i < size-1; i++){+        best_i = i;+        for (j = i+1; j < size; j++){+            if (lt(array[j], array[best_i]))+                best_i = j;+        }+        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;+    }+}+template <class T> static inline void selectionSort(T* array, int size) {+    selectionSort(array, size, LessThan_default<T>()); }++template <class T, class LessThan>+void sort(T* array, int size, LessThan lt)+{+    if (size <= 15)+        selectionSort(array, size, lt);++    else{+        T           pivot = array[size / 2];+        T           tmp;+        int         i = -1;+        int         j = size;++        for(;;){+            do i++; while(lt(array[i], pivot));+            do j--; while(lt(pivot, array[j]));++            if (i >= j) break;++            tmp = array[i]; array[i] = array[j]; array[j] = tmp;+        }++        sort(array    , i     , lt);+        sort(&array[i], size-i, lt);+    }+}+template <class T> static inline void sort(T* array, int size) {+    sort(array, size, LessThan_default<T>()); }+++//=================================================================================================+// For 'vec's:+++template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) {+    sort((T*)v, v.size(), lt); }+template <class T> void sort(vec<T>& v) {+    sort(v, LessThan_default<T>()); }+++//=================================================================================================+}++#endif
+ minisat/minisat/mtl/Vec.h view
@@ -0,0 +1,134 @@+/*******************************************************************************************[Vec.h]+Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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 Minisat_Vec_h+#define Minisat_Vec_h++#include <assert.h>+#include <limits>+#include <new>++#include "minisat/mtl/IntTypes.h"+#include "minisat/mtl/XAlloc.h"++namespace Minisat {++//=================================================================================================+// Automatically resizable arrays+//+// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)++template<class T, class _Size = int>+class vec {+public:+    typedef _Size Size;+private:+    T*   data;+    Size sz;+    Size cap;++    // Don't allow copying (error prone):+    vec<T>&  operator=(vec<T>& other);+             vec      (vec<T>& other);++    static inline Size max(Size x, Size y){ return (x > y) ? x : y; }++public:+    // Constructors:+    vec()                        : data(NULL), sz(0), cap(0)    { }+    explicit vec(Size size)      : data(NULL), sz(0), cap(0)    { growTo(size); }+    vec(Size size, const T& pad) : data(NULL), sz(0), cap(0)    { growTo(size, pad); }+   ~vec()                                                       { clear(true); }++    // Pointer to first element:+    operator T*       (void)           { return data; }++    // Size operations:+    Size     size     (void) const   { return sz; }+    void     shrink   (Size nelems)  { assert(nelems <= sz); for (Size i = 0; i < nelems; i++) sz--, data[sz].~T(); }+    void     shrink_  (Size nelems)  { assert(nelems <= sz); sz -= nelems; }+    int      capacity (void) const   { return cap; }+    void     capacity (Size min_cap);+    void     growTo   (Size size);+    void     growTo   (Size size, const T& pad);+    void     clear    (bool dealloc = false);++    // Stack interface:+    void     push  (void)              { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }+    //void     push  (const T& elem)     { if (sz == cap) capacity(sz+1); data[sz++] = elem; }+    void     push  (const T& elem)     { if (sz == cap) capacity(sz+1); new (&data[sz++]) T(elem); }+    void     push_ (const T& elem)     { assert(sz < cap); data[sz++] = elem; }+    void     pop   (void)              { assert(sz > 0); sz--, data[sz].~T(); }+    // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but+    // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not+    // happen given the way capacities are calculated (below). Essentially, all capacities are+    // even, but INT_MAX is odd.++    const T& last  (void) const        { return data[sz-1]; }+    T&       last  (void)              { return data[sz-1]; }++    // Vector interface:+    const T& operator [] (Size index) const { return data[index]; }+    T&       operator [] (Size index)       { return data[index]; }++    // Duplicatation (preferred instead):+    void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (Size i = 0; i < sz; i++) copy[i] = data[i]; }+    void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }+};+++template<class T, class _Size>+void vec<T,_Size>::capacity(Size min_cap) {+    if (cap >= min_cap) return;+    Size add = max((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1);   // NOTE: grow by approximately 3/2+    const Size size_max = std::numeric_limits<Size>::max();+    if ( ((size_max <= std::numeric_limits<int>::max()) && (add > size_max - cap))+    ||   (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) )+        throw OutOfMemoryException();+ }+++template<class T, class _Size>+void vec<T,_Size>::growTo(Size size, const T& pad) {+    if (sz >= size) return;+    capacity(size);+    for (Size i = sz; i < size; i++) data[i] = pad;+    sz = size; }+++template<class T, class _Size>+void vec<T,_Size>::growTo(Size size) {+    if (sz >= size) return;+    capacity(size);+    for (Size i = sz; i < size; i++) new (&data[i]) T();+    sz = size; }+++template<class T, class _Size>+void vec<T,_Size>::clear(bool dealloc) {+    if (data != NULL){+        for (Size i = 0; i < sz; i++) data[i].~T();+        sz = 0;+        if (dealloc) free(data), data = NULL, cap = 0; } }++//=================================================================================================+}++#endif
+ minisat/minisat/mtl/XAlloc.h view
@@ -0,0 +1,45 @@+/****************************************************************************************[XAlloc.h]+Copyright (c) 2009-2010, 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 Minisat_XAlloc_h+#define Minisat_XAlloc_h++#include <errno.h>+#include <stdlib.h>++namespace Minisat {++//=================================================================================================+// Simple layer on top of malloc/realloc to catch out-of-memory situtaions and provide some typing:++class OutOfMemoryException{};+static inline void* xrealloc(void *ptr, size_t size)+{+    void* mem = realloc(ptr, size);+    if (mem == NULL && errno == ENOMEM){+        throw OutOfMemoryException();+    }else+        return mem;+}++//=================================================================================================+}++#endif
+ minisat/minisat/simp/SimpSolver.cc view
@@ -0,0 +1,725 @@+/***********************************************************************************[SimpSolver.cc]+Copyright (c) 2006,      Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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.+**************************************************************************************************/++#include "minisat/mtl/Sort.h"+#include "minisat/simp/SimpSolver.h"+#include "minisat/utils/System.h"++using namespace Minisat;++//=================================================================================================+// Options:+++static const char* _cat = "SIMP";++static BoolOption   opt_use_asymm        (_cat, "asymm",        "Shrink clauses by asymmetric branching.", false);+static BoolOption   opt_use_rcheck       (_cat, "rcheck",       "Check if a clause is already implied. (costly)", false);+static BoolOption   opt_use_elim         (_cat, "elim",         "Perform variable elimination.", true);+static IntOption    opt_grow             (_cat, "grow",         "Allow a variable elimination step to grow by a number of clauses.", 0);+static IntOption    opt_clause_lim       (_cat, "cl-lim",       "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20,   IntRange(-1, INT32_MAX));+static IntOption    opt_subsumption_lim  (_cat, "sub-lim",      "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));+static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.",  0.5, DoubleRange(0, false, HUGE_VAL, false));+++//=================================================================================================+// Constructor/Destructor:+++SimpSolver::SimpSolver() :+    grow               (opt_grow)+  , clause_lim         (opt_clause_lim)+  , subsumption_lim    (opt_subsumption_lim)+  , simp_garbage_frac  (opt_simp_garbage_frac)+  , use_asymm          (opt_use_asymm)+  , use_rcheck         (opt_use_rcheck)+  , use_elim           (opt_use_elim)+  , extend_model       (true)+  , merges             (0)+  , asymm_lits         (0)+  , eliminated_vars    (0)+  , elimorder          (1)+  , use_simplification (true)+  , occurs             (ClauseDeleted(ca))+  , elim_heap          (ElimLt(n_occ))+  , bwdsub_assigns     (0)+  , n_touched          (0)+{+    vec<Lit> dummy(1,lit_Undef);+    ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.+    bwdsub_tmpunit        = ca.alloc(dummy);+    remove_satisfied      = false;+}+++SimpSolver::~SimpSolver()+{+}+++Var SimpSolver::newVar(lbool upol, bool dvar) {+    Var v = Solver::newVar(upol, dvar);++    frozen    .insert(v, (char)false);+    eliminated.insert(v, (char)false);++    if (use_simplification){+        n_occ     .insert( mkLit(v), 0);+        n_occ     .insert(~mkLit(v), 0);+        occurs    .init  (v);+        touched   .insert(v, 0);+        elim_heap .insert(v);+    }+    return v; }+++void SimpSolver::releaseVar(Lit l)+{+    assert(!isEliminated(var(l)));+    if (!use_simplification && var(l) >= max_simp_var)+        // Note: Guarantees that no references to this variable is+        // left in model extension datastructure. Could be improved!+        Solver::releaseVar(l);+    else+        // Otherwise, don't allow variable to be reused.+        Solver::addClause(l);+}+++lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)+{+    vec<Var> extra_frozen;+    lbool    result = l_True;++    do_simp &= use_simplification;++    if (do_simp){+        // Assumptions must be temporarily frozen to run variable elimination:+        for (int i = 0; i < assumptions.size(); i++){+            Var v = var(assumptions[i]);++            // If an assumption has been eliminated, remember it.+            assert(!isEliminated(v));++            if (!frozen[v]){+                // Freeze and store.+                setFrozen(v, true);+                extra_frozen.push(v);+            } }++        result = lbool(eliminate(turn_off_simp));+    }++    if (result == l_True)+        result = Solver::solve_();+    else if (verbosity >= 1)+        printf("===============================================================================\n");++    if (result == l_True && extend_model)+        extendModel();++    if (do_simp)+        // Unfreeze the assumptions that were frozen:+        for (int i = 0; i < extra_frozen.size(); i++)+            setFrozen(extra_frozen[i], false);++    return result;+}++++bool SimpSolver::addClause_(vec<Lit>& ps)+{+#ifndef NDEBUG+    for (int i = 0; i < ps.size(); i++)+        assert(!isEliminated(var(ps[i])));+#endif++    int nclauses = clauses.size();++    if (use_rcheck && implied(ps))+        return true;++    if (!Solver::addClause_(ps))+        return false;++    if (use_simplification && clauses.size() == nclauses + 1){+        CRef          cr = clauses.last();+        const Clause& c  = ca[cr];++        // NOTE: the clause is added to the queue immediately and then+        // again during 'gatherTouchedClauses()'. If nothing happens+        // in between, it will only be checked once. Otherwise, it may+        // be checked twice unnecessarily. This is an unfortunate+        // consequence of how backward subsumption is used to mimic+        // forward subsumption.+        subsumption_queue.insert(cr);+        for (int i = 0; i < c.size(); i++){+            occurs[var(c[i])].push(cr);+            n_occ[c[i]]++;+            touched[var(c[i])] = 1;+            n_touched++;+            if (elim_heap.inHeap(var(c[i])))+                elim_heap.increase(var(c[i]));+        }+    }++    return true;+}+++void SimpSolver::removeClause(CRef cr)+{+    const Clause& c = ca[cr];++    if (use_simplification)+        for (int i = 0; i < c.size(); i++){+            n_occ[c[i]]--;+            updateElimHeap(var(c[i]));+            occurs.smudge(var(c[i]));+        }++    Solver::removeClause(cr);+}+++bool SimpSolver::strengthenClause(CRef cr, Lit l)+{+    Clause& c = ca[cr];+    assert(decisionLevel() == 0);+    assert(use_simplification);++    // FIX: this is too inefficient but would be nice to have (properly implemented)+    // if (!find(subsumption_queue, &c))+    subsumption_queue.insert(cr);++    if (c.size() == 2){+        removeClause(cr);+        c.strengthen(l);+    }else{+        detachClause(cr, true);+        c.strengthen(l);+        attachClause(cr);+        remove(occurs[var(l)], cr);+        n_occ[l]--;+        updateElimHeap(var(l));+    }++    return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;+}+++// Returns FALSE if clause is always satisfied ('out_clause' should not be used).+bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)+{+    merges++;+    out_clause.clear();++    bool  ps_smallest = _ps.size() < _qs.size();+    const Clause& ps  =  ps_smallest ? _qs : _ps;+    const Clause& qs  =  ps_smallest ? _ps : _qs;++    for (int i = 0; i < qs.size(); i++){+        if (var(qs[i]) != v){+            for (int j = 0; j < ps.size(); j++)+                if (var(ps[j]) == var(qs[i])){+                    if (ps[j] == ~qs[i])+                        return false;+                    else+                        goto next;+                }+            out_clause.push(qs[i]);+        }+        next:;+    }++    for (int i = 0; i < ps.size(); i++)+        if (var(ps[i]) != v)+            out_clause.push(ps[i]);++    return true;+}+++// Returns FALSE if clause is always satisfied.+bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)+{+    merges++;++    bool  ps_smallest = _ps.size() < _qs.size();+    const Clause& ps  =  ps_smallest ? _qs : _ps;+    const Clause& qs  =  ps_smallest ? _ps : _qs;+    const Lit*  __ps  = (const Lit*)ps;+    const Lit*  __qs  = (const Lit*)qs;++    size = ps.size()-1;++    for (int i = 0; i < qs.size(); i++){+        if (var(__qs[i]) != v){+            for (int j = 0; j < ps.size(); j++)+                if (var(__ps[j]) == var(__qs[i])){+                    if (__ps[j] == ~__qs[i])+                        return false;+                    else+                        goto next;+                }+            size++;+        }+        next:;+    }++    return true;+}+++void SimpSolver::gatherTouchedClauses()+{+    if (n_touched == 0) return;++    int i,j;+    for (i = j = 0; i < subsumption_queue.size(); i++)+        if (ca[subsumption_queue[i]].mark() == 0)+            ca[subsumption_queue[i]].mark(2);++    for (i = 0; i < nVars(); i++)+        if (touched[i]){+            const vec<CRef>& cs = occurs.lookup(i);+            for (j = 0; j < cs.size(); j++)+                if (ca[cs[j]].mark() == 0){+                    subsumption_queue.insert(cs[j]);+                    ca[cs[j]].mark(2);+                }+            touched[i] = 0;+        }++    for (i = 0; i < subsumption_queue.size(); i++)+        if (ca[subsumption_queue[i]].mark() == 2)+            ca[subsumption_queue[i]].mark(0);++    n_touched = 0;+}+++bool SimpSolver::implied(const vec<Lit>& c)+{+    assert(decisionLevel() == 0);++    trail_lim.push(trail.size());+    for (int i = 0; i < c.size(); i++)+        if (value(c[i]) == l_True){+            cancelUntil(0);+            return true;+        }else if (value(c[i]) != l_False){+            assert(value(c[i]) == l_Undef);+            uncheckedEnqueue(~c[i]);+        }++    bool result = propagate() != CRef_Undef;+    cancelUntil(0);+    return result;+}+++// Backward subsumption + backward subsumption resolution+bool SimpSolver::backwardSubsumptionCheck(bool verbose)+{+    int cnt = 0;+    int subsumed = 0;+    int deleted_literals = 0;+    assert(decisionLevel() == 0);++    while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){++        // Empty subsumption queue and return immediately on user-interrupt:+        if (asynch_interrupt){+            subsumption_queue.clear();+            bwdsub_assigns = trail.size();+            break; }++        // Check top-level assignments by creating a dummy clause and placing it in the queue:+        if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){+            Lit l = trail[bwdsub_assigns++];+            ca[bwdsub_tmpunit][0] = l;+            ca[bwdsub_tmpunit].calcAbstraction();+            subsumption_queue.insert(bwdsub_tmpunit); }++        CRef    cr = subsumption_queue.peek(); subsumption_queue.pop();+        Clause& c  = ca[cr];++        if (c.mark()) continue;++        if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)+            printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);++        assert(c.size() > 1 || value(c[0]) == l_True);    // Unit-clauses should have been propagated before this point.++        // Find best variable to scan:+        Var best = var(c[0]);+        for (int i = 1; i < c.size(); i++)+            if (occurs[var(c[i])].size() < occurs[best].size())+                best = var(c[i]);++        // Search all candidates:+        vec<CRef>& _cs = occurs.lookup(best);+        CRef*       cs = (CRef*)_cs;++        for (int j = 0; j < _cs.size(); j++)+            if (c.mark())+                break;+            else if (!ca[cs[j]].mark() &&  cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){+                Lit l = c.subsumes(ca[cs[j]]);++                if (l == lit_Undef)+                    subsumed++, removeClause(cs[j]);+                else if (l != lit_Error){+                    deleted_literals++;++                    if (!strengthenClause(cs[j], ~l))+                        return false;++                    // Did current candidate get deleted from cs? Then check candidate at index j again:+                    if (var(l) == best)+                        j--;+                }+            }+    }++    return true;+}+++bool SimpSolver::asymm(Var v, CRef cr)+{+    Clause& c = ca[cr];+    assert(decisionLevel() == 0);++    if (c.mark() || satisfied(c)) return true;++    trail_lim.push(trail.size());+    Lit l = lit_Undef;+    for (int i = 0; i < c.size(); i++)+        if (var(c[i]) != v && value(c[i]) != l_False)+            uncheckedEnqueue(~c[i]);+        else+            l = c[i];++    if (propagate() != CRef_Undef){+        cancelUntil(0);+        asymm_lits++;+        if (!strengthenClause(cr, l))+            return false;+    }else+        cancelUntil(0);++    return true;+}+++bool SimpSolver::asymmVar(Var v)+{+    assert(use_simplification);++    const vec<CRef>& cls = occurs.lookup(v);++    if (value(v) != l_Undef || cls.size() == 0)+        return true;++    for (int i = 0; i < cls.size(); i++)+        if (!asymm(v, cls[i]))+            return false;++    return backwardSubsumptionCheck();+}+++static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)+{+    elimclauses.push(toInt(x));+    elimclauses.push(1);+}+++static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)+{+    int first = elimclauses.size();+    int v_pos = -1;++    // Copy clause to elimclauses-vector. Remember position where the+    // variable 'v' occurs:+    for (int i = 0; i < c.size(); i++){+        elimclauses.push(toInt(c[i]));+        if (var(c[i]) == v)+            v_pos = i + first;+    }+    assert(v_pos != -1);++    // Swap the first literal with the 'v' literal, so that the literal+    // containing 'v' will occur first in the clause:+    uint32_t tmp = elimclauses[v_pos];+    elimclauses[v_pos] = elimclauses[first];+    elimclauses[first] = tmp;++    // Store the length of the clause last:+    elimclauses.push(c.size());+}++++bool SimpSolver::eliminateVar(Var v)+{+    assert(!frozen[v]);+    assert(!isEliminated(v));+    assert(value(v) == l_Undef);++    // Split the occurrences into positive and negative:+    //+    const vec<CRef>& cls = occurs.lookup(v);+    vec<CRef>        pos, neg;+    for (int i = 0; i < cls.size(); i++)+        (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);++    // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no+    // clause must exceed the limit on the maximal clause size (if it is set):+    //+    int cnt         = 0;+    int clause_size = 0;++    for (int i = 0; i < pos.size(); i++)+        for (int j = 0; j < neg.size(); j++)+            if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) && +                (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))+                return true;++    // Delete and store old clauses:+    eliminated[v] = true;+    setDecisionVar(v, false);+    eliminated_vars++;++    if (pos.size() > neg.size()){+        for (int i = 0; i < neg.size(); i++)+            mkElimClause(elimclauses, v, ca[neg[i]]);+        mkElimClause(elimclauses, mkLit(v));+    }else{+        for (int i = 0; i < pos.size(); i++)+            mkElimClause(elimclauses, v, ca[pos[i]]);+        mkElimClause(elimclauses, ~mkLit(v));+    }++    for (int i = 0; i < cls.size(); i++)+        removeClause(cls[i]); ++    // Produce clauses in cross product:+    vec<Lit>& resolvent = add_tmp;+    for (int i = 0; i < pos.size(); i++)+        for (int j = 0; j < neg.size(); j++)+            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))+                return false;++    // Free occurs list for this variable:+    occurs[v].clear(true);+    +    // Free watchers lists for this variable, if possible:+    if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);+    if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);++    return backwardSubsumptionCheck();+}+++bool SimpSolver::substitute(Var v, Lit x)+{+    assert(!frozen[v]);+    assert(!isEliminated(v));+    assert(value(v) == l_Undef);++    if (!ok) return false;++    eliminated[v] = true;+    setDecisionVar(v, false);+    const vec<CRef>& cls = occurs.lookup(v);+    +    vec<Lit>& subst_clause = add_tmp;+    for (int i = 0; i < cls.size(); i++){+        Clause& c = ca[cls[i]];++        subst_clause.clear();+        for (int j = 0; j < c.size(); j++){+            Lit p = c[j];+            subst_clause.push(var(p) == v ? x ^ sign(p) : p);+        }++        removeClause(cls[i]);++        if (!addClause_(subst_clause))+            return ok = false;+    }++    return true;+}+++void SimpSolver::extendModel()+{+    int i, j;+    Lit x;++    for (i = elimclauses.size()-1; i > 0; i -= j){+        for (j = elimclauses[i--]; j > 1; j--, i--)+            if (modelValue(toLit(elimclauses[i])) != l_False)+                goto next;++        x = toLit(elimclauses[i]);+        model[var(x)] = lbool(!sign(x));+    next:;+    }+}+++bool SimpSolver::eliminate(bool turn_off_elim)+{+    if (!simplify())+        return false;+    else if (!use_simplification)+        return true;++    // Main simplification loop:+    //+    while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){++        gatherTouchedClauses();+        // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);+        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) && +            !backwardSubsumptionCheck(true)){+            ok = false; goto cleanup; }++        // Empty elim_heap and return immediately on user-interrupt:+        if (asynch_interrupt){+            assert(bwdsub_assigns == trail.size());+            assert(subsumption_queue.size() == 0);+            assert(n_touched == 0);+            elim_heap.clear();+            goto cleanup; }++        // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());+        for (int cnt = 0; !elim_heap.empty(); cnt++){+            Var elim = elim_heap.removeMin();+            +            if (asynch_interrupt) break;++            if (isEliminated(elim) || value(elim) != l_Undef) continue;++            if (verbosity >= 2 && cnt % 100 == 0)+                printf("elimination left: %10d\r", elim_heap.size());++            if (use_asymm){+                // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:+                bool was_frozen = frozen[elim];+                frozen[elim] = true;+                if (!asymmVar(elim)){+                    ok = false; goto cleanup; }+                frozen[elim] = was_frozen; }++            // At this point, the variable may have been set by assymetric branching, so check it+            // again. Also, don't eliminate frozen variables:+            if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){+                ok = false; goto cleanup; }++            checkGarbage(simp_garbage_frac);+        }++        assert(subsumption_queue.size() == 0);+    }+ cleanup:++    // If no more simplification is needed, free all simplification-related data structures:+    if (turn_off_elim){+        touched  .clear(true);+        occurs   .clear(true);+        n_occ    .clear(true);+        elim_heap.clear(true);+        subsumption_queue.clear(true);++        use_simplification    = false;+        remove_satisfied      = true;+        ca.extra_clause_field = false;+        max_simp_var          = nVars();++        // Force full cleanup (this is safe and desirable since it only happens once):+        rebuildOrderHeap();+        garbageCollect();+    }else{+        // Cheaper cleanup:+        checkGarbage();+    }++    if (verbosity >= 1 && elimclauses.size() > 0)+        printf("|  Eliminated clauses:     %10.2f Mb                                      |\n", +               double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));++    return ok;+}+++//=================================================================================================+// Garbage Collection methods:+++void SimpSolver::relocAll(ClauseAllocator& to)+{+    if (!use_simplification) return;++    // All occurs lists:+    //+    for (int i = 0; i < nVars(); i++){+        occurs.clean(i);+        vec<CRef>& cs = occurs[i];+        for (int j = 0; j < cs.size(); j++)+            ca.reloc(cs[j], to);+    }++    // Subsumption queue:+    //+    for (int i = subsumption_queue.size(); i > 0; i--){+        CRef cr = subsumption_queue.peek(); subsumption_queue.pop();+        if (ca[cr].mark()) continue;+        ca.reloc(cr, to);+        subsumption_queue.insert(cr);+    }+        +    // Temporary clause:+    //+    ca.reloc(bwdsub_tmpunit, to);+}+++void SimpSolver::garbageCollect()+{+    // Initialize the next region to a size corresponding to the estimated utilization degree. This+    // is not precise but should avoid some unnecessary reallocations for the new region:+    ClauseAllocator to(ca.size() - ca.wasted()); ++    to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.+    relocAll(to);+    Solver::relocAll(to);+    if (verbosity >= 2)+        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", +               ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);+    to.moveTo(ca);+}
+ minisat/minisat/simp/SimpSolver.h view
@@ -0,0 +1,222 @@+/************************************************************************************[SimpSolver.h]+Copyright (c) 2006,      Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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 Minisat_SimpSolver_h+#define Minisat_SimpSolver_h++#include "minisat/mtl/Queue.h"+#include "minisat/core/Solver.h"+++namespace Minisat {++//=================================================================================================+++class SimpSolver : public Solver {+ public:+    // Constructor/Destructor:+    //+    SimpSolver();+    ~SimpSolver();++    // Problem specification:+    //+    Var     newVar    (lbool upol = l_Undef, bool dvar = true);+    void    releaseVar(Lit l);+    bool    addClause (const vec<Lit>& ps);+    bool    addEmptyClause();                // Add the empty clause to the solver.+    bool    addClause (Lit p);               // Add a unit clause to the solver.+    bool    addClause (Lit p, Lit q);        // Add a binary clause to the solver.+    bool    addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.+    bool    addClause (Lit p, Lit q, Lit r, Lit s); // Add a quaternary clause to the solver. +    bool    addClause_(      vec<Lit>& ps);+    bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).++    // Variable mode:+    // +    void    setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.+    bool    isEliminated(Var v) const;++    // Alternative freeze interface (may replace 'setFrozen()'):+    void    freezeVar (Var v);         // Freeze one variable so it will not be eliminated.+    void    thaw      ();              // Thaw all frozen variables.+++    // Solving:+    //+    bool    solve       (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);+    lbool   solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);+    bool    solve       (                     bool do_simp = true, bool turn_off_simp = false);+    bool    solve       (Lit p       ,        bool do_simp = true, bool turn_off_simp = false);       +    bool    solve       (Lit p, Lit q,        bool do_simp = true, bool turn_off_simp = false);+    bool    solve       (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);+    bool    eliminate   (bool turn_off_elim = false);  // Perform variable elimination based simplification. ++    // Memory managment:+    //+    virtual void garbageCollect();+++    // Generate a (possibly simplified) DIMACS file:+    //+#if 0+    void    toDimacs  (const char* file, const vec<Lit>& assumps);+    void    toDimacs  (const char* file);+    void    toDimacs  (const char* file, Lit p);+    void    toDimacs  (const char* file, Lit p, Lit q);+    void    toDimacs  (const char* file, Lit p, Lit q, Lit r);+#endif++    // Mode of operation:+    //+    int     grow;              // Allow a variable elimination step to grow by a number of clauses (default to zero).+    int     clause_lim;        // Variables are not eliminated if it produces a resolvent with a length above this limit.+                               // -1 means no limit.+    int     subsumption_lim;   // Do not check if subsumption against a clause larger than this. -1 means no limit.+    double  simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').++    bool    use_asymm;         // Shrink clauses by asymmetric branching.+    bool    use_rcheck;        // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)+    bool    use_elim;          // Perform variable elimination.+    bool    extend_model;      // Flag to indicate whether the user needs to look at the full model.++    // Statistics:+    //+    int     merges;+    int     asymm_lits;+    int     eliminated_vars;++ protected:++    // Helper structures:+    //+    struct ElimLt {+        const LMap<int>& n_occ;+        explicit ElimLt(const LMap<int>& no) : n_occ(no) {}++        // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating+        // 32-bit implementation instead then, but this will have to do for now.+        uint64_t cost  (Var x)        const { return (uint64_t)n_occ[mkLit(x)] * (uint64_t)n_occ[~mkLit(x)]; }+        bool operator()(Var x, Var y) const { return cost(x) < cost(y); }+        +        // TODO: investigate this order alternative more.+        // bool operator()(Var x, Var y) const { +        //     int c_x = cost(x);+        //     int c_y = cost(y);+        //     return c_x < c_y || c_x == c_y && x < y; }+    };++    struct ClauseDeleted {+        const ClauseAllocator& ca;+        explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}+        bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };++    // Solver state:+    //+    int                 elimorder;+    bool                use_simplification;+    Var                 max_simp_var;        // Max variable at the point simplification was turned off.+    vec<uint32_t>       elimclauses;+    VMap<char>          touched;+    OccLists<Var, vec<CRef>, ClauseDeleted>+                        occurs;+    LMap<int>           n_occ;+    Heap<Var,ElimLt>    elim_heap;+    Queue<CRef>         subsumption_queue;+    VMap<char>          frozen;+    vec<Var>            frozen_vars;+    VMap<char>          eliminated;+    int                 bwdsub_assigns;+    int                 n_touched;++    // Temporaries:+    //+    CRef                bwdsub_tmpunit;++    // Main internal methods:+    //+    lbool         solve_                   (bool do_simp = true, bool turn_off_simp = false);+    bool          asymm                    (Var v, CRef cr);+    bool          asymmVar                 (Var v);+    void          updateElimHeap           (Var v);+    void          gatherTouchedClauses     ();+    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);+    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, int& size);+    bool          backwardSubsumptionCheck (bool verbose = false);+    bool          eliminateVar             (Var v);+    void          extendModel              ();++    void          removeClause             (CRef cr);+    bool          strengthenClause         (CRef cr, Lit l);+    bool          implied                  (const vec<Lit>& c);+    void          relocAll                 (ClauseAllocator& to);+};+++//=================================================================================================+// Implementation of inline methods:+++inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }+inline void SimpSolver::updateElimHeap(Var v) {+    assert(use_simplification);+    // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)+    if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))+        elim_heap.update(v); }+++inline bool SimpSolver::addClause    (const vec<Lit>& ps)    { ps.copyTo(add_tmp); return addClause_(add_tmp); }+inline bool SimpSolver::addEmptyClause()                     { add_tmp.clear(); return addClause_(add_tmp); }+inline bool SimpSolver::addClause    (Lit p)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }+inline bool SimpSolver::addClause    (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, Lit s){ add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); add_tmp.push(s); return addClause_(add_tmp); }+inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }++inline void SimpSolver::freezeVar(Var v){+    if (!frozen[v]){+        frozen[v] = 1;+        frozen_vars.push(v); +    } }++inline void SimpSolver::thaw(){+    for (int i = 0; i < frozen_vars.size(); i++){+        Var v = frozen_vars[i];+        frozen[v] = 0;+        if (use_simplification)+            updateElimHeap(v);+    }+    frozen_vars.clear(); }++inline bool SimpSolver::solve        (                     bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }+inline bool SimpSolver::solve        (Lit p       ,        bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; }+inline bool SimpSolver::solve        (Lit p, Lit q,        bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; }+inline bool SimpSolver::solve        (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; }+inline bool SimpSolver::solve        (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ +    budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; }++inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ +    assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }++//=================================================================================================+}++#endif
+ minisat/minisat/utils/Options.h view
@@ -0,0 +1,386 @@+/***************************************************************************************[Options.h]+Copyright (c) 2008-2010, 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 Minisat_Options_h+#define Minisat_Options_h++#include <stdlib.h>+#include <stdio.h>+#include <math.h>+#include <string.h>++#include "minisat/mtl/IntTypes.h"+#include "minisat/mtl/Vec.h"+#include "minisat/utils/ParseUtils.h"++namespace Minisat {++//==================================================================================================+// Top-level option parse/help functions:+++extern void parseOptions     (int& argc, char** argv, bool strict = false);+extern void printUsageAndExit(int  argc, char** argv, bool verbose = false);+extern void setUsageHelp     (const char* str);+extern void setHelpPrefixStr (const char* str);+++//==================================================================================================+// Options is an abstract class that gives the interface for all types options:+++class Option+{+ protected:+    const char* name;+    const char* description;+    const char* category;+    const char* type_name;++    static vec<Option*>& getOptionList () { static vec<Option*> options; return options; }+    static const char*&  getUsageString() { static const char* usage_str; return usage_str; }+    static const char*&  getHelpPrefixString() { static const char* help_prefix_str = ""; return help_prefix_str; }++    struct OptionLt {+        bool operator()(const Option* x, const Option* y) {+            int test1 = strcmp(x->category, y->category);+            return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);+        }+    };++    Option(const char* name_, +           const char* desc_,+           const char* cate_,+           const char* type_) : +      name       (name_)+    , description(desc_)+    , category   (cate_)+    , type_name  (type_)+    { +        getOptionList().push(this); +    }++ public:+    virtual ~Option() {}++    virtual bool parse             (const char* str)      = 0;+    virtual void help              (bool verbose = false) = 0;++    friend  void parseOptions      (int& argc, char** argv, bool strict);+    friend  void printUsageAndExit (int  argc, char** argv, bool verbose);+    friend  void setUsageHelp      (const char* str);+    friend  void setHelpPrefixStr  (const char* str);+};+++//==================================================================================================+// Range classes with specialization for floating types:+++struct IntRange {+    int begin;+    int end;+    IntRange(int b, int e) : begin(b), end(e) {}+};++struct Int64Range {+    int64_t begin;+    int64_t end;+    Int64Range(int64_t b, int64_t e) : begin(b), end(e) {}+};++struct DoubleRange {+    double begin;+    double end;+    bool  begin_inclusive;+    bool  end_inclusive;+    DoubleRange(double b, bool binc, double e, bool einc) : begin(b), end(e), begin_inclusive(binc), end_inclusive(einc) {}+};+++//==================================================================================================+// Double options:+++class DoubleOption : public Option+{+ protected:+    DoubleRange range;+    double      value;++ public:+    DoubleOption(const char* c, const char* n, const char* d, double def = double(), DoubleRange r = DoubleRange(-HUGE_VAL, false, HUGE_VAL, false))+        : Option(n, d, c, "<double>"), range(r), value(def) {+        // FIXME: set LC_NUMERIC to "C" to make sure that strtof/strtod parses decimal point correctly.+    }++    operator      double   (void) const { return value; }+    operator      double&  (void)       { return value; }+    DoubleOption& operator=(double x)   { value = x; return *this; }++    virtual bool parse(const char* str){+        const char* span = str; ++        if (!match(span, "-") || !match(span, name) || !match(span, "="))+            return false;++        char*  end;+        double tmp = strtod(span, &end);++        if (end == NULL) +            return false;+        else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)){+            fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);+            exit(1);+        }else if (tmp <= range.begin && (!range.begin_inclusive || tmp != range.begin)){+            fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);+            exit(1); }++        value = tmp;+        // fprintf(stderr, "READ VALUE: %g\n", value);++        return true;+    }++    virtual void help (bool verbose = false){+        fprintf(stderr, "  -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n", +                name, type_name, +                range.begin_inclusive ? '[' : '(', +                range.begin,+                range.end,+                range.end_inclusive ? ']' : ')', +                value);+        if (verbose){+            fprintf(stderr, "\n        %s\n", description);+            fprintf(stderr, "\n");+        }+    }+};+++//==================================================================================================+// Int options:+++class IntOption : public Option+{+ protected:+    IntRange range;+    int32_t  value;++ public:+    IntOption(const char* c, const char* n, const char* d, int32_t def = int32_t(), IntRange r = IntRange(INT32_MIN, INT32_MAX))+        : Option(n, d, c, "<int32>"), range(r), value(def) {}+ +    operator   int32_t   (void) const { return value; }+    operator   int32_t&  (void)       { return value; }+    IntOption& operator= (int32_t x)  { value = x; return *this; }++    virtual bool parse(const char* str){+        const char* span = str; ++        if (!match(span, "-") || !match(span, name) || !match(span, "="))+            return false;++        char*   end;+        int32_t tmp = strtol(span, &end, 10);++        if (end == NULL) +            return false;+        else if (tmp > range.end){+            fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);+            exit(1);+        }else if (tmp < range.begin){+            fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);+            exit(1); }++        value = tmp;++        return true;+    }++    virtual void help (bool verbose = false){+        fprintf(stderr, "  -%-12s = %-8s [", name, type_name);+        if (range.begin == INT32_MIN)+            fprintf(stderr, "imin");+        else+            fprintf(stderr, "%4d", range.begin);++        fprintf(stderr, " .. ");+        if (range.end == INT32_MAX)+            fprintf(stderr, "imax");+        else+            fprintf(stderr, "%4d", range.end);++        fprintf(stderr, "] (default: %d)\n", value);+        if (verbose){+            fprintf(stderr, "\n        %s\n", description);+            fprintf(stderr, "\n");+        }+    }+};+++// Leave this out for visual C++ until Microsoft implements C99 and gets support for strtoll.+#ifndef _MSC_VER++class Int64Option : public Option+{+ protected:+    Int64Range range;+    int64_t  value;++ public:+    Int64Option(const char* c, const char* n, const char* d, int64_t def = int64_t(), Int64Range r = Int64Range(INT64_MIN, INT64_MAX))+        : Option(n, d, c, "<int64>"), range(r), value(def) {}+ +    operator     int64_t   (void) const { return value; }+    operator     int64_t&  (void)       { return value; }+    Int64Option& operator= (int64_t x)  { value = x; return *this; }++    virtual bool parse(const char* str){+        const char* span = str; ++        if (!match(span, "-") || !match(span, name) || !match(span, "="))+            return false;++        char*   end;+        int64_t tmp = strtoll(span, &end, 10);++        if (end == NULL) +            return false;+        else if (tmp > range.end){+            fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);+            exit(1);+        }else if (tmp < range.begin){+            fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);+            exit(1); }++        value = tmp;++        return true;+    }++    virtual void help (bool verbose = false){+        fprintf(stderr, "  -%-12s = %-8s [", name, type_name);+        if (range.begin == INT64_MIN)+            fprintf(stderr, "imin");+        else+            fprintf(stderr, "%4"PRIi64, range.begin);++        fprintf(stderr, " .. ");+        if (range.end == INT64_MAX)+            fprintf(stderr, "imax");+        else+            fprintf(stderr, "%4"PRIi64, range.end);++        fprintf(stderr, "] (default: %"PRIi64")\n", value);+        if (verbose){+            fprintf(stderr, "\n        %s\n", description);+            fprintf(stderr, "\n");+        }+    }+};+#endif++//==================================================================================================+// String option:+++class StringOption : public Option+{+    const char* value;+ public:+    StringOption(const char* c, const char* n, const char* d, const char* def = NULL) +        : Option(n, d, c, "<string>"), value(def) {}++    operator      const char*  (void) const     { return value; }+    operator      const char*& (void)           { return value; }+    StringOption& operator=    (const char* x)  { value = x; return *this; }++    virtual bool parse(const char* str){+        const char* span = str; ++        if (!match(span, "-") || !match(span, name) || !match(span, "="))+            return false;++        value = span;+        return true;+    }++    virtual void help (bool verbose = false){+        fprintf(stderr, "  -%-10s = %8s\n", name, type_name);+        if (verbose){+            fprintf(stderr, "\n        %s\n", description);+            fprintf(stderr, "\n");+        }+    }    +};+++//==================================================================================================+// Bool option:+++class BoolOption : public Option+{+    bool value;++ public:+    BoolOption(const char* c, const char* n, const char* d, bool v) +        : Option(n, d, c, "<bool>"), value(v) {}++    operator    bool     (void) const { return value; }+    operator    bool&    (void)       { return value; }+    BoolOption& operator=(bool b)     { value = b; return *this; }++    virtual bool parse(const char* str){+        const char* span = str; +        +        if (match(span, "-")){+            bool b = !match(span, "no-");++            if (strcmp(span, name) == 0){+                value = b;+                return true; }+        }++        return false;+    }++    virtual void help (bool verbose = false){++        fprintf(stderr, "  -%s, -no-%s", name, name);++        for (uint32_t i = 0; i < 32 - strlen(name)*2; i++)+            fprintf(stderr, " ");++        fprintf(stderr, " ");+        fprintf(stderr, "(default: %s)\n", value ? "on" : "off");+        if (verbose){+            fprintf(stderr, "\n        %s\n", description);+            fprintf(stderr, "\n");+        }+    }+};++//=================================================================================================+}++#endif
+ minisat/minisat/utils/ParseUtils.h view
@@ -0,0 +1,129 @@+/************************************************************************************[ParseUtils.h]+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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 Minisat_ParseUtils_h+#define Minisat_ParseUtils_h++#include <stdlib.h>+#include <stdio.h>++#include <zlib.h>++#include "minisat/mtl/XAlloc.h"++namespace Minisat {++//-------------------------------------------------------------------------------------------------+// A simple buffered character stream class:++++class StreamBuffer {+    gzFile         in;+    unsigned char* buf;+    int            pos;+    int            size;++    enum { buffer_size = 64*1024 };++    void assureLookahead() {+        if (pos >= size) {+            pos  = 0;+            size = gzread(in, buf, buffer_size); } }++public:+    explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0){+        buf = (unsigned char*)xrealloc(NULL, buffer_size);+        assureLookahead();+    }+    ~StreamBuffer() { free(buf); }++    int  operator *  () const { return (pos >= size) ? EOF : buf[pos]; }+    void operator ++ ()       { pos++; assureLookahead(); }+    int  position    () const { return pos; }+};+++//-------------------------------------------------------------------------------------------------+// End-of-file detection functions for StreamBuffer and char*:+++static inline bool isEof(StreamBuffer& in) { return *in == EOF;  }+static inline bool isEof(const char*   in) { return *in == '\0'; }++//-------------------------------------------------------------------------------------------------+// Generic parse functions parametrized over the input-stream type.+++template<class B>+static void skipWhitespace(B& in) {+    while ((*in >= 9 && *in <= 13) || *in == 32)+        ++in; }+++template<class B>+static void skipLine(B& in) {+    for (;;){+        if (isEof(in)) return;+        if (*in == '\n') { ++in; return; }+        ++in; } }+++template<class B>+static int parseInt(B& in) {+    int     val = 0;+    bool    neg = false;+    skipWhitespace(in);+    if      (*in == '-') neg = true, ++in;+    else if (*in == '+') ++in;+    if (*in < '0' || *in > '9') fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3);+    while (*in >= '0' && *in <= '9')+        val = val*10 + (*in - '0'),+        ++in;+    return neg ? -val : val; }+++// String matching: in case of a match the input iterator will be advanced the corresponding+// number of characters.+template<class B>+static bool match(B& in, const char* str) {+    int i;+    for (i = 0; str[i] != '\0'; i++)+        if (in[i] != str[i])+            return false;++    in += i;++    return true; +}++// String matching: consumes characters eagerly, but does not require random access iterator.+template<class B>+static bool eagerMatch(B& in, const char* str) {+    for (; *str != '\0'; ++str, ++in)+        if (*str != *in)+            return false;+    return true; }+++//=================================================================================================+}++#endif
+ minisat/minisat/utils/System.cc view
@@ -0,0 +1,169 @@+/***************************************************************************************[System.cc]+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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.+**************************************************************************************************/++#include <signal.h>+#include <stdio.h>++#include "minisat/utils/System.h"++#if defined(__linux__)++#include <stdlib.h>++using namespace Minisat;++static inline int memReadStat(int field)+{+    char  name[256];+    pid_t pid = getpid();+    int   value;++    sprintf(name, "/proc/%d/statm", pid);+    FILE* in = fopen(name, "rb");+    if (in == NULL) return 0;++    for (; field >= 0; field--)+        if (fscanf(in, "%d", &value) != 1)+            printf("ERROR! Failed to parse memory statistics from \"/proc\".\n"), exit(1);+    fclose(in);+    return value;+}+++static inline int memReadPeak(void)+{+    char  name[256];+    pid_t pid = getpid();++    sprintf(name, "/proc/%d/status", pid);+    FILE* in = fopen(name, "rb");+    if (in == NULL) return 0;++    // Find the correct line, beginning with "VmPeak:":+    int peak_kb = 0;+    while (!feof(in) && fscanf(in, "VmPeak: %d kB", &peak_kb) != 1)+        while (!feof(in) && fgetc(in) != '\n')+            ;+    fclose(in);++    return peak_kb;+}++double Minisat::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }+double Minisat::memUsedPeak(bool strictlyPeak) { +    double peak = memReadPeak() / (double)1024;+    return peak == 0 && !strictlyPeak ? memUsed() : peak; }++#elif defined(__FreeBSD__) || defined(__FreeBSD_kernel__) || defined(__gnu_hurd__)++double Minisat::memUsed() {+    struct rusage ru;+    getrusage(RUSAGE_SELF, &ru);+    return (double)ru.ru_maxrss / 1024; }+double Minisat::memUsedPeak(bool) { return memUsed(); }+++#elif defined(__APPLE__)+#include <malloc/malloc.h>++double Minisat::memUsed() {+    malloc_statistics_t t;+    malloc_zone_statistics(NULL, &t);+    return (double)t.max_size_in_use / (1024*1024); }+double Minisat::memUsedPeak(bool) { return memUsed(); }++#else+double Minisat::memUsed()     { return 0; }+double Minisat::memUsedPeak(bool) { return 0; }+#endif+++void Minisat::setX86FPUPrecision()+{+#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)+    // Only correct FPU precision on Linux architectures that needs and supports it:+    fpu_control_t oldcw, newcw;+    _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);+    printf("WARNING: for repeatability, setting FPU to use double precision\n");+#endif+}+++#if !defined(_MSC_VER) && !defined(__MINGW32__)+void Minisat::limitMemory(uint64_t max_mem_mb)+{+// FIXME: OpenBSD does not support RLIMIT_AS. Not sure how well RLIMIT_DATA works instead.+#if defined(__OpenBSD__)+#define RLIMIT_AS RLIMIT_DATA+#endif++    // Set limit on virtual memory:+    if (max_mem_mb != 0){+        rlim_t new_mem_lim = (rlim_t)max_mem_mb * 1024*1024;+        rlimit rl;+        getrlimit(RLIMIT_AS, &rl);+        if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){+            rl.rlim_cur = new_mem_lim;+            if (setrlimit(RLIMIT_AS, &rl) == -1)+                printf("WARNING! Could not set resource limit: Virtual memory.\n");+        }+    }++#if defined(__OpenBSD__)+#undef RLIMIT_AS+#endif+}+#else+void Minisat::limitMemory(uint64_t /*max_mem_mb*/)+{+    printf("WARNING! Memory limit not supported on this architecture.\n");+}+#endif+++#if !defined(_MSC_VER) && !defined(__MINGW32__)+void Minisat::limitTime(uint32_t max_cpu_time)+{+    if (max_cpu_time != 0){+        rlimit rl;+        getrlimit(RLIMIT_CPU, &rl);+        if (rl.rlim_max == RLIM_INFINITY || (rlim_t)max_cpu_time < rl.rlim_max){+            rl.rlim_cur = max_cpu_time;+            if (setrlimit(RLIMIT_CPU, &rl) == -1)+                printf("WARNING! Could not set resource limit: CPU-time.\n");+        }+    }+}+#else+void Minisat::limitTime(uint32_t /*max_cpu_time*/)+{+    printf("WARNING! CPU-time limit not supported on this architecture.\n");+}+#endif+++void Minisat::sigTerm(void handler(int))+{+    signal(SIGINT, handler);+    signal(SIGTERM,handler);+#ifdef SIGXCPU+    signal(SIGXCPU,handler);+#endif+}
+ minisat/minisat/utils/System.h view
@@ -0,0 +1,72 @@+/****************************************************************************************[System.h]+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson+Copyright (c) 2007-2010, 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 Minisat_System_h+#define Minisat_System_h++#if defined(__linux__)+#include <fpu_control.h>+#endif++#include "minisat/mtl/IntTypes.h"++//-------------------------------------------------------------------------------------------------++namespace Minisat {++static inline double cpuTime(void); // CPU-time in seconds.++extern double memUsed();            // Memory in mega bytes (returns 0 for unsupported architectures).+extern double memUsedPeak(bool strictlyPeak = false); // Peak-memory in mega bytes (returns 0 for unsupported architectures).++extern void   setX86FPUPrecision(); // Make sure double's are represented with the same precision+                                    // in memory and registers.++extern void   limitMemory(uint64_t max_mem_mb); // Set a limit on total memory usage. The exact+                                                // semantics varies depending on architecture.++extern void   limitTime(uint32_t max_cpu_time); // Set a limit on maximum CPU time. The exact+                                                // semantics varies depending on architecture.++extern void   sigTerm(void handler(int));      // Set up handling of available termination signals.++}++//-------------------------------------------------------------------------------------------------+// Implementation of inline functions:++#if defined(_MSC_VER) || defined(__MINGW32__)+#include <time.h>++static inline double Minisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }++#else+#include <sys/time.h>+#include <sys/resource.h>+#include <unistd.h>++static inline double Minisat::cpuTime(void) {+    struct rusage ru;+    getrusage(RUSAGE_SELF, &ru);+    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }++#endif++#endif