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.

5 files changed, 41 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)
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 <vector>
 
 #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<std::vector<Node>> d_globalDefineFunLemmas;
+  /** The index of the above list that we have processed */
+  context::CDO<size_t> 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)