diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-24 14:29:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-24 14:29:40 -0500 |
commit | df2150c721b811a588e5f731b6bc11b236ee3a7e (patch) | |
tree | 580d1d55b4655c1f213ac25944b2cd4b93747aef /src | |
parent | 706dbdac95131bf45efbfcb9a8ca4df9dfb85478 (diff) |
Do not use relevance during non-linear check model (#4938)
This led to a model soundness issue in rare cases where a relevant literal was dropped due to an entailment check by an irrelevant literal.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index fb5b6eec8..8535396e7 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -427,17 +427,11 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions, // get the presubstitution Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl; - std::vector<Node> passertions; - if (options::nlRlvMode() != options::NlRlvMode::NONE) - { - // only keep the relevant assertions (those required for showing input - // is satisfied) - computeRelevantAssertions(assertions, passertions); - } - else - { - passertions = assertions; - } + // Notice that we do not consider relevance here, since assertions were + // already filtered based on relevance. It is incorrect to filter based on + // relevance here, since we may have discarded literals that are relevant + // that are entailed based on the techniques in getAssertions. + std::vector<Node> passertions = assertions; if (options::nlExt()) { // preprocess the assertions with the trancendental solver |