Fixes for skolem definition management (#8301)

Fixes two issues with how we manage skolem definitions (used for tracking which assertions are relevant for the decision engine).

First, the theory proxy must be notified of skolem definitions before we have assertions involving them, or else hasSkolems is wrong. This was previously done incorrectly for lemmas. This PR changes the order in PropEngine::assertLemmasInternal.

Second, skolem definitions are local to a solver instance and should not be managed by attributes, moreover they are user-context dependent. This changes it to a local user-context dependent map in Skolem.

Fixes #8296.

diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp
index bced3d662c2bf8186f3a594621f1027e627ee6f4..6c3ddfd04862ef44403b37a06f1b636fff646027 100644 (file)
--- a/src/decision/justification_strategy.cpp
+++ b/src/decision/justification_strategy.cpp
@@ -508,6 +508,7 @@ bool JustificationStrategy::needsActiveSkolemDefs() const
 
 void JustificationStrategy::notifyActiveSkolemDefs(std::vector<TNode>& defs)
 {
+  Trace("jh-assert") << "notifyActiveSkolemDefs: " << defs << std::endl;
   Assert(d_jhSkRlvMode == options::JutificationSkolemRlvMode::ASSERT);
   // assertion processed makes all skolems in assertion active,
   // which triggers their definitions to becoming relevant

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 4fe7da6959e1ea71521972984d392a4a3854c41e..8728593469aaee370542b3a6568c89224fa23a53 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -267,15 +267,11 @@ void PropEngine::assertLemmasInternal(
     const std::vector<theory::SkolemLemma>& ppLemmas,
     bool removable)
 {
-  if (!trn.isNull())
-  {
-    assertTrustedLemmaInternal(trn, removable);
-  }
-  for (const theory::SkolemLemma& lem : ppLemmas)
-  {
-    assertTrustedLemmaInternal(lem.d_lemma, removable);
-  }
-  // assert to decision engine
+  // Assert to decision engine. Notice this must come before the calls to
+  // assertTrustedLemmaInternal below, since the decision engine requires
+  // setting up information about the relevance of skolems before literals
+  // are potentially asserted to the theory engine, which it listens to for
+  // tracking active skolem definitions.
   if (!removable)
   {
     // also add to the decision engine, where notice we don't need proofs
@@ -289,6 +285,14 @@ void PropEngine::assertLemmasInternal(
       d_theoryProxy->notifyAssertion(lem.getProven(), lem.d_skolem, true);
     }
   }
+  if (!trn.isNull())
+  {
+    assertTrustedLemmaInternal(trn, removable);
+  }
+  for (const theory::SkolemLemma& lem : ppLemmas)
+  {
+    assertTrustedLemmaInternal(lem.d_lemma, removable);
+  }
 }
 
 void PropEngine::requirePhase(TNode n, bool phase) {

diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp
index 36849424e0ab26284a57d030d73be92f7a6cf304..b4609ebe8d3caf1ca8586553aee7ecedfba1fcca 100644 (file)
--- a/src/prop/skolem_def_manager.cpp
+++ b/src/prop/skolem_def_manager.cpp
@@ -15,14 +15,12 @@
 
 #include "prop/skolem_def_manager.h"
 
-#include "expr/attribute.h"
-
 namespace cvc5 {
 namespace prop {
 
 SkolemDefManager::SkolemDefManager(context::Context* context,
                                    context::UserContext* userContext)
-    : d_skDefs(userContext), d_skActive(context)
+    : d_skDefs(userContext), d_skActive(context), d_hasSkolems(userContext)
 {
 }
 
@@ -37,6 +35,9 @@ void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def)
   // equivalent up to purification
   if (d_skDefs.find(skolem) == d_skDefs.end())
   {
+    // should not have already computed whether the skolem has skolems, or else
+    // our computation of hasSkolems is wrong after adding this definition
+    Assert(d_hasSkolems.find(skolem) == d_hasSkolems.end());
     d_skDefs.insert(skolem, def);
   }
 }
@@ -54,6 +55,8 @@ void SkolemDefManager::notifyAsserted(TNode literal,
 {
   std::unordered_set<Node> skolems;
   getSkolems(literal, skolems);
+  Trace("sk-defs") << "notifyAsserted: " << literal << " has skolems "
+                   << skolems << std::endl;
   for (const Node& k : skolems)
   {
     if (d_skActive.find(k) != d_skActive.end())
@@ -62,6 +65,7 @@ void SkolemDefManager::notifyAsserted(TNode literal,
       continue;
     }
     d_skActive.insert(k);
+    Trace("sk-defs") << "...activate " << k << std::endl;
     if (useDefs)
     {
       // add its definition to the activated list
@@ -77,28 +81,20 @@ void SkolemDefManager::notifyAsserted(TNode literal,
   }
 }
 
-struct HasSkolemTag
-{
-};
-struct HasSkolemComputedTag
-{
-};
-/** Attribute true for nodes with skolems in them */
-typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr;
-/** Attribute true for nodes where we have computed the above attribute */
-typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr;
-
-bool SkolemDefManager::hasSkolems(TNode n) const
+bool SkolemDefManager::hasSkolems(TNode n)
 {
+  Trace("sk-defs-debug") << "Compute has skolems for " << n << std::endl;
   std::unordered_set<TNode> visited;
   std::unordered_set<TNode>::iterator it;
+  NodeBoolMap::const_iterator itn;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(n);
   do
   {
     cur = visit.back();
-    if (cur.getAttribute(HasSkolemComputedAttr()))
+    itn = d_hasSkolems.find(cur);
+    if (itn != d_hasSkolems.end())
     {
       visit.pop_back();
       // already computed
@@ -116,8 +112,7 @@ bool SkolemDefManager::hasSkolems(TNode n) const
         {
           hasSkolem = (d_skDefs.find(cur) != d_skDefs.end());
         }
-        cur.setAttribute(HasSkolemAttr(), hasSkolem);
-        cur.setAttribute(HasSkolemComputedAttr(), true);
+        d_hasSkolems[cur] = hasSkolem;
       }
       else
       {
@@ -133,7 +128,7 @@ bool SkolemDefManager::hasSkolems(TNode n) const
       visit.pop_back();
       bool hasSkolem;
       if (cur.getMetaKind() == kind::metakind::PARAMETERIZED
-          && cur.getOperator().getAttribute(HasSkolemAttr()))
+          && d_hasSkolems[cur.getOperator()])
       {
         hasSkolem = true;
       }
@@ -142,24 +137,22 @@ bool SkolemDefManager::hasSkolems(TNode n) const
         hasSkolem = false;
         for (TNode i : cur)
         {
-          Assert(i.getAttribute(HasSkolemComputedAttr()));
-          if (i.getAttribute(HasSkolemAttr()))
+          Assert(d_hasSkolems.find(i) != d_hasSkolems.end());
+          if (d_hasSkolems[i])
           {
             hasSkolem = true;
             break;
           }
         }
       }
-      cur.setAttribute(HasSkolemAttr(), hasSkolem);
-      cur.setAttribute(HasSkolemComputedAttr(), true);
+      d_hasSkolems[cur] = hasSkolem;
     }
   } while (!visit.empty());
-  Assert(n.getAttribute(HasSkolemComputedAttr()));
-  return n.getAttribute(HasSkolemAttr());
+  Assert(d_hasSkolems.find(n) != d_hasSkolems.end());
+  return d_hasSkolems[n];
 }
 
-void SkolemDefManager::getSkolems(TNode n,
-                                  std::unordered_set<Node>& skolems) const
+void SkolemDefManager::getSkolems(TNode n, std::unordered_set<Node>& skolems)
 {
   std::unordered_set<TNode> visited;
   std::unordered_set<TNode>::iterator it;

diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h
index d3b59f895bdfb36cecaf9c3990dc155bc274f7de..59213302e86430169eeaa63363f7c385e3948b63 100644 (file)
--- a/src/prop/skolem_def_manager.h
+++ b/src/prop/skolem_def_manager.h
@@ -22,6 +22,7 @@
 #include <unordered_set>
 #include <vector>
 
+#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdinsert_hashmap.h"
 #include "context/context.h"
@@ -42,6 +43,7 @@ namespace prop {
 class SkolemDefManager
 {
   using NodeNodeMap = context::CDInsertHashMap<Node, Node>;
+  using NodeBoolMap = context::CDHashMap<Node, bool>;
   using NodeSet = context::CDHashSet<Node>;
 
  public:
@@ -81,15 +83,21 @@ class SkolemDefManager
    * @param n The node to traverse
    * @param skolems The set where the skolems are added
    */
-  void getSkolems(TNode n, std::unordered_set<Node>& skolems) const;
-  /** Does n have skolems having definitions managed by this class? */
-  bool hasSkolems(TNode n) const;
+  void getSkolems(TNode n, std::unordered_set<Node>& skolems);
+  /**
+   * Does n have skolems having definitions managed by this class? Should call
+   * this method *after* notifying skolem definitions for all potential
+   * skolems occurring in n.
+   */
+  bool hasSkolems(TNode n);
 
  private:
   /** skolems to definitions (user-context dependent) */
   NodeNodeMap d_skDefs;
   /** set of active skolems (SAT-context dependent) */
   NodeSet d_skActive;
+  /** Cache for hasSkolems */
+  NodeBoolMap d_hasSkolems;
 };
 
 }  // namespace prop

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 05b16abb474aec40a6ad8b4af1138c7d0c1d12d9..67073033d18fb5caf3e37a4ba36e50396b221f2c 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -575,6 +575,7 @@ set(regress_0_tests
   regress0/decision/error20.delta01.smtv1.smt2
   regress0/decision/error20.smtv1.smt2
   regress0/decision/error3.delta01.smtv1.smt2
+  regress0/decision/issue8296-sk-def-before-assert.smt2
   regress0/decision/pp-regfile.delta01.smtv1.smt2
   regress0/decision/pp-regfile.delta02.smtv1.smt2
   regress0/decision/quant-ex1.smt2

diff --git a/test/regress/regress0/decision/issue8296-sk-def-before-assert.smt2 b/test/regress/regress0/decision/issue8296-sk-def-before-assert.smt2
new file mode 100644 (file)
index 0000000..3665d6a
--- /dev/null
+++ b/test/regress/regress0/decision/issue8296-sk-def-before-assert.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(set-option :miniscope-quant false)
+(declare-fun i2 () Int)
+(declare-fun v6 () Bool)
+(declare-sort S2 0)
+(assert (exists ((q521 S2)) (exists ((q523 Int)) (exists ((q524 S2)) (forall ((q525 Bool)) (or (= q524 q521) (= q523 (abs i2)) (and v6 (= q525 (= 0 (abs i2))))))))))
+(check-sat)
+(assert (= 1 (abs i2)))
+(check-sat)