diff options
Diffstat (limited to 'src/smt/options')
| -rw-r--r-- | src/smt/options | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/smt/options b/src/smt/options index 69b5102de..b76822caf 100644 --- a/src/smt/options +++ b/src/smt/options @@ -22,14 +22,16 @@ option expandDefinitions expand-definitions bool :default false always expand symbol definitions in output common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h" support the get-value and get-model commands -option checkProofs check-proofs --check-proofs bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" - after UNSAT/VALID, machine-check the generated proof -option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" +option checkModels check-models --check-models bool :link --produce-models --interactive :link-smt produce-models :link-smt interactive-mode :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions -option dumpModels --dump-models bool :default false +option dumpModels --dump-models bool :default false :link --produce-models output models after every SAT/INVALID/UNKNOWN response option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on proof generation +option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + after UNSAT/VALID, machine-check the generated proof +option dumpProofs --dump-proofs bool :default false :link --proof + output proofs after every UNSAT/VALID response # this is just a placeholder for later; it doesn't show up in command-line options listings undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on unsat core generation (NOT YET SUPPORTED) |