Rename getAntecedent to getPremises (#5754)

Changes:

renamed d_new_skolem to d_newSkolem
renamed d_ant to d_premises (antecedent is usually used with consequent, and premise is used with conclusion)

7 files changed, 43 insertions, 44 deletions

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index dc7b11144..38396bc63 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1484,7 +1484,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       if (!isRev)
       {
         // add temporarily to the antecedant of iinfo.
-        NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, iinfo.d_ant);
+        NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, iinfo.d_premises);
         ProcessLoopResult plr =
             processLoop(lhsLoopIdx != -1 ? nfi : nfj,
                         lhsLoopIdx != -1 ? nfj : nfi,
@@ -1502,7 +1502,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         }
         Assert(plr == ProcessLoopResult::SKIPPED);
         // not processing an inference here, undo changes to ant
-        iinfo.d_ant.clear();
+        iinfo.d_premises.clear();
       }
     }
 
@@ -1583,8 +1583,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         if (p > 1)
         {
           NormalForm::getExplanationForPrefixEq(
-              nfc, nfnc, cIndex, ncIndex, iinfo.d_ant);
-          iinfo.d_ant.push_back(expNonEmpty);
+              nfc, nfnc, cIndex, ncIndex, iinfo.d_premises);
+          iinfo.d_premises.push_back(expNonEmpty);
           // make the conclusion
           SkolemCache* skc = d_termReg.getSkolemCache();
           Node xcv =
@@ -1593,7 +1593,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
           iinfo.d_conc = getConclusion(
               xcv, stra, PfRule::CONCAT_CPROP, isRev, skc, newSkolems);
           Assert(newSkolems.size() == 1);
-          iinfo.d_new_skolem[LENGTH_SPLIT].push_back(newSkolems[0]);
+          iinfo.d_newSkolem[LENGTH_SPLIT].push_back(newSkolems[0]);
           iinfo.d_id = Inference::SSPLIT_CST_PROP;
           iinfo.d_idRev = isRev;
           pinfer.push_back(info);
@@ -1610,10 +1610,10 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       iinfo.d_conc = getConclusion(
           nc, nfcv[index], PfRule::CONCAT_CSPLIT, isRev, skc, newSkolems);
       NormalForm::getExplanationForPrefixEq(
-          nfi, nfj, index, index, iinfo.d_ant);
-      iinfo.d_ant.push_back(expNonEmpty);
+          nfi, nfj, index, index, iinfo.d_premises);
+      iinfo.d_premises.push_back(expNonEmpty);
       Assert(newSkolems.size() == 1);
-      iinfo.d_new_skolem[LENGTH_SPLIT].push_back(newSkolems[0]);
+      iinfo.d_newSkolem[LENGTH_SPLIT].push_back(newSkolems[0]);
       iinfo.d_id = Inference::SSPLIT_CST;
       iinfo.d_idRev = isRev;
       pinfer.push_back(info);
@@ -1681,7 +1681,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       utils::flattenOp(AND, lenConstraint, lcVec);
     }
 
-    NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, iinfo.d_ant);
+    NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, iinfo.d_premises);
     // Add premises for x != "" ^ y != ""
     for (unsigned xory = 0; xory < 2; xory++)
     {
@@ -1709,7 +1709,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       if (options::stringUnifiedVSpt() && !options::stringLenConc())
       {
         Assert(newSkolems.size() == 1);
-        iinfo.d_new_skolem[LENGTH_GEQ_ONE].push_back(newSkolems[0]);
+        iinfo.d_newSkolem[LENGTH_GEQ_ONE].push_back(newSkolems[0]);
       }
     }
     else if (lentTestSuccess == 0)
@@ -1727,7 +1727,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     }
     // add the length constraint(s) as the last antecedant
     Node lc = utils::mkAnd(lcVec);
-    iinfo.d_ant.push_back(lc);
+    iinfo.d_premises.push_back(lc);
     iinfo.d_idRev = isRev;
     pinfer.push_back(info);
     break;
@@ -1835,7 +1835,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
       Trace("strings-loop") << "Strings::Loop: tails are different."
                             << std::endl;
       d_im.sendInference(
-          iinfo.d_ant, conc, Inference::FLOOP_CONFLICT, false, true);
+          iinfo.d_premises, conc, Inference::FLOOP_CONFLICT, false, true);
       return ProcessLoopResult::CONFLICT;
     }
   }
