New InferenceIds for BV theory (#5909)

This PR introduces new InferenceId for the BV theory and uses them instead of InferenceId::UNKNOWN.

diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 0c541ba89ee471cb7a3f9cec87157158e597dc2e..97ff7e04421f8f27301cddd2e2ff8fb026603736 100644 (file)
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -416,9 +416,9 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
       lemmab << d_cnf->getNode(clause[i]);
     }
     Node lemma = lemmab;
-    d_bv->d_im.lemma(lemma, InferenceId::UNKNOWN);
+    d_bv->d_im.lemma(lemma, InferenceId::BV_LAZY_LEMMA);
   } else {
-    d_bv->d_im.lemma(d_cnf->getNode(clause[0]), InferenceId::UNKNOWN);
+    d_bv->d_im.lemma(d_cnf->getNode(clause[0]), InferenceId::BV_LAZY_LEMMA);
   }
 }
 

diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index bf264f9cd757ce7887bcac27470511ea7e065f8d..55ae457bb285ddfcf8f5a4ce99de57bb47bb0a22 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -118,7 +118,7 @@ void BVSolverBitblast::postCheck(Theory::Effort level)
     }
 
     NodeManager* nm = NodeManager::currentNM();
-    d_im.conflict(nm->mkAnd(conflict), InferenceId::UNKNOWN);
+    d_im.conflict(nm->mkAnd(conflict), InferenceId::BV_BITBLAST_CONFLICT);
   }
 }
 

diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index 0e81d064862ce295eb7cd290a2c254362f279814..d8d8dbed7f7467a33c1cf2f9b11a422235d167b4 100644 (file)
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -196,7 +196,7 @@ void BVSolverLazy::sendConflict()
   {
     Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict "
                        << d_conflictNode << std::endl;
-    d_im.conflict(d_conflictNode, InferenceId::UNKNOWN);
+    d_im.conflict(d_conflictNode, InferenceId::BV_LAZY_CONFLICT);
     d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
     d_conflictNode = Node::null();
   }
@@ -287,11 +287,11 @@ void BVSolverLazy::check(Theory::Effort e)
     {
       if (assertions.size() == 1)
       {
-        d_im.conflict(assertions[0], InferenceId::UNKNOWN);
+        d_im.conflict(assertions[0], InferenceId::BV_LAZY_CONFLICT);
         return;
       }
       Node conflict = utils::mkAnd(assertions);
-      d_im.conflict(conflict, InferenceId::UNKNOWN);
+      d_im.conflict(conflict, InferenceId::BV_LAZY_CONFLICT);
       return;
     }
     return;

diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index 46d01d129d6301cf00ef10d6eee6f3806a51b1e4..8e1a9e1084f3aeaa44eddc0ee686c376a902ec49 100644 (file)
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -203,7 +203,7 @@ class BVSolverLazy : public BVSolver
 
   void lemma(TNode node)
   {
-    d_im.lemma(node, InferenceId::UNKNOWN);
+    d_im.lemma(node, InferenceId::BV_LAZY_LEMMA);
     d_lemmasAdded = true;
   }
 

diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
index 02196a4ede181ce0dad68e4319e957e866f543df..58be5d826c036240642910c521a3fa62dee02f1c 100644 (file)
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -93,12 +93,12 @@ void BVSolverSimple::addBBLemma(TNode fact)
 
   if (d_epg == nullptr)
   {
-    d_im.lemma(lemma, InferenceId::UNKNOWN);
+    d_im.lemma(lemma, InferenceId::BV_SIMPLE_BITBLAST_LEMMA);
   }
   else
   {
     TrustNode tlem = d_epg->mkTrustNode(lemma, PfRule::BV_BITBLAST, {}, {fact});
-    d_im.trustedLemma(tlem, InferenceId::UNKNOWN);
+    d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_BITBLAST_LEMMA);
   }
 }
 
@@ -123,13 +123,13 @@ bool BVSolverSimple::preNotifyFact(
 
     if (d_epg == nullptr)
     {
-      d_im.lemma(lemma, InferenceId::UNKNOWN);
+      d_im.lemma(lemma, InferenceId::BV_SIMPLE_LEMMA);
     }
     else
     {
       TrustNode tlem =
           d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact});
-      d_im.trustedLemma(tlem, InferenceId::UNKNOWN);
+      d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_LEMMA);
     }
 
     std::unordered_set<Node, NodeHashFunction> bv_atoms;

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index b839066888b0414dbfcdf4b28de093506d2db48f..d56cb9ebbed97a32757cc0e3f5d2cd26939222a7 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -559,7 +559,7 @@ bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
                               nm->mkNode(kind::LT, n, max));
         Trace("bv-extf-lemma")
             << "BV extf lemma (range) : " << lem << std::endl;
-        d_bv->d_im.lemma(lem, InferenceId::UNKNOWN);
+        d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_LEMMA);
         sentLemma = true;
       }
     }
@@ -608,7 +608,7 @@ bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
           //   (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
           Trace("bv-extf-lemma")
               << "BV extf lemma (collapse) : " << lem << std::endl;
-          d_bv->d_im.lemma(lem, InferenceId::UNKNOWN);
+          d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_COLLAPSE);
           sentLemma = true;
         }
       }

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 2ce1a463414552418251c14b3a66267581217a18..7adf3df0c54b48b52d76c75f70719d65b8793ae6 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -114,6 +114,14 @@ enum class InferenceId
   BAG_DIFFERENCE_REMOVE,
   BAG_DUPLICATE_REMOVAL,
 
+  BV_BITBLAST_CONFLICT,
+  BV_LAZY_CONFLICT,
+  BV_LAZY_LEMMA,
+  BV_SIMPLE_LEMMA,
+  BV_SIMPLE_BITBLAST_LEMMA,
+  BV_EXTF_LEMMA,
+  BV_EXTF_COLLAPSE,
+
   // (= (C t1 ... tn) (C s1 .. sn)) => (= ti si)
   DATATYPES_UNIF,
   // ((_ is Ci) t) => (= t (Ci (sel_1 t) ... (sel_n t)))