8070 Commits (3bc350331deb1ec26e9db2e0b555bec32e7d0712)
 

Author SHA1 Message Date
Scott Owens 49d95f40a2 [sledge sem] Adds a theorem about block processing order
5 years ago
Nikos Gorogiannis 3b46c3b4da [racerd] refactor analysis driver function
5 years ago
Sungkeun Cho 572af451a9 [inferbo] Sanity check when constructing a set of known locations
5 years ago
Mitya Lyubarskiy 6a75ba6429 [nullsafe] Take into account Lambda classes in JavaClassName
5 years ago
Sungkeun Cho 2152af123d [inferbo] Remove dead check in appending field to location
5 years ago
Mitya Lyubarskiy 54c4715adc [nullsafe] Specify the right class location in meta-issue info
5 years ago
Scott Owens 8d49b8d6ef [sledge sem] Remove some proof cheats
5 years ago
Scott Owens 9327f41880 [sledge sem] Organise the tranlation corectness proof
5 years ago
Scott Owens 2a6ababa99 [sledge sem] Rework emap invariant
5 years ago
Sungkeun Cho 30ca51366d [inferbo] Do not append field to the unknown location
5 years ago
Josh Berdine 6e4a729ab6 [sledge] Do not add simple constants to Equality relation representation
5 years ago
Josh Berdine 1b5302b4d2 [sledge] Simplify remainder of a rational by an integer
5 years ago
Josh Berdine fcd0e41ee6 [sledge] Return early for == args in Term compare and equal
5 years ago
Josh Berdine 76695690b8 [sledge] Do not simplify Mul and Div terms
5 years ago
Josh Berdine a3a6a5a6fe [sledge] Do not solve for Integer constants
5 years ago
Josh Berdine 32c5fb2837 [sledge] Do not represent Equality rep sparsely on constants
5 years ago
Josh Berdine de1689ac87 [sledge] Change And and Or terms from binary to flattened n-ary
5 years ago
Josh Berdine 87c8eb7c3a [sledge] Strengthen normalization of division
5 years ago
Josh Berdine cd72d3a82e [sledge] Simplify Term.Sum.to_term
5 years ago
Josh Berdine 2fc8bc1f84 [sledge] Export Term.map_rec_pre and add Term.fold_map_rec_pre
5 years ago
Josh Berdine 548928a839 [sledge] Strengthen Equality invariant to ensure carrier closed under subterms
5 years ago
Josh Berdine 2124be1c71 [sledge] Remove the "simplified" intermediate between interpreted and uninterpreted
5 years ago
Josh Berdine ee595f2ebf [sledge] Strengthen Equality.close to handle rep being sparse on constants
5 years ago
Josh Berdine 2f4f9801ed [sledge] Add Term.is_constant
5 years ago
Josh Berdine c91e09031f [sledge] Strengthen Equality normalization
5 years ago
Josh Berdine 0f50d3c248 [sledge] Do not solve polynomials for Mul or Div terms
5 years ago
Josh Berdine eb750ba6f9 [sledge] Avoid cyclic solutions to polynomial equations
5 years ago
Josh Berdine 1b20f02052 [sledge] Strengthen normalization of division, avoiding non-reals
5 years ago
Josh Berdine 4ea9eced05 [sledge] Improve Term.Sum.to_term
5 years ago
Josh Berdine 1a34e7eed2 [sledge] Add rational constants
5 years ago
Josh Berdine 7b33996072 [sledge] Use term height to avoid "pumpable" cyclic equations in Equality
5 years ago
Josh Berdine 6c03d88cf7 [sledge] Move Term.agg_size
5 years ago
Josh Berdine 0cee03aaa1 [sledge] Simplify identity type conversions only at initial construction
5 years ago
Josh Berdine 7e4673cbeb [sledge] Improve Equality invariant checking and debugging support
5 years ago
Josh Berdine 3c0924cf01 [sledge] Minor code improvement
5 years ago
Josh Berdine 60df5d6f3a [sledge] Fix Equality.Subst.compose to preserve physical equality
5 years ago
Josh Berdine 013b948dc4 [sledge] Rename extend to compose1 to avoid potential shadowing confusion
5 years ago
Josh Berdine fddb2fa991 [sledge] Add Map.map_endo
5 years ago
Josh Berdine ef63683a16 [sledge] Add Term.fold_map
5 years ago
Josh Berdine b35e3d30e0 [sledge] Add Map.fold_until
5 years ago
Josh Berdine b09f3774a4 [sledge] Add Qset.is_empty
5 years ago
Josh Berdine 165454e17d [sledge] Add Map and Qset operations to access top of underlying tree
5 years ago
Josh Berdine 7fdd3cccbb [sledge] Add Option.or_else
5 years ago
Josh Berdine 2aacc03880 [sledge] Remove eliminated existentials from equality relations
5 years ago
Josh Berdine 30c23f8cd6 [sledge] Fix term ordering bug between monomials and vars
5 years ago
Josh Berdine e7217ac5fe [sledge] Check equality of logical variables by id only
5 years ago
Josh Berdine c8e75e3b82 [sledge] Dump perf diagnostics and replays for slow queries to stderr
5 years ago
Josh Berdine a4e523b5b6 [sledge] Rename `*_preserves_phys_equal` to `*_endo` and clarify docs
5 years ago
Josh Berdine ec52259d31 [sledge] Substitute out alias of option when including Monad_syntax
5 years ago
Josh Berdine 1ae192dc0e [sledge] Use __LOC__ for Not_found_s
5 years ago