src/smt/options

   1 #
   2 # Option specification file for CVC4
   3 # See src/options/base_options for a description of this file format
   4 #
   5
   6 module SMT "smt/options.h" SMT layer
   7
   8 common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h"
   9  dump preprocessed assertions, etc., see --dump=help
  10 common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h"
  11  all dumping goes to FILE (instead of stdout)
  12
  13 option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h"
  14  choose simplification mode, see --simplification=help
  15 alias --no-simplification = --simplification=none
  16  turn off all simplification (same as --simplification=none)
  17
  18 option doStaticLearning static-learning --static-learning bool :default true
  19  use static learning (on by default)
  20
  21 option expandDefinitions expand-definitions bool :default false
  22  always expand symbol definitions in output
  23 common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  24  support the get-value and get-model commands
  25 option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  26  after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
  27 option dumpModels --dump-models bool :default false
  28  output models after every SAT/INVALID/UNKNOWN response
  29 option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  30  turn on proof generation
  31 # this is just a placeholder for later; it doesn't show up in command-line options listings
  32 undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  33  turn on unsat core generation (NOT YET SUPPORTED)
  34 option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  35  support the get-assignment command
  36
  37 # This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
  38 # is a mode in which the assertion list must be kept.  So it belongs here.
  39 common-option interactive interactive-mode --interactive bool :read-write
  40  force interactive mode
  41
  42 option doITESimp --ite-simp bool :read-write
  43  turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
  44
  45 option doITESimpOnRepeat --on-repeat-ite-simp bool :read-write :default false
  46  do the ite simplification pass again if repeating simplification
  47
  48 option simplifyWithCareEnabled --simp-with-care bool :default false :read-write
  49  enables simplifyWithCare in ite simplificiation
  50
  51 option compressItes --simp-ite-compress bool :default false :read-write
  52  enables compressing ites after ite simplification
  53
  54 option unconstrainedSimp --unconstrained-simp bool :default false :read-write
  55  turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
  56
  57 option repeatSimp --repeat-simp bool :read-write
  58  make multiple passes with nonclausal simplifier
  59
  60 option zombieHuntThreshold --simp-ite-hunt-zombies uint32_t :default 524288
  61  post ite compression enables zombie removal while the number of nodes is above this threshold
  62
  63 option sortInference --sort-inference bool :read-write :default false
  64  calculate sort inference of input problem, convert the input based on monotonic sorts
  65
  66 common-option incrementalSolving incremental -i --incremental bool :default true
  67  enable incremental solving
  68
  69 option abstractValues abstract-values --abstract-values bool :default false
  70  in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard
  71 option modelUninterpDtEnum --model-u-dt-enum bool :default false
  72  in models, output uninterpreted sorts as datatype enumerations
  73
  74 option - regular-output-channel argument :handler CVC4::smt::setRegularOutputChannel :handler-include "smt/options_handlers.h"
  75  set the regular output channel of the solver
  76 option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h"
  77  set the diagnostic output channel of the solver
  78
  79 common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long"
  80  enable time limiting (give milliseconds)
  81 common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long"
  82  enable time limiting per query (give milliseconds)
  83 common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long"
  84  enable resource limiting (currently, roughly the number of SAT conflicts)
  85 common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long"
  86  enable resource limiting per query
  87
  88 # --replay is currently broken; don't document it for 1.0
  89 undocumented-option replayFilename --replay=FILE std::string :handler CVC4::smt::checkReplayFilename :handler-include "smt/options_handlers.h"
  90  replay decisions from file
  91 undocumented-option replayLog --replay-log=FILE std::ostream* :handler CVC4::smt::checkReplayLogFilename :handler-include "smt/options_handlers.h"
  92  log decisions and propagations to file
  93 option replayStream ExprStream*
  94
  95 # portfolio options
  96 option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_input_channel.h"
  97  The input channel to receive notfication events for new lemmas
  98 option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"
  99  The output channel to receive notfication events for new lemmas
 100
 101 endmodule