cnf_manager.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file cnf_manager.h
00004  *\brief Manager for conversion to and traversal of CNF formulas
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Thu Dec 15 13:53:16 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_manager_h_
00022 #define _cvc3__include__cnf_manager_h_
00023 
00024 #include "cnf.h"
00025 #include "expr.h"
00026 #include "expr_map.h"
00027 #include "cdmap.h"
00028 #include "statistics.h"
00029 
00030 namespace CVC3 {
00031 
00032 class CommonProofRules;
00033 class CNF_Rules;
00034 class ValidityChecker;
00035 class Statistics;
00036 
00037 }
00038 
00039 namespace SAT {
00040 
00041 class CNF_Manager {
00042 
00043   //! For clause minimization
00044   CVC3::ValidityChecker* d_vc;
00045 
00046   //! Whether to use brute-force clause minimization
00047   bool d_minimizeClauses;
00048 
00049   //! Common proof rules
00050   CVC3::CommonProofRules* d_commonRules;
00051 
00052   //! Rules for manipulating CNF
00053   CVC3::CNF_Rules* d_rules;
00054 
00055   //! Information kept for each CNF variable
00056   struct Varinfo {
00057     CVC3::Expr expr;
00058     std::vector<Lit> fanins;
00059     std::vector<Var> fanouts;
00060   };
00061 
00062   //! vector that maps a variable index to information for that variable
00063   std::vector<Varinfo> d_varInfo;
00064 
00065   //! Map from Exprs to Vars representing those Exprs
00066   CVC3::ExprMap<Var> d_cnfVars;
00067 
00068   //! Cached translation of term-ite-containing expressions
00069   CVC3::ExprMap<CVC3::Theorem> d_iteMap;
00070 
00071   //! Maps a clause id to the theorem justifying that clause
00072   /*! Note that clauses created by simple CNF translation are not given id's.
00073    *  This is because theorems for these clauses can be created lazily later. */
00074   //  CVC3::CDMap<int, CVC3::Theorem> d_theorems;
00075 
00076   //! Next clause id
00077   int d_clauseIdNext;
00078 
00079   //! Whether expr has already been translated
00080   //  CVC3::CDMap<CVC3::Expr, bool> d_translated;
00081 
00082   //! Bottom scope in which translation is valid
00083   int d_bottomScope;
00084 
00085   //! Queue of theorems to translate
00086   std::deque<CVC3::Theorem> d_translateQueueThms;
00087 
00088   //! Queue of fanouts corresponding to thms to translate
00089   std::deque<Var> d_translateQueueVars;
00090 
00091   //! Whether thm to translate is "translate only"
00092   std::deque<bool> d_translateQueueFlags;
00093 
00094   //! Reference to statistics object
00095   CVC3::Statistics& d_statistics;
00096 
00097 public:
00098   //! Abstract class for callbacks
00099   class CNFCallback {
00100   public:
00101     CNFCallback() {}
00102     virtual ~CNFCallback() {}
00103     //! Register an atom
00104     virtual void registerAtom(const CVC3::Expr& e,
00105                               const CVC3::Theorem& thm) = 0;
00106   };
00107 
00108 private:
00109   //! Instance of CNF_CallBack: must be registered
00110   CNFCallback* d_cnfCallback;
00111 
00112   CVC3::CNF_Rules* createProofRules(CVC3::TheoremManager* tm);
00113 
00114   //! Register a new atomic formula
00115   void registerAtom(const CVC3::Expr& e, const CVC3::Theorem& thm);
00116 
00117   //! Recursively translate e into cnf
00118   /*! A non-context dependent cache, d_cnfVars is used to remember translations
00119    * of expressions.  A context-dependent attribute, isTranslated, is used to
00120    * remember whether an expression has been translated in the current context */
00121   Lit translateExprRec(const CVC3::Expr& e, CNF_Formula& cnf,
00122                        const CVC3::Theorem& thmIn);
00123 
00124   //! Recursively traverse an expression with an embedded term ITE
00125   /*! Term ITE's are handled by introducing a skolem variable for the ITE term
00126    * and then adding new constraints describing the ITE in terms of the new variable.
00127    */
00128   CVC3::Theorem replaceITErec(const CVC3::Expr& e, Var v, bool translateOnly);
00129 
00130   //! Recursively translate e into cnf
00131   /*! Call translateExprRec.  If additional expressions are queued up,
00132    * translate them too, until none are left. */
00133   Lit translateExpr(const CVC3::Theorem& thmIn, CNF_Formula& cnf);
00134 
00135 //   bool isTranslated(const CVC3::Expr& e)
00136 //     { CVC3::CDMap<CVC3::Expr, bool>::iterator i = d_translated.find(e);
00137 //       return i != d_translated.end() && (*i).second; }
00138 //   void setTranslated(const CVC3::Expr& e)
00139 //     { DebugAssert(!isTranslated(e),"already set");
00140 //       d_translated.insert(e, true, d_bottomScope); }
00141 //   void clearTranslated(const CVC3::Expr& e)
00142 //     { d_translated.insert(e, false, d_bottomScope); }
00143 
00144 public:
00145   CNF_Manager(CVC3::TheoremManager* tm, CVC3::Statistics& statistics, bool minimizeClauses);
00146   ~CNF_Manager();
00147 
00148   //! Register CNF callback
00149   void registerCNFCallback(CNFCallback* cnfCallback)
00150     { d_cnfCallback = cnfCallback; }
00151 
00152   //! Set scope for translation
00153   void setBottomScope(int scope) { d_bottomScope = scope; }
00154 
00155   //! Return the number of variables being managed
00156   unsigned numVars() { return d_varInfo.size(); }
00157 
00158   //! Return number of fanins for CNF node c
00159   /*! A CNF node x is a fanin of CNF node y if the expr for x is a child of the
00160    *  expr for y or if y is an ITE leaf and x is a new CNF node obtained by
00161    *  translating the ITE leaf y.
00162    *  \sa isITELeaf()
00163    */
00164   unsigned numFanins(Lit c) {
00165     if (!c.isVar()) return 0;
00166     int index = c.getVar();
00167     if ((unsigned)index >= d_varInfo.size()) return 0;
00168     return d_varInfo[index].fanins.size();
00169   }
00170 
00171   //! Returns the ith fanin of c.
00172   Lit getFanin(Lit c, unsigned i) {
00173     DebugAssert(i < numFanins(c), "attempt to access unknown fanin");
00174     return d_varInfo[c.getVar()].fanins[i];
00175   }
00176 
00177   //! Return number of fanins for c
00178   /*! x is a fanout of y if y is a fanin of x
00179    *  \sa numFanins
00180    */
00181   unsigned numFanouts(Lit c) {
00182     if (!c.isVar()) return 0;
00183     int index = c.getVar();
00184     if ((unsigned)index >= d_varInfo.size()) return 0;
00185     return d_varInfo[index].fanouts.size();
00186   }
00187 
00188   //! Returns the ith fanout of c.
00189   Lit getFanout(Lit c, unsigned i) {
00190     DebugAssert(i < numFanouts(c), "attempt to access unknown fanin");
00191     return Lit(d_varInfo[c.getVar()].fanouts[i]);
00192   }
00193 
00194   //! Convert a CNF literal to an Expr literal
00195   /*! Returns a NULL Expr if there is no corresponding Expr for l
00196    */
00197   CVC3::Expr concreteLit(Lit l, bool checkTranslated = true) {
00198     if (l.isNull()) return CVC3::Expr();
00199     bool inverted = !l.isPositive();
00200     int index = l.getVar();
00201     if ((unsigned)index >= d_varInfo.size() ||
00202         (checkTranslated && !d_varInfo[index].expr.isTranslated()))
00203       return CVC3::Expr();
00204     return inverted ? !d_varInfo[index].expr : d_varInfo[index].expr;
00205   }
00206 
00207   //! Look up the CNF literal for an Expr
00208   /*! Returns a NULL Lit if there is no corresponding CNF literal for e
00209    */
00210   Lit getCNFLit(const CVC3::Expr& e) {
00211     if (e.isFalse()) return Lit::getFalse();
00212     if (e.isTrue()) return Lit::getTrue();
00213     if (e.isNot()) return !getCNFLit(e[0]);
00214     CVC3::ExprMap<Var>::iterator i = d_cnfVars.find(e);
00215     if (!e.isTranslated() || i == d_cnfVars.end()) return Lit();
00216     return Lit((*i).second);
00217   }
00218 
00219   void cons(unsigned lb, unsigned ub, const CVC3::Expr& e2, std::vector<unsigned>& newLits);
00220 
00221   //! Convert thm A |- B (A is a set of literals) into a clause ~A \/ B
00222   /*! c should be an empty clause that will be filled with the result */
00223   void convertLemma(const CVC3::Theorem& thm, Clause& c);
00224 
00225   //! Given thm of form A |- B, convert B to CNF and add it to cnf
00226   /*! Returns Lit corresponding to the root of the expression that was
00227    * translated. */
00228   Lit addAssumption(const CVC3::Theorem& thm, CNF_Formula& cnf);
00229 
00230   //! Convert thm to CNF and add it to the current formula
00231   /*! \param thm should be of form A |- B where A is a set of literals.
00232    * \param cnf the new clauses are added to cnf.
00233    * Returns Lit corresponding to the root of the expression that was
00234    * translated. */
00235   Lit addLemma(const CVC3::Theorem& thm, CNF_Formula& cnf);
00236 
00237 };
00238 
00239 }
00240 
00241 #endif

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