CVC3  2.4.1
cnf.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file cnf.h
4  *\brief Basic classes for reasoning about formulas in CNF
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Mon Dec 12 20:32:33 2005
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__cnf_h_
22 #define _cvc3__include__cnf_h_
23 
24 #include <deque>
25 #include "compat_hash_map.h"
26 #include "cvc_util.h"
27 #include "cdo.h"
28 #include "cdlist.h"
29 #include "theorem.h"
30 
31 
32 namespace SAT {
33 
34 class Var {
35  int d_index;
36 public:
37  enum Val { UNKNOWN = -1, FALSE_VAL, TRUE_VAL};
38  static Val invertValue(Val);
39  Var() : d_index(-1) {}
40  Var(int index) :d_index(index) {}
41  operator int() { return d_index; }
42  bool isNull() const { return d_index == -1; }
43  void reset() { d_index = -1; }
44  int getIndex() const { return d_index; }
45  bool isVar() const { return d_index > 0; }
46  bool operator==(const Var& var) const { return (d_index == var.d_index); }
47 };
49 { return v == Var::UNKNOWN ? Var::UNKNOWN : Var::Val(1-v); }
50 
51 class Lit {
52  int d_index;
53  static Lit mkLit(int index) { Lit l; l.d_index = index; return l; }
54 public:
55  Lit() : d_index(0) {}
56  explicit Lit(Var v, bool positive=true) {
57  if (v.isNull()) d_index = 0;
58  else d_index = positive ? v+1 : -v-1;
59  }
60  static Lit getTrue() { return mkLit(1); }
61  static Lit getFalse() { return mkLit(-1); }
62 
63  bool isNull() const { return d_index == 0; }
64  bool isPositive() const { return d_index > 1; }
65  bool isInverted() const { return d_index < -1; }
66  bool isFalse() const { return d_index == -1; }
67  bool isTrue() const { return d_index == 1; }
68  bool isVar() const { return abs(d_index) > 1; }
69  int getID() const { return d_index; }
70  Var getVar() const {
71  DebugAssert(isVar(),"Bad call to Lit::getVar");
72  return abs(d_index)-1;
73  }
74  void reset() { d_index = 0; }
75  friend Lit operator!(const Lit& lit) { return mkLit(-lit.d_index); }
76 };
77 
78 class Clause {
79  int d_satisfied:1;
80  int d_unit:1;
81  std::vector<Lit> d_lits;
82  CVC3::Theorem d_reason; //the theorem for the clause, used in proofs. by yeting
83 
84  public:
85 
86  Clause(): d_satisfied(0), d_unit(0) { };
87 
88  Clause(const Clause& clause)
89  : d_satisfied(clause.d_satisfied), d_unit(clause.d_unit),
90  d_lits(clause.d_lits), d_reason(clause.d_reason) { };
91 
92  typedef std::vector<Lit>::const_iterator const_iterator;
93  const_iterator begin() const { return d_lits.begin(); }
94  const_iterator end() const { return d_lits.end(); }
95 
96  void clear() { d_satisfied = d_unit = 0; d_lits.clear(); }
97  unsigned size() const { return d_lits.size(); }
98  void addLiteral(Lit l) { if (!d_satisfied) d_lits.push_back(l); }
99  unsigned getMaxVar() const;
100  bool isSatisfied() const { return d_satisfied != 0; }
101  bool isUnit() const { return d_unit != 0; }
102  bool isNull() const { return d_lits.size() == 0; }
103  void setSatisfied() { d_satisfied = 1; }
104  void setUnit() { d_unit = 1; }
105  void print() const;
106  void setClauseTheorem(CVC3::Theorem thm){ d_reason = thm;}
107 
109 };
110 
111 
112 class CNF_Formula {
113 protected:
115 
116  virtual void setNumVars(unsigned numVars) = 0;
117  void copy(const CNF_Formula& cnf);
118 
119 public:
120  CNF_Formula() : d_current(NULL) {}
121  virtual ~CNF_Formula() {}
122 
123  typedef std::deque<Clause>::const_iterator const_iterator;
124 
125  virtual bool empty() const = 0;
126  virtual const Clause& operator[](int i) const = 0;
127  virtual const_iterator begin() const = 0;
128  virtual const_iterator end() const = 0;
129  virtual unsigned numVars() const = 0;
130  virtual unsigned numClauses() const = 0;
131  virtual void newClause() = 0;
132  virtual void registerUnit() = 0;
133 
134  void addLiteral(Lit l, bool invert=false)
135  { if (l.isVar() && unsigned(l.getVar()) > numVars())
136  setNumVars(l.getVar());
137  d_current->addLiteral(invert ? !l : l); }
139  void print() const;
140  const CNF_Formula& operator+=(const CNF_Formula& cnf);
141  const CNF_Formula& operator+=(const Clause& c);
142 };
143 
144 
147  std::deque<Clause> d_formula;
148  unsigned d_numVars;
149 private:
150  void setNumVars(unsigned numVars) { d_numVars = numVars; }
151 public:
152  CNF_Formula_Impl() : CNF_Formula(), d_numVars(0) {}
153  CNF_Formula_Impl(const CNF_Formula& cnf) : CNF_Formula() { copy(cnf); }
155 
156  bool empty() const { return d_formula.empty(); }
157  const Clause& operator[](int i) const { return d_formula[i]; }
158  const_iterator begin() const { return d_formula.begin(); }
159  const_iterator end() const { return d_formula.end(); }
160  unsigned numVars() const { return d_numVars; }
161  unsigned numClauses() const { return d_formula.size(); }
162  void deleteLast() { DebugAssert(d_formula.size() > 0, "size == 0"); d_formula.pop_back(); }
163  void newClause();
164  void registerUnit();
165 
166  void simplify();
167  void reset();
168 };
169 
170 
174 private:
175  void setNumVars(unsigned numVars) { d_numVars = numVars; }
176 public:
178  : CNF_Formula(), d_formula(context), d_numVars(context, 0, 0) {}
180 
181  bool empty() const { return d_formula.empty(); }
182  const Clause& operator[](int i) const { return d_formula[i]; }
183  const_iterator begin() const { return d_formula.begin(); }
184  const_iterator end() const { return d_formula.end(); }
185  unsigned numVars() const { return d_numVars.get(); }
186  unsigned numClauses() const { return d_formula.size(); }
187  void deleteLast() { d_formula.pop_back(); }
188 
189  void newClause();
190  void registerUnit();
191 };
192 
193 }
194 
195 #endif
static Lit getTrue()
Definition: cnf.h:60
void reset()
Definition: cnf.h:43
basic helper utilities
void setNumVars(unsigned numVars)
Definition: cnf.h:175
void registerUnit()
Definition: cnf.cpp:190
const_iterator begin() const
Definition: cnf.h:93
unsigned getMaxVar() const
Definition: cnf.cpp:30
unsigned numClauses() const
Definition: cnf.h:161
const_iterator begin() const
Definition: cnf.h:158
CD_CNF_Formula(CVC3::Context *context)
Definition: cnf.h:177
void print() const
Definition: cnf.cpp:42
bool operator==(const Var &var) const
Definition: cnf.h:46
int getIndex() const
Definition: cnf.h:44
void deleteLast()
Definition: cnf.h:162
const_iterator end() const
Definition: cnf.h:159
Clause(const Clause &clause)
Definition: cnf.h:88
std::vector< Lit > d_lits
Definition: cnf.h:81
const Clause & operator[](int i) const
Definition: cnf.h:182
bool isInverted() const
Definition: cnf.h:65
unsigned numVars() const
Definition: cnf.h:185
void reset()
Definition: cnf.h:74
virtual unsigned numClauses() const =0
int getID() const
Definition: cnf.h:69
void setClauseTheorem(CVC3::Theorem thm)
Definition: cnf.h:106
CVC3::CDList< Clause > d_formula
Definition: cnf.h:172
bool empty() const
Definition: cdlist.h:65
bool isVar() const
Definition: cnf.h:68
std::deque< Clause >::const_iterator const_iterator
Definition: cnf.h:123
bool isNull() const
Definition: cnf.h:63
virtual void newClause()=0
void print() const
Definition: cnf.cpp:85
unsigned size() const
Definition: cnf.h:97
void setSatisfied()
Definition: cnf.h:103
const_iterator begin() const
Definition: cnf.h:183
unsigned numVars() const
Definition: cnf.h:160
#define DebugAssert(cond, str)
Definition: debug.h:408
CVC3::Theorem d_reason
Definition: cnf.h:82
int d_unit
Definition: cnf.h:80
static Lit mkLit(int index)
Definition: cnf.h:53
static Lit getFalse()
Definition: cnf.h:61
void deleteLast()
Definition: cnf.h:187
void setUnit()
Definition: cnf.h:104
virtual const Clause & operator[](int i) const =0
void newClause()
Definition: cnf.cpp:183
Var(int index)
Definition: cnf.h:40
bool isTrue() const
Definition: cnf.h:67
CVC3::Theorem getClauseTheorem() const
Definition: cnf.h:108
const_iterator end() const
Definition: cdlist.h:91
Clause * d_current
Definition: cnf.h:114
CNF_Formula_Impl(const CNF_Formula &cnf)
Definition: cnf.h:153
friend Lit operator!(const Lit &lit)
Definition: cnf.h:75
int d_index
Definition: cnf.h:52
virtual unsigned numVars() const =0
void copy(const CNF_Formula &cnf)
Definition: cnf.cpp:60
bool empty() const
Definition: cnf.h:181
void pop_back()
Definition: cdlist.h:68
unsigned d_numVars
Definition: cnf.h:148
bool empty() const
Definition: cnf.h:156
bool isVar() const
Definition: cnf.h:45
T abs(T t)
Definition: cvc_util.h:53
Val
Definition: cnf.h:37
void setNumVars(unsigned numVars)
Definition: cnf.h:150
void addLiteral(Lit l, bool invert=false)
Definition: cnf.h:134
Definition: cnf.h:51
virtual void setNumVars(unsigned numVars)=0
int d_index
Definition: cnf.h:35
void clear()
Definition: cnf.h:96
unsigned size() const
Definition: cdlist.h:64
Clause()
Definition: cnf.h:86
const T & get() const
Definition: cdo.h:64
const_iterator end() const
Definition: cnf.h:94
std::vector< Lit >::const_iterator const_iterator
Definition: cnf.h:90
int d_satisfied
Definition: cnf.h:79
Var()
Definition: cnf.h:39
const CNF_Formula & operator+=(const CNF_Formula &cnf)
Definition: cnf.cpp:94
virtual ~CNF_Formula()
Definition: cnf.h:121
virtual const_iterator begin() const =0
Definition: cnf.h:32
const_iterator end() const
Definition: cnf.h:184
virtual bool empty() const =0
Var getVar() const
Definition: cnf.h:70
void addLiteral(Lit l)
Definition: cnf.h:98
bool isNull() const
Definition: cnf.h:42
bool isSatisfied() const
Definition: cnf.h:100
const_iterator begin() const
Definition: cdlist.h:88
bool isUnit() const
Definition: cnf.h:101
Lit()
Definition: cnf.h:55
virtual const_iterator end() const =0
const Clause & operator[](int i) const
Definition: cnf.h:157
void registerUnit()
Definition: cnf.cpp:144
bool isPositive() const
Definition: cnf.h:64
static Val invertValue(Val)
Definition: cnf.h:48
Clause & getCurrentClause()
Definition: cnf.h:138
bool isNull() const
Definition: cnf.h:102
unsigned numClauses() const
Definition: cnf.h:186
Lit(Var v, bool positive=true)
Definition: cnf.h:56
std::deque< Clause > d_formula
Definition: cnf.h:147
bool isFalse() const
Definition: cnf.h:66
CVC3::CDO< unsigned > d_numVars
Definition: cnf.h:173
std::hash_map< int, bool > d_lits
Definition: cnf.h:146
Definition: cnf.h:34
virtual void registerUnit()=0