/*****************************************************************************/
/*!
 *\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>
 *
 * 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.
 * 
 * <hr>
 */
/*****************************************************************************/

#ifndef _cvc3__include__cnf_manager_h_
#define _cvc3__include__cnf_manager_h_

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

namespace CVC3 {

class CommonProofRules;
class CNF_Rules;
class ValidityChecker;
class Statistics;

}

namespace SAT {

class CNF_Manager {

  //! For clause minimization
  CVC3::ValidityChecker* d_vc;

  //! Whether to use brute-force clause minimization
  bool d_minimizeClauses;

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

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

  //! Information kept for each CNF variable
  struct Varinfo {
    CVC3::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
  CVC3::ExprMap<Var> d_cnfVars;

  //! Cached translation of term-ite-containing expressions
  CVC3::ExprMap<CVC3::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. */
  //  CVC3::CDMap<int, CVC3::Theorem> d_theorems;

  //! Next clause id
  int d_clauseIdNext;

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

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

  //! Queue of theorems to translate
  std::deque<CVC3::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;

  //! Reference to statistics object
  CVC3::Statistics& d_statistics;

public:
  //! Abstract class for callbacks
  class CNFCallback {
  public:
    CNFCallback() {}
    virtual ~CNFCallback() {}
    //! Register an atom
    virtual void registerAtom(const CVC3::Expr& e,
                              const CVC3::Theorem& thm) = 0;
  };

private:
  //! Instance of CNF_CallBack: must be registered
  CNFCallback* d_cnfCallback;

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

  //! Register a new atomic formula
  void registerAtom(const CVC3::Expr& e, const CVC3::Theorem& thm);

  //! 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 CVC3::Expr& e, CNF_Formula& cnf,
                       const CVC3::Theorem& thmIn);

  //! 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.
   */
  CVC3::Theorem replaceITErec(const CVC3::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 CVC3::Theorem& thmIn, CNF_Formula& cnf);

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

public:
  CNF_Manager(CVC3::TheoremManager* tm, CVC3::Statistics& statistics, bool minimizeClauses);
  ~CNF_Manager();

  //! Register CNF callback
  void registerCNFCallback(CNFCallback* cnfCallback)
    { d_cnfCallback = cnfCallback; }

  //! 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 Lit(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
   */
  CVC3::Expr concreteLit(Lit l, bool checkTranslated = true) {
    if (l.isNull()) return CVC3::Expr();
    bool inverted = !l.isPositive();
    int index = l.getVar();
    if ((unsigned)index >= d_varInfo.size() ||
        (checkTranslated && !d_varInfo[index].expr.isTranslated()))
      return CVC3::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 CVC3::Expr& e) {
    if (e.isFalse()) return Lit::getFalse();
    if (e.isTrue()) return Lit::getTrue();
    if (e.isNot()) return !getCNFLit(e[0]);
    CVC3::ExprMap<Var>::iterator i = d_cnfVars.find(e);
    if (!e.isTranslated() || i == d_cnfVars.end()) return Lit();
    return Lit((*i).second);
  }

  void cons(unsigned lb, unsigned ub, const CVC3::Expr& e2, std::vector<unsigned>& newLits);

  //! 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 CVC3::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 CVC3::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.
   * \param cnf the new clauses are added to cnf.
   * Returns Lit corresponding to the root of the expression that was
   * translated. */
  Lit addLemma(const CVC3::Theorem& thm, CNF_Formula& cnf);

};

}

#endif