Expand arith's farkas lemma rule as a macro (#6577)

reflects that it is a macro, which we will eliminate

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index fbeaea72945bc72a4e4e4dcb476e123f4546fae4..02323b6062553ff3ac1dd172cfacb78a85a10ad0 100644 (file)
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -196,7 +196,9 @@ const char* toString(PfRule id)
     case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ";
     case PfRule::STRING_TRUST: return "STRING_TRUST";
     //================================================= Arith rules
-    case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS: return "ARITH_SCALE_SUM_UPPER_BOUNDS";
+    case PfRule::MACRO_ARITH_SCALE_SUM_UB:
+      return "ARITH_SCALE_SUM_UPPER_BOUNDS";
+    case PfRule::ARITH_SUM_UB: return "ARITH_SUM_UB";
     case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY";
     case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB";
     case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB";

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 4730df652571ea5bf44378ef5b3fba234328d28a..cfab15614f560391b1b70765e12e68b9a5edaecd 100644 (file)
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -1124,8 +1124,7 @@ enum class PfRule : uint32_t
   //    t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n *
   //    poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n
   //    * const_n)
-  ARITH_SCALE_SUM_UPPER_BOUNDS,
-
+  MACRO_ARITH_SCALE_SUM_UB,
   // ======== Sum Upper Bounds
   // Children: (P1, ... , Pn)
   //           where each Pi has form (><i, Li, Ri)

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 618cdebacf865f0b6689b47b6930129b720cfa80..f98d1d72773a7830f4d80946bb647b5ed87a464c 100644 (file)
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -1028,6 +1028,58 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     // otherwise no update
     Trace("final-pf-hole") << "hole: " << id << " : " << eq << std::endl;
   }
