#ifndef ARGT_READER_H
#define ARGT_READER_H

#include <map>
#include <string>
#include <fstream>
#include "stdlib.h"

using namespace std;

class t_ConfigurationOptions
{

public:
  string m_sModuleName;
  string m_sCDFGFileName;
  string m_sRunFromStageName;
  string m_sRunToStageName;
  string m_sSTEFileName;
  string m_sSTEAntecedentFile;
  string m_sSTEConsequentFile;
  string pythonConvertSTEFile;
  string m_dagNodeIdFile;
  int m_VerbosityLevel;
  int m_nCycleCountForEvaluation;
  string m_sSignalsToObserveFileName;
  int m_fixed_input_simulation_flag;
  string m_fixed_input_simulation_inputs_file;
  int m_restructuring_disable_flag;
  string m_sCDFGGen_arguments;
  bool m_allowCombinationalSignalsInCycle;
  bool m_generateNewInputs;
  bool m_bPerformWSTE;
  string m_CustomAtomIndicesFile;
  int invBitGenerationLevel;
  string m_pathSeparator;
  string m_extraConstraintsFile;
  string m_weakenFile;
  string m_extraSignalSTE;
  bool m_checkAssertion;
  
  bool m_printDebugOutput;
  bool m_lastDimensionBitVec; //treats last dimension of an array as bitvector rather than printing it as a one dimensional array
  bool m_doBitBlasting;
  bool m_convertSelectOnMemoryToReads;
  bool m_printFullExpression;
  
  /**
   * If this option is on then in consequent constraints are modified to:
   * Invalid Bits of Consequent and Generated should be same AND if valid then their values should also be equal.<br/>
   * Otherwise we generate the constraint specifying that generated value should be stronger than consequent i.e.
   * If consequent is valid the generated is valid and their values are equal.
   */
  bool m_consequentExactMatch;
  
  /**
   * bitNo.
   * 0      -> no pruning
   * 1      -> pruning based on consequent
   * 2      -> pruning based on antecedent
   * 3      -> pruning based on weakening
   */
  int m_pruningLevel;
  
  //lists the signals in the consequent
  string m_consequentSignalsFile;
  
  //lists the signals in the antecedent
  string m_antecedentSignalsFile;

  // Directory in which all temporary information is to be written
  string m_sTempInfoDir;

  // Directory in which all log files are to be written
  string m_sLogDir;

  // Directory in which time information is to be written
  string m_sTimeInfoDir;

  // File from which user input values for state signals are to be read when
  // comparing the results of evaluating symbolic expressions generated by symbolic 
  // simulator with concrete values vis-a-vis constant-propagated values given
  // by LIRA
  string m_sUserInputValuesForStateSignalsFile;

  // File from which user input values for primary input signals are to be read when
  // comparing the results of evaluating symbolic expressions generated by symbolic 
  // simulator with concrete values vis-a-vis constant-propagated values given
  // by LIRA
  string m_sUserInputValuesForPrimaryInputsFile;

  // If this flag is set to true, the tool exits after generating atom information
  // Otherwise, the tool proceeds to symbolic simulation and beyond.
  bool m_bGenerateAtomInformationOnly;

  // The following member is perhaps not needed. Need to clean this up.
  string m_initialMarkedSignalsFile;

  /**
   * if the following flag is on then bounded model checking (BMC) is performed
   * where in each clock cycle, the ckt is unrolled, i.e. the outputs of state
   * signals go into a virtual copy of that ckt in next clock cycle. This is
   * done via generating new intermediate variables and plugging that variable
   * in the expression tree for the expression from previous cycle (for variable
   * valued state signals) in order to prevent the whole expression from getting
   * huge at the time of replacement. It also throws a constraint while doing
   * it to make sure that this temporary variables agree with the expressions
   * generated via WSTE
   * 
   * by default, its value is set as false
   */
  bool m_performBMC;
  
private:
  void readOptionsFromConfigFile(string config_file_name);
  void readOptionsFromCmdline(map<string, string>& cmdline_options);
  bool readUserOption(string line);
  
  /** 
   * initialize with default values. important to call this first from
   * all constructors
   */
  void init();

public:
    
    /**
     * default constructor for convenience
     */
     t_ConfigurationOptions();

    /**
     * constructor that takes configuration filename
     * 
     * @param filename the configuration filename
     */
     t_ConfigurationOptions(string filename);

    /**
     * constructor that takes map of user specified cmdline options
     * 
     * @param cmdline_options map containing user specified options as
     * option and their corresponding value as key-value pair
     */
     t_ConfigurationOptions(map<string, string>& cmdline_options);
  
  
#ifdef OLD
  t_ConfigurationOptions(t_ConfigurationOptions& copyOptions);
#endif
    static t_ConfigurationOptions* getConfig(){
        return config;
    }

    /**
     * the method returns a map contains the cmdline options and their corresponding
     * descriptions as key and value respectively, useful for showing help and parsing
     * cmdline options. when adding a new option add an entry here to make it available 
     * from cmdline
     * 
     * @return the map containing cmdline options
     */
    static map<string, vector<string> >& get_cmdline_options();
    
protected:
    static t_ConfigurationOptions *config;
};

#endif // ARGT_READER_H