# cnf.h

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

Generated on Thu Apr 13 16:57:30 2006 for CVC Lite by  1.4.4