Merge pull request #14 from gwils/self-negate2

Implement logic for equalities involving the same variable twice
ekmett · Apr 17, 2019 · 4434198 · 4434198
2 parents a216ea4 + fe2ccf9
commit 4434198
Show file tree

Hide file tree

Showing 2 changed files with 123 additions and 2 deletions.
diff --git a/src/Domain/Internal.hs b/src/Domain/Internal.hs
@@ -271,6 +271,12 @@ no :: Unit -> a -> a -> a
 no One x _ = x
 no NegativeOne _ y = y
 
+inside :: MonadRef m => Either (Ps m) Z -> Either (Ps m) Z -> Z -> Bool
+inside (Right lo) (Right hi) z = lo <= z && z <= hi
+inside (Left _) (Right hi) z = z <= hi
+inside (Right lo) (Left _) z = lo <= z
+inside (Left _) (Left _) _ = True
+
 -- this is a special case when we go to define 'addition' and only two of the entries are non-constant
 -- and is implemented by union-find rather than propagation
 -- union x f y means x := f(y), y = (f^-1)(x)
@@ -279,9 +285,34 @@ eqRef x d y = do
   (xd, R xrank xlo xhi xlop xhip xcov, xroot) <- findRef x
   (yd, R yrank ylo yhi ylop yhip ycov, yroot) <- findRef y
   -- xroot = t(yroot)
-  let t@(Aff u _) = inv xd <> d <> yd
+  -- o(xroot) = yroot
+  let t@(Aff u k) = inv xd <> d <> yd
       o = inv t
-  if xrank < yrank then do
+  if xroot == yroot then do
+    let zlop = no u ylop yhip
+        zhip = no u yhip ylop
+        (todo,  xlo') = maxx zlop xlop t (no u ylo yhi) xlo
+        (todo', xhi') = minx zhip xhip t (no u yhi ylo) xhi
+    case u of
+      -- eg. x = -x+4 --> x must be 2
+      NegativeOne -> do
+        let solution = k `div` 2
+            result = mkR (yrank+1) (Right solution) (Right solution) nil nil nil
+        guard $ even k && inside xlo' xhi' solution
+        writeRef xroot $ Root result
+        runPs (todo <> todo') xroot
+        runKs (rel t ycov <> xcov) solution
+      -- x = x+c --> c must be zero
+      One -> do
+        guard $ k == 0
+        let result = mkR (yrank+1) xlo' xhi' (xlop <> rel t zlop)
+              (xhip <> rel t zhip) (xcov <> rel t ycov)
+        writeRef xroot $ Root result
+        runPs (todo <> todo') xroot
+        case covered result of
+          Just z -> runKs (rel t ycov <> xcov) z
+          Nothing -> pure ()
+  else if xrank < yrank then do
     writeRef xroot $ Child t yroot
     let zlop = no u xlop xhip
         zhip = no u xhip xlop

diff --git a/test/Spec/Domain/Interval.hs b/test/Spec/Domain/Interval.hs
@@ -116,6 +116,96 @@ spec = do
       --       x `gt` y
       --       knowns x y
       --   result `shouldBe` [(Just 2,Just 1)]
+      it "x = x+4" $ do
+        let
+          result = run $ do
+            x <- 1...5
+            x `eq` (x `plus` 4)
+            concrete x
+        result `shouldBe` []
+      it "x+4 = x" $ do
+        let
+          result = run $ do
+            x <- 1...5
+            (x `plus` 4) `eq` x
+            concrete x
+        result `shouldBe` []
+      it "x+3 = x+3" $ do
+        let
+          result = run $ do
+            input <- 0...5
+            let added = input `plus` 3
+            eq added added
+            concrete added
+        result `shouldBe` [3,4,5,6,7,8]
+      it "x = -x overlapping" $ do
+        let
+          result = run $ do
+            input <- (-3)...4
+            negd <- bottom
+            negatei input negd
+            eq input negd
+            (,) <$> concrete input <*> concrete negd
+        result `shouldBe` [(0,0)]
+      it "x = -x non-overlaping" $ do
+        let
+          result = run $ do
+            input <- 2...5
+            negd <- bottom
+            negatei input negd
+            eq input negd
+            (,) <$> concrete input <*> concrete negd
+        result `shouldBe` []
+      it "x = -x+5 (odd case) (no integer solution)" $ do
+        let
+          result = run $ do
+            input <- 2...5 --solution is 2.5
+            negd <- bottom
+            negatei input negd
+            let added = negd `plus` 5
+            eq input added
+            (,) <$> concrete input <*> concrete added
+        result `shouldBe` []
+      it "x = -x+4 (even case) with solution" $ do
+        let
+          result = run $ do
+            input <- 1...5 --solution is 2
+            negd <- bottom
+            negatei input negd
+            let added = negd `plus` 4
+            eq input added
+            (,) <$> concrete input <*> concrete added
+        result `shouldBe` [(2,2)]
+      it "-x+4 = x (even case) with solution" $ do
+        let
+          result = run $ do
+            input <- 1...5 --solution is 2
+            negd <- bottom
+            negatei input negd
+            let added = negd `plus` 4
+            eq added input
+            (,) <$> concrete input <*> concrete added
+        result `shouldBe` [(2,2)]
+      it "x-4 = -x (even case) with solution" $ do
+        let
+          result = run $ do
+            input <- 1...5 --solution is 2
+            negd <- bottom
+            negatei input negd
+            let added = input `plus` (-4)
+            eq added negd
+            (,) <$> concrete negd <*> concrete added
+        result `shouldBe` [(-2,-2)]
+      it "x = -x+4 (even case) without solution" $ do
+        let
+          result = run $ do
+            input <- 3...5 --solution is 2
+            negd <- bottom
+            negatei input negd
+            let added = negd `plus` 4
+            eq input added
+            (,) <$> concrete input <*> concrete added
+        result `shouldBe` []
       it "[1] le [1..2]" $ do
         let
           result = run $ do