diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-15 00:52:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-15 00:52:33 -0500 |
commit | 617f1b0fe93e077d6e76e03dcf1a75730740fe27 (patch) | |
tree | f90a752936d1d3c218bc52517af53f4e7e19cae6 /src | |
parent | b18ebfd50bfcb3b2ec422daf5b2fd8d99ca6406a (diff) |
Always flush lemmas from downwards closure in sets (#4297)
Fixes #4283.
This also makes a few minor improvements to how lemmas are sent in sets. In particular, lemmas are not sent if we are already in conflict.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/sets/inference_manager.cpp | 17 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 5 |
2 files changed, 11 insertions, 11 deletions
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index a2507d6cf..595dd16c3 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -189,15 +189,22 @@ void InferenceManager::split(Node n, int reqPol) } void InferenceManager::flushLemmas(std::vector<Node>& lemmas, bool preprocess) { - for (const Node& l : lemmas) + if (!d_state.isInConflict()) { - flushLemma(l, preprocess); + for (const Node& l : lemmas) + { + flushLemma(l, preprocess); + } } lemmas.clear(); } void InferenceManager::flushLemma(Node lem, bool preprocess) { + if (d_state.isInConflict()) + { + return; + } if (d_lemmas_produced.find(lem) != d_lemmas_produced.end()) { Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl; @@ -211,11 +218,7 @@ void InferenceManager::flushLemma(Node lem, bool preprocess) void InferenceManager::flushPendingLemmas(bool preprocess) { - for (const Node& l : d_pendingLemmas) - { - flushLemma(l, preprocess); - } - d_pendingLemmas.clear(); + flushLemmas(d_pendingLemmas, preprocess); } bool InferenceManager::hasLemmaCached(Node lem) const diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 30bb4bad0..d6eec3821 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -514,10 +514,7 @@ void TheorySetsPrivate::fullEffortCheck() } // check downwards closure checkDownwardsClosure(); - if (options::setsInferAsLemmas()) - { - d_im.flushPendingLemmas(); - } + d_im.flushPendingLemmas(); if (d_im.hasProcessed()) { continue; |