#!/usr/bin/env python
# -*- coding: utf-8 -*-

# Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
#
# This program is free software; you can redistribute it and/or
# modify it under the terms of the GNU General Public License
# as published by the Free Software Foundation; version 2
# of the License.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program; if not, write to the Free Software
# Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
# 02110-1301, USA.

import optparse
import random
import time
import string
import configparser


def parse_arguments():
    class PlainHelpFormatter(optparse.IndentedHelpFormatter):

        def format_description(self, description):
            if description:
                return description + "\n"
            else:
                return ""

    usage = """usage: %prog

To use other solvers, give:
--solver SWDiA5BY.alt.vd.res.va2.15000.looseres.3tierC5/binary/SWDiA5BY_static.alt.vd
--solver SWDiA5BY_A26/binary/SWDiA5BY_static_A26
--solver lingeling_ayv/binary/lingeling_ayv
--solver glucose2016/simp/glucose_static_2016
--solver MapleCOMSPS/simp/maplecomsps_static
--solver cmsat-satcomp16/bin/cryptominisat4_simple
--solver lingeling-bbc/build/lingeling/lingeling_bbc
--solver Maple_LCM_Dist/Maple_LCM_Dist # may work with --drat, but needs updated DRAT checker


Use-cases:
# normal run
./launch_server.py --cnflist satcomp17_updated

# stats run
./launch_server.py --cnf test_updated --stats --drat --tout 600 --memlimit 10000
./launch_server.py --cnf unsat_small_candidates_fullpath --stats --drat --tout 600 --memlimit 10000


# testing, using small instance to check (cheaper & faster)
./launch_server.py --cnflist test_updated

# 2 clients, no preprocessing
./launch_server.py --cnflist satcomp14 -c 2 --opt "--preproc 0" --folder no_preproc

# gaussian elimination -- automatic detection, built with GAUSS
./launch_server.py --cnflist satcomp14 --folder gauss

# clause IDs so learning can be performed -- gzipped SQL output with clause IDs will be produced
./launch_server.py --stats --drat --folder learning

# to give options to the solver
./launch_server.py --folder with_opts --opt \"--ml=1,--keepglue=4\""

 # to upload satzilla_features_to_reconf.cpp
aws s3 cp ../../src/satzilla_features_to_reconf.cpp s3://msoos-solve-data/solvers/

"""
    parser = optparse.OptionParser(usage=usage, formatter=PlainHelpFormatter())
    parser.add_option("--verbose", "-v", action="store_true",
                      default=False, dest="verbose", help="Be more verbose"
                      )

    parser.add_option("--numclients", "-c", default=None, type=int,
                      dest="client_count", help="Number of clients to launch"
                      )

    parser.add_option("--port", "-p", default=10000, dest="port",
                      help="Port to listen on. [default: %default]", type="int"
                      )

    parser.add_option("--tout", "-t", default=3000, dest="timeout_in_secs",
                      help="Timeout for the file in seconds"
                      "[default: %default]",
                      type=int
                      )

    parser.add_option("--toutmult", default=12.1, dest="tout_mult",
                      help="Approx: 1x is solving, 10x time is DRAT time wait, 1x is parsing, 0.1x that is sending us the result."
                      "[default: %default]",
                      type=float
                      )

    parser.add_option("--memlimit", "-m", default=1600, dest="mem_limit_in_mb",
                      help="Memory limit in MB"
                      "[default: %default]",
                      type=int
                      )

    parser.add_option("--cnflist", default="satcomp14_updated", dest="cnf_list",
                      type=str,
                      help="The list of CNF files to solve, first line the dir"
                      "[default: %default]",
                      )

    parser.add_option("--dir", default="/home/ubuntu/", dest="base_dir", type=str,
                      help="The home dir of cryptominisat [default: %default]"
                      )

    parser.add_option("--solver",
                      default="cryptominisat/build/cryptominisat5",
                      dest="solver",
                      help="Solver executable"
                      "[default: %default]",
                      type=str
                      )

    parser.add_option("--folder", default="results", dest="given_folder",
                      help="S3 folder name to upload data"
                      "[default: %default]",
                      type=str
                      )

    parser.add_option("--git", dest="git_rev", type=str,
                      help="The GIT revision to use. Default: HEAD"
                      )

    parser.add_option("--opt", dest="extra_opts", type=str, default="",
                      help="Extra options to give to solver"
                      "[default: %default]",
                      )

    parser.add_option("--noshutdown", "-n", default=False, dest="noshutdown",
                      action="store_true", help="Do not shut down clients"
                      )

    parser.add_option("--drat", default=False, dest="drat",
                      action="store_true", help="Use DRAT"
                      )

    parser.add_option("--stats", default=False, dest="stats",
                      action="store_true", help="Use STATS and get SQLITE data"
                      )

    parser.add_option("--gauss", default=False, dest="gauss",
                      action="store_true", help="Use GAUSS"
                      )

    parser.add_option("--logfile", dest="logfile_name", type=str,
                      default="python_server_log.log", help="Name of LOG file")

    # parse options
    options, args = parser.parse_args()
    conf = configparser.ConfigParser()
    if options.cnf_list == "test":
        conf.read('ec2-spot-instance-test.cfg')
    else:
        conf.read('ec2-spot-instance.cfg')

    options.s3_bucket = conf.get("ec2", "result_bucket")
    options.key_name = conf.get("ec2", "key_name")
    options.security_group_server = conf.get("ec2", "security_group_server")
    options.subnet_id = conf.get("ec2", "subnet_id")
    options.ami_id = conf.get("ec2", "ami_id")
    options.region = conf.get("ec2", "region")

    def rnd_id():
        return ''.join(random.choice(string.ascii_uppercase + string.digits) for _ in range(5))

    options.logfile_name = options.base_dir + options.logfile_name
    options.given_folder += "-" + time.strftime("%d-%B-%Y")
    options.given_folder += "-%s" % rnd_id()
    options.given_folder += "-%s" % options.cnf_list

    if options.drat and not options.stats:
        print("ERROR: You must have --stats when you use --drat")
        exit(-1)

    return options, args


if __name__ == "__main__":
    options, args = parse_arguments()
    print("Options are:", options)
    print("args are:", args)
