summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDeianStefan <>2020-01-12 03:44:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2020-01-12 03:44:00 (GMT)
commitbf2a26dc5a6abcda1f4af6553192e6d8ff25d933 (patch)
tree856736142ac71344505086d49bf943bc8b193454
parentda62e8335faef02ae6f3ff99c7c977929e44c483 (diff)
version 0.0.0.100.0.0.10
-rw-r--r--boolector.cabal2
-rw-r--r--src/Boolector/Foreign.chs185
2 files changed, 95 insertions, 92 deletions
diff --git a/boolector.cabal b/boolector.cabal
index 020c819..f26223a 100644
--- 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
index 30c0575..f07d322 100644
--- a/src/Boolector/Foreign.chs
+++ b/src/Boolector/Foreign.chs
@@ -201,97 +201,100 @@ deriving instance Ord Sort
-- | 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 ) #}