CVC3

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