CVC3

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::ExprHashMap<Var> d_cnfVars;
00067 
00068   //! Cached translation of term-ite-containing expressions
00069   CVC3::ExprHashMap<CVC3::Theorem> d_iteMap;
00070 
00071   //! Map of possibly useful lemmas
00072   //  CVC3::ExprMap<int> d_usefulLemmas;
00073 
00074   //! Maps a clause id to the theorem justifying that clause
00075   /*! Note that clauses created by simple CNF translation are not given id's.
00076    *  This is because theorems for these clauses can be created lazily later. */
00077   //  CVC3::CDMap<int, CVC3::Theorem> d_theorems;
00078   //  CVC3::CDMap<int, CVC3::Theorem> d_theorems;
00079 
00080   //! Next clause id
00081   int d_clauseIdNext;
00082 
00083   //! Whether expr has already been translated
00084   //  CVC3::CDMap<CVC3::Expr, bool> d_translated;
00085 
00086   //! Bottom scope in which translation is valid
00087   int d_bottomScope;
00088 
00089   //! Queue of theorems to translate
00090   std::deque<CVC3::Theorem> d_translateQueueThms;
00091 
00092   //! Queue of fanouts corresponding to thms to translate
00093   std::deque<Var> d_translateQueueVars;
00094 
00095   //! Whether thm to translate is "translate only"
00096   std::deque<bool> d_translateQueueFlags;
00097 
00098   //! Reference to statistics object
00099   CVC3::Statistics& d_statistics;
00100 
00101   //! Reference to command-line flags
00102   const CVC3::CLFlags& d_flags;
00103 
00104   //! Reference to null Expr
00105   const CVC3::Expr& d_nullExpr;
00106 
00107 public:
00108   //! Abstract class for callbacks
00109   class CNFCallback {
00110   public:
00111     CNFCallback() {}
00112     virtual ~CNFCallback() {}
00113     //! Register an atom
00114     virtual void registerAtom(const CVC3::Expr& e,
00115                               const CVC3::Theorem& thm) = 0;
00116   };
00117 
00118 private:
00119   //! Instance of CNF_CallBack: must be registered
00120   CNFCallback* d_cnfCallback;
00121 
00122   CVC3::CNF_Rules* createProofRules(CVC3::TheoremManager* tm, const CVC3::CLFlags&);
00123 
00124   //! Register a new atomic formula
00125   void registerAtom(const CVC3::Expr& e, const CVC3::Theorem& thm);
00126 
00127   //! Return the expr corresponding to the literal unless the expr is TRUE of FALSE
00128   CVC3::Expr concreteExpr(const CVC3::Expr& e, const Lit& literal);
00129 
00130   //! Return the theorem if e is not as concreteExpr(e).
00131   CVC3::Theorem concreteThm(const CVC3::Expr& e);
00132 
00133   //! Recursively translate e into cnf
00134   /*! A non-context dependent cache, d_cnfVars is used to remember translations
00135    * of expressions.  A context-dependent attribute, isTranslated, is used to
00136    * remember whether an expression has been translated in the current context */
00137   Lit translateExprRec(const CVC3::Expr& e, CNF_Formula& cnf,
00138                        const CVC3::Theorem& thmIn);
00139 
00140   //! Recursively traverse an expression with an embedded term ITE
00141   /*! Term ITE's are handled by introducing a skolem variable for the ITE term
00142    * and then adding new constraints describing the ITE in terms of the new variable.
00143    */
00144   CVC3::Theorem replaceITErec(const CVC3::Expr& e, Var v, bool translateOnly);
00145 
00146   //! Recursively translate e into cnf
00147   /*! Call translateExprRec.  If additional expressions are queued up,
00148    * translate them too, until none are left. */
00149   Lit translateExpr(const CVC3::Theorem& thmIn, CNF_Formula& cnf);
00150 
00151 //   bool isTranslated(const CVC3::Expr& e)
00152 //     { CVC3::CDMap<CVC3::Expr, bool>::iterator i = d_translated.find(e);
00153 //       return i != d_translated.end() && (*i).second; }
00154 //   void setTranslated(const CVC3::Expr& e)
00155 //     { DebugAssert(!isTranslated(e),"already set");
00156 //       d_translated.insert(e, true, d_bottomScope); }
00157 //   void clearTranslated(const CVC3::Expr& e)
00158 //     { d_translated.insert(e, false, d_bottomScope); }
00159 
00160 public:
00161   CNF_Manager(CVC3::TheoremManager* tm, CVC3::Statistics& statistics,
00162               const CVC3::CLFlags& flags);
00163   ~CNF_Manager();
00164 
00165   //! Register CNF callback
00166   void registerCNFCallback(CNFCallback* cnfCallback)
00167     { d_cnfCallback = cnfCallback; }
00168 
00169   //! Set scope for translation
00170   void setBottomScope(int scope) { d_bottomScope = scope; }
00171 
00172   //! Return the number of variables being managed
00173   unsigned numVars() { return d_varInfo.size(); }
00174 
00175   //! Return number of fanins for CNF node c
00176   /*! A CNF node x is a fanin of CNF node y if the expr for x is a child of the
00177    *  expr for y or if y is an ITE leaf and x is a new CNF node obtained by
00178    *  translating the ITE leaf y.
00179    *  \sa isITELeaf()
00180    */
00181   unsigned numFanins(Var c) {
00182     if (!c.isVar()) return 0;
00183     if (unsigned(c) >= d_varInfo.size()) return 0;
00184     return d_varInfo[c].fanins.size();
00185   }
00186 
00187   //! Returns the ith fanin of c.
00188   Lit getFanin(Var c, unsigned i) {
00189     DebugAssert(i < numFanins(c), "attempt to access unknown fanin");
00190     return d_varInfo[c].fanins[i];
00191   }
00192 
00193   //! Return number of fanins for c
00194   /*! x is a fanout of y if y is a fanin of x
00195    *  \sa numFanins
00196    */
00197   unsigned numFanouts(Var c) {
00198     if (!c.isVar()) return 0;
00199     if (unsigned(c) >= d_varInfo.size()) return 0;
00200     return d_varInfo[c].fanouts.size();
00201   }
00202 
00203   //! Returns the ith fanout of c.
00204   Lit getFanout(Var c, unsigned i) {
00205     DebugAssert(i < numFanouts(c), "attempt to access unknown fanin");
00206     return Lit(d_varInfo[c].fanouts[i]);
00207   }
00208 
00209   //! Convert a CNF literal to an Expr literal
00210   /*! Returns a NULL Expr if there is no corresponding Expr for l
00211    */
00212   const CVC3::Expr& concreteVar(Var v) {
00213     if (v.isNull()) return d_nullExpr;
00214     if (unsigned(v) >= d_varInfo.size() ||
00215         (!d_varInfo[v].expr.isTranslated()))
00216       return d_nullExpr;
00217     return d_varInfo[v].expr;
00218   }
00219 
00220   //! Convert a CNF literal to an Expr literal
00221   /*! Returns a NULL Expr if there is no corresponding Expr for l
00222    */
00223   CVC3::Expr concreteLit(Lit l, bool checkTranslated = true) {
00224     if (l.isNull()) return d_nullExpr;
00225     bool inverted = !l.isPositive();
00226     int index = l.getVar();
00227     if ((unsigned)index >= d_varInfo.size() ||
00228         (checkTranslated && !d_varInfo[index].expr.isTranslated()))
00229       return d_nullExpr;
00230     return inverted ? !d_varInfo[index].expr : d_varInfo[index].expr;
00231   }
00232 
00233   //! Look up the CNF literal for an Expr
00234   /*! Returns a NULL Lit if there is no corresponding CNF literal for e
00235    */
00236   Lit getCNFLit(const CVC3::Expr& e) {
00237     if (e.isFalse()) return Lit::getFalse();
00238     if (e.isTrue()) return Lit::getTrue();
00239     if (e.isNot()) return !getCNFLit(e[0]);
00240     CVC3::ExprHashMap<Var>::iterator i = d_cnfVars.find(e);
00241     if (!e.isTranslated() || i == d_cnfVars.end()) return Lit();
00242     return Lit((*i).second);
00243   }
00244 
00245   void cons(unsigned lb, unsigned ub, const CVC3::Expr& e2, std::vector<unsigned>& newLits);
00246 
00247   //! Convert thm A |- B (A is a set of literals) into one or more clauses
00248   /*! cnf should be empty -- it will be filled with the result */
00249   void convertLemma(const CVC3::Theorem& thm, CNF_Formula& cnf);
00250 
00251   //! Given thm of form A |- B, convert B to CNF and add it to cnf
00252   /*! Returns Lit corresponding to the root of the expression that was
00253    * translated. */
00254   Lit addAssumption(const CVC3::Theorem& thm, CNF_Formula& cnf);
00255 
00256   //! Convert thm to CNF and add it to the current formula
00257   /*! \param thm should be of form A |- B where A is a set of literals.
00258    * \param cnf the new clauses are added to cnf.
00259    * Returns Lit corresponding to the root of the expression that was
00260    * translated. */
00261   Lit addLemma(CVC3::Theorem thm, CNF_Formula& cnf);
00262 
00263 };
00264 
00265 }
00266 
00267 #endif