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,
}
Assert(plr == ProcessLoopResult::SKIPPED);
// not processing an inference here, undo changes to ant
- iinfo.d_ant.clear();
+ iinfo.d_premises.clear();
}
}
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 =
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);
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);
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++)
{
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)
}
// 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;
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;
}
}
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;
}
else
{
- iinfo.d_ant.push_back(expNonEmpty);
+ iinfo.d_premises.push_back(expNonEmpty);
}
}
else
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)
{
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())
{
* 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
* (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,
/** 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;
* 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;
};
/**
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)
{
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;
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);
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);
}
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;
{
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);
}
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);
}
// (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)
{
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);
}
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);
projects / cvc5.git / commitdiff