/*! \mainpage CMS_Solver(Cost-Minimizing Search QBF Solver)
    
 *
 * \section intro_sec Introduction
 *
 * This is the introduction.
 *
 * \section install_sec Installation
 *
 * \subsection step1 Step 1: Opening the box
 * 
 * 
 * etc...
 */

//! driver file
/*!  It take an instance file as an input argument. Then parse and solve, and return the result.
 */
#include <iostream>
#include "qbf.hpp"
#include "qbf_lexer.hpp"
#include "qbf_parser.hpp"
#include "variable.hpp"
#include <ctime>
#include <fstream>

int main(int argc //!< Number of arguments.
	 , char** argv //!< String buffer for the arguments.
    )
{
  std::cout << "CMS Solver" << std::endl 
	    << "Microsoft Research Asia, Copyright (c) 2008 Microsoft Corporation" << std::endl;

    std::ifstream input_file_stream;
    QBF_Lexer* qbf_lexer;
    // If input argument exists, take it as a input file name
    // If not, take std::cin as a input stream.
    if(argc == 2) {
      //	std::cout << "Input File : " << argv[1] << std::endl;
	input_file_stream.open(argv[1]);
	qbf_lexer = new QBF_Lexer(input_file_stream);
    }
    else {
      //	std::cout << "Input from the standard input." << std::endl;
	qbf_lexer = new QBF_Lexer(std::cin);
    }

    // Parse the input
    QBF_Parser qbf_parser(qbf_lexer);
    QBF* qbf = qbf_parser.parse();
    //    std::cerr << "parsing time : " << ((double)clock() / CLOCKS_PER_SEC) << " sec" << std::endl;
    
    // Check for the parsing error.
    if (qbf == NULL) {
	std::cerr << "Parse Error" << std::endl;
	return -1;
    }

    // Update
    qbf->update();
    //    std::cerr << "update time : " << ((double)clock() / CLOCKS_PER_SEC) << " sec" << std::endl;
    qbf->reset_status();
    qbf->update();
    //    std::cerr << "update time : " << ((double)clock() / CLOCKS_PER_SEC) << " sec" << std::endl;
  
    //    std::cout << "# of Var : " << Variable::counter << std::endl;    
    // Evaluate
    bool result = qbf->eval();

    //    std::cout << (result == true ? "\nTrue" : "\nFalse") << std::endl;
    //    std::cerr << "eval time : " << ((double)clock() / CLOCKS_PER_SEC) << " sec" << std::endl;

    // Delete
    delete qbf;
    delete qbf_lexer;

    // Return the result
    return (result == true) ? 10 : 20;
}
