boolector 0.0.0.9 → 0.0.0.10

raw patch · 2 files changed

+95/−92 lines, 2 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• boolector.cabal +1/−1
• src/Boolector/Foreign.chs +94/−91

@@ -1,5 +1,5 @@ name:                boolector-version:             0.0.0.9+version:             0.0.0.10 synopsis:            Haskell bindings for the Boolector SMT solver description: 

@@ -201,97 +201,100 @@ -- | Solver option. -- See <https://github.com/Boolector/boolector/blob/47f94b39fb6e099195da043ddaf8d82e4b2aebc9/src/btortypes.h#L37> {# enum define Option {-BTOR_OPT_MODEL_GEN                     as OPT_MODEL_GEN,-BTOR_OPT_INCREMENTAL                   as OPT_INCREMENTAL,-BTOR_OPT_INCREMENTAL_SMT1              as OPT_INCREMENTAL_SMT1,-BTOR_OPT_INPUT_FORMAT                  as OPT_INPUT_FORMAT,-BTOR_OPT_OUTPUT_NUMBER_FORMAT          as OPT_OUTPUT_NUMBER_FORMAT,-BTOR_OPT_OUTPUT_FORMAT                 as OPT_OUTPUT_FORMAT,-BTOR_OPT_ENGINE                        as OPT_ENGINE,-BTOR_OPT_SAT_ENGINE                    as OPT_SAT_ENGINE,-BTOR_OPT_AUTO_CLEANUP                  as OPT_AUTO_CLEANUP,-BTOR_OPT_PRETTY_PRINT                  as OPT_PRETTY_PRINT,-BTOR_OPT_EXIT_CODES                    as OPT_EXIT_CODES,-BTOR_OPT_SEED                          as OPT_SEED,-BTOR_OPT_VERBOSITY                     as OPT_VERBOSITY,-BTOR_OPT_LOGLEVEL                      as OPT_LOGLEVEL,-BTOR_OPT_REWRITE_LEVEL                 as OPT_REWRITE_LEVEL,-BTOR_OPT_SKELETON_PREPROC              as OPT_SKELETON_PREPROC,-BTOR_OPT_ACKERMANN                     as OPT_ACKERMANN,-BTOR_OPT_BETA_REDUCE_ALL               as OPT_BETA_REDUCE_ALL,-BTOR_OPT_ELIMINATE_SLICES              as OPT_ELIMINATE_SLICES,-BTOR_OPT_VAR_SUBST                     as OPT_VAR_SUBST,-BTOR_OPT_UCOPT                         as OPT_UCOPT,-BTOR_OPT_MERGE_LAMBDAS                 as OPT_MERGE_LAMBDAS,-BTOR_OPT_EXTRACT_LAMBDAS               as OPT_EXTRACT_LAMBDAS,-BTOR_OPT_NORMALIZE                     as OPT_NORMALIZE,-BTOR_OPT_NORMALIZE_ADD                 as OPT_NORMALIZE_ADD,-BTOR_OPT_FUN_PREPROP                   as OPT_FUN_PREPROP,-BTOR_OPT_FUN_PRESLS                    as OPT_FUN_PRESLS,-BTOR_OPT_FUN_DUAL_PROP                 as OPT_FUN_DUAL_PROP,-BTOR_OPT_FUN_DUAL_PROP_QSORT           as OPT_FUN_DUAL_PROP_QSORT,-BTOR_OPT_FUN_JUST                      as OPT_FUN_JUST,-BTOR_OPT_FUN_JUST_HEURISTIC            as OPT_FUN_JUST_HEURISTIC,-BTOR_OPT_FUN_LAZY_SYNTHESIZE           as OPT_FUN_LAZY_SYNTHESIZE,-BTOR_OPT_FUN_EAGER_LEMMAS              as OPT_FUN_EAGER_LEMMAS,-BTOR_OPT_FUN_STORE_LAMBDAS             as OPT_FUN_STORE_LAMBDAS,-BTOR_OPT_SLS_NFLIPS                    as OPT_SLS_NFLIPS,-BTOR_OPT_SLS_STRATEGY                  as OPT_SLS_STRATEGY,-BTOR_OPT_SLS_JUST                      as OPT_SLS_JUST,-BTOR_OPT_SLS_MOVE_GW                   as OPT_SLS_MOVE_GW,-BTOR_OPT_SLS_MOVE_RANGE                as OPT_SLS_MOVE_RANGE,-BTOR_OPT_SLS_MOVE_SEGMENT              as OPT_SLS_MOVE_SEGMENT,-BTOR_OPT_SLS_MOVE_RAND_WALK            as OPT_SLS_MOVE_RAND_WALK,-BTOR_OPT_SLS_PROB_MOVE_RAND_WALK       as OPT_SLS_PROB_MOVE_RAND_WALK,-BTOR_OPT_SLS_MOVE_RAND_ALL             as OPT_SLS_MOVE_RAND_ALL,-BTOR_OPT_SLS_MOVE_RAND_RANGE           as OPT_SLS_MOVE_RAND_RANGE,-BTOR_OPT_SLS_MOVE_PROP                 as OPT_SLS_MOVE_PROP,-BTOR_OPT_SLS_MOVE_PROP_N_PROP          as OPT_SLS_MOVE_PROP_N_PROP,-BTOR_OPT_SLS_MOVE_PROP_N_SLS           as OPT_SLS_MOVE_PROP_N_SLS,-BTOR_OPT_SLS_MOVE_PROP_FORCE_RW        as OPT_SLS_MOVE_PROP_FORCE_RW,-BTOR_OPT_SLS_MOVE_INC_MOVE_TEST        as OPT_SLS_MOVE_INC_MOVE_TEST,-BTOR_OPT_SLS_USE_RESTARTS              as OPT_SLS_USE_RESTARTS,-BTOR_OPT_SLS_USE_BANDIT                as OPT_SLS_USE_BANDIT,-BTOR_OPT_PROP_NPROPS                   as OPT_PROP_NPROPS,-BTOR_OPT_PROP_USE_RESTARTS             as OPT_PROP_USE_RESTARTS,-BTOR_OPT_PROP_USE_BANDIT               as OPT_PROP_USE_BANDIT,-BTOR_OPT_PROP_PATH_SEL                 as OPT_PROP_PATH_SEL,-BTOR_OPT_PROP_PROB_USE_INV_VALUE       as OPT_PROP_PROB_USE_INV_VALUE,-BTOR_OPT_PROP_PROB_FLIP_COND           as OPT_PROP_PROB_FLIP_COND,-BTOR_OPT_PROP_PROB_FLIP_COND_CONST     as OPT_PROP_PROB_FLIP_COND_CONST,-BTOR_OPT_PROP_FLIP_COND_CONST_DELTA    as OPT_PROP_FLIP_COND_CONST_DELTA,-BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL as OPT_PROP_FLIP_COND_CONST_NPATHSEL,-BTOR_OPT_PROP_PROB_SLICE_KEEP_DC       as OPT_PROP_PROB_SLICE_KEEP_DC,-BTOR_OPT_PROP_PROB_CONC_FLIP           as OPT_PROP_PROB_CONC_FLIP,-BTOR_OPT_PROP_PROB_SLICE_FLIP          as OPT_PROP_PROB_SLICE_FLIP,-BTOR_OPT_PROP_PROB_EQ_FLIP             as OPT_PROP_PROB_EQ_FLIP,-BTOR_OPT_PROP_PROB_AND_FLIP            as OPT_PROP_PROB_AND_FLIP,-BTOR_OPT_PROP_NO_MOVE_ON_CONFLICT      as OPT_PROP_NO_MOVE_ON_CONFLICT,-BTOR_OPT_AIGPROP_USE_RESTARTS          as OPT_AIGPROP_USE_RESTARTS,-BTOR_OPT_AIGPROP_USE_BANDIT            as OPT_AIGPROP_USE_BANDIT,-BTOR_OPT_QUANT_SYNTH                   as OPT_QUANT_SYNTH,-BTOR_OPT_QUANT_DUAL_SOLVER             as OPT_QUANT_DUAL_SOLVER,-BTOR_OPT_QUANT_SYNTH_LIMIT             as OPT_QUANT_SYNTH_LIMIT,-BTOR_OPT_QUANT_SYNTH_ITE_COMPLETE      as OPT_QUANT_SYNTH_ITE_COMPLETE,-BTOR_OPT_QUANT_FIXSYNTH                as OPT_QUANT_FIXSYNTH,-BTOR_OPT_QUANT_SYNTH_QI                as OPT_QUANT_SYNTH_QI,-BTOR_OPT_QUANT_DER                     as OPT_QUANT_DER,-BTOR_OPT_QUANT_CER                     as OPT_QUANT_CER,-BTOR_OPT_QUANT_MINISCOPE               as OPT_QUANT_MINISCOPE,-BTOR_OPT_DEFAULT_TO_CADICAL            as OPT_DEFAULT_TO_CADICAL,-BTOR_OPT_SORT_EXP                      as OPT_SORT_EXP,-BTOR_OPT_SORT_AIG                      as OPT_SORT_AIG,-BTOR_OPT_SORT_AIGVEC                   as OPT_SORT_AIGVEC,-BTOR_OPT_AUTO_CLEANUP_INTERNAL         as OPT_AUTO_CLEANUP_INTERNAL,-BTOR_OPT_SIMPLIFY_CONSTRAINTS          as OPT_SIMPLIFY_CONSTRAINTS,-BTOR_OPT_CHK_FAILED_ASSUMPTIONS        as OPT_CHK_FAILED_ASSUMPTIONS,-BTOR_OPT_CHK_MODEL                     as OPT_CHK_MODEL,-BTOR_OPT_CHK_UNCONSTRAINED             as OPT_CHK_UNCONSTRAINED,-BTOR_OPT_PARSE_INTERACTIVE             as OPT_PARSE_INTERACTIVE,-BTOR_OPT_SAT_ENGINE_LGL_FORK           as OPT_SAT_ENGINE_LGL_FORK,-BTOR_OPT_INCREMENTAL_RW                as OPT_INCREMENTAL_RW,-BTOR_OPT_DECLSORT_BV_WIDTH             as OPT_DECLSORT_BV_WIDTH,-BTOR_OPT_NUM_OPTS                      as OPT_NUM_OPTS+  BTOR_OPT_MODEL_GEN as OPT_MODEL_GEN,+  BTOR_OPT_INCREMENTAL as OPT_INCREMENTAL,+  BTOR_OPT_INCREMENTAL_SMT1 as OPT_INCREMENTAL_SMT1,+  BTOR_OPT_INPUT_FORMAT as OPT_INPUT_FORMAT,+  BTOR_OPT_OUTPUT_NUMBER_FORMAT as OPT_OUTPUT_NUMBER_FORMAT,+  BTOR_OPT_OUTPUT_FORMAT as OPT_OUTPUT_FORMAT,+  BTOR_OPT_ENGINE as OPT_ENGINE,+  BTOR_OPT_SAT_ENGINE as OPT_SAT_ENGINE,+  BTOR_OPT_AUTO_CLEANUP as OPT_AUTO_CLEANUP,+  BTOR_OPT_PRETTY_PRINT as OPT_PRETTY_PRINT,+  BTOR_OPT_EXIT_CODES as OPT_EXIT_CODES,+  BTOR_OPT_SEED as OPT_SEED,+  BTOR_OPT_VERBOSITY as OPT_VERBOSITY,+  BTOR_OPT_LOGLEVEL as OPT_LOGLEVEL,+  BTOR_OPT_REWRITE_LEVEL as OPT_REWRITE_LEVEL,+  BTOR_OPT_SKELETON_PREPROC as OPT_SKELETON_PREPROC,+  BTOR_OPT_ACKERMANN as OPT_ACKERMANN,+  BTOR_OPT_BETA_REDUCE as OPT_BETA_REDUCE,+  BTOR_OPT_ELIMINATE_SLICES as OPT_ELIMINATE_SLICES,+  BTOR_OPT_VAR_SUBST as OPT_VAR_SUBST,+  BTOR_OPT_UCOPT as OPT_UCOPT,+  BTOR_OPT_MERGE_LAMBDAS as OPT_MERGE_LAMBDAS,+  BTOR_OPT_EXTRACT_LAMBDAS as OPT_EXTRACT_LAMBDAS,+  BTOR_OPT_NORMALIZE as OPT_NORMALIZE,+  BTOR_OPT_NORMALIZE_ADD as OPT_NORMALIZE_ADD,+  BTOR_OPT_FUN_PREPROP as OPT_FUN_PREPROP,+  BTOR_OPT_FUN_PRESLS as OPT_FUN_PRESLS,+  BTOR_OPT_FUN_DUAL_PROP as OPT_FUN_DUAL_PROP,+  BTOR_OPT_FUN_DUAL_PROP_QSORT as OPT_FUN_DUAL_PROP_QSORT,+  BTOR_OPT_FUN_JUST as OPT_FUN_JUST,+  BTOR_OPT_FUN_JUST_HEURISTIC as OPT_FUN_JUST_HEURISTIC,+  BTOR_OPT_FUN_LAZY_SYNTHESIZE as OPT_FUN_LAZY_SYNTHESIZE,+  BTOR_OPT_FUN_EAGER_LEMMAS as OPT_FUN_EAGER_LEMMAS,+  BTOR_OPT_FUN_STORE_LAMBDAS as OPT_FUN_STORE_LAMBDAS,+  BTOR_OPT_SLS_NFLIPS as OPT_SLS_NFLIPS,+  BTOR_OPT_SLS_STRATEGY as OPT_SLS_STRATEGY,+  BTOR_OPT_SLS_JUST as OPT_SLS_JUST,+  BTOR_OPT_SLS_MOVE_GW as OPT_SLS_MOVE_GW,+  BTOR_OPT_SLS_MOVE_RANGE as OPT_SLS_MOVE_RANGE,+  BTOR_OPT_SLS_MOVE_SEGMENT as OPT_SLS_MOVE_SEGMENT,+  BTOR_OPT_SLS_MOVE_RAND_WALK as OPT_SLS_MOVE_RAND_WALK,+  BTOR_OPT_SLS_PROB_MOVE_RAND_WALK as OPT_SLS_PROB_MOVE_RAND_WALK,+  BTOR_OPT_SLS_MOVE_RAND_ALL as OPT_SLS_MOVE_RAND_ALL,+  BTOR_OPT_SLS_MOVE_RAND_RANGE as OPT_SLS_MOVE_RAND_RANGE,+  BTOR_OPT_SLS_MOVE_PROP_N_SLS as OPT_SLS_MOVE_PROP_N_SLS,+  BTOR_OPT_SLS_MOVE_PROP as OPT_SLS_MOVE_PROP,+  BTOR_OPT_SLS_MOVE_PROP_N_PROP as OPT_SLS_MOVE_PROP_N_PROP,+  BTOR_OPT_SLS_MOVE_PROP_FORCE_RW as OPT_SLS_MOVE_PROP_FORCE_RW,+  BTOR_OPT_SLS_MOVE_INC_MOVE_TEST as OPT_SLS_MOVE_INC_MOVE_TEST,+  BTOR_OPT_SLS_USE_RESTARTS as OPT_SLS_USE_RESTARTS,+  BTOR_OPT_SLS_USE_BANDIT as OPT_SLS_USE_BANDIT,+  BTOR_OPT_PROP_NPROPS as OPT_PROP_NPROPS,+  BTOR_OPT_PROP_USE_RESTARTS as OPT_PROP_USE_RESTARTS,+  BTOR_OPT_PROP_USE_BANDIT as OPT_PROP_USE_BANDIT,+  BTOR_OPT_PROP_PATH_SEL as OPT_PROP_PATH_SEL,+  BTOR_OPT_PROP_PROB_USE_INV_VALUE as OPT_PROP_PROB_USE_INV_VALUE,+  BTOR_OPT_PROP_PROB_FLIP_COND as OPT_PROP_PROB_FLIP_COND,+  BTOR_OPT_PROP_PROB_FLIP_COND_CONST as OPT_PROP_PROB_FLIP_COND_CONST,+  BTOR_OPT_PROP_FLIP_COND_CONST_DELTA as OPT_PROP_FLIP_COND_CONST_DELTA,+  BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL as OPT_PROP_FLIP_COND_CONST_NPATHSEL,+  BTOR_OPT_PROP_PROB_SLICE_KEEP_DC as OPT_PROP_PROB_SLICE_KEEP_DC,+  BTOR_OPT_PROP_PROB_CONC_FLIP as OPT_PROP_PROB_CONC_FLIP,+  BTOR_OPT_PROP_PROB_SLICE_FLIP as OPT_PROP_PROB_SLICE_FLIP,+  BTOR_OPT_PROP_PROB_EQ_FLIP as OPT_PROP_PROB_EQ_FLIP,+  BTOR_OPT_PROP_PROB_AND_FLIP as OPT_PROP_PROB_AND_FLIP,+  BTOR_OPT_PROP_NO_MOVE_ON_CONFLICT as OPT_PROP_NO_MOVE_ON_CONFLICT,+  BTOR_OPT_AIGPROP_USE_RESTARTS as OPT_AIGPROP_USE_RESTARTS,+  BTOR_OPT_AIGPROP_USE_BANDIT as OPT_AIGPROP_USE_BANDIT,+  BTOR_OPT_QUANT_SYNTH as OPT_QUANT_SYNTH,+  BTOR_OPT_QUANT_DUAL_SOLVER as OPT_QUANT_DUAL_SOLVER,+  BTOR_OPT_QUANT_SYNTH_LIMIT as OPT_QUANT_SYNTH_LIMIT,+  BTOR_OPT_QUANT_SYNTH_QI as OPT_QUANT_SYNTH_QI,+  BTOR_OPT_QUANT_DER as OPT_QUANT_DER,+  BTOR_OPT_QUANT_CER as OPT_QUANT_CER,+  BTOR_OPT_QUANT_MINISCOPE as OPT_QUANT_MINISCOPE,+  BTOR_OPT_SORT_EXP as OPT_SORT_EXP,+  BTOR_OPT_SORT_AIG as OPT_SORT_AIG,+  BTOR_OPT_SORT_AIGVEC as OPT_SORT_AIGVEC,+  BTOR_OPT_AUTO_CLEANUP_INTERNAL as OPT_AUTO_CLEANUP_INTERNAL,+  BTOR_OPT_SIMPLIFY_CONSTRAINTS as OPT_SIMPLIFY_CONSTRAINTS,+  BTOR_OPT_CHK_FAILED_ASSUMPTIONS as OPT_CHK_FAILED_ASSUMPTIONS,+  BTOR_OPT_CHK_MODEL as OPT_CHK_MODEL,+  BTOR_OPT_CHK_UNCONSTRAINED as OPT_CHK_UNCONSTRAINED,+  BTOR_OPT_PARSE_INTERACTIVE as OPT_PARSE_INTERACTIVE,+  BTOR_OPT_SAT_ENGINE_LGL_FORK as OPT_SAT_ENGINE_LGL_FORK,+  BTOR_OPT_SAT_ENGINE_CADICAL_FREEZE as OPT_SAT_ENGINE_CADICAL_FREEZE,+  BTOR_OPT_SAT_ENGINE_N_THREADS as OPT_SAT_ENGINE_N_THREADS,+  BTOR_OPT_SIMP_NORMAMLIZE_ADDERS as OPT_SIMP_NORMAMLIZE_ADDERS,+  BTOR_OPT_DECLSORT_BV_WIDTH as OPT_DECLSORT_BV_WIDTH,+  BTOR_OPT_QUANT_SYNTH_ITE_COMPLETE as OPT_QUANT_SYNTH_ITE_COMPLETE,+  BTOR_OPT_QUANT_FIXSYNTH as OPT_QUANT_FIXSYNTH,+  BTOR_OPT_RW_ZERO_LOWER_SLICE as OPT_RW_ZERO_LOWER_SLICE,+  BTOR_OPT_NONDESTR_SUBST as OPT_NONDESTR_SUBST,+  BTOR_OPT_NUM_OPTS as OPT_NUM_OPTS } deriving (Eq, Ord, Show ) #}