diff --git a/boolector.cabal b/boolector.cabal --- a/boolector.cabal +++ b/boolector.cabal @@ -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: diff --git a/src/Boolector/Foreign.chs b/src/Boolector/Foreign.chs --- a/src/Boolector/Foreign.chs +++ b/src/Boolector/Foreign.chs @@ -201,97 +201,100 @@ -- | Solver option. -- See {# 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 ) #}