("help,h", "Help screen")
("input,i", boost::program_options::value<std::string>(), "(required) Path to get the input file")
("input-type,it", boost::program_options::value<std::string>()->default_value("cnf"), "The input type")
("method,m", boost::program_options::value<std::string>(), "(required) The method we run (counting for model counting, ddnnf-compiler for decision DNNF compilation, projMC for a dedicated projected model counting, max#SAT for running a max#sat solver).")
("maxsharpsat-option-cut-max",boost::program_options::value<bool>()->default_value(true),"Try to cut the search space by considering lower and upper bounds in the max part.")
("maxsharpsat-option-cut-ind",boost::program_options::value<bool>()->default_value(true),"Try to cut the search space by considering lower and upper bounds in the projected part.")
("maxsharpsat-option-greedy-init",boost::program_options::value<bool>()->default_value(true),"Search for a first max interpretation greedily.")
("solver,s", boost::program_options::value<std::string>()->default_value("minisat"), "The solver we will use")
("preproc-solver,ps", boost::program_options::value<std::string>()->default_value("minisat"), "The solver we will use in the preproc")
("preproc,p",boost::program_options::value<std::string>()->default_value("basic"), "The preprocessing technique we will use (basic, backbone).")
("scoring-method,sm",boost::program_options::value<std::string>()->default_value("vsads"),"The scoring method used for selecting the next variable. [mom, dlcs, vsids, vsads, jwts]")
("occurrence-manager,om",boost::program_options::value<std::string>()->default_value("dynamic"),"The occurrence manager used. [add a description]")
("phase-heuristic,ph",boost::program_options::value<std::string>()->default_value("polarity"),"The way the phase of the next decision is selected (false, true, polarity or occurrence).")
("partitioning-heuristic,pvh",boost::program_options::value<std::string>()->default_value("decomposition-static-dual"),"The method used to compute a cut. [none, decomposition-static, bipartition-primal or bipartition-dual]")
("partitioning-heuristic-partitioner,php",boost::program_options::value<std::string>()->default_value("patoh"),"The partitioner we will call (patoh or kahypar).")
("partitioning-heuristic-bipartite-phase",boost::program_options::value<std::string>()->default_value("none"),"Use a two phases heuristic, where the tree decomposition construction is given in parameter [none, natural, primal or dual].")
("partitioning-heuristic-bipartite-phase-dynamic",boost::program_options::value<double>()->default_value(0),"Use a static decomposition when it seems that the initial decomposition is no more good enough (the given value gives the balanced limit ratio).")
("partitioning-heuristic-bipartite-phase-static",boost::program_options::value<int>()->default_value(0),"Use a static decomposition when the number of variable is more than the given parameter. Switch to the dynamic decomposition otherwise. If 0, this option is deactivated.")
("partitioning-heuristic-simplification-equivalence,phse",boost::program_options::value<bool>()->default_value(true),"The graph with be simplified by considering literal equivalence.")
("partitioning-heuristic-simplification-hyperedge,phsh",boost::program_options::value<bool>()->default_value(true),"The graph with be simplified by reducing the hyper edges.")
("cache-reduction-strategy,crs", boost::program_options::value<std::string>()->default_value("expectation"), "The strategy used to reduce the cache structure [none, expectation, cache or sharpSAT].")
("cache-reduction-strategy-cachet-limit,crscl", boost::program_options::value<unsigned long>()->default_value(10UL * (1<<21)), "The limit in term of number of entries, the cachet reduction strategy allows.")
("cache-reduction-strategy-expectation-limit,crsel", boost::program_options::value<unsigned long>()->default_value(100000), "The frequency in term of number of negative hits used for the expectation reduction strategy allows.")
("cache-reduction-strategy-expectation-ratio,crser", boost::program_options::value<double>()->default_value(0.3), "The ratio used to decide if a clause can be kept or not.")
("cache-smudge-activation", boost::program_options::value<bool>()->default_value(true), "It does not directly remove the entries, but we do it when we need more memory.")
("cache-size-first-page", boost::program_options::value<unsigned long>()->default_value((1UL<<31)), "The block size of memory allocated for the first page of the cache structure.")
("cache-size-additional-page", boost::program_options::value<unsigned long>()->default_value((1UL<<29)), "The block size of memory allocated for the next page of the cache structure.")
("cache-store-strategy", boost::program_options::value<std::string>()->default_value("not-touched"), "The strategy used to store the clause in a bucket (all, not-binary and not-touched).")
("cache-clause-representation", boost::program_options::value<std::string>()->default_value("clause"), "The way the clause are represented in the cache (combi, sym, clause and index).")
("cache-clause-representation-combi-limitVar-sym", boost::program_options::value<unsigned>()->default_value(20), "In the mixed strategy, if we have less than a given number of variable then we use the symmetry caching representation.")
("cache-clause-representation-combi-limitVar-index", boost::program_options::value<unsigned>()->default_value(2000), "In the mixed strategy, if we have more than a given number of variable then we use the index caching representation.")
("cache-limit-number-variable", boost::program_options::value<unsigned>()->default_value(100000), "The number of variables threshold used to decide if the cache is used or not.")
("cache-limit-ratio", boost::program_options::value<double>()->default_value(0), "For the dynamic limit, posHit/negHit < ratio.")
("cache-activated", boost::program_options::value<bool>()->default_value(true), "Activate or not the cache.")
("phase-heuristic-reversed,pha", boost::program_options::value<bool>()->default_value(false), "Consider or not the reverse of the current phase.")
("float-precision,fp", boost::program_options::value<int>()->default_value(128), "The precision for the float.")
("float,f", boost::program_options::value<bool>()->default_value(false), "If the count is computed as a float or not.")
("dump-ddnnf", boost::program_options::value<std::string>(), "Print out the decision DNNF formula in a given file.")
("query,q", boost::program_options::value<std::string>(), "Perform the queries given in a file (m l1 l2 ... ln 0 for a model counting query, and d l1 l2 ... ln 0 for a satisfiability query).")
("projMC-refinement", boost::program_options::value<bool>()->default_value(false), "Try to reduce the set of selector by computing a MSS.")
("keyword-output-format-solution", boost::program_options::value<std::string>()->default_value("s"), "The keyword prints in front of the solution when it is printed out.")
("output-format", boost::program_options::value<std::string>()->default_value("classic"), "The way the solution is printed out ('classic' only gives the number of solution after printing 's', 'competition' follows the MC competition 2021).")