d_satContext(c),
d_userContext(u),
d_pnm(pnm),
+ // Construct d_pfGenEe with the SAT context, since its proof include
+ // unclosed assumptions of theory literals.
d_pfGenEe(
new EagerProofGenerator(pnm, c, "ArithCongruenceManager::pfGenEe")),
+ // Construct d_pfGenEe with the USER context, since its proofs are closed.
d_pfGenExplain(new EagerProofGenerator(
pnm, u, "ArithCongruenceManager::pfGenExplain")),
d_pfee(nullptr)
++(d_statistics.d_watchedVariableIsZero);
ArithVar s = lb->getVariable();
- Node reason = Constraint::externalExplainByAssertions(lb,ub);
+ TNode eq = d_watchedEqualities[s];
+ ConstraintCP eqC = d_constraintDatabase.getConstraint(
+ s, ConstraintType::Equality, lb->getValue());
+ NodeBuilder<> reasonBuilder(Kind::AND);
+ auto pfLb = lb->externalExplainByAssertions(reasonBuilder);
+ auto pfUb = ub->externalExplainByAssertions(reasonBuilder);
+ Node reason = safeConstructNary(reasonBuilder);
+ std::shared_ptr<ProofNode> pf{};
+ if (isProofEnabled())
+ {
+ pf = d_pnm->mkNode(
+ PfRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {eqC->getProofLiteral()});
+ pf = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {eq});
+ }
d_keepAlive.push_back(reason);
- assertionToEqualityEngine(true, s, reason);
+ Trace("arith-ee") << "Asserting an equality on " << s << ", on trichotomy"
+ << std::endl;
+ Trace("arith-ee") << " based on " << lb << std::endl;
+ Trace("arith-ee") << " based on " << ub << std::endl;
+ assertionToEqualityEngine(true, s, reason, pf);
}
void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){
+ Debug("arith::cong") << "Cong::watchedVariableIsZero: " << *eq << std::endl;
+
Assert(eq->isEquality());
Assert(eq->getValue().sgn() == 0);
//Explain for conflict is correct as these proofs are generated
//and stored eagerly
//These will be safe for propagation later as well
- Node reason = eq->externalExplainByAssertions();
+ NodeBuilder<> nb(Kind::AND);
+ // An open proof of eq from literals now in reason.
+ if (Debug.isOn("arith::cong"))
+ {
+ eq->printProofTree(Debug("arith::cong"));
+ }
+ auto pf = eq->externalExplainByAssertions(nb);
+ if (isProofEnabled())
+ {
+ pf = d_pnm->mkNode(
+ PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {d_watchedEqualities[s]});
+ }
+ Node reason = safeConstructNary(nb);
d_keepAlive.push_back(reason);
- assertionToEqualityEngine(true, s, reason);
+ assertionToEqualityEngine(true, s, reason, pf);
}
void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){
+ Debug("arith::cong::notzero")
+ << "Cong::watchedVariableCannotBeZero " << *c << std::endl;
++(d_statistics.d_watchedVariableIsNotZero);
ArithVar s = c->getVariable();
+ Node disEq = d_watchedEqualities[s].negate();
//Explain for conflict is correct as these proofs are generated and stored eagerly
//These will be safe for propagation later as well
- Node reason = c->externalExplainByAssertions();
-
+ 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::ARITH_SCALE_SUM_UPPER_BOUNDS,
+ {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);
+ }
d_keepAlive.push_back(reason);
- assertionToEqualityEngine(false, s, reason);
+ assertionToEqualityEngine(false, s, reason, pf);
}
d_watchedEqualities.set(s, eq);
}
-void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar s, TNode reason){
+void ArithCongruenceManager::assertLitToEqualityEngine(
+ Node lit, TNode reason, std::shared_ptr<ProofNode> pf)
+{
+ bool isEquality = lit.getKind() != Kind::NOT;
+ Node eq = isEquality ? lit : lit[0];
+ Assert(eq.getKind() == Kind::EQUAL);
+
+ Trace("arith-ee") << "Assert to Eq " << lit << ", reason " << reason
+ << std::endl;
+ if (isProofEnabled())
+ {
+ if (CDProof::isSame(lit, reason))
+ {
+ Trace("arith-pfee") << "Asserting only, b/c implied by symm" << std::endl;
+ // The equality engine doesn't ref-count for us...
+ d_keepAlive.push_back(eq);
+ d_keepAlive.push_back(reason);
+ d_ee->assertEquality(eq, isEquality, reason);
+ }
+ else if (hasProofFor(lit))
+ {
+ Trace("arith-pfee") << "Skipping b/c already done" << std::endl;
+ }
+ else
+ {
+ setProofFor(lit, pf);
+ Trace("arith-pfee") << "Actually asserting" << std::endl;
+ if (Debug.isOn("arith-pfee"))
+ {
+ Trace("arith-pfee") << "Proof: ";
+ pf->printDebug(Trace("arith-pfee"));
+ Trace("arith-pfee") << std::endl;
+ }
+ // The proof equality engine *does* ref-count for us...
+ d_pfee->assertFact(lit, reason, d_pfGenEe.get());
+ }
+ }
+ else
+ {
+ // The equality engine doesn't ref-count for us...
+ d_keepAlive.push_back(eq);
+ d_keepAlive.push_back(reason);
+ d_ee->assertEquality(eq, isEquality, reason);
+ }
+}
+
+void ArithCongruenceManager::assertionToEqualityEngine(
+ bool isEquality, ArithVar s, TNode reason, std::shared_ptr<ProofNode> pf)
+{
Assert(isWatchedVariable(s));
TNode eq = d_watchedEqualities[s];
Assert(eq.getKind() == kind::EQUAL);
- Trace("arith-ee") << "Assert " << eq << ", pol " << isEquality << ", reason " << reason << std::endl;
- if(isEquality){
- d_ee->assertEquality(eq, true, reason);
- }else{
- d_ee->assertEquality(eq, false, reason);
+ Node lit = isEquality ? Node(eq) : eq.notNode();
+ Trace("arith-ee") << "Assert to Eq " << eq << ", pol " << isEquality
+ << ", reason " << reason << std::endl;
+ assertLitToEqualityEngine(lit, reason, pf);
+}
+
+bool ArithCongruenceManager::hasProofFor(TNode f) const
+{
+ Assert(isProofEnabled());
+ if (d_pfGenEe->hasProofFor(f))
+ {
+ return true;
}
+ Node sym = CDProof::getSymmFact(f);
+ Assert(!sym.isNull());
+ return d_pfGenEe->hasProofFor(sym);
+}
+
+void ArithCongruenceManager::setProofFor(TNode f,
+ std::shared_ptr<ProofNode> pf) const
+{
+ Assert(!hasProofFor(f));
+ d_pfGenEe->mkTrustNode(f, pf);
+ Node symF = CDProof::getSymmFact(f);
+ auto symPf = d_pnm->mkNode(PfRule::SYMM, {pf}, {});
+ d_pfGenEe->mkTrustNode(symF, symPf);
}
void ArithCongruenceManager::equalsConstant(ConstraintCP c){
Node xAsNode = d_avariables.asNode(x);
Node asRational = mkRationalNode(c->getValue().getNoninfinitesimalPart());
-
- //No guarentee this is in normal form!
+ // No guarentee this is in normal form!
+ // Note though, that it happens to be in proof normal form!
Node eq = xAsNode.eqNode(asRational);
d_keepAlive.push_back(eq);
- Node reason = c->externalExplainByAssertions();
+ NodeBuilder<> nb(Kind::AND);
+ auto pf = c->externalExplainByAssertions(nb);
+ Node reason = safeConstructNary(nb);
d_keepAlive.push_back(reason);
Trace("arith-ee") << "Assert equalsConstant " << eq << ", reason " << reason << std::endl;
- d_ee->assertEquality(eq, true, reason);
+ assertLitToEqualityEngine(eq, reason, pf);
}
void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
<< ub << std::endl;
ArithVar x = lb->getVariable();
- Node reason = Constraint::externalExplainByAssertions(lb,ub);
+ NodeBuilder<> nb(Kind::AND);
+ auto pfLb = lb->externalExplainByAssertions(nb);
+ auto pfUb = ub->externalExplainByAssertions(nb);
+ Node reason = safeConstructNary(nb);
Node xAsNode = d_avariables.asNode(x);
Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart());
- //No guarentee this is in normal form!
+ // No guarentee this is in normal form!
+ // Note though, that it happens to be in proof normal form!
Node eq = xAsNode.eqNode(asRational);
+ std::shared_ptr<ProofNode> pf;
+ if (isProofEnabled())
+ {
+ pf = d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {eq});
+ }
d_keepAlive.push_back(eq);
d_keepAlive.push_back(reason);
Trace("arith-ee") << "Assert equalsConstant2 " << eq << ", reason " << reason << std::endl;
- d_ee->assertEquality(eq, true, reason);
+
+ assertLitToEqualityEngine(eq, reason, pf);
}
bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; }
projects / cvc5.git / commitdiff