diff options
Diffstat (limited to 'src/smt/assertions.cpp')
| -rw-r--r-- | src/smt/assertions.cpp | 27 |
1 files changed, 17 insertions, 10 deletions
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 77646c002..9c24dd690 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -40,6 +40,7 @@ Assertions::Assertions(Env& env, AbstractValues& absv) d_produceAssertions(false), d_assertionList(userContext()), d_assertionListDefs(userContext()), + d_globalDefineFunLemmasIndex(userContext(), 0), d_globalNegation(false), d_assertions() { @@ -49,6 +50,22 @@ Assertions::~Assertions() { } +void Assertions::refresh() +{ + if (d_globalDefineFunLemmas != nullptr) + { + // Global definitions are asserted now to ensure they always exist. This is + // done at the beginning of preprocessing, to ensure that definitions take + // priority over, e.g. solving during preprocessing. See issue #7479. + size_t numGlobalDefs = d_globalDefineFunLemmas->size(); + for (size_t i = d_globalDefineFunLemmasIndex.get(); i < numGlobalDefs; i++) + { + addFormula((*d_globalDefineFunLemmas)[i], false, true, false); + } + d_globalDefineFunLemmasIndex = numGlobalDefs; + } +} + void Assertions::finishInit() { // [MGD 10/20/2011] keep around in incremental mode, due to a @@ -107,16 +124,6 @@ void Assertions::initializeCheckSat(const std::vector<Node>& assumptions, ensureBoolean(n); addFormula(n, true, false, false); } - if (d_globalDefineFunLemmas != nullptr) - { - // Global definitions are asserted at check-sat-time because we have to - // make sure that they are always present (they are essentially level - // zero assertions) - for (const Node& lemma : *d_globalDefineFunLemmas) - { - addFormula(lemma, false, true, false); - } - } } void Assertions::assertFormula(const Node& n) |