@@ -1853,7 +1853,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
       if (expNonEmpty.isNull())
       {
         // no antecedants necessary
-        iinfo.d_ant.clear();
+        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 = Inference::LEN_SPLIT_EMP;
@@ -1861,7 +1861,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
       }
       else
       {
-        iinfo.d_ant.push_back(expNonEmpty);
+        iinfo.d_premises.push_back(expNonEmpty);
       }
     }
     else
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index e1cdc5ec3..15d8bbde7 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -131,10 +131,10 @@ bool InferInfo::isFact() const
   return !atom.isConst() && atom.getKind() != kind::OR && d_noExplain.empty();
 }
 
-Node InferInfo::getAntecedent() const
+Node InferInfo::getPremises() const
 {
   // d_noExplain is a subset of d_ant
-  return utils::mkAnd(d_ant);
+  return utils::mkAnd(d_premises);
 }
 
 std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
@@ -144,9 +144,9 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
   {
     out << " :rev";
   }
-  if (!ii.d_ant.empty())
+  if (!ii.d_premises.empty())
   {
-    out << " :ant (" << ii.d_ant << ")";
+    out << " :ant (" << ii.d_premises << ")";
   }
   if (!ii.d_noExplain.empty())
   {
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 70048b2fa..b586609ad 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -355,7 +355,7 @@ class InferenceManager;
  * send a fact, lemma, or conflict that is waiting to be asserted to the
  * equality engine or sent on the output channel.
  *
- * For the sake of proofs, the antecedents in InferInfo have a particular
+ * For the sake of proofs, the premises in InferInfo have a particular
  * ordering for many of the core strings rules, which is expected by
  * InferProofCons for constructing proofs of F_CONST, F_UNIFY, N_CONST, etc.
  * which apply to a pair of string terms t and s. At a high level, the ordering
@@ -365,7 +365,7 @@ class InferenceManager;
  * (3) (optionally) a length constraint.
  * For example, say we have:
  *   { x ++ y ++ v1 = z ++ w ++ v2, x = z ++ u, u = "", len(y) = len(w) }
- * We can conclude y = w by the N_UNIFY rule from the left side. The antecedent
+ * We can conclude y = w by the N_UNIFY rule from the left side. The premise
  * has the following form:
  * - (prefix up to y/w equal) x = z ++ u, u = "",
  * - (main equality) x ++ y ++ v1 = z ++ w ++ v2,
@@ -387,15 +387,15 @@ class InferInfo : public TheoryInference
   /** The conclusion */
   Node d_conc;
   /**
-   * The antecedent(s) of the inference, interpreted conjunctively. These are
+   * The premise(s) of the inference, interpreted conjunctively. These are
    * literals that currently hold in the equality engine.
    */
-  std::vector<Node> d_ant;
+  std::vector<Node> d_premises;
   /**
-   * The "new literal" antecedent(s) of the inference, interpreted
+   * The "new literal" premise(s) of the inference, interpreted
    * conjunctively. These are literals that were needed to show the conclusion
    * but do not currently hold in the equality engine. These should be a subset
-   * of d_ant. In other words, antecedents that are not explained are stored
+   * of d_ant. In other words, premises that are not explained are stored
    * in *both* d_ant and d_noExplain.
    */
   std::vector<Node> d_noExplain;
@@ -404,22 +404,22 @@ class InferInfo : public TheoryInference
    * are mapped to by a length status, indicating the length constraint that
    * can be assumed for them.
    */
-  std::map<LengthStatus, std::vector<Node> > d_new_skolem;
+  std::map<LengthStatus, std::vector<Node> > d_newSkolem;
   /**  Is this infer info trivial? True if d_conc is true. */
   bool isTrivial() const;
   /**
    * Does this infer info correspond to a conflict? True if d_conc is false
-   * and it has no new antecedents (d_noExplain).
+   * and it has no new premises (d_noExplain).
    */
   bool isConflict() const;
   /**
    * Does this infer info correspond to a "fact". A fact is an inference whose
    * conclusion should be added as an equality or predicate to the equality
-   * engine with no new external antecedents (d_noExplain).
+   * engine with no new external premises (d_noExplain).
    */
   bool isFact() const;
-  /** Get antecedent */
-  Node getAntecedent() const;
+  /** Get premises */
+  Node getPremises() const;
 };
 
 /**
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 902b90615..4df7ca36a 100644
--- 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_ant, ps, psb, useBuffer);
+  convert(ii->d_id, 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 b982f24a1..05937cf56 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -143,7 +143,7 @@ bool InferenceManager::sendInference(const std::vector<Node>& exp,
   ii.d_id = infer;
   ii.d_idRev = isRev;
   ii.d_conc = eq;
-  ii.d_ant = exp;
+  ii.d_premises = exp;
   ii.d_noExplain = noExplain;
   sendInference(ii, asLemma);
   return true;
@@ -170,10 +170,9 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
   if (ii.isConflict())
   {
     Trace("strings-infer-debug") << "...as conflict" << std::endl;
-    Trace("strings-lemma") << "Strings::Conflict: " << ii.d_ant << " by "
+    Trace("strings-lemma") << "Strings::Conflict: " << ii.d_premises << " by "
                            << ii.d_id << std::endl;
-    Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_ant
-                              << " by " << ii.d_id << std::endl;
+    Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_premises << " by " << ii.d_id << std::endl;
     ++(d_statistics.d_conflictsInfer);
     // process the conflict immediately
     processConflict(ii);
@@ -190,7 +189,7 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
     std::vector<Node> vars;
     std::vector<Node> subs;
     std::vector<Node> unproc;
-    for (const Node& ac : ii.d_ant)
+    for (const Node& ac : ii.d_premises)
     {
       d_termReg.inferSubstitutionProxyVars(ac, vars, subs, unproc);
     }
@@ -306,7 +305,7 @@ void InferenceManager::processConflict(const InferInfo& ii)
     d_ipc->notifyFact(ii);
   }
   // make the trust node
-  TrustNode tconf = mkConflictExp(ii.d_ant, d_ipc.get());
+  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;
@@ -329,13 +328,13 @@ bool InferenceManager::processFact(InferInfo& ii)
   {
     facts.push_back(ii.d_conc);
   }
-  Trace("strings-assert") << "(assert (=> " << ii.getAntecedent() << " "
+  Trace("strings-assert") << "(assert (=> " << ii.getPremises() << " "
                           << ii.d_conc << ")) ; fact " << ii.d_id << std::endl;
   Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from "
-                         << ii.getAntecedent() << " by " << ii.d_id
+                         << ii.getPremises() << " by " << ii.d_id
                          << std::endl;
   std::vector<Node> exp;
-  for (const Node& ec : ii.d_ant)
+  for (const Node& ec : ii.d_premises)
   {
     utils::flattenOp(AND, ec, exp);
   }
@@ -378,7 +377,7 @@ bool InferenceManager::processLemma(InferInfo& ii)
   Assert(!ii.isConflict());
   // set up the explanation and no-explanation
   std::vector<Node> exp;
-  for (const Node& ec : ii.d_ant)
+  for (const Node& ec : ii.d_premises)
   {
     utils::flattenOp(AND, ec, exp);
   }
@@ -413,7 +412,7 @@ bool InferenceManager::processLemma(InferInfo& ii)
   // (lazily), since this is the moment when we have decided to process the
   // inference.
   for (const std::pair<const LengthStatus, std::vector<Node> >& sks :
-       ii.d_new_skolem)
+       ii.d_newSkolem)
   {
     for (const Node& n : sks.second)
     {
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 89d77b033..d9fac6718 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -237,7 +237,7 @@ void SolverState::setPendingPrefixConflictWhen(Node conf)
   InferInfo iiPrefixConf;
   iiPrefixConf.d_id = Inference::PREFIX_CONFLICT;
   iiPrefixConf.d_conc = d_false;
-  utils::flattenOp(AND, conf, iiPrefixConf.d_ant);
+  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 6187233e0..dbe03afee 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -631,9 +631,9 @@ void TheoryStrings::notifyFact(TNode atom,
     InferInfo iiPendingConf;
     d_state.getPendingConflict(iiPendingConf);
     Trace("strings-pending")
-        << "Process pending conflict " << iiPendingConf.d_ant << std::endl;
+        << "Process pending conflict " << iiPendingConf.d_premises << std::endl;
     Trace("strings-conflict")
-        << "CONFLICT: Eager : " << iiPendingConf.d_ant << std::endl;
+        << "CONFLICT: Eager : " << iiPendingConf.d_premises << std::endl;
     ++(d_statistics.d_conflictsEager);
     // call the inference manager to send the conflict
     d_im.processConflict(iiPendingConf);