+  else if (id == PfRule::MACRO_ARITH_SCALE_SUM_UB)
+  {
+    Debug("macro::arith") << "Expand MACRO_ARITH_SCALE_SUM_UB" << std::endl;
+    if (Debug.isOn("macro::arith"))
+    {
+      for (const auto& child : children)
+      {
+        Debug("macro::arith") << "  child: " << child << std::endl;
+      }
+      Debug("macro::arith") << "   args: " << args << std::endl;
+    }
+    Assert(args.size() == children.size());
+    NodeManager* nm = NodeManager::currentNM();
+    ProofStepBuffer steps{d_pnm->getChecker()};
+
+    // Scale all children, accumulating
+    std::vector<Node> scaledRels;
+    for (size_t i = 0; i < children.size(); ++i)
+    {
+      TNode child = children[i];
+      TNode scalar = args[i];
+      bool isPos = scalar.getConst<Rational>() > 0;
+      Node scalarCmp =
+          nm->mkNode(isPos ? GT : LT, scalar, nm->mkConst(Rational(0)));
+      // (= scalarCmp true)
+      Node scalarCmpOrTrue = steps.tryStep(PfRule::EVALUATE, {}, {scalarCmp});
+      Assert(!scalarCmpOrTrue.isNull());
+      // scalarCmp
+      steps.addStep(PfRule::TRUE_ELIM, {scalarCmpOrTrue}, {}, scalarCmp);
+      // (and scalarCmp relation)
+      Node scalarCmpAndRel =
+          steps.tryStep(PfRule::AND_INTRO, {scalarCmp, child}, {});
+      Assert(!scalarCmpAndRel.isNull());
+      // (=> (and scalarCmp relation) scaled)
+      Node impl =
+          steps.tryStep(isPos ? PfRule::ARITH_MULT_POS : PfRule::ARITH_MULT_NEG,
+                        {},
+                        {scalar, child});
+      Assert(!impl.isNull());
+      // scaled
+      Node scaled =
+          steps.tryStep(PfRule::MODUS_PONENS, {scalarCmpAndRel, impl}, {});
+      Assert(!scaled.isNull());
+      scaledRels.emplace_back(scaled);
+    }
+
+    Node sumBounds = steps.tryStep(PfRule::ARITH_SUM_UB, scaledRels, {});
+    cdp->addSteps(steps);
+    Debug("macro::arith") << "Expansion done. Proved: " << sumBounds
+                          << std::endl;
+    return sumBounds;
+  }
 
   // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
 

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 23bdb20f6850652490e4dfd3c909ef53c1ebe4b2..3d5e7270bb40aab27a7fcb260b05073360dee510 100644 (file)
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -311,7 +311,7 @@ void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){
       const auto isZeroPf = d_pnm->mkAssume(isZero);
       const auto nm = NodeManager::currentNM();
       const auto sumPf = d_pnm->mkNode(
-          PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
+          PfRule::MACRO_ARITH_SCALE_SUM_UB,
           {isZeroPf, pf},
           // Trick for getting correct, opposing signs.
           {nm->mkConst(Rational(-1 * cSign)), nm->mkConst(Rational(cSign))});

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index fc2506f8483245a7e5bb278178738792ec37ec53..15dfe47914073a6f16f6ff1e4ea29605cd47fae4 100644 (file)
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -1092,7 +1092,7 @@ TrustNode Constraint::split()
     auto ltPf = d_database->d_pnm->mkNode(
         PfRule::MACRO_SR_PRED_TRANSFORM, {nGeqPf}, {ltNode});
     auto sumPf = d_database->d_pnm->mkNode(
-        PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
+        PfRule::MACRO_ARITH_SCALE_SUM_UB,
         {gtPf, ltPf},
         {nm->mkConst<Rational>(-1), nm->mkConst<Rational>(1)});
     auto botPf = d_database->d_pnm->mkNode(
@@ -1779,10 +1779,8 @@ std::shared_ptr<ProofNode> Constraint::externalExplain(
           }
 
           // Apply the scaled-sum rule.
-          std::shared_ptr<ProofNode> sumPf =
-              pnm->mkNode(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
-                          farkasChildren,
-                          farkasCoeffs);
+          std::shared_ptr<ProofNode> sumPf = pnm->mkNode(
+              PfRule::MACRO_ARITH_SCALE_SUM_UB, farkasChildren, farkasCoeffs);
 
           // Provable rewrite the result
           auto botPf = pnm->mkNode(
@@ -2081,7 +2079,7 @@ void ConstraintDatabase::proveOr(std::vector<TrustNode>& out,
     int sndSign = negateSecond ? -1 : 1;
     auto bot_pf =
         d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
-                      {d_pnm->mkNode(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
+                      {d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
                                      {pf_neg_la, pf_neg_lb},
                                      {nm->mkConst<Rational>(-1 * sndSign),
                                       nm->mkConst<Rational>(sndSign)})},

diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp
index 535d6b09018b163b1680d032912519f464d06317..4e25ae76ba0d00b0d1936af30220fad76fde84b3 100644 (file)
--- a/src/theory/arith/proof_checker.cpp
+++ b/src/theory/arith/proof_checker.cpp
@@ -30,7 +30,7 @@ namespace arith {
 
 void ArithProofRuleChecker::registerTo(ProofChecker* pc)
 {
-  pc->registerChecker(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, this);
+  pc->registerChecker(PfRule::MACRO_ARITH_SCALE_SUM_UB, this);
   pc->registerChecker(PfRule::ARITH_SUM_UB, this);
   pc->registerChecker(PfRule::ARITH_TRICHOTOMY, this);
   pc->registerChecker(PfRule::INT_TIGHT_UB, this);
@@ -141,21 +141,30 @@ Node ArithProofRuleChecker::checkInternal(PfRule id,
                           rightSum.constructNode());
       return r;
     }
-    case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS:
+    case PfRule::MACRO_ARITH_SCALE_SUM_UB:
     {
+      //================================================= Arithmetic rules
+      // ======== Adding Inequalities
+      // Note: an ArithLiteral is a term of the form (>< poly const)
+      // where
+      //   >< is >=, >, ==, <, <=, or not(== ...).
+      //   poly is a polynomial
+      //   const is a rational constant
+
       // Children: (P1:l1, ..., Pn:ln)
       //           where each li is an ArithLiteral
       //           not(= ...) is dis-allowed!
       //
       // Arguments: (k1, ..., kn), non-zero reals
       // ---------------------
-      // Conclusion: (>< (* k t1) (* k t2))
+      // Conclusion: (>< t1 t2)
       //    where >< is the fusion of the combination of the ><i, (flipping each
       //    it its ki is negative). >< is always one of <, <= NB: this implies
       //    that lower bounds must have negative ki,
       //                      and upper bounds must have positive ki.
-      //    t1 is the sum of the polynomials.
-      //    t2 is the sum of the constants.
+      //    t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n *
+      //    poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... +
+      //    k_n * const_n)
       Assert(children.size() == args.size());
       if (children.size() < 2)
       {
@@ -234,9 +243,9 @@ Node ArithProofRuleChecker::checkInternal(PfRule id,
           }
         }
         leftSum << nm->mkNode(
-            Kind::MULT, children[i][0], nm->mkConst<Rational>(scalar));
+            Kind::MULT, nm->mkConst<Rational>(scalar), children[i][0]);
         rightSum << nm->mkNode(
-            Kind::MULT, children[i][1], nm->mkConst<Rational>(scalar));
+            Kind::MULT, nm->mkConst<Rational>(scalar), children[i][1]);
       }
       Node r = nm->mkNode(strict ? Kind::LT : Kind::LEQ,
                           leftSum.constructNode(),

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index a4a5ad229d817a060a46931fc9f401dfa68105ea..911954a5a0f178ae4244e6ad485aaaf8f2366864 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1460,7 +1460,7 @@ TrustNode TheoryArithPrivate::dioCutting()
       Pf pfLt =
           d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pfNotGeq}, {lt});
       Pf pfSum =
-          d_pnm->mkNode(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
+          d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
                         {pfGt, pfLt},
                         {nm->mkConst<Rational>(-1), nm->mkConst<Rational>(1)});
       Pf pfBot = d_pnm->mkNode(
@@ -4547,9 +4547,8 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
             [nm](const Rational& r) { return nm->mkConst<Rational>(r); });
 
         // Prove bottom.
-        auto sumPf = d_pnm->mkNode(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
-                                   conflictPfs,
-                                   farkasCoefficients);
+        auto sumPf = d_pnm->mkNode(
+            PfRule::MACRO_ARITH_SCALE_SUM_UB, conflictPfs, farkasCoefficients);
         auto botPf = d_pnm->mkNode(
             PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});