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 # FIXME: need to add support for SMT-LIBv2-required options:
   7 #
   8 #   expand-definitions
   9 #   regular-output-channel
  10 #   diagnostic-output-channel
  11 #   produce-unsat-cores
  12 #
  13
  14 module SMT "smt/options.h" SMT layer
  15
  16 common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h"
  17  dump preprocessed assertions, etc., see --dump=help
  18 common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h"
  19  all dumping goes to FILE (instead of stdout)
  20
  21 expert-option lazyDefinitionExpansion --lazy-definition-expansion bool
  22  expand define-funs/LAMBDAs lazily
  23
  24 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"
  25  choose simplification mode, see --simplification=help
  26 alias --no-simplification = --simplification=none
  27  turn off all simplification (same as --simplification=none)
  28
  29 option doStaticLearning static-learning /--no-static-learning bool :default true
  30  use static learning (on by default)
  31 /turn off static learning (e.g. diamond-breaking)
  32
  33 common-option produceModels produce-models -m --produce-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h"
  34  support the get-value and get-model commands
  35 option checkModels check-models --check-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h"
  36  after SAT/INVALID, double-check that the generated model satisfies all user assertions
  37 common-option produceAssignments produce-assignments --produce-assignments bool
  38  support the get-assignment command
  39 option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::smt::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "smt/model_format_mode.h" :handler-include "smt/options_handlers.h"
  40  print format mode for models, see --model-format=help
  41
  42 # This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
  43 # is a mode in which the assertion list must be kept.  So it belongs here.
  44 common-option interactive interactive-mode --interactive bool :read-write
  45  force interactive mode
  46
  47 option doITESimp --ite-simp bool :read-write
  48  turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
  49 /turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)
  50
  51 option unconstrainedSimp --unconstrained-simp bool :default false :read-write
  52  turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
  53 /turn off unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
  54
  55 option repeatSimp --repeat-simp bool :read-write
  56  make multiple passes with nonclausal simplifier
  57 /do not make multiple passes with nonclausal simplifier
  58
  59 common-option incrementalSolving incremental -i --incremental bool
  60  enable incremental solving
  61
  62 option - regular-output-channel argument :handler CVC4::smt::setRegularOutputChannel :handler-include "smt/options_handlers.h"
  63  set the regular output channel of the solver
  64 option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h"
  65  set the diagnostic output channel of the solver
  66
  67 common-option cumulativeMillisecondLimit --tlimit=MS "unsigned long"
  68  enable time limiting (give milliseconds)
  69 common-option perCallMillisecondLimit --tlimit-per=MS "unsigned long"
  70  enable time limiting per query (give milliseconds)
  71 common-option cumulativeResourceLimit --rlimit=N "unsigned long"
  72  enable resource limiting
  73 common-option perCallResourceLimit --rlimit-per=N "unsigned long"
  74  enable resource limiting per query
  75
  76 option replayFilename --replay=FILE std::string :handler CVC4::smt::checkReplayFilename :handler-include "smt/options_handlers.h"
  77  replay decisions from file
  78 option replayLog --replay-log=FILE std::ostream* :handler CVC4::smt::checkReplayLogFilename :handler-include "smt/options_handlers.h"
  79  log decisions and propagations to file
  80 option replayStream ExprStream*
  81
  82 # portfolio options
  83 option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_input_channel.h"
  84  The input channel to receive notfication events for new lemmas
  85 option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"
  86  The output channel to receive notfication events for new lemmas
  87
  88 endmodule