diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -1,8 +1,8 @@ # Builds and tests this Haskell project on "GitHub Actions" # -# 2021-2023 Rudy Matela +# 2021-2024 Rudy Matela # -# some docs: https://github.com/haskell/actions/tree/main/setup +# some docs: https://github.com/haskell-actions/setup # # The official haskell docker image: https://hub.docker.com/_/haskell name: build @@ -11,58 +11,66 @@ build-and-test: runs-on: ubuntu-latest steps: + - run: git --version + - run: make --version + - run: ghc --version + - run: cabal --version - - name: Cache ~/.cabal/packages + - name: Check out repository + uses: actions/checkout@v3 + + # check out needs to happen before cache so that hashing works + - name: Cache hash + run: echo Cache hash = ${{ hashFiles('*.cabal') }} + + - name: Cache cabal (source) packages uses: actions/cache@v3 with: - path: ~/.cabal/packages + path: | + ~/.cabal/packages + ~/.cache/cabal key: v1-${{ runner.os }}-cabal-packages-${{ hashFiles('*.cabal') }} restore-keys: v1-${{ runner.os }}-cabal-packages- - - name: Cache ~/.cabal and ~/.ghc + - name: Cache installed cabal packages uses: actions/cache@v3 with: path: | ~/.cabal !~/.cabal/packages + ~/.config/cabal + ~/.local/state/cabal ~/.ghc key: v1-${{ runner.os }}-cabal-ghc-latest-${{ hashFiles('*.cabal') }} - restore-keys: v1-${{ runner.os }}-cabal-ghc-latest- - - - run: du -hd3 ~/.cabal ~/.ghc || true - - - run: make --version + restore-keys: v1-${{ runner.os }}-cabal-ghc-latest-${{ hashFiles('*.cabal') }} + # restore with exact match has some versions of cabal have trouble updating - run: haddock --version || sudo apt-get install ghc-haddock - - run: ghc --version - - run: cabal --version - - run: haddock --version - - run: ghc-pkg list - - - name: Check out repository - uses: actions/checkout@v3 + # blank line + # blank line for alignment with matrix scripts - - run: git --version + - run: du -hd3 ~/.ghc ~/.cabal ~/.config/cabal ~/.cache/cabal ~/.local/state/cabal || true + - run: ghc-pkg list - run: make install-dependencies + - run: ghc-pkg list - # 2023-07: some projects were failing with missing base for GHC 9.6. - # Here we compile through cabal only provisionally. - # - run: make - # - run: make test - # - run: make haddock + - run: du -hd3 ~/.ghc ~/.cabal ~/.config/cabal ~/.cache/cabal ~/.local/state/cabal || true + + - run: make + - run: make test + - run: make haddock - run: make test-sdist - #- run: make test-via-cabal - - run: cabal configure --enable-tests --enable-benchmarks --ghc-options="-O0" - - run: cabal build - - run: cabal test - - run: cabal haddock + - run: make test-via-cabal test-with-ghc: strategy: + max-parallel: 6 matrix: ghc: + - '9.8' + - '9.6' - '9.4' - '9.2' - '9.0' @@ -73,39 +81,52 @@ needs: build-and-test container: haskell:${{ matrix.ghc }} steps: - - name: Cache ~/.cabal/packages + - run: git --version || true # git is missing in some images + - run: make --version || true # make is missing in some images + - run: ghc --version + - run: cabal --version + + - name: Check out repository + uses: actions/checkout@v3 + + # check out needs to happen before cache so that hashing works + - name: Cache hash + run: echo Cache hash = ${{ hashFiles('*.cabal') }} + + - name: Cache cabal (source) packages uses: actions/cache@v3 with: - path: ~/.cabal/packages + path: | + ~/.cabal/packages + ~/.cache/cabal key: v1-${{ runner.os }}-cabal-packages-${{ hashFiles('*.cabal') }} restore-keys: v1-${{ runner.os }}-cabal-packages- - - name: Cache ~/.cabal and ~/.ghc + - name: Cache installed cabal packages uses: actions/cache@v3 with: path: | ~/.cabal !~/.cabal/packages + ~/.config/cabal + ~/.local/state/cabal ~/.ghc key: v1-${{ runner.os }}-cabal-ghc-${{ matrix.ghc }}-${{ hashFiles('*.cabal') }} - restore-keys: v1-${{ runner.os }}-cabal-ghc-${{ matrix.ghc }}- - - - run: du -hd3 ~/.cabal ~/.ghc || true + restore-keys: v1-${{ runner.os }}-cabal-ghc-${{ matrix.ghc }}-${{ hashFiles('*.cabal') }} + # restore with exact match has some versions of cabal have trouble updating - run: make --version || rm /etc/apt/sources.list.d/*.list # faster update - run: make --version || apt-get update - run: make --version || apt-get install make - - run: ghc --version - - run: cabal --version - - run: haddock --version - - run: ghc-pkg list - - - name: Check out repository - uses: actions/checkout@v3 + - run: du -hd3 ~/.ghc ~/.cabal ~/.config/cabal ~/.cache/cabal ~/.local/state/cabal || true + - run: ghc-pkg list - run: make install-dependencies + - run: ghc-pkg list + - run: du -hd3 ~/.ghc ~/.cabal ~/.config/cabal ~/.cache/cabal ~/.local/state/cabal || true + - run: make - run: make test - run: make haddock @@ -116,20 +137,41 @@ runs-on: ubuntu-latest needs: build-and-test steps: - - name: Setup Haskell's GHC and Cabal as required by current Stackage LTS - uses: haskell/actions/setup@v2 - with: # lts-19.19 - ghc-version: '9.0.2' - cabal-version: '3.4' + - name: Check out repository + uses: actions/checkout@v3 - - uses: actions/cache@v3 + # check out needs to happen before cache so that hashing works + - name: Cache hash + run: echo Cache hash = ${{ hashFiles('stack.yaml') }} + + - name: Cache stack folder + uses: actions/cache@v3 with: path: ~/.stack key: v1-${{ runner.os }}-stack-${{ hashFiles('stack.yaml') }} restore-keys: v1-${{ runner.os }}-stack- + - name: Cache ghcup folder + uses: actions/cache@v3 + with: + path: | + ~/.ghcup + /usr/local/.ghcup/bin + /usr/local/.ghcup/db + /usr/local/.ghcup/ghc/9.0.2 + key: v1-${{ runner.os }}-ghcup-${{ hashFiles('stack.yaml') }} + restore-keys: v1-${{ runner.os }}-ghcup- + + - name: Setup Haskell's GHC and Cabal as required by current Stackage LTS + uses: haskell-actions/setup@v2 + with: # lts-19.19 + ghc-version: '9.0.2' + cabal-version: '3.4' + + - run: du -hd2 ~/.stack ~/.ghcup /usr/local/.ghcup || true + - run: stack --version - - name: Check out repository - uses: actions/checkout@v3 - run: make test-via-stack + + - run: du -hd2 ~/.stack ~/.ghcup /usr/local/.ghcup || true diff --git a/Makefile b/Makefile --- a/Makefile +++ b/Makefile @@ -10,6 +10,9 @@ | grep -v "^Warning: Couldn't find .haddock for export [A-Z]$$" INSTALL_DEPS = leancheck express speculate template-haskell +NJOBS := $(shell grep ^processor /proc/cpuinfo | head -n -1 | wc -l | sed 's/^0$$/1/') +LONG := $(shell which long >/dev/null 2>/dev/null && echo long) + EG = \ eg/arith \ eg/count \ @@ -104,6 +107,16 @@ test-via-stack: stack test code-conjure:test:expr --ghc-options="$(GHCFLAGS) -O0" --system-ghc --no-install-ghc --no-terminal + + +fastest: + $(LONG) make test -j$(NJOBS) + +fastestbench: + $(LONG) make test -j$(NJOBS) && $(LONG) make bench + +fastxtestbench: + $(LONG) make txt -j$(NJOBS) && $(LONG) make test -j$(NJOBS) && $(LONG) make bench clean: clean-hi-o clean-haddock rm -f $(EG) $(TESTS) mk/toplibs diff --git a/TODO.md b/TODO.md --- a/TODO.md +++ b/TODO.md @@ -6,8 +6,6 @@ * improve documentation of `conjureIsDeconstruction`. Document behaviour outside of function, not inside of it. -* `bench/erroneous`: report number of errors in addition to the example error - * consider non top-level cases diff --git a/bench/candidates.hs b/bench/candidates.hs --- a/bench/candidates.hs +++ b/bench/candidates.hs @@ -37,14 +37,14 @@ [ pr (0 :: Int) , pr (1 :: Int) , prim "+" ((+) :: Int -> Int -> Int) - , prim "*" ((+) :: Int -> Int -> Int) + , prim "*" ((*) :: Int -> Int -> Int) , prim "-" ((-) :: Int -> Int -> Int) ] - printCandidates 9 6 "?" (undefined :: Int -> Int -> Int) + printCandidates 9 5 "?" (undefined :: Int -> Int -> Int) [ pr (0 :: Int) , prim "+" ((+) :: Int -> Int -> Int) - , prim "*" ((+) :: Int -> Int -> Int) + , prim "*" ((*) :: Int -> Int -> Int) , prim "dec" (subtract 1 :: Int -> Int) ] diff --git a/bench/candidates.txt b/bench/candidates.txt --- a/bench/candidates.txt +++ b/bench/candidates.txt @@ -1,2111 +1,1589 @@ Candidates for: foo :: Int -> Int - pruning with 15/35 rules - [3,0,7,0,19,0,90,0,454] direct candidates, 0 duplicates - [3,3,8,9,21,27,98,133,461] pattern candidates, 0 duplicates - -rules: -x * y == x + y -x * y == y + x -x - x == 0 -x + 0 == x -0 + x == x -x - 0 == x -(x + y) + z == x + (y + z) -(x + y) + z == y + (x + z) -x - (y - z) == z + (x - y) -(x - y) - z == x - (y + z) -(x - y) - z == x - (z + y) -(x + y) - z == x + (y - z) -(x + y) - z == y + (x - z) -x + (y - x) == y -(x - y) + y == x -equations: -y + x == x + y -y + (x + z) == x + (y + z) -z + (x + y) == x + (y + z) -z + (y + x) == x + (y + z) -y + (x - z) == x + (y - z) -(x - z) + y == x + (y - z) -(z - y) + x == (x - y) + z -y - (x + y) == 0 - x -y - (y + x) == 0 - x -z - (y + z) == x - (x + y) -z - (y + z) == x - (y + x) -z - (z + y) == x - (x + y) -z - (z + y) == x - (y + x) -x + (0 - y) == x - y -(0 - y) + x == x - y -x - (x + 1) == 0 - 1 -x - (1 + x) == 0 - 1 -y - (y + 1) == x - (x + 1) -y - (y + 1) == x - (1 + x) -y - (1 + y) == x - (1 + x) - -direct candidates: - -foo x = x - -foo x = 0 - -foo x = 1 - -foo x = x + x - -foo x = x + 1 - -foo x = 1 + 1 - -foo x = x - 1 - -foo x = 0 - x - -foo x = 0 - 1 - -foo x = 1 - x - -foo x = x + (x + x) - -foo x = x + (x + 1) - -foo x = x + (1 + 1) - -foo x = x + (x - 1) - -foo x = x + (0 - 1) - -foo x = 1 + (x + x) - -foo x = 1 + (x + 1) - -foo x = 1 + (1 + 1) - -foo x = 1 + (0 - x) - -foo x = 1 + (1 - x) - -foo x = x - (x + x) - -foo x = x - (x + 1) - -foo x = x - (1 + 1) - -foo x = 0 - (x + x) - -foo x = 0 - (x + 1) - -foo x = 0 - (1 + 1) - -foo x = 1 - (x + x) - -foo x = 1 - (x + 1) - -foo x = 1 - (1 + 1) - - -pattern candidates: - -foo x = x - -foo x = 0 - -foo x = 1 - -foo 0 = 0 -foo x = 1 - -foo 0 = 1 -foo x = x - -foo 0 = 1 -foo x = 0 - -foo x = x + x - -foo x = x + 1 - -foo x = x - 1 - -foo x = 0 - x - -foo x = 1 - x - -foo 1 = 0 -foo x = x - -foo 1 = 0 -foo x = 1 - -foo 1 = 1 -foo x = 0 - -foo 0 = 0 -foo x = x + 1 - -foo 0 = 0 -foo x = x - 1 - -foo 0 = 0 -foo x = 1 - x - -foo 0 = 1 -foo x = x + x - -foo 0 = 1 -foo x = x - 1 - -foo 0 = 1 -foo x = 0 - x - -foo 0 = 0 -foo 1 = 0 -foo x = 1 - -foo 0 = 1 -foo 1 = 0 -foo x = x - -foo 0 = 1 -foo 1 = 1 -foo x = 0 - -foo x = x + (x + x) - -foo x = x + (x + 1) - -foo x = x + (x - 1) - -foo x = 1 + (x + x) - -foo x = 1 + (x + 1) - -foo x = 1 + (0 - x) - -foo x = 1 + (1 - x) - -foo x = x - (x + x) - -foo x = x - (x + 1) - -foo x = 0 - (x + x) - -foo x = 0 - (x + 1) - -foo x = 1 - (x + x) - -foo x = 1 - (x + 1) - -foo 1 = 0 -foo x = x + x - -foo 1 = 0 -foo x = x + 1 - -foo 1 = 0 -foo x = 0 - x - -foo 1 = 1 -foo x = x + x - -foo 1 = 1 -foo x = x + 1 - -foo 1 = 1 -foo x = x - 1 - -foo 1 = 1 -foo x = 0 - x - -foo 1 = 1 -foo x = 1 - x - -foo 0 = 0 -foo x = x + (x + 1) - -foo 0 = 0 -foo x = x + (x - 1) - -foo 0 = 0 -foo x = 1 + (x + x) - -foo 0 = 0 -foo x = 1 + (x + 1) - -foo 0 = 0 -foo x = 1 + (0 - x) - -foo 0 = 0 -foo x = 1 + (1 - x) - -foo 0 = 0 -foo x = x - (x + 1) - -foo 0 = 0 -foo x = 0 - (x + 1) - -foo 0 = 0 -foo x = 1 - (x + x) - -foo 0 = 1 -foo x = x + (x + x) - -foo 0 = 1 -foo x = x + (x - 1) - -foo 0 = 1 -foo x = 1 + (x + 1) - -foo 0 = 1 -foo x = 1 + (1 - x) - -foo 0 = 1 -foo x = x - (x + x) - -foo 0 = 1 -foo x = x - (x + 1) - -foo 0 = 1 -foo x = 0 - (x + x) - -foo 0 = 1 -foo x = 0 - (x + 1) - -foo 0 = 1 -foo x = 1 - (x + 1) - -foo 0 = 0 -foo 1 = 0 -foo x = x + 1 - -foo 0 = 0 -foo 1 = 1 -foo x = x + 1 - -foo 0 = 0 -foo 1 = 1 -foo x = x - 1 - -foo 0 = 0 -foo 1 = 1 -foo x = 1 - x - -foo 0 = 1 -foo 1 = 0 -foo x = x + x - -foo 0 = 1 -foo 1 = 0 -foo x = 0 - x - -foo 0 = 1 -foo 1 = 1 -foo x = x + x - -foo 0 = 1 -foo 1 = 1 -foo x = x - 1 - -foo 0 = 1 -foo 1 = 1 -foo x = 0 - x - - -Candidates for: ? :: Int -> Int -> Int - pruning with 10/23 rules - [3,3,6,9,21,39,87,180,390] direct candidates, 0 duplicates - [3,8,22,50,116,302,765,1864,4439] pattern candidates, 0 duplicates - -rules: -x * y == x + y -x * y == y + x -x + 0 == x -0 + x == x -dec (x + y) == x + dec y -dec (x + y) == y + dec x -dec (x + y) == dec x + y -dec (x + y) == dec y + x -(x + y) + z == x + (y + z) -(x + y) + z == y + (x + z) -equations: -y + x == x + y -y + dec x == x + dec y -dec x + y == x + dec y -dec y + x == dec x + y -x + dec 0 == dec x -dec 0 + x == dec x -y + (x + z) == x + (y + z) -z + (x + y) == x + (y + z) -z + (y + x) == x + (y + z) -y + dec (dec x) == x + dec (dec y) -dec (dec x) + y == x + dec (dec y) -x + dec (dec 0) == dec (dec x) -dec (dec 0) + x == dec (dec x) - -direct candidates: - -x ? y = x - -x ? y = y - -x ? y = 0 - -x ? y = dec x - -x ? y = dec y - -x ? y = dec 0 - -x ? y = x + x - -x ? y = x + y - -x ? y = y + y - -x ? y = dec (dec x) - -x ? y = dec (dec y) - -x ? y = dec (dec 0) - -x ? y = dec (dec (dec x)) - -x ? y = dec (dec (dec y)) - -x ? y = dec (dec (dec 0)) - -x ? y = x + dec x - -x ? y = x + dec y - -x ? y = x + dec 0 - -x ? y = y + dec x - -x ? y = y + dec y - -x ? y = y + dec 0 - -x ? y = dec (dec (dec (dec x))) - -x ? y = dec (dec (dec (dec y))) - -x ? y = dec (dec (dec (dec 0))) - -x ? y = x + (x + x) - -x ? y = x + (x + y) - -x ? y = x + (y + y) - -x ? y = x + dec (dec x) - -x ? y = x + dec (dec y) - -x ? y = x + dec (dec 0) - -x ? y = y + (x + x) - -x ? y = y + (x + y) - -x ? y = y + (y + y) - -x ? y = y + dec (dec x) - -x ? y = y + dec (dec y) - -x ? y = y + dec (dec 0) - -x ? y = dec x + dec x - -x ? y = dec x + dec y - -x ? y = dec x + dec 0 - -x ? y = dec y + dec y - -x ? y = dec y + dec 0 - -x ? y = dec 0 + dec 0 - -x ? y = dec (dec (dec (dec (dec x)))) - -x ? y = dec (dec (dec (dec (dec y)))) - -x ? y = dec (dec (dec (dec (dec 0)))) - -x ? y = x + dec (dec (dec x)) - -x ? y = x + dec (dec (dec y)) - -x ? y = x + dec (dec (dec 0)) - -x ? y = x + (x + dec x) - -x ? y = x + (x + dec y) - -x ? y = x + (x + dec 0) - -x ? y = x + (y + dec x) - -x ? y = x + (y + dec y) - -x ? y = x + (y + dec 0) - -x ? y = y + dec (dec (dec x)) - -x ? y = y + dec (dec (dec y)) - -x ? y = y + dec (dec (dec 0)) - -x ? y = y + (x + dec x) - -x ? y = y + (x + dec y) - -x ? y = y + (x + dec 0) - -x ? y = y + (y + dec x) - -x ? y = y + (y + dec y) - -x ? y = y + (y + dec 0) - -x ? y = dec x + (x + x) - -x ? y = dec x + (x + y) - -x ? y = dec x + (y + y) - -x ? y = dec x + dec (dec x) - -x ? y = dec x + dec (dec y) - -x ? y = dec x + dec (dec 0) - -x ? y = dec y + (x + x) - -x ? y = dec y + (x + y) - -x ? y = dec y + (y + y) - -x ? y = dec y + dec (dec x) - -x ? y = dec y + dec (dec y) - -x ? y = dec y + dec (dec 0) - -x ? y = dec 0 + (x + x) - -x ? y = dec 0 + (x + y) - -x ? y = dec 0 + (y + y) - -x ? y = dec 0 + dec (dec x) - -x ? y = dec 0 + dec (dec y) - -x ? y = dec 0 + dec (dec 0) - - -pattern candidates: - -x ? y = x - -x ? y = y - -x ? y = 0 - -x ? y = dec x - -x ? y = dec y - -x ? 0 = x -x ? y = y - -x ? 0 = x -x ? y = 0 - -x ? 0 = 0 -x ? y = x - -0 ? x = x -x ? y = x - -0 ? x = x -x ? y = 0 - -0 ? x = 0 -x ? y = y - -x ? y = x + x - -x ? y = x + y - -x ? y = y + y - -x ? y = dec (dec x) - -x ? y = dec (dec y) - -x ? 0 = x -x ? y = dec x - -x ? 0 = x -x ? y = dec y - -x ? 0 = 0 -x ? y = dec x - -x ? 0 = 0 -x ? y = dec y - -x ? 0 = dec x -x ? y = x - -x ? 0 = dec x -x ? y = y - -x ? 0 = dec x -x ? y = 0 - -0 ? x = x -x ? y = dec x - -0 ? x = x -x ? y = dec y - -0 ? x = 0 -x ? y = dec x - -0 ? x = 0 -x ? y = dec y - -0 ? x = dec x -x ? y = x - -0 ? x = dec x -x ? y = y - -0 ? x = dec x -x ? y = 0 - -0 ? x = x -x ? 0 = x -x ? y = 0 - -0 ? x = x -x ? 0 = 0 -x ? y = x - -0 ? x = 0 -x ? 0 = x -x ? y = y - -x ? y = dec (dec (dec x)) - -x ? y = dec (dec (dec y)) - -x ? y = x + dec x - -x ? y = x + dec y - -x ? y = y + dec x - -x ? y = y + dec y - -x ? 0 = x -x ? y = x + x - -x ? 0 = x -x ? y = y + y - -x ? 0 = x -x ? y = dec (dec x) - -x ? 0 = x -x ? y = dec (dec y) - -x ? 0 = 0 -x ? y = x + x - -x ? 0 = 0 -x ? y = x + y - -x ? 0 = 0 -x ? y = dec (dec x) - -x ? 0 = 0 -x ? y = dec (dec y) - -x ? 0 = dec x -x ? y = dec y - -x ? 0 = x + x -x ? y = x - -x ? 0 = x + x -x ? y = y - -x ? 0 = x + x -x ? y = 0 - -x ? 0 = dec (dec x) -x ? y = x - -x ? 0 = dec (dec x) -x ? y = y - -x ? 0 = dec (dec x) -x ? y = 0 - -0 ? x = x -x ? y = x + x - -0 ? x = x -x ? y = y + y - -0 ? x = x -x ? y = dec (dec x) - -0 ? x = x -x ? y = dec (dec y) - -0 ? x = 0 -x ? y = x + y - -0 ? x = 0 -x ? y = y + y - -0 ? x = 0 -x ? y = dec (dec x) - -0 ? x = 0 -x ? y = dec (dec y) - -0 ? x = dec x -x ? y = dec x - -0 ? x = x + x -x ? y = x - -0 ? x = x + x -x ? y = y - -0 ? x = x + x -x ? y = 0 - -0 ? x = dec (dec x) -x ? y = x - -0 ? x = dec (dec x) -x ? y = y - -0 ? x = dec (dec x) -x ? y = 0 - -0 ? x = x -x ? 0 = x -x ? y = dec x - -0 ? x = x -x ? 0 = x -x ? y = dec y - -0 ? x = x -x ? 0 = 0 -x ? y = dec x - -0 ? x = x -x ? 0 = 0 -x ? y = dec y - -0 ? x = x -x ? 0 = dec x -x ? y = x - -0 ? x = x -x ? 0 = dec x -x ? y = 0 - -0 ? x = 0 -x ? 0 = x -x ? y = dec x - -0 ? x = 0 -x ? 0 = x -x ? y = dec y - -0 ? x = 0 -x ? 0 = 0 -x ? y = dec x - -0 ? x = 0 -x ? 0 = 0 -x ? y = dec y - -0 ? x = 0 -x ? 0 = dec x -x ? y = y - -0 ? x = dec x -x ? 0 = x -x ? y = y - -0 ? x = dec x -x ? 0 = x -x ? y = 0 - -0 ? x = dec x -x ? 0 = 0 -x ? y = x - -x ? 0 = x -x ? y = x ? dec y - -x ? 0 = x -x ? y = y ? dec x - -x ? 0 = x -x ? y = y ? dec y - -x ? 0 = x -x ? y = 0 ? dec y - -x ? 0 = x -x ? y = dec x ? x - -x ? 0 = x -x ? y = dec x ? y - -x ? 0 = x -x ? y = dec y ? x - -0 ? x = x -x ? y = x ? dec y - -0 ? x = x -x ? y = y ? dec x - -0 ? x = x -x ? y = y ? dec y - -0 ? x = x -x ? y = dec x ? x - -0 ? x = x -x ? y = dec x ? y - -0 ? x = x -x ? y = dec x ? 0 - -0 ? x = x -x ? y = dec y ? x - -x ? y = dec (dec (dec (dec x))) - -x ? y = dec (dec (dec (dec y))) - -x ? y = x + (x + x) - -x ? y = x + (x + y) - -x ? y = x + (y + y) - -x ? y = x + dec (dec x) - -x ? y = x + dec (dec y) - -x ? y = y + (x + x) - -x ? y = y + (x + y) - -x ? y = y + (y + y) - -x ? y = y + dec (dec x) - -x ? y = y + dec (dec y) - -x ? y = dec x + dec x - -x ? y = dec x + dec y - -x ? y = dec y + dec y - -x ? 0 = x -x ? y = dec (dec (dec x)) - -x ? 0 = x -x ? y = dec (dec (dec y)) - -x ? 0 = x -x ? y = x + dec x - -x ? 0 = x -x ? y = x + dec y - -x ? 0 = x -x ? y = y + dec x - -x ? 0 = x -x ? y = y + dec y - -x ? 0 = 0 -x ? y = dec (dec (dec x)) - -x ? 0 = 0 -x ? y = dec (dec (dec y)) - -x ? 0 = 0 -x ? y = x + dec x - -x ? 0 = 0 -x ? y = x + dec y - -x ? 0 = 0 -x ? y = y + dec x - -x ? 0 = 0 -x ? y = y + dec y - -x ? 0 = dec x -x ? y = x + x - -x ? 0 = dec x -x ? y = x + y - -x ? 0 = dec x -x ? y = y + y - -x ? 0 = dec x -x ? y = dec (dec x) - -x ? 0 = dec x -x ? y = dec (dec y) - -x ? 0 = x + x -x ? y = dec x - -x ? 0 = x + x -x ? y = dec y - -x ? 0 = dec (dec x) -x ? y = dec x - -x ? 0 = dec (dec x) -x ? y = dec y - -x ? 0 = dec (dec (dec x)) -x ? y = x - -x ? 0 = dec (dec (dec x)) -x ? y = y - -x ? 0 = dec (dec (dec x)) -x ? y = 0 - -x ? 0 = x + dec x -x ? y = x - -x ? 0 = x + dec x -x ? y = y - -x ? 0 = x + dec x -x ? y = 0 - -0 ? x = x -x ? y = dec (dec (dec x)) - -0 ? x = x -x ? y = dec (dec (dec y)) - -0 ? x = x -x ? y = x + dec x - -0 ? x = x -x ? y = x + dec y - -0 ? x = x -x ? y = y + dec x - -0 ? x = x -x ? y = y + dec y - -0 ? x = 0 -x ? y = dec (dec (dec x)) - -0 ? x = 0 -x ? y = dec (dec (dec y)) - -0 ? x = 0 -x ? y = x + dec x - -0 ? x = 0 -x ? y = x + dec y - -0 ? x = 0 -x ? y = y + dec x - -0 ? x = 0 -x ? y = y + dec y - -0 ? x = dec x -x ? y = x + x - -0 ? x = dec x -x ? y = x + y - -0 ? x = dec x -x ? y = y + y - -0 ? x = dec x -x ? y = dec (dec x) - -0 ? x = dec x -x ? y = dec (dec y) - -0 ? x = x + x -x ? y = dec x - -0 ? x = x + x -x ? y = dec y - -0 ? x = dec (dec x) -x ? y = dec x - -0 ? x = dec (dec x) -x ? y = dec y - -0 ? x = dec (dec (dec x)) -x ? y = x - -0 ? x = dec (dec (dec x)) -x ? y = y - -0 ? x = dec (dec (dec x)) -x ? y = 0 - -0 ? x = x + dec x -x ? y = x - -0 ? x = x + dec x -x ? y = y - -0 ? x = x + dec x -x ? y = 0 - -0 ? x = x -x ? 0 = x -x ? y = x + x - -0 ? x = x -x ? 0 = x -x ? y = y + y - -0 ? x = x -x ? 0 = x -x ? y = dec (dec x) - -0 ? x = x -x ? 0 = x -x ? y = dec (dec y) - -0 ? x = x -x ? 0 = 0 -x ? y = x + x - -0 ? x = x -x ? 0 = 0 -x ? y = dec (dec x) - -0 ? x = x -x ? 0 = 0 -x ? y = dec (dec y) - -0 ? x = x -x ? 0 = dec x -x ? y = dec y - -0 ? x = x -x ? 0 = x + x -x ? y = x - -0 ? x = x -x ? 0 = x + x -x ? y = 0 - -0 ? x = x -x ? 0 = dec (dec x) -x ? y = x - -0 ? x = x -x ? 0 = dec (dec x) -x ? y = 0 - -0 ? x = 0 -x ? 0 = x -x ? y = y + y - -0 ? x = 0 -x ? 0 = x -x ? y = dec (dec x) - -0 ? x = 0 -x ? 0 = x -x ? y = dec (dec y) - -0 ? x = 0 -x ? 0 = 0 -x ? y = x + y - -0 ? x = 0 -x ? 0 = 0 -x ? y = dec (dec x) - -0 ? x = 0 -x ? 0 = 0 -x ? y = dec (dec y) - -0 ? x = 0 -x ? 0 = dec x -x ? y = dec y - -0 ? x = 0 -x ? 0 = x + x -x ? y = y - -0 ? x = 0 -x ? 0 = dec (dec x) -x ? y = y - -0 ? x = dec x -x ? 0 = x -x ? y = dec x - -0 ? x = dec x -x ? 0 = 0 -x ? y = dec x - -0 ? x = dec x -x ? 0 = dec x -x ? y = x - -0 ? x = dec x -x ? 0 = dec x -x ? y = y - -0 ? x = dec x -x ? 0 = dec x -x ? y = 0 - -0 ? x = x + x -x ? 0 = x -x ? y = y - -0 ? x = x + x -x ? 0 = x -x ? y = 0 - -0 ? x = x + x -x ? 0 = 0 -x ? y = x - -0 ? x = dec (dec x) -x ? 0 = x -x ? y = y - -0 ? x = dec (dec x) -x ? 0 = x -x ? y = 0 - -0 ? x = dec (dec x) -x ? 0 = 0 -x ? y = x - -0 ? 0 = 0 -0 ? x = dec x -x ? y = dec x - -x ? 0 = x -x ? y = x ? dec (dec y) - -x ? 0 = x -x ? y = y ? dec (dec x) - -x ? 0 = x -x ? y = y ? dec (dec y) - -x ? 0 = x -x ? y = 0 ? dec (dec y) - -x ? 0 = x -x ? y = dec x ? dec x - -x ? 0 = x -x ? y = dec x ? dec y - -x ? 0 = x -x ? y = dec y ? dec x - -x ? 0 = x -x ? y = dec y ? dec y - -x ? 0 = x -x ? y = dec (dec x) ? x - -x ? 0 = x -x ? y = dec (dec x) ? y - -x ? 0 = x -x ? y = dec (dec y) ? x - -0 ? x = x -x ? y = x ? dec (dec y) - -0 ? x = x -x ? y = y ? dec (dec x) - -0 ? x = x -x ? y = y ? dec (dec y) - -0 ? x = x -x ? y = dec x ? dec x - -0 ? x = x -x ? y = dec x ? dec y - -0 ? x = x -x ? y = dec y ? dec x - -0 ? x = x -x ? y = dec y ? dec y - -0 ? x = x -x ? y = dec (dec x) ? x - -0 ? x = x -x ? y = dec (dec x) ? y - -0 ? x = x -x ? y = dec (dec x) ? 0 - -0 ? x = x -x ? y = dec (dec y) ? x - -x ? 0 = x -x ? y = dec (x ? dec y) - -x ? 0 = x -x ? y = dec (y ? dec x) - -x ? 0 = x -x ? y = dec (y ? dec y) - -x ? 0 = x -x ? y = dec (0 ? dec y) - -x ? 0 = x -x ? y = dec (dec x ? x) - -x ? 0 = x -x ? y = dec (dec x ? y) - -x ? 0 = x -x ? y = dec (dec y ? x) - -x ? 0 = 0 -x ? y = dec (x ? dec y) - -x ? 0 = 0 -x ? y = dec (y ? dec x) - -x ? 0 = 0 -x ? y = dec (y ? dec y) - -x ? 0 = 0 -x ? y = dec (0 ? dec y) - -x ? 0 = 0 -x ? y = dec (dec x ? x) - -x ? 0 = 0 -x ? y = dec (dec x ? y) - -x ? 0 = 0 -x ? y = dec (dec y ? x) - -x ? 0 = dec x -x ? y = x ? dec y - -x ? 0 = dec x -x ? y = y ? dec x - -x ? 0 = dec x -x ? y = y ? dec y - -x ? 0 = dec x -x ? y = 0 ? dec y - -x ? 0 = dec x -x ? y = dec x ? x - -x ? 0 = dec x -x ? y = dec x ? y - -x ? 0 = dec x -x ? y = dec y ? x - -0 ? x = x -x ? y = dec (x ? dec y) - -0 ? x = x -x ? y = dec (y ? dec x) - -0 ? x = x -x ? y = dec (y ? dec y) - -0 ? x = x -x ? y = dec (dec x ? x) - -0 ? x = x -x ? y = dec (dec x ? y) - -0 ? x = x -x ? y = dec (dec x ? 0) - -0 ? x = x -x ? y = dec (dec y ? x) - -0 ? x = 0 -x ? y = dec (x ? dec y) - -0 ? x = 0 -x ? y = dec (y ? dec x) - -0 ? x = 0 -x ? y = dec (y ? dec y) - -0 ? x = 0 -x ? y = dec (dec x ? x) - -0 ? x = 0 -x ? y = dec (dec x ? y) - -0 ? x = 0 -x ? y = dec (dec x ? 0) - -0 ? x = 0 -x ? y = dec (dec y ? x) - -0 ? x = dec x -x ? y = x ? dec y - -0 ? x = dec x -x ? y = y ? dec x - -0 ? x = dec x -x ? y = y ? dec y - -0 ? x = dec x -x ? y = dec x ? x - -0 ? x = dec x -x ? y = dec x ? y - -0 ? x = dec x -x ? y = dec x ? 0 - -0 ? x = dec x -x ? y = dec y ? x - -0 ? x = x -x ? 0 = x -x ? y = x ? dec y - -0 ? x = x -x ? 0 = x -x ? y = y ? dec x - -0 ? x = x -x ? 0 = x -x ? y = y ? dec y - -0 ? x = x -x ? 0 = x -x ? y = dec x ? x - -0 ? x = x -x ? 0 = x -x ? y = dec x ? y - -0 ? x = x -x ? 0 = x -x ? y = dec y ? x - -0 ? x = x -x ? 0 = 0 -x ? y = x ? dec y - -0 ? x = x -x ? 0 = 0 -x ? y = y ? dec x - -0 ? x = x -x ? 0 = 0 -x ? y = y ? dec y - -0 ? x = x -x ? 0 = 0 -x ? y = dec x ? x - -0 ? x = x -x ? 0 = 0 -x ? y = dec x ? y - -0 ? x = x -x ? 0 = 0 -x ? y = dec y ? x - -0 ? x = 0 -x ? 0 = x -x ? y = x ? dec y - -0 ? x = 0 -x ? 0 = x -x ? y = y ? dec x - -0 ? x = 0 -x ? 0 = x -x ? y = y ? dec y - -0 ? x = 0 -x ? 0 = x -x ? y = dec x ? x - -0 ? x = 0 -x ? 0 = x -x ? y = dec x ? y - -0 ? x = 0 -x ? 0 = x -x ? y = dec y ? x - -x ? y = dec (dec (dec (dec (dec x)))) - -x ? y = dec (dec (dec (dec (dec y)))) - -x ? y = x + dec (dec (dec x)) - -x ? y = x + dec (dec (dec y)) - -x ? y = x + (x + dec x) - -x ? y = x + (x + dec y) - -x ? y = x + (y + dec x) - -x ? y = x + (y + dec y) - -x ? y = y + dec (dec (dec x)) - -x ? y = y + dec (dec (dec y)) - -x ? y = y + (x + dec x) - -x ? y = y + (x + dec y) - -x ? y = y + (y + dec x) - -x ? y = y + (y + dec y) - -x ? y = dec x + (x + x) - -x ? y = dec x + (x + y) - -x ? y = dec x + (y + y) - -x ? y = dec x + dec (dec x) - -x ? y = dec x + dec (dec y) - -x ? y = dec y + (x + x) - -x ? y = dec y + (x + y) - -x ? y = dec y + (y + y) - -x ? y = dec y + dec (dec x) - -x ? y = dec y + dec (dec y) - -x ? 0 = x -x ? y = dec (dec (dec (dec x))) - -x ? 0 = x -x ? y = dec (dec (dec (dec y))) - -x ? 0 = x -x ? y = x + (x + x) - -x ? 0 = x -x ? y = x + (x + y) - -x ? 0 = x -x ? y = x + dec (dec x) - -x ? 0 = x -x ? y = x + dec (dec y) - -x ? 0 = x -x ? y = y + (x + x) - -x ? 0 = x -x ? y = y + (y + y) - -x ? 0 = x -x ? y = y + dec (dec x) - -x ? 0 = x -x ? y = y + dec (dec y) - -x ? 0 = x -x ? y = dec x + dec x - -x ? 0 = x -x ? y = dec x + dec y - -x ? 0 = x -x ? y = dec y + dec y - -x ? 0 = 0 -x ? y = dec (dec (dec (dec x))) - -x ? 0 = 0 -x ? y = dec (dec (dec (dec y))) - -x ? 0 = 0 -x ? y = x + (x + x) - -x ? 0 = 0 -x ? y = x + (x + y) - -x ? 0 = 0 -x ? y = x + (y + y) - -x ? 0 = 0 -x ? y = x + dec (dec x) - -x ? 0 = 0 -x ? y = x + dec (dec y) - -x ? 0 = 0 -x ? y = y + (x + x) - -x ? 0 = 0 -x ? y = y + (x + y) - -x ? 0 = 0 -x ? y = y + dec (dec x) - -x ? 0 = 0 -x ? y = y + dec (dec y) - -x ? 0 = 0 -x ? y = dec x + dec x - -x ? 0 = 0 -x ? y = dec x + dec y - -x ? 0 = 0 -x ? y = dec y + dec y - -x ? 0 = dec x -x ? y = dec (dec (dec x)) - -x ? 0 = dec x -x ? y = dec (dec (dec y)) - -x ? 0 = dec x -x ? y = x + dec x - -x ? 0 = dec x -x ? y = x + dec y - -x ? 0 = dec x -x ? y = y + dec y - -x ? 0 = x + x -x ? y = x + y - -x ? 0 = x + x -x ? y = y + y - -x ? 0 = x + x -x ? y = dec (dec x) - -x ? 0 = x + x -x ? y = dec (dec y) - -x ? 0 = dec (dec x) -x ? y = x + x - -x ? 0 = dec (dec x) -x ? y = x + y - -x ? 0 = dec (dec x) -x ? y = y + y - -x ? 0 = dec (dec x) -x ? y = dec (dec y) - -x ? 0 = dec (dec (dec x)) -x ? y = dec x - -x ? 0 = dec (dec (dec x)) -x ? y = dec y - -x ? 0 = x + dec x -x ? y = dec x - -x ? 0 = x + dec x -x ? y = dec y - -x ? 0 = dec (dec (dec (dec x))) -x ? y = x - -x ? 0 = dec (dec (dec (dec x))) -x ? y = y - -x ? 0 = dec (dec (dec (dec x))) -x ? y = 0 - -x ? 0 = x + (x + x) -x ? y = x - -x ? 0 = x + (x + x) -x ? y = y - -x ? 0 = x + (x + x) -x ? y = 0 - -x ? 0 = x + dec (dec x) -x ? y = x - -x ? 0 = x + dec (dec x) -x ? y = y - -x ? 0 = x + dec (dec x) -x ? y = 0 - -x ? 0 = dec x + dec x -x ? y = x - -x ? 0 = dec x + dec x -x ? y = y - -x ? 0 = dec x + dec x -x ? y = 0 - -0 ? x = x -x ? y = dec (dec (dec (dec x))) - -0 ? x = x -x ? y = dec (dec (dec (dec y))) - -0 ? x = x -x ? y = x + (x + x) - -0 ? x = x -x ? y = x + (y + y) - -0 ? x = x -x ? y = x + dec (dec x) - -0 ? x = x -x ? y = x + dec (dec y) - -0 ? x = x -x ? y = y + (x + y) - -0 ? x = x -x ? y = y + (y + y) - -0 ? x = x -x ? y = y + dec (dec x) - -0 ? x = x -x ? y = y + dec (dec y) - -0 ? x = x -x ? y = dec x + dec x - -0 ? x = x -x ? y = dec x + dec y - -0 ? x = x -x ? y = dec y + dec y - -0 ? x = 0 -x ? y = dec (dec (dec (dec x))) - -0 ? x = 0 -x ? y = dec (dec (dec (dec y))) - -0 ? x = 0 -x ? y = x + (x + y) - -0 ? x = 0 -x ? y = x + (y + y) - -0 ? x = 0 -x ? y = x + dec (dec x) - -0 ? x = 0 -x ? y = x + dec (dec y) - -0 ? x = 0 -x ? y = y + (x + x) - -0 ? x = 0 -x ? y = y + (x + y) - -0 ? x = 0 -x ? y = y + (y + y) - -0 ? x = 0 -x ? y = y + dec (dec x) - -0 ? x = 0 -x ? y = y + dec (dec y) - -0 ? x = 0 -x ? y = dec x + dec x - -0 ? x = 0 -x ? y = dec x + dec y - -0 ? x = 0 -x ? y = dec y + dec y - -0 ? x = dec x -x ? y = dec (dec (dec x)) - -0 ? x = dec x -x ? y = dec (dec (dec y)) - -0 ? x = dec x -x ? y = x + dec x - -0 ? x = dec x -x ? y = y + dec x - -0 ? x = dec x -x ? y = y + dec y - -0 ? x = x + x -x ? y = x + x - -0 ? x = x + x -x ? y = x + y - -0 ? x = x + x -x ? y = dec (dec x) - -0 ? x = x + x -x ? y = dec (dec y) - -0 ? x = dec (dec x) -x ? y = x + x - -0 ? x = dec (dec x) -x ? y = x + y - -0 ? x = dec (dec x) -x ? y = y + y - -0 ? x = dec (dec x) -x ? y = dec (dec x) - -0 ? x = dec (dec (dec x)) -x ? y = dec x - -0 ? x = dec (dec (dec x)) -x ? y = dec y - -0 ? x = x + dec x -x ? y = dec x - -0 ? x = x + dec x -x ? y = dec y - -0 ? x = dec (dec (dec (dec x))) -x ? y = x - -0 ? x = dec (dec (dec (dec x))) -x ? y = y - -0 ? x = dec (dec (dec (dec x))) -x ? y = 0 - -0 ? x = x + (x + x) -x ? y = x - -0 ? x = x + (x + x) -x ? y = y - -0 ? x = x + (x + x) -x ? y = 0 - -0 ? x = x + dec (dec x) -x ? y = x - -0 ? x = x + dec (dec x) -x ? y = y - -0 ? x = x + dec (dec x) -x ? y = 0 - -0 ? x = dec x + dec x -x ? y = x - -0 ? x = dec x + dec x -x ? y = y - -0 ? x = dec x + dec x -x ? y = 0 - -0 ? x = x -x ? 0 = x -x ? y = dec (dec (dec x)) - -0 ? x = x -x ? 0 = x -x ? y = dec (dec (dec y)) - -0 ? x = x -x ? 0 = x -x ? y = x + dec x - -0 ? x = x -x ? 0 = x -x ? y = x + dec y - -0 ? x = x -x ? 0 = x -x ? y = y + dec x - -0 ? x = x -x ? 0 = x -x ? y = y + dec y - -0 ? x = x -x ? 0 = 0 -x ? y = dec (dec (dec x)) - -0 ? x = x -x ? 0 = 0 -x ? y = dec (dec (dec y)) - -0 ? x = x -x ? 0 = 0 -x ? y = x + dec x - -0 ? x = x -x ? 0 = 0 -x ? y = x + dec y - -0 ? x = x -x ? 0 = 0 -x ? y = y + dec x - -0 ? x = x -x ? 0 = 0 -x ? y = y + dec y - -0 ? x = x -x ? 0 = dec x -x ? y = x + x - -0 ? x = x -x ? 0 = dec x -x ? y = y + y - -0 ? x = x -x ? 0 = dec x -x ? y = dec (dec x) - -0 ? x = x -x ? 0 = dec x -x ? y = dec (dec y) - -0 ? x = x -x ? 0 = x + x -x ? y = dec x - -0 ? x = x -x ? 0 = x + x -x ? y = dec y - -0 ? x = x -x ? 0 = dec (dec x) -x ? y = dec x - -0 ? x = x -x ? 0 = dec (dec x) -x ? y = dec y - -0 ? x = x -x ? 0 = dec (dec (dec x)) -x ? y = x - -0 ? x = x -x ? 0 = dec (dec (dec x)) -x ? y = 0 - -0 ? x = x -x ? 0 = x + dec x -x ? y = x - -0 ? x = x -x ? 0 = x + dec x -x ? y = 0 - -0 ? x = 0 -x ? 0 = x -x ? y = dec (dec (dec x)) - -0 ? x = 0 -x ? 0 = x -x ? y = dec (dec (dec y)) - -0 ? x = 0 -x ? 0 = x -x ? y = x + dec x - -0 ? x = 0 -x ? 0 = x -x ? y = x + dec y - -0 ? x = 0 -x ? 0 = x -x ? y = y + dec x - -0 ? x = 0 -x ? 0 = x -x ? y = y + dec y - -0 ? x = 0 -x ? 0 = 0 -x ? y = dec (dec (dec x)) - -0 ? x = 0 -x ? 0 = 0 -x ? y = dec (dec (dec y)) - -0 ? x = 0 -x ? 0 = 0 -x ? y = x + dec x - -0 ? x = 0 -x ? 0 = 0 -x ? y = x + dec y - -0 ? x = 0 -x ? 0 = 0 -x ? y = y + dec x - -0 ? x = 0 -x ? 0 = 0 -x ? y = y + dec y - -0 ? x = 0 -x ? 0 = dec x -x ? y = x + y - -0 ? x = 0 -x ? 0 = dec x -x ? y = y + y - -0 ? x = 0 -x ? 0 = dec x -x ? y = dec (dec x) - -0 ? x = 0 -x ? 0 = dec x -x ? y = dec (dec y) - -0 ? x = 0 -x ? 0 = x + x -x ? y = dec x - -0 ? x = 0 -x ? 0 = x + x -x ? y = dec y - -0 ? x = 0 -x ? 0 = dec (dec x) -x ? y = dec x - -0 ? x = 0 -x ? 0 = dec (dec x) -x ? y = dec y - -0 ? x = 0 -x ? 0 = dec (dec (dec x)) -x ? y = y - -0 ? x = 0 -x ? 0 = x + dec x -x ? y = y - -0 ? x = dec x -x ? 0 = x -x ? y = x + x - -0 ? x = dec x -x ? 0 = x -x ? y = y + y - -0 ? x = dec x -x ? 0 = x -x ? y = dec (dec x) - -0 ? x = dec x -x ? 0 = x -x ? y = dec (dec y) - -0 ? x = dec x -x ? 0 = 0 -x ? y = x + x - -0 ? x = dec x -x ? 0 = 0 -x ? y = x + y - -0 ? x = dec x -x ? 0 = 0 -x ? y = dec (dec x) - -0 ? x = dec x -x ? 0 = 0 -x ? y = dec (dec y) - -0 ? x = dec x -x ? 0 = x + x -x ? y = x - -0 ? x = dec x -x ? 0 = x + x -x ? y = y - -0 ? x = dec x -x ? 0 = x + x -x ? y = 0 - -0 ? x = dec x -x ? 0 = dec (dec x) -x ? y = x - -0 ? x = dec x -x ? 0 = dec (dec x) -x ? y = y - -0 ? x = dec x -x ? 0 = dec (dec x) -x ? y = 0 - -0 ? x = x + x -x ? 0 = x -x ? y = dec x - -0 ? x = x + x -x ? 0 = x -x ? y = dec y - -0 ? x = x + x -x ? 0 = 0 -x ? y = dec x - -0 ? x = x + x -x ? 0 = 0 -x ? y = dec y - -0 ? x = x + x -x ? 0 = dec x -x ? y = x - -0 ? x = x + x -x ? 0 = dec x -x ? y = y - -0 ? x = x + x -x ? 0 = dec x -x ? y = 0 - -0 ? x = dec (dec x) -x ? 0 = x -x ? y = dec x - -0 ? x = dec (dec x) -x ? 0 = x -x ? y = dec y - -0 ? x = dec (dec x) -x ? 0 = 0 -x ? y = dec x - -0 ? x = dec (dec x) -x ? 0 = 0 -x ? y = dec y - -0 ? x = dec (dec x) -x ? 0 = dec x -x ? y = x - -0 ? x = dec (dec x) -x ? 0 = dec x -x ? y = y - -0 ? x = dec (dec x) -x ? 0 = dec x -x ? y = 0 - -0 ? x = dec (dec (dec x)) -x ? 0 = x -x ? y = y - -0 ? x = dec (dec (dec x)) -x ? 0 = x -x ? y = 0 - -0 ? x = dec (dec (dec x)) -x ? 0 = 0 -x ? y = x - -0 ? x = x + dec x -x ? 0 = x -x ? y = y - -0 ? x = x + dec x -x ? 0 = x -x ? y = 0 - -0 ? x = x + dec x -x ? 0 = 0 -x ? y = x - -0 ? 0 = 0 -0 ? x = dec x -x ? y = dec (dec x) - -0 ? 0 = 0 -0 ? x = dec x -x ? y = dec (dec y) - -0 ? 0 = 0 -0 ? x = dec (dec x) -x ? y = dec x - -0 ? 0 = 0 -0 ? x = dec (dec x) -x ? y = dec y + pruning with 27/65 rules + [3,0,8,0,30,0,194,0,1406] direct candidates, 0 duplicates + [3,3,9,10,32,39,197,247,1325] pattern candidates, 0 duplicates + +rules: +x - x == 0 +x * 0 == 0 +x * 1 == x +0 * x == 0 +1 * x == x +x + 0 == x +0 + x == x +x - 0 == x +(x * y) * z == x * (y * z) +(x * y) * z == y * (x * z) +(x + y) + z == x + (y + z) +(x + y) + z == y + (x + z) +x - (y - z) == z + (x - y) +(x - y) - z == x - (y + z) +(x - y) - z == x - (z + y) +(x + y) - z == x + (y - z) +(x + y) - z == y + (x - z) +(x + x) * y == x * (y + y) +x + (y - x) == y +(x - y) + y == x +x * y - x == x * (y - 1) +x * y - y == y * (x - 1) +x * (y + 1) == x + x * y +x * (y + 1) == x * y + x +(x + 1) * y == y + x * y +0 - x * y == x * (0 - y) +0 - x * y == y * (0 - x) +equations: +y * x == x * y +y + x == x + y +y * (x * z) == x * (y * z) +z * (x * y) == x * (y * z) +z * (y * x) == x * (y * z) +y + (x + z) == x + (y + z) +z + (x + y) == x + (y + z) +z + (y + x) == x + (y + z) +(z + y) * x == x * (y + z) +y + (x - z) == x + (y - z) +z * y + x == x + y * z +(x - z) + y == x + (y - z) +(z - y) + x == (x - y) + z +y * (x + x) == x * (y + y) +y - (x + y) == 0 - x +y - (y + x) == 0 - x +z - (y + z) == x - (x + y) +z - (y + z) == x - (y + x) +z - (z + y) == x - (x + y) +z - (z + y) == x - (y + x) +x * (1 - y) == x - x * y +x * (1 - y) == x - y * x +y * (0 - x) == x * (0 - y) +(0 - x) * y == x * (0 - y) +(0 - y) * x == (0 - x) * y +(1 - y) * x == x - x * y +(1 - y) * x == x - y * x +x + (0 - y) == x - y +(0 - y) + x == x - y +x - (x + 1) == 0 - 1 +x - (1 + x) == 0 - 1 +y - (y + 1) == x - (x + 1) +y - (y + 1) == x - (1 + x) +y - (1 + y) == x - (1 + x) +x * (0 - 1) == 0 - x +(0 - 1) * x == 0 - x +(0 - 1) * y == x - (x + y) +(0 - 1) * y == x - (y + x) + +direct candidates: + +foo x = x + +foo x = 0 + +foo x = 1 + +foo x = x + x + +foo x = x + 1 + +foo x = 1 + 1 + +foo x = x * x + +foo x = x - 1 + +foo x = 0 - x + +foo x = 0 - 1 + +foo x = 1 - x + +foo x = x * x - 1 + +foo x = x + (x + x) + +foo x = x + (x + 1) + +foo x = x + (1 + 1) + +foo x = x + x * x + +foo x = x + (x - 1) + +foo x = x + (0 - 1) + +foo x = 1 + (x + x) + +foo x = 1 + (x + 1) + +foo x = 1 + (1 + 1) + +foo x = 1 + x * x + +foo x = 1 + (0 - x) + +foo x = 1 + (1 - x) + +foo x = x * (x + x) + +foo x = x * (x * x) + +foo x = x * (x - 1) + +foo x = x * (0 - x) + +foo x = x * (0 - 1) + +foo x = x * (1 - x) + +foo x = x - (x + x) + +foo x = x - (x + 1) + +foo x = x - (1 + 1) + +foo x = x - x * x + +foo x = 0 - (x + x) + +foo x = 0 - (x + 1) + +foo x = 0 - (1 + 1) + +foo x = 1 - (x + x) + +foo x = 1 - (x + 1) + +foo x = 1 - (1 + 1) + +foo x = 1 - x * x + + +pattern candidates: + +foo x = x + +foo x = 0 + +foo x = 1 + +foo 0 = 0 +foo x = 1 + +foo 0 = 1 +foo x = x + +foo 0 = 1 +foo x = 0 + +foo x = x + x + +foo x = x + 1 + +foo x = x * x + +foo x = x - 1 + +foo x = 0 - x + +foo x = 1 - x + +foo 1 = 0 +foo x = x + +foo 1 = 0 +foo x = 1 + +foo 1 = 1 +foo x = 0 + +foo 0 = 0 +foo x = x + 1 + +foo 0 = 0 +foo x = x - 1 + +foo 0 = 0 +foo x = 1 - x + +foo 0 = 1 +foo x = x + x + +foo 0 = 1 +foo x = x * x + +foo 0 = 1 +foo x = x - 1 + +foo 0 = 1 +foo x = 0 - x + +foo 0 = 0 +foo 1 = 0 +foo x = 1 + +foo 0 = 1 +foo 1 = 0 +foo x = x + +foo 0 = 1 +foo 1 = 1 +foo x = 0 + +foo x = x * x - 1 + +foo x = x + (x + x) + +foo x = x + (x + 1) + +foo x = x + x * x + +foo x = x + (x - 1) + +foo x = 1 + (x + x) + +foo x = 1 + (x + 1) + +foo x = 1 + x * x + +foo x = 1 + (0 - x) + +foo x = 1 + (1 - x) + +foo x = x * (x + x) + +foo x = x * (x * x) + +foo x = x * (x - 1) + +foo x = x * (0 - x) + +foo x = x * (1 - x) + +foo x = x - (x + x) + +foo x = x - (x + 1) + +foo x = x - x * x + +foo x = 0 - (x + x) + +foo x = 0 - (x + 1) + +foo x = 1 - (x + x) + +foo x = 1 - (x + 1) + +foo x = 1 - x * x + +foo 1 = 0 +foo x = x + x + +foo 1 = 0 +foo x = x + 1 + +foo 1 = 0 +foo x = x * x + +foo 1 = 0 +foo x = 0 - x + +foo 1 = 1 +foo x = x + x + +foo 1 = 1 +foo x = x + 1 + +foo 1 = 1 +foo x = x - 1 + +foo 1 = 1 +foo x = 0 - x + +foo 1 = 1 +foo x = 1 - x + +foo 0 = 0 +foo x = x * x - 1 + +foo 0 = 0 +foo x = x + (x + 1) + +foo 0 = 0 +foo x = x + (x - 1) + +foo 0 = 0 +foo x = 1 + (x + x) + +foo 0 = 0 +foo x = 1 + (x + 1) + +foo 0 = 0 +foo x = 1 + x * x + +foo 0 = 0 +foo x = 1 + (0 - x) + +foo 0 = 0 +foo x = 1 + (1 - x) + +foo 0 = 0 +foo x = x - (x + 1) + +foo 0 = 0 +foo x = 0 - (x + 1) + +foo 0 = 0 +foo x = 1 - (x + x) + +foo 0 = 0 +foo x = 1 - x * x + +foo 0 = 1 +foo x = x * x - 1 + +foo 0 = 1 +foo x = x + (x + x) + +foo 0 = 1 +foo x = x + x * x + +foo 0 = 1 +foo x = x + (x - 1) + +foo 0 = 1 +foo x = 1 + (x + 1) + +foo 0 = 1 +foo x = 1 + (1 - x) + +foo 0 = 1 +foo x = x * (x + x) + +foo 0 = 1 +foo x = x * (x * x) + +foo 0 = 1 +foo x = x * (x - 1) + +foo 0 = 1 +foo x = x * (0 - x) + +foo 0 = 1 +foo x = x * (1 - x) + +foo 0 = 1 +foo x = x - (x + x) + +foo 0 = 1 +foo x = x - (x + 1) + +foo 0 = 1 +foo x = x - x * x + +foo 0 = 1 +foo x = 0 - (x + x) + +foo 0 = 1 +foo x = 0 - (x + 1) + +foo 0 = 1 +foo x = 1 - (x + 1) + +foo 0 = 0 +foo 1 = 0 +foo x = x + 1 + +foo 0 = 0 +foo 1 = 1 +foo x = x + 1 + +foo 0 = 0 +foo 1 = 1 +foo x = x - 1 + +foo 0 = 0 +foo 1 = 1 +foo x = 1 - x + +foo 0 = 1 +foo 1 = 0 +foo x = x + x + +foo 0 = 1 +foo 1 = 0 +foo x = x * x + +foo 0 = 1 +foo 1 = 0 +foo x = 0 - x + +foo 0 = 1 +foo 1 = 1 +foo x = x + x + +foo 0 = 1 +foo 1 = 1 +foo x = x - 1 + +foo 0 = 1 +foo 1 = 1 +foo x = 0 - x + + +Candidates for: ? :: Int -> Int -> Int + pruning with 13/34 rules + [3,3,9,18,60,162,516,1587,5148] direct candidates, 0 duplicates + [3,8,25,71,205,632,1976,6067,19140] pattern candidates, 0 duplicates + +rules: +x * 0 == 0 +0 * x == 0 +x + 0 == x +0 + x == x +dec (x + y) == x + dec y +dec (x + y) == y + dec x +dec (x + y) == dec x + y +dec (x + y) == dec y + x +(x * y) * z == x * (y * z) +(x * y) * z == y * (x * z) +(x + y) + z == x + (y + z) +(x + y) + z == y + (x + z) +(x + x) * y == x * (y + y) +equations: +y * x == x * y +y + x == x + y +y + dec x == x + dec y +dec x + y == x + dec y +dec y + x == dec x + y +x + dec 0 == dec x +dec 0 + x == dec x +y * (x * z) == x * (y * z) +z * (x * y) == x * (y * z) +z * (y * x) == x * (y * z) +y + (x + z) == x + (y + z) +z + (x + y) == x + (y + z) +z + (y + x) == x + (y + z) +(z + y) * x == x * (y + z) +z * y + x == x + y * z +y * (x + x) == x * (y + y) +y + dec (dec x) == x + dec (dec y) +dec (dec x) + y == x + dec (dec y) +dec (dec y) + x == dec (dec x) + y +x + dec (dec 0) == dec (dec x) +dec (dec 0) + x == dec (dec x) + +direct candidates: + +x ? y = x + +x ? y = y + +x ? y = 0 + +x ? y = dec x + +x ? y = dec y + +x ? y = dec 0 + +x ? y = x + x + +x ? y = x + y + +x ? y = y + y + +x ? y = x * x + +x ? y = x * y + +x ? y = y * y + +x ? y = dec (dec x) + +x ? y = dec (dec y) + +x ? y = dec (dec 0) + +x ? y = dec (x * x) + +x ? y = dec (x * y) + +x ? y = dec (y * y) + +x ? y = dec (dec (dec x)) + +x ? y = dec (dec (dec y)) + +x ? y = dec (dec (dec 0)) + +x ? y = x + dec x + +x ? y = x + dec y + +x ? y = x + dec 0 + +x ? y = y + dec x + +x ? y = y + dec y + +x ? y = y + dec 0 + +x ? y = x * dec x + +x ? y = x * dec y + +x ? y = x * dec 0 + +x ? y = y * dec x + +x ? y = y * dec y + +x ? y = y * dec 0 + +x ? y = dec (dec (x * x)) + +x ? y = dec (dec (x * y)) + +x ? y = dec (dec (y * y)) + +x ? y = dec (dec (dec (dec x))) + +x ? y = dec (dec (dec (dec y))) + +x ? y = dec (dec (dec (dec 0))) + +x ? y = dec (x * dec x) + +x ? y = dec (x * dec y) + +x ? y = dec (x * dec 0) + +x ? y = dec (y * dec x) + +x ? y = dec (y * dec y) + +x ? y = dec (y * dec 0) + +x ? y = x + (x + x) + +x ? y = x + (x + y) + +x ? y = x + (y + y) + +x ? y = x + x * x + +x ? y = x + x * y + +x ? y = x + y * y + +x ? y = x + dec (dec x) + +x ? y = x + dec (dec y) + +x ? y = x + dec (dec 0) + +x ? y = y + (x + x) + +x ? y = y + (x + y) + +x ? y = y + (y + y) + +x ? y = y + x * x + +x ? y = y + x * y + +x ? y = y + y * y + +x ? y = y + dec (dec x) + +x ? y = y + dec (dec y) + +x ? y = y + dec (dec 0) + +x ? y = x * (x + x) + +x ? y = x * (x + y) + +x ? y = x * (y + y) + +x ? y = x * (x * x) + +x ? y = x * (x * y) + +x ? y = x * (y * y) + +x ? y = x * dec (dec x) + +x ? y = x * dec (dec y) + +x ? y = x * dec (dec 0) + +x ? y = y * (x + x) + +x ? y = y * (x + y) + +x ? y = y * (y + y) + +x ? y = y * (x * x) + +x ? y = y * (x * y) + +x ? y = y * (y * y) + +x ? y = y * dec (dec x) + +x ? y = y * dec (dec y) + +x ? y = y * dec (dec 0) + +x ? y = dec x + dec x + +x ? y = dec x + dec y + +x ? y = dec x + dec 0 + +x ? y = dec y + dec y + +x ? y = dec y + dec 0 + +x ? y = dec 0 + dec 0 + +x ? y = dec x * dec x + +x ? y = dec x * dec y + +x ? y = dec x * dec 0 + +x ? y = dec y * dec y + +x ? y = dec y * dec 0 + +x ? y = dec 0 * dec 0 + + +pattern candidates: + +x ? y = x + +x ? y = y + +x ? y = 0 + +x ? y = dec x + +x ? y = dec y + +x ? 0 = x +x ? y = y + +x ? 0 = x +x ? y = 0 + +x ? 0 = 0 +x ? y = x + +0 ? x = x +x ? y = x + +0 ? x = x +x ? y = 0 + +0 ? x = 0 +x ? y = y + +x ? y = x + x + +x ? y = x + y + +x ? y = y + y + +x ? y = x * x + +x ? y = x * y + +x ? y = y * y + +x ? y = dec (dec x) + +x ? y = dec (dec y) + +x ? 0 = x +x ? y = dec x + +x ? 0 = x +x ? y = dec y + +x ? 0 = 0 +x ? y = dec x + +x ? 0 = 0 +x ? y = dec y + +x ? 0 = dec x +x ? y = x + +x ? 0 = dec x +x ? y = y + +x ? 0 = dec x +x ? y = 0 + +0 ? x = x +x ? y = dec x + +0 ? x = x +x ? y = dec y + +0 ? x = 0 +x ? y = dec x + +0 ? x = 0 +x ? y = dec y + +0 ? x = dec x +x ? y = x + +0 ? x = dec x +x ? y = y + +0 ? x = dec x +x ? y = 0 + +0 ? x = x +x ? 0 = x +x ? y = 0 + +0 ? x = x +x ? 0 = 0 +x ? y = x + +0 ? x = 0 +x ? 0 = x +x ? y = y + +x ? y = dec (x * x) + +x ? y = dec (x * y) + +x ? y = dec (y * y) + +x ? y = dec (dec (dec x)) + +x ? y = dec (dec (dec y)) + +x ? y = x + dec x + +x ? y = x + dec y + +x ? y = y + dec x + +x ? y = y + dec y + +x ? y = x * dec x + +x ? y = x * dec y + +x ? y = y * dec x + +x ? y = y * dec y + +x ? 0 = x +x ? y = x + x + +x ? 0 = x +x ? y = y + y + +x ? 0 = x +x ? y = x * x + +x ? 0 = x +x ? y = x * y + +x ? 0 = x +x ? y = y * y + +x ? 0 = x +x ? y = dec (dec x) + +x ? 0 = x +x ? y = dec (dec y) + +x ? 0 = 0 +x ? y = x + x + +x ? 0 = 0 +x ? y = x + y + +x ? 0 = 0 +x ? y = x * x + +x ? 0 = 0 +x ? y = dec (dec x) + +x ? 0 = 0 +x ? y = dec (dec y) + +x ? 0 = dec x +x ? y = dec y + +x ? 0 = x + x +x ? y = x + +x ? 0 = x + x +x ? y = y + +x ? 0 = x + x +x ? y = 0 + +x ? 0 = x * x +x ? y = x + +x ? 0 = x * x +x ? y = y + +x ? 0 = x * x +x ? y = 0 + +x ? 0 = dec (dec x) +x ? y = x + +x ? 0 = dec (dec x) +x ? y = y + +x ? 0 = dec (dec x) +x ? y = 0 + +0 ? x = x +x ? y = x + x + +0 ? x = x +x ? y = y + y + +0 ? x = x +x ? y = x * x + +0 ? x = x +x ? y = x * y + +0 ? x = x +x ? y = y * y + +0 ? x = x +x ? y = dec (dec x) + +0 ? x = x +x ? y = dec (dec y) + +0 ? x = 0 +x ? y = x + y + +0 ? x = 0 +x ? y = y + y + +0 ? x = 0 +x ? y = y * y + +0 ? x = 0 +x ? y = dec (dec x) + +0 ? x = 0 +x ? y = dec (dec y) + +0 ? x = dec x +x ? y = dec x + +0 ? x = x + x +x ? y = x + +0 ? x = x + x +x ? y = y + +0 ? x = x + x +x ? y = 0 + +0 ? x = x * x +x ? y = x + +0 ? x = x * x +x ? y = y + +0 ? x = x * x +x ? y = 0 + +0 ? x = dec (dec x) +x ? y = x + +0 ? x = dec (dec x) +x ? y = y + +0 ? x = dec (dec x) +x ? y = 0 + +0 ? x = x +x ? 0 = x +x ? y = dec x + +0 ? x = x +x ? 0 = x +x ? y = dec y + +0 ? x = x +x ? 0 = 0 +x ? y = dec x + +0 ? x = x +x ? 0 = 0 +x ? y = dec y + +0 ? x = x +x ? 0 = dec x +x ? y = x + +0 ? x = x +x ? 0 = dec x +x ? y = 0 + +0 ? x = 0 +x ? 0 = x +x ? y = dec x + +0 ? x = 0 +x ? 0 = x +x ? y = dec y + +0 ? x = 0 +x ? 0 = 0 +x ? y = dec x + +0 ? x = 0 +x ? 0 = 0 +x ? y = dec y + +0 ? x = 0 +x ? 0 = dec x +x ? y = y + +0 ? x = dec x +x ? 0 = x +x ? y = y + +0 ? x = dec x +x ? 0 = x +x ? y = 0 + +0 ? x = dec x +x ? 0 = 0 +x ? y = x + +x ? 0 = x +x ? y = x ? dec y + +x ? 0 = x +x ? y = y ? dec x + +x ? 0 = x +x ? y = y ? dec y + +x ? 0 = x +x ? y = 0 ? dec y + +x ? 0 = x +x ? y = dec x ? x + +x ? 0 = x +x ? y = dec x ? y + +x ? 0 = x +x ? y = dec y ? x + +0 ? x = x +x ? y = x ? dec y + +0 ? x = x +x ? y = y ? dec x + +0 ? x = x +x ? y = y ? dec y + +0 ? x = x +x ? y = dec x ? x + +0 ? x = x +x ? y = dec x ? y + +0 ? x = x +x ? y = dec x ? 0 + +0 ? x = x +x ? y = dec y ? x + +x ? y = dec (dec (x * x)) + +x ? y = dec (dec (x * y)) + +x ? y = dec (dec (y * y)) + +x ? y = dec (dec (dec (dec x))) + +x ? y = dec (dec (dec (dec y))) + +x ? y = dec (x * dec x) + +x ? y = dec (x * dec y) + +x ? y = dec (y * dec x) + +x ? y = dec (y * dec y) + +x ? y = x + (x + x) + +x ? y = x + (x + y) + +x ? y = x + (y + y) + +x ? y = x + x * x + +x ? y = x + x * y + +x ? y = x + y * y + +x ? y = x + dec (dec x) + +x ? y = x + dec (dec y) + +x ? y = y + (x + x) + +x ? y = y + (x + y) + +x ? y = y + (y + y) + +x ? y = y + x * x + +x ? y = y + x * y + +x ? y = y + y * y + +x ? y = y + dec (dec x) + +x ? y = y + dec (dec y) + +x ? y = x * (x + x) + +x ? y = x * (x + y) + +x ? y = x * (y + y) + +x ? y = x * (x * x) + +x ? y = x * (x * y) + +x ? y = x * (y * y) + +x ? y = x * dec (dec x) + +x ? y = x * dec (dec y) + +x ? y = y * (x + x) + +x ? y = y * (x + y) + +x ? y = y * (y + y) + +x ? y = y * (x * x) + +x ? y = y * (x * y) + +x ? y = y * (y * y) + +x ? y = y * dec (dec x) + +x ? y = y * dec (dec y) + +x ? y = dec x + dec x + +x ? y = dec x + dec y + +x ? y = dec y + dec y + +x ? y = dec x * dec x + +x ? y = dec x * dec y + +x ? y = dec y * dec y + +x ? 0 = x +x ? y = dec (x * x) + +x ? 0 = x +x ? y = dec (x * y) + +x ? 0 = x +x ? y = dec (y * y) + +x ? 0 = x +x ? y = dec (dec (dec x)) + +x ? 0 = x +x ? y = dec (dec (dec y)) + +x ? 0 = x +x ? y = x + dec x + +x ? 0 = x +x ? y = x + dec y + +x ? 0 = x +x ? y = y + dec x + +x ? 0 = x +x ? y = y + dec y + +x ? 0 = x +x ? y = x * dec x + +x ? 0 = x +x ? y = x * dec y + +x ? 0 = x +x ? y = y * dec x + +x ? 0 = x +x ? y = y * dec y + +x ? 0 = 0 +x ? y = dec (x * x) + +x ? 0 = 0 +x ? y = dec (x * y) + +x ? 0 = 0 +x ? y = dec (y * y) + +x ? 0 = 0 +x ? y = dec (dec (dec x)) + +x ? 0 = 0 +x ? y = dec (dec (dec y)) + +x ? 0 = 0 +x ? y = x + dec x + +x ? 0 = 0 +x ? y = x + dec y + +x ? 0 = 0 +x ? y = y + dec x + +x ? 0 = 0 +x ? y = y + dec y + +x ? 0 = 0 +x ? y = x * dec x + +x ? 0 = 0 +x ? y = x * dec y + +x ? 0 = dec x +x ? y = x + x + +x ? 0 = dec x +x ? y = x + y + +x ? 0 = dec x +x ? y = y + y + +x ? 0 = dec x +x ? y = x * x + +x ? 0 = dec x +x ? y = x * y + +x ? 0 = dec x +x ? y = y * y + +x ? 0 = dec x +x ? y = dec (dec x) + +x ? 0 = dec x +x ? y = dec (dec y) + +x ? 0 = x + x +x ? y = dec x + +x ? 0 = x + x +x ? y = dec y + +x ? 0 = x * x +x ? y = dec x + +x ? 0 = x * x +x ? y = dec y + +x ? 0 = dec (dec x) +x ? y = dec x + +x ? 0 = dec (dec x) +x ? y = dec y + +x ? 0 = dec (x * x) +x ? y = x + +x ? 0 = dec (x * x) +x ? y = y + +x ? 0 = dec (x * x) +x ? y = 0 + +x ? 0 = dec (dec (dec x)) +x ? y = x + +x ? 0 = dec (dec (dec x)) +x ? y = y + +x ? 0 = dec (dec (dec x)) +x ? y = 0 + +x ? 0 = x + dec x +x ? y = x + +x ? 0 = x + dec x +x ? y = y + +x ? 0 = x + dec x +x ? y = 0 + +x ? 0 = x * dec x +x ? y = x + +x ? 0 = x * dec x +x ? y = y + +x ? 0 = x * dec x +x ? y = 0 + +0 ? x = x +x ? y = dec (x * x) + +0 ? x = x +x ? y = dec (x * y) + +0 ? x = x +x ? y = dec (y * y) + +0 ? x = x +x ? y = dec (dec (dec x)) + +0 ? x = x +x ? y = dec (dec (dec y)) + +0 ? x = x +x ? y = x + dec x + +0 ? x = x +x ? y = x + dec y + +0 ? x = x +x ? y = y + dec x + +0 ? x = x +x ? y = y + dec y + +0 ? x = x +x ? y = x * dec x + +0 ? x = x +x ? y = x * dec y + +0 ? x = x +x ? y = y * dec x + +0 ? x = x +x ? y = y * dec y + +0 ? x = 0 +x ? y = dec (x * x) + +0 ? x = 0 +x ? y = dec (x * y) + +0 ? x = 0 +x ? y = dec (y * y) + +0 ? x = 0 +x ? y = dec (dec (dec x)) + +0 ? x = 0 +x ? y = dec (dec (dec y)) + +0 ? x = 0 +x ? y = x + dec x + +0 ? x = 0 +x ? y = x + dec y + +0 ? x = 0 +x ? y = y + dec x + +0 ? x = 0 +x ? y = y + dec y + +0 ? x = 0 +x ? y = y * dec x + +0 ? x = 0 +x ? y = y * dec y + +0 ? x = dec x +x ? y = x + x + +0 ? x = dec x +x ? y = x + y + +0 ? x = dec x +x ? y = y + y + +0 ? x = dec x +x ? y = x * x + +0 ? x = dec x +x ? y = x * y + +0 ? x = dec x +x ? y = y * y + +0 ? x = dec x +x ? y = dec (dec x) + +0 ? x = dec x +x ? y = dec (dec y) + +0 ? x = x + x +x ? y = dec x + +0 ? x = x + x +x ? y = dec y + +0 ? x = x * x +x ? y = dec x + +0 ? x = x * x +x ? y = dec y + +0 ? x = dec (dec x) +x ? y = dec x + +0 ? x = dec (dec x) +x ? y = dec y + +0 ? x = dec (x * x) +x ? y = x + +0 ? x = dec (x * x) +x ? y = y + +0 ? x = dec (x * x) +x ? y = 0 + +0 ? x = dec (dec (dec x)) +x ? y = x + +0 ? x = dec (dec (dec x)) +x ? y = y + +0 ? x = dec (dec (dec x)) +x ? y = 0 + +0 ? x = x + dec x +x ? y = x + +0 ? x = x + dec x +x ? y = y + +0 ? x = x + dec x +x ? y = 0 + +0 ? x = x * dec x +x ? y = x + +0 ? x = x * dec x +x ? y = y + +0 ? x = x * dec x +x ? y = 0 + +0 ? x = x +x ? 0 = x +x ? y = x + x + +0 ? x = x +x ? 0 = x +x ? y = y + y + +0 ? x = x +x ? 0 = x +x ? y = x * x + +0 ? x = x +x ? 0 = x +x ? y = x * y + +0 ? x = x +x ? 0 = x +x ? y = y * y + +0 ? x = x +x ? 0 = x +x ? y = dec (dec x) + +0 ? x = x +x ? 0 = x +x ? y = dec (dec y) + +0 ? x = x +x ? 0 = 0 +x ? y = x + x + +0 ? x = x +x ? 0 = 0 +x ? y = x * x + +0 ? x = x +x ? 0 = 0 +x ? y = dec (dec x) + +0 ? x = x +x ? 0 = 0 +x ? y = dec (dec y) + +0 ? x = x +x ? 0 = dec x +x ? y = dec y + +0 ? x = x +x ? 0 = x + x +x ? y = x + +0 ? x = x +x ? 0 = x + x +x ? y = 0 + +0 ? x = x +x ? 0 = x * x +x ? y = x + +0 ? x = x +x ? 0 = x * x +x ? y = 0 + +0 ? x = x +x ? 0 = dec (dec x) +x ? y = x + +0 ? x = x +x ? 0 = dec (dec x) +x ? y = 0 + +0 ? x = 0 +x ? 0 = x +x ? y = y + y + +0 ? x = 0 +x ? 0 = x +x ? y = y * y + +0 ? x = 0 +x ? 0 = x +x ? y = dec (dec x) + +0 ? x = 0 +x ? 0 = x +x ? y = dec (dec y) + +0 ? x = 0 +x ? 0 = 0 +x ? y = x + y + +0 ? x = 0 +x ? 0 = 0 +x ? y = dec (dec x) + +0 ? x = 0 +x ? 0 = 0 +x ? y = dec (dec y) + +0 ? x = 0 +x ? 0 = dec x +x ? y = dec y + +0 ? x = 0 +x ? 0 = x + x +x ? y = y + +0 ? x = 0 +x ? 0 = x * x +x ? y = y + +0 ? x = 0 +x ? 0 = dec (dec x) +x ? y = y + +0 ? x = dec x +x ? 0 = x +x ? y = dec x + +0 ? x = dec x +x ? 0 = 0 +x ? y = dec x + +0 ? x = dec x +x ? 0 = dec x +x ? y = x + +0 ? x = dec x +x ? 0 = dec x +x ? y = y + +0 ? x = dec x +x ? 0 = dec x +x ? y = 0 + +0 ? x = x + x +x ? 0 = x +x ? y = y + +0 ? x = x + x +x ? 0 = x +x ? y = 0 + +0 ? x = x + x +x ? 0 = 0 +x ? y = x + +0 ? x = x * x +x ? 0 = x +x ? y = y + +0 ? x = x * x +x ? 0 = x +x ? y = 0 + +0 ? x = x * x +x ? 0 = 0 +x ? y = x + +0 ? x = dec (dec x) +x ? 0 = x +x ? y = y + +0 ? x = dec (dec x) +x ? 0 = x +x ? y = 0 + +0 ? x = dec (dec x) +x ? 0 = 0 +x ? y = x + +0 ? 0 = 0 +0 ? x = dec x +x ? y = dec x Candidates for: goo :: [Int] -> [Int] diff --git a/bench/erroneous.hs b/bench/erroneous.hs --- a/bench/erroneous.hs +++ b/bench/erroneous.hs @@ -31,11 +31,11 @@ putStrLn $ " " ++ show numErroneous ++ "/" ++ show numCandidates ++ " erroneous candidates" putStrLn "" --printThy thy - putStrLn $ unlines . map showDefnWithError $ erroneous + putStrLn $ unlines . map showDefnWithErrors $ erroneous where numCandidates = length candidates numErroneous = length erroneous - erroneous = [(c, e) | c <- candidates, Just e <- [findError c]] + erroneous = [(c, e, es) | c <- candidates, (e:es) <- [listErrors c]] candidates = concat css css = take n . discardT isRedundantByIntroduction -- additional pruning rule @@ -45,9 +45,9 @@ nREs = length (equations thy) + nRules maxTests = 60 -- a hardcoded value probably will not hurt in this simple benchmark maxEvalRecursions = 60 - findError = findDefnError maxTests maxEvalRecursions nm f - showDefnWithError (d,e) = showDefn d - ++ "-- " ++ showExpr e ++ " = bottom\n" + listErrors = listDefnErrors maxTests maxEvalRecursions nm f + showDefnWithErrors (d,e,es) = showDefn d + ++ "-- " ++ showExpr e ++ " = bottom -- and " ++ show (length es) ++ " other errors\n" main :: IO () @@ -55,24 +55,25 @@ -- This N value limits the maximum size of candidates, -- increase it to print erroneous candidates of bigger size. - let n = 7 + let n = 6 - printErroneousCandidates n "foo" (undefined :: Int -> Int) + printErroneousCandidates (n+1) "foo" (undefined :: Int -> Int) [ pr (0 :: Int) , pr (1 :: Int) + , pr (2 :: Int) , prim "+" ((+) :: Int -> Int -> Int) - , prim "*" ((+) :: Int -> Int -> Int) + , prim "*" ((*) :: Int -> Int -> Int) , prim "-" ((-) :: Int -> Int -> Int) ] printErroneousCandidates n "?" (undefined :: Int -> Int -> Int) [ pr (0 :: Int) , prim "+" ((+) :: Int -> Int -> Int) - , prim "*" ((+) :: Int -> Int -> Int) + , prim "*" ((*) :: Int -> Int -> Int) , prim "dec" (subtract 1 :: Int -> Int) ] - printErroneousCandidates n "goo" (undefined :: [Int] -> [Int]) + printErroneousCandidates (n+1) "goo" (undefined :: [Int] -> [Int]) [ pr ([] :: [Int]) , prim ":" ((:) :: Int -> [Int] -> [Int]) , prim "++" ((++) :: [Int] -> [Int] -> [Int]) diff --git a/bench/erroneous.txt b/bench/erroneous.txt --- a/bench/erroneous.txt +++ b/bench/erroneous.txt @@ -1,620 +1,237 @@ Erroneous candidates for: foo :: Int -> Int - pruning with 15/35 rules - [3,3,8,9,21,27,98] candidates - 0/169 erroneous candidates + pruning with 41/82 rules + [4,8,16,42,70,162,493] candidates + 30/795 erroneous candidates +foo 0 = 0 +foo x = x + foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -Erroneous candidates for: ? :: Int -> Int -> Int - pruning with 10/23 rules - [3,8,22,50,116,302,765] candidates - 147/1266 erroneous candidates +foo 0 = 0 +foo x = foo (x - 2) + 1 +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = dec x ? y --- 0 ? 1 = bottom +foo 0 = 0 +foo x = foo (x - 2) + 2 +-- foo 1 = bottom -- and 14 other errors -0 ? x = x -x ? y = x ? dec y --- 1 ? 0 = bottom +foo 0 = 0 +foo x = x * foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = x ? dec (dec y) --- 0 ? 1 = bottom +foo 0 = 0 +foo x = x - foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = y ? dec (dec x) --- 0 ? 1 = bottom +foo 0 = 0 +foo x = foo (x - 2) - x +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = y ? dec (dec y) --- 0 ? 1 = bottom +foo 0 = 0 +foo x = foo (x - 2) - 1 +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = 0 ? dec (dec y) --- 0 ? 1 = bottom +foo 0 = 0 +foo x = foo (x - 2) - 2 +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = dec x ? dec x --- 0 ? 1 = bottom +foo 0 = 0 +foo x = 0 - foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = dec y ? dec x --- 0 ? 1 = bottom +foo 0 = 0 +foo x = 1 - foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = dec (dec x) ? x --- 1 ? 1 = bottom +foo 0 = 1 +foo x = x + foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = dec (dec x) ? y --- 0 ? 1 = bottom +foo 0 = 1 +foo x = foo (x - 2) + 1 +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = dec (dec y) ? x --- 1 ? 1 = bottom +foo 0 = 1 +foo x = foo (x - 2) + 2 +-- foo 1 = bottom -- and 14 other errors -0 ? x = x -x ? y = x ? dec (dec y) --- 1 ? 0 = bottom +foo 0 = 1 +foo x = x * foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -0 ? x = x -x ? y = y ? dec (dec x) --- 1 ? 1 = bottom +foo 0 = 1 +foo x = x - foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -0 ? x = x -x ? y = y ? dec (dec y) --- 1 ? 1 = bottom +foo 0 = 1 +foo x = foo (x - 2) - x +-- foo 1 = bottom -- and 14 other errors -0 ? x = x -x ? y = dec y ? dec x --- 1 ? 0 = bottom +foo 0 = 1 +foo x = foo (x - 2) - 1 +-- foo 1 = bottom -- and 14 other errors -0 ? x = x -x ? y = dec y ? dec y --- 1 ? 0 = bottom +foo 0 = 1 +foo x = foo (x - 2) - 2 +-- foo 1 = bottom -- and 14 other errors -0 ? x = x -x ? y = dec (dec x) ? x --- 1 ? 0 = bottom +foo 0 = 1 +foo x = 0 - foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -0 ? x = x -x ? y = dec (dec x) ? y --- 1 ? 0 = bottom +foo 0 = 1 +foo x = 1 - foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -0 ? x = x -x ? y = dec (dec x) ? 0 --- 1 ? 0 = bottom +foo 0 = 2 +foo x = x + foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -0 ? x = x -x ? y = dec (dec y) ? x --- 1 ? 0 = bottom +foo 0 = 2 +foo x = foo (x - 2) + 1 +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = dec (dec x ? y) --- 0 ? 1 = bottom +foo 0 = 2 +foo x = foo (x - 2) + 2 +-- foo 1 = bottom -- and 14 other errors -x ? 0 = 0 -x ? y = dec (dec x ? y) --- 0 ? 1 = bottom +foo 0 = 2 +foo x = x * foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -x ? 0 = dec x -x ? y = dec x ? y --- 0 ? 1 = bottom +foo 0 = 2 +foo x = x - foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -0 ? x = x -x ? y = dec (x ? dec y) --- 1 ? 0 = bottom +foo 0 = 2 +foo x = foo (x - 2) - x +-- foo 1 = bottom -- and 14 other errors -0 ? x = 0 -x ? y = dec (x ? dec y) --- 1 ? 0 = bottom +foo 0 = 2 +foo x = foo (x - 2) - 1 +-- foo 1 = bottom -- and 14 other errors -0 ? x = dec x -x ? y = x ? dec y --- 1 ? 0 = bottom +foo 0 = 2 +foo x = foo (x - 2) - 2 +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = x ? dec (dec (dec y)) --- 0 ? 1 = bottom +foo 0 = 2 +foo x = 0 - foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = y ? dec (dec (dec x)) --- 0 ? 1 = bottom +foo 0 = 2 +foo x = 1 - foo (x - 2) +-- foo 1 = bottom -- and 14 other errors -x ? 0 = x -x ? y = y ? dec (dec (dec y)) --- 0 ? 1 = bottom -x ? 0 = x -x ? y = 0 ? dec (dec (dec y)) --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec x ? (x + y) --- 1 ? 1 = bottom - -x ? 0 = x -x ? y = dec x ? (y + y) --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec x ? dec (dec x) --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec x ? dec (dec y) --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec y ? dec (dec x) --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec y ? dec (dec y) --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec (dec x) ? dec x --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec (dec y) ? dec x --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec (dec (dec x)) ? x --- 1 ? 1 = bottom - -x ? 0 = x -x ? y = dec (dec (dec x)) ? y --- 0 ? 1 = bottom +Erroneous candidates for: ? :: Int -> Int -> Int + pruning with 13/34 rules + [3,8,25,71,205,632] candidates + 26/944 erroneous candidates x ? 0 = x -x ? y = dec (dec (dec y)) ? x --- 1 ? 1 = bottom - -0 ? x = x -x ? y = x ? dec (dec (dec y)) --- 1 ? 0 = bottom - -0 ? x = x -x ? y = y ? dec (dec (dec x)) --- 1 ? 1 = bottom - -0 ? x = x -x ? y = y ? dec (dec (dec y)) --- 1 ? 1 = bottom - -0 ? x = x -x ? y = dec y ? dec (dec x) --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec y ? dec (dec y) --- 1 ? 0 = bottom - -0 ? x = x -x ? y = (x + x) ? dec y --- 1 ? 0 = bottom - -0 ? x = x -x ? y = (x + y) ? dec y --- 1 ? 1 = bottom - -0 ? x = x -x ? y = dec (dec x) ? dec x --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec (dec x) ? dec y --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec (dec y) ? dec x --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec (dec y) ? dec y --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec (dec (dec x)) ? x --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec (dec (dec x)) ? y --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec (dec (dec x)) ? 0 --- 1 ? 0 = bottom +x ? y = dec x ? y +-- 0 ? 1 = bottom -- and 16 other errors 0 ? x = x -x ? y = dec (dec (dec y)) ? x --- 1 ? 0 = bottom - -x ? 0 = x -x ? y = dec (x ? dec (dec y)) --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec (y ? dec (dec x)) --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec (y ? dec (dec y)) --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec (0 ? dec (dec y)) --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec (dec x ? dec x) --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec (dec y ? dec x) --- 0 ? 1 = bottom - -x ? 0 = x -x ? y = dec (dec (dec x) ? x) --- 1 ? 1 = bottom - -x ? 0 = x -x ? y = dec (dec (dec x) ? y) --- 0 ? 1 = bottom +x ? y = x ? dec y +-- 1 ? 0 = bottom -- and 16 other errors x ? 0 = x -x ? y = dec (dec (dec y) ? x) --- 1 ? 1 = bottom - -x ? 0 = 0 -x ? y = dec (x ? dec (dec y)) --- 0 ? 1 = bottom - -x ? 0 = 0 -x ? y = dec (y ? dec (dec x)) --- 0 ? 1 = bottom - -x ? 0 = 0 -x ? y = dec (y ? dec (dec y)) --- 0 ? 1 = bottom - -x ? 0 = 0 -x ? y = dec (0 ? dec (dec y)) --- 0 ? 1 = bottom - -x ? 0 = 0 -x ? y = dec (dec x ? dec x) --- 0 ? 1 = bottom - -x ? 0 = 0 -x ? y = dec (dec y ? dec x) --- 0 ? 1 = bottom - -x ? 0 = 0 -x ? y = dec (dec (dec x) ? x) --- 1 ? 1 = bottom - -x ? 0 = 0 -x ? y = dec (dec (dec x) ? y) --- 0 ? 1 = bottom - -x ? 0 = 0 -x ? y = dec (dec (dec y) ? x) --- 1 ? 1 = bottom - -x ? 0 = dec x x ? y = x ? dec (dec y) --- 0 ? 1 = bottom +-- 0 ? 1 = bottom -- and 9 other errors -x ? 0 = dec x +x ? 0 = x x ? y = y ? dec (dec x) --- 0 ? 1 = bottom +-- 0 ? 1 = bottom -- and 6 other errors -x ? 0 = dec x +x ? 0 = x x ? y = y ? dec (dec y) --- 0 ? 1 = bottom +-- 0 ? 1 = bottom -- and 9 other errors -x ? 0 = dec x +x ? 0 = x x ? y = 0 ? dec (dec y) --- 0 ? 1 = bottom +-- 0 ? 1 = bottom -- and 9 other errors -x ? 0 = dec x +x ? 0 = x x ? y = dec x ? dec x --- 0 ? 1 = bottom - -x ? 0 = dec x -x ? y = dec y ? dec x --- 0 ? 1 = bottom - -x ? 0 = dec x -x ? y = dec (dec x) ? x --- 1 ? 1 = bottom - -x ? 0 = dec x -x ? y = dec (dec x) ? y --- 0 ? 1 = bottom - -x ? 0 = dec x -x ? y = dec (dec y) ? x --- 1 ? 1 = bottom - -0 ? x = x -x ? y = dec (x ? dec (dec y)) --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec (y ? dec (dec x)) --- 1 ? 1 = bottom - -0 ? x = x -x ? y = dec (y ? dec (dec y)) --- 1 ? 1 = bottom - -0 ? x = x -x ? y = dec (dec y ? dec x) --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec (dec y ? dec y) --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec (dec (dec x) ? x) --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec (dec (dec x) ? y) --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec (dec (dec x) ? 0) --- 1 ? 0 = bottom - -0 ? x = x -x ? y = dec (dec (dec y) ? x) --- 1 ? 0 = bottom - -0 ? x = 0 -x ? y = dec (x ? dec (dec y)) --- 1 ? 0 = bottom - -0 ? x = 0 -x ? y = dec (y ? dec (dec x)) --- 1 ? 1 = bottom - -0 ? x = 0 -x ? y = dec (y ? dec (dec y)) --- 1 ? 1 = bottom - -0 ? x = 0 -x ? y = dec (dec y ? dec x) --- 1 ? 0 = bottom - -0 ? x = 0 -x ? y = dec (dec y ? dec y) --- 1 ? 0 = bottom - -0 ? x = 0 -x ? y = dec (dec (dec x) ? x) --- 1 ? 0 = bottom - -0 ? x = 0 -x ? y = dec (dec (dec x) ? y) --- 1 ? 0 = bottom - -0 ? x = 0 -x ? y = dec (dec (dec x) ? 0) --- 1 ? 0 = bottom - -0 ? x = 0 -x ? y = dec (dec (dec y) ? x) --- 1 ? 0 = bottom - -0 ? x = dec x -x ? y = x ? dec (dec y) --- 1 ? 0 = bottom - -0 ? x = dec x -x ? y = y ? dec (dec x) --- 1 ? 1 = bottom - -0 ? x = dec x -x ? y = y ? dec (dec y) --- 1 ? 1 = bottom +-- 0 ? 1 = bottom -- and 4 other errors -0 ? x = dec x +x ? 0 = x x ? y = dec y ? dec x --- 1 ? 0 = bottom - -0 ? x = dec x -x ? y = dec y ? dec y --- 1 ? 0 = bottom - -0 ? x = dec x -x ? y = dec (dec x) ? x --- 1 ? 0 = bottom - -0 ? x = dec x -x ? y = dec (dec x) ? y --- 1 ? 0 = bottom - -0 ? x = dec x -x ? y = dec (dec x) ? 0 --- 1 ? 0 = bottom - -0 ? x = dec x -x ? y = dec (dec y) ? x --- 1 ? 0 = bottom +-- 0 ? 1 = bottom -- and 5 other errors -0 ? x = x x ? 0 = x -x ? y = x ? dec (dec y) --- 1 ? 1 = bottom - -0 ? x = x -x ? 0 = x -x ? y = y ? dec (dec x) --- 1 ? 1 = bottom - -0 ? x = x -x ? 0 = x -x ? y = y ? dec (dec y) --- 1 ? 1 = bottom - -0 ? x = x -x ? 0 = x x ? y = dec (dec x) ? x --- 1 ? 1 = bottom +-- 1 ? 1 = bottom -- and 6 other errors -0 ? x = x x ? 0 = x x ? y = dec (dec x) ? y --- 1 ? 1 = bottom +-- 0 ? 1 = bottom -- and 16 other errors -0 ? x = x x ? 0 = x x ? y = dec (dec y) ? x --- 1 ? 1 = bottom +-- 1 ? 1 = bottom -- and 3 other errors 0 ? x = x -x ? 0 = 0 x ? y = x ? dec (dec y) --- 1 ? 1 = bottom +-- 1 ? 0 = bottom -- and 16 other errors 0 ? x = x -x ? 0 = 0 x ? y = y ? dec (dec x) --- 1 ? 1 = bottom +-- 1 ? 1 = bottom -- and 3 other errors 0 ? x = x -x ? 0 = 0 x ? y = y ? dec (dec y) --- 1 ? 1 = bottom +-- 1 ? 1 = bottom -- and 6 other errors 0 ? x = x -x ? 0 = 0 -x ? y = dec (dec x) ? x --- 1 ? 1 = bottom +x ? y = dec y ? dec x +-- 1 ? 0 = bottom -- and 5 other errors 0 ? x = x -x ? 0 = 0 -x ? y = dec (dec x) ? y --- 1 ? 1 = bottom +x ? y = dec y ? dec y +-- 1 ? 0 = bottom -- and 4 other errors 0 ? x = x -x ? 0 = 0 -x ? y = dec (dec y) ? x --- 1 ? 1 = bottom - -0 ? x = 0 -x ? 0 = x -x ? y = x ? dec (dec y) --- 1 ? 1 = bottom - -0 ? x = 0 -x ? 0 = x -x ? y = y ? dec (dec x) --- 1 ? 1 = bottom - -0 ? x = 0 -x ? 0 = x -x ? y = y ? dec (dec y) --- 1 ? 1 = bottom - -0 ? x = 0 -x ? 0 = x x ? y = dec (dec x) ? x --- 1 ? 1 = bottom +-- 1 ? 0 = bottom -- and 9 other errors -0 ? x = 0 -x ? 0 = x +0 ? x = x x ? y = dec (dec x) ? y --- 1 ? 1 = bottom - -0 ? x = 0 -x ? 0 = x -x ? y = dec (dec y) ? x --- 1 ? 1 = bottom +-- 1 ? 0 = bottom -- and 9 other errors -x ? 0 = x -x ? y = x + dec x ? y --- 0 ? 1 = bottom +0 ? x = x +x ? y = dec (dec x) ? 0 +-- 1 ? 0 = bottom -- and 9 other errors -x ? 0 = x -x ? y = dec x ? y + y --- 0 ? 1 = bottom +0 ? x = x +x ? y = dec (dec y) ? x +-- 1 ? 0 = bottom -- and 6 other errors x ? 0 = x -x ? y = dec (dec (dec x ? y)) --- 0 ? 1 = bottom - -x ? 0 = 0 -x ? y = x + dec x ? y --- 0 ? 1 = bottom - -x ? 0 = 0 -x ? y = dec x ? y + y --- 0 ? 1 = bottom +x ? y = dec (dec x ? y) +-- 0 ? 1 = bottom -- and 16 other errors x ? 0 = 0 -x ? y = dec (dec (dec x ? y)) --- 0 ? 1 = bottom - -x ? 0 = dec x x ? y = dec (dec x ? y) --- 0 ? 1 = bottom - -x ? 0 = x + x -x ? y = dec x ? y --- 0 ? 1 = bottom +-- 0 ? 1 = bottom -- and 16 other errors -x ? 0 = dec (dec x) +x ? 0 = dec x x ? y = dec x ? y --- 0 ? 1 = bottom - -0 ? x = x -x ? y = x + x ? dec y --- 1 ? 0 = bottom - -0 ? x = x -x ? y = x ? dec y + y --- 1 ? 0 = bottom +-- 0 ? 1 = bottom -- and 16 other errors 0 ? x = x -x ? y = dec (dec (x ? dec y)) --- 1 ? 0 = bottom - -0 ? x = 0 -x ? y = x + x ? dec y --- 1 ? 0 = bottom - -0 ? x = 0 -x ? y = x ? dec y + y --- 1 ? 0 = bottom +x ? y = dec (x ? dec y) +-- 1 ? 0 = bottom -- and 16 other errors 0 ? x = 0 -x ? y = dec (dec (x ? dec y)) --- 1 ? 0 = bottom - -0 ? x = dec x x ? y = dec (x ? dec y) --- 1 ? 0 = bottom - -0 ? x = x + x -x ? y = x ? dec y --- 1 ? 0 = bottom - -0 ? x = dec (dec x) -x ? y = x ? dec y --- 1 ? 0 = bottom +-- 1 ? 0 = bottom -- and 16 other errors -0 ? 0 = 0 0 ? x = dec x x ? y = x ? dec y --- 1 ? 0 = bottom +-- 1 ? 0 = bottom -- and 16 other errors Erroneous candidates for: goo :: [Int] -> [Int] @@ -625,19 +242,19 @@ Erroneous candidates for: ?? :: [Int] -> [Int] -> [Int] pruning with 4/4 rules - [3,8,15,43,122,264,830] candidates - 0/1285 erroneous candidates + [3,8,15,43,122,264] candidates + 0/455 erroneous candidates Erroneous candidates for: ton :: Bool -> Bool pruning with 39/49 rules - [3,2,0,0,0,0,0] candidates + [3,2,0,0,0,0] candidates 0/5 erroneous candidates Erroneous candidates for: &| :: Bool -> Bool -> Bool pruning with 39/49 rules - [4,12,20,6,2,16,18] candidates - 0/78 erroneous candidates + [4,12,20,6,2,16] candidates + 0/60 erroneous candidates diff --git a/bench/gps.txt b/bench/gps.txt --- a/bench/gps.txt +++ b/bench/gps.txt @@ -4,9 +4,9 @@ -- looking through 1 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 1 candidates of size 3 --- looking through 1 candidates of size 4 +-- looking through 2 candidates of size 4 -- tested 4 candidates -gps1 x y = y + fromIntegral x +gps1 x y = fromIntegral x + y gps2 :: Int -> Maybe [Char] -- testing 6 combinations of argument values @@ -334,7 +334,7 @@ -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 1 candidates of size 3 --- looking through 9 candidates of size 4 +-- looking through 10 candidates of size 4 -- tested 13 candidates gps18 xs ys = zipWith (+) xs ys diff --git a/bench/gps2.txt b/bench/gps2.txt --- a/bench/gps2.txt +++ b/bench/gps2.txt @@ -43,11 +43,11 @@ -- pruning with 2/6 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 --- looking through 17 candidates of size 3 --- looking through 62 candidates of size 4 --- looking through 266 candidates of size 5 --- looking through 1154 candidates of size 6 --- tested 1503 candidates +-- looking through 18 candidates of size 3 +-- looking through 66 candidates of size 4 +-- looking through 316 candidates of size 5 +-- looking through 1376 candidates of size 6 +-- tested 1780 candidates cannot conjure gps3 :: [Char] -> Int @@ -58,7 +58,7 @@ cannot conjure gps4 :: [Char] -> [Char] --- pruning with 13/20 rules +-- pruning with 13/21 rules -- looking through 2 candidates of size 1 -- looking through 3 candidates of size 2 -- looking through 8 candidates of size 3 @@ -259,10 +259,10 @@ -- looking through 2 candidates of size 1 -- looking through 8 candidates of size 2 -- looking through 32 candidates of size 3 --- looking through 70 candidates of size 4 --- looking through 396 candidates of size 5 --- looking through 1016 candidates of size 6 --- tested 1524 candidates +-- looking through 74 candidates of size 4 +-- looking through 433 candidates of size 5 +-- looking through 1218 candidates of size 6 +-- tested 1767 candidates cannot conjure gps19_snowday :: Int -> Double -> Double -> Double -> Double @@ -270,11 +270,11 @@ -- pruning with 6/19 rules -- looking through 3 candidates of size 1 -- looking through 6 candidates of size 2 --- looking through 24 candidates of size 3 --- looking through 120 candidates of size 4 --- looking through 318 candidates of size 5 --- looking through 1944 candidates of size 6 --- tested 2415 candidates +-- looking through 27 candidates of size 3 +-- looking through 138 candidates of size 4 +-- looking through 435 candidates of size 5 +-- looking through 2715 candidates of size 6 +-- tested 3324 candidates cannot conjure gps20 :: [Char] -> Bool @@ -379,9 +379,9 @@ -- looking through 2 candidates of size 1 -- looking through 9 candidates of size 2 -- looking through 49 candidates of size 3 --- looking through 195 candidates of size 4 --- looking through 1035 candidates of size 5 --- looking through 4596 candidates of size 6 --- tested 5886 candidates +-- looking through 200 candidates of size 4 +-- looking through 1104 candidates of size 5 +-- looking through 5170 candidates of size 6 +-- tested 6534 candidates cannot conjure diff --git a/bench/p12.txt b/bench/p12.txt --- a/bench/p12.txt +++ b/bench/p12.txt @@ -1,7 +1,7 @@ running with 13 primitives factorial :: Int -> Int -- testing 6 combinations of argument values --- pruning with 67/100 rules +-- pruning with 67/101 rules -- looking through 3 candidates of size 1 -- looking through 3 candidates of size 2 -- looking through 6 candidates of size 3 diff --git a/bench/redundants.hs b/bench/redundants.hs --- a/bench/redundants.hs +++ b/bench/redundants.hs @@ -58,28 +58,29 @@ -- This N value limits the maximum size of candidates, -- increase it to print redundant candidates of bigger size. - let n = 6 - -- With n = 6, this should run in a few seconds. + let n = 5 + -- With n = 5, this should run in a few seconds. + -- With n = 6, this should run in a few more seconds. -- With n = 7 and -O2 optimization, -- this should take a few minutes to run and generate a ~300K text file. -- We can also customize the n per-function below: - printRedundantCandidates n "foo" (undefined :: Int -> Int) + printRedundantCandidates (n+1) "foo" (undefined :: Int -> Int) [ pr (0 :: Int) , pr (1 :: Int) , prim "+" ((+) :: Int -> Int -> Int) - , prim "*" ((+) :: Int -> Int -> Int) + , prim "*" ((*) :: Int -> Int -> Int) , prim "-" ((-) :: Int -> Int -> Int) ] printRedundantCandidates n "?" (undefined :: Int -> Int -> Int) [ pr (0 :: Int) , prim "+" ((+) :: Int -> Int -> Int) - , prim "*" ((+) :: Int -> Int -> Int) + , prim "*" ((*) :: Int -> Int -> Int) , prim "dec" (subtract 1 :: Int -> Int) ] - printRedundantCandidates n "goo" (undefined :: [Int] -> [Int]) + printRedundantCandidates (n+1) "goo" (undefined :: [Int] -> [Int]) [ pr ([] :: [Int]) , prim ":" ((:) :: Int -> [Int] -> [Int]) , prim "++" ((++) :: [Int] -> [Int] -> [Int]) @@ -91,7 +92,7 @@ , prim "++" ((++) :: [Int] -> [Int] -> [Int]) ] - printRedundantCandidates n "ton" (undefined :: Bool -> Bool) + printRedundantCandidates (n+1) "ton" (undefined :: Bool -> Bool) [ pr False , pr True , prim "&&" (&&) diff --git a/bench/redundants.txt b/bench/redundants.txt --- a/bench/redundants.txt +++ b/bench/redundants.txt @@ -1,1934 +1,902 @@ Redundant candidates for: foo :: Int -> Int - pruning with 15/35 rules - [3,3,8,9,21,27] candidates - 63/71 unique candidates - 8/71 redundant candidates - -rules: -x * y == x + y -x * y == y + x -x - x == 0 -x + 0 == x -0 + x == x -x - 0 == x -(x + y) + z == x + (y + z) -(x + y) + z == y + (x + z) -x - (y - z) == z + (x - y) -(x - y) - z == x - (y + z) -(x - y) - z == x - (z + y) -(x + y) - z == x + (y - z) -(x + y) - z == y + (x - z) -x + (y - x) == y -(x - y) + y == x -equations: -y + x == x + y -y + (x + z) == x + (y + z) -z + (x + y) == x + (y + z) -z + (y + x) == x + (y + z) -y + (x - z) == x + (y - z) -(x - z) + y == x + (y - z) -(z - y) + x == (x - y) + z -y - (x + y) == 0 - x -y - (y + x) == 0 - x -z - (y + z) == x - (x + y) -z - (y + z) == x - (y + x) -z - (z + y) == x - (x + y) -z - (z + y) == x - (y + x) -x + (0 - y) == x - y -(0 - y) + x == x - y -x - (x + 1) == 0 - 1 -x - (1 + x) == 0 - 1 -y - (y + 1) == x - (x + 1) -y - (y + 1) == x - (1 + x) -y - (1 + y) == x - (1 + x) - -class of 3 equivalent candidates: - - foo x = 0 - x - - foo x = x - (x + x) - - foo x = 1 - (x + 1) - - -class of 2 equivalent candidates: - - foo x = 1 - x - - foo x = 1 + (0 - x) - - -class of 2 equivalent candidates: - - foo 0 = 0 - foo x = 1 - x - - foo 0 = 0 - foo x = 1 + (0 - x) - - -class of 3 equivalent candidates: - - foo 0 = 1 - foo x = 0 - x - - foo 0 = 1 - foo x = x - (x + x) - - foo 0 = 1 - foo x = 1 - (x + 1) - - -class of 2 equivalent candidates: - - foo x = x + (x + 1) - - foo x = 1 + (x + x) - - -class of 2 equivalent candidates: - - foo 0 = 0 - foo x = x + (x + 1) - - foo 0 = 0 - foo x = 1 + (x + x) - - - -Redundant candidates for: ? :: Int -> Int -> Int - pruning with 10/23 rules - [3,8,22,50,116,302] candidates - 410/501 unique candidates - 91/501 redundant candidates - -rules: -x * y == x + y -x * y == y + x -x + 0 == x -0 + x == x -dec (x + y) == x + dec y -dec (x + y) == y + dec x -dec (x + y) == dec x + y -dec (x + y) == dec y + x -(x + y) + z == x + (y + z) -(x + y) + z == y + (x + z) -equations: -y + x == x + y -y + dec x == x + dec y -dec x + y == x + dec y -dec y + x == dec x + y -x + dec 0 == dec x -dec 0 + x == dec x -y + (x + z) == x + (y + z) -z + (x + y) == x + (y + z) -z + (y + x) == x + (y + z) -y + dec (dec x) == x + dec (dec y) -dec (dec x) + y == x + dec (dec y) -x + dec (dec 0) == dec (dec x) -dec (dec 0) + x == dec (dec x) - -class of 3 equivalent candidates: - - x ? y = x - - x ? 0 = x - x ? y = x ? dec y - - 0 ? x = 0 - x ? 0 = x - x ? y = x ? dec y - - -class of 3 equivalent candidates: - - x ? y = y - - 0 ? x = x - x ? y = dec x ? y - - 0 ? x = x - x ? 0 = 0 - x ? y = dec x ? y - - -class of 2 equivalent candidates: - - x ? y = dec x - - x ? 0 = dec x - x ? y = x ? dec y - - -class of 2 equivalent candidates: - - x ? y = dec y - - 0 ? x = dec x - x ? y = dec x ? y - - -class of 2 equivalent candidates: - - x ? 0 = x - x ? y = y - - 0 ? x = x - x ? 0 = x - x ? y = dec x ? y - - -class of 6 equivalent candidates: - - x ? 0 = x - x ? y = 0 - - x ? 0 = x - x ? y = 0 ? dec y - - x ? 0 = x - x ? y = dec y ? dec y - - 0 ? x = 0 - x ? 0 = x - x ? y = dec x ? x - - 0 ? x = 0 - x ? 0 = x - x ? y = dec x ? y - - 0 ? x = 0 - x ? 0 = x - x ? y = dec y ? x - - -class of 2 equivalent candidates: - - 0 ? x = x - x ? y = x - - 0 ? x = x - x ? 0 = x - x ? y = x ? dec y - - -class of 6 equivalent candidates: - - 0 ? x = x - x ? y = 0 - - 0 ? x = x - x ? y = dec x ? 0 - - 0 ? x = x - x ? y = dec x ? dec x - - 0 ? x = x - x ? 0 = 0 - x ? y = x ? dec y - - 0 ? x = x - x ? 0 = 0 - x ? y = y ? dec x - - 0 ? x = x - x ? 0 = 0 - x ? y = y ? dec y - - -class of 2 equivalent candidates: - - x ? 0 = dec x - x ? y = 0 - - x ? 0 = dec x - x ? y = y ? dec y - - -class of 2 equivalent candidates: - - 0 ? x = dec x - x ? y = 0 - - 0 ? x = dec x - x ? y = dec x ? x - - -class of 4 equivalent candidates: - - x ? y = x + dec y - - x ? y = y + dec x - - x ? 0 = dec x - x ? y = x + dec y - - 0 ? x = dec x - x ? y = y + dec x - - -class of 3 equivalent candidates: - - x ? 0 = x - x ? y = dec x ? y - - x ? 0 = x - x ? y = dec (dec x) ? y - - x ? 0 = x - x ? y = dec (dec x ? y) - - -class of 3 equivalent candidates: - - 0 ? x = x - x ? y = x ? dec y - - 0 ? x = x - x ? y = x ? dec (dec y) - - 0 ? x = x - x ? y = dec (x ? dec y) - - -class of 2 equivalent candidates: - - x ? y = x + (x + y) - - x ? y = y + (x + x) - - -class of 2 equivalent candidates: - - x ? y = x + (y + y) - - x ? y = y + (x + y) - - -class of 2 equivalent candidates: - - x ? y = x + dec (dec x) - - x ? y = dec x + dec x - - -class of 3 equivalent candidates: - - x ? y = x + dec (dec y) - - x ? y = y + dec (dec x) - - x ? y = dec x + dec y - - -class of 2 equivalent candidates: - - x ? y = y + dec (dec y) - - x ? y = dec y + dec y - - -class of 2 equivalent candidates: - - x ? 0 = x - x ? y = x + dec y - - x ? 0 = x - x ? y = y + dec x - - -class of 2 equivalent candidates: - - x ? 0 = 0 - x ? y = x + dec y - - x ? 0 = 0 - x ? y = y + dec x - - -class of 2 equivalent candidates: - - 0 ? x = x - x ? y = x + dec y - - 0 ? x = x - x ? y = y + dec x - - -class of 2 equivalent candidates: - - 0 ? x = 0 - x ? y = x + dec y - - 0 ? x = 0 - x ? y = y + dec x - - -class of 2 equivalent candidates: - - x ? 0 = x - x ? y = dec x ? dec y - - x ? 0 = x - x ? y = dec (x ? dec y) - - -class of 2 equivalent candidates: - - 0 ? x = x - x ? y = dec x ? dec y - - 0 ? x = x - x ? y = dec (dec x ? y) - - -class of 3 equivalent candidates: - - x ? 0 = 0 - x ? y = dec (x ? dec y) - - x ? 0 = 0 - x ? y = dec (y ? dec y) - - x ? 0 = 0 - x ? y = dec (0 ? dec y) - - -class of 3 equivalent candidates: - - 0 ? x = 0 - x ? y = dec (dec x ? x) - - 0 ? x = 0 - x ? y = dec (dec x ? y) - - 0 ? x = 0 - x ? y = dec (dec x ? 0) - - -class of 2 equivalent candidates: - - 0 ? x = x - x ? 0 = x - x ? y = y ? dec y - - 0 ? x = x - x ? 0 = x - x ? y = dec x ? x - - -class of 2 equivalent candidates: - - x ? y = x + dec (dec (dec x)) - - x ? y = dec x + dec (dec x) - - -class of 4 equivalent candidates: - - x ? y = x + dec (dec (dec y)) - - x ? y = y + dec (dec (dec x)) - - x ? y = dec x + dec (dec y) - - x ? y = dec y + dec (dec x) - - -class of 2 equivalent candidates: - - x ? y = x + (x + dec x) - - x ? y = dec x + (x + x) - - -class of 5 equivalent candidates: - - x ? y = x + (x + dec y) - - x ? y = x + (y + dec x) - - x ? y = y + (x + dec x) - - x ? y = dec x + (x + y) - - x ? y = dec y + (x + x) - - -class of 5 equivalent candidates: - - x ? y = x + (y + dec y) - - x ? y = y + (x + dec y) - - x ? y = y + (y + dec x) - - x ? y = dec x + (y + y) - - x ? y = dec y + (x + y) - - -class of 2 equivalent candidates: - - x ? y = y + dec (dec (dec y)) - - x ? y = dec y + dec (dec y) - - -class of 2 equivalent candidates: - - x ? y = y + (y + dec y) - - x ? y = dec y + (y + y) - - -class of 2 equivalent candidates: - - x ? 0 = x - x ? y = x + (x + y) - - x ? 0 = x - x ? y = y + (x + x) - - -class of 2 equivalent candidates: - - x ? 0 = x - x ? y = x + dec (dec x) - - x ? 0 = x - x ? y = dec x + dec x - - -class of 3 equivalent candidates: - - x ? 0 = x - x ? y = x + dec (dec y) - - x ? 0 = x - x ? y = y + dec (dec x) - - x ? 0 = x - x ? y = dec x + dec y - - -class of 2 equivalent candidates: - - x ? 0 = x - x ? y = y + dec (dec y) - - x ? 0 = x - x ? y = dec y + dec y - - -class of 2 equivalent candidates: - - x ? 0 = 0 - x ? y = x + (x + y) - - x ? 0 = 0 - x ? y = y + (x + x) - - -class of 2 equivalent candidates: - - x ? 0 = 0 - x ? y = x + (y + y) - - x ? 0 = 0 - x ? y = y + (x + y) - - -class of 2 equivalent candidates: - - x ? 0 = 0 - x ? y = x + dec (dec x) - - x ? 0 = 0 - x ? y = dec x + dec x - - -class of 3 equivalent candidates: - - x ? 0 = 0 - x ? y = x + dec (dec y) - - x ? 0 = 0 - x ? y = y + dec (dec x) - - x ? 0 = 0 - x ? y = dec x + dec y - - -class of 2 equivalent candidates: - - x ? 0 = 0 - x ? y = y + dec (dec y) - - x ? 0 = 0 - x ? y = dec y + dec y - - -class of 2 equivalent candidates: - - x ? 0 = x + dec (dec x) - x ? y = x - - x ? 0 = dec x + dec x - x ? y = x - - -class of 2 equivalent candidates: - - x ? 0 = x + dec (dec x) - x ? y = y - - x ? 0 = dec x + dec x - x ? y = y - - -class of 2 equivalent candidates: - - x ? 0 = x + dec (dec x) - x ? y = 0 - - x ? 0 = dec x + dec x - x ? y = 0 - - -class of 2 equivalent candidates: - - 0 ? x = x - x ? y = x + (y + y) - - 0 ? x = x - x ? y = y + (x + y) - - -class of 2 equivalent candidates: - - 0 ? x = x - x ? y = x + dec (dec x) - - 0 ? x = x - x ? y = dec x + dec x - - -class of 3 equivalent candidates: - - 0 ? x = x - x ? y = x + dec (dec y) - - 0 ? x = x - x ? y = y + dec (dec x) - - 0 ? x = x - x ? y = dec x + dec y - - -class of 2 equivalent candidates: - - 0 ? x = x - x ? y = y + dec (dec y) - - 0 ? x = x - x ? y = dec y + dec y - - -class of 2 equivalent candidates: - - 0 ? x = 0 - x ? y = x + (x + y) - - 0 ? x = 0 - x ? y = y + (x + x) - - -class of 2 equivalent candidates: - - 0 ? x = 0 - x ? y = x + (y + y) - - 0 ? x = 0 - x ? y = y + (x + y) - - -class of 2 equivalent candidates: - - 0 ? x = 0 - x ? y = x + dec (dec x) - - 0 ? x = 0 - x ? y = dec x + dec x - - -class of 3 equivalent candidates: - - 0 ? x = 0 - x ? y = x + dec (dec y) - - 0 ? x = 0 - x ? y = y + dec (dec x) - - 0 ? x = 0 - x ? y = dec x + dec y - - -class of 2 equivalent candidates: - - 0 ? x = 0 - x ? y = y + dec (dec y) - - 0 ? x = 0 - x ? y = dec y + dec y - - -class of 2 equivalent candidates: - - 0 ? x = x + dec (dec x) - x ? y = x - - 0 ? x = dec x + dec x - x ? y = x - - -class of 2 equivalent candidates: - - 0 ? x = x + dec (dec x) - x ? y = y - - 0 ? x = dec x + dec x - x ? y = y - - -class of 2 equivalent candidates: - - 0 ? x = x + dec (dec x) - x ? y = 0 - - 0 ? x = dec x + dec x - x ? y = 0 - - -class of 2 equivalent candidates: - - 0 ? x = x - x ? 0 = x - x ? y = x + dec y - - 0 ? x = x - x ? 0 = x - x ? y = y + dec x - - -class of 2 equivalent candidates: - - 0 ? x = x - x ? 0 = 0 - x ? y = x + dec y - - 0 ? x = x - x ? 0 = 0 - x ? y = y + dec x - - -class of 2 equivalent candidates: - - 0 ? x = 0 - x ? 0 = x - x ? y = x + dec y - - 0 ? x = 0 - x ? 0 = x - x ? y = y + dec x - - -class of 2 equivalent candidates: - - 0 ? x = 0 - x ? 0 = 0 - x ? y = x + dec y - - 0 ? x = 0 - x ? 0 = 0 - x ? y = y + dec x - - - -Redundant candidates for: goo :: [Int] -> [Int] - pruning with 4/4 rules - [2,1,1,2,4,7] candidates - 15/17 unique candidates - 2/17 redundant candidates - -rules: -xs ++ [] == xs -[] ++ xs == xs -(xs ++ ys) ++ zs == xs ++ (ys ++ zs) -(x:xs) ++ ys == x:(xs ++ ys) - -class of 2 equivalent candidates: - - goo xs = xs - - goo [] = [] - goo (x:xs) = x:goo xs - - -class of 2 equivalent candidates: - - goo xs = [] - - goo [] = [] - goo (x:xs) = goo xs ++ goo xs - - - -Redundant candidates for: ?? :: [Int] -> [Int] -> [Int] - pruning with 4/4 rules - [3,8,15,43,122,264] candidates - 325/455 unique candidates - 130/455 redundant candidates - -rules: -xs ++ [] == xs -[] ++ xs == xs -(xs ++ ys) ++ zs == xs ++ (ys ++ zs) -(x:xs) ++ ys == x:(xs ++ ys) - -class of 9 equivalent candidates: - - xs ?? ys = xs - - xs ?? [] = xs - xs ?? (x:ys) = xs ?? ys - - xs ?? [] = xs - xs ?? (x:ys) = xs ++ [] ?? xs - - xs ?? [] = xs - xs ?? (x:ys) = xs ++ [] ?? ys - - xs ?? [] = xs - xs ?? (x:ys) = [] ?? xs ++ xs - - xs ?? [] = xs - xs ?? (x:ys) = [] ?? ys ++ xs - - [] ?? xs = [] - (x:xs) ?? ys = x:xs ?? xs - - [] ?? xs = [] - (x:xs) ?? ys = x:xs ?? ys - - [] ?? xs = [] - (x:xs) ?? ys = x:xs ?? [] - - -class of 9 equivalent candidates: - - xs ?? ys = ys - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? ys - - xs ?? [] = [] - xs ?? (x:ys) = x:xs ?? ys - - xs ?? [] = [] - xs ?? (x:ys) = x:ys ?? ys - - xs ?? [] = [] - xs ?? (x:ys) = x:[] ?? ys - - [] ?? xs = xs - (x:xs) ?? ys = ys ++ xs ?? [] - - [] ?? xs = xs - (x:xs) ?? ys = ys ++ ys ?? [] - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? [] ++ ys - - [] ?? xs = xs - (x:xs) ?? ys = ys ?? [] ++ ys - - -class of 6 equivalent candidates: - - xs ?? [] = xs - xs ?? (x:ys) = [] - - xs ?? [] = xs - xs ?? (x:ys) = ys ?? ys - - xs ?? [] = xs - xs ?? (x:ys) = [] ?? xs - - xs ?? [] = xs - xs ?? (x:ys) = [] ?? ys - - [] ?? xs = [] - (x:xs) ?? [] = x:xs - (x:xs) ?? (y:ys) = [] - - xs ?? [] = xs - xs ?? (x:ys) = (ys ++ ys) ?? ys - - -class of 6 equivalent candidates: - - xs ?? [] = [] - xs ?? (x:ys) = xs - - [] ?? xs = [] - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = x:xs - - xs ?? [] = [] - xs ?? (x:ys) = xs ++ [] ?? xs - - xs ?? [] = [] - xs ?? (x:ys) = xs ++ [] ?? ys - - xs ?? [] = [] - xs ?? (x:ys) = [] ?? xs ++ xs - - xs ?? [] = [] - xs ?? (x:ys) = [] ?? ys ++ xs - - -class of 3 equivalent candidates: - - xs ?? [] = [] - xs ?? (x:ys) = ys - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? ys = xs ?? ys - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? ys = [] ?? ys - - -class of 11 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? ys = [] - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? xs - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? [] - - [] ?? xs = xs - (x:xs) ?? ys = ys ?? [] - - [] ?? xs = xs - (x:xs) ?? [] = xs ?? xs - (x:xs) ?? (y:ys) = [] - - [] ?? xs = xs - (x:xs) ?? [] = xs ?? [] - (x:xs) ?? (y:ys) = [] - - [] ?? xs = xs - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = xs ?? xs - - [] ?? xs = xs - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = xs ?? [] - - [] ?? xs = xs - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = ys ?? ys - - [] ?? xs = xs - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = ys ?? [] - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? (xs ++ xs) - - -class of 2 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? ys = xs - - [] ?? [] = [] - [] ?? (x:xs) = [] ?? xs - (x:xs) ?? ys = xs - - -class of 7 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? ys = ys - - [] ?? [] = [] - [] ?? (x:xs) = xs ?? [] - (x:xs) ?? ys = ys - - [] ?? [] = [] - [] ?? (x:xs) = [] ?? xs - (x:xs) ?? ys = ys - - [] ?? xs = [] - (x:xs) ?? ys = ys ++ xs ?? [] - - [] ?? xs = [] - (x:xs) ?? ys = ys ++ ys ?? [] - - [] ?? xs = [] - (x:xs) ?? ys = xs ?? [] ++ ys - - [] ?? xs = [] - (x:xs) ?? ys = ys ?? [] ++ ys - - -class of 2 equivalent candidates: - - xs ?? ys = xs ++ xs - - xs ?? [] = xs ++ xs - xs ?? (x:ys) = xs ?? ys - - -class of 4 equivalent candidates: - - xs ?? ys = xs ++ ys - - [] ?? xs = xs - (x:xs) ?? ys = x:xs ?? ys - - xs ?? [] = xs - xs ?? (x:ys) = xs ++ (x:ys) - - [] ?? xs = xs - (x:xs) ?? ys = x:(xs ++ ys) - - -class of 4 equivalent candidates: - - xs ?? ys = ys ++ xs - - xs ?? [] = xs - xs ?? (x:ys) = x:xs ?? ys - - xs ?? [] = xs - xs ?? (x:ys) = x:(ys ++ xs) - - [] ?? xs = xs - (x:xs) ?? ys = ys ++ (x:xs) - - -class of 2 equivalent candidates: - - xs ?? ys = ys ++ ys - - [] ?? xs = xs ++ xs - (x:xs) ?? ys = xs ?? ys - - -class of 3 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = [] - - [] ?? xs = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = xs ?? xs - - [] ?? xs = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys ?? ys - - -class of 2 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = xs - - [] ?? xs = xs - (x:xs) ?? [] = xs ?? [] - (x:xs) ?? (y:ys) = xs - - -class of 2 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = ys - - [] ?? xs = xs - (x:xs) ?? [] = xs ?? [] - (x:xs) ?? (y:ys) = ys - - -class of 2 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys - - [] ?? [] = [] - [] ?? (x:xs) = [] ?? xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys - - -class of 5 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = [] - - [] ?? xs = [] - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = xs ?? xs - - [] ?? xs = [] - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys ?? ys - - [] ?? [] = [] - [] ?? (x:xs) = xs ?? xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = [] - - [] ?? [] = [] - [] ?? (x:xs) = [] ?? xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = [] - - -class of 2 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = xs - - [] ?? xs = [] - (x:xs) ?? [] = xs ?? [] - (x:xs) ?? (y:ys) = xs - - -class of 2 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = ys - - [] ?? xs = [] - (x:xs) ?? [] = xs ?? [] - (x:xs) ?? (y:ys) = ys - - -class of 2 equivalent candidates: - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? ys = ys - - [] ?? [] = [] - [] ?? (x:xs) = xs ?? xs - (x:xs) ?? ys = ys - - -class of 6 equivalent candidates: - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? ys = [] - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? ys = xs ?? xs - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? ys = xs ?? [] - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? ys = ys ?? [] - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs ?? xs - (x:xs) ?? (y:ys) = [] - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs ?? [] - (x:xs) ?? (y:ys) = [] - - -class of 2 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? ys = ys ?? xs - - [] ?? xs = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = xs ?? ys - - -class of 3 equivalent candidates: - - xs ?? [] = xs - xs ?? (x:ys) = x:ys - - xs ?? [] = xs - xs ?? (x:ys) = x:ys ?? ys - - xs ?? [] = xs - xs ?? (x:ys) = x:[] ?? ys - - -class of 4 equivalent candidates: - - xs ?? [] = xs ++ xs - xs ?? (x:ys) = [] - - xs ?? [] = xs ++ xs - xs ?? (x:ys) = ys ?? ys - - xs ?? [] = xs ++ xs - xs ?? (x:ys) = [] ?? xs - - xs ?? [] = xs ++ xs - xs ?? (x:ys) = [] ?? ys - - -class of 3 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? ys = x:xs - - [] ?? xs = xs - (x:xs) ?? ys = x:xs ?? xs - - [] ?? xs = xs - (x:xs) ?? ys = x:xs ?? [] - - -class of 4 equivalent candidates: - - [] ?? xs = xs ++ xs - (x:xs) ?? ys = [] - - [] ?? xs = xs ++ xs - (x:xs) ?? ys = xs ?? xs - - [] ?? xs = xs ++ xs - (x:xs) ?? ys = xs ?? [] - - [] ?? xs = xs ++ xs - (x:xs) ?? ys = ys ?? [] - - -class of 3 equivalent candidates: - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = [] - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = xs ?? xs - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys ?? ys - - -class of 2 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = xs ?? ys - - [] ?? xs = [] - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = xs ?? [] - - -class of 2 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys ?? xs - - [] ?? xs = [] - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys ?? [] - - -class of 2 equivalent candidates: - - [] ?? [] = [] - [] ?? (x:xs) = xs ?? xs - (x:xs) ?? ys = xs - - [] ?? [] = [] - [] ?? (x:xs) = xs ?? [] - (x:xs) ?? ys = xs - - -class of 4 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = xs ++ ys - - [] ?? xs = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys ++ xs - - [] ?? xs = xs - (x:xs) ?? ys = xs ++ ys ?? [] - - [] ?? xs = xs - (x:xs) ?? ys = ys ?? [] ++ xs - - -class of 2 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = xs ++ ys - - [] ?? xs = xs - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = ys ++ xs - - -class of 4 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = xs ++ ys - - [] ?? xs = [] - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys ++ xs - - [] ?? xs = [] - (x:xs) ?? ys = xs ++ ys ?? [] - - [] ?? xs = [] - (x:xs) ?? ys = ys ?? [] ++ xs - - -class of 2 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = xs ++ ys - - [] ?? xs = [] - (x:xs) ?? [] = [] - (x:xs) ?? (y:ys) = ys ++ xs - - -class of 2 equivalent candidates: - - xs ?? [] = xs - xs ?? (x:ys) = (x:ys) ?? ys - - xs ?? [] = xs - xs ?? (x:ys) = [x] ?? ys - - -class of 2 equivalent candidates: - - xs ?? [] = xs - xs ?? (x:ys) = (xs ++ ys) ?? ys - - xs ?? [] = xs - xs ?? (x:ys) = xs ++ ys ?? ys - - -class of 2 equivalent candidates: - - xs ?? [] = xs - xs ?? (x:ys) = (ys ++ xs) ?? ys - - xs ?? [] = xs - xs ?? (x:ys) = ys ?? ys ++ xs - - -class of 2 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? (x:xs) - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? [x] - - -class of 2 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? (xs ++ ys) - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? xs ++ ys - - -class of 2 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? (ys ++ xs) - - [] ?? xs = xs - (x:xs) ?? ys = ys ++ xs ?? xs - - -class of 2 equivalent candidates: - - xs ?? [] = xs - xs ?? (x:ys) = x:ys ?? xs - - xs ?? [] = xs - xs ?? (x:ys) = x:(xs ++ ys) - - -class of 2 equivalent candidates: - - xs ?? [] = xs - xs ?? (x:ys) = xs ++ xs ?? ys - - xs ?? [] = xs - xs ?? (x:ys) = xs ?? ys ++ xs - - -class of 2 equivalent candidates: - - xs ?? [] = xs - xs ?? (x:ys) = ys ++ ys ?? xs - - xs ?? [] = xs - xs ?? (x:ys) = ys ?? xs ++ ys - - -class of 2 equivalent candidates: - - xs ?? [] = xs - xs ?? (x:ys) = ys ++ ys ?? ys - - xs ?? [] = xs - xs ?? (x:ys) = ys ++ [] ?? ys - - -class of 2 equivalent candidates: - - xs ?? [] = xs - xs ?? (x:ys) = ys ++ [] ?? xs - - xs ?? [] = xs - xs ?? (x:ys) = [] ?? xs ++ ys - - -class of 2 equivalent candidates: - - xs ?? [] = xs - xs ?? (x:ys) = ys ?? ys ++ ys - - xs ?? [] = xs - xs ?? (x:ys) = [] ?? ys ++ ys - - -class of 2 equivalent candidates: - - xs ?? [] = [] - xs ?? (x:ys) = xs ++ xs ?? ys - - xs ?? [] = [] - xs ?? (x:ys) = xs ?? ys ++ xs - - -class of 3 equivalent candidates: - - xs ?? [] = [] - xs ?? (x:ys) = ys ++ xs ?? ys - - xs ?? [] = [] - xs ?? (x:ys) = ys ++ ys ?? ys - - xs ?? [] = [] - xs ?? (x:ys) = ys ++ [] ?? ys - - -class of 2 equivalent candidates: - - xs ?? [] = [] - xs ?? (x:ys) = ys ++ ys ?? xs - - xs ?? [] = [] - xs ?? (x:ys) = ys ?? xs ++ ys - - -class of 2 equivalent candidates: - - xs ?? [] = [] - xs ?? (x:ys) = ys ++ [] ?? xs - - xs ?? [] = [] - xs ?? (x:ys) = [] ?? xs ++ ys - - -class of 3 equivalent candidates: - - xs ?? [] = [] - xs ?? (x:ys) = xs ?? ys ++ ys - - xs ?? [] = [] - xs ?? (x:ys) = ys ?? ys ++ ys - - xs ?? [] = [] - xs ?? (x:ys) = [] ?? ys ++ ys - - -class of 2 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? ys = x:ys ?? xs - - [] ?? xs = xs - (x:xs) ?? ys = x:(ys ++ xs) - - -class of 2 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? ys = xs ++ xs ?? xs - - [] ?? xs = xs - (x:xs) ?? ys = xs ++ xs ?? [] - - -class of 2 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? ys = xs ++ ys ?? xs - - [] ?? xs = xs - (x:xs) ?? ys = ys ?? xs ++ xs - - -class of 2 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? ys = ys ++ xs ?? ys - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? ys ++ ys - - -class of 2 equivalent candidates: - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? xs ++ xs - - [] ?? xs = xs - (x:xs) ?? ys = xs ?? [] ++ xs - - -class of 3 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? ys = xs ++ xs ?? xs - - [] ?? xs = [] - (x:xs) ?? ys = xs ++ xs ?? ys - - [] ?? xs = [] - (x:xs) ?? ys = xs ++ xs ?? [] - - -class of 2 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? ys = xs ++ ys ?? xs - - [] ?? xs = [] - (x:xs) ?? ys = ys ?? xs ++ xs - - -class of 2 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? ys = ys ++ xs ?? ys - - [] ?? xs = [] - (x:xs) ?? ys = xs ?? ys ++ ys - - -class of 3 equivalent candidates: - - [] ?? xs = [] - (x:xs) ?? ys = xs ?? xs ++ xs - - [] ?? xs = [] - (x:xs) ?? ys = xs ?? ys ++ xs - - [] ?? xs = [] - (x:xs) ?? ys = xs ?? [] ++ xs - - -class of 2 equivalent candidates: - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = xs ?? ys - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys ?? xs - - -class of 2 equivalent candidates: - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = xs ?? [] - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = [] ?? xs - - -class of 2 equivalent candidates: - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys ?? [] - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = [] ?? ys - - -class of 2 equivalent candidates: - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs ?? xs - (x:xs) ?? (y:ys) = xs - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = [] ?? xs - (x:xs) ?? (y:ys) = xs - - -class of 2 equivalent candidates: - - [] ?? [] = [] - [] ?? (x:xs) = xs ?? xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys - - [] ?? [] = [] - [] ?? (x:xs) = xs ?? [] - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys - - -class of 2 equivalent candidates: - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = xs ++ ys - - [] ?? [] = [] - [] ?? (x:xs) = xs - (x:xs) ?? [] = xs - (x:xs) ?? (y:ys) = ys ++ xs - - - -Redundant candidates for: ton :: Bool -> Bool - pruning with 39/49 rules - [3,2,0,0,0,0] candidates - 4/5 unique candidates - 1/5 redundant candidates - -rules: -not False == True -not True == False -p && p == p -p || p == p -not (not p) == p -p && False == False -p && True == p -False && p == False -True && p == p -p || False == p -p || True == True -False || p == p -True || p == True -not (p && q) == not p || not q -not (p && q) == not q || not p -not (p || q) == not p && not q -not (p || q) == not q && not p -p && not p == False -not p && p == False -p || not p == True -not p || p == True -(p && q) && r == p && (q && r) -(p && q) && r == q && (p && r) -(p || q) || r == p || (q || r) -(p || q) || r == q || (p || r) -p && (p && q) == p && q -p && (q && p) == p && q -p && (q && p) == q && p -p || (p || q) == p || q -p || (q || p) == p || q -p || (q || p) == q || p -p && (p || q) == p -p && (q || p) == p -(p || q) && p == p -(p || q) && q == q -p || p && q == p -p || q && p == p -p && q || p == p -p && q || q == q -equations: -q && p == p && q -q || p == p || q -q && (p && r) == p && (q && r) -r && (p && q) == p && (q && r) -r && (q && p) == p && (q && r) -q || (p || r) == p || (q || r) -r || (p || q) == p || (q || r) -r || (q || p) == p || (q || r) -(r || q) && p == p && (q || r) -r && q || p == p || q && r - -class of 2 equivalent candidates: - - ton p = not p - - ton False = True - ton True = False - - - -Redundant candidates for: &| :: Bool -> Bool -> Bool - pruning with 39/49 rules - [4,12,20,6,2,16] candidates - 16/60 unique candidates - 44/60 redundant candidates - -rules: -not False == True -not True == False -p && p == p -p || p == p -not (not p) == p -p && False == False -p && True == p -False && p == False -True && p == p -p || False == p -p || True == True -False || p == p -True || p == True -not (p && q) == not p || not q -not (p && q) == not q || not p -not (p || q) == not p && not q -not (p || q) == not q && not p -p && not p == False -not p && p == False -p || not p == True -not p || p == True -(p && q) && r == p && (q && r) -(p && q) && r == q && (p && r) -(p || q) || r == p || (q || r) -(p || q) || r == q || (p || r) -p && (p && q) == p && q -p && (q && p) == p && q -p && (q && p) == q && p -p || (p || q) == p || q -p || (q || p) == p || q -p || (q || p) == q || p -p && (p || q) == p -p && (q || p) == p -(p || q) && p == p -(p || q) && q == q -p || p && q == p -p || q && p == p -p && q || p == p -p && q || q == q -equations: -q && p == p && q -q || p == p || q -q && (p && r) == p && (q && r) -r && (p && q) == p && (q && r) -r && (q && p) == p && (q && r) -q || (p || r) == p || (q || r) -r || (p || q) == p || (q || r) -r || (q || p) == p || (q || r) -(r || q) && p == p && (q || r) -r && q || p == p || q && r - -class of 5 equivalent candidates: - - p &| q = False - - p &| q = p && (q && not p) - - p &| q = q && (p && not q) - - p &| q = not p && (p && q) - - p &| q = not q && (p && q) - - -class of 5 equivalent candidates: - - p &| q = True - - p &| q = p || (q || not p) - - p &| q = q || (p || not q) - - p &| q = not p || (p || q) - - p &| q = not q || (p || q) - - -class of 2 equivalent candidates: - - p &| q = not p - - False &| p = True - True &| p = False - - -class of 4 equivalent candidates: - - p &| q = not q - - p &| False = True - p &| True = False - - False &| p = not p - True &| False = True - True &| True = False - - False &| False = True - False &| True = False - True &| p = not p - - -class of 5 equivalent candidates: - - p &| False = p - p &| True = False - - False &| p = False - True &| p = not p - - False &| p = False - True &| False = True - True &| True = False - - p &| q = p && not q - - p &| q = not q && (p || q) - - -class of 5 equivalent candidates: - - p &| False = p - p &| True = True - - False &| p = p - True &| p = True - - p &| q = p || q - - p &| q = p || q && not p - - p &| q = q || p && not q - - -class of 5 equivalent candidates: - - p &| False = False - p &| True = p - - False &| p = False - True &| p = p - - p &| q = p && q - - p &| q = p && (q || not p) - - p &| q = q && (p || not q) - - -class of 5 equivalent candidates: - - p &| False = True - p &| True = p - - False &| p = not p - True &| p = True - - False &| False = True - False &| True = False - True &| p = True - - p &| q = p || not q - - p &| q = not q || p && q - - -class of 4 equivalent candidates: - - False &| p = p - True &| p = False - - p &| False = False - p &| True = not p - - p &| q = q && not p - - p &| q = not p && (p || q) - - -class of 4 equivalent candidates: - - False &| p = True - True &| p = p - - p &| False = not p - p &| True = True - - p &| q = q || not p - - p &| q = not p || p && q + pruning with 27/65 rules + [3,3,9,10,32,39] candidates + 86/96 unique candidates + 10/96 redundant candidates + +rules: +x - x == 0 +x * 0 == 0 +x * 1 == x +0 * x == 0 +1 * x == x +x + 0 == x +0 + x == x +x - 0 == x +(x * y) * z == x * (y * z) +(x * y) * z == y * (x * z) +(x + y) + z == x + (y + z) +(x + y) + z == y + (x + z) +x - (y - z) == z + (x - y) +(x - y) - z == x - (y + z) +(x - y) - z == x - (z + y) +(x + y) - z == x + (y - z) +(x + y) - z == y + (x - z) +(x + x) * y == x * (y + y) +x + (y - x) == y +(x - y) + y == x +x * y - x == x * (y - 1) +x * y - y == y * (x - 1) +x * (y + 1) == x + x * y +x * (y + 1) == x * y + x +(x + 1) * y == y + x * y +0 - x * y == x * (0 - y) +0 - x * y == y * (0 - x) +equations: +y * x == x * y +y + x == x + y +y * (x * z) == x * (y * z) +z * (x * y) == x * (y * z) +z * (y * x) == x * (y * z) +y + (x + z) == x + (y + z) +z + (x + y) == x + (y + z) +z + (y + x) == x + (y + z) +(z + y) * x == x * (y + z) +y + (x - z) == x + (y - z) +z * y + x == x + y * z +(x - z) + y == x + (y - z) +(z - y) + x == (x - y) + z +y * (x + x) == x * (y + y) +y - (x + y) == 0 - x +y - (y + x) == 0 - x +z - (y + z) == x - (x + y) +z - (y + z) == x - (y + x) +z - (z + y) == x - (x + y) +z - (z + y) == x - (y + x) +x * (1 - y) == x - x * y +x * (1 - y) == x - y * x +y * (0 - x) == x * (0 - y) +(0 - x) * y == x * (0 - y) +(0 - y) * x == (0 - x) * y +(1 - y) * x == x - x * y +(1 - y) * x == x - y * x +x + (0 - y) == x - y +(0 - y) + x == x - y +x - (x + 1) == 0 - 1 +x - (1 + x) == 0 - 1 +y - (y + 1) == x - (x + 1) +y - (y + 1) == x - (1 + x) +y - (1 + y) == x - (1 + x) +x * (0 - 1) == 0 - x +(0 - 1) * x == 0 - x +(0 - 1) * y == x - (x + y) +(0 - 1) * y == x - (y + x) + +class of 3 equivalent candidates: + + foo x = 0 - x + + foo x = x - (x + x) + + foo x = 1 - (x + 1) + + +class of 2 equivalent candidates: + + foo x = 1 - x + + foo x = 1 + (0 - x) + + +class of 2 equivalent candidates: + + foo 0 = 0 + foo x = 1 - x + + foo 0 = 0 + foo x = 1 + (0 - x) + + +class of 3 equivalent candidates: + + foo 0 = 1 + foo x = 0 - x + + foo 0 = 1 + foo x = x - (x + x) + + foo 0 = 1 + foo x = 1 - (x + 1) + + +class of 2 equivalent candidates: + + foo x = x + (x + 1) + + foo x = 1 + (x + x) + + +class of 2 equivalent candidates: + + foo x = x * (1 - x) + + foo x = x - x * x + + +class of 2 equivalent candidates: + + foo 0 = 0 + foo x = x + (x + 1) + + foo 0 = 0 + foo x = 1 + (x + x) + + +class of 2 equivalent candidates: + + foo 0 = 1 + foo x = x * (1 - x) + + foo 0 = 1 + foo x = x - x * x + + + +Redundant candidates for: ? :: Int -> Int -> Int + pruning with 13/34 rules + [3,8,25,71,205] candidates + 294/312 unique candidates + 18/312 redundant candidates + +rules: +x * 0 == 0 +0 * x == 0 +x + 0 == x +0 + x == x +dec (x + y) == x + dec y +dec (x + y) == y + dec x +dec (x + y) == dec x + y +dec (x + y) == dec y + x +(x * y) * z == x * (y * z) +(x * y) * z == y * (x * z) +(x + y) + z == x + (y + z) +(x + y) + z == y + (x + z) +(x + x) * y == x * (y + y) +equations: +y * x == x * y +y + x == x + y +y + dec x == x + dec y +dec x + y == x + dec y +dec y + x == dec x + y +x + dec 0 == dec x +dec 0 + x == dec x +y * (x * z) == x * (y * z) +z * (x * y) == x * (y * z) +z * (y * x) == x * (y * z) +y + (x + z) == x + (y + z) +z + (x + y) == x + (y + z) +z + (y + x) == x + (y + z) +(z + y) * x == x * (y + z) +z * y + x == x + y * z +y * (x + x) == x * (y + y) +y + dec (dec x) == x + dec (dec y) +dec (dec x) + y == x + dec (dec y) +dec (dec y) + x == dec (dec x) + y +x + dec (dec 0) == dec (dec x) +dec (dec 0) + x == dec (dec x) + +class of 2 equivalent candidates: + + x ? y = x + + x ? 0 = x + x ? y = x ? dec y + + +class of 2 equivalent candidates: + + x ? y = y + + 0 ? x = x + x ? y = dec x ? y + + +class of 2 equivalent candidates: + + x ? 0 = x + x ? y = 0 + + x ? 0 = x + x ? y = 0 ? dec y + + +class of 2 equivalent candidates: + + 0 ? x = x + x ? y = 0 + + 0 ? x = x + x ? y = dec x ? 0 + + +class of 2 equivalent candidates: + + x ? y = x + dec y + + x ? y = y + dec x + + +class of 2 equivalent candidates: + + x ? y = x + (x + y) + + x ? y = y + (x + x) + + +class of 2 equivalent candidates: + + x ? y = x + (y + y) + + x ? y = y + (x + y) + + +class of 2 equivalent candidates: + + x ? y = x + dec (dec x) + + x ? y = dec x + dec x + + +class of 3 equivalent candidates: + + x ? y = x + dec (dec y) + + x ? y = y + dec (dec x) + + x ? y = dec x + dec y + + +class of 2 equivalent candidates: + + x ? y = y + dec (dec y) + + x ? y = dec y + dec y + + +class of 2 equivalent candidates: + + x ? y = x * (y + y) + + x ? y = y * (x + x) + + +class of 2 equivalent candidates: + + x ? y = x * (x * y) + + x ? y = y * (x * x) + + +class of 2 equivalent candidates: + + x ? y = x * (y * y) + + x ? y = y * (x * y) + + +class of 2 equivalent candidates: + + x ? 0 = x + x ? y = x + dec y + + x ? 0 = x + x ? y = y + dec x + + +class of 2 equivalent candidates: + + x ? 0 = 0 + x ? y = x + dec y + + x ? 0 = 0 + x ? y = y + dec x + + +class of 2 equivalent candidates: + + 0 ? x = x + x ? y = x + dec y + + 0 ? x = x + x ? y = y + dec x + + +class of 2 equivalent candidates: + + 0 ? x = 0 + x ? y = x + dec y + + 0 ? x = 0 + x ? y = y + dec x + + + +Redundant candidates for: goo :: [Int] -> [Int] + pruning with 4/4 rules + [2,1,1,2,4,7] candidates + 15/17 unique candidates + 2/17 redundant candidates + +rules: +xs ++ [] == xs +[] ++ xs == xs +(xs ++ ys) ++ zs == xs ++ (ys ++ zs) +(x:xs) ++ ys == x:(xs ++ ys) + +class of 2 equivalent candidates: + + goo xs = xs + + goo [] = [] + goo (x:xs) = x:goo xs + + +class of 2 equivalent candidates: + + goo xs = [] + + goo [] = [] + goo (x:xs) = goo xs ++ goo xs + + + +Redundant candidates for: ?? :: [Int] -> [Int] -> [Int] + pruning with 4/4 rules + [3,8,15,43,122] candidates + 150/191 unique candidates + 41/191 redundant candidates + +rules: +xs ++ [] == xs +[] ++ xs == xs +(xs ++ ys) ++ zs == xs ++ (ys ++ zs) +(x:xs) ++ ys == x:(xs ++ ys) + +class of 2 equivalent candidates: + + xs ?? ys = xs + + xs ?? [] = xs + xs ?? (x:ys) = xs ?? ys + + +class of 2 equivalent candidates: + + xs ?? ys = ys + + [] ?? xs = xs + (x:xs) ?? ys = xs ?? ys + + +class of 5 equivalent candidates: + + xs ?? [] = xs + xs ?? (x:ys) = [] + + xs ?? [] = xs + xs ?? (x:ys) = ys ?? ys + + xs ?? [] = xs + xs ?? (x:ys) = [] ?? xs + + xs ?? [] = xs + xs ?? (x:ys) = [] ?? ys + + [] ?? xs = [] + (x:xs) ?? [] = x:xs + (x:xs) ?? (y:ys) = [] + + +class of 2 equivalent candidates: + + xs ?? [] = [] + xs ?? (x:ys) = xs + + [] ?? xs = [] + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = x:xs + + +class of 3 equivalent candidates: + + xs ?? [] = [] + xs ?? (x:ys) = ys + + [] ?? [] = [] + [] ?? (x:xs) = xs + (x:xs) ?? ys = xs ?? ys + + [] ?? [] = [] + [] ?? (x:xs) = xs + (x:xs) ?? ys = [] ?? ys + + +class of 10 equivalent candidates: + + [] ?? xs = xs + (x:xs) ?? ys = [] + + [] ?? xs = xs + (x:xs) ?? ys = xs ?? xs + + [] ?? xs = xs + (x:xs) ?? ys = xs ?? [] + + [] ?? xs = xs + (x:xs) ?? ys = ys ?? [] + + [] ?? xs = xs + (x:xs) ?? [] = xs ?? xs + (x:xs) ?? (y:ys) = [] + + [] ?? xs = xs + (x:xs) ?? [] = xs ?? [] + (x:xs) ?? (y:ys) = [] + + [] ?? xs = xs + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = xs ?? xs + + [] ?? xs = xs + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = xs ?? [] + + [] ?? xs = xs + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = ys ?? ys + + [] ?? xs = xs + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = ys ?? [] + + +class of 2 equivalent candidates: + + [] ?? xs = [] + (x:xs) ?? ys = xs + + [] ?? [] = [] + [] ?? (x:xs) = [] ?? xs + (x:xs) ?? ys = xs + + +class of 3 equivalent candidates: + + [] ?? xs = [] + (x:xs) ?? ys = ys + + [] ?? [] = [] + [] ?? (x:xs) = xs ?? [] + (x:xs) ?? ys = ys + + [] ?? [] = [] + [] ?? (x:xs) = [] ?? xs + (x:xs) ?? ys = ys + + +class of 3 equivalent candidates: + + [] ?? xs = xs + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = [] + + [] ?? xs = xs + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = xs ?? xs + + [] ?? xs = xs + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = ys ?? ys + + +class of 2 equivalent candidates: + + [] ?? xs = xs + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = xs + + [] ?? xs = xs + (x:xs) ?? [] = xs ?? [] + (x:xs) ?? (y:ys) = xs + + +class of 2 equivalent candidates: + + [] ?? xs = xs + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = ys + + [] ?? xs = xs + (x:xs) ?? [] = xs ?? [] + (x:xs) ?? (y:ys) = ys + + +class of 3 equivalent candidates: + + [] ?? xs = [] + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = [] + + [] ?? xs = [] + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = xs ?? xs + + [] ?? xs = [] + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = ys ?? ys + + +class of 2 equivalent candidates: + + [] ?? xs = [] + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = xs + + [] ?? xs = [] + (x:xs) ?? [] = xs ?? [] + (x:xs) ?? (y:ys) = xs + + +class of 2 equivalent candidates: + + [] ?? xs = [] + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = ys + + [] ?? xs = [] + (x:xs) ?? [] = xs ?? [] + (x:xs) ?? (y:ys) = ys + + +class of 2 equivalent candidates: + + [] ?? [] = [] + [] ?? (x:xs) = xs + (x:xs) ?? ys = ys + + [] ?? [] = [] + [] ?? (x:xs) = xs ?? xs + (x:xs) ?? ys = ys + + +class of 4 equivalent candidates: + + [] ?? [] = [] + [] ?? (x:xs) = xs + (x:xs) ?? ys = [] + + [] ?? [] = [] + [] ?? (x:xs) = xs + (x:xs) ?? ys = xs ?? xs + + [] ?? [] = [] + [] ?? (x:xs) = xs + (x:xs) ?? ys = xs ?? [] + + [] ?? [] = [] + [] ?? (x:xs) = xs + (x:xs) ?? ys = ys ?? [] + + +class of 2 equivalent candidates: + + [] ?? xs = xs + (x:xs) ?? ys = ys ?? xs + + [] ?? xs = xs + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = xs ?? ys + + +class of 2 equivalent candidates: + + [] ?? xs = [] + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = xs ?? ys + + [] ?? xs = [] + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = xs ?? [] + + +class of 2 equivalent candidates: + + [] ?? xs = [] + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = ys ?? xs + + [] ?? xs = [] + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = ys ?? [] + + +class of 2 equivalent candidates: + + [] ?? [] = [] + [] ?? (x:xs) = xs ?? xs + (x:xs) ?? ys = xs + + [] ?? [] = [] + [] ?? (x:xs) = xs ?? [] + (x:xs) ?? ys = xs + + +class of 2 equivalent candidates: + + [] ?? xs = xs + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = xs ++ ys + + [] ?? xs = xs + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = ys ++ xs + + +class of 2 equivalent candidates: + + [] ?? xs = xs + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = xs ++ ys + + [] ?? xs = xs + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = ys ++ xs + + +class of 2 equivalent candidates: + + [] ?? xs = [] + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = xs ++ ys + + [] ?? xs = [] + (x:xs) ?? [] = xs + (x:xs) ?? (y:ys) = ys ++ xs + + +class of 2 equivalent candidates: + + [] ?? xs = [] + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = xs ++ ys + + [] ?? xs = [] + (x:xs) ?? [] = [] + (x:xs) ?? (y:ys) = ys ++ xs + + + +Redundant candidates for: ton :: Bool -> Bool + pruning with 39/49 rules + [3,2,0,0,0,0] candidates + 4/5 unique candidates + 1/5 redundant candidates + +rules: +not False == True +not True == False +p && p == p +p || p == p +not (not p) == p +p && False == False +p && True == p +False && p == False +True && p == p +p || False == p +p || True == True +False || p == p +True || p == True +not (p && q) == not p || not q +not (p && q) == not q || not p +not (p || q) == not p && not q +not (p || q) == not q && not p +p && not p == False +not p && p == False +p || not p == True +not p || p == True +(p && q) && r == p && (q && r) +(p && q) && r == q && (p && r) +(p || q) || r == p || (q || r) +(p || q) || r == q || (p || r) +p && (p && q) == p && q +p && (q && p) == p && q +p && (q && p) == q && p +p || (p || q) == p || q +p || (q || p) == p || q +p || (q || p) == q || p +p && (p || q) == p +p && (q || p) == p +(p || q) && p == p +(p || q) && q == q +p || p && q == p +p || q && p == p +p && q || p == p +p && q || q == q +equations: +q && p == p && q +q || p == p || q +q && (p && r) == p && (q && r) +r && (p && q) == p && (q && r) +r && (q && p) == p && (q && r) +q || (p || r) == p || (q || r) +r || (p || q) == p || (q || r) +r || (q || p) == p || (q || r) +(r || q) && p == p && (q || r) +r && q || p == p || q && r + +class of 2 equivalent candidates: + + ton p = not p + + ton False = True + ton True = False + + + +Redundant candidates for: &| :: Bool -> Bool -> Bool + pruning with 39/49 rules + [4,12,20,6,2] candidates + 16/44 unique candidates + 28/44 redundant candidates + +rules: +not False == True +not True == False +p && p == p +p || p == p +not (not p) == p +p && False == False +p && True == p +False && p == False +True && p == p +p || False == p +p || True == True +False || p == p +True || p == True +not (p && q) == not p || not q +not (p && q) == not q || not p +not (p || q) == not p && not q +not (p || q) == not q && not p +p && not p == False +not p && p == False +p || not p == True +not p || p == True +(p && q) && r == p && (q && r) +(p && q) && r == q && (p && r) +(p || q) || r == p || (q || r) +(p || q) || r == q || (p || r) +p && (p && q) == p && q +p && (q && p) == p && q +p && (q && p) == q && p +p || (p || q) == p || q +p || (q || p) == p || q +p || (q || p) == q || p +p && (p || q) == p +p && (q || p) == p +(p || q) && p == p +(p || q) && q == q +p || p && q == p +p || q && p == p +p && q || p == p +p && q || q == q +equations: +q && p == p && q +q || p == p || q +q && (p && r) == p && (q && r) +r && (p && q) == p && (q && r) +r && (q && p) == p && (q && r) +q || (p || r) == p || (q || r) +r || (p || q) == p || (q || r) +r || (q || p) == p || (q || r) +(r || q) && p == p && (q || r) +r && q || p == p || q && r + +class of 2 equivalent candidates: + + p &| q = not p + + False &| p = True + True &| p = False + + +class of 4 equivalent candidates: + + p &| q = not q + + p &| False = True + p &| True = False + + False &| p = not p + True &| False = True + True &| True = False + + False &| False = True + False &| True = False + True &| p = not p + + +class of 4 equivalent candidates: + + p &| False = p + p &| True = False + + False &| p = False + True &| p = not p + + False &| p = False + True &| False = True + True &| True = False + + p &| q = p && not q + + +class of 3 equivalent candidates: + + p &| False = p + p &| True = True + + False &| p = p + True &| p = True + + p &| q = p || q + + +class of 3 equivalent candidates: + + p &| False = False + p &| True = p + + False &| p = False + True &| p = p + + p &| q = p && q + + +class of 4 equivalent candidates: + + p &| False = True + p &| True = p + + False &| p = not p + True &| p = True + + False &| False = True + False &| True = False + True &| p = True + + p &| q = p || not q + + +class of 3 equivalent candidates: + + False &| p = p + True &| p = False + + p &| False = False + p &| True = not p + + p &| q = q && not p + + +class of 3 equivalent candidates: + + False &| p = True + True &| p = p + + p &| False = not p + p &| True = True + + p &| q = q || not p class of 3 equivalent candidates: diff --git a/bench/runtime/lapmatrud/bench/candidates.runtime b/bench/runtime/lapmatrud/bench/candidates.runtime --- a/bench/runtime/lapmatrud/bench/candidates.runtime +++ b/bench/runtime/lapmatrud/bench/candidates.runtime @@ -1,1 +1,1 @@ -5.5 +10.8 diff --git a/bench/runtime/lapmatrud/bench/erroneous.runtime b/bench/runtime/lapmatrud/bench/erroneous.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/lapmatrud/bench/erroneous.runtime @@ -0,0 +1,1 @@ +3.2 diff --git a/bench/runtime/lapmatrud/bench/gps2.runtime b/bench/runtime/lapmatrud/bench/gps2.runtime --- a/bench/runtime/lapmatrud/bench/gps2.runtime +++ b/bench/runtime/lapmatrud/bench/gps2.runtime @@ -1,1 +1,1 @@ -13.1 +14.3 diff --git a/bench/runtime/lapmatrud/bench/ill-hit.runtime b/bench/runtime/lapmatrud/bench/ill-hit.runtime --- a/bench/runtime/lapmatrud/bench/ill-hit.runtime +++ b/bench/runtime/lapmatrud/bench/ill-hit.runtime @@ -1,1 +1,1 @@ -0.4 +0.5 diff --git a/bench/runtime/lapmatrud/bench/p12.runtime b/bench/runtime/lapmatrud/bench/p12.runtime --- a/bench/runtime/lapmatrud/bench/p12.runtime +++ b/bench/runtime/lapmatrud/bench/p12.runtime @@ -1,1 +1,1 @@ -1.7 +1.8 diff --git a/bench/runtime/lapmatrud/bench/redundants.runtime b/bench/runtime/lapmatrud/bench/redundants.runtime --- a/bench/runtime/lapmatrud/bench/redundants.runtime +++ b/bench/runtime/lapmatrud/bench/redundants.runtime @@ -1,1 +1,1 @@ -3.9 +3.2 diff --git a/bench/runtime/lapmatrud/bench/terpret.runtime b/bench/runtime/lapmatrud/bench/terpret.runtime --- a/bench/runtime/lapmatrud/bench/terpret.runtime +++ b/bench/runtime/lapmatrud/bench/terpret.runtime @@ -1,1 +1,1 @@ -8.3 +9.2 diff --git a/bench/runtime/lapmatrud/bench/weird.runtime b/bench/runtime/lapmatrud/bench/weird.runtime --- a/bench/runtime/lapmatrud/bench/weird.runtime +++ b/bench/runtime/lapmatrud/bench/weird.runtime @@ -1,1 +1,1 @@ -3.1 +3.3 diff --git a/bench/runtime/lapmatrud/eg/arith.runtime b/bench/runtime/lapmatrud/eg/arith.runtime --- a/bench/runtime/lapmatrud/eg/arith.runtime +++ b/bench/runtime/lapmatrud/eg/arith.runtime @@ -1,1 +1,1 @@ -0.9 +1.0 diff --git a/bench/runtime/lapmatrud/eg/bools.runtime b/bench/runtime/lapmatrud/eg/bools.runtime --- a/bench/runtime/lapmatrud/eg/bools.runtime +++ b/bench/runtime/lapmatrud/eg/bools.runtime @@ -1,1 +1,1 @@ -1.6 +2.1 diff --git a/bench/runtime/lapmatrud/eg/dupos.runtime b/bench/runtime/lapmatrud/eg/dupos.runtime --- a/bench/runtime/lapmatrud/eg/dupos.runtime +++ b/bench/runtime/lapmatrud/eg/dupos.runtime @@ -1,1 +1,1 @@ -3.3 +3.5 diff --git a/bench/runtime/lapmatrud/eg/either.runtime b/bench/runtime/lapmatrud/eg/either.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/lapmatrud/eg/either.runtime @@ -0,0 +1,1 @@ +0.1 diff --git a/bench/runtime/lapmatrud/eg/factorial.runtime b/bench/runtime/lapmatrud/eg/factorial.runtime --- a/bench/runtime/lapmatrud/eg/factorial.runtime +++ b/bench/runtime/lapmatrud/eg/factorial.runtime @@ -1,1 +1,1 @@ -1.2 +1.3 diff --git a/bench/runtime/lapmatrud/eg/fib01.runtime b/bench/runtime/lapmatrud/eg/fib01.runtime --- a/bench/runtime/lapmatrud/eg/fib01.runtime +++ b/bench/runtime/lapmatrud/eg/fib01.runtime @@ -1,1 +1,1 @@ -1.2 +1.5 diff --git a/bench/runtime/lapmatrud/eg/fibonacci.runtime b/bench/runtime/lapmatrud/eg/fibonacci.runtime --- a/bench/runtime/lapmatrud/eg/fibonacci.runtime +++ b/bench/runtime/lapmatrud/eg/fibonacci.runtime @@ -1,1 +1,1 @@ -4.2 +15.5 diff --git a/bench/runtime/lapmatrud/eg/higher.runtime b/bench/runtime/lapmatrud/eg/higher.runtime --- a/bench/runtime/lapmatrud/eg/higher.runtime +++ b/bench/runtime/lapmatrud/eg/higher.runtime @@ -1,1 +1,1 @@ -0.6 +0.7 diff --git a/bench/runtime/lapmatrud/eg/ints.runtime b/bench/runtime/lapmatrud/eg/ints.runtime --- a/bench/runtime/lapmatrud/eg/ints.runtime +++ b/bench/runtime/lapmatrud/eg/ints.runtime @@ -1,1 +1,1 @@ -0.5 +0.6 diff --git a/bench/runtime/lapmatrud/eg/list.runtime b/bench/runtime/lapmatrud/eg/list.runtime --- a/bench/runtime/lapmatrud/eg/list.runtime +++ b/bench/runtime/lapmatrud/eg/list.runtime @@ -1,1 +1,1 @@ -1.0 +1.2 diff --git a/bench/runtime/lapmatrud/eg/maybe.runtime b/bench/runtime/lapmatrud/eg/maybe.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/lapmatrud/eg/maybe.runtime @@ -0,0 +1,1 @@ +0.3 diff --git a/bench/runtime/lapmatrud/eg/oddeven.runtime b/bench/runtime/lapmatrud/eg/oddeven.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/lapmatrud/eg/oddeven.runtime @@ -0,0 +1,1 @@ +2.1 diff --git a/bench/runtime/lapmatrud/eg/pow.runtime b/bench/runtime/lapmatrud/eg/pow.runtime --- a/bench/runtime/lapmatrud/eg/pow.runtime +++ b/bench/runtime/lapmatrud/eg/pow.runtime @@ -1,1 +1,1 @@ -3.8 +4.4 diff --git a/bench/runtime/lapmatrud/eg/setelem.runtime b/bench/runtime/lapmatrud/eg/setelem.runtime --- a/bench/runtime/lapmatrud/eg/setelem.runtime +++ b/bench/runtime/lapmatrud/eg/setelem.runtime @@ -1,1 +1,1 @@ -1.1 +1.3 diff --git a/bench/runtime/lapmatrud/eg/sort.runtime b/bench/runtime/lapmatrud/eg/sort.runtime --- a/bench/runtime/lapmatrud/eg/sort.runtime +++ b/bench/runtime/lapmatrud/eg/sort.runtime @@ -1,1 +1,1 @@ -1.2 +1.4 diff --git a/bench/runtime/lapmatrud/eg/spec.runtime b/bench/runtime/lapmatrud/eg/spec.runtime --- a/bench/runtime/lapmatrud/eg/spec.runtime +++ b/bench/runtime/lapmatrud/eg/spec.runtime @@ -1,1 +1,1 @@ -0.5 +0.6 diff --git a/bench/runtime/lapmatrud/eg/subset.runtime b/bench/runtime/lapmatrud/eg/subset.runtime --- a/bench/runtime/lapmatrud/eg/subset.runtime +++ b/bench/runtime/lapmatrud/eg/subset.runtime @@ -1,1 +1,1 @@ -0.4 +0.5 diff --git a/bench/runtime/lapmatrud/eg/tapps.runtime b/bench/runtime/lapmatrud/eg/tapps.runtime --- a/bench/runtime/lapmatrud/eg/tapps.runtime +++ b/bench/runtime/lapmatrud/eg/tapps.runtime @@ -1,1 +1,1 @@ -0.4 +0.5 diff --git a/bench/runtime/lapmatrud/eg/tree.runtime b/bench/runtime/lapmatrud/eg/tree.runtime --- a/bench/runtime/lapmatrud/eg/tree.runtime +++ b/bench/runtime/lapmatrud/eg/tree.runtime @@ -1,1 +1,1 @@ -1.5 +1.4 diff --git a/bench/runtime/lapmatrud/versions b/bench/runtime/lapmatrud/versions --- a/bench/runtime/lapmatrud/versions +++ b/bench/runtime/lapmatrud/versions @@ -1,4 +1,4 @@ GHC 9.0.2 leancheck-1.0.2 -express-1.0.14 -speculate-0.4.14 +express-1.0.16 +speculate-0.4.18 diff --git a/bench/runtime/zero/bench/candidates.runtime b/bench/runtime/zero/bench/candidates.runtime --- a/bench/runtime/zero/bench/candidates.runtime +++ b/bench/runtime/zero/bench/candidates.runtime @@ -1,1 +1,1 @@ -9.7 +17.3 diff --git a/bench/runtime/zero/bench/erroneous.runtime b/bench/runtime/zero/bench/erroneous.runtime --- a/bench/runtime/zero/bench/erroneous.runtime +++ b/bench/runtime/zero/bench/erroneous.runtime @@ -1,1 +1,1 @@ -3.7 +6.4 diff --git a/bench/runtime/zero/bench/gps.runtime b/bench/runtime/zero/bench/gps.runtime --- a/bench/runtime/zero/bench/gps.runtime +++ b/bench/runtime/zero/bench/gps.runtime @@ -1,1 +1,1 @@ -28.5 +28.9 diff --git a/bench/runtime/zero/bench/gps2.runtime b/bench/runtime/zero/bench/gps2.runtime --- a/bench/runtime/zero/bench/gps2.runtime +++ b/bench/runtime/zero/bench/gps2.runtime @@ -1,1 +1,1 @@ -26.1 +24.4 diff --git a/bench/runtime/zero/bench/ill-hit.runtime b/bench/runtime/zero/bench/ill-hit.runtime --- a/bench/runtime/zero/bench/ill-hit.runtime +++ b/bench/runtime/zero/bench/ill-hit.runtime @@ -1,1 +1,1 @@ -0.8 +0.9 diff --git a/bench/runtime/zero/bench/p12.runtime b/bench/runtime/zero/bench/p12.runtime --- a/bench/runtime/zero/bench/p12.runtime +++ b/bench/runtime/zero/bench/p12.runtime @@ -1,1 +1,1 @@ -3.8 +3.3 diff --git a/bench/runtime/zero/bench/redundants.runtime b/bench/runtime/zero/bench/redundants.runtime --- a/bench/runtime/zero/bench/redundants.runtime +++ b/bench/runtime/zero/bench/redundants.runtime @@ -1,1 +1,1 @@ -14.9 +8.1 diff --git a/bench/runtime/zero/bench/terpret.runtime b/bench/runtime/zero/bench/terpret.runtime --- a/bench/runtime/zero/bench/terpret.runtime +++ b/bench/runtime/zero/bench/terpret.runtime @@ -1,1 +1,1 @@ -14.8 +14.5 diff --git a/bench/runtime/zero/bench/weird.runtime b/bench/runtime/zero/bench/weird.runtime --- a/bench/runtime/zero/bench/weird.runtime +++ b/bench/runtime/zero/bench/weird.runtime @@ -1,1 +1,1 @@ -5.4 +6.3 diff --git a/bench/runtime/zero/eg/bst.runtime b/bench/runtime/zero/eg/bst.runtime --- a/bench/runtime/zero/eg/bst.runtime +++ b/bench/runtime/zero/eg/bst.runtime @@ -1,1 +1,1 @@ -13.8 +14.0 diff --git a/bench/runtime/zero/eg/count.runtime b/bench/runtime/zero/eg/count.runtime --- a/bench/runtime/zero/eg/count.runtime +++ b/bench/runtime/zero/eg/count.runtime @@ -1,1 +1,1 @@ -0.6 +0.7 diff --git a/bench/runtime/zero/eg/dupos.runtime b/bench/runtime/zero/eg/dupos.runtime --- a/bench/runtime/zero/eg/dupos.runtime +++ b/bench/runtime/zero/eg/dupos.runtime @@ -1,1 +1,1 @@ -6.5 +6.9 diff --git a/bench/runtime/zero/eg/either.runtime b/bench/runtime/zero/eg/either.runtime --- a/bench/runtime/zero/eg/either.runtime +++ b/bench/runtime/zero/eg/either.runtime @@ -1,1 +1,1 @@ -0.2 +0.3 diff --git a/bench/runtime/zero/eg/fibonacci.runtime b/bench/runtime/zero/eg/fibonacci.runtime --- a/bench/runtime/zero/eg/fibonacci.runtime +++ b/bench/runtime/zero/eg/fibonacci.runtime @@ -1,1 +1,1 @@ -9.1 +8.1 diff --git a/bench/runtime/zero/eg/list.runtime b/bench/runtime/zero/eg/list.runtime --- a/bench/runtime/zero/eg/list.runtime +++ b/bench/runtime/zero/eg/list.runtime @@ -1,1 +1,1 @@ -2.0 +2.4 diff --git a/bench/runtime/zero/eg/oddeven.runtime b/bench/runtime/zero/eg/oddeven.runtime --- a/bench/runtime/zero/eg/oddeven.runtime +++ b/bench/runtime/zero/eg/oddeven.runtime @@ -1,1 +1,1 @@ -2.8 +2.7 diff --git a/bench/runtime/zero/eg/pow.runtime b/bench/runtime/zero/eg/pow.runtime --- a/bench/runtime/zero/eg/pow.runtime +++ b/bench/runtime/zero/eg/pow.runtime @@ -1,1 +1,1 @@ -7.4 +8.6 diff --git a/bench/runtime/zero/eg/replicate.runtime b/bench/runtime/zero/eg/replicate.runtime --- a/bench/runtime/zero/eg/replicate.runtime +++ b/bench/runtime/zero/eg/replicate.runtime @@ -1,1 +1,1 @@ -0.5 +0.6 diff --git a/bench/runtime/zero/eg/sort.runtime b/bench/runtime/zero/eg/sort.runtime --- a/bench/runtime/zero/eg/sort.runtime +++ b/bench/runtime/zero/eg/sort.runtime @@ -1,1 +1,1 @@ -2.7 +2.4 diff --git a/bench/runtime/zero/eg/spec.runtime b/bench/runtime/zero/eg/spec.runtime --- a/bench/runtime/zero/eg/spec.runtime +++ b/bench/runtime/zero/eg/spec.runtime @@ -1,1 +1,1 @@ -1.1 +1.3 diff --git a/bench/runtime/zero/eg/tree.runtime b/bench/runtime/zero/eg/tree.runtime --- a/bench/runtime/zero/eg/tree.runtime +++ b/bench/runtime/zero/eg/tree.runtime @@ -1,1 +1,1 @@ -2.2 +2.3 diff --git a/bench/runtime/zero/versions b/bench/runtime/zero/versions --- a/bench/runtime/zero/versions +++ b/bench/runtime/zero/versions @@ -1,4 +1,4 @@ GHC 9.0.2 leancheck-1.0.2 express-1.0.16 -speculate-0.4.14 +speculate-0.4.20 diff --git a/bench/weird.hs b/bench/weird.hs --- a/bench/weird.hs +++ b/bench/weird.hs @@ -16,12 +16,12 @@ _ ^^^ _ = 0 main :: IO () -main = do +main = do conjure "^^^" (^^^) primitives conjureWith args{usePatterns = False} "^^^" (^^^) primitives primitives :: [Prim] -primitives = +primitives = [ pr (0::Int) , pr (1::Int) , prim "+" ((+) :: Int -> Int -> Int) diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -2,6 +2,14 @@ ============================ +v0.5.12 (February 2024) +----------------------- + +* bump Speculate requirement to v0.4.20 +* improve testing of Conjure itself +* improvements and fixes of Conjure's benchmarks + + v0.5.10 (February 2024) ----------------------- diff --git a/code-conjure.cabal b/code-conjure.cabal --- a/code-conjure.cabal +++ b/code-conjure.cabal @@ -3,7 +3,7 @@ -- Copyright (C) 2021-2024 Rudy Matela -- Distributed under the 3-Clause BSD licence (see the file LICENSE). name: code-conjure -version: 0.5.10 +version: 0.5.12 synopsis: synthesize Haskell functions out of partial definitions description: Conjure is a tool that synthesizes Haskell functions out of partial definitions. @@ -51,7 +51,9 @@ , bench/time , test/mk , test/sdist -tested-with: GHC==9.4 +tested-with: GHC==9.8 + , GHC==9.6 + , GHC==9.4 , GHC==9.2 , GHC==9.0 , GHC==8.10 @@ -65,7 +67,7 @@ source-repository this type: git location: https://github.com/rudymatela/conjure - tag: v0.5.10 + tag: v0.5.12 library exposed-modules: Conjure @@ -84,7 +86,7 @@ build-depends: base >= 4 && < 5 , leancheck >= 1.0.0 , template-haskell - , speculate >= 0.4.14 + , speculate >= 0.4.20 , express >= 1.0.16 hs-source-dirs: src default-language: Haskell2010 diff --git a/eg/fib01.txt b/eg/fib01.txt --- a/eg/fib01.txt +++ b/eg/fib01.txt @@ -11,7 +11,7 @@ fib01 :: Int -> Int -> Int -> Int -- testing 8 combinations of argument values --- pruning with 18/37 rules +-- pruning with 18/38 rules -- looking through 4 candidates of size 1 -- looking through 4 candidates of size 2 -- looking through 10 candidates of size 3 diff --git a/mk/haskell.mk b/mk/haskell.mk --- a/mk/haskell.mk +++ b/mk/haskell.mk @@ -1,6 +1,6 @@ # Implicit rules for compiling Haskell code. # -# Copyright (c) 2015-2023 Rudy Matela. +# Copyright (c) 2015-2024 Rudy Matela. # Distributed under the 3-Clause BSD licence. # # You can optionally configure the "Configuration variables" below in your main @@ -91,9 +91,14 @@ install-dependencies: if [ -n "$(INSTALL_DEPS)" ]; then \ + cd ~ && \ cabal update && \ - $(CABAL_INSTALL) $(INSTALL_DEPS); \ + $(CABAL_INSTALL) $(INSTALL_DEPS) || true; \ fi + # above, "|| true" is needed for cabal >= 3.10.2 + # Before, cabal would successfully skip installation + # of already existing packages + # cd ~ is needed so cabal installs only dependencies # haddock rules haddock: doc/index.html diff --git a/src/Conjure/Defn/Test.hs b/src/Conjure/Defn/Test.hs --- a/src/Conjure/Defn/Test.hs +++ b/src/Conjure/Defn/Test.hs @@ -13,6 +13,7 @@ ( equalModuloTesting , erroneousCandidate , findDefnError + , listDefnErrors ) where @@ -52,9 +53,14 @@ -- Warning: this is an experimental function -- which may be taken out of the API at any moment. findDefnError :: Conjurable f => Int -> Int -> String -> f -> Defn -> Maybe Expr -findDefnError maxTests maxEvalRecursions nm f d = - find is testGrounds +findDefnError maxTests maxEvalRecursions nm f = + listToMaybe . listDefnErrors maxTests maxEvalRecursions nm f + + +listDefnErrors :: Conjurable f => Int -> Int -> String -> f -> Defn -> [Expr] +listDefnErrors maxTests maxEvalRecursions nm f d = filter is testGrounds where + testGrounds :: [Expr] testGrounds = nonNegativeAppGrounds maxTests maxEvalRecursions nm f is :: Expr -> Bool is e = isError (devlEqual maxEvalRecursions f d d e) diff --git a/src/Conjure/Reason.hs b/src/Conjure/Reason.hs --- a/src/Conjure/Reason.hs +++ b/src/Conjure/Reason.hs @@ -74,6 +74,10 @@ commutativeOperators :: Thy -> [Expr] commutativeOperators thy = [ ef | (ef :$ ex :$ ey, ef' :$ ey' :$ ex') <- equations thy + , isConst ef + , isVar ex + , isVar ey + , ex /= ey , ef == ef' , ex == ex' , ey == ey' diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -10,5 +10,5 @@ extra-deps: - leancheck-1.0.2 -- speculate-0.4.14 +- speculate-0.4.20 - express-1.0.16 diff --git a/test/mk b/test/mk --- a/test/mk +++ b/test/mk @@ -26,7 +26,7 @@ } make -s ls-eg ls-test | sort >$tmp/ls-mk -find eg bench proto test -name '*.hs' -maxdepth 1 | flt | sort >$tmp/ls-find +find eg bench proto test -maxdepth 1 -name '*.hs' | flt | sort >$tmp/ls-find grep -E "^[^/]*/[^.]*:" mk/depend.mk | flt | sort >$tmp/ls-depend grep -E "(eg|bench|proto|test)/" .gitignore | flt | sort >$tmp/ls-gitignore $diff $tmp/ls-{mk,find} # compares make variables with actual directory diff --git a/test/sdist b/test/sdist --- a/test/sdist +++ b/test/sdist @@ -2,7 +2,7 @@ # # test/sdist: tests the package generated by "cabal sdist". # -# Copyright (c) 2015-2023 Rudy Matela. +# Copyright (c) 2015-2024 Rudy Matela. # Distributed under the 3-Clause BSD licence. set -xe