From: Gereon Kremer <gkremer@stanford.edu>
Date: Thu, 18 Feb 2021 20:37:30 +0000 (+0100)
Subject: New InferenceIds for BV theory (#5909)
X-Git-Tag: cvc5-1.0.0~2265
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ba30b690b29e7e52dd8ea1ea953525c401abf3d9;p=cvc5.git

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 0c541ba89..97ff7e044 100644
--- 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 bf264f9cd..55ae457bb 100644
--- 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 0e81d0648..d8d8dbed7 100644
--- 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 46d01d129..8e1a9e108 100644
--- 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 02196a4ed..58be5d826 100644
--- 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 b83906688..d56cb9ebb 100644
--- 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 2ce1a4634..7adf3df0c 100644
--- 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)))