Merge branch '1.4.x'

[cvc5.git] / src / smt / options

diff --git a/src/smt/options b/src/smt/options
index 873aec6d1f5c9ffa61ab7018558e1cc98490c82e..3ee3dbecbee510085bba0a53de2664c17e377196 100644 (file)
--- a/src/smt/options
+++ b/src/smt/options
@@ -5,9 +5,9 @@
 
 module SMT "smt/options.h" SMT layer
 
-common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h"
+common-option - dump --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h"
  dump preprocessed assertions, etc., see --dump=help
-common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h"
+common-option - dump-to --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h"
  all dumping goes to FILE (instead of stdout)
 
 expert-option forceLogic force-logic --force-logic=LOGIC LogicInfo :include "theory/logic_info.h" :handler CVC4::smt::stringToLogicInfo :handler-include "smt/options_handlers.h" :default '""'
@@ -35,9 +35,13 @@ option checkProofs check-proofs --check-proofs bool :link --proof :link-smt prod
  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)
+option dumpInstantiations --dump-instantiations bool :default false
+ output instantiations of quantified formulas after every UNSAT/VALID response
+option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ turn on unsat core generation
+option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ output unsat cores after every UNSAT/VALID response
+
 option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  support the get-assignment command
 
@@ -108,4 +112,7 @@ option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_i
 option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"
  The output channel to receive notfication events for new lemmas
 
+option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false
+ Force no CPU limit when dumping models and proofs
+
 endmodule