+++ /dev/null
-#
-# 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
projects / cvc5.git / commitdiff