From: mudathirmahgoub Date: Fri, 8 Jan 2021 17:07:32 +0000 (-0600) Subject: Rename getAntecedent to getPremises (#5754) X-Git-Tag: cvc5-1.0.0~2390 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a7d214409def441dcf072dd483f31823fd2620ed;p=cvc5.git 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) --- 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 d_ant; + std::vector 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 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 > d_new_skolem; + std::map > 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 InferProofCons::getProofFor(Node fact) TheoryProofStepBuffer psb(d_pnm->getChecker()); std::shared_ptr 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& 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 vars; std::vector subs; std::vector 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 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 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 >& 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);