Config.h

 
#pragma once
 
#include <iosfwd>
#include <string>
#include <string_view>
 
#include "dlinear/util/OptionValue.hpp"
 
namespace dlinear {
 
#define DLINEAR_PARAMETER(param_name, type, default_value, help)                           \
 public:                                                                                   \
    \
  OptionValue<type> &m_##param_name() { return param_name##_; }                            \
 \
  [[nodiscard]] const type &param_name() const { return param_name##_.get(); }             \
  static constexpr type default_##param_name{default_value};                               \
  static constexpr const char *const help_##param_name{help};                              \
                                                                                           \
 private:                                                                                  \
  OptionValue<type> param_name##_{default_value};
 
class Config {
 public:
  enum class LPSolver {
    SOPLEX = 0,   
    QSOPTEX = 1,  
  };
  enum class SatSolver {
    CADICAL = 0,  
    PICOSAT = 1,  
  };
  enum class SatDefaultPhase {
    False = 0,              
    True = 1,               
    JeroslowWang = 2,       
    RandomInitialPhase = 3  
  };
  enum class Format {
    AUTO,   
    SMT2,   
    MPS,    
    VNNLIB  
  };
  enum class LPMode {
    AUTO = 0,                       
    PURE_PRECISION_BOOSTING = 1,    
    PURE_ITERATIVE_REFINEMENT = 2,  
    HYBRID = 3,                     
  };
  enum class BoundPropagationType {
    AUTO = 0,           
    EQ_BINOMIAL = 1,    
    EQ_POLYNOMIAL = 2,  
    BOUND_POLYNOMIAL = 3,  
  };
  enum class PreprocessingRunningFrequency {
    AUTO,          
    NEVER,         
    ON_FIXED,      
    ON_ITERATION,  
    ALWAYS         
  };
 
  Config() = default;
  explicit Config(std::string filename);
  explicit Config(bool read_from_stdin);
 
 public:
  static constexpr std::string_view help_onnx_file{"ONNX file name"};
  static constexpr std::string_view help_filename{"Input file name"};
 
  [[nodiscard]] std::string filename() const { return filename_.get(); }
  [[nodiscard]] std::string filename_extension() const;
  OptionValue<std::string> &m_filename() { return filename_; }
  [[nodiscard]] std::string onnx_file() const { return onnx_file_.get(); }
  OptionValue<std::string> &m_onnx_file() { return onnx_file_; }
  [[nodiscard]] bool needs_expansion() const;
  [[nodiscard]] LPMode actual_lp_mode() const;
  [[nodiscard]] Format actual_format() const;
  [[nodiscard]] BoundPropagationType actual_bound_propagation_type() const;
  [[nodiscard]] PreprocessingRunningFrequency actual_bound_propagation_frequency() const;
  [[nodiscard]] PreprocessingRunningFrequency actual_bound_implication_frequency() const;
 
 private:
  OptionValue<std::string> filename_{""};
  OptionValue<std::string> onnx_file_{""};
 
  DLINEAR_PARAMETER(bound_propagation_type, BoundPropagationType, BoundPropagationType::AUTO,
                    "The type of bound propagation to apply in the preprocessing phase.\n"
                    "\t\tEach of the options is more complete and expensive than the previous one.\n"
                    "\t\tOne of: auto (1), eq-binomial (2), eq-polynomial (3), bound-polynomial (4)")
  DLINEAR_PARAMETER(bound_propagation_frequency, PreprocessingRunningFrequency, PreprocessingRunningFrequency::AUTO,
                    "How often to run the generic bound propagation preprocessing.\n"
                    "\t\tOne of: auto (1), never (2), on-fixed (3), on-iteration (4), always (5)")
  DLINEAR_PARAMETER(bound_implication_frequency, PreprocessingRunningFrequency, PreprocessingRunningFrequency::AUTO,
                    "How often to run the bound implication preprocessing.\n"
                    "\t\tOne of: auto (1), never (2), always (3)")
  DLINEAR_PARAMETER(complete, bool, false,
                    "Run the solver in complete mode.\n"
                    "\t\tThe precision will be set to 0 and strict inequalities will be taken into account")
  DLINEAR_PARAMETER(continuous_output, bool, false, "Continuous output")
  DLINEAR_PARAMETER(csv, bool, false, "Produce CSV output. Must also specify --with-timings to get the time stats")
  DLINEAR_PARAMETER(debug_parsing, bool, false, "Debug parsing")
  DLINEAR_PARAMETER(debug_scanning, bool, false, "Debug scanning/lexing")
  DLINEAR_PARAMETER(disable_expansion, bool, false,
                    "Disable formula expansion.\n"
                    "\t\tMakes the parser faster, "
                    "but may create issues if an intermediate formula of the input becomes non linear")
  DLINEAR_PARAMETER(
      enforce_check_sat, bool, false,
      "Perform a satisfiability check at the end of parsing if the input does not contain a (check-sat) directive")
  DLINEAR_PARAMETER(format, Format, dlinear::Config::Format::AUTO,
                    "Input file format\n"
                    "\t\tOne of: auto (1), smt2 (2), mps (3), vnnlib (4)")
  DLINEAR_PARAMETER(lp_mode, LPMode, dlinear::Config::LPMode::AUTO,
                    "LP mode used by the LP solver.\n"
                    "\t\tOne of: auto (1), pure-precision-boosting (2), pure-iterative-refinement (3), hybrid (4)")
  DLINEAR_PARAMETER(lp_solver, LPSolver, dlinear::Config::LPSolver::SOPLEX,
                    "Underlying LP solver used by the theory solver.\n"
                    "\t\tOne of: soplex (1), qsoptex (2)")
  DLINEAR_PARAMETER(number_of_jobs, unsigned int, 1u, "Number of jobs")
  DLINEAR_PARAMETER(optimize, bool, false, "Whether to optimize the objective function. Only affects the MPS format")
  DLINEAR_PARAMETER(precision, double, 9.999999999999996e-4,
                    "Delta precision used by the LP solver solver.\n"
                    "\t\tEven when set to 0, a positive infinitesimal value will be considered.\n"
                    "\t\twhile the LP solver will yield an exact solution, strict inequalities will still be relaxed\n"
                    "\t\tUse the --complete flag if you are looking for a complete solution")
  DLINEAR_PARAMETER(produce_models, bool, false,
                    "Produce models, showing a valid assignment.\n"
                    "\t\tOnly applicable if the result is sat or delta-sat")
  DLINEAR_PARAMETER(random_seed, unsigned int, 0u,
                    "Set the random seed. 0 means that the seed will be generated on the fly")
  DLINEAR_PARAMETER(read_from_stdin, bool, false, "Read the input from the standard input")
  DLINEAR_PARAMETER(sat_default_phase, SatDefaultPhase, dlinear::Config::SatDefaultPhase::JeroslowWang,
                    "set default initial phase for SAT solver.\n"
                    "\t\tOne of: false (0), true (1), Jeroslow-Wang (2), random initial phase (3)")
  DLINEAR_PARAMETER(sat_solver, SatSolver, dlinear::Config::SatSolver::PICOSAT,
                    "Underlying SAT solver used by the SAT solver.\n"
                    "\t\tOne of: cadical (1), picosat (2)")
  DLINEAR_PARAMETER(silent, bool, false, "Silent mode. Nothing will be printed on the standard output")
  DLINEAR_PARAMETER(simplex_sat_phase, int, 1, "What phase to use to verify the feasibility of the LP problem")
  DLINEAR_PARAMETER(skip_check_sat, bool, false, "Parse the input, but does not run the solver")
  DLINEAR_PARAMETER(verbose_dlinear, int, 2, "Verbosity level for dlinear. In the range [0, 5]")
  DLINEAR_PARAMETER(verbose_simplex, int, 0, "Verbosity level for simplex. In the range [0, 5]")
  DLINEAR_PARAMETER(verify, bool, false, "If the input produces a SAT output, verify the assignment against the input")
  DLINEAR_PARAMETER(with_timings, bool, false, "Report timings alongside results")
};
 
std::ostream &operator<<(std::ostream &os, const Config &config);
std::ostream &operator<<(std::ostream &os, const Config::SatDefaultPhase &sat_default_phase);
std::ostream &operator<<(std::ostream &os, const Config::LPSolver &lp_solver);
std::ostream &operator<<(std::ostream &os, const Config::SatSolver &mode);
std::ostream &operator<<(std::ostream &os, const Config::Format &format);
std::ostream &operator<<(std::ostream &os, const Config::LPMode &mode);
std::ostream &operator<<(std::ostream &os, const Config::BoundPropagationType &type);
std::ostream &operator<<(std::ostream &os, const Config::PreprocessingRunningFrequency &frequency);
 
}  // namespace dlinear
 
#ifdef DLINEAR_INCLUDE_FMT
#include "dlinear/util/logging.h"
 
OSTREAM_FORMATTER(dlinear::Config);
OSTREAM_FORMATTER(dlinear::Config::SatDefaultPhase);
OSTREAM_FORMATTER(dlinear::Config::LPSolver);
OSTREAM_FORMATTER(dlinear::Config::SatSolver);
OSTREAM_FORMATTER(dlinear::Config::Format);
OSTREAM_FORMATTER(dlinear::Config::LPMode);
OSTREAM_FORMATTER(dlinear::Config::BoundPropagationType);
OSTREAM_FORMATTER(dlinear::Config::PreprocessingRunningFrequency);
 
#endif