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);
Var()39 Var() : d_index(-1) {}
Var(int index)40 Var(int index) :d_index(index) {}
41 operator int() { return d_index; }
isNull()42 bool isNull() const { return d_index == -1; }
reset()43 void reset() { d_index = -1; }
getIndex()44 int getIndex() const { return d_index; }
isVar()45 bool isVar() const { return d_index > 0; }
46 bool operator==(const Var& var) const { return (d_index == var.d_index); }
47 };
invertValue(Var::Val v)48 inline Var::Val Var::invertValue(Var::Val v)
49 { return v == Var::UNKNOWN ? Var::UNKNOWN : Var::Val(1-v); }
50
51 class Lit {
52 int d_index;
mkLit(int index)53 static Lit mkLit(int index) { Lit l; l.d_index = index; return l; }
54 public:
Lit()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 }
getTrue()60 static Lit getTrue() { return mkLit(1); }
getFalse()61 static Lit getFalse() { return mkLit(-1); }
62
isNull()63 bool isNull() const { return d_index == 0; }
isPositive()64 bool isPositive() const { return d_index > 1; }
isInverted()65 bool isInverted() const { return d_index < -1; }
isFalse()66 bool isFalse() const { return d_index == -1; }
isTrue()67 bool isTrue() const { return d_index == 1; }
isVar()68 bool isVar() const { return abs(d_index) > 1; }
getID()69 int getID() const { return d_index; }
getVar()70 Var getVar() const {
71 DebugAssert(isVar(),"Bad call to Lit::getVar");
72 return abs(d_index)-1;
73 }
reset()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
Clause()86 Clause(): d_satisfied(0), d_unit(0) { };
87
Clause(const Clause & clause)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;
begin()93 const_iterator begin() const { return d_lits.begin(); }
end()94 const_iterator end() const { return d_lits.end(); }
95
clear()96 void clear() { d_satisfied = d_unit = 0; d_lits.clear(); }
size()97 unsigned size() const { return d_lits.size(); }
addLiteral(Lit l)98 void addLiteral(Lit l) { if (!d_satisfied) d_lits.push_back(l); }
99 unsigned getMaxVar() const;
isSatisfied()100 bool isSatisfied() const { return d_satisfied != 0; }
isUnit()101 bool isUnit() const { return d_unit != 0; }
isNull()102 bool isNull() const { return d_lits.size() == 0; }
setSatisfied()103 void setSatisfied() { d_satisfied = 1; }
setUnit()104 void setUnit() { d_unit = 1; }
105 void print() const;
setClauseTheorem(CVC3::Theorem thm)106 void setClauseTheorem(CVC3::Theorem thm){ d_reason = thm;}
107
getClauseTheorem()108 CVC3::Theorem getClauseTheorem() const { return d_reason;}
109 };
110
111
112 class CNF_Formula {
113 protected:
114 Clause* d_current;
115
116 virtual void setNumVars(unsigned numVars) = 0;
117 void copy(const CNF_Formula& cnf);
118
119 public:
CNF_Formula()120 CNF_Formula() : d_current(NULL) {}
~CNF_Formula()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); }
getCurrentClause()138 Clause& getCurrentClause() { return *d_current; }
139 void print() const;
140 const CNF_Formula& operator+=(const CNF_Formula& cnf);
141 const CNF_Formula& operator+=(const Clause& c);
142 };
143
144
145 class CNF_Formula_Impl :public CNF_Formula {
146 std::hash_map<int, bool> d_lits;
147 std::deque<Clause> d_formula;
148 unsigned d_numVars;
149 private:
setNumVars(unsigned numVars)150 void setNumVars(unsigned numVars) { d_numVars = numVars; }
151 public:
CNF_Formula_Impl()152 CNF_Formula_Impl() : CNF_Formula(), d_numVars(0) {}
CNF_Formula_Impl(const CNF_Formula & cnf)153 CNF_Formula_Impl(const CNF_Formula& cnf) : CNF_Formula() { copy(cnf); }
~CNF_Formula_Impl()154 ~CNF_Formula_Impl() {};
155
empty()156 bool empty() const { return d_formula.empty(); }
157 const Clause& operator[](int i) const { return d_formula[i]; }
begin()158 const_iterator begin() const { return d_formula.begin(); }
end()159 const_iterator end() const { return d_formula.end(); }
numVars()160 unsigned numVars() const { return d_numVars; }
numClauses()161 unsigned numClauses() const { return d_formula.size(); }
deleteLast()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
171 class CD_CNF_Formula :public CNF_Formula {
172 CVC3::CDList<Clause> d_formula;
173 CVC3::CDO<unsigned> d_numVars;
174 private:
setNumVars(unsigned numVars)175 void setNumVars(unsigned numVars) { d_numVars = numVars; }
176 public:
CD_CNF_Formula(CVC3::Context * context)177 CD_CNF_Formula(CVC3::Context* context)
178 : CNF_Formula(), d_formula(context), d_numVars(context, 0, 0) {}
~CD_CNF_Formula()179 ~CD_CNF_Formula() {}
180
empty()181 bool empty() const { return d_formula.empty(); }
182 const Clause& operator[](int i) const { return d_formula[i]; }
begin()183 const_iterator begin() const { return d_formula.begin(); }
end()184 const_iterator end() const { return d_formula.end(); }
numVars()185 unsigned numVars() const { return d_numVars.get(); }
numClauses()186 unsigned numClauses() const { return d_formula.size(); }
deleteLast()187 void deleteLast() { d_formula.pop_back(); }
188
189 void newClause();
190 void registerUnit();
191 };
192
193 }
194
195 #endif
196