diff options
| -rw-r--r-- | src/options/smt_options | 185 |
1 files changed, 0 insertions, 185 deletions
diff --git a/src/options/smt_options b/src/options/smt_options deleted file mode 100644 index 811cc5a71..000000000 --- a/src/options/smt_options +++ /dev/null @@ -1,185 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module SMT "options/smt_options.h" SMT layer - -common-option dumpModeString dump --dump=MODE std::string :default "" :notify notifyDumpMode - dump preprocessed assertions, etc., see --dump=help -common-option dumpToFileName dump-to --dump-to=FILE std::string :notify notifyDumpToFile - all dumping goes to FILE (instead of stdout) - -expert-option forceLogicString force-logic --force-logic=LOGIC std::string :default "" :notify notifyForceLogic - set the logic, and override all further user attempts to change it - -option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "options/simplification_mode.h" - choose simplification mode, see --simplification=help -alias --no-simplification = --simplification=none - turn off all simplification (same as --simplification=none) - -option doStaticLearning static-learning --static-learning bool :default true - use static learning (on by default) - -option expandDefinitions expand-definitions bool :default false - always expand symbol definitions in output -common-option produceModels produce-models -m --produce-models bool :default false :notify notifyBeforeSearch - support the get-value and get-model commands -option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :notify notifyBeforeSearch - after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions -option dumpModels --dump-models bool :default false :link --produce-models :link-smt produce-models - output models after every SAT/INVALID/UNKNOWN response -option omitDontCares --omit-dont-cares bool :default false - When producing a model, omit variables whose value does not matter -option proof produce-proofs --proof bool :default false :predicate proofEnabledBuild :notify notifyBeforeSearch - turn on proof generation -option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate LFSCEnabledBuild :notify notifyBeforeSearch :read-write - after UNSAT/VALID, machine-check the generated proof -option dumpProofs --dump-proofs bool :default false :link --proof :link-smt produce-proofs - output proofs after every UNSAT/VALID response -option dumpInstantiations --dump-instantiations bool :default false - output instantiations of quantified formulas after every UNSAT/VALID response -option sygusOut --sygus-out=MODE SygusSolutionOutMode :default SYGUS_SOL_OUT_STATUS_AND_DEF :include "options/sygus_out_mode.h" :handler stringToSygusSolutionOutMode :read-write - output mode for sygus -option sygusPrintCallbacks --sygus-print-callbacks bool :default true - use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging) -option dumpSynth --dump-synth bool :read-write :default false - output solution for synthesis conjectures after every UNSAT/VALID response -option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch - turn on unsat core generation -option checkUnsatCores check-unsat-cores --check-unsat-cores bool :link --produce-unsat-cores :link-smt produce-unsat-cores :read-write - after UNSAT/VALID, produce and check an unsat core (expensive) -option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :notify notifyBeforeSearch - output unsat cores after every UNSAT/VALID response -option dumpUnsatCoresFull dump-unsat-cores-full --dump-unsat-cores-full bool :default false :link --dump-unsat-cores :link-smt dump-unsat-cores :notify notifyBeforeSearch - dump the full unsat core, including unlabeled assertions - -option unsatAssumptions produce-unsat-assumptions --produce-unsat-assumptions bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate proofEnabledBuild :notify notifyBeforeSearch - turn on unsat assumptions generation - -option checkSynthSol --check-synth-sol bool :default false - checks whether produced solutions to functions-to-synthesize satisfy the conjecture - -option produceAssignments produce-assignments --produce-assignments bool :default false :notify notifyBeforeSearch - support the get-assignment command - -undocumented-option interactiveMode interactive-mode bool :predicate setProduceAssertions :read-write :notify notifyBeforeSearch - deprecated name for produce-assertions -common-option produceAssertions produce-assertions --produce-assertions bool :predicate setProduceAssertions :read-write :notify notifyBeforeSearch - keep an assertions list (enables get-assertions command) - -option doITESimp --ite-simp bool :read-write - turn on ite simplification (Kim (and Somenzi) et al., SAT 2009) - -option doITESimpOnRepeat --on-repeat-ite-simp bool :read-write :default false - do the ite simplification pass again if repeating simplification - -option extRewPrep --ext-rew-prep bool :read-write :default false - use extended rewriter as a preprocessing pass -option extRewPrepAgg --ext-rew-prep-agg bool :read-write :default false - use aggressive extended rewriter as a preprocessing pass - -option simplifyWithCareEnabled --simp-with-care bool :default false :read-write - enables simplifyWithCare in ite simplificiation - -option compressItes --simp-ite-compress bool :default false :read-write - enables compressing ites after ite simplification - -option unconstrainedSimp --unconstrained-simp bool :default false :read-write - turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis) - -option repeatSimp --repeat-simp bool :read-write - make multiple passes with nonclausal simplifier - -option zombieHuntThreshold --simp-ite-hunt-zombies uint32_t :default 524288 - post ite compression enables zombie removal while the number of nodes is above this threshold - -option sortInference --sort-inference bool :read-write :default false - calculate sort inference of input problem, convert the input based on monotonic sorts - -common-option incrementalSolving incremental -i --incremental bool :default true - enable incremental solving - -option abstractValues abstract-values --abstract-values bool :default false - in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard -option modelUninterpDtEnum --model-u-dt-enum bool :default false - in models, output uninterpreted sorts as datatype enumerations - -option regularChannelName regular-output-channel std::string :notify notifySetRegularOutputChannel - set the regular output channel of the solver -option diagnosticChannelName diagnostic-output-channel std::string :notify notifySetDiagnosticOutputChannel - set the diagnostic output channel of the solver - -common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler tlimitHandler :notify notifyTlimit - enable time limiting (give milliseconds) -common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" :handler tlimitPerHandler :notify notifyTlimitPer - enable time limiting per query (give milliseconds) -common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler rlimitHandler :notify notifyRlimit - enable resource limiting (currently, roughly the number of SAT conflicts) -common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler rlimitPerHandler :notify notifyRlimitPer - enable resource limiting per query -common-option hardLimit hard-limit --hard-limit bool :default false - the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out) -common-option cpuTime cpu-time --cpu-time bool :default false - measures CPU time if set to true and wall time if false (default false) - -# Resource spending options for SPARK -expert-option rewriteStep rewrite-step --rewrite-step unsigned :default 1 - amount of resources spent for each rewrite step - -expert-option theoryCheckStep theory-check-step --theory-check-step unsigned :default 1 - amount of resources spent for each theory check call - -expert-option decisionStep decision-step --decision-step unsigned :default 1 - amount of getNext decision calls in the decision engine - -expert-option bitblastStep bitblast-step --bitblast-step unsigned :default 1 - amount of resources spent for each bitblast step - -expert-option parseStep parse-step --parse-step unsigned :default 1 - amount of resources spent for each command/expression parsing - -expert-option lemmaStep lemma-step --lemma-step unsigned :default 1 - amount of resources spent when adding lemmas - -expert-option restartStep restart-step --restart-step unsigned :default 1 - amount of resources spent for each theory restart - -expert-option cnfStep cnf-step --cnf-step unsigned :default 1 - amount of resources spent for each call to cnf conversion - -expert-option preprocessStep preprocess-step --preprocess-step unsigned :default 1 - amount of resources spent for each preprocessing step in SmtEngine - -expert-option quantifierStep quantifier-step --quantifier-step unsigned :default 1 - amount of resources spent for quantifier instantiations - -expert-option satConflictStep sat-conflict-step --sat-conflict-step unsigned :default 1 - amount of resources spent for each sat conflict (main sat solver) - -expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsigned :default 1 - amount of resources spent for each sat conflict (bitvectors) - - -expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false - eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 - - -# --replay is currently broken; don't document it for 1.0 -undocumented-option replayInputFilename --replay=FILE std::string :handler checkReplayFilename - replay decisions from file - -# --replay is currently broken; don't document it for 1.0 -undocumented-option replayLogFilename --replay-log=FILE std::string :handler checkReplayFilename :notify notifySetReplayLogFilename :notify notifyBeforeSearch - replay decisions from file - -option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false - Force no CPU limit when dumping models and proofs - -undocumented-option solveIntAsBV --solve-int-as-bv uint32_t :default 0 - attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental) - -undocumented-option solveRealAsInt --solve-real-as-int bool :default false - attempt to solve a pure real satisfiable problem as a integer problem (for non-linear) - -endmodule |