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.

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 77646c0028a0c2b37319561ae6ff38bff433a31b..9c24dd690d086c00dd536c1b29709a78b0a37b35 100644 (file)
--- 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 15131be60c71b1aa8963ba4065dd4e4eff2197e3..5cda366e63c655d74d24ce52b2ec05f7385f1c67 100644 (file)
--- 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 67e83bcd1864193d38cac8f29e6b03164a5edfdb..473b53015ea5b8973ce0ab68d965e911171bcd2c 100644 (file)
--- 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 c248d2231cb701baeac67221ee70b4a51bf11a74..215f75e977c1fb18e73d1cf476fc2187bddbc9ce 100644 (file)
--- 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 (file)
index 0000000..ddf8996
--- /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)