00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021 #ifndef _cvc3__include__cnf_h_
00022 #define _cvc3__include__cnf_h_
00023
00024 #include <deque>
00025 #include "compat_hash_map.h"
00026 #include "cvc_util.h"
00027 #include "cdo.h"
00028 #include "cdlist.h"
00029
00030 namespace SAT {
00031
00032 class Var {
00033 int d_index;
00034 public:
00035 enum Val { UNKNOWN = -1, FALSE_VAL, TRUE_VAL};
00036 static Val invertValue(Val);
00037 Var() : d_index(-1) {}
00038 Var(int index) :d_index(index) {}
00039 operator int() { return d_index; }
00040 bool isNull() const { return d_index == -1; }
00041 void reset() { d_index = -1; }
00042 int getIndex() const { return d_index; }
00043 bool operator==(const Var& var) const { return (d_index == var.d_index); }
00044 };
00045 inline Var::Val Var::invertValue(Var::Val v)
00046 { return v == Var::UNKNOWN ? Var::UNKNOWN : Var::Val(1-v); }
00047
00048 class Lit {
00049 int d_index;
00050 static Lit mkLit(int index) { Lit l; l.d_index = index; return l; }
00051 public:
00052 Lit() : d_index(0) {}
00053 explicit Lit(Var v, bool positive=true) {
00054 if (v.isNull()) d_index = 0;
00055 else d_index = positive ? v+1 : -v-1;
00056 }
00057 static Lit getTrue() { return mkLit(1); }
00058 static Lit getFalse() { return mkLit(-1); }
00059
00060 bool isNull() const { return d_index == 0; }
00061 bool isPositive() const { return d_index > 1; }
00062 bool isInverted() const { return d_index < -1; }
00063 bool isFalse() const { return d_index == -1; }
00064 bool isTrue() const { return d_index == 1; }
00065 bool isVar() const { return abs(d_index) > 1; }
00066 int getID() const { return d_index; }
00067 Var getVar() const {
00068 DebugAssert(isVar(),"Bad call to Lit::getVar");
00069 return abs(d_index)-1;
00070 }
00071 void reset() { d_index = 0; }
00072 friend Lit operator!(const Lit& lit) { return mkLit(-lit.d_index); }
00073 };
00074
00075 class Clause {
00076
00077
00078
00079 int d_id:30;
00080 int d_satisfied:1;
00081 int d_unit:1;
00082 std::vector<Lit> d_lits;
00083 public:
00084 Clause() : d_id(0), d_satisfied(0), d_unit(0) {}
00085
00086 typedef std::vector<Lit>::const_iterator const_iterator;
00087 const_iterator begin() const { return d_lits.begin(); }
00088 const_iterator end() const { return d_lits.end(); }
00089
00090 void clear() { d_id = d_satisfied = d_unit = 0; d_lits.clear(); }
00091 unsigned size() const { return d_lits.size(); }
00092 void addLiteral(Lit l) { if (!d_satisfied) d_lits.push_back(l); }
00093 unsigned getMaxVar() const;
00094
00095 int getId() const { return d_id; }
00096 bool isSatisfied() const { return d_satisfied != 0; }
00097 bool isUnit() const { return d_unit != 0; }
00098 bool isNull() const { return d_lits.size() == 0; }
00099 void setId(int id)
00100 { d_id = id; FatalAssert(int(d_id) == id, "clause id overflow"); }
00101 void setSatisfied() { d_satisfied = 1; }
00102 void setUnit() { d_unit = 1; }
00103 void print() const;
00104 };
00105
00106
00107 class CNF_Formula {
00108 protected:
00109 Clause* d_current;
00110
00111 virtual void setNumVars(unsigned numVars) = 0;
00112 void copy(const CNF_Formula& cnf);
00113
00114 public:
00115 CNF_Formula() : d_current(NULL) {}
00116 virtual ~CNF_Formula() {}
00117
00118 typedef std::deque<Clause>::const_iterator const_iterator;
00119
00120 virtual bool empty() const = 0;
00121 virtual const Clause& operator[](int i) const = 0;
00122 virtual const_iterator begin() const = 0;
00123 virtual const_iterator end() const = 0;
00124 virtual unsigned numVars() const = 0;
00125 virtual unsigned numClauses() const = 0;
00126 virtual void newClause() = 0;
00127 virtual void registerUnit() = 0;
00128
00129 void addLiteral(Lit l, bool invert=false)
00130 { if (l.isVar() && unsigned(l.getVar()) > numVars())
00131 setNumVars(l.getVar());
00132 d_current->addLiteral(invert ? !l : l); }
00133 Clause& getCurrentClause() { return *d_current; }
00134 void print() const;
00135 const CNF_Formula& operator+=(const CNF_Formula& cnf);
00136 const CNF_Formula& operator+=(const Clause& c);
00137 };
00138
00139
00140 class CNF_Formula_Impl :public CNF_Formula {
00141 std::hash_map<int, bool> d_lits;
00142 std::deque<Clause> d_formula;
00143 unsigned d_numVars;
00144 private:
00145 void setNumVars(unsigned numVars) { d_numVars = numVars; }
00146 public:
00147 CNF_Formula_Impl() : CNF_Formula(), d_numVars(0) {}
00148 CNF_Formula_Impl(const CNF_Formula& cnf) : CNF_Formula() { copy(cnf); }
00149 ~CNF_Formula_Impl() {};
00150
00151 bool empty() const { return d_formula.empty(); }
00152 const Clause& operator[](int i) const { return d_formula[i]; }
00153 const_iterator begin() const { return d_formula.begin(); }
00154 const_iterator end() const { return d_formula.end(); }
00155 unsigned numVars() const { return d_numVars; }
00156 unsigned numClauses() const { return d_formula.size(); }
00157 void deleteLast() { DebugAssert(d_formula.size() > 0, "size == 0"); d_formula.pop_back(); }
00158 void newClause();
00159 void registerUnit();
00160
00161 void simplify();
00162 void reset();
00163 };
00164
00165
00166 class CD_CNF_Formula :public CNF_Formula {
00167 CVC3::CDList<Clause> d_formula;
00168 CVC3::CDO<unsigned> d_numVars;
00169 private:
00170 void setNumVars(unsigned numVars) { d_numVars = numVars; }
00171 public:
00172 CD_CNF_Formula(CVC3::Context* context)
00173 : CNF_Formula(), d_formula(context), d_numVars(context, 0, 0) {}
00174 ~CD_CNF_Formula() {}
00175
00176 bool empty() const { return d_formula.empty(); }
00177 const Clause& operator[](int i) const { return d_formula[i]; }
00178 const_iterator begin() const { return d_formula.begin(); }
00179 const_iterator end() const { return d_formula.end(); }
00180 unsigned numVars() const { return d_numVars.get(); }
00181 unsigned numClauses() const { return d_formula.size(); }
00182 void deleteLast() { d_formula.pop_back(); }
00183
00184 void newClause();
00185 void registerUnit();
00186 };
00187
00188 }
00189
00190 #endif