Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: nick8325/twee
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: twee-2.0
Choose a base ref
...
head repository: nick8325/twee
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: master
Choose a head ref
4 contributors
Loading
Showing with 17,004 additions and 3,099 deletions.
  1. +6 −0 .hgtags
  2. +1 −1 LICENSE
  3. +0 −10 README
  4. +22 −0 README.md
  5. +1 −0 cabal.project
  6. +1 −594 executable/Main.hs
  7. +65 −0 executable/ParallelMain.hs
  8. +1,076 −0 executable/SequentialMain.hs
  9. +12 −0 executable/link.c
  10. +208 −0 misc/BestTwee.hs
  11. +114 −0 misc/Localise.hs
  12. +63 −0 misc/MaxCover.hs
  13. +334 −0 misc/Test.hs
  14. +10 −10 misc/bench.hs
  15. +111 −0 misc/magic.py
  16. +50 −0 misc/print_trace.pl
  17. +8 −0 misc/starexec/bin/parallel-twee
  18. +2 −0 misc/starexec/bin/starexec_run_twee
  19. +0 −129 misc/test.hs
  20. +6 −0 notes/ac plus
  21. +0 −53 notes/ideas
  22. +0 −25 notes/kbc simplifier notes
  23. +0 −92 notes/to do
  24. +34 −0 patches/Historical.hs
  25. +25 −0 patches/MemoFun.hs
  26. +33 −0 patches/MultiIndex.hs
  27. +52 −0 patches/Nested.hs
  28. +245 −0 patches/cancellation.patch
  29. +267 −0 patches/cereal.patch
  30. +130 −0 patches/dynarr.patch
  31. +21 −0 patches/equals-div-2.patch
  32. +117 −0 patches/fifo.patch
  33. +51 −0 patches/flatten-difficult-axioms.patch
  34. +635 −0 patches/history.patch
  35. +48 −0 patches/improve-cp.patch
  36. +72 −0 patches/induction-demo.patch
  37. +273 −0 patches/more-work-with-size.patch
  38. +84 −0 patches/multicp.patch
  39. +134 −0 patches/noindex.patch
  40. +583 −0 patches/noproof.patch
  41. +24 −0 patches/requeue.patch
  42. +79 −0 patches/skip-skolem.patch
  43. +565 −0 patches/st.patch
  44. +136 −0 patches/strict-deriv.patch
  45. +137 −0 patches/strict-proofs.patch
  46. +117 −0 patches/subsumption.patch
  47. +166 −0 patches/use_ground_joinable_for_rewriting.patch
  48. +1,196 −0 patches/work-on-size.patch
  49. +465 −0 patches/working-subst.patch
  50. +145 −0 src/Data/BatchedQueue.hs
  51. +7 −5 src/{Twee → Data}/ChurchList.hs
  52. +34 −16 src/{Twee/Array.hs → Data/DynamicArray.hs}
  53. +140 −0 src/Data/Heap.hs
  54. +42 −16 src/{Twee → Data}/Label.hs
  55. +89 −0 src/Data/Numbered.hs
  56. +45 −0 src/Data/PackedSequence.hs
  57. +3 −0 src/Data/Primitive/ByteArray/Checked.hs
  58. +14 −0 src/Data/Primitive/Checked.hs
  59. +3 −0 src/Data/Primitive/SmallArray/Checked.hs
  60. +30 −0 src/LICENSE
  61. +631 −318 src/Twee.hs
  62. +163 −122 src/Twee/Base.hs
  63. +170 −128 src/Twee/CP.hs
  64. +34 −18 src/Twee/Constraints.hs
  65. +38 −26 src/Twee/Equation.hs
  66. +121 −0 src/Twee/Generate.hs
  67. +0 −130 src/Twee/Heap.hs
  68. +452 −128 src/Twee/Index.hs
  69. +0 −119 src/Twee/Index/Lookup.hs
  70. +106 −71 src/Twee/Join.hs
  71. +92 −18 src/Twee/KBO.hs
  72. +61 −25 src/Twee/Pretty.hs
  73. +155 −0 src/Twee/Profile.hs
  74. +601 −306 src/Twee/Proof.hs
  75. +622 −223 src/Twee/Rule.hs
  76. +11 −14 src/Twee/Rule/Index.hs
  77. +15 −11 src/Twee/Task.hs
  78. +349 −135 src/Twee/Term.hs
  79. +214 −166 src/Twee/Term/Core.hs
  80. +103 −26 src/Twee/Utils.hs
  81. +104 −0 src/twee-lib.cabal
  82. +5 −5 stack.yaml
  83. +19 −5 tests/{semigroup2.p → GRP196-1.p}
  84. +63 −0 tests/GRP666-4.p
  85. +4 −4 tests/{nand.p → LAT071-1.p}
  86. +37 −0 tests/LAT073-1.p
  87. +106 −0 tests/PUZ037-3-2.p
  88. +110 −0 tests/PUZ037-3.p
  89. +129 −0 tests/PUZ052-1.p
  90. +14 −0 tests/REL038-1.p
  91. +9 −0 tests/RNG025-buggy.p
  92. +12 −0 tests/RNG035-7.p
  93. +56 −0 tests/ROB027-1-pretty.p
  94. +56 −0 tests/ROB027-1.p
  95. +1,759 −0 tests/ROB027-1.proof
  96. +10 −0 tests/ROB033-1.p
  97. +3 −3 tests/append-rev.p
  98. +3 −0 tests/cm.p
  99. +0 −17 tests/db.p
  100. +1,344 −0 tests/db.proof
  101. +37 −0 tests/deriv.p
  102. +8 −4 tests/diff.p
  103. +44 −0 tests/factor.p
  104. +74 −0 tests/gmv.p
  105. +14 −0 tests/group.p
  106. +18 −9 tests/gt6.tptp.p
  107. +170 −0 tests/haken.p
  108. +0 −16 tests/lat.p
  109. +0 −7 tests/lcl.p
  110. +6 −6 tests/loop.p
  111. +6 −6 tests/loop2.p
  112. +10 −0 tests/minus.p
  113. +36 −18 tests/nicomachus.p
  114. +32 −0 tests/rel.p
  115. +32 −0 tests/rel2.p
  116. +27 −0 tests/rellat_appendixa.p
  117. +28 −0 tests/rellat_appendixb.p
  118. +30 −0 tests/rellat_appendixb_easier.p
  119. +30 −0 tests/rellat_appendixc.p
  120. +32 −0 tests/rellat_theorem34_6.p
  121. +29 −0 tests/rellat_theorem34_6a.p
  122. +29 −0 tests/rellat_theorem34_6b.p
  123. +9 −0 tests/ring2-cancel.p
  124. +38 −0 tests/sam.p
  125. +1 −0 tests/satisfiable/abelian.p
  126. +1 −0 tests/satisfiable/and-or.p
  127. +6 −0 tests/satisfiable/bad-ac.p
  128. +3 −0 tests/satisfiable/commutativity-bad.p
  129. +1 −0 tests/satisfiable/groupoid.p
  130. +1 −0 tests/satisfiable/length.p
  131. +1 −0 tests/satisfiable/length2.p
  132. +1 −0 tests/satisfiable/length3.p
  133. +1 −0 tests/satisfiable/martin-nipkow-2.p
  134. +1 −0 tests/satisfiable/martin-nipkow-3.p
  135. +1 −0 tests/satisfiable/martin-nipkow.p
  136. +1 −0 tests/satisfiable/plus-combinator.p
  137. +1 −0 tests/satisfiable/plus-times.p
  138. +1 −0 tests/satisfiable/plus.p
  139. +1 −0 tests/satisfiable/pretty.p
  140. +11 −0 tests/satisfiable/veroff.p
  141. +32 −0 tests/union.tptp
  142. +18 −0 tests/vbool.p
  143. +11 −0 tests/veroff-short.p
  144. +11 −0 tests/veroff.p
  145. 0 tests/{winkler-easy.p → winker-easy.p}
  146. 0 tests/{winkler.p → winker.p}
  147. 0 tests/{winkler2.p → winker2.p}
  148. +4 −0 tests/y-easy.p
  149. +5 −0 tests/y-encoded.p
  150. +3 −3 tests/y.p
  151. +36 −61 twee.cabal
