/*****************************************************************************/
/*!
 * \file translator.h
 * \brief An exception to be thrown by the smtlib translator.
 * 
 * Author: Clark Barrett
 * 
 * Created: Sat Jun 25 18:03:09 2005
 *
 * <hr>
 * Copyright (C) 2003 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 _CVC_lite__translator_h_
#define _CVC_lite__translator_h_

#include <string>
#include <fstream>
#include "queryresult.h"

namespace CVCL {

class Expr;
class Type;
class ExprManager;
class ExprStream;
class TheoryCore;
class TheoryUF;
class TheoryArith;
class TheoryArray;
class TheoryQuant;
class TheoryRecords;
class TheorySimulate;
class TheoryBitvector;
class TheoryDatatype;
template <class Data> class ExprMap;

//Eventually all the nontrivial translation code should go here
class Translator {
  ExprManager* d_em;
  const bool& d_translate;
  const bool& d_real2int;
  const std::string& d_convertToDiff;
  bool d_iteLiftArith;

  //! The log file for top-level API calls in the CVCL input language
  std::ostream* d_osdump;
  std::ostream* d_osdumpTranslate;
  std::ofstream d_osdumpFile, d_osdumpTranslateFile;
  std::ifstream d_tmpFile;
  bool d_dump, d_dumpFileOpen, d_translateFileOpen;

  bool d_auflia, d_auflira, d_unknown;

  Expr* d_zeroVar;

  TheoryCore* d_theoryCore;
  TheoryUF* d_theoryUF;
  TheoryArith* d_theoryArith;
  TheoryArray* d_theoryArray;
  TheoryQuant* d_theoryQuant;
  TheoryRecords* d_theoryRecords;
  TheorySimulate* d_theorySimulate;
  TheoryBitvector* d_theoryBitvector;
  TheoryDatatype* d_theoryDatatype;

  std::string fileToSMTLIBIdentifier(const std::string& filename);
  Expr preprocessRec(const Expr& e, ExprMap<Expr>& cache, Type desiredType);
  Expr preprocess(const Expr& e);

public:
  // Constructors
  Translator(ExprManager* em,
             const bool& translate,
             const bool& real2int,
             const std::string& convertToDiff,
             bool iteLiftArith);

  bool start(const std::string& dumpFile);
  void dump(const Expr& e, bool dumpOnly = false);
  void dumpAssertion(const Expr& e);
  bool dumpQuery(const Expr& e);
  void dumpQueryResult(QueryResult qres);
  void finish();

  void setTheoryCore(TheoryCore* theoryCore) { d_theoryCore = theoryCore; }
  void setTheoryUF(TheoryUF* theoryUF) { d_theoryUF = theoryUF; }
  void setTheoryArith(TheoryArith* theoryArith) { d_theoryArith = theoryArith; }
  void setTheoryArray(TheoryArray* theoryArray) { d_theoryArray = theoryArray; }
  void setTheoryQuant(TheoryQuant* theoryQuant) { d_theoryQuant = theoryQuant; }
  void setTheoryRecords(TheoryRecords* theoryRecords) { d_theoryRecords = theoryRecords; }
  void setTheorySimulate(TheorySimulate* theorySimulate) { d_theorySimulate = theorySimulate; }
  void setTheoryBitvector(TheoryBitvector* theoryBitvector) { d_theoryBitvector = theoryBitvector; }
  void setTheoryDatatype(TheoryDatatype* theoryDatatype) { d_theoryDatatype = theoryDatatype; }

  void translateArray(ExprStream& os, const Expr& e);

  Expr zeroVar();

  // Destructor
  virtual ~Translator() { }

}; // end of class Translator

} // end of namespace CVCL 

#endif
