From 50da62ab1ebd71d619e4ada901c35009396f772e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 25 Oct 2021 13:23:39 -0500 Subject: [PATCH] Fix support for global declarations (#7480) Previously, we asserted global declarations as substitutions/formulas just before check-sat. This is not ideal since the current set of assertions can be preprocessed without having knowledge of definitions of defined functions. Moreover, this could lead to model unsoundness if it were the case that a defined symbol was solved during preprocessing. Fixes #7479. In that example, y was solved for true and then we failed to overwrite y with its definition (> x 0), hence dropping the definition. Now, y is defined as (> x 0) before we preprocess. --- src/smt/assertions.cpp | 27 ++++++++++++------- src/smt/assertions.h | 13 +++++++++ src/smt/process_assertions.cpp | 2 ++ test/regress/CMakeLists.txt | 1 + .../push-pop/issue7479-global-decls.smt2 | 8 ++++++ 5 files changed, 41 insertions(+), 10 deletions(-) create mode 100644 test/regress/regress0/push-pop/issue7479-global-decls.smt2 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& 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) diff --git a/src/smt/assertions.h b/src/smt/assertions.h index 15131be60..5cda366e6 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -21,6 +21,7 @@ #include #include "context/cdlist.h" +#include "context/cdo.h" #include "expr/node.h" #include "preprocessing/assertion_pipeline.h" #include "smt/env_obj.h" @@ -56,6 +57,16 @@ class Assertions : protected EnvObj * without a check-sat. */ void clearCurrent(); + /** refresh + * + * Ensures that all global declarations have been processed in the current + * context. This may trigger substitutions to be added to the top-level + * substitution and/or formulas added to the current set of assertions. + * + * If global declarations are true, this method must be called before + * processing assertions. + */ + void refresh(); /* * Initialize a call to check satisfiability. This adds assumptions to * the list of assumptions maintained by this class, and finalizes the @@ -163,6 +174,8 @@ class Assertions : protected EnvObj * assert this list of definitions in each check-sat call. */ std::unique_ptr> d_globalDefineFunLemmas; + /** The index of the above list that we have processed */ + context::CDO d_globalDefineFunLemmasIndex; /** * The list of assumptions from the previous call to checkSatisfiability. * Note that if the last call to checkSatisfiability was an entailment check, diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 67e83bcd1..473b53015 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -93,6 +93,8 @@ void ProcessAssertions::spendResource(Resource r) bool ProcessAssertions::apply(Assertions& as) { + // must first refresh the assertions, in the case global declarations is true + as.refresh(); AssertionPipeline& assertions = as.getAssertionPipeline(); Assert(d_preprocessingPassContext != nullptr); // Dump the assertions diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c248d2231..215f75e97 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -890,6 +890,7 @@ set(regress_0_tests regress0/push-pop/issue1986.smt2 regress0/push-pop/issue2137.min.smt2 regress0/push-pop/issue6535-inc-solve.smt2 + regress0/push-pop/issue7479-global-decls.smt2 regress0/push-pop/quant-fun-proc-unfd.smt2 regress0/push-pop/real-as-int-incremental.smt2 regress0/push-pop/simple_unsat_cores.smt2 diff --git a/test/regress/regress0/push-pop/issue7479-global-decls.smt2 b/test/regress/regress0/push-pop/issue7479-global-decls.smt2 new file mode 100644 index 000000000..ddf89960e --- /dev/null +++ b/test/regress/regress0/push-pop/issue7479-global-decls.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: -i +; EXPECT: unsat +(set-logic ALL) +(set-option :global-declarations true) +(define-fun y () Bool (> 0 0)) +(assert y) +(push) +(check-sat) -- 2.30.2