8455 Commits (0475e79d0ecf3aedcdfa1070a0046aceaa3034b8)
 

Author SHA1 Message Date
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
Josh Berdine ef0dfe0d70 [sledge] Fix doc of List.remove_exn
5 years ago
Dulma Churchill bdba1db6ef [biabduction] Remove the flags for modelling alloc and release functions that are unused
5 years ago
Dulma Churchill 2d168f75a6 [pulse] Add options for modelling alloc models and free models from user-defined regexes.
5 years ago
David Pichardie b22f7c83d5 Java source baby parser for class declaration locations
5 years ago
Daiva Naudziuniene db965085b9 Fix tests
5 years ago
Mitya Lyubarskiy c4c8c053a1 [nullsafe] Treat not annotated synthetic fields as StrictNonnull
5 years ago
Jules Villard 6247437296 [pulse] unified API for arithmetic
5 years ago
Jules Villard 0a8ad85596 [pulse][minor] rename AbductiveDomain.Domain -> AbductiveDomain.PostDomain
5 years ago
Jules Villard af2aaf2a14 [pulse][minor] remove skipped_calls getter
5 years ago
Jules Villard bb9726bbd7 [pulse] enforce short forms for PulseDomainInterface
5 years ago
Jules Villard 94e3b06900 [pulse] enforce short forms for PulseBasicInterface
5 years ago
Jules Villard a0d1fee1dc [pulse] move SkippedCalls to its own file
5 years ago
Jules Villard c00de7ad27 [pulse] move interproc call to its own file
5 years ago
Jules Villard 9ed10d435b [pulse][minor] simplify rewriting of callee post attributes
5 years ago
Mitya Lyubarskiy 1eb762f935 [nullsafe] Recommend "trust none" as a promotion mode, when it is possible.
5 years ago