6 changes: 6 additions & 0 deletions .hgtags
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
972ce3b158a3aa15635d97df50d2d9f4a79935c1 2.3
972ce3b158a3aa15635d97df50d2d9f4a79935c1 2.3
d5b711974520f288880ab19bf5368460c49ecb50 2.3
2c842bc4aecdb6e7d2faefe78558b80db5345eee 2.3.1
dbd094b7fdfa201a7fb6e6d1faca448983a89835 2.4
035f2b1250431364d46d1cfabe7f3ca71d16109b 2.4.2
2 changes: 1 addition & 1 deletion LICENSE
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Copyright (c) 2015, Nick Smallbone
Copyright (c) 2015-2017, Nick Smallbone

All rights reserved.

10 changes: 0 additions & 10 deletions README
View file

This file was deleted.

22 changes: 22 additions & 0 deletions README.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
This is twee, an equational theorem prover.

The version in this git repository is likely to be unstable!
To install the latest stable version, run:

cabal install twee

If you have LLVM installed, you can get a slightly faster version by
running:

cabal install twee -fllvm

If you really want the latest unstable version, run
`cabal install src/ .` in this repository.

Afterwards, run `twee nameofproblem.p`. The problem should be in TPTP
format (http://www.tptp.org). You can find a few examples in the
`tests` directory. All axioms and conjectures must be equations, but
you can freely use quantifiers. If it succeeds in proving your
problem, twee will print a human-readable proof.

For the official manual, see http://nick8325.github.io/twee.
1 change: 1 addition & 0 deletions cabal.project
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
packages: ./*.cabal src/twee-lib.cabal
Loading