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  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
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   /*! If d_id is 0 then the clause is a translation clause and its theorem
00077    *  can be figured out lazily.  Otherwise, d_id gives the index into
00078    *  d_theorems for the theorem justifying this clause. */
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

Generated on Tue Jul 3 14:33:35 2007 for CVC3 by  doxygen 1.5.1