From 2d5fd2cad363e3e966ddbb15abfaa45a0a971065 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Wed, 16 Dec 2020 13:22:59 -0600 Subject: Renamed InferInfo::getAntecedant to InferInfo::getAntecedent (#5683) Renamed InferInfo::getAntecedant to InferInfo::getAntecedent --- src/theory/strings/infer_info.cpp | 2 +- src/theory/strings/infer_info.h | 20 ++++++++++---------- src/theory/strings/inference_manager.cpp | 4 ++-- 3 files changed, 13 insertions(+), 13 deletions(-) (limited to 'src/theory/strings') diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index 0d2f94f91..e1cdc5ec3 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -131,7 +131,7 @@ bool InferInfo::isFact() const return !atom.isConst() && atom.getKind() != kind::OR && d_noExplain.empty(); } -Node InferInfo::getAntecedant() const +Node InferInfo::getAntecedent() const { // d_noExplain is a subset of d_ant return utils::mkAnd(d_ant); diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 4c5674d2b..70048b2fa 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -56,7 +56,7 @@ enum class Inference : uint32_t // explain_constant(x, c) => x = c // Above, explain_constant(x,c) is a basic explanation of why x must be equal // to string constant c, which is computed by taking arguments of - // concatentation terms that are entailed to be constants. For example: + // concatenation terms that are entailed to be constants. For example: // ( y = "AB" ^ z = "C" ) => y ++ z = "ABC" I_CONST_MERGE, // initial constant conflict @@ -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 antecedants in InferInfo have a particular + * For the sake of proofs, the antecedents 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 antecedant + * We can conclude y = w by the N_UNIFY rule from the left side. The antecedent * 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 antecedant(s) of the inference, interpreted conjunctively. These are + * The antecedent(s) of the inference, interpreted conjunctively. These are * literals that currently hold in the equality engine. */ std::vector d_ant; /** - * The "new literal" antecedant(s) of the inference, interpreted + * The "new literal" antecedent(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, antecedants that are not explained are stored + * of d_ant. In other words, antecedents that are not explained are stored * in *both* d_ant and d_noExplain. */ std::vector d_noExplain; @@ -409,17 +409,17 @@ class InferInfo : public TheoryInference bool isTrivial() const; /** * Does this infer info correspond to a conflict? True if d_conc is false - * and it has no new antecedants (d_noExplain). + * and it has no new antecedents (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 antecedants (d_noExplain). + * engine with no new external antecedents (d_noExplain). */ bool isFact() const; - /** Get antecedant */ - Node getAntecedant() const; + /** Get antecedent */ + Node getAntecedent() const; }; /** diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index e324689f5..b982f24a1 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -329,10 +329,10 @@ bool InferenceManager::processFact(InferInfo& ii) { facts.push_back(ii.d_conc); } - Trace("strings-assert") << "(assert (=> " << ii.getAntecedant() << " " + Trace("strings-assert") << "(assert (=> " << ii.getAntecedent() << " " << ii.d_conc << ")) ; fact " << ii.d_id << std::endl; Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from " - << ii.getAntecedant() << " by " << ii.d_id + << ii.getAntecedent() << " by " << ii.d_id << std::endl; std::vector exp; for (const Node& ec : ii.d_ant) -- cgit v1.2.3