1 /* Boolector: Satisfiability Modulo Theories (SMT) solver. 2 * 3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file. 4 * 5 * This file is part of Boolector. 6 * See COPYING for more information on using this software. 7 */ 8 9 #ifndef BTOROPTS_H_INCLUDED 10 #define BTOROPTS_H_INCLUDED 11 12 #include <stdbool.h> 13 #include <stdint.h> 14 #include "btortypes.h" 15 #include "utils/btorhashptr.h" 16 #include "utils/btormem.h" 17 18 /*------------------------------------------------------------------------*/ 19 20 struct BtorOpt 21 { 22 bool internal; /* internal option? */ 23 bool isflag; /* flag? */ 24 const char *shrt; /* short option identifier (may be 0) */ 25 const char *lng; /* long option identifier */ 26 const char *desc; /* description */ 27 uint32_t val; /* value */ 28 uint32_t dflt; /* default value */ 29 uint32_t min; /* min value */ 30 uint32_t max; /* max value */ 31 char *valstr; /* optional option string value */ 32 BtorPtrHashTable *options; /* maps option CL value strings to enum values */ 33 }; 34 typedef struct BtorOpt BtorOpt; 35 36 /*------------------------------------------------------------------------*/ 37 38 /** 39 * Represents the data required to print help messages for options that 40 * expect an enum value rather than an (u)int value. This is mainly needed 41 * for invoking the solver via the command line (with '--<opt>=help'). 42 */ 43 struct BtorOptHelp 44 { 45 int32_t val; /* the enum value */ 46 const char *msg; /* the help message */ 47 }; 48 typedef struct BtorOptHelp BtorOptHelp; 49 50 /*------------------------------------------------------------------------*/ 51 52 /* enum BtorOption is in btortypes.h */ 53 54 #define BTOR_OPT_NUM_OPTS_STR "end_of_options_marker" 55 #define BTOR_OPT_INVALID_OPT_STR "invalid_option" 56 57 /*------------------------------------------------------------------------*/ 58 59 #define BTOR_VERBOSITY_MAX 4 60 61 #define BTOR_PROB_MAX 1000 62 63 /* enums for option values are defined in btortypes.h */ 64 65 #define BTOR_SAT_ENGINE_MIN BTOR_SAT_ENGINE_LINGELING 66 #define BTOR_SAT_ENGINE_MAX BTOR_SAT_ENGINE_CMS 67 #ifdef BTOR_USE_CADICAL 68 #define BTOR_SAT_ENGINE_DFLT BTOR_SAT_ENGINE_CADICAL 69 #elif BTOR_USE_LINGELING 70 #define BTOR_SAT_ENGINE_DFLT BTOR_SAT_ENGINE_LINGELING 71 #elif BTOR_USE_PICOSAT 72 #define BTOR_SAT_ENGINE_DFLT BTOR_SAT_ENGINE_PICOSAT 73 #elif BTOR_USE_MINISAT 74 #define BTOR_SAT_ENGINE_DFLT BTOR_SAT_ENGINE_MINISAT 75 #elif BTOR_USE_CMS 76 #define BTOR_SAT_ENGINE_DFLT BTOR_SAT_ENGINE_CMS 77 #endif 78 extern const char *const g_btor_se_name[BTOR_SAT_ENGINE_MAX + 1]; 79 80 #define BTOR_ENGINE_MIN BTOR_ENGINE_FUN 81 #define BTOR_ENGINE_MAX BTOR_ENGINE_QUANT 82 #define BTOR_ENGINE_DFLT BTOR_ENGINE_FUN 83 84 #define BTOR_INPUT_FORMAT_MIN BTOR_INPUT_FORMAT_NONE 85 #define BTOR_INPUT_FORMAT_MAX BTOR_INPUT_FORMAT_SMT2 86 #define BTOR_INPUT_FORMAT_DFLT BTOR_INPUT_FORMAT_NONE 87 88 #define BTOR_OUTPUT_BASE_MIN BTOR_OUTPUT_BASE_BIN 89 #define BTOR_OUTPUT_BASE_MAX BTOR_OUTPUT_BASE_DEC 90 #define BTOR_OUTPUT_BASE_DFLT BTOR_OUTPUT_BASE_BIN 91 92 #define BTOR_OUTPUT_FORMAT_MIN BTOR_OUTPUT_FORMAT_NONE 93 #define BTOR_OUTPUT_FORMAT_MAX BTOR_OUTPUT_FORMAT_AIGER_BINARY 94 #define BTOR_OUTPUT_FORMAT_DFLT BTOR_OUTPUT_FORMAT_NONE 95 96 #define BTOR_DP_QSORT_MIN BTOR_DP_QSORT_JUST 97 #define BTOR_DP_QSORT_MAX BTOR_DP_QSORT_DESC 98 #define BTOR_DP_QSORT_DFLT BTOR_DP_QSORT_JUST 99 100 #define BTOR_JUST_HEUR_MIN BTOR_JUST_HEUR_BRANCH_LEFT 101 #define BTOR_JUST_HEUR_MAX BTOR_JUST_HEUR_BRANCH_MIN_DEP 102 #define BTOR_JUST_HEUR_DFLT BTOR_JUST_HEUR_BRANCH_MIN_APP 103 104 #define BTOR_SLS_STRAT_MIN BTOR_SLS_STRAT_BEST_MOVE 105 #define BTOR_SLS_STRAT_MAX BTOR_SLS_STRAT_ALWAYS_PROP 106 #define BTOR_SLS_STRAT_DFLT BTOR_SLS_STRAT_BEST_MOVE 107 108 #define BTOR_PROP_PATH_SEL_MIN BTOR_PROP_PATH_SEL_CONTROLLING 109 #define BTOR_PROP_PATH_SEL_MAX BTOR_PROP_PATH_SEL_RANDOM 110 #define BTOR_PROP_PATH_SEL_DFLT BTOR_PROP_PATH_SEL_ESSENTIAL 111 112 #define BTOR_QUANT_SYNTH_MIN BTOR_QUANT_SYNTH_NONE 113 #define BTOR_QUANT_SYNTH_MAX BTOR_QUANT_SYNTH_ELMR 114 #define BTOR_QUANT_SYNTH_DFLT BTOR_QUANT_SYNTH_ELMR 115 116 #define BTOR_FUN_EAGER_LEMMAS_MIN BTOR_FUN_EAGER_LEMMAS_NONE 117 #define BTOR_FUN_EAGER_LEMMAS_MAX BTOR_FUN_EAGER_LEMMAS_ALL 118 #define BTOR_FUN_EAGER_LEMMAS_DFLT BTOR_FUN_EAGER_LEMMAS_CONF 119 120 #define BTOR_INCREMENTAL_SMT1_MIN BTOR_INCREMENTAL_SMT1_BASIC 121 #define BTOR_INCREMENTAL_SMT1_MAX BTOR_INCREMENTAL_SMT1_CONTINUE 122 #define BTOR_INCREMENTAL_SMT1_DFLT BTOR_INCREMENTAL_SMT1_BASIC 123 124 #define BTOR_BETA_REDUCE_MIN BTOR_BETA_REDUCE_NONE 125 #define BTOR_BETA_REDUCE_MAX BTOR_BETA_REDUCE_ALL 126 #define BTOR_BETA_REDUCE_DFLT BTOR_BETA_REDUCE_NONE 127 128 /*------------------------------------------------------------------------*/ 129 130 void btor_opt_init_opts (Btor *btor); 131 void btor_opt_clone_opts (Btor *btor, Btor *clone); 132 void btor_opt_delete_opts (Btor *btor); 133 134 bool btor_opt_is_valid (const Btor *btor, const BtorOption opt); 135 136 uint32_t btor_opt_get (const Btor *btor, const BtorOption opt); 137 uint32_t btor_opt_get_min (const Btor *btor, const BtorOption opt); 138 uint32_t btor_opt_get_max (const Btor *btor, const BtorOption opt); 139 uint32_t btor_opt_get_dflt (const Btor *btor, const BtorOption opt); 140 const char *btor_opt_get_lng (const Btor *btor, const BtorOption opt); 141 const char *btor_opt_get_shrt (const Btor *btor, const BtorOption opt); 142 const char *btor_opt_get_desc (const Btor *btor, const BtorOption opt); 143 const char *btor_opt_get_valstr (const Btor *btor, const BtorOption opt); 144 145 void btor_opt_set (Btor *btor, const BtorOption opt, uint32_t val); 146 void btor_opt_set_str (Btor *btor, const BtorOption opt, const char *str); 147 148 BtorOption btor_opt_first (Btor *btor); 149 BtorOption btor_opt_next (Btor *btor, BtorOption cur); 150 151 #ifndef NBTORLOG 152 void btor_opt_log_opts (Btor *btor); 153 #endif 154 #endif 155