CVC3
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;
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:
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(); }
188 
189  void newClause();
190  void registerUnit();
191 };
192 
193 }
194 
195 #endif