summaryrefslogtreecommitdiff
path: root/src/options/base_options.toml
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-04-06 16:44:01 -0500
committerGitHub <noreply@github.com>2020-04-06 16:44:01 -0500
commit45e489e2d48e3edde15be2187e32893fc35d859b (patch)
tree6a6d267aefc48283a6c5de4b4f7b2f87abd23367 /src/options/base_options.toml
parent49c5a2aef84d1c17b4401eae9c60a92190b0b5a7 (diff)
Remove links field in all toml files (#4201)
This includes: All options pertaining to SMTEngine are now handled at the top of setDefaults. smtlibStrict was deleted in favor of a script. statsEveryQuery enables stats by modifying a public option function. This is a slight hack but this code will likely get refactored as well soon. A few other changes: Fix a bug in SMTEngine: defineFunction should finalize options. Call setDefaults before initilizing the TheoryEngine and ProofManager. This is necessary so that the PROOF(...) macro works earlier during initialization. The next step will be to remove the links infrastructure for the options infrastructure. This will enable further detangling of our options dependencies.
Diffstat (limited to 'src/options/base_options.toml')
-rw-r--r--src/options/base_options.toml7
1 files changed, 0 insertions, 7 deletions
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 43060bc54..65eeda3ae 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -99,7 +99,6 @@ header = "options/base_options.h"
long = "stats-every-query"
type = "bool"
default = "false"
- links = ["--stats"]
read_only = true
help = "in incremental mode, print stats after every satisfiability or validity query"
@@ -155,9 +154,3 @@ header = "options/base_options.h"
notifies = ["notifyPrintSuccess"]
read_only = true
help = "print the \"success\" output required of SMT-LIBv2"
-
-[[alias]]
- category = "regular"
- long = "smtlib-strict"
- links = ["--lang=smt2", "--output-lang=smt2", "--strict-parsing", "--default-expr-depth=-1", "--print-success", "--incremental", "--abstract-values"]
- help = "SMT-LIBv2 compliance mode (implies other options)"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback