Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)

This PR adds a new InferenceId member to the TheoryInference class.
All classes derived from TheoryInference are adapted accordingly.

diff --git a/src/theory/arith/arith_lemma.h b/src/theory/arith/arith_lemma.h
index 85e55b1e3ac736a654f612ed1f376aaee3d913aa..e50df15c028e5e1e824167a704bb9eb7c0d75b72 100644 (file)
--- a/src/theory/arith/arith_lemma.h
+++ b/src/theory/arith/arith_lemma.h
@@ -41,13 +41,10 @@ class ArithLemma : public SimpleTheoryLemma
              LemmaProperty p,
              ProofGenerator* pg,
              InferenceId inf = InferenceId::UNKNOWN)
-      : SimpleTheoryLemma(n, p, pg), d_inference(inf)
+      : SimpleTheoryLemma(inf, n, p, pg)
   {
   }
   virtual ~ArithLemma() {}
-
-  /** The inference id for the lemma */
-  InferenceId d_inference;
 };
 /**
  * Writes an arithmetic lemma to a stream.

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 6a1f898d3a9e6604f392c1f691531c467151fde2..aa0aa4f2ae6da00b2ca77efbaf9a8b9430b9c98c 100644 (file)
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -32,7 +32,7 @@ InferenceManager::InferenceManager(TheoryArith& ta,
 void InferenceManager::addPendingArithLemma(std::unique_ptr<ArithLemma> lemma,
                                             bool isWaiting)
 {
-  Trace("arith::infman") << "Add " << lemma->d_inference << " " << lemma->d_node
+  Trace("arith::infman") << "Add " << lemma->getId() << " " << lemma->d_node
                          << (isWaiting ? " as waiting" : "") << std::endl;
   if (hasCachedLemma(lemma->d_node, lemma->d_property))
   {
@@ -81,7 +81,7 @@ void InferenceManager::flushWaitingLemmas()
   for (auto& lem : d_waitingLem)
   {
     Trace("arith::infman") << "Flush waiting lemma to pending: "
-                           << lem->d_inference << " " << lem->d_node
+                           << lem->getId() << " " << lem->d_node
                            << std::endl;
     d_pendingLem.emplace_back(std::move(lem));
   }

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index d6a1e94a1fbb3122f416d17d29c856337b7413e4..709b1e7770bbf48aecf3b06ee896161f55184461 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -89,10 +89,10 @@ void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)
 {
   for (const NlLemma& nlem : out)
   {
-    Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_inference
+    Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.getId()
                           << " : " << nlem.d_node << std::endl;
     d_im.addPendingArithLemma(nlem);
-    d_stats.d_inferences << nlem.d_inference;
+    d_stats.d_inferences << nlem.getId();
   }
 }
 

diff --git a/src/theory/bags/infer_info.cpp b/src/theory/bags/infer_info.cpp
index 9b5187689c2ccdb3a1f50705d37e1284dea254c2..c4e9570876749c54c88931a39fb7361d52186ed0 100644 (file)
--- a/src/theory/bags/infer_info.cpp
+++ b/src/theory/bags/infer_info.cpp
@@ -20,7 +20,7 @@ namespace CVC4 {
 namespace theory {
 namespace bags {
 
-InferInfo::InferInfo() : d_id(InferenceId::UNKNOWN) {}
+InferInfo::InferInfo(InferenceId id) : TheoryInference(id) {}
 
 bool InferInfo::process(TheoryInferenceManager* im, bool asLemma)
 {
@@ -77,7 +77,7 @@ bool InferInfo::isFact() const
 
 std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
 {
-  out << "(infer :id " << ii.d_id << std::endl;
+  out << "(infer :id " << ii.getId() << std::endl;
   out << ":conclusion " << ii.d_conclusion << std::endl;
   if (!ii.d_premises.empty())
   {

diff --git a/src/theory/bags/infer_info.h b/src/theory/bags/infer_info.h
index 8628d19f697030ebc4ff65bcdc289d8305b42110..66d75b5dc68808502a3116e5980b7a10e09f7a86 100644 (file)
--- a/src/theory/bags/infer_info.h
+++ b/src/theory/bags/infer_info.h
@@ -38,12 +38,10 @@ class InferenceManager;
 class InferInfo : public TheoryInference
 {
  public:
-  InferInfo();
+  InferInfo(InferenceId id);
   ~InferInfo() {}
   /** Process this inference */
   bool process(TheoryInferenceManager* im, bool asLemma) override;
-  /** The inference identifier */
-  InferenceId d_id;
   /** The conclusion */
   Node d_conclusion;
   /**

diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index 6d8b6a33bca06fe1971682065d206c295c31038a..2d4a5afedfcf32b3cb42368af174154ab0172ce7 100644 (file)
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -37,8 +37,7 @@ InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
   Assert(n.getType().isBag());
   Assert(e.getType() == n.getType().getBagElementType());
 
-  InferInfo inferInfo;
-  inferInfo.d_id = InferenceId::BAG_NON_NEGATIVE_COUNT;
+  InferInfo inferInfo(InferenceId::BAG_NON_NEGATIVE_COUNT);
   Node count = d_nm->mkNode(kind::BAG_COUNT, e, n);
 
   Node gte = d_nm->mkNode(kind::GEQ, count, d_zero);
@@ -51,28 +50,30 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e)
   Assert(n.getKind() == kind::MK_BAG);
   Assert(e.getType() == n.getType().getBagElementType());
 
-  InferInfo inferInfo;
-  Node skolem = getSkolem(n, inferInfo);
-  Node count = getMultiplicityTerm(e, skolem);
   if (n[0] == e)
   {
     // TODO issue #78: refactor this with BagRewriter
     // (=> true (= (bag.count e (bag e c)) c))
-    inferInfo.d_id = InferenceId::BAG_MK_BAG_SAME_ELEMENT;
+    InferInfo inferInfo(InferenceId::BAG_MK_BAG_SAME_ELEMENT);
+    Node skolem = getSkolem(n, inferInfo);
+    Node count = getMultiplicityTerm(e, skolem);
     inferInfo.d_conclusion = count.eqNode(n[1]);
+    return inferInfo;
   }
   else
   {
     // (=>
     //   true
     //   (= (bag.count e (bag x c)) (ite (= e x) c 0)))
-    inferInfo.d_id = InferenceId::BAG_MK_BAG;
+    InferInfo inferInfo(InferenceId::BAG_MK_BAG);
+    Node skolem = getSkolem(n, inferInfo);
+    Node count = getMultiplicityTerm(e, skolem);
     Node same = d_nm->mkNode(kind::EQUAL, n[0], e);
     Node ite = d_nm->mkNode(kind::ITE, same, n[1], d_zero);
     Node equal = count.eqNode(ite);
     inferInfo.d_conclusion = equal;
+    return inferInfo;
   }
-  return inferInfo;
 }
 
 struct BagsDeqAttributeId
@@ -87,8 +88,7 @@ InferInfo InferenceGenerator::bagDisequality(Node n)
   Node A = n[0];
   Node B = n[1];
 
-  InferInfo inferInfo;
-  inferInfo.d_id = InferenceId::BAG_DISEQUALITY;
+  InferInfo inferInfo(InferenceId::BAG_DISEQUALITY);
 
   TypeNode elementType = A.getType().getBagElementType();
   BoundVarManager* bvm = d_nm->getBoundVarManager();
@@ -121,9 +121,8 @@ InferInfo InferenceGenerator::empty(Node n, Node e)
   Assert(n.getKind() == kind::EMPTYBAG);
   Assert(e.getType() == n.getType().getBagElementType());
 
-  InferInfo inferInfo;
+  InferInfo inferInfo(InferenceId::BAG_EMPTY);
   Node skolem = getSkolem(n, inferInfo);
-  inferInfo.d_id = InferenceId::BAG_EMPTY;
   Node count = getMultiplicityTerm(e, skolem);
 
   Node equal = count.eqNode(d_zero);
@@ -138,8 +137,7 @@ InferInfo InferenceGenerator::unionDisjoint(Node n, Node e)
 
   Node A = n[0];
   Node B = n[1];
-  InferInfo inferInfo;
-  inferInfo.d_id = InferenceId::BAG_UNION_DISJOINT;
+  InferInfo inferInfo(InferenceId::BAG_UNION_DISJOINT);
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -161,8 +159,7 @@ InferInfo InferenceGenerator::unionMax(Node n, Node e)
 
   Node A = n[0];
   Node B = n[1];
-  InferInfo inferInfo;
-  inferInfo.d_id = InferenceId::BAG_UNION_MAX;
+  InferInfo inferInfo(InferenceId::BAG_UNION_MAX);
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -185,8 +182,7 @@ InferInfo InferenceGenerator::intersection(Node n, Node e)
 
   Node A = n[0];
   Node B = n[1];
-  InferInfo inferInfo;
-  inferInfo.d_id = InferenceId::BAG_INTERSECTION_MIN;
+  InferInfo inferInfo(InferenceId::BAG_INTERSECTION_MIN);
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -207,8 +203,7 @@ InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
 
   Node A = n[0];
   Node B = n[1];
-  InferInfo inferInfo;
-  inferInfo.d_id = InferenceId::BAG_DIFFERENCE_SUBTRACT;
+  InferInfo inferInfo(InferenceId::BAG_DIFFERENCE_SUBTRACT);
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -230,8 +225,7 @@ InferInfo InferenceGenerator::differenceRemove(Node n, Node e)
 
   Node A = n[0];
   Node B = n[1];
-  InferInfo inferInfo;
-  inferInfo.d_id = InferenceId::BAG_DIFFERENCE_REMOVE;
+  InferInfo inferInfo(InferenceId::BAG_DIFFERENCE_REMOVE);
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -252,8 +246,7 @@ InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e)
   Assert(e.getType() == n[0].getType().getBagElementType());
 
   Node A = n[0];
-  InferInfo inferInfo;
-  inferInfo.d_id = InferenceId::BAG_DUPLICATE_REMOVAL;
+  InferInfo inferInfo(InferenceId::BAG_DUPLICATE_REMOVAL);
 
   Node countA = getMultiplicityTerm(e, A);
   Node skolem = getSkolem(n, inferInfo);

diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index fcf16b1273df800612364ab0d5308af35ef752a8..14dc9fbf1b82e38f0833f39b64f08ccc1b983a8f 100644 (file)
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -261,7 +261,7 @@ std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
   // now go back and convert it to proof steps and add to proof
   std::shared_ptr<DatatypesInference> di = (*it).second;
   // run the conversion
-  convert(di->getInferId(), di->d_conc, di->d_exp, &pf);
+  convert(di->getId(), di->d_conc, di->d_exp, &pf);
   return pf.getProofFor(fact);
 }
 

diff --git a/src/theory/datatypes/inference.cpp b/src/theory/datatypes/inference.cpp
index 0f5a5e869d7e0b6fac2196e619e318e57f8b1e96..5d68159f7651d1f8e3160eeb89cdd5c34a497afb 100644 (file)
--- a/src/theory/datatypes/inference.cpp
+++ b/src/theory/datatypes/inference.cpp
@@ -29,7 +29,7 @@ DatatypesInference::DatatypesInference(InferenceManager* im,
                                        Node conc,
                                        Node exp,
                                        InferenceId i)
-    : SimpleTheoryInternalFact(conc, exp, nullptr), d_im(im), d_id(i)
+    : SimpleTheoryInternalFact(i, conc, exp, nullptr), d_im(im)
 {
   // false is not a valid explanation
   Assert(d_exp.isNull() || !d_exp.isConst() || d_exp.getConst<bool>());
@@ -68,13 +68,11 @@ bool DatatypesInference::process(TheoryInferenceManager* im, bool asLemma)
   // sent as a lemma in addPendingInference below.
   if (asLemma || mustCommunicateFact(d_conc, d_exp))
   {
-    return d_im->processDtLemma(d_conc, d_exp, d_id);
+    return d_im->processDtLemma(d_conc, d_exp, getId());
   }
-  return d_im->processDtFact(d_conc, d_exp, d_id);
+  return d_im->processDtFact(d_conc, d_exp, getId());
 }
 
-InferenceId DatatypesInference::getInferId() const { return d_id; }
-
 }  // namespace datatypes
 }  // namespace theory
 }  // namespace CVC4

diff --git a/src/theory/datatypes/inference.h b/src/theory/datatypes/inference.h
index ca7e08f43ecce8c9de61aa8ba34ff404b0eb6bbd..d31f7b8398e37233296e55c632261b23cdf5fb31 100644 (file)
--- a/src/theory/datatypes/inference.h
+++ b/src/theory/datatypes/inference.h
@@ -62,14 +62,10 @@ class DatatypesInference : public SimpleTheoryInternalFact
    * above method.
    */
   bool process(TheoryInferenceManager* im, bool asLemma) override;
-  /** Get the inference identifier */
-  InferenceId getInferId() const;
 
  private:
   /** Pointer to the inference manager */
   InferenceManager* d_im;
-  /** The inference */
-  InferenceId d_id;
 };
 
 }  // namespace datatypes

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index bc038a149fefc08442814392d661e71d5dc57aec..e5f6ae4e48849f4b307b929b9dddbd313294cab2 100644 (file)
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -59,7 +59,7 @@ bool InferenceManagerBuffered::addPendingLemma(Node lem,
     }
   }
   // make the simple theory lemma
-  d_pendingLem.emplace_back(new SimpleTheoryLemma(lem, p, pg));
+  d_pendingLem.emplace_back(new SimpleTheoryLemma(InferenceId::UNKNOWN, lem, p, pg));
   return true;
 }
 
@@ -75,7 +75,7 @@ void InferenceManagerBuffered::addPendingFact(Node conc,
 {
   // make a simple theory internal fact
   Assert(conc.getKind() != AND && conc.getKind() != OR);
-  d_pendingFact.emplace_back(new SimpleTheoryInternalFact(conc, exp, pg));
+  d_pendingFact.emplace_back(new SimpleTheoryInternalFact(InferenceId::UNKNOWN, conc, exp, pg));
 }
 
 void InferenceManagerBuffered::addPendingFact(

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 343332da5be8c36f5d57a0b8994c7bb2887bb3cd..7268a35e2f46b4ee05bb69a4263bcaba5118580a 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -30,7 +30,7 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-CoreInferInfo::CoreInferInfo() : d_index(0), d_rev(false) {}
+CoreInferInfo::CoreInferInfo(InferenceId id) : d_infer(id), d_index(0), d_rev(false) {}
 
 CoreSolver::CoreSolver(SolverState& s,
                        InferenceManager& im,
@@ -1223,11 +1223,11 @@ void CoreSolver::processNEqc(Node eqc,
     InferInfo& ii = ipii.d_infer;
     Trace("strings-solve") << "#" << i << ": From " << ipii.d_i << " / "
                            << ipii.d_j << " (rev=" << ipii.d_rev << ") : ";
-    Trace("strings-solve") << ii.d_conc << " by " << ii.d_id << std::endl;
-    if (!set_use_index || ii.d_id < min_id
-        || (ii.d_id == min_id && ipii.d_index > max_index))
+    Trace("strings-solve") << ii.d_conc << " by " << ii.getId() << std::endl;
+    if (!set_use_index || ii.getId() < min_id
+        || (ii.getId() == min_id && ipii.d_index > max_index))
     {
-      min_id = ii.d_id;
+      min_id = ii.getId();
       max_index = ipii.d_index;
       use_index = i;
       set_use_index = true;
@@ -1443,7 +1443,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     }
 
     // The candidate inference "info"
-    CoreInferInfo info;
+    CoreInferInfo info(InferenceId::UNKNOWN);
     InferInfo& iinfo = info.d_infer;
     info.d_index = index;
     // for debugging
@@ -1466,7 +1466,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       Node lenEq = nm->mkNode(EQUAL, xLenTerm, yLenTerm);
       lenEq = Rewriter::rewrite(lenEq);
       iinfo.d_conc = nm->mkNode(OR, lenEq, lenEq.negate());
-      iinfo.d_id = InferenceId::STRINGS_LEN_SPLIT;
+      iinfo.setId(InferenceId::STRINGS_LEN_SPLIT);
       info.d_pendingPhase[lenEq] = true;
       pinfer.push_back(info);
       break;
@@ -1546,12 +1546,12 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
           // inferred
           iinfo.d_conc = nm->mkNode(
               AND, p.eqNode(nc), !eq.getConst<bool>() ? pEq.negate() : pEq);
-          iinfo.d_id = InferenceId::STRINGS_INFER_EMP;
+          iinfo.setId(InferenceId::STRINGS_INFER_EMP);
         }
         else
         {
           iinfo.d_conc = nm->mkNode(OR, eq, eq.negate());
-          iinfo.d_id = InferenceId::STRINGS_LEN_SPLIT_EMP;
+          iinfo.setId(InferenceId::STRINGS_LEN_SPLIT_EMP);
         }
         pinfer.push_back(info);
         break;
@@ -1594,7 +1594,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
               xcv, stra, PfRule::CONCAT_CPROP, isRev, skc, newSkolems);
           Assert(newSkolems.size() == 1);
           iinfo.d_skolems[LENGTH_SPLIT].push_back(newSkolems[0]);
-          iinfo.d_id = InferenceId::STRINGS_SSPLIT_CST_PROP;
+          iinfo.setId(InferenceId::STRINGS_SSPLIT_CST_PROP);
           iinfo.d_idRev = isRev;
           pinfer.push_back(info);
           break;
@@ -1614,7 +1614,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       iinfo.d_premises.push_back(expNonEmpty);
       Assert(newSkolems.size() == 1);
       iinfo.d_skolems[LENGTH_SPLIT].push_back(newSkolems[0]);
-      iinfo.d_id = InferenceId::STRINGS_SSPLIT_CST;
+      iinfo.setId(InferenceId::STRINGS_SSPLIT_CST);
       iinfo.d_idRev = isRev;
       pinfer.push_back(info);
       break;
@@ -1703,7 +1703,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     // make the conclusion
     if (lentTestSuccess == -1)
     {
-      iinfo.d_id = InferenceId::STRINGS_SSPLIT_VAR;
+      iinfo.setId(InferenceId::STRINGS_SSPLIT_VAR);
       iinfo.d_conc =
           getConclusion(x, y, PfRule::CONCAT_SPLIT, isRev, skc, newSkolems);
       if (options::stringUnifiedVSpt() && !options::stringLenConc())
@@ -1714,14 +1714,14 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     }
     else if (lentTestSuccess == 0)
     {
-      iinfo.d_id = InferenceId::STRINGS_SSPLIT_VAR_PROP;
+      iinfo.setId(InferenceId::STRINGS_SSPLIT_VAR_PROP);
       iinfo.d_conc =
           getConclusion(x, y, PfRule::CONCAT_LPROP, isRev, skc, newSkolems);
     }
     else
     {
       Assert(lentTestSuccess == 1);
-      iinfo.d_id = InferenceId::STRINGS_SSPLIT_VAR_PROP;
+      iinfo.setId(InferenceId::STRINGS_SSPLIT_VAR_PROP);
       iinfo.d_conc =
           getConclusion(y, x, PfRule::CONCAT_LPROP, isRev, skc, newSkolems);
     }
@@ -1856,7 +1856,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
         iinfo.d_premises.clear();
         // try to make t equal to empty to avoid loop
         iinfo.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate());
-        iinfo.d_id = InferenceId::STRINGS_LEN_SPLIT_EMP;
+        iinfo.setId(InferenceId::STRINGS_LEN_SPLIT_EMP);
         return ProcessLoopResult::INFERENCE;
       }
       else
