abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Data Structures | Typedefs | Functions | Variables
Minisat Namespace Reference

Data Structures

class  RegionAllocator
 
class  Heap
 
struct  Hash
 
struct  Equal
 
struct  DeepHash
 
struct  DeepEqual
 
class  Map
 
class  Option
 
struct  IntRange
 
struct  Int64Range
 
struct  DoubleRange
 
class  DoubleOption
 
class  IntOption
 
class  StringOption
 
class  BoolOption
 
class  StreamBuffer
 
class  Queue
 
class  SimpSolver
 
class  Solver
 
struct  Lit
 
class  lbool
 
class  Clause
 
class  ClauseAllocator
 
class  OccLists
 
class  CMap
 
struct  LessThan_default
 
class  vec
 
class  OutOfMemoryException
 

Typedefs

typedef int Var
 
typedef RegionAllocator
< uint32_t >::Ref 		CRef
 

Functions

template<class V , class T >
static void remove (V &ts, const T &t)
 
template<class V , class T >
static bool find (V &ts, const T &t)
 
template<class T >
static void copy (const T &from, T &to)
 
template<class T >
static void copy (const vec< T > &from, vec< T > &to, bool append=false)
 
template<class T >
static void append (const vec< T > &from, vec< T > &to)
 
template<class B , class Solver >
static void readClause (B &in, Solver &S, vec< Lit > &lits)
 
template<class B , class Solver >
static void parse_DIMACS_main (B &in, Solver &S)
 
template<class Solver >
static void parse_DIMACS (gzFile input_stream, Solver &S)
 
static uint32_t hash (uint32_t x)
 
static uint32_t hash (uint64_t x)
 
static uint32_t hash (int32_t x)
 
static uint32_t hash (int64_t x)
 
int parseOptions (int &argc, char **argv, bool strict=false)
 
int printUsageAndExit (int argc, char **argv, bool verbose=false)
 
void setUsageHelp (const char *str)
 
void setHelpPrefixStr (const char *str)
 
static bool isEof (StreamBuffer &in)
 
static bool isEof (const char *in)
 
template<class B >
static void skipWhitespace (B &in)
 
template<class B >
static void skipLine (B &in)
 
template<class B >
static int parseInt (B &in)
 
template<class B >
static bool match (B &in, const char *str)
 
template<class B >
static bool eagerMatch (B &in, const char *str)
 
Lit mkLit (Var var, bool sign)
 
Lit operator~ (Lit p)
 
Lit operator^ (Lit p, bool b)
 
bool sign (Lit p)
 
int var (Lit p)
 
int toInt (Var v)
 
int toInt (Lit p)
 
Lit toLit (int i)
 
int toInt (lbool l)
 
lbool toLbool (int v)
 
template<class T , class LessThan >
void selectionSort (T *array, int size, LessThan lt)
 
template<class T >
static void selectionSort (T *array, int size)
 
template<class T , class LessThan >
void sort (T *array, int size, LessThan lt)
 
template<class T >
static void sort (T *array, int size)
 
template<class T , class LessThan >
void sort (vec< T > &v, LessThan lt)
 
template<class T >
void sort (vec< T > &v)
 
static double cpuTime (void)
 
double memUsed ()
 
double memUsedPeak ()
 
static void * xrealloc (void *ptr, size_t size)
 

Variables

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 }
 
static const int buffer_size = 1048576
 
const Lit lit_Undef = { -2 }
 
const Lit lit_Error = { -1 }
 
const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef
 

Typedef Documentation

typedef RegionAllocator<uint32_t>::Ref Minisat::CRef

Definition at line 120 of file SolverTypes.h.

typedef int Minisat::Var

Definition at line 42 of file SolverTypes.h.

Function Documentation

template<class T >
static void Minisat::append ( const vec< T > &  from,
vec< T > &  to 
)
inlinestatic

Definition at line 79 of file Alg.h.

79 { copy(from, to, true); }
Minisat::copy
static void copy(const vec< T > &from, vec< T > &to, bool append=false)
Definition: Alg.h:68
template<class T >
static void Minisat::copy ( const T &  from,
T &  to 
)
inlinestatic

