Revert

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

Hide file tree

Showing 2 changed files with 25 additions and 5 deletions.
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -796,10 +796,13 @@ 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);
-      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));
+      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)));
     }
   }
   return ret;

diff --git a/src/theory/arith/rewrites b/src/theory/arith/rewrites
@@ -79,5 +79,22 @@
 (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))))
+;(define-rule arith-abs-int-gt ((x Int) (y Int)) 
+;  (> (abs x) (abs y)) 
+;  (ite (>= x 0)
+;    (ite (>= y 0)
+;      (> x y)
+;      (> x (- y)))
+;    (ite (>= y 0)
+;      (> (- x) y)
+;      (> (- x) (- y)))))
+;  
+;(define-rule arith-abs-real-gt ((x Real) (y Real)) 
+;  (> (abs x) (abs y)) 
+;  (ite (>= x 0/1)
+;    (ite (>= y 0/1)
+;      (> x y)
+;      (> x (- y)))
+;    (ite (>= y 0/1)
+;      (> (- x) y)
+;      (> (- x) (- y)))))