diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-06 16:44:01 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-06 16:44:01 -0500 |
| commit | 45e489e2d48e3edde15be2187e32893fc35d859b (patch) | |
| tree | 6a6d267aefc48283a6c5de4b4f7b2f87abd23367 /contrib | |
| parent | 49c5a2aef84d1c17b4401eae9c60a92190b0b5a7 (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 'contrib')
| -rw-r--r-- | contrib/cvc4_strict_smtlib | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/contrib/cvc4_strict_smtlib b/contrib/cvc4_strict_smtlib new file mode 100644 index 000000000..0a97bd74b --- /dev/null +++ b/contrib/cvc4_strict_smtlib @@ -0,0 +1,8 @@ +#!/bin/bash + +cvc4="${CVC4_HOME}/cvc4" + +# This is the set of command line arguments that is required to be strictly +# complaint with the input and output requirements of the current SMT-LIB +# standard. +"$cvc4" --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --abstract-values $@ |