cnf_manager.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 *\file cnf_manager.h
 *\brief Manager for conversion to and traversal of CNF formulas
 *
 * Author: Clark Barrett
 *
 * Created: Thu Dec 15 13:53:16 2005
 *
 * <hr>
 * Copyright (C) 2005 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 */
/*****************************************************************************/

#ifndef _cvcl__include__cnf_manager_h_
#define _cvcl__include__cnf_manager_h_

#include "cnf.h"
#include "expr.h"
#include "expr_map.h"
#include "cdmap.h"

namespace CVCL {

class CommonProofRules;
class CNF_Rules;

}

namespace SAT {

class CNF_Manager {

  //! Common proof rules
  CVCL::CommonProofRules* d_commonRules;

  //! Rules for manipulating CNF
  CVCL::CNF_Rules* d_rules;

  //! Information kept for each CNF variable
  struct Varinfo {
    CVCL::Expr expr;
    std::vector<Lit> fanins;
    std::vector<Var> fanouts;
  };

  //! vector that maps a variable index to information for that variable
  std::vector<Varinfo> d_varInfo;

  //! Map from Exprs to Vars representing those Exprs
  CVCL::ExprMap<Var> d_cnfVars;

  //! Cached translation of term-ite-containing expressions
  CVCL::ExprMap<CVCL::Theorem> d_iteMap;

  //! Maps a clause id to the theorem justifying that clause
  /*! Note that clauses created by simple CNF translation are not given id's.
   *  This is because theorems for these clauses can be created lazily later. */
  CVCL::CDMap<int, CVCL::Theorem> d_theorems;

  //! Next clause id
  int d_clauseIdNext;

  //! Whether expr has already been translated
  //  CVCL::CDMap<CVCL::Expr, bool> d_translated;

  //! Bottom scope in which translation is valid
  int d_bottomScope;

  //! Queue of theorems to translate
  std::deque<CVCL::Theorem> d_translateQueueThms;

  //! Queue of fanouts corresponding to thms to translate
  std::deque<Var> d_translateQueueVars;

  //! Whether thm to translate is "translate only"
  std::deque<bool> d_translateQueueFlags;

private:

  CVCL::CNF_Rules* createProofRules(CVCL::TheoremManager* tm);

  //! Recursively translate e into cnf
  /*! A non-context dependent cache, d_cnfVars is used to remember translations
   * of expressions.  A context-dependent attribute, isTranslated, is used to
   * remember whether an expression has been translated in the current context */
  Lit translateExprRec(const CVCL::Expr& e, CNF_Formula& cnf);

  //! Recursively traverse an expression with an embedded term ITE
  /*! Term ITE's are handled by introducing a skolem variable for the ITE term
   * and then adding new constraints describing the ITE in terms of the new variable.
   */
  CVCL::Theorem replaceITErec(const CVCL::Expr& e, Var v, bool translateOnly);

  //! Recursively translate e into cnf
  /*! Call translateExprRec.  If additional expressions are queued up,
   * translate them too, until none are left. */
  Lit translateExpr(const CVCL::Expr& e, CNF_Formula& cnf);

//   bool isTranslated(const CVCL::Expr& e)
//     { CVCL::CDMap<CVCL::Expr, bool>::iterator i = d_translated.find(e);
//       return i != d_translated.end() && (*i).second; }
//   void setTranslated(const CVCL::Expr& e)
//     { DebugAssert(!isTranslated(e),"already set");
//       d_translated.insert(e, true, d_bottomScope); }
//   void clearTranslated(const CVCL::Expr& e)
//     { d_translated.insert(e, false, d_bottomScope); }

public:
  CNF_Manager(CVCL::TheoremManager* tm);
  ~CNF_Manager();

  //! Set scope for translation
  void setBottomScope(int scope) { d_bottomScope = scope; }

  //! Return the number of variables being managed
  unsigned numVars() { return d_varInfo.size(); }

  //! Return number of fanins for CNF node c
  /*! A CNF node x is a fanin of CNF node y if the expr for x is a child of the
   *  expr for y or if y is an ITE leaf and x is a new CNF node obtained by
   *  translating the ITE leaf y.
   *  \sa isITELeaf()
   */
  unsigned numFanins(Lit c) {
    if (!c.isVar()) return 0;
    int index = c.getVar();
    if ((unsigned)index >= d_varInfo.size()) return 0;
    return d_varInfo[index].fanins.size();
  }

  //! Returns the ith fanin of c.
  Lit getFanin(Lit c, unsigned i) {
    DebugAssert(i < numFanins(c), "attempt to access unknown fanin");
    return d_varInfo[c.getVar()].fanins[i];
  }

  //! Return number of fanins for c
  /*! x is a fanout of y if y is a fanin of x
   *  \sa numFanins
   */
  unsigned numFanouts(Lit c) {
    if (!c.isVar()) return 0;
    int index = c.getVar();
    if ((unsigned)index >= d_varInfo.size()) return 0;
    return d_varInfo[index].fanouts.size();
  }

  //! Returns the ith fanout of c.
  Lit getFanout(Lit c, unsigned i) {
    DebugAssert(i < numFanouts(c), "attempt to access unknown fanin");
    return d_varInfo[c.getVar()].fanouts[i];
  }

  //! Convert a CNF literal to an Expr literal
  /*! Returns a NULL Expr if there is no corresponding Expr for l
   */
  CVCL::Expr concreteLit(Lit l) {
    if (l.isNull()) return CVCL::Expr();
    bool inverted = !l.isPositive();
    int index = l.getVar();
    if ((unsigned)index >= d_varInfo.size() ||
        !d_varInfo[index].expr.isTranslated()) return CVCL::Expr();
    return inverted ? !d_varInfo[index].expr : d_varInfo[index].expr;
  }

  //! Look up the CNF literal for an Expr
  /*! Returns a NULL Lit if there is no corresponding CNF literal for e
   */
  Lit getCNFLit(const CVCL::Expr& e) {
    if (e.isFalse()) return Lit::getFalse();
    if (e.isTrue()) return Lit::getTrue();
    if (e.isNot()) return !getCNFLit(e[0]);
    CVCL::ExprMap<Var>::iterator i = d_cnfVars.find(e);
    if (!e.isTranslated() || i == d_cnfVars.end()) return Lit();
    return Lit((*i).second);
  }

  //! Convert thm A |- B (A is a set of literals) into a clause ~A \/ B
  /*! c should be an empty clause that will be filled with the result */
  void convertLemma(const CVCL::Theorem& thm, Clause& c);

  //! Given thm of form A |- B, convert B to CNF and add it to cnf
  /*! Returns Lit corresponding to the root of the expression that was
   * translated. */
  Lit addAssumption(const CVCL::Theorem& thm, CNF_Formula& cnf);

  //! Convert thm to CNF and add it to the current formula
  /*! \param thm should be of form A |- B where A is a set of literals
   * The new clauses are added to cnf.
   * Returns Lit corresponding to the root of the expression that was
   * translated. */
  Lit addLemma(const CVCL::Theorem& thm, CNF_Formula& cnf);

};

}

#endif

---