+ NodeBuilder nb(Kind::AND);
+ // An open proof of eq from literals now in reason.
+ auto pf = c->externalExplainByAssertions(nb);
+ if (Debug.isOn("arith::cong::notzero"))
+ {
+ Debug("arith::cong::notzero") << " original proof ";
+ pf->printDebug(Debug("arith::cong::notzero"));
+ Debug("arith::cong::notzero") << std::endl;
+ }
+ Node reason = safeConstructNary(nb);
+ if (isProofEnabled())
+ {
+ if (c->getType() == ConstraintType::Disequality)
+ {
+ Assert(c->getLiteral() == d_watchedEqualities[s].negate());
+ // We have to prove equivalence to the watched disequality.
+ pf = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {disEq});
+ }
+ else
+ {
+ Debug("arith::cong::notzero")
+ << " proof modification needed" << std::endl;
+
+ // Four cases:
+ // c has form x_i = d, d > 0 => multiply c by -1 in Farkas proof
+ // c has form x_i = d, d > 0 => multiply c by 1 in Farkas proof
+ // c has form x_i <= d, d < 0 => multiply c by 1 in Farkas proof
+ // c has form x_i >= d, d > 0 => multiply c by -1 in Farkas proof
+ const bool scaleCNegatively = c->getType() == ConstraintType::LowerBound
+ || (c->getType() == ConstraintType::Equality
+ && c->getValue().sgn() > 0);
+ const int cSign = scaleCNegatively ? -1 : 1;
+ TNode isZero = d_watchedEqualities[s];
+ const auto isZeroPf = d_pnm->mkAssume(isZero);
+ const auto nm = NodeManager::currentNM();
+ const auto sumPf = d_pnm->mkNode(
+ PfRule::MACRO_ARITH_SCALE_SUM_UB,
+ {isZeroPf, pf},
+ // Trick for getting correct, opposing signs.
+ {nm->mkConst(Rational(-1 * cSign)), nm->mkConst(Rational(cSign))});
+ const auto botPf = d_pnm->mkNode(
+ PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});
+ std::vector<Node> assumption = {isZero};
+ pf = d_pnm->mkScope(botPf, assumption, false);
+ Debug("arith::cong::notzero") << " new proof ";
+ pf->printDebug(Debug("arith::cong::notzero"));
+ Debug("arith::cong::notzero") << std::endl;
+ }
+ Assert(pf->getResult() == disEq);
+ }