Add proof for mult sign lemma (#5966)

This PR adds the proof for a nonlinear refinement lemma that infers the sign of a monomial from the sign of the variables.

4 files changed, 95 insertions, 2 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index cc5613057..d29aca6ea 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -159,6 +159,7 @@ const char* toString(PfRule id)
     case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB";
     case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB";
     case PfRule::INT_TRUST: return "INT_TRUST";
+    case PfRule::ARITH_MULT_SIGN: return "ARITH_MULT_SIGN";
     case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS";
     case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG";
     case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index bf6f1d6ae..76c2d0958 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -1092,6 +1092,18 @@ enum class PfRule : uint32_t
   // Conclusion: (Q)
   INT_TRUST,
 
+  //======== Multiplication sign inference
+  // Children: none
+  // Arguments: (f1, ..., fk, m)
+  // ---------------------
+  // Conclusion: (=> (and f1 ... fk) (~ m 0))
+  // Where f1, ..., fk are variables compared to zero (less, greater or not
+  // equal), m is a monomial from these variables, and ~ is the comparison (less
+  // or greater) that results from the signs of the variables. All variables
+  // with even exponent in m should be given as not equal to zero while all
+  // variables with odd exponent in m should be given as less or greater than
+  // zero.
+  ARITH_MULT_SIGN,
   //======== Multiplication with positive factor
   // Children: none
   // Arguments: (m, orig, lhs, rel, rhs)
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index c6ee3d764..a3e56358b 100644
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -295,7 +295,15 @@ int MonomialCheck::compareSign(
     {
       Node lemma =
           nm->mkAnd(exp).impNode(mkLit(oa, d_data->d_zero, status * 2));
-      d_data->d_im.addPendingLemma(lemma, InferenceId::ARITH_NL_SIGN);
+      CDProof* proof = nullptr;
+      if (d_data->isProofEnabled())
+      {
+        proof = d_data->getProof();
+        std::vector<Node> args = exp;
+        args.emplace_back(oa);
+        proof->addStep(lemma, PfRule::ARITH_MULT_SIGN, {}, args);
+      }
+      d_data->d_im.addPendingLemma(lemma, InferenceId::ARITH_NL_SIGN, proof);
     }
     return status;
   }
diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp
index a0c5d2021..e3e26cb65 100644
--- a/src/theory/arith/nl/ext/proof_checker.cpp
+++ b/src/theory/arith/nl/ext/proof_checker.cpp
@@ -27,6 +27,7 @@ namespace nl {
 
 void ExtProofRuleChecker::registerTo(ProofChecker* pc)
 {
+  pc->registerChecker(PfRule::ARITH_MULT_SIGN, this);
   pc->registerChecker(PfRule::ARITH_MULT_POS, this);
   pc->registerChecker(PfRule::ARITH_MULT_NEG, this);
   pc->registerChecker(PfRule::ARITH_MULT_TANGENT, this);
@@ -47,7 +48,78 @@ Node ExtProofRuleChecker::checkInternal(PfRule id,
   {
     Trace("nl-ext-checker") << "\t" << c << std::endl;
   }
-  if (id == PfRule::ARITH_MULT_POS)
+  if (id == PfRule::ARITH_MULT_SIGN)
+  {
+    Assert(children.empty());
+    Assert(args.size() > 1);
+    Node mon = args.back();
+    std::map<Node, int> exps;
+    std::vector<Node> premise = args;
+    premise.pop_back();
+    Assert(mon.getKind() == Kind::MULT
+           || mon.getKind() == Kind::NONLINEAR_MULT);
+    for (const auto& v : mon)
+    {
+      exps[v]++;
+    }
+    std::map<Node, int> signs;
+    for (const auto& f : premise)
+    {
+      if (f.getKind() == Kind::NOT)
+      {
+        Assert(f[0].getKind() == Kind::EQUAL);
+        Assert(f[0][1].isConst() && f[0][1].getConst<Rational>().isZero());
+        Assert(signs.find(f[0][0]) == signs.end());
+        signs.emplace(f[0][0], 0);
+        continue;
+      }
+      Assert(f.getKind() == Kind::LT || f.getKind() == Kind::GT);
+      Assert(f[1].isConst() && f[1].getConst<Rational>().isZero());
+      Assert(signs.find(f[0]) == signs.end());
+      signs.emplace(f[0], f.getKind() == Kind::LT ? -1 : 1);
+    }
+    int sign = 0;
+    for (const auto& ve : exps)
+    {
+      auto sit = signs.find(ve.first);
+      Assert(sit != signs.end());
+      if (ve.second % 2 == 0)
+      {
+        Assert(sit->second == 0);
+        if (sign == 0)
+        {
+          sign = 1;
+        }
+      }
+      else
+      {
+        Assert(sit->second != 0);
+        if (sign == 0)
+        {
+          sign = sit->second;
+        }
+        else
+        {
+          sign *= sit->second;
+        }
+      }
+    }
+    switch (sign)
+    {
+      case -1:
+        return nm->mkNode(
+            Kind::IMPLIES, nm->mkAnd(premise), nm->mkNode(Kind::GT, zero, mon));
+      case 0:
+        return nm->mkNode(Kind::IMPLIES,
+                          nm->mkAnd(premise),
+                          nm->mkNode(Kind::DISTINCT, mon, zero));
+      case 1:
+        return nm->mkNode(
+            Kind::IMPLIES, nm->mkAnd(premise), nm->mkNode(Kind::GT, mon, zero));
+      default: Assert(false); return Node();
+    }
+  }
+  else if (id == PfRule::ARITH_MULT_POS)
   {
     Assert(children.empty());
     Assert(args.size() == 3);