diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-21 12:08:14 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-21 12:08:14 -0500 |
| commit | b8301cde27c455c8da3e9017072a577a0816939b (patch) | |
| tree | 816d1cccdda0625419b1b088644bafb85a857d14 /src/options/theory_options.toml | |
| parent | 905dc2b51fd0145e0bb69a166c06a1731ef4c44b (diff) | |
Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic (#4930)
This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this.
This addresses CVC4/cvc4-projects#113.
Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB:
QF_NIA: +484-53 unsat +792-440 sat
QF_NRA: +32-19 unsat +57-23 sat
However, this PR does not (yet) enable this method by default.
Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions.
Diffstat (limited to 'src/options/theory_options.toml')
| -rw-r--r-- | src/options/theory_options.toml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index 84c994c3f..6ec9d8854 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -34,3 +34,11 @@ header = "options/theory_options.h" default = "true" read_only = true help = "condense values for functions in models rather than explicitly representing them" + +[[option]] + name = "relevanceFilter" + category = "regular" + long = "relevance-filter" + type = "bool" + default = "false" + help = "enable analysis of relevance of asserted literals with respect to the input formula" |