Simplifications, draft RARE rules

ajreynol · Oct 18, 2024 · a197e07 · a197e07
1 parent 951a3cd
commit a197e07
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 88 deletions.
diff --git a/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp b/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp
@@ -356,69 +356,6 @@ Node ArithNlCompareProofGenerator::isDisequalZero(const Node& g)
   return Node::null();
 }
 
-/*
-bool ArithNlCompareProofGenerator::diffProduct(const std::vector<Node>& a,
-                                               const std::vector<Node>& b,
-                                               std::map<Node, size_t>& diff)
-{
-  size_t indexb = 0;
-  for (size_t i = 0, nmona = a.size(); i < nmona; i++)
-  {
-    if (indexb < b.size() && b[indexb] == a[i])
-    {
-      indexb++;
-    }
-    else
-    {
-      diff[a[i]]++;
-    }
-  }
-  // success if we consumed all
-  return (indexb == b.size());
-}
-
-void ArithNlCompareProofGenerator::iterateWhile(const Node& a,
-                                                const std::vector<Node>& avec,
-                                                size_t& aindex)
-{
-  size_t asize = avec.size();
-  while (aindex < asize && avec[aindex] == a)
-  {
-    aindex++;
-  }
-}
-void ArithNlCompareProofGenerator::iterateWhileCmp(
-    const Node& a,
-    const std::vector<Node>& avec,
-    size_t& aindex,
-    const Node& b,
-    const std::vector<Node>& bvec,
-    size_t& bindex)
-{
-  size_t asize = avec.size();
-  size_t bsize = bvec.size();
-  while (aindex < asize && bindex < bsize && avec[aindex] == a
-         && bvec[bindex] == b)
-  {
-    aindex++;
-    bindex++;
-  }
-}
-void ArithNlCompareProofGenerator::iterateWhileEq(const std::vector<Node>& avec,
-                                                  size_t& aindex,
-                                                  const std::vector<Node>& bvec,
-                                                  size_t& bindex)
-{
-  size_t asize = avec.size();
-  size_t bsize = bvec.size();
-  while (aindex < asize && bindex < bsize && avec[aindex] == bvec[bindex])
-  {
-    aindex++;
-    bindex++;
-  }
-}
-*/
-
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory

diff --git a/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.h b/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.h
@@ -59,25 +59,6 @@ class ArithNlCompareProofGenerator : protected EnvObj, public ProofGenerator
                                   bool isSingleton);
   /** */
   static Node isDisequalZero(const Node& lit);
-
-  /**
-  static bool diffProduct(const std::vector<Node>& a,
-                          const std::vector<Node>& b,
-                          std::map<Node, size_t>& diff);
-  static void iterateWhile(const Node& a,
-                           const std::vector<Node>& avec,
-                           size_t& index);
-  static void iterateWhileCmp(const Node& a,
-                              const std::vector<Node>& avec,
-                              size_t& aindex,
-                              const Node& b,
-                              const std::vector<Node>& bvec,
-                              size_t& bindex);
-  static void iterateWhileEq(const std::vector<Node>& avec,
-                             size_t& aindex,
-                             const std::vector<Node>& bvec,
-                             size_t& bindex);
-                             */
 };
 
 }  // namespace nl

diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -796,13 +796,10 @@ Node MonomialCheck::mkLit(Node a, Node b, int status, bool isAbsolute) const
       Node zero = mkZero(a.getType());
       Node a_is_nonnegative = nm->mkNode(Kind::GEQ, a, zero);
       Node b_is_nonnegative = nm->mkNode(Kind::GEQ, b, zero);
-      Node negate_a = nm->mkNode(Kind::NEG, a);
       Node negate_b = nm->mkNode(Kind::NEG, b);
-      ret = a_is_nonnegative.iteNode(
-          b_is_nonnegative.iteNode(nm->mkNode(k, a, b),
-                                   nm->mkNode(k, a, negate_b)),
-          b_is_nonnegative.iteNode(nm->mkNode(k, negate_a, b),
-                                   nm->mkNode(k, negate_a, negate_b)));
+      Node polEq = a_is_nonnegative.eqNode(b_is_nonnegative);
+      ret = nm->mkNode(Kind::ITE, polEq, nm->mkNode(k, a, b),
+                                   nm->mkNode(k, a, negate_b));
     }
   }
   return ret;

diff --git a/src/theory/arith/rewrites b/src/theory/arith/rewrites
@@ -77,3 +77,7 @@
 (define-rule arith-cotangent-elim ((x Real)) (cot x) (/ (cos x) (sin x)))
 
 (define-rule arith-pi-not-int () (is_int real.pi) false)
+
+;(define-rule arith-abs-eq ((x ?) (y ?)) (= (abs x) (abs y)) (or (= x y) (= x (- y))))
+;(define-rule arith-abs-int-gt ((x Int) (y Int)) (> (abs x) (abs y)) (ite (= (>= x 0) (>= y 0)) (= x y) (= x (- y))))
+;(define-rule arith-abs-real-gt ((x Real) (y Real)) (> (abs x) (abs y)) (ite (= (>= x 0/1) (>= y 0/1)) (= x y) (= x (- y))))