@@ -1973,7 +1973,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
 
   // we will be done
   iinfo.d_conc = conc;
-  iinfo.d_id = InferenceId::STRINGS_FLOOP;
+  iinfo.setId(InferenceId::STRINGS_FLOOP);
   info.d_nfPair[0] = nfi.d_base;
   info.d_nfPair[1] = nfj.d_base;
   return ProcessLoopResult::INFERENCE;

diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h
index 6e536cbfa16413c442d1042b386d7d51b5952e7e..8c4c28a96236d0cf11db1667a6b4826da8c85c92 100644 (file)
--- a/src/theory/strings/core_solver.h
+++ b/src/theory/strings/core_solver.h
@@ -40,7 +40,7 @@ namespace strings {
 class CoreInferInfo
 {
  public:
-  CoreInferInfo();
+  CoreInferInfo(InferenceId id);
   ~CoreInferInfo() {}
   /** The infer info of this class */
   InferInfo d_infer;

diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index c543de0e0fa034c94a274760693c994be6f54bc5..7242c58bc2d2191a6a4bc8e7440dbdf830b6209e 100644 (file)
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -21,7 +21,7 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-InferInfo::InferInfo() : d_sim(nullptr), d_id(InferenceId::UNKNOWN), d_idRev(false)
+InferInfo::InferInfo(InferenceId id): TheoryInference(id), d_sim(nullptr), d_idRev(false)
 {
 }
 
@@ -61,7 +61,7 @@ Node InferInfo::getPremises() const
 
 std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
 {
-  out << "(infer " << ii.d_id << " " << ii.d_conc;
+  out << "(infer " << ii.getId() << " " << ii.d_conc;
   if (ii.d_idRev)
   {
     out << " :rev";

diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index c0667e53c7bf5cf8b5842d1d08147137e1d02e7c..d697f42ae56ccd9c45586ba223907ad7c055f856 100644 (file)
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -72,14 +72,12 @@ class InferenceManager;
 class InferInfo : public TheoryInference
 {
  public:
-  InferInfo();
+  InferInfo(InferenceId id);
   ~InferInfo() {}
   /** Process this inference */
   bool process(TheoryInferenceManager* im, bool asLemma) override;
   /** Pointer to the class used for processing this info */
   InferenceManager* d_sim;
-  /** The inference identifier */
-  InferenceId d_id;
   /** Whether it is the reverse form of the above id */
   bool d_idRev;
   /** The conclusion */

diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 4817df39d6e5c757d5aa1fef2d3c64c23d893a7a..c3e1ce294c089399d91af09adcca10082a924a0b 100644 (file)
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -987,7 +987,7 @@ std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
   TheoryProofStepBuffer psb(d_pnm->getChecker());
   std::shared_ptr<InferInfo> ii = (*it).second;
   // run the conversion
-  convert(ii->d_id, ii->d_idRev, ii->d_conc, ii->d_premises, ps, psb, useBuffer);
+  convert(ii->getId(), ii->d_idRev, ii->d_conc, ii->d_premises, ps, psb, useBuffer);
   // make the proof based on the step or the buffer
   if (useBuffer)
   {

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 6a4fd55df74139ee635d66ad29d58b5ed927273a..a348585e74ac38fecccc13eab98815a6a7633bbb 100644 (file)
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -139,8 +139,7 @@ bool InferenceManager::sendInference(const std::vector<Node>& exp,
     return false;
   }
   // wrap in infer info and send below
-  InferInfo ii;
-  ii.d_id = infer;
+  InferInfo ii(infer);
   ii.d_idRev = isRev;
   ii.d_conc = eq;
   ii.d_premises = exp;
@@ -171,8 +170,8 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
   {
     Trace("strings-infer-debug") << "...as conflict" << std::endl;
     Trace("strings-lemma") << "Strings::Conflict: " << ii.d_premises << " by "
-                           << ii.d_id << std::endl;
-    Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_premises << " by " << ii.d_id << std::endl;
+                           << ii.getId() << std::endl;
+    Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_premises << " by " << ii.getId() << std::endl;
     ++(d_statistics.d_conflictsInfer);
     // process the conflict immediately
     processConflict(ii);
@@ -194,11 +193,10 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
     if (unproc.empty())
     {
       Node eqs = ii.d_conc;
-      InferInfo iiSubsLem;
-      iiSubsLem.d_sim = this;
       // keep the same id for now, since we are transforming the form of the
       // inference, not the root reason.
-      iiSubsLem.d_id = ii.d_id;
+      InferInfo iiSubsLem(ii.getId());
+      iiSubsLem.d_sim = this;
       iiSubsLem.d_conc = eqs;
       if (Trace.isOn("strings-lemma-debug"))
       {
@@ -234,9 +232,8 @@ bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
     return false;
   }
   NodeManager* nm = NodeManager::currentNM();
-  InferInfo iiSplit;
+  InferInfo iiSplit(infer);
   iiSplit.d_sim = this;
-  iiSplit.d_id = infer;
   iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
   eq = Rewriter::rewrite(eq);
   addPendingPhaseRequirement(eq, preq);
@@ -291,7 +288,7 @@ void InferenceManager::processConflict(const InferInfo& ii)
 {
   Assert(!d_state.isInConflict());
   // setup the fact to reproduce the proof in the call below
-  d_statistics.d_inferences << ii.d_id;
+  d_statistics.d_inferences << ii.getId();
   if (d_ipc != nullptr)
   {
     d_ipc->notifyFact(ii);
@@ -300,7 +297,7 @@ void InferenceManager::processConflict(const InferInfo& ii)
   TrustNode tconf = mkConflictExp(ii.d_premises, d_ipc.get());
   Assert(tconf.getKind() == TrustNodeKind::CONFLICT);
   Trace("strings-assert") << "(assert (not " << tconf.getNode()
-                          << ")) ; conflict " << ii.d_id << std::endl;
+                          << ")) ; conflict " << ii.getId() << std::endl;
   // send the trusted conflict
   trustedConflict(tconf);
 }
@@ -321,9 +318,9 @@ bool InferenceManager::processFact(InferInfo& ii)
     facts.push_back(ii.d_conc);
   }
   Trace("strings-assert") << "(assert (=> " << ii.getPremises() << " "
-                          << ii.d_conc << ")) ; fact " << ii.d_id << std::endl;
+                          << ii.d_conc << ")) ; fact " << ii.getId() << std::endl;
   Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from "
-                         << ii.getPremises() << " by " << ii.d_id
+                         << ii.getPremises() << " by " << ii.getId()
                          << std::endl;
   std::vector<Node> exp;
   for (const Node& ec : ii.d_premises)
@@ -335,7 +332,7 @@ bool InferenceManager::processFact(InferInfo& ii)
   for (const Node& fact : facts)
   {
     ii.d_conc = fact;
-    d_statistics.d_inferences << ii.d_id;
+    d_statistics.d_inferences << ii.getId();
     bool polarity = fact.getKind() != NOT;
     TNode atom = polarity ? fact : fact[0];
     bool curRet = false;
@@ -390,7 +387,7 @@ bool InferenceManager::processLemma(InferInfo& ii)
   }
   // ensure that the proof generator is ready to explain the final conclusion
   // of the lemma (ii.d_conc).
-  d_statistics.d_inferences << ii.d_id;
+  d_statistics.d_inferences << ii.getId();
   if (d_ipc != nullptr)
   {
     d_ipc->notifyFact(ii);
@@ -412,14 +409,14 @@ bool InferenceManager::processLemma(InferInfo& ii)
     }
   }
   LemmaProperty p = LemmaProperty::NONE;
-  if (ii.d_id == InferenceId::STRINGS_REDUCTION)
+  if (ii.getId() == InferenceId::STRINGS_REDUCTION)
   {
     p |= LemmaProperty::NEEDS_JUSTIFY;
   }
   Trace("strings-assert") << "(assert " << tlem.getNode() << ") ; lemma "
-                          << ii.d_id << std::endl;
+                          << ii.getId() << std::endl;
   Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by "
-                         << ii.d_id << std::endl;
+                         << ii.getId() << std::endl;
   ++(d_statistics.d_lemmasInfer);
 
   // call the trusted lemma, without caching

diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index b6e9c68f4869310910d11a8de2643280fc6688ed..e42952175fbcb54e7f4467a45b94df43a7f5e920 100644 (file)
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -28,7 +28,7 @@ namespace strings {
 SolverState::SolverState(context::Context* c,
                          context::UserContext* u,
                          Valuation& v)
-    : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false)
+    : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false), d_pendingConflict(InferenceId::UNKNOWN)
 {
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -137,8 +137,7 @@ void SolverState::setPendingPrefixConflictWhen(Node conf)
   {
     return;
   }
-  InferInfo iiPrefixConf;
-  iiPrefixConf.d_id = InferenceId::STRINGS_PREFIX_CONFLICT;
+  InferInfo iiPrefixConf(InferenceId::STRINGS_PREFIX_CONFLICT);
   iiPrefixConf.d_conc = d_false;
   utils::flattenOp(AND, conf, iiPrefixConf.d_premises);
   setPendingConflict(iiPrefixConf);

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 48d461f7a233f0c07bc3e628b7bb4575c20b881d..0157a47f042b47b50fa2fc66102a3c989cd2ac29 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -615,7 +615,7 @@ void TheoryStrings::notifyFact(TNode atom,
   // process pending conflicts due to reasoning about endpoints
   if (!d_state.isInConflict() && d_state.hasPendingConflict())
   {
-    InferInfo iiPendingConf;
+    InferInfo iiPendingConf(InferenceId::UNKNOWN);
     d_state.getPendingConflict(iiPendingConf);
     Trace("strings-pending")
         << "Process pending conflict " << iiPendingConf.d_premises << std::endl;

diff --git a/src/theory/theory_inference.cpp b/src/theory/theory_inference.cpp
index 8e52c8cd1182c51aef428508267f6c4cf6d33240..f64b88daa6cdde851690ef3c9cef62797b3f9846 100644 (file)
--- a/src/theory/theory_inference.cpp
+++ b/src/theory/theory_inference.cpp
@@ -21,10 +21,11 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace theory {
 
-SimpleTheoryLemma::SimpleTheoryLemma(Node n,
+SimpleTheoryLemma::SimpleTheoryLemma(InferenceId id, 
+                                     Node n,
                                      LemmaProperty p,
                                      ProofGenerator* pg)
-    : d_node(n), d_property(p), d_pg(pg)
+    : TheoryInference(id), d_node(n), d_property(p), d_pg(pg)
 {
 }
 
@@ -36,10 +37,11 @@ bool SimpleTheoryLemma::process(TheoryInferenceManager* im, bool asLemma)
   return im->trustedLemma(TrustNode::mkTrustLemma(d_node, d_pg), d_property);
 }
 
-SimpleTheoryInternalFact::SimpleTheoryInternalFact(Node conc,
+SimpleTheoryInternalFact::SimpleTheoryInternalFact(InferenceId id,
+                                                   Node conc,
                                                    Node exp,
                                                    ProofGenerator* pg)
-    : d_conc(conc), d_exp(exp), d_pg(pg)
+    : TheoryInference(id), d_conc(conc), d_exp(exp), d_pg(pg)
 {
 }
 

diff --git a/src/theory/theory_inference.h b/src/theory/theory_inference.h
index 4fea944d6b66d02225b2b13848f272e86ace29c9..9cf787886573759027aad28c8122ff4ce009ceef 100644 (file)
--- a/src/theory/theory_inference.h
+++ b/src/theory/theory_inference.h
@@ -18,6 +18,7 @@
 #define CVC4__THEORY__THEORY_INFERENCE_H
 
 #include "expr/node.h"
+#include "theory/inference_id.h"
 #include "theory/output_channel.h"
 
 namespace CVC4 {
@@ -34,6 +35,7 @@ class TheoryInferenceManager;
 class TheoryInference
 {
  public:
+  TheoryInference(InferenceId id) : d_id(id) {}
   virtual ~TheoryInference() {}
   /**
    * Called by the provided inference manager to process this inference. This
@@ -60,6 +62,14 @@ class TheoryInference
    * lemma that was already cached by im and hence was discarded.
    */
   virtual bool process(TheoryInferenceManager* im, bool asLemma) = 0;
+
+  /** Get the InferenceId of this theory inference. */
+  InferenceId getId() const { return d_id; }
+  /** Set the InferenceId of this theory inference. */
+  void setId(InferenceId id) { d_id = id; }
+
+ private:
+  InferenceId d_id;
 };
 
 /**
@@ -69,7 +79,7 @@ class TheoryInference
 class SimpleTheoryLemma : public TheoryInference
 {
  public:
-  SimpleTheoryLemma(Node n, LemmaProperty p, ProofGenerator* pg);
+  SimpleTheoryLemma(InferenceId id, Node n, LemmaProperty p, ProofGenerator* pg);
   virtual ~SimpleTheoryLemma() {}
   /**
    * Send the lemma using inference manager im, return true if the lemma was
@@ -97,7 +107,7 @@ class SimpleTheoryLemma : public TheoryInference
 class SimpleTheoryInternalFact : public TheoryInference
 {
  public:
-  SimpleTheoryInternalFact(Node conc, Node exp, ProofGenerator* pg);
+  SimpleTheoryInternalFact(InferenceId id, Node conc, Node exp, ProofGenerator* pg);
   virtual ~SimpleTheoryInternalFact() {}
   /**
    * Send the lemma using inference manager im, return true if the lemma was

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 124b88e3ef12b9006944125d66bc5f4f4768d9a5..324ceb5e1c39e62bee2a46edbb86f34de43ba761 100644 (file)
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -21,6 +21,7 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
+#include "theory/inference_id.h"
 #include "theory/output_channel.h"
 #include "theory/theory_state.h"
 #include "theory/trust_node.h"