Articulate proof-related debug statements in arith (#3700)

4 files changed, 95 insertions, 14 deletions

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index e7b1289a4..20405d359 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -526,6 +526,50 @@ bool Constraint::hasTrichotomyProof() const {
   return getProofType() == TrichotomyAP;
 }
 
+void Constraint::printProofTree(std::ostream& out, size_t depth) const
+{
+#if IS_PROOFS_BUILD
+  const ConstraintRule& rule = getConstraintRule();
+  out << std::string(2 * depth, ' ') << "* " << getVariable() << " [";
+  if (hasLiteral())
+  {
+    out << getLiteral();
+  }
+  else
+  {
+    out << "NOLIT";
+  };
+  out << "]" << ' ' << getType() << ' ' << getValue() << " (" << getProofType()
+      << ")";
+  if (getProofType() == FarkasAP)
+  {
+    out << " [";
+    bool first = true;
+    for (const auto& coeff : *rule.d_farkasCoefficients)
+    {
+      if (not first)
+      {
+        out << ", ";
+      }
+      first = false;
+      out << coeff;
+    }
+    out << "]";
+  }
+  out << endl;
+
+  for (AntecedentId i = rule.d_antecedentEnd; i != AntecedentIdSentinel; --i) {
+    ConstraintCP antecdent = d_database->getAntecedent(i);
+    if (antecdent == NullConstraint) {
+      break;
+    }
+    antecdent->printProofTree(out, depth + 1);
+  }
+#else  /* IS_PROOFS_BUILD */
+  out << "Cannot print proof. This is not a proof build." << endl;
+#endif /* IS_PROOFS_BUILD */
+}
+
 bool Constraint::sanityChecking(Node n) const {
   Comparison cmp = Comparison::parseNormalForm(n);
   Kind k = cmp.comparisonKind();
@@ -1361,7 +1405,7 @@ Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){
 }
 
 Node Constraint::externalExplainConflict() const{
-  Debug("pf::arith") << this << std::endl;
+  Debug("pf::arith::explain") << this << std::endl;
   Assert(inConflict());
   NodeBuilder<> nb(kind::AND);
   externalExplainByAssertions(nb);
@@ -1431,11 +1475,11 @@ void Constraint::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{
   Assert(!isAssumption() || assertedToTheTheory());
   Assert(!isInternalAssumption());
 
-  if (Debug.isOn("pf::arith"))
+  if (Debug.isOn("pf::arith::explain"))
   {
-    Debug("pf::arith") << "Explaining: " << this << " with rule ";
-    getConstraintRule().print(Debug("pf::arith"));
-    Debug("pf::arith") << std::endl;
+    Debug("pf::arith::explain") << "Explaining: " << this << " with rule ";
+    getConstraintRule().print(Debug("pf::arith::explain"));
+    Debug("pf::arith::explain") << std::endl;
   }
 
   if(assertedBefore(order)){
@@ -1448,7 +1492,7 @@ void Constraint::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{
     ConstraintCP antecedent = d_database->d_antecedents[p];
 
     while(antecedent != NullConstraint){
-      Debug("pf::arith") << "Explain " << antecedent << std::endl;
+      Debug("pf::arith::explain") << "Explain " << antecedent << std::endl;
       antecedent->externalExplain(nb, order);
       --p;
       antecedent = d_database->d_antecedents[p];
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index f2c0c4b02..61b999a25 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -517,6 +517,8 @@ class Constraint {
   /** Returns true if the node has a trichotomy proof. */
   bool hasTrichotomyProof() const;
 
+  void printProofTree(std::ostream & out, size_t depth = 0) const;
+
   /**
    * A sets the constraint to be an internal assumption.
    *
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 2b8ce922d..76d8dbc01 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1194,7 +1194,7 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
       // 0 <= n[0] - toIntSkolem < 1
       Node one = mkRationalNode(1);
       Node lem = mkAxiomForTotalIntDivision(n[0], one, toIntSkolem);
-      d_containing.d_out->lemma(lem);
+      outputLemma(lem);
     }else{
       toIntSkolem = (*it).second;
     }
@@ -1247,7 +1247,7 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
                                         nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1))))))));                
       }    
       if( !lem.isNull() ){
-        d_containing.d_out->lemma(lem);
+        outputLemma(lem);
       }
     }else{
       intVar = (*it).second;
@@ -1270,7 +1270,7 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
     if( it==d_div_skolem.end() ){
       var = nm->mkSkolem("nonlinearDiv", nm->realType(), "the result of a non-linear div term");
       d_div_skolem[rw] = var;
-      d_containing.d_out->lemma(nm->mkNode(kind::IMPLIES, den.eqNode(nm->mkConst(Rational(0))).negate(), nm->mkNode(kind::MULT, den, var).eqNode(num)));
+      outputLemma(nm->mkNode(kind::IMPLIES, den.eqNode(nm->mkConst(Rational(0))).negate(), nm->mkNode(kind::MULT, den, var).eqNode(num)));
     }else{
       var = (*it).second;
     }
@@ -2017,6 +2017,10 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){
       ConstraintP floorConstraint = constraint->getFloor();
       if(!floorConstraint->isTrue()){
         bool inConflict = floorConstraint->negationHasProof();
+        if (Debug.isOn("arith::intbound")) {
+          Debug("arith::intbound") << "literal, before: " << constraint->getLiteral() << std::endl;
+          Debug("arith::intbound") << "constraint, after: " << floorConstraint << std::endl;
+        }
         floorConstraint->impliedByIntHole(constraint, inConflict);
         floorConstraint->tryToPropagate();
         if(inConflict){
@@ -2033,6 +2037,10 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){
       ConstraintP ceilingConstraint = constraint->getCeiling();
       if(!ceilingConstraint->isTrue()){
         bool inConflict = ceilingConstraint->negationHasProof();
+        if (Debug.isOn("arith::intbound")) {
+          Debug("arith::intbound") << "literal, before: " << constraint->getLiteral() << std::endl;
+          Debug("arith::intbound") << "constraint, after: " << ceilingConstraint << std::endl;
+        }
         ceilingConstraint->impliedByIntHole(constraint, inConflict);
         ceilingConstraint->tryToPropagate();
         if(inConflict){
@@ -2172,6 +2180,11 @@ void TheoryArithPrivate::outputConflicts(){
               << conflict[conflict.getNumChildren() - i - 1];
         }
 
+        if (Debug.isOn("arith::pf::tree")) {
+          confConstraint->printProofTree(Debug("arith::pf::tree"));
+          confConstraint->getNegation()->printProofTree(Debug("arith::pf::tree"));
+        }
+
         Assert(conflict.getNumChildren() == pf.d_farkasCoefficients->size());
         d_containing.d_proofRecorder->saveFarkasCoefficients(
             conflictInFarkasCoefficientOrder, pf.d_farkasCoefficients);
@@ -2181,7 +2194,7 @@ void TheoryArithPrivate::outputConflicts(){
         Debug("arith::conflict") << "(normalized to) " << conflict << endl;
       }
 
-      (d_containing.d_out)->conflict(conflict);
+      outputConflict(conflict);
     }
   }
   if(!d_blackBoxConflict.get().isNull()){
@@ -2195,15 +2208,30 @@ void TheoryArithPrivate::outputConflicts(){
       Debug("arith::conflict") << "(normalized to) " << bb << endl;
     }
 
-    (d_containing.d_out)->conflict(bb);
+    outputConflict(bb);
   }
 }
 
 void TheoryArithPrivate::outputLemma(TNode lem) {
-  Debug("arith::lemma") << "Arith Lemma: " << lem << std::endl;
+  Debug("arith::channel") << "Arith lemma: " << lem << std::endl;
   (d_containing.d_out)->lemma(lem);
 }
 
+void TheoryArithPrivate::outputConflict(TNode lit) {
+  Debug("arith::channel") << "Arith conflict: " << lit << std::endl;
+  (d_containing.d_out)->conflict(lit);
+}
+
+void TheoryArithPrivate::outputPropagate(TNode lit) {
+  Debug("arith::channel") << "Arith propagation: " << lit << std::endl;
+  (d_containing.d_out)->propagate(lit);
+}
+
+void TheoryArithPrivate::outputRestart() {
+  Debug("arith::channel") << "Arith restart!" << std::endl;
+  (d_containing.d_out)->demandRestart();
+}
+
 // void TheoryArithPrivate::branchVector(const std::vector<ArithVar>& lemmas){
 //   //output the lemmas
 //   for(vector<ArithVar>::const_iterator i = lemmas.begin(); i != lemmas.end();
@@ -4889,6 +4917,12 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
     //   * coeffs[i+1] is for explain[i]
     d_linEq.propagateRow(explain, ridx, rowUp, implied, coeffs);
     if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){
+      if (Debug.isOn("arith::prop::pf")) {
+        for (const auto & constraint : explain) {
+          Assert(constraint->hasProof());
+          constraint->printProofTree(Debug("arith::prop::pf"));
+        }
+      }
       Node implication = implied->externalImplication(explain);
       Node clause = flattenImplication(implication);
       PROOF(if (d_containing.d_proofRecorder
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 3f46ddd59..f964c4e04 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -655,8 +655,9 @@ private:
     d_nlIncomplete = true;
   }
   void outputLemma(TNode lem);
-  inline void outputPropagate(TNode lit) { (d_containing.d_out)->propagate(lit); }
-  inline void outputRestart() { (d_containing.d_out)->demandRestart(); }
+  void outputConflict(TNode lit);
+  void outputPropagate(TNode lit);
+  void outputRestart();
 
   inline bool isSatLiteral(TNode l) const {
     return (d_containing.d_valuation).isSatLiteral(l);