Definition at line 61 of file Alg.h.

62 {
63  to = from;
64 }
template<class T >
static void Minisat::copy ( const vec< T > &  from,
vec< T > &  to,
bool  append = false 
)
inlinestatic

Definition at line 68 of file Alg.h.

69 {
70  if (!append)
71  to.clear();
72  for (int i = 0; i < from.size(); i++){
73  to.push();
74  copy(from[i], to.last());
75  }
76 }
Minisat::append
static void append(const vec< T > &from, vec< T > &to)
Definition: Alg.h:79
Minisat::copy
static void copy(const vec< T > &from, vec< T > &to, bool append=false)
Definition: Alg.h:68
static double Minisat::cpuTime ( void  )
inlinestatic

Definition at line 53 of file System.h.

53  {
54  struct rusage ru;
55  getrusage(RUSAGE_SELF, &ru);
56  return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
template<class B >
static bool Minisat::eagerMatch ( B &  in,
const char *  str 
)
static

Definition at line 112 of file ParseUtils.h.

112  {
113  for (; *str != '\0'; ++str, ++in)
114  if (*str != *in)
115  return false;
116  return true; }
template<class V , class T >
static bool Minisat::find ( V &  ts,
const T &  t 
)
inlinestatic

Definition at line 47 of file Alg.h.

48 {
49  int j = 0;
50  for (; j < ts.size() && ts[j] != t; j++);
51  return j < ts.size();
52 }
static uint32_t Minisat::hash ( uint32_t  x)
inlinestatic

Definition at line 38 of file Map.h.

38 { return x; }
static uint32_t Minisat::hash ( uint64_t  x)
inlinestatic

Definition at line 39 of file Map.h.

39 { return (uint32_t)x; }
static uint32_t Minisat::hash ( int32_t  x)
inlinestatic

Definition at line 40 of file Map.h.

40 { return (uint32_t)x; }
static uint32_t Minisat::hash ( int64_t  x)
inlinestatic

Definition at line 41 of file Map.h.

41 { return (uint32_t)x; }
static bool Minisat::isEof ( StreamBuffer &  in)
inlinestatic

Definition at line 61 of file ParseUtils.h.

61 { return *in == EOF; }
static bool Minisat::isEof ( const char *  in)
inlinestatic

Definition at line 62 of file ParseUtils.h.

62 { return *in == '\0'; }
template<class B >
static bool Minisat::match ( B &  in,
const char *  str 
)
static

Definition at line 99 of file ParseUtils.h.

99  {
100  int i;
101  for (i = 0; str[i] != '\0'; i++)
102  if (in[i] != str[i])
103  return false;
104 
105  in += i;
106 
107  return true;
108 }
double Minisat::memUsed ( )

Definition at line 93 of file System.cpp.

93 { return 0; }
double Minisat::memUsedPeak ( )

Definition at line 94 of file System.cpp.

94 { return 0; }
Lit Minisat::mkLit ( Var  var,
bool  sign = false 
)
inline

Definition at line 58 of file SolverTypes.h.

58 { Lit p; p.x = var + var + (int)sign; return p; }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
Minisat::sign
bool sign(Lit p)
Definition: SolverTypes.h:61
Lit Minisat::operator^ ( Lit  p,
bool  b 
)
inline

Definition at line 60 of file SolverTypes.h.

60 { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Lit Minisat::operator~ ( Lit  p)
inline

Definition at line 59 of file SolverTypes.h.

59 { Lit q; q.x = p.x ^ 1; return q; }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
template<class Solver >
static void Minisat::parse_DIMACS ( gzFile  input_stream,
Solver &  S 
)
static

Definition at line 82 of file Dimacs.h.

82  {
83  StreamBuffer in(input_stream);
84  parse_DIMACS_main(in, S); }
Minisat::parse_DIMACS_main
static void parse_DIMACS_main(B &in, Solver &S)
Definition: Dimacs.h:48
S
static shot S[256]
Definition: kitPerm.c:40
template<class B , class Solver >
static void Minisat::parse_DIMACS_main ( B &  in,
Solver &  S 
)
static

Definition at line 48 of file Dimacs.h.

48  {
49  vec<Lit> lits;
50  int vars = 0;
51  int clauses = 0;
52  int cnt = 0;
53  for (;;){
54  skipWhitespace(in);
55  if (*in == EOF) break;
56  else if (*in == 'p'){
57  if (eagerMatch(in, "p cnf")){
58  vars = parseInt(in);
59  clauses = parseInt(in);
60  // SATRACE'06 hack
61  // if (clauses > 4000000)
62  // S.eliminate(true);
63  }else{
64  printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
65  }
66  } else if (*in == 'c' || *in == 'p')
67  skipLine(in);
68  else{
69  cnt++;
70  readClause(in, S, lits);
71  S.addClause_(lits); }
72  }
73  if (vars != S.nVars())
74  fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of variables.\n");
75  if (cnt != clauses)
76  fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of clauses.\n");
77 }
exit
VOID_HACK exit()
Minisat::eagerMatch
static bool eagerMatch(B &in, const char *str)
Definition: ParseUtils.h:112
Minisat::readClause
static void readClause(B &in, Solver &S, vec< Lit > &lits)
Definition: Dimacs.h:35
Minisat::parseInt
static int parseInt(B &in)
Definition: ParseUtils.h:83
Minisat::skipWhitespace
static void skipWhitespace(B &in)
Definition: ParseUtils.h:69
skipLine
static void skipLine(char **pIn)
Definition: msatRead.c:111
S
static shot S[256]
Definition: kitPerm.c:40
template<class B >
static int Minisat::parseInt ( B &  in)
static

Definition at line 83 of file ParseUtils.h.

83  {
84  int val = 0;
85  bool neg = false;
86  skipWhitespace(in);
87  if (*in == '-') neg = true, ++in;
88  else if (*in == '+') ++in;
89  if (*in < '0' || *in > '9') fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
90  while (*in >= '0' && *in <= '9')
91  val = val*10 + (*in - '0'),
92  ++in;
93  return neg ? -val : val; }
exit
VOID_HACK exit()
Minisat::skipWhitespace
static void skipWhitespace(B &in)
Definition: ParseUtils.h:69
int Minisat::parseOptions ( int &  argc,
char **  argv,
bool  strict = false 
)

Definition at line 26 of file Options.cpp.

27 {
28  int i, j;
29  for (i = j = 1; i < argc; i++){
30  const char* str = argv[i];
31  if (match(str, "--") && match(str, Option::getHelpPrefixString()) && match(str, "help")){
32  if (*str == '\0')
33  return printUsageAndExit(argc, argv);
34  else if (match(str, "-verb"))
35  return printUsageAndExit(argc, argv, true);
36  } else {
37  bool parsed_ok = false;
38 
39  for (int k = 0; !parsed_ok && k < Option::getOptionList().size(); k++){
40  parsed_ok = Option::getOptionList()[k]->parse(argv[i]);
41 
42  // fprintf(stderr, "checking %d: %s against flag <%s> (%s)\n", i, argv[i], Option::getOptionList()[k]->name, parsed_ok ? "ok" : "skip");
43  }
44 
45  if (!parsed_ok)
46  if (strict && match(argv[i], "-"))
47  { fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()); return 0; } // exit(0);
48  else
49  argv[j++] = argv[i];
50  }
51  }
52 
53  argc -= (i - j);
54  return 1;
55 }
Minisat::match
static bool match(B &in, const char *str)
Definition: ParseUtils.h:99
Minisat::printUsageAndExit
int printUsageAndExit(int argc, char **argv, bool verbose=false)
Definition: Options.cpp:60
int Minisat::printUsageAndExit ( int  argc,
char **  argv,
bool  verbose = false 
)

Definition at line 60 of file Options.cpp.

61 {
62  const char* usage = Option::getUsageString();
63  if (usage != NULL)
64  fprintf(stderr, usage, argv[0]);
65 
66  sort(Option::getOptionList(), Option::OptionLt());
67 
68  const char* prev_cat = NULL;
69  const char* prev_type = NULL;
70 
71  for (int i = 0; i < Option::getOptionList().size(); i++){
72  const char* cat = Option::getOptionList()[i]->category;
73  const char* type = Option::getOptionList()[i]->type_name;
74 
75  if (cat != prev_cat)
76  fprintf(stderr, "\n%s OPTIONS:\n\n", cat);
77  else if (type != prev_type)
78  fprintf(stderr, "\n");
79 
80  Option::getOptionList()[i]->help(verbose);
81 
82  prev_cat = Option::getOptionList()[i]->category;
83  prev_type = Option::getOptionList()[i]->type_name;
84  }
85 
86  fprintf(stderr, "\nHELP OPTIONS:\n\n");
87  fprintf(stderr, " --%shelp Print help message.\n", Option::getHelpPrefixString());
88  fprintf(stderr, " --%shelp-verb Print verbose help message.\n", Option::getHelpPrefixString());
89  fprintf(stderr, "\n");
90 // exit(0);
91  return 0;
92 }
Minisat::sort
void sort(T *array, int size, LessThan lt)
Definition: Sort.h:57
template<class B , class Solver >
static void Minisat::readClause ( B &  in,
Solver &  S,
vec< Lit > &  lits 
)
static

Definition at line 35 of file Dimacs.h.

35  {
36  int parsed_lit, var;
37  lits.clear();
38  for (;;){
39  parsed_lit = parseInt(in);
40  if (parsed_lit == 0) break;
41  var = abs(parsed_lit)-1;
42  while (var >= S.nVars()) S.newVar();
43  lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
44  }
45 }
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
Minisat::mkLit
Lit mkLit(Var var, bool sign)
Definition: SolverTypes.h:58
Minisat::parseInt
static int parseInt(B &in)
Definition: ParseUtils.h:83
S
static shot S[256]
Definition: kitPerm.c:40
template<class V , class T >
static void Minisat::remove ( V &  ts,
const T &  t 
)
inlinestatic

Definition at line 36 of file Alg.h.

37 {
38  int j = 0;
39  for (; j < ts.size() && ts[j] != t; j++);
40  assert(j < ts.size());
41  for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
42  ts.pop();
43 }
assert
#define assert(ex)
Definition: util_old.h:213
template<class T , class LessThan >
void Minisat::selectionSort ( T *  array,
int  size,
LessThan  lt 
)

Definition at line 39 of file Sort.h.

40 {
41  int i, j, best_i;
42  T tmp;
43 
44  for (i = 0; i < size-1; i++){
45  best_i = i;
46  for (j = i+1; j < size; j++){
47  if (lt(array[j], array[best_i]))
48  best_i = j;
49  }
50  tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
51  }
52 }
size
static int size
Definition: cuddSign.c:86
template<class T >
static void Minisat::selectionSort ( T *  array,
int  size 
)
inlinestatic

Definition at line 53 of file Sort.h.

53  {
54  selectionSort(array, size, LessThan_default<T>()); }
size
static int size
Definition: cuddSign.c:86
Minisat::selectionSort
static void selectionSort(T *array, int size)
Definition: Sort.h:53
void Minisat::setHelpPrefixStr ( const char *  str)

Definition at line 59 of file Options.cpp.

59 { Option::getHelpPrefixString() = str; }
void Minisat::setUsageHelp ( const char *  str)

Definition at line 58 of file Options.cpp.

58 { Option::getUsageString() = str; }
bool Minisat::sign ( Lit  p)
inline

Definition at line 61 of file SolverTypes.h.

61 { return p.x & 1; }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
template<class B >
static void Minisat::skipLine ( B &  in)
static

Definition at line 75 of file ParseUtils.h.

75  {
76  for (;;){
77  if (isEof(in)) return;
78  if (*in == '\n') { ++in; return; }
79  ++in; } }
Minisat::isEof
static bool isEof(const char *in)
Definition: ParseUtils.h:62
template<class B >
static void Minisat::skipWhitespace ( B &  in)
static

Definition at line 69 of file ParseUtils.h.

69  {
70  while ((*in >= 9 && *in <= 13) || *in == 32)
71  ++in; }
template<class T , class LessThan >
void Minisat::sort ( T *  array,
int  size,
LessThan  lt 
)

Definition at line 57 of file Sort.h.

58 {
59  if (size <= 15)
60  selectionSort(array, size, lt);
61 
62  else{
63  T pivot = array[size / 2];
64  T tmp;
65  int i = -1;
66  int j = size;
67 
68  for(;;){
69  do i++; while(lt(array[i], pivot));
70  do j--; while(lt(pivot, array[j]));
71 
72  if (i >= j) break;
73 
74  tmp = array[i]; array[i] = array[j]; array[j] = tmp;
75  }
76 
77  sort(array , i , lt);
78  sort(&array[i], size-i, lt);
79  }
80 }
size
static int size
Definition: cuddSign.c:86
Minisat::sort
void sort(vec< T > &v)
Definition: Sort.h:91
Minisat::selectionSort
static void selectionSort(T *array, int size)
Definition: Sort.h:53
template<class T >
static void Minisat::sort ( T *  array,
int  size 
)
inlinestatic

Definition at line 81 of file Sort.h.

81  {
82  sort(array, size, LessThan_default<T>()); }
size
static int size
Definition: cuddSign.c:86
Minisat::sort
void sort(vec< T > &v)
Definition: Sort.h:91
template<class T , class LessThan >
void Minisat::sort ( vec< T > &  v,
LessThan  lt 
)

Definition at line 89 of file Sort.h.

89  {
90  sort((T*)v, v.size(), lt); }
Minisat::sort
void sort(vec< T > &v)
Definition: Sort.h:91
template<class T >
void Minisat::sort ( vec< T > &  v)

Definition at line 91 of file Sort.h.

91  {
92  sort(v, LessThan_default<T>()); }
Minisat::sort
void sort(vec< T > &v)
Definition: Sort.h:91
int Minisat::toInt ( Var  v)
inline

Definition at line 65 of file SolverTypes.h.

65 { return v; }
int Minisat::toInt ( Lit  p)
inline

Definition at line 66 of file SolverTypes.h.

66 { return p.x; }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Minisat::toInt ( lbool  l)
inline

Definition at line 114 of file SolverTypes.h.

114 { return l.value; }
lbool Minisat::toLbool ( int  v)
inline

Definition at line 115 of file SolverTypes.h.

115 { return lbool((uint8_t)v); }
lbool
char lbool
Definition: satVec.h:133
Lit Minisat::toLit ( int  i)
inline

Definition at line 67 of file SolverTypes.h.

67 { Lit p; p.x = i; return p; }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Minisat::var ( Lit  p)
inline

Definition at line 62 of file SolverTypes.h.

62 { return p.x >> 1; }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void* Minisat::xrealloc ( void *  ptr,
size_t  size 
)
inlinestatic

Definition at line 33 of file XAlloc.h.

34 {
35  void* mem = realloc(ptr, size);
36  if (mem == NULL && errno == ENOMEM){
37  throw OutOfMemoryException();
38  }else
39  return mem;
40 }
realloc
char * realloc()
size
static int size
Definition: cuddSign.c:86

Variable Documentation

const int Minisat::buffer_size = 1048576
static

Definition at line 34 of file ParseUtils.h.

const CRef Minisat::CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef

Definition at line 193 of file SolverTypes.h.

const Lit Minisat::lit_Error = { -1 }

Definition at line 73 of file SolverTypes.h.

const Lit Minisat::lit_Undef = { -2 }

Definition at line 72 of file SolverTypes.h.

const int Minisat::nprimes = 25
static

Definition at line 48 of file Map.h.

const int Minisat::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 }
static

Definition at line 49 of file